TRAIAN 3.13 released on March 30, 2024

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

Release Notes

TRAIAN 3.13 has been prepared by Hubert Garavel, Frederic Lang, and Wendelin Serwe, with contribution of Radu Mateescu who reported a bug. It was released three months after version 3.12 of TRAIAN.

In October 2023, TRAIAN became part of the CADP toolbox, where it provides a full-fledged compiler front-end for the LNT language, allowing to catch mistakes not detected by the "lightweight" approach of the LNT2LOTOS translator. Precisely, TRAIAN 3.12 was integrated in CADP 2024-a; later, TRAIAN 3.13 beta 2 became part of CADP 2024-b and TRAIAN 3.13 beta 5 became part of CADP 2024-c.

TRAIAN 3.13 brings three language changes, twelve static-semantics changes, four code-generation changes, one release change, and five bug fixes (see below their description).

Language Changes

An alternative notation was introduced for the "select" construct. From now on:
```
   select
      B1
   []
      ...
   []
      Bn
   end select
```
may also be written, equivalently:
```
   alt
      B1
   []
      ...
   []
      Bn
   end alt
```
The reasons for this evolution are threefold:
- The keyword "alt" has the same length as "par", thus enforcing a nice symmetry, whereas "select" was sometimes felt too long and verbose.
- Introducing the keyword "alt", which was present in the Occam language, is our tribute to Tony Hoare (see "The transputer and occam: a personal story", Concurrency: Practice & Experience, August 1991).
- In the code and documentation of TRAIAN, the word "select" was also used for other purposes: field selector, array selection, etc. Adopting a different name ("alt") for nondeterminism was therefore suitable.
From now on, "select" is deprecated. The use of "alt" should be preferred when writing new LNT programs. The evolution is scheduled in three steps:
1. For one year, it will be possible to use either "select" or "alt". However, mixing both in the same LNT program is forbidden (leading to a fatal error).
2. In the next year, the use of "select" will trigger a non-fatal warning.
3. After two years, the use of "select" will trigger a fatal error.
Users are advised to upgrade their LNT programs by running the following command:
```
   traian_upc 2024-LOTNT-SELECT [<file> or <directory>]
```
which will replace "select" by "alt" automatically. See item 619 in the HISTORY.txt file.

The semantics of exceptions in LNT has evolved. This was done in several steps:
1. A new channel EXIT (similar to NONE, yet different) has been added to "lotosnt_predefined.lnt".
2. The channel of the UNEXPECTED event is no longer NONE, but EXIT.
3. From now on, the event parameters of LNT processes and functions must be declared with channel EXIT (instead of NONE) if these parameters correspond to exceptions.
  Users are advised to upgrade their LNT programs by running the following command:
```
      traian_upc 2024-LOTNT-EXIT [<file> or <directory>]
```
  which will automatically replace NONE by EXIT for the event parameters of functions. This only applies to functions: process definitions that declare exceptions must be updated manually (fortunately, such definitions are less frequent than functions raising exceptions).
4. In the predefined library and scheme files of TRAIAN (namely, "lotosnt_predefined.lnt", "scheme_list.lnt", "scheme_sorted_list.lnt", and "scheme_set.lnt"), NONE has been replaced by EXIT in the definition of event parameters of standard functions.
5. From now on, TRAIAN checks that all event parameters of functions have the channel EXIT. Formerly, this check was not done by TRAIAN itself, but LNT2LOTOS rejected all function definitions with event parameters not having the channel NONE.
6. TRAIAN now checks that, in any "raise E" instruction or behaviour, the event E has channel EXIT.
7. TRAIAN now checks that, in any "trap E ..." instruction or behaviour, the event E has channel EXIT.
8. TRAIAN now checks that, in any "E(...)" behaviour, the event E does not have channel EXIT.
9. TRAIAN now checks that, in any "hide E ..." behaviour, the event E does not have channel EXIT.
The editor style files (in directory "$LNTDIR/ext") have been updated to recognize EXIT as a predefined channel, in the same way as NONE. See item 620 in the HISTORY.txt file.

The syntax of "trap" instructions and behaviours was modified, in order:
- to make it simpler and coherent with other LNT constructs,
- to align it with the syntax proposed in the research paper by Garavel & Sighireanu: On the Introduction of Exceptions in E-LOTOS (FORTE/PSTV'1996).
The former syntax:
```
   trap
      exception E1 is I1,
      ...,
      exception En is In
   in
      I0
   end trap
```
has been replaced with:
```
   trap
      E1:exit -> I1
   |  ...
   |  En:exit -> In
   in
      I0
   end trap
```
(same for behaviours B0, B1, ..., Bn).
Users are advised to upgrade their LNT programs by running the following command:
```
   traian_upc 2024-LOTNT-TRAP [<file> or <directory>]
```
which will update "trap" constructs automatically.
Consequently, "exception" is no longer a reserved keyword. The editor style files (in directory "$LNTDIR/ext") have been updated accordingly. See item 621 in the HISTORY.txt file.

Static-Semantics Changes

Taking inspiration from the static semantics checks already implemented in the LNT2LOTOS translator, the static analysis done by TRAIAN on LNT parallel operators was enhanced, leading to better messages. In particular, the warning:
```
   useless assignment to X
```
is now displayed more often, especially when a branch of a "par" statement assigns variable X, e.g.:
```
   X := 0; -- warning: useless assignment to X
   Y := 0; -- warning: useless assignment to Y
   par
      X := 1 || G (?Y)
   end par;
   PRINT (X, Y)
```
See item 604 in the HISTORY.txt file.

The static semantics checks done by TRAIAN have been enhanced to avoid certain warnings that were counter-intuitive. From now on, TRAIAN no longer displays the following warning:
```
   "out" parameter X both used and modified (should be an "out var" parameter)
```
when variable X is only used in an input guard, e.g.:
```
   process P [G: any] (out X: Nat) is
      G (?X) where X < 10
   end process
```
or in the "where" clause of a nondeterministic assignment:
```
   process P [G: any] (out X: Nat) is
      X := any Nat where X < 10
   end process
```
Similarly, the warning:
```
   "out var" parameter X never used (should be an "out" parameter)
```
is no longer displayed when variable X is only used in the "where" clause of an input or a nondeterministic assignment, e.g.:
```
   process P (out var X: Int) is
      X := any Int where (X >= 0) and (X < 10)
   end process
```
See item 606 in the HISTORY.txt file.

The data flow analysis of TRAIAN was modified, so that the warning:

   "in out" parameter X modified before used (should be an "out" parameter)

is now displayed more often, e.g., in the following example:

   function F (B: Bool, in out X: Nat): Nat is
      loop L in
         if B then
            X := 0
         else
            X := 1
         end if;
         ...
      end loop
   end function

See item 607 in the HISTORY.txt file.

The static semantics checks of TRAIAN have been further enhanced, based on those of LNT2LOTOS. From now on, TRAIAN emits the warning:

   useless assignment to X

more often in presence of loops that do not terminate, e.g.:

   loop
      X := 1 -- warning: useless assignment to X
   end loop

or:

   X := 0; -- warning: useless assignment to X
   loop
      X := any Nat where X < 10;
      ...
   end loop

or:

   loop L in
      if B then
         X := 0;
         break L
      end if;
      X := 1 -- warning: useless assignment to X
   end loop

See item 608 in the HISTORY.txt file.

Two new warnings have been introduced in TRAIAN:
a) From now on, if a module has a "with F" clause, where F is either NIL, CONS, or INSERT, TRAIAN emits a warning:
```
      useless clause "with F" in module M
```
b) From now on, if a list, sorted list, or set type T has a "with F" clause, where F is either NIL, CONS, or INSERT, with no pragma (namely, !implementedby or !external) attached to this clause, TRAIAN emits a warning:
```
      useless clause "with F" in type T
```
In both cases, the "with" clause is indeed useless since:
- Only lists, sorted lists, and sets may have such a "with F" clause;
- For these types, the NIL, CONS, and INSERT functions are defined automatically;
- The "with F" clause is only useful if it comes with a pragma that qualifies function F.
See item 609 in the HISTORY.txt file.

The static analysis of TRAIAN was refined to emit more accurate warnings. For instance, given the definition:

   function F [E : none] (X : BOOL, out Y : BOOL) : BOOL is
      trap
         exception Y is
	    X := false
         exception Z is
	    raise E
      in
         loop
	    raise Z
         end loop
      end trap;
      return X or Y
   end function

TRAIAN now displays:

   "in" parameter X modified (should be an "in var" parameter)

rather than:

   "in" parameter X modified before used (should be a local variable)

See item 612 in the HISTORY.txt file.

The static analysis done by TRAIAN for "stop" behaviours was enhanced, exploiting the fact that no variable can be read after "stop", even the variables of "ensure" clauses. Consequently, more warnings of the form:
```
   useless assignment to X
```
are now displayed by TRAIAN, e.g.
```
   process MAIN [PRINT : any] (out X : BOOL) is
      X := true;  --  warning: useless assignment to X
      stop
   end process
```
See item 613 in the HISTORY.txt file.

The static analysis of TRAIAN was further enhanced, to warn about "ensure" clauses that cannot be executed because the function or process contains infinite loops or "stop" behaviours (the latter being only allowed for processes):
```
   unreachable "ensure" (dead code) after infinite loop
   unreachable "ensure" (dead code) after "stop"
```
See item 614 in the HISTORY.txt file.

The static analysis of "case" patterns was enhanced. From now on, TRAIAN does more accurate checks for pattern exhaustiveness and emits more warnings of the following form:
```
   superfluous pattern(s) after the Nth pattern
```
when the previous patterns from 1 to (N-1) already cover all possible cases. In practice, these new warnings enable one to detect and simplify LNT programs containing useless patterns (such as extra patterns "any -> null" that were formerly required by TRAIAN 2.x). See item 615 in the HISTORY.txt file.

The error messages emitted by TRAIAN for functions containing infinite loops have been simplified. From now on, the couples of error messages:
```
   - function with "out" parameter(s) but looping infinitely
   - infinite loop
```
and:
```
   - function with result but looping infinitely
   - infinite loop
```
are replaced by a single error message:
```
   function looping infinitely
```
which is less ambiguous, as it does not suggest that functions having neither "out" parameters nor result are allowed not to terminate. The messages emitted by TRAIAN for processes that contain infinite loops are kept unchanged. See item 616 in the HISTORY.txt file.

The data flow analysis of TRAIAN was enhanced to better analyze the continuations of "raise" behaviours. This led to simpler warning messages:
```
   unreachable behaviour (dead code) after ...
```
by removing, from the "..." list, infinite loops when they are followed by an event and "raise" behaviours if their event is local to a "trap" in which it is declared. See item 622 in the HISTORY.txt file.

The data flow analyses for "trap" instructions and "trap" behaviours have been unified. Hence, TRAIAN now emits more warnings, e.g.:
```
   loop body is executed at most once
```
or:
```
   unreachable behaviour (dead code) after infinite loop and "break"
```
for processes that contain "trap" behaviours. See item 623 in the HISTORY.txt file.

Code-Generation Changes

The code generation of TRAIAN was extended to produce C code for implementing the FIRST and LAST functions on cascade types. See item 600 in the HISTORY.txt file.

The readability of the C code produced by TRAIAN was enhanced: from now on, TRAIAN generates more or fewer blank lines, dashed lines, or double dashed lines where appropriate (especially in the implementation of cascade types). See item 610 in the HISTORY.txt file.

The code generator of TRAIAN was modified to produce the C code that implements the FIRST and LAST functions for singleton types. The code generator was also modified not to generate the PRED and SUCC functions for singleton types, as these two functions are no longer supported. See item 617 in the HISTORY.txt file.

The implementation of the "<=>" and "xor" operators on Booleans was optimized. From now on, the two functions ADT_IFF() and ADT_XOR() defined in file "incl/lotosnt_predefined.h" have been replaced by two macro-definitions, which are simpler and faster. See item 618 in the HISTORY.txt file.

Release Changes

The 32-bit Windows executables ("win32") have been removed from the TRAIAN release, because they are nicely replaced by 64-bit Windows executables ("win64"), which are faster. Thus, the directories bin.win32 and gc/bin.win32 have been deleted. See item 603 in the HISTORY.txt file.

Bug Fixes

The code generation of TRAIAN for cascade types was corrected: formerly, if a cascade type T had a clause "with STRING", TRAIAN did not generate the selector and updater functions for type T, resulting in incomplete C code that did not compile properly. See item 601 in the HISTORY.txt file.

Another problem was fixed in the C code generation for cascade types: for some (but not all) constructors Ci of cascade types, the TRAIAN_MATCH_Ci() macro-definitions used for pattern-matching were incorrectly generated and could return incorrect Boolean results. This issue was solved. See item 602 in the HISTORY.txt file.

An error in the implementation of the operator "=>" on Booleans was found and repaired. The C macro-definition ADT_IMPLIES() that implemented this operator was incorrect. The error was introduced in October 2023 and has been present in versions 1.178 to 1.184 (included) of "lotosnt_predefined.h". Versions 3.11 and 3.12 of the TRAIAN compiler were not affected by the error, nor any CADP tools built using TRAIAN; only the include file "lotosnt_predefined.h" released with TRAIAN 3.12 was wrong. See item 605 in the HISTORY.txt file.

An issue in the data flow analysis of TRAIAN was corrected to avoid a spurious warning. From now on, TRAIAN better analyzes function and process calls where the same variable X is used in various arguments that have different modes ("in", "out", "in out", etc.). For instance, TRAIAN no longer emits incorrect warnings for such calls:
```
   function F1 (Y : Nat) : Nat is
      var X : Nat in
         X := Z;  -- no more warning: useless assignment to X
         F2 (?X, X);
         return X
      end var
   end function
```
because, in the call "F2 (?X, X)", X is necessarily read before written. Indeed, "in" and "in out" parameters are read before the call, while "out" and "in out" parameters are written after the call, in whatever order these arguments are passed to the called function. See item 611 in the HISTORY.txt file.

An error was fixed in the data flow analysis for "trap" handlers that do not terminate normally, i.e.:
- In a "trap" instruction, handlers that raise an event:
```
   trap
      E: exit -> raise E'
   ...
```
- In a "trap" behaviour, handlers that raise an event or contain an infinite loop:
```
   trap
      E1: exit -> raise E'1
   |  E2: exit -> loop E'2 end loop
   ...
```
This correction suppressed various error messages emitted by TRAIAN, e.g.:
```
   - process with "out" parameter(s) but looping infinitely
   - function F may return without assigning parameter X
   - process P may return without assigning parameter Y
```
See item 624 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 part of the CADP toolbox, in which it serves to analyze formal specifications of concurrent systems.

We plan to pursue the progressive unification of the LOTOS NT and LNT languages, and to increase the co-operation between the LNT2LOTOS and TRAIAN compilers.

Download

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

http://vasy.inria.fr/traian