TRAIAN 3.2 released on October 29, 2020

The CONVECS team is pleased to announce that version 3.2 of the TRAIAN compiler for LOTOS NT is available.

Release Notes

TRAIAN 3.2 brings nine language changes, twelve code-generation changes, three miscellaneous changes, and nine bug fixes (see below their description).

Language Changes

TRAIAN 3.2 introduces various changes to the LOTOS NT language in order to progressively 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. All syntactic constructs deprecated in TRAIAN 3.1 are now forbidden in TRAIAN 3.2, namely: "inout" notation, "case...is" instruction, "[...]" conditions for pattern, "raises" notation, "for...do" loop, and "while...do" loop. Consequently, "inout", "raises", and "do" are no longer reserved keywords of LOTOS NT. Users are advised to upgrade their source LOTOS NT files using the "traian_upc" command with the following options:

      2020-LOTNT-INOUT             2020-LOTNT-CASE-IS         2020-LOTNT-CASE-CONDITIONS
      2020-LOTNT-FUNCTION-RAISES   2020-LOTNT-UPDATE-RAISES   2020-LOTNT-PREFIX-RAISES
      2020-LOTNT-INFIX-RAISES      2020-LOTNT-FOR-DO          2020-LOTNT-WHILE-DO
   

   See items 210, 190-193, and 196-200 in the HISTORY.txt file.


2. To align LOTOS NT with LNT, the "=>" symbol used in positional parameter lists has been replaced by the "->" symbol. Users are advised to upgrade their source LOTOS NT files using the command:

      traian_upc 2020-LOTNT-ARROWS [<file> or <directory>]
   

   See item 212 in the HISTORY.txt file.


3. To align LOTOS NT with LNT, the following keywords are now reserved in LOTOS NT: "access", "alt", "array", "assert", "disrupt", "ensure", "hide", "only", "par", "range", "require", "result", "select", "set", "sorted", and "use". Users are advised to upgrade their source LOTOS NT files using the command:

      traian_upc 2020-LOTNT-KEYWORDS [<file> or <directory>]
   

   See item 213 in the HISTORY.txt file.


4. LOTOS NT has been extended with a simple form of process definition consisting in a sequence of communication actions, which can be used to compute and display the result of expressions. See item 217 in the HISTORY.txt file.


5. Previously, TRAIAN rejected incomplete "case" instructions when it could not prove statically that all possible values are covered by at least one branch. From now on, potentially incomplete "case" instructions are tolerated but a compile-time warning is emitted. If they are actually incomplete, a fatal error will occur at run-time. See item 227 in the HISTORY.txt file.


6. LOTOS NT was extended to support "case" instructions with multiple values (e.g. "case X+1, Y+1, Z in ..."); previously only one single value was supported. See item 228 in the HISTORY.txt file.


7. The integer division operator on values of type "nat" or "int" is no longer noted "/" but "div". From now on, "div" is a reserved keyword. Users are advised to upgrade their source LOTOS NT files using the command:

      traian_upc 2020-LOTNT-DIV-MOD-REM [<file> or <directory>]
   

   See item 236 in the HISTORY.txt file.


8. The integer modulus operator on values of type "nat" or "int" is no longer noted "%" but either "mod" (on "nat" or "int" values) or "rem" (on "int" values). From now on, "mod" and "rem" are reserved keywords. Users are advised to upgrade their source LOTOS NT files using the command:

      traian_upc 2020-LOTNT-DIV-MOD-REM [<file> or <directory>]
   

   See item 237 in the HISTORY.txt file.


9. The deprecated syntax "?" for passing actual "in out" parameters is no longer accepted: one must use the "!?" syntax instead. See items 238 and 201 in the HISTORY.txt file.

Code-Generation Changes

1. The constants ADT_SFALSE and ADT_STRUE have been replaced with ADT_FALSE() and ADT_TRUE(), respectively, in the predefined library and the C code generated by TRAIAN. See item 214 in the HISTORY.txt file.


2. The C code generated by TRAIAN was made more readable by adding missing spaces and line breaks, removing useless extra spaces and line breaks, fixing typos in comments, and removing superfluous parentheses. Also, a local variable improperly named HASH_VALUE was renamed to TRAIAN_HASH_VALUE. See item 215 in the HISTORY.txt file.


3. TRAIAN no longer generates C expressions of the form "((x == y))", which caused warnings from the Clang compiler. See item 220 in the HISTORY.txt file.


4. Useless code fragments related to exception handling have been removed. See item 221 in the HISTORY.txt file.


5. The order in which certain types, macros, and functions are defined in the generated C code now reproduces the order in which they appear in the source LOTOS NT file. See item 222 in the HISTORY.txt file.


6. The C code generated by TRAIAN was further simplified by removing useless braces in function definitions and simplifying some "#define" directives. See item 224 in the HISTORY.txt file.


7. The C code generated for negative numbers was simplified, e.g., "-13" or "-27.2" instead of "ADT_UMINUS_INT (13)" or "ADT_UMINUS_REAL (27.2)". See item 226 in the HISTORY.txt file.


8. Useless "else { /* empty */ }" clauses have been removed from the generated C code. See item 231 in the HISTORY.txt file.


9. The "break" instructions of LOTOS NT are no longer implemented as exception raises using "longjmp()" calls, but as mere "goto" statements. On various examples, the generated C code is smaller by 11.5% and faster by 10%. See item 235 in the HISTORY.txt file.


10. Compound statements of the form "if (...) {...} else if (...) {...} else if (...) {...} else {...}" have been replaced by successive "if (...) {...}" statements, each terminated by a "return" or a "goto" statement. See item 240 in the HISTORY.txt file.


11. Boolean conditions have been simplified, e.g., by replacing "ADT_TRUE() == xxxxxx" with "xxxxxx", and "/* CONSTANTCONDITION */ 1 == 1" with "ADT_TRUE ()". See item 241 in the HISTORY.txt file.


12. The C code generated for "case" instructions in which a free variable declared in some pattern is only used in a "where" guard was modified to avoid "variable ... set but not used" warnings from the C compiler. See item 242 in the HISTORY.txt file.

Miscellaneous Changes

1. An error message of TRAIAN for function calls in the positional style has been enhanced. See item 219 in the HISTORY.txt file.


2. The "mac86" executables have been removed from the TRAIAN distribution, since recent versions of of macOS (starting from macOS 10.15 "Catalina" and upwards) no longer support 32-bit binaries. See item 225 in the HISTORY.txt file.


3. A better algorithm for checking the completeness of "case" instructions has been implemented, which displays more explanative error messages for potentially incomplete "case" instructions dealing with numerical values. See item 229 in the HISTORY.txt file.

Bug Fixes

1. In some cases, the translation of the "where" conditions of patterns could generate an extra occurrence of the "&&" operator. See item 211 in the HISTORY.txt file.


2. The C code generated for exceptions contained "..., "file", 1, 1)" instead of "..., __FILE__, __LINE__, 0)". See item 216 in the HISTORY.txt file.


3. In the generated code, all loops had the same number. From now on, each loop has a unique number. See item 218 in the HISTORY.txt file.


4. The functions to access fields of singleton type could return incorrect values (most of the time ignored by the functions operating on singleton types). See item 223 in the HISTORY.txt file.


5. The previous versions of TRAIAN did not check whether "case" instructions dealing with strings were complete (i.e., did contain an "any" clause). See item 230 in the HISTORY.txt file.


6. The code generated for loops containing "return" instructions could trigger "statement not reached" warnings from some C compilers. See item 232 in the HISTORY.txt file.


7. Enumerated types with more than 65,536 elements were not properly implemented. See item 233 in the HISTORY.txt file.


8. Irrelevant "forward" declarations were generated for the PRED and SUCC functions of enumerated types. See item 234 in the HISTORY.txt file.


9. "Forward" declarations were not generated for the ORD and HASH functions of tuple types. See item 239 in the HISTORY.txt file.

Future Work

Download

TRAIAN 3.2 can be freely downloaded from the TRAIAN Web Page located at: