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.

  1. 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.

  2. 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.

  3. 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.

  4. 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.

  5. 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.

  6. 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.

  7. 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.

  8. 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.

  9. 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

  1. 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.

  2. 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.

  3. 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.

  4. 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.

  5. 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.

  6. 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

  1. 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.

  2. 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.

  3. 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.

  4. 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