TRAIAN 3.1 released on June 29, 2020

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

Release Notes

TRAIAN 3.1 has been prepared by Hubert Garavel, Frederic Lang, and Wendelin Serwe. It was released four months after version 3.0 of TRAIAN, which was a complete rewrite of the compiler.

On the one hand, TRAIAN 3.1 is a consolidation release, which brings five general enhancements and eight bug fixes (see below their description).

On the other hand, TRAIAN 3.1 is also a transition release, which introduces various changes to the LOTOS NT language, in order to progressively align it with the LNT language supported by the CADP toolbox. Indeed, the syntax of LOTOS NT is non-intuitive, and even confusing, at various places. For instance, there are much too many brackets in the syntax of LOTOS NT, with different meanings (Boolean guards, sets of values, lists of values, lists of gates, and lists of exceptions). This defect inherited from LOTOS is properly solved in LNT, where brackets are exclusively used to denote event lists.

To do so, seventeen language changes have been introduced with TRAIAN 3.0 (see below their description). All but one of these changes are backward compatible. Only the 10th change listed below is not. Thus, all existing LOTOS NT programs that compiled using TRAIAN 3.0 and do not use the list notation "[x, y, z]", will still compile using TRAIAN 3.1.

However, end-users are advised to upgrade all their source LOTOS NT programs in order to only use the new notations introduced by TRAIAN 3.1. Even if the old notations are still supported by TRAIAN 3.1, they are deprecated, meaning that they will be removed from future versions of TRAIAN, most likely as soon as TRAIAN 3.2.

To ease the upgrade of LOTOS NT source code, a conversion tool named "traian_upc" has been developed and is provided with TRAIAN 3.1. Using this tool, the CONVECS team was able to swiftly upgrade seven compilers written using LOTOS NT (namely, EXP2C, FSP2LOTOS, GRL2LNT, MCL_EXPAND, PIC2LNT, SVL, and TRAIAN itself) totalling 168,000 lines of LOTOS NT code, as well as the LOTOS NT test suites totalling 1,940,000 lines of code.

General Changes

The C code generated by TRAIAN to implement LOTOS NT exceptions was enhanced.

A new shell script traian_upc (where "upc" stands for "User Program Conversion") was added. This script serves to automatically (or quasi-automatically, but to a large extent) upgrade LOTOS NT programs, following certain language changes described in the next section.

The file "incl/lotosnt_predefined.h" was modified to declare each predefined function with its prototype.

The definition of ADT_PRINT_BOOL() in file "incl/lotosnt_predefined.h" was modified to avoid a "-Wformat-security" warning of the Clang compiler.

The LOTOS NT Reference Manual was updated at many places to reflect some changes introduced in TRAIAN 3.0 and TRAIAN 3.1 (see items 177 and 204 in the HISTORY.txt file for details).

Language Changes

TRAIAN 3.1 no longer rejects those LOTOS NT programs containing a "return" instruction inside a loop; such programs are now supported.

TRAIAN 3.1 now emits a new warning:
```
   superfluous "..." after all parameters have been listed
```
if the ellipsis notation "..." is used (in a function call, a constructor call, or a field update) where there is no missing element in the parameter list.

TRAIAN 3.1 now emits a warning
```
   empty field update
```
when an expression of the form "V.{}" or "V.{...}" is used.

TRAIAN 3.1 now rejects nested loops that have the same name, since this is error-prone, as in the following code:

   loop L in
      ...
      loop L in -- this loop should have a different name
	 ...
	 break L -- risk of confusion between both loops
      end loop
   end loop

The behaviour of TRAIAN 3.1 for useless "raises [E]" clauses was modified. From now on, if a value projection or a value update that cannot raise an exception has an attached "raises [E]" clause, which is irrelevant, TRAIAN emits a fatal error message ("impossible exception"), while it previously emitted a warning only ("superfluous exception").
This decision was dictated by four reasons: (i) Useless "raises" clauses confuse those who read the LOTOS NT code; (ii) TRAIAN 3.0 already forbad invoking "F (...) raises [X]" if function F was not declared to raise an exception; (iii) TRAIAN 3.0 also forbad redundant "raises" clauses, as in "V raises [X1] raises [X2]"; and (iv) TRAIAN 3.1 now behaves like TRAIAN 2.x, which already emitted a fatal error for useless "raises" clauses.

The former LOTOS NT keyword "inout" was replaced by "in out", so as to align the syntax of LOTOS NT with that of LNT. TRAIAN 3.1 still accepts both syntaxes "inout" and "in out", but the former syntax is deprecated and might be removed from future versions of TRAIAN. End-users are advised to upgrade their source LOTOS NT files, using the command:
```
   traian_upc 2020-LOTNT-INOUT [<file> or <directory>]
```

The former LOTOS NT syntax "case ... is" was replaced by "case ... in", so as to align the syntax of LOTOS NT with that of LNT. TRAIAN 3.1 still accepts both syntaxes, but the former syntax is deprecated. End-users are advised to upgrade their LOTOS NT files:
```
   traian_upc 2020-LOTNT-CASE-IS [<file> or <directory>]
```

The former LOTOS NT syntax "for ... do ... end for" was replaced by "for ... loop ... end loop", so as to align the syntax of LOTOS NT with that of LNT. TRAIAN 3.1 still accepts both syntaxes, but the former syntax is deprecated. End-users are advised to upgrade their LOTOS NT files:
```
   traian_upc 2020-LOTNT-FOR-DO [<file> or <directory>]
```

The former LOTOS NT syntax "while ... do ... end while" was replaced by "while ... loop ... end loop", so as to align the syntax of LOTOS NT with that of LNT. TRAIAN 3.1 still accepts both syntaxes, but the former syntax is deprecated. End-users are advised to upgrade their LOTOS NT files:
```
   traian_upc 2020-LOTNT-WHILE-DO [<file> or <directory>]
```

The old syntax for LOTOS NT lists and sets in value expressions and value patterns, i.e., "[x, y, z]", was replaced by a new syntax "{x, y, z}" that is aligned on the syntax of LNT for lists and sets. For grammar parsing reasons, it was not possible to support both syntaxes "[x, y, z]" and "{x, y, z}" simultaneously. Using the old syntax will cause errors in TRAIAN 3.1. End-users are thus advised to upgrade their LOTOS NT files, which can be partly automated using:
```
   traian_upc 2020-LOTNT-VALUE-LIST [<file> or <directory>]
   traian_upc 2020-LOTNT-PATTERN-LIST [<file> or <directory>]
```
Beware that these commands may modify comments and character strings.

The old LOTOS NT syntax for declaring exceptions when defining a function was replaced by a new syntax aligned on that of LOTOS NT. Here are two examples with the old syntax

   function F (B: BOOL) : BOOL raises [E: none] is ... 
   function F (X, Y : NAT) : NAT raises [ZDIV, UFLOW : none] is ...

and with the new syntax:

   function F [E: none] (B: BOOL) : BOOL is ...
   function F [ZDIV, UFLOW : none] (X, Y : NAT) : NAT is ...

TRAIAN 3.1 still accepts both syntaxes, but the former syntax is deprecated. End-users are advised to upgrade their LOTOS NT files:

   traian_upc 2020-LOTNT-FUNCTION-RAISES [<file> or <directory>]

The old syntax for handling exceptions in field updates:
```
   (V0.{X => V}) raises [E] 
```
was replaced by a new, more readable syntax aligned on that of LNT:
```
   V0 .[E] {X => V}
```
TRAIAN 3.1 still accepts both syntaxes, but the former syntax is deprecated. End-users are advised to upgrade their LOTOS NT files:
```
   traian_upc 2020-LOTNT-UPDATE-RAISES [<file> or <directory>]
```

The old syntax for handling exceptions when calling a prefix function F (possibly with a missing or empty parameter list)
```
   F raises [E]
   F () raises [E]
   F (V1, ..., Vm) raises [E1, ..., En]
```
was replaced by a new, more concise syntax aligned on that of LNT:
```
   F [E]
   F [E] ()
   F [E1, ..., En] (V1, ..., Vm)
```
TRAIAN 3.1 still accepts both syntaxes, but the former syntax is deprecated. End-users are advised to upgrade their LOTOS NT files:
```
   traian_upc 2020-LOTNT-PREFIX-RAISES [<file> or <directory>]
```

The old syntax for handling exceptions when calling an infix function F in value expressions and patterns, e.g.,:
```
   (V1 F V2) raises [E1, ..., En]
   (V1 - V2) raises [E]
   (V1 / V2) raises [E]
```
was replaced by a new, more concise syntax aligned on that of LNT:
```
   V1 F[E1, ..., En] V2
   V1 -[E] V2
   V1 /[E] V2
```
This change also concerns field selection, whose old syntax:
```
   V.F raises [E]
```
becomes:
```
   V .[E] F
```
TRAIAN 3.1 still accepts both syntaxes, but the former syntax is deprecated. End-users are advised to upgrade their LOTOS NT files:
```
   traian_upc 2020-LOTNT-INFIX-RAISES [<file> or <directory>]
```
In some rare, complex cases, the elimination of "raises" is better done manually, especially in presence of expressions with "raises" nested at various levels.

The old LOTOS NT syntax for Boolean guards in "case":
```
   P1 | ... | Pn [V]
```
was confusing, as the Boolean guard V applies, not only to Pn, but also to P1, ..., P(n-1). TRAIAN 3.1 supports a new syntax inspired from that of LNT:
```
   P1 where V | ... | Pn where V
```
TRAIAN 3.1 still accepts both syntaxes, but the former syntax is deprecated. Mixing both syntaxes is possible, yet not commendable (see item 200 in the HISTORY.txt file for details). End-users are advised to upgrade their LOTOS NT files:
```
   traian_upc 2020-LOTNT-CASE-CONDITIONS [<file> or <directory>]
```

The old LOTOS NT syntax "?" for "in out" parameters was replaced by a new syntax "!?" aligned on that of LNT. TRAIAN 3.1 still accepts both syntaxes, but now emits a warning wherever "?" is used in place of "!?". The former syntax is deprecated. End-users are advised to upgrade their LOTOS NT files:
```
   traian_upc 2020-LOTNT-ACTUAL-INOUT [<file> or <directory>]
```

Two predefined events ("i" and "UNEXPECTED") have been introduced, so as to make LOTOS NT closer to the LNT language. See the Reference Manual for details.

Bug Fixes

TRAIAN 3.1 no longer allows "asm" and "fortran" to be specified as C identifiers to implement LOTOS NT definitions.

TRAIAN 3.1 was modified to avoid a fatal error ("dead code following a return instruction") that was not justified. See item 184 in the HISTORY.txt file for details.

The data-flow analysis was strengthened, so that TRAIAN 3.1 now rejects LOTOS NT programs (previously accepted by TRAIAN 2.x and 3.0) that contain dead code. See item 185 in the HISTORY.txt file for details.

TRAIAN 3.1 now rejects incorrect LOTOS NT programs containing an "if" instruction without "else" that does not assign all the expected variables. See item 186 in the HISTORY.txt file for details.

TRAIAN 3.1 now rejects incorrect LOTOS NT programs, in which a function may return without assigning one of its "out" parameters on some execution path involving a "if", "case", or "trap" statement.

In certain cases, TRAIAN 3.0 failed to detect a variable (or an exception or a loop identifier) used but not declared. The problem occurred when, e.g., a variable was declared in nested blocks inside a function F1 and was used in another function F2 where it was not declared. In such case, TRAIAN 3.0 would generate incorrect C code that was rejected by the C compiler. This issue was fixed in TRAIAN 3.1.

TRAIAN 3.0 did not properly detect non-initialized variables in "case" instructions with multiple patterns (see item 205 in the HISTORY.txt file for details). In such case, TRAIAN 3.1 emits an error message "variable X may be uninitialized".

TRAIAN 2.x and 3.0 did not detect those LOTOS NT functions declared to return a result but whose body lacks a "return" instruction, and would generate C code for them. TRAIAN 3.1 rejects such situations with an error message. End-users may have to modify their LOTOS NT files to avoid such a new error. One option is to insert an instruction:
```
   raise UNEXPECTED
```
where a "return" is missing, especially after calling an external function that never returns.

Future Work

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

Download

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

http://vasy.inria.fr/traian