TRAIAN 3.6 released on February 28, 2022

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

Release Notes

TRAIAN 3.6 has been prepared by Hubert Garavel, Frederic Lang, and Wendelin Serwe. It was released four months after version 3.5 of TRAIAN.

TRAIAN 3.6 brings twenty-four language changes, twelve library and code-generation changes, and five bug fixes (see below their description).

Language Changes

TRAIAN 3.6 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 demo examples have been updated to reflect these changes.

The syntax of LOTOS NT type definitions was extended by adding the following syntactic constructs:
```
   array [m .. n] of T
   range m .. n of T
   set of T
   sorted list of T
   sorted set of T
   X:T where V (i.e., predicate types)
```
Code generation for such type definitions is not yet implemented; TRAIAN 3.6 displays an error message when they are used. See item 327 in the HISTORY.txt file.

The syntax of LOTOS NT was extended by allowing several process definitions rather than a single MAIN process. For the moment, multiple processes are not yet handled by C code generation. See item 330 in the HISTORY.txt file.

TRAIAN 3.6 performs binding checks for events, functions, types, and variables present in LOTOS NT process definitions. See item 331 in the HISTORY.txt file.

The syntax of LOTOS NT patterns was extended to accept "any T", in addition to "any" and "any of T", which were already accepted. LOTOS NT thus becomes a superset of LNT, which only accepts restricted uses of "any". See item 332 in the HISTORY.txt file.

The code generation part of TRAIAN 3.6 explicitly rejects LOTOS NT processes having value parameters. Previously, such parameters were simply ignored at code generation. See item 333 in the HISTORY.txt file.

TRAIAN 3.6 performs type checking in LOTOS NT process definitions. See item 334 in the HISTORY.txt file.

TRAIAN 3.6 performs the expansion of ellipses "..." in the LOTOS NT behaviours. See item 335 in the HISTORY.txt file.

The grammar of LOTOS NT was modified, so that pragma names occurring after "!" (e.g., "implementedby", "external", etc.) are no longer reserved keywords. Consequently, certain LOTOS NT specifications that were previously rejected are now accepted, e.g.,
```
   type implementedby is A, B, C end type
```
Conversely, it is now forbidden to insert spaces between "!" and pragma names. See item 336 in the HISTORY.txt file.

The syntax of LOTOS NT was extended to accept the same module pragmas as those of LNT, namely:

   !int_bits
   !int_check
   !int_inf
   !int_sup
   !nat_bits
   !nat_check
   !nat_inf
   !nat_sup
   !num_bits
   !num_card
   !string_card

See item 337 in the HISTORY.txt file.

The syntax of LOTOS NT was extended by adding three type pragmas:
```
   !bits n
   !card n
   !list
```
The latter pragma is automatically set for the LOTOS NT types defined as "list", "sorted list", "set", and "sorted set". See item 339 in the HISTORY.txt file.

The former pragma "!enumeratedby S" was replaced by a new pragma "!iteratedby S1, S2". The "lotosnt_predefined" library has been updated accordingly. Users should upgrade their source LOTOS NT files by running the following command:
```
   traian_upc 2021-LOTNT-ENUMERATEDBY [<file> or <directory>]
```
See item 340 in the HISTORY.txt file.

The editor style files contained in the "ext" directory have been updated
- to take into account the new reserved keyword "range", the new pragmas ("bits", "card", etc.), and the operators "|", "||", and "[]";
- to remove the deprecated operator "%";
- and to replace the former "enumeratedby" pragma by the new "iteratedby" pragma.
See item 341 in the HISTORY.txt file.

The syntax of LOTOS NT real numbers was extended: from now on, the exponents of real numbers may start with a zero and contain underscore characters. See item 343 in the HISTORY.txt file.

From now on, the syntax of LOTOS NT integer and real numbers may not contain consecutive underscore characters, nor end with an underscore character. See item 344 in the HISTORY.txt file.

The syntax of octal constants in LOTOS NT was modified: these constants are no longer written "0nnn" but "0onnn", e.g. "0o123" instead of "0123". Users should upgrade their source LOTOS NT files by running the following command:
```
   traian_upc 2022-LOTNT-OCT [<file> or <directory>]
```
Also, octal constants may now contain underscore characters, provided that they are neither initial, consecutive, nor terminal. See item 345 in the HISTORY.txt file.

The syntax of LOTOS NT hexadecimal constants was modified. From now on, these constants must start with "Ox" (lower case), as the prefix "0X" (upper case) is no longer accepted, e.g., "0X001F" must be written "0x001F". Users should upgrade their source LOTOS NT files by running the following command:
```
   traian_upc 2022-LOTNT-HEX [<file> or <directory>]
```
Also, hexadecimal constants may now contain underscore characters, provided that they are neither initial, consecutive, nor terminal. See item 346 in the HISTORY.txt file.

The syntax of LOTOS NT was extended with binary constants, which are prefixed with "0b" and may contain underscore characters, e.g., 0b1011 or 0b0101_1011. The code generation part of TRAIAN 3.6 was enhanced to handle such constants. See item 347 in the HISTORY.txt file.

The syntax of LOTOS NT identifiers was made more stringent. From now on, identifiers cannot contain consecutive underscore characters, nor end with an underscore character. Users should upgrade their source LOTOS NT files by running the following command:
```
   traian_upc 2022-LOTNT-UNDERSCORES [<file> or <directory>]
```
See item 348 in the HISTORY.txt file.

The syntax of LOTOS NT real numbers was made more stringent:
- Real numbers starting with a dot are no longer allowed (e.g., ".45" should be written "0.45").
- Real numbers ending with a dot are no longer allowed (e.g., "4." should be written "4.0" and "3.e+2" should be written "3e+2" or "3.0e+2").
Users should upgrade their source LOTOS NT files by invoking the following command:
```
   traian_upc 2022-LOTNT-REALS [<file> or <directory>]
```
See item 349 in the HISTORY.txt file.

TRAIAN 3.6 now generates C code for the functions defined using LOTOS NT code in the "lotosnt_predefined" library. See item 351 in the HISTORY.txt file.

The syntax of LOTOS NT expressions and patterns was slightly modified: from now on, any nullary function or constructor whose name is a special identifier (i.e., built using the characters % & * + - / > = < @ \ ^ ~) must be followed by parentheses "()" when it is invoked. For instance, given the following type definition:
```
   type OP is
      *, +
   end type
```
the following function:
```
  function F (X: OP): bool is
      case X in
	 * -> return true
      |  + -> return false
      end case
   end function
```
must be rewritten as follows:
```
   function F (X: OP): bool is
      case X in
	 *() -> return true
      |  +() -> return false
      end case
   end function
```
See item 359 in the HISTORY.txt file.

The syntax of LOTOS NT patterns and expressions was relaxed: any unary function or constructor whose name is a special identifier no longer requires parentheses around its argument. For instance, one may write "return -X" rather than "return -(X)". See item 360 in the HISTORY.txt file.

The auxiliary files that provide C code to implement the functions (respectively, types) declared as external in LOTOS NT specifications now have the ".fnt" (respectively, ".tnt") suffix. The former suffixes ".f" and ".t" are still accepted but trigger warnings. Invoking the following command:
```
   traian_upc 2022-LOTNT-FNT-TNT [<file> or <directory>]
```
will rename these files automatically. See item 364 in the HISTORY.txt file.

TRAIAN 3.6 emits warnings if a LOTOS NT specification defines external functions (respectively, types) but no corresponding ".fnt" (respectively, ".tnt") file is present in the current directory to implement these types and functions. See item 365 in the HISTORY.txt file.

Library and Code-Generation Changes

The implementation in "lotosnt_predefined.h" of the five string-comparison functions ADT_GE_STRING(), ADT_GT_STRING(), ADT_LE_STRING(), ADT_LT_STRING(), and ADT_NE_STRING() was made more efficient. See item 325 in the HISTORY.txt file.

The "lotosnt_exceptions" library was enhanced with a global variable TRAIAN_LIB_ERROR_MESSAGE that enables one to display, when an error occurs, a specific message. See item 326 in the HISTORY.txt file.

The "lotosnt_predefined" library was extended by adding several function definitions, which duplicate LOTOS NT functions that already exist with the same profile but with an additional event parameter. These new functions raise the UNEXPECTED event if an error occurs:

   function - (X1: NAT, X2: NAT): NAT 
   function mod (X1: NAT, X2: NAT): NAT 
   function div (X1: NAT, X2: NAT): NAT 
   function INT (X: NAT): INT
   function CHAR (X: NAT): CHAR
   function REAL (X: NAT): REAL

   function div (X1: INT, X2: INT): INT
   function mod (X1: INT, X2: INT): INT
   function rem (X1: INT, X2: INT): INT
   function NAT (X: INT): NAT
   function CHAR (X: INT): CHAR
   function REAL (X: INT): REAL

   function / (X1: REAL, X2: REAL): REAL
   function INT (X: REAL): INT
   function NAT (X: STRING): NAT
   function INT (X: STRING): INT
   function REAL (X: STRING): REAL

See item 342 in the HISTORY.txt file.

The C code generation of TRAIAN was simplified by renaming the macro TRAIAN_GET_1_ADT_SUCC() to TRAIAN_GET_ADT_NAT_SUCC_X(), which suppressed a particular case that existed for the SUCC: NAT -> NAT function only. See item 352 in the HISTORY.txt file.

Various C identifiers defined or used in "lotosnt_hash.h" and "lotosnt_predefined.h" have been simplified:

The deprecated macros ADT_SFALSE and ADT_STRUE have been removed.
The macro TRAIAN_ADT_GC was renamed to TRAIAN_LIB_GARBAGE_COLLECTION.
The macro TRAIAN_ADT_INTERFACE_ONLY was renamed to TRAIAN_LIB_HEADERS_ONLY.

Many identifiers in the C code generated by TRAIAN have also been shortened by removing the module name, which was useless because type and function names are globally unique:

   TRAIAN_EQ_module_type -> TRAIAN_EQ_type
   TRAIAN_GE_module_type -> TRAIAN_GE_type
   TRAIAN_GT_module_type -> TRAIAN_GT_type
   TRAIAN_LE_module_type -> TRAIAN_LE_type
   TRAIAN_LT_module_type -> TRAIAN_LT_type
   TRAIAN_NE_module_type -> TRAIAN_NE_type
   TRAIAN_FUNCTION_module_function -> TRAIAN_FUNCTION_function
   TRAIAN_ITERATE_FIRST_module_type -> TRAIAN_ITERATE_FIRST_type
   TRAIAN_ITERATE_NEXT_module_type -> TRAIAN_ITERATE_NEXT_type
   TRAIAN_PRINT_module_type -> TRAIAN_PRINT_type
   TRAIAN_STRINGIFY_module_type -> TRAIAN_STRING_type
   TRAIAN_TYPE_module_type -> TRAIAN_TYPE_type

Users should upgrade their handwritten C files by running the following command:

   traian_upc 2022-LOTNT-C-NAMES-1 [<file> or <directory>]

See item 353 in the HISTORY.txt file.

In the C code generated by TRAIAN for memory allocation, the character strings passed as 4th parameters in the calls to TRAIAN_ALLOC() have been made more informative: instead of the name of a generated C function, they contain the name of a source LOTOS NT function, as well as the file and line number where this function is defined. See item 355 in the HISTORY.txt file.

The "_t.h" and "_f.h" files generated by TRAIAN were enhanced in various ways:
- The preamble of the "_t.h" files was simplified by removing redundant #include directives, moving five macro definitions to the "lotosnt_predefined.h" file, and removing /* LINTLIBRARY */ comments.
- The various error messages for memory shortage have been greatly simplified.
See item 356 in the HISTORY.txt file.

The "_t.h" and "_f.h" files generated by TRAIAN were further enhanced:
- Spaces, line breaks, and dash lines have been deleted or inserted where appropriate.
- All comments about external types, previously scattered at many places in the "_t.h" file, have been gathered at one single place, just after the #include directive.
- These comments have been enhanced by adding the file and line numbers where external LOTOS NT types are declared.
See item 357 in the HISTORY.txt file.

The "_f.h" files generated by TRAIAN have been enhanced with informative comments that list all C functions that need to be provided by the user for implementing the LOTOS NT functions declared as external. See item 358 in the HISTORY.txt file.

The "lotosnt_exceptions" library and the C code generated by TRAIAN were simplified as follows:
- The former function TRAIAN_ADTI_enter_function() was replaced by two specialized functions: TRAIAN_LIB_ROUTINE_ENTRY() and TRAIAN_LIB_TRAP_ENTRY().
- The former function TRAIAN_ADTI_leave_function() was replaced by two specialized functions: TRAIAN_LIB_ROUTINE_LEAVE() and TRAIAN_LIB_TRAP_LEAVE().
- The global variable TRAIAN_ADTx_ENTERTRAP and the two macros TRAIAN_ADTx_LEAVEFUNCTION and TRAIAN_ADTx_LEAVETRAP have been removed.
See item 361 in the HISTORY.txt file.

The C code generated by TRAIAN was modified to pass an empty string to TRAIAN_LIB_ROUTINE_ENTRY() unless the C code is compiled with the DEBUG macro defined (i.e., "cc -DDEBUG ..."). This reduces the size of the binary executables generated from LOTOS NT specifications. See item 362 in the HISTORY.txt file.

The C code generated by TRAIAN and the "lotosnt_exceptions" library were modified to display, when an exception event occurs and is not trapped, the call stack of the LOTOS NT program. Such display will only occur if the C code generated by TRAIAN is compiled with the DEBUG macro defined. See item 363 in the HISTORY.txt file.

Bug Fixes

The LOTOS NT reference manual was extended to document the syntax of behaviours and the "case" instruction with multiple choices. See item 328 in the HISTORY.txt file.

The static analysis of TRAIAN 3.5 did not detect the unused variables declared in the "var" clause of a "case". From now on, TRAIAN 3.6 warns about these variables. See item 329 in the HISTORY.txt file.

TRAIAN 3.6 fixes a bug in the C code generated for "case" instructions in which a variable used as the "case" condition is also present in a "case" pattern (and thus, assigned if the corresponding branch is selected). This bug could cause incorrect execution, possibly with segmentation faults. See item 338 in the HISTORY.txt file.

The code generation of TRAIAN 3.6 no longer prints in the generated C code the underscore characters present in LOTOS NT numeric constants. See item 350 in the HISTORY.txt file.

Two issues were fixed in the lexer of TRAIAN:
- Block comments of the form "(* ... *)" were not properly handled if the opening symbol was immediately followed by an exclamation mark, i.e., "(*! ... *)".
- TRAIAN 3.5 rejected offers of the form "!identifier" if identifier was a prefix of some pragma name. For instance, "G (!b)" and "G (!im)" were rejected because "b" is a prefix of "bits" and "im" a prefix of "implementedby".
See item 354 in the HISTORY.txt file.

Future Work

TRAIAN 3.6 will continue to evolve, our goal being to merge LOTOS NT and LNT in one single language.

Download

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

http://vasy.inria.fr/traian