TRAIAN 3.15 released on September 29, 2024

The CONVECS team is pleased to announce that version 3.15 of the TRAIAN compiler for LNT is available.

Release Notes

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

In October 2023, TRAIAN found its way into the CADP toolbox, where it supplements the LNT2LOTOS translator with the features of a full-fledged compiler front-end for LNT. Recently, TRAIAN 3.14 became part of CADP 2024-g, TRAIAN 3.15 beta-4 became part of CADP 2024-h, and TRAIAN 3.15 beta-6 became part of CADP 2024-i.

TRAIAN 3.15 brings four language changes, thirty-three static-semantics changes, one release change, and six bug fixes (see below their description).

Language Changes

The definition of the LNT language and its implementation in TRAIAN have been modified as follows. From now on, the ".in" and ".out" qualifiers are only allowed for "in out" parameters. In particular, the ".in" qualifier is no longer allowed for "in" parameters, and the ".out" qualifier is no longer allowed for ".out" parameters (in such cases, these qualifiers were redundant). See item 677 in the HISTORY.txt file.

The definition of LNT and the static-semantics checks implemented in TRAIAN evolved as follows:
From now on, when an "ensure" clause refers to an "in var" parameter X, it must either specify X.in (i.e., the actual parameter value of X when the function or process was called) or X.out (i.e., the value of X when the function or process terminates). Using merely X in an "ensure" clause was ambiguous and is no longer permitted (this restriction already applied to "in out" parameters).
Since "ensure" clauses express guarantees given to the caller of a function or process, it is a bit awkward for them to use the modified value of an "in var" parameter, as the caller is not aware of this value. For this reason, TRAIAN now emits a warning if an "ensure" clause refers to X.out, where X is an "in var" parameter:
```
     dubious ".out" qualifier for "in var" parameter X
```
See item 699 in the HISTORY.txt file.

The definition of LNT and the data-flow analysis done by TRAIAN have been modified to forbid the use, in "ensure" clauses, of "in" parameters that are assigned in the body of a function or process.
Indeed, assigning an "in" parameter is already forbidden, and triggers a warning mentioning that the parameter should be declared "in var" instead of "in". Furthermore, it is ambiguous to use a modified "in" parameter X in an "ensure" clause, because one does not know if X refers to the value of X at the beginning or at the end of the function or process. For "in var" parameters, this ambiguity is now resolved by using ".in" or ".out" qualifiers, but such qualifiers would be meaningless for "in" parameters; thus, a fatal error is now emitted if a modified "in" parameter occurs in an "ensure" clause. See item 701 in the HISTORY.txt file.

The definition of LNT and the static-semantics checks implemented in TRAIAN were further modified. From now on, when an "out" parameter X is used in an "ensure" clause, this no longer triggers a warning that X is both used and modified (namely, the use of X in the "ensure" clause does not imply that X should be an "out var" rather than an "out" parameter). For instance, the two following definitions:
```
   function C (X : nat) : bool is
      return X > 0
   end function

   function F (out X : nat) is
      ensure C (...);
      X := 1 
   end function
```
no longer trigger, in function F, the warning:
```
   "out" parameter X both used and modified (should be an "out var" parameter)
```
See item 702 in the HISTORY.txt file.

Static-Semantics Changes

TRAIAN was modified to no longer reject LNT programs containing the pragmas:
```
   !card 1
```
and/or:
```
   !num_card 1
```
From now on, TRAIAN accept the value 1 for these pragmas, as it makes sense in theory. However, LNT2LOTOS was not designed to handle this case, and will reject (as a "limitation") these pragmas if they come with a value less than two. See item 660 in the HISTORY.txt file.

The data-flow analysis of TRAIAN was refined. Various error messages emitted by TRAIAN:
```
   variable X is uninitialized
```
have been replaced by:
```
   variable X may be uninitialized
```
where it was not fully certain that X was not initialized. This change especially occurred with array elements and when assigning variables in loops containing tests. See item 661 in the HISTORY.txt file.

A semantic check formerly done by LNT2LOTOS was added to TRAIAN. If the pragmas !nat_inf and !nat_sup are both present, TRAIAN checks that the former is less or equal to the latter; if not, the following error message is displayed:
```
   !nat_inf value greater than !nat_sup value
```
Similar checks are done for pragmas !int_inf and !int_sup, leading to the following error message:
```
   !int_inf value greater than !int_sup value
```
Consequently, TRAIAN 3.15 may reject LNT programs accepted by former versions of TRAIAN. See item 662 in the HISTORY.txt file.

The data-flow analysis of TRAIAN was enhanced to detect the situations where a "use X" clause is applied to a variable X that is certainly not initialized. In such case, the "use" clause is meaningless. For instance, given the following definition:
```
   function F (N : nat) : nat is
      var X : nat in
         use X;
         X := 0;
         ...
         return X
      end var
   end function
```
TRAIAN now emits the following warning for the "use" clause:
```
   variable X is uninitialized (superfluous "use")
```
See item 663 in the HISTORY.txt file.

The prior work undertaken to detect "false" and "true" conditions in LNT programs pursued. At present, TRAIAN also issue warnings for the "false" and "true" conditions present in:
- "assert" clauses
- "require" clauses
- "ensure" clauses
- "where" clauses of events
Indeed:
- "assert true [raise E]", "require true [raise E]", and "ensure true [raise E]" can be removed.
- "assert false [raise E]", "require false [raise E]", and "ensure false [raise E]" can be replaced by "raise E" (or "raise UNEXPECTED" if "raise E" is absent).
- "E (?X) where true" can be replaced by "E (?X)".
- "E (?X) where false" can be replaced by "stop".
See item 664 in the HISTORY.txt file.

The error message emitted by TRAIAN when the predefined event "i" is used in unexpected contexts, such as:
```
   access i
   raise i
   X .[i] Y 
```
has been enhanced. The former error message of TRAIAN, namely:
```
   event i is not declared
```
was replaced by more explicative messages emitted during the event-checking or type-checking phases of TRAIAN:
```
   predefined event "i" forbidden in "access" clause
```
or:
```
   event i has non-"raise" channel NONE
```
See item 665 in the HISTORY.txt file.

Two error messages of TRAIAN have been enhanced to make them more informative.

a) The message:

   array type T with empty index range

was replaced by:

   invalid bounds for array type T (5 greater than 1)

b) The message

   range type T with empty range

was replaced by:

   invalid bounds for range type T (2 greater than -1)
   invalid bounds for range type T ('z' greater than 'a')
   etc.

See item 666 in the HISTORY.txt file.

Some static-semantics checks were moved from TRAIAN's type-checking phase to the (earlier) context-checking phase. Consequently, the following errors:
```
   "X.in" allowed only in "ensure" clauses
   "X.out" allowed only in "ensure" clauses
   "result" allowed only in "ensure" clauses
   "result" only allowed in functions that return a result
```
are now displayed sooner by TRAIAN. This also avoids superfluous error messages when the ".in" or ".out" qualifiers were used out of "ensure" clauses. See item 668 in the HISTORY.txt file.

Some other static-semantics checks were moved from TRAIAN's type-checking phase to the (earlier) variable-binding phase, so as to reduce the complexity of the type-checking phase. Consequently, the following errors:
```
   invalid ".in" qualifier for "out" parameter X
   invalid ".out" qualifier for "in" parameter X
   missing ".in" or ".out" after "in out" parameter X
```
are now detected sooner by TRAIAN during variable binding. See item 669 in the HISTORY.txt file.

The verification of module pragmas was strengthened. Formerly, TRAIAN did not detect the case where a module (possibly importing other modules transitively) contained several occurrences of the same module pragma, e.g.:
```
   !int_bits 10
   ...
   !int_bits 10
```
or even:
```
   !int_bits 10
   ...
   !int_bits 13
```
From now on, TRAIAN emits a warning in the former case:
```
   pragma !int_bits already present (with same value) for this module
```
and a (fatal) error in the latter case:
```
   pragma !int_bits already present for this module
```
See item 670 in the HISTORY.txt file.

Inspiration taken from LNT2LOTOS contributed to enhance the error messages emitted by TRAIAN when a process is called in the named style with event parameters occurring several times on the left-hand side of "->" symbols. Formerly, the type-checking phase of TRAIAN would reject such process calls with obscure error messages such as:
```
   process P called with incorrect profile
   in behaviour
      P [E1 -> E2, E1 -> E3]
   the call uses process profile:
      P [E1 : any, E1 : any]
   but the called process has profile: 
      P [E1 : any, E2 : any]
```
From now on, TRAIAN emits a clearer error message:
```
   multiple occurrences of event parameter E1 before "->"
```
which is the same message, for processes, as the message already emitted for functions in presence of similar errors. See item 671 in the HISTORY.txt file.

Inspiration taken from LNT2LOTOS contributed to enhance the error messages emitted by TRAIAN when a process is called in the named style with undeclared event parameters on the left-hand side of "->" symbols. Formerly, the type-checking phase of TRAIAN would reject such process calls with lengthy error messages such as:
```
   error: process P called with incorrect profile
   in behaviour
      P [E1 -> E3]
   the call uses process profile:
      P [E1 : any] 
   but the called process has profile:
      P [E2 : any] 
```
From now on, TRAIAN emits a clearer error message:
```
   process P has no event parameter named E1
```
See item 672 in the HISTORY.txt file.

Inspiration taken from LNT2LOTOS contributed to enhance the error messages emitted by TRAIAN when a function is called in the named style with undeclared event parameters on the left-hand side of "->" symbols. Formerly, the type-checking phase of TRAIAN would reject such function calls with lengthy error messages such as:
```
   function F called with incorrect profile
   in value: 
      F [E1 -> E3] (X)
   no function exists with the requested profile:
      F [E1 : exit] (T1) : any
   but other functions exist with the same name and different
   profiles:
      F [E2 : exit] (X : T1) : T2 
```
From now on, TRAIAN emits a clearer error message:
```
   function F has no parameter named E1
```
or, in the case where function F is overloaded:
```
   no function F has a parameter named E1
```
See item 673 in the HISTORY.txt file.

The grammar of TRAIAN was extended to align it with the syntax of LNT2LOTOS. From now on, the declaration of each constructor of a type can be followed by several pragmas (instead of a single one, formerly). For instance, one can now define:
```
   type T is 
      F1 !implementedby "C:F1" !implementedby "LOTOS:F1",
      F2 !implementedby "C:F2" !implementedby "LOTOS:F2"	
   end type
```
See item 674 in the HISTORY.txt file.

Inspiration taken from LNT2LOTOS contributed to enhance the error messages emitted by TRAIAN when a function or process is called in the named style with undeclared value parameters on the left-hand side of "->" symbols. Formerly, the type-checking phase of TRAIAN would reject such function or process calls with lengthy error messages such as:
```
   function F called with incorrect profile
   in instruction:
      V := F (X -> V1, Z -> V2)
   no function exists with the requested profile:
      F (X : T, X : T) : T
   but other functions exist with the same name and different
   profiles:
      F (X : T, Y : T) : T
```
From now on, TRAIAN emits clearer error messages:
```
   function F has no value parameter named Z
   process F has no value parameter named Z
```
or, in the case where function F is overloaded:
```
   no function F has a value parameter named Z
```
See item 676 in the HISTORY.txt file.

Taking inspiration from LNT2LOTOS, the way TRAIAN handles LNT programs that contain unknown pragmas (e.g., !nat_card for instance) was enhanced. Formerly, TRAIAN would emit verbose lexical/syntactic errors:
```
   !nat_card 0
      ^
   TEST.lnt:3: error: "a" is deleted

   !nat_card 0
       ^
   TEST.lnt:3: error: "r" is deleted

   !nat_card 0
	^
   TEST.lnt:3: error: "d" is deleted

   etc.
```
From now on, TRAIAN emits a more intuitive error message:
```
   unknown module pragma !nat_card
```
See item 678 in the HISTORY.txt file.

The checks done by TRAIAN for the "any" channel have been strengthened. It is no longer allowed to define a channel named "any" (or any case-sensitive variant of "any"). In such case, TRAIAN emits a new error message:
```
   forbidden declaration of predefined channel "any"
   forbidden declaration of predefined channel "Any"
   forbidden declaration of predefined channel "ANY"
```
Former versions of TRAIAN tolerated the definition of "Any" or "ANY" but later considered these channels as different from "any". They rejected the definition of "any", but with a cryptic internal error message:
```
   redundant binding for channel any
```
See item 679 in the HISTORY.txt file.

To discourage using case-sensitive variants of the "any" channel, added to TRAIAN a new warning:
```
   predefined channel noted "Any" instead of "any"
   predefined channel noted "ANY" instead of "any"
```
See item 680 in the HISTORY.txt file.

Taking inspiration from LNT2LOTOS, the grammar of TRAIAN was extended to syntactically accept incorrect pragmas attached to types, constructors, functions, and processes. Formerly, TRAIAN would reject such incorrect pragmas with a syntax error. From now on, it displays more informative messages, such as:
```
   unknown type pragma !enumeratedby
   unknown function pragma !revertedby
   unknown process pragma !iterated
   forbidden pragma !external for constructor
```
See item 681 in the HISTORY.txt file.

The way TRAIAN reports about pragmas improperly written using capital letters was enhanced. Formerly, when TRAIAN detected capital letters in a pragma name (e.g., "!ComparedBy" instead of "!comparedby"), it reported a syntax error, followed by proposals for recovery. From now on, TRAIAN syntactically accepts such a pragma, but emits a dedicated error message such as:
```
   pragma name !ComparedBy contains uppercase characters
```
See item 682 in the HISTORY.txt file.

The data-flow analysis of TRAIAN was further enhanced to change certain error messages:
```
   variable X may be uninitialized
```
into:
```
   variable X is uninitialized
```
when TRAIAN is absolutely sure that X is not initialized. See item 683 in the HISTORY.txt file.

The error and warning messages emitted by TRAIAN for duplicated or redundant "with" clauses have been enhanced. From now on, TRAIAN mentions, in such messages, the line number of (the first function defined in) the "with" clause, rather than the first line of the module or type containing the "with" clause. See item 685 in the HISTORY.txt file.

Further checks have been added to detect occurrences of "use X" clauses at places where variable X will be used later on at least one execution path. For such occurrences, TRAIAN now emits a new warning:
```
   variable X is used later (superfluous "use")
```
See item 686 in the HISTORY.txt file.

The error messages emitted by TRAIAN for write-write conflicts in parallel composition were shortened. Formerly, TRAIAN emitted messages such as:
```
   X is modified in the 1st, 2nd, and 3rd parallel branches
   but used in the 1st and 3rd parallel branches
```
which were too detailed, since the existence of a write-write conflict is enough to reject the LNT program. From now on, when a "par" operators contains both write-write and read-write conflicts on the same variable, TRAIAN will only display the write-write conflicts, e.g.:
```
   X is modified in the 1st, 2nd, and 3rd parallel branches
```
See item 688 in the HISTORY.txt file.

The error messages emitted by TRAIAN for read-write conflicts in parallel composition were also shortened. Formerly, TRAIAN emitted messages such as:
```
   X is modified in the 1st parallel branch but used in the 1st and 2nd parallel branches
```
The information that X is both read and written in the 1st branch was not useful. From now on, TRAIAN displays shorter messages such as:
```
   X is modified in the 1st parallel branch but used in the 2nd parallel branch
```
See item 689 in the HISTORY.txt file.

The error messages emitted by TRAIAN for write-write and read-write conflicts in parallel compositions were further enhanced by adding line numbers that point out where variables are read or modified. For instance, the messages:

   X is modified in the 1st and 2nd parallel branches

and:

   X is modified in the 1st parallel branch but used in the 2nd parallel branch

become, respectively:

   X is modified in the 1st (line 13) and 2nd (line 18) parallel branches

and:

   X is modified in the 1st (line 11) parallel branch but used in the 2nd (line 24) parallel branch

See item 690 in the HISTORY.txt file.

Inspiration taken from LNT2LOTOS contributed to enhance the messages emitted by TRAIAN when some function or process is called with too few or too many (event or value) parameters. Formerly, TRAIAN would emit generic error messages of the following form:
```
   function F called with incorrect profile
   process P called with incorrect profile
```
From now on, TRAIAN emits more precise error messages:
```
   function F called with 0 instead of 1 event parameter(s)
   function F called with 2 instead of 1 value parameter(s)
   process P called with 1 instead of 2 event parameter(s)
   process P called with 2 instead of 3 value parameter(s)
```
For overloaded functions, TRAIAN emits slightly different error messages:
```
   function F called with 1 instead of at least 2 event parameter(s)
   function F called with 4 instead of at most 3 value parameter(s)
```
In all cases, these messages are followed by a detailed explanation about the permitted profiles for the function or process. See item 691 in the HISTORY.txt file.

The messages emitted by TRAIAN for events invoked with an incorrect number of offer parameters have been enhanced. Formerly, TRAIAN would display a generic error message:
```
   event E used with incorrect channel
```
From now on, TRAIAN emits a more precise message, such as:
```
   event E accessed with 1 instead of 2 parameter(s)
```
If the channel has several profiles, the message emitted by TRAIAN may be slightly different, depending whether there are too few or too many parameters:
```
   event E accessed with 1 instead of at least 2 parameter(s)
   event E accessed with 5 instead of at most 4 parameter(s)
```
In all cases, these messages are followed by a detailed explanation about the permitted profiles for the event. See item 692 in the HISTORY.txt file.

Checks have been added, that detect useless occurrences of the "access" construct, leading to the new warning:
```
   event E is already accessed (superfluous "access")
```
See item 693 in the HISTORY.txt file.

Inspiration taken from LNT2LOTOS helped to shorten the error messages emitted by TRAIAN when a process is called in the positional style and either only one event parameter has an incorrect channel or only one value parameter has an incorrect type. In such cases, instead of displaying the default (verbose) message for incorrect process calls, TRAIAN emits a one-line message:
```
   Nth event parameter of process P has channel C1 instead of C2
```
or:
```
   Nth value parameter of process P has type T1 instead of T2
```
See item 694 in the HISTORY.txt file.

Inspiration taken from LNT2LOTOS helped to shorten the error messages emitted by TRAIAN when a non-overloaded function is called in the positional style and either only one event parameter has an incorrect channel or only one value parameter has an incorrect type. In such cases, instead of displaying the default (verbose) message for incorrect function calls, TRAIAN emits a one-line message:
```
   Nth event parameter of function F has channel C1 instead of C2
```
or:
```
   Nth value parameter of function F has type T1 instead of T2
```
See item 696 in the HISTORY.txt file.

The following error message:
```
   event E has non-"raise" channel C
```
that TRAIAN emitted when a function was called with an event parameter whose channel is not a "raise" channel (i.e., an exception) was removed. This message was a bit obscure and is now replaced with TRAIAN's default error message when a function is called with an event parameter having the wrong channel. See item 697 in the HISTORY.txt file.

The error messages emitted by TRAIAN for mistyped events whose channel has a unique profile and that are invoked with offer parameters in the positional style have been simplified. When only one offer parameter is mistyped, TRAIAN now displays a concise error message:
```
   Nth parameter of event E has type T1 instead of T2 required by channel C
```
instead of the default (more detailed, but more verbose) error message for incorrect events. See item 698 in the HISTORY.txt file.

Release Changes

The manual of TRAIAN was modified to replace LOTOS NT by LNT (almost) everywhere. The title of this manual also changed from "LOTOS NT User Manual" to "LNT User Manual". See item 675 in the HISTORY.txt file.

Bug Fixes

A spurious warning:
```
   variable X not used
```
emitted when some variable X was assigned by an "eval" and not used later, was removed. Yet, in such case, a warning:
```
   useless assignment
```
is still displayed for variable X. See item 659 in the HISTORY.txt file.

The following bug was fixed: when two LNT types had "with get" and/or "with set" clauses with the same pragma !implementedby "LOTOS:...", TRAIAN would abort (i.e., raise the UNEXPECTED event). From now on, it halts properly after displaying the following error message:
```
   "pragma !... already present for this function"
```
See item 667 in the HISTORY.txt file.

In the data-flow analysis of TRAIAN, a bug was fixed, which caused correct LNT programs to be rejected. For instance, the following process definition:
```
   process P (X: bool, out var Y: bool, out Z: bool) is
      case X in
         false -> Y := true
      |  true -> stop
      end case;
      Z := Y
   end process
```
triggered an error message:
```
   process P may return without assigning "out" parameter Y
```
This issue has been solved by ignoring, when determining whether "out" variables are assigned or not, all "case" branches that do not terminate. See item 684 in the HISTORY.txt file.

An issue was detected and fixed in the data-flow analysis done by TRAIAN to compute the variables necessarily defined in "case" statements. This error led to the computation of a possibly too small set of variables. See item 687 in the HISTORY.txt file.

In data-flow analysis, a bug was found and fixed that, in a few cases, prevented TRAIAN from detecting write-write conflicts in parallel compositions, and thus led to the acceptance of incorrect LNT programs. See item 695 in the HISTORY.txt file.

A bug was fixed in the data-flow analysis of TRAIAN: from now on, in "ensure" clauses, the occurrences of X (where X is an "in" or "in var" parameter) or X.in (where X is an "in out" parameter) are now counted as uses of X at the beginning (rather than the end) of the function or process, even if the "ensure" clause is evaluated last, because these occurrences refer to the value of X upon entry of the function or process.
For instance, given the following definition:
```
   function F (in out X : nat, Y : nat) is
      ensure Y == X.in;
      X := Y
   end function
```
TRAIAN no longer display a warning:
```
   "in out" parameter X modified before used (should be an "out var" parameter) 
```
Also, given the following definition:
```
   function F (in var X : nat, Y : nat) is
      ensure X.in > 0;
      case Y in
         0 -> X := 1
      |  X -> null
      end case
   end function
```
TRAIAN now displays two warnings:
```
   useless assignment to X
```
See item 700 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 further deepen the co-operation between TRAIAN and the LNT2LOTOS translator.

Download

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

http://vasy.inria.fr/traian