TRAIAN 3.11 released on September 29, 2023

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

Release Notes

TRAIAN 3.11 has been prepared by Hubert Garavel, Frederic Lang, and Wendelin Serwe. It was released three months after version 3.10 of TRAIAN.

With TRAIAN 3.11, the convergence between LOTOS NT and LNT is complete. Measured on a test suite of 13,600+ correct LNT programs totalling more than 9 million non-blank lines of LNT code, TRAIAN 3.11 syntactically accepts 100% of these programs and semantically accepts 100% of them (whereas TRAIAN 3.10 accepted 93.5% of them).

TRAIAN 3.11 brings three language changes, three compiler changes, three code-generation changes, fourteen library changes, one release change, and seven bug fixes (see below their description).

Language Changes

To further align TRAIAN with the LNT language supported by LNT2LOTOS, the semantics of the "of" notation was extended as follows:
- Formerly, the expression "E of T" had the sole purpose of indicating to the type checker that expression E has type T, which can be helpful in resolving function overloading.
- From now on, "E of T" has an additional meaning when E is not of type T. In the particular case where type T is defined either as:
```
     type T is range ... of T' end type
```
  or
```
     type T is X:T' where ... end type
```
  and E is of type T', then "E of T" means "T (E)", i.e., the conversion of expression E from type T' to type T.
- Notice that "of" can be used to denote conversion from T' to T, but not in the other direction; for such purpose, the notation "T' (E')" should be used, as "E' of T'" will be rejected by TRAIAN.
- Such extended "of" notation is particularly useful for numeric constants. For instance, given the following type definitions:
```
     type T1 is range 0..255 of nat end type
     type T2 is X:T1 where X * X < 100 end type
```
  one can write "0 of T1", "1 of T2", etc., or equivalently "T1 (0)", "T2 (T1 (1))", etc.
The same conversion rules also apply to patterns "P of T".
Consequently, many LOTOS NT or LNT programs formerly rejected by TRAIAN are now accepted. See item 541 in the HISTORY.txt file.

To further align TRAIAN with the LNT language supported by LNT2LOTOS, the semantics of {...}-expressions was modified as follows:
- Previously, {...}-expressions were expanded using NIL and CONS functions. This was correct for "list" types, but not for "set" nor "sorted list" types: in the two latter cases, lists need to be sorted, which is not done by the CONS function.
- From now on, TRAIAN expands {...}-expressions using NIL and INSERT functions, assuming that the INSERT function is identical to CONS for "list" types, and does sort insertion for "set" and "sorted list" types.
- However, for those LOTOS NT types explicitly defined using NIL and CONS constructors (rather than using the "list", "set", or "sorted list" declarations), {...}-expressions will be expanded using NIL and CONS, unless an INSERT function exists; in such case, it will be used in place of CONS.
Notice that the semantics of {...}-patterns has been kept unchanged: contrary to {...}-expressions, {...}-patterns are always expanded using NIL and CONS constructors only.
See item 542 in the HISTORY.txt file.

To further align TRAIAN with the LNT language supported by LPP and LNT2LOTOS, the lexical analyzer of TRAIAN was modified to forbid certain hexadecimal and octal character notations that are not accepted by LPP. From now on:
- Hexadecimal characters must have exactly two digits. For instance, hexadecimal notations with a single digit (e.g., '\xA' or "--\x1--") are no longer accepted.
- Octal characters must either be '\0' or have exactly three digits. For instance, octal notations with one or two digits (e.g., '\12' or "--\7--") are no longer accepted.
See item 546 in the HISTORY.txt file.

Compiler Changes

The use of scheme files for "set" and "sorted list" types was enabled. From now on, TRAIAN no longer emits an error message:
```
   limitation: types not yet fully implemented
```
when an input LOTOS NT program contains sets or sorted lists, and generates C code for the functions defined in the scheme files of these types. See item 522 in the HISTORY.txt file.

A limitation that existed in former versions of TRAIAN was removed: when named offers (possibly including the ellipsis symbol "...") are present in a communication, TRAIAN no longer emits a "limitation" error message during semantic analysis. See item 544 in the HISTORY.txt file.

Another limitation of TRAIAN concerning types defined as "range ... of char" was lifted. From those types, TRAIAN no longer issues the error message:
```
   limitation: types not yet fully implemented
```
See item 547 in the HISTORY.txt file.

Code-Generation Changes

The C code generated by TRAIAN was modified to replace by new-style prototypes some old-style prototypes that remained (especially, for tuple and ordinary types). Also, many C function declarations of the form "F ()" have been replaced with "F (void)". The TRAIAN demos 01, 02, and 04 have been updated to use new-style prototypes only. See item 519 in the HISTORY.txt file.

The number of lines in the C code generated by TRAIAN was reduced by 17.4% on average. This was done by taking into account the presence or absence of "!bits" and "!card" pragmas to remove many C code fragments enclosed between #if or #ifdef conditionals. See item 538 in the HISTORY.txt file.

In the C code generated for tuple and ordinary types, the functions named TRAIAN_INSERT_<type> have been renamed by TRAIAN_STORE_<type>. Indeed, the former name conflicted with the C code generated for the INSERT functions of "list", "set", and "sorted list" types. See item 540 in the HISTORY.txt file.

Library Changes

The scheme files for "list", "set", and "sorted list" types have been enhanced:
- The "<", "<=" ">", and ">=" functions defining lexicographic order on such types have been added.
- The EMPTY and MEMBER functions on such types have been added.
- The PRED and SUCC functions for such types have been removed, as they are not used in practice.
- The LENGTH functions on "list" and "sorted list" types have been added.
- New functions have been introduced:
```
     function HEAD [EMPTY : NONE] (X : LNT_T1) : LNT_T2 
     function TAIL [EMPTY : NONE] (X : LNT_T1) : LNT_T1
```
  in addition to the already existing ones:
```
     function HEAD (X : LNT_T1) : LNT_T2 
     function TAIL (X : LNT_T1) : LNT_T1
```
  Consequently, the expansion phase of TRAIAN has been modified to handle the case where a scheme file contains overloaded functions, such as HEAD and TAIL, which exist under the same name, with and without event parameter.
See item 523 in the HISTORY.txt file.

The CARD functions defined in all scheme files have been removed, as these functions were not really useful and their name was potentially misleading.
The existing LOTOS NT programs that invoke CARD functions defined in "with" clauses should be updated to define such functions explicitly. See item 524 in the HISTORY.txt file.

To further align TRAIAN with the LNT language supported by LNT2LOTOS, the scheme file of "set" types to rename the LENGTH function (which returns the number of elements in a set) to CARD (which is the usual name).
The existing LOTOS NT programs that invoke the LENGTH function on sets should be updated accordingly, so as not to be rejected by TRAIAN with the following message:
```
  error: unknown function length in "with" clause of type SET
```
See item 525 in the HISTORY.txt file.

Two string-manipulation functions of TRAIAN's predefined library:
```
   function ISEMPTY (X : STRING) : BOOL
   function NTH (X : STRING, N : NAT) : CHAR
```
have been renamed into, respectively:
```
   function EMPTY (X : STRING) : BOOL
   function ELEMENT (X1 : STRING, X2: NAT) : CHAR
```
by analogy with the EMPTY and ELEMENT functions defined on "list", "set", and "sorted list" types.
Users are advised to upgrade their LOTOS NT programs by running the following command:
```
   traian_upc 2023-LOTNT-PREDEFINED [<file> or <directory>]
```
which will rename functions where appropriate. See item 527 in the HISTORY.txt file.

To further align TRAIAN with the LNT language supported by LNT2LOTOS, the predefined library of TRAIAN was modified to define the constructors NEG and POS for the INT type. These constructors are inspired by the following paper: Hubert Garavel, "On the Most Suitable Axiomatization of Signed Integers", December 2017. See item 530 in the HISTORY.txt file.

The C function implementing the SUCC constructor of the NAT type was renamed. This function, formerly named ADT_SUCC_NAT(), is now named ADT_CSUCC_NAT(). This change, which was unavoidable for technical reasons, should be invisible to most users. See item 531 in the HISTORY.txt file.

The predefined library of TRAIAN was extended by adding eight new functions:
```
   function PRED [RANGE_ERROR: NONE] (X : BOOL) : BOOL
   function PRED [RANGE_ERROR: NONE] (X : NAT) : NAT
   function PRED [RANGE_ERROR: NONE] (X : INT) : INT
   function PRED [RANGE_ERROR: NONE] (X : CHAR) : CHAR
   function SUCC [RANGE_ERROR: NONE] (X : BOOL) : BOOL
   function SUCC [RANGE_ERROR: NONE] (X : NAT) : NAT
   function SUCC [RANGE_ERROR: NONE] (X : INT) : INT
   function SUCC [RANGE_ERROR: NONE] (X : CHAR) : CHAR
```
Moreover, the semantics of the PRED and SUCC functions (with or witout a RANGE_ERROR event parameter) has been modified as follows. Formerly, when invoked on the smallest (resp. largest) value of the BOOL, NAT, INT, or CHAR type, the PRED (resp. SUCC) function returned this value. From now on, they raise an exception, which is either the actual event passed to the RANGE_ERROR parameter, or UNEXPECTED if the RANGE_ERROR parameter is absent. See item 532 in the HISTORY.txt file.

To further align TRAIAN with the LNT language supported by LNT2LOTOS, eight functions have been removed from the predefined library of TRAIAN:
```
   function CARD (X : BOOL) : NAT
   function CARD (X : NAT) : NAT
   function CARD (X : INT) : NAT
   function CARD (X : CHAR) : NAT
   function ORD (X : BOOL) : NAT
   function ORD (X : NAT) : NAT
   function ORD (X : INT) : NAT
   function ORD (X : CHAR) : NAT
```
as well as the eight C functions implementing them, namely: ADT_CARD_BOOL(), ADT_CARD_NAT(), ADT_CARD_INT(), ADT_CARD_CHAR(), ADT_ORD_BOOL(), ADT_ORD_NAT(), ADT_ORD_INT(), and ADT_ORD_CHAR(). See item 533 in the HISTORY.txt file.

To further align TRAIAN with the LNT language supported by LNT2LOTOS, the two following functions:
```
   function CHAR [RANGE_ERROR : NONE] (X : INT) : CHAR
   function CHAR (X : INT) : CHAR
```
have been removed from the predefined library of TRAIAN, together with the two C functions ADT_TO_CHAR_INT() and TRAIAN_LIB_TO_CHAR_INT() implementing them. Indeed, these functions were useless, since there already exist two similar functions:
```
   function CHAR [RANGE_ERROR : NONE] (X : NAT) : CHAR
   function CHAR (X : NAT) : CHAR
```
and one does not want to introduce in LOTOS NT the fruitless notion of signed characters. See item 534 in the HISTORY.txt file.

The PRED and SUCC functions defined for tuple and ordinary types have been removed. Former versions of TRAIAN allowed such functions, but generated only "fake" C code ("/* NOT YET IMPLEMENTED */") for them. See item 535 in the HISTORY.txt file.

The ELEMENT functions have been added in the schemes for "list", "set", and "sorted list" types. See item 536 in the HISTORY.txt file.

The scheme files of "list", "set", and "sorted list" types have been extended by introducing new functions:
- three auxiliary LNT_REVAPPEND functions, the definition of which is generated directly by TRAIAN as native C code;
- one APPEND function for "list" types;
- two INSERT functions for "set" and "sorted list" types.
From now on, whenever a "set of T" or "sorted list of T" type is defined, the two functions
== : T, T → bool and < : T, T → bool must be defined for type T.
This change, combined with item 542 above, fixes an issue that existed in former versions of TRAIAN. From now, both expressions {1, 2} and {2, 1} are equal for "set" and "sorted list" types, whereas they were formerly different. See item 543 in the HISTORY.txt file.

Three new functions have been added to the predefined library of TRAIAN:
```
   function CHAR [RANGE_ERROR : NONE] (X : STRING) : CHAR
   function CHAR (X : STRING) : CHAR
   function STRING (X : STRING) : STRING
```
the latter being an identity function. See item 545 in the HISTORY.txt file.

The schemes of "array" and "where" types have been simplified by removing:
- the PRED and SUCC functions on "array" types,
- the FIRST and LAST functions on "where" types,
- the PRED and SUCC functions on "where" types,
- the VAL function on "where" types.
See item 548 in the HISTORY.txt file.

Release Changes

The file doc/manual.ps.Z (compressed using compress) was replaced by file doc/manual.ps.gz (compressed using gzip). Similarly, file traian.tar.Z was replaced by traian.tar.gz. The documentation and web site of TRAIAN have been updated. See item 518 in the HISTORY.txt file.

Bug Fixes

A bug that had been present in TRAIAN for long (since at least versions 2.*) was fixed. For certain classes of LOTOS NT types that can be implemented using natural numbers, TRAIAN could generate incorrect C code, containing "switch" statements with identical "case" branches (e.g., "case 1" and "case 1"); such generated code was later rejected by the C compiler, e.g.:
```
   "test.c", line 207: duplicate case in switch: 1
```
See item 520 in the HISTORY.txt file.

Another bug was fixed, which had been present in TRAIAN for long (since at least versions 2.*) but appeared recently when switching to new-style function prototypes. From now on, the C code generated by TRAIAN no longer contains TRAIAN_CLOBBERED attributes (i.e., "volatile") in the declaration of function parameters. The presence of such attributes caused conflicts with "forward" declarations of functions, the prototypes of which did not contain any TRAIAN_CLOBBERED attribute. See item 521 in the HISTORY.txt file.

An issue was fixed in the former versions of TRAIAN, which failed to reject LOTOS NT programs defining several functions having the same profile (i.e., same function name, same parameter types, and same result type) if a "var" keyword was used. For instance, the following definitions were accepted:
```
   function F (X : nat) : bool is ...
   function F (in var X : nat) : bool is ...
```
as well as the following ones:
```
   function G (out X : nat) is ...
   function G (out var X : nat) is ...
```
However, if functions F or G were invoked, TRAIAN emitted an error message: "ambiguous call to overloaded function". Thus, the issue only occurred with functions never called.
From now on, TRAIAN considers that "in var" and "out var" are identical to "in" and "out", respectively, and rejects the two above definitions, with error messages such as:
```
  function F is already defined with the same profile at ...
  function G is already defined with the same profile at ...
```
See item 526 in the HISTORY.txt file.

An issue was fixed in the generation of the C code for certain functions (e.g., HASH and ORD) defined in scheme files for general types (such as tuple and ordinary types), TRAIAN did not generate the "forward" declarations needed for these functions. See item 528 in the HISTORY.txt file.

An issue was fixed in the handling of scheme files: the loop identifiers present in such files were not properly bound, leading to memory faults for those scheme functions containing named loops (i.e., "loop L in ..."). See item 529 in the HISTORY.txt file.

The following bug was fixed: from now on, when a function defined in a scheme file has "require" or "ensure" clauses, TRAIAN no longer issues spurious warnings such as:
```
   scheme_list.lnt:170: error: variable N may be uninitialized
```
See item 537 in the HISTORY.txt file.

A bug that caused, which caused core dumps when an "!implementedby" pragma was attached to the NIL or CONS functions of "set" and "sorted list" types. See item 539 in the HISTORY.txt file.

Future Work

For many years, TRAIAN has been used to develop compilers, including those of the CADP toolbox.

At present, TRAIAN is also increasingly used to check LNT specifications of concurrent systems, allowing to catch mistakes not detected by the "lightweight" approach of the LNT2LOTOS translator. Given that LOTOS NT and LNT have been merged in one single language, we plan to integrate soon TRAIAN in the CADP toolbox, where it will provide a full-fledged compiler front-end for the LNT language.

Download

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

http://vasy.inria.fr/traian