TRAIAN 3.4 released on June 29, 2021
The CONVECS team is pleased to announce
that version 3.4 of the TRAIAN compiler for LOTOS NT is available.
Release Notes
TRAIAN 3.4 has been prepared by Hubert Garavel, Frederic Lang, and
Wendelin Serwe. It was released four months after
version 3.3 of TRAIAN.
TRAIAN 3.4 brings nine language changes, six code-generation changes, and
four bug fixes (see below their description).
Language Changes
TRAIAN 3.4 introduces various changes to the LOTOS NT language in order to
further align it with the LNT language supported by the
CADP toolbox. The LOTOS NT Reference Manual
and the style files for text editors have been updated to reflect these
changes.
-
To further align LOTOS NT with LNT, the syntax of the "case"
instruction was simplified. From now on, one should write:
case E
var X:T in
...
end case
rather than:
case E in
var X:T in
...
end case
i.e., the double "in" is suppressed. Users should update their
existing LOTOS NT programs by running the following command:
traian_upc 2021-LOTNT-CASE-VAR [<file> or <directory>]
See item 266 in the HISTORY.txt file.
-
The syntax of functions was extended by introducing an "assert"
instruction. The LOTOS NT manual was updated. For this purpose, the predefined
library "lotosnt_exceptions" was modified as follows:
- Function TRAIAN_ADTI_do_raise_exception() was extended
with a 6th parameter.
- A new function TRAIAN_ADTI_exception_get_kind() was
added.
- A new function TRAIAN_ADTI_raise_event() was added.
- Function TRAIAN_ADTI_raise_exception_with_data() is now
deprecated and kept for backward compatibility; it is no longer
invoked in the C code generated by TRAIAN.
See item 267 in the HISTORY.txt file.
-
To increase syntactic compatibility between LOTOS NT and LNT, it is now
possible to have the "raise" keyword in the event parameter lists of
function and process declarations (this is permitted in LNT, but has been
prohibited so far in LOTOS NT). From now on, the "raise" keyword in
event parameter lists is syntactically tolerated by TRAIAN, but the following
warning message is emitted:
"raise" before event declaration is deprecated and should be removed (12 occurrences found)
See item 269 in the HISTORY.txt file.
-
The syntax of LOTOS NT processes was extended by adding a "raise"
behaviour. The LOTOS NT manual was updated.
See item 270 in the HISTORY.txt file.
-
The syntax of LOTOS NT processes was extended by adding an "assert"
behaviour. The LOTOS NT manual was updated.
See item 271 in the HISTORY.txt file.
-
Preconditions ("require") have been introduced in both LOTOS NT
functions and processes. The LOTOS NT manual was updated accordingly.
See item 273 in the HISTORY.txt file.
-
Postconditions ("ensure") have been introduced in both LOTOS NT
functions and processes (with syntax extensions "result",
"X.in", and "X.out"). The LOTOS NT manual was updated
accordingly.
See item 275 in the HISTORY.txt file.
-
The syntax of functions was extended by introducing an
"access E0, ..., En" instruction, where
E0, ..., En are distinct event identifiers declared in
the environment. This instruction eliminates warnings (currently generated
by the C compiler) indicating that these events are not used. The LOTOS NT
manual was updated accordingly.
See item 283 in the HISTORY.txt file.
-
In order to increase the compatibility between LOTOS NT and LNT, the syntax
of LOTOS NT processes has been extended as follows:
- Modules can now contain more than one process definition.
- Processes can now have variable parameters.
- Processes can now have no event parameters.
- Processes now support the "null" behaviour.
- Processes now support variable declarations ("var").
- Processes now support assignments to variables.
- Processes now support nondeterministic assignments ("any").
- Processes now support "use" behaviours.
- Processes now support "access" behaviours.
- Processes now support function and procedure calls ("eval").
- Processes now support "if...then...else"
behaviours.
- Processes now support "loop" (with "break")
behaviours.
- Processes now support "for...loop" behaviours.
- Processes now support "while...loop" behaviours.
- Communication actions are now more general, with emissions
and/or receptions, named or positional mode, and an optional
"where" clause.
- Processes now support "select" (with "only if")
behaviours.
- Processes now support "par" behaviours.
- Processes now support "hide" behaviours.
- Processes now support "trap" behaviours.
- Processes now support "disrupt" behaviours.
- Processes now support process calls.
So far, these extensions are merely syntactical, meaning that
they are accepted by the lexer and parser of TRAIAN, but not
further analyzed. In later semantic phases, an error message
of the following form:
limitation: [...] processes not yet fully implemented
is emitted if any of such extensions is met.
See item 284 in the HISTORY.txt file.
Code-Generation Changes
-
The C code generated for LOTOS NT functions was modified, so as to ensure
that each function that terminates normally (i.e., whose execution is not
halted by an exception) has a unique exit point. In the generated C code,
a label TRAIAN_RETURN was introduced to reference this exit point.
Normal termination of the function is thus implemented by a
"goto TRAIAN_RETURN" statement. The actions to be executed
upon normal termination of the function are put just after the
TRAIAN_RETURN label.
See item 274 in the HISTORY.txt file.
-
The predefined library "lotosnt_exceptions" was extended by introducing a
new function named TRAIAN_ADTI_TRAP_ERROR(), which is invoked from
the C code generated by TRAIAN.
See item 276 in the HISTORY.txt file.
-
The C code generation was extended to support external LOTOS NT functions
having preconditions and/or postconditions.
See item 277 in the HISTORY.txt file.
-
The C code generated by TRAIAN was modified so that the error messages arising
from a "raise" statement, an "assert" statement, a precondition,
a postcondition, or a "case" statement that offers no valid branch for
pattern matching now display the file name and line number of the source
LOTOS NT code instead of the file name and line number of the C code generated
by TRAIAN.
See item 279 in the HISTORY.txt file.
-
The readability of the C code generated by TRAIAN was enhanced by:
- removing extra spaces and adding missing ones,
- removing extra newlines and adding missing ones,
- better indenting the C code, and
- removing useless "default: break" statements.
See item 280 in the HISTORY.txt file.
-
The size of the C code produced by TRAIAN was shortened and this code was
made safer and more readable by renaming numerous C identifiers generated
by TRAIAN. Specifically, the following renamings have been applied:
DATA -> TRAIAN_DATA
NEXT -> TRAIAN_NEXT
TRAIAN_ADT -> TRAIAN_VERSION
TRAIAN_ADT_0 -> TRAIAN_0
TRAIAN_ADT_1 -> TRAIAN_1
TRAIAN_ADT_2 -> TRAIAN_2
TRAIAN_ADT_ALLOC -> TRAIAN_ALLOC
TRAIAN_ADT_BITS_%s -> TRAIAN_BITS_%s
TRAIAN_ADT_BODY_%s -> TRAIAN_BODY_%s
TRAIAN_ADT_BODY_HASH_ENTRY_%s -> TRAIAN_ITEMSTRUCT_%s
TRAIAN_ADT_BOUND_%s -> TRAIAN_BOUND_%s
TRAIAN_ADT_CASE_%s -> TRAIAN_ENUMVAL_%s
TRAIAN_ADT_CASEVAR_%s -> TRAIAN_CASEVAR_%s
TRAIAN_ADT_CONSTR_%s -> TRAIAN_RECORD_%s
TRAIAN_ADT_ENUM_%s (if a value) -> TRAIAN_ENUM_%s
TRAIAN_ADT_ENUM_%s (if an iterator) -> TRAIAN_ENUMERATE_%s
TRAIAN_ADT_EQ_%s -> TRAIAN_EQ_%s
TRAIAN_ADT_FIELD_%s -> TRAIAN_FIELD_%s
TRAIAN_ADT_FILE -> TRAIAN_FILE
TRAIAN_ADT_FUN_%s -> TRAIAN_FUNCTION_%s
TRAIAN_ADT_GE_%s -> TRAIAN_GE_%s
TRAIAN_ADT_Get_1_ADT_SUCC -> TRAIAN_GET_1_ADT_SUCC
TRAIAN_ADT_GET_%s -> TRAIAN_GET_%s
TRAIAN_ADT_GT_%s -> TRAIAN_GT_%s
TRAIAN_ADT_HASH_%s_INSERT -> TRAIAN_INSERT_%s
TRAIAN_ADT_HASH_%s_LOOKUP -> TRAIAN_LOOKUP_%s
TRAIAN_ADT_HASH_PJW -> TRAIAN_PJW
TRAIAN_ADT_HASH_ENTRY_%s -> TRAIAN_ITEM_%s_
TRAIAN_ADT_HASH_SIZE_%s -> TRAIAN_SIZE_%s_
TRAIAN_ADT_HASH_TABLE_%s -> TRAIAN_TABLE_%s_
TRAIAN_ADT_INCLUDE_%s -> TRAIAN_INCLUDE_%s
TRAIAN_ADT_INDEX -> TRAIAN_0
TRAIAN_ADT_INT_STEP_%s -> TRAIAN_STEP_%s
TRAIAN_ADT_is_%s -> TRAIAN_MATCH_%s
TRAIAN_ADT_LE_%s -> TRAIAN_LE_%s
TRAIAN_ADT_LOCAL_%s -> TRAIAN_VAR_%s
TRAIAN_ADT_LT_%s -> TRAIAN_LT_%s
TRAIAN_ADT_MAX_%s -> TRAIAN_MAX_%s
TRAIAN_ADT_NE_%s -> TRAIAN_NE_%s
TRAIAN_ADT_NO_ITERATOR -> TRAIAN_NO_ITERATOR
TRAIAN_ADT_O -> TRAIAN_1
TRAIAN_ADT_POINTER_%s -> TRAIAN_POINTER_%s
TRAIAN_ADT_PRINT_%s -> TRAIAN_PRINT_%s
TRAIAN_ADT_SCALAR_%s -> TRAIAN_SCALAR_%s
TRAIAN_ADT_SINGLETON -> TRAIAN_SINGLETON
TRAIAN_ADT_SIGNAL -> TRAIAN_SIGNAL
TRAIAN_ADT_SIGNAL_%s -> TRAIAN_EVENT_%s
TRAIAN_ADT_STAR_%s -> TRAIAN_STAR_%s
TRAIAN_ADT_STRUCT_%s -> TRAIAN_STRUCT_%s
TRAIAN_ADT_TEMP -> either TRAIAN_RESULT or TRAIAN_TMP
TRAIAN_ADT_TEMP_1 -> either TRAIAN_TMP or TRAIAN_TMP_1
TRAIAN_ADT_TEMP_2 -> either TRAIAN_TMP or TRAIAN_TMP_2
TRAIAN_ADT_TEMP_%d -> TRAIAN_TMP_%d
TRAIAN_ADT_TMP -> TRAIAN_2
TRAIAN_ADT_TO_STRING_%s -> TRAIAN_STRINGIFY_%s
TRAIAN_ADT_TYPE_%s -> TRAIAN_TYPE_%s
TRAIAN_ADT_UNION_%s -> TRAIAN_UNION_%s
TRAIAN_ADT_UPDATE_%s -> TRAIAN_UPDATE_%s
TRAIAN_ADT_VARIABLE -> TRAIAN_CLOBBERED
TRAIAN_HASH_VALUE -> TRAIAN_HASH
Some of these renamings have been applied as well to the LOTOS NT predefined
libraries. For instance, the function TRAIAN_ADT_HASH_PJW() has been
renamed to TRAIAN_PJW() in "lotosnt_hash.h". Also, the following
renamings:
TRAIAN_ADT_BITS_ADT_BOOL -> TRAIAN_BITS_ADT_BOOL
TRAIAN_ADT_Get_1_ADT_SUCC -> TRAIAN_GET_1_ADT_SUCC
TRAIAN_ADT_is_%s -> TRAIAN_MATCH_%s
TRAIAN_ADT_SCALAR_%s -> TRAIAN_SCALAR_%s
have been applied to "lotosnt_predefined".
See item 281 in the HISTORY.txt file.
Bug Fixes
-
The C functions generated by TRAIAN for converting numeral types (i.e.,
types whose definition is isomorphic to natural numbers) to strings did
not allocate enough memory to store the literal string representing the
constructor corresponding to the value '0' (one byte was missing). This was reported by a Gcc warning:
xxx_t.h: In function 'TRAIAN_ADT_TO_STRING_XXX':
xxx_t.h:XXX:XXX: warning: 'sprintf' writing a terminating nul
past the end of the destination [-Werror=format-overflow=]
See item 268 in the HISTORY.txt file.
-
Formerly, it was not possible to call a function F from the principal
process P by passing to F an event parameter E declared
in P, e.g.:
process P [PRINT: any, E: none] is
PRINT (F [E] (0))
end process
To make this possible, the C code generated by TRAIAN was modified, so that
functions can be called with event parameters from the principal process.
This was done by adding an implicit "trap" for event parameters.
See item 272 in the HISTORY.txt file.
-
In process definitions, value expressions containing function calls with
the ellipsis notation "..." were not properly checked, so that potential
errors could remain undetected. The new version of TRAIAN performs more
stringent semantic checks.
See item 278 in the HISTORY.txt file.
-
The C code generator of TRAIAN was modified to avoid duplicated "forward"
declarations of the TRAIAN_GET_*() functions. Such duplicated definitions
were harmless, but annoying.
See item 282 in the HISTORY.txt file.
Future Work
TRAIAN 3.4 will continue to evolve, our goal being to merge LOTOS NT and LNT
in one single language.
Download
TRAIAN 3.4 can be freely downloaded from the
TRAIAN Web Page located at:
http://vasy.inria.fr/traian