TRAIAN 3.16 released on December 27, 2024

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

Release Notes

TRAIAN 3.16 has been prepared by Hubert Garavel, Frederic Lang, and Wendelin Serwe. It was released three months after version 3.15 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.15 became part of CADP 2024-j, TRAIAN 3.16 beta-5 became part of CADP 2024-k, and TRAIAN 3.16 beta-7 became part of CADP 2024-l.

TRAIAN 3.16 brings five language changes, eight static-semantics changes, four compiler changes, and four bug fixes (see below their description).

Language Changes

The behaviour of TRAIAN was further aligned on that of LNT2LOTOS. From now on, the "with val" clause is only allowed for enumerated types and range types. TRAIAN now rejects such clauses for other types with the following error message:
```
   forbidden function val in "with" clause of type T
```
See item 707 in the HISTORY.txt file.

The analysis of TRAIAN was made stricter. From now on, the use of a modified "in" parameter in an "ensure" clause triggers a fatal error, rather than a warning:
```
   error: modified "in" parameter X forbidden in "ensure" clause (should be an "in var" parameter)
```
See item 711 in the HISTORY.txt file.

Following a prior change (see item #708), the syntax of LNT types was extended to allow predicate types without conditions. From now on, the following type definition
```
   type T is X:T' end type
```
is permitted, and is equivalent to:
```
   type T is X:T' where true end type
```
but does not trigger the warning mentioned at item #708. Such a type definition introduces a new type T that is identical to the existing type T', except that values of type T and T' are not compatible and cannot be mixed together without explicit type conversions. This is similar to the concept of "derived types" in Ada. See item 716 in the HISTORY.txt file.

TRAIAN was made stricter with respect to module imports. From now on, all the identifiers used in a module M should have been declared either in M, or in one of the sub-modules transitively imported by M, or in one of the LNT files transitively included by M (using "library" directives).
Otherwise, TRAIAN now emits warnings to report identifiers used in a module but declared in another module that is not transitively imported or included by M:
```
   channel C is declared in non-imported module M'
   function F is declared in non-imported module M'
   process P is declared in non-imported module M'
   type T is declared in non-imported module M'
```
Each warning is displayed only once, even if the identifier is used multiple times.
Such warnings promote a clearer, DAG-like organization of LNT modules as self-contained collections of definitions. See item 719 in the HISTORY.txt file.

LNT was extended to support generic modules parameterized by formal definitions of types, channels, functions, or processes. The first step was done to introduce modules parameterized by (so-called "virtual") processes.
Any module M can now declare processes containing a new "!virtual" pragma. The body of such processes must be empty. The value parameters of virtual processes should not be declared with modes "in var" or "out var", but "in" or "out", respectively. Otherwise, TRAIAN issues the following warnings:
```
  "in var" parameter X of virtual process P should be an "in" parameter

  "out var" parameter Y of virtual process P should be an "out" parameter
```
Each virtual process can later be instantiated with another "actual" process having the same name and the same profile, i.e., parameters with the same names, types or channels, and modes; however, the "in" and "out" parameters of a virtual processs may be matched by the corresponding "in var" and "out var" parameters of a real process.
This actual process may be defined in a module that is not transitively imported or included by M, and does not trigger any warning (see item #719 above). See item 721 in the HISTORY.txt file.

Static-Semantics Changes

The event binding phase of TRAIAN was modified to ensure that binding errors in "par" operators are reported by increasing line numbers. For instance, the following error messages:

   FILE.lnt:177: error: event Input is not declared
   FILE.lnt:180: error: event Input is not declared
   FILE.lnt:178: error: event Input is not declared
   FILE.lnt:178: error: event actionA is not declared
   FILE.lnt:178: error: event actionB is not declared

are now displayed in a correct order:

   FILE.lnt:177: error: event Input is not declared
   FILE.lnt:178: error: event Input is not declared
   FILE.lnt:178: error: event actionA is not declared
   FILE.lnt:178: error: event actionB is not declared
   FILE.lnt:180: error: event Input is not declared

See item 704 in the HISTORY.txt file.

Some error messages of TRAIAN have been enhanced, which could be ambiguous, e.g.:

   1st event parameter of process P has channel D instead of C
   2nd value parameter of function F has type T2 instead of T1
   3rd parameter of event E has type T2 instead of T1 required
   by channel C

as it was unclear whether these messages referred to formal or actual parameters. From now on, TRAIAN displays clearer error messages:

   1st event parameter of process P supplied with channel D instead of C

   2nd value parameter of function F supplied with type T2 instead of T1

   3rd parameter of event E supplied with type T2 instead of T1 required by channel C

See item 705 in the HISTORY.txt file.

Pursuing prior efforts to simplify the error messages emitted by TRAIAN when events, functions, and processes are called with incorrect arguments passed in the named style (see items #694, #696, and #698), the messages were further simplified to also deal with arguments passed in the positional style. For instance, the former error message:

   FILE.lnt:6: error: event E accessed with incorrect channel
   in behaviour:
      E (X -> "false")
   channel C cannot match the profile:
      (X : String)

now displays as:

   FILE.lnt:6: error: 1st parameter X of event E supplied with
   type String instead of Bool required by channel C

Also, the former error message:

   FILE.lnt:9: error: function F called with incorrect profile 
   in pattern:
      F (X -> 1.0, Y -> 2, Z -> -1)
   no function exists with the requested profile:
      F (X : real, Y : NAT|INT, Z : int) : any 
   but other functions exist with the same name and different
   profiles:
      F (X : int, Y : int, Z : int) : Point at FILE.lnt:19

now displays as:

   FILE.lnt:9: error: 1st value parameter X of function F
   supplied with type real instead of int

Similarly, the former error message:

   FILE.lnt:37: error: process P called with incorrect profile
   in behaviour
      P [E -> E']
   the call uses process profile:
      P [E : D]
   but the called process has profile:
      P [E : C]

now displays as:

   FILE.lnt:37: error: 1st event parameter E of process P
   supplied with channel D instead of C

See item 706 in the HISTORY.txt file.

Warnings have been added for those LNT predicate types whose "where" condition is always false (respectively, always true). For such types, TRAIAN emits warnings of the following form:
```
   warning: condition always false
```
or
```
   warning: condition always true
```
See item 708 in the HISTORY.txt file.

The warning messages emitted by TRAIAN for the presence of "with get" or "with set" clauses in enumerated types or range types have been enhanced. Formerly, TRAIAN warned about such clauses with the following messages:
```
   unknown function get in "with" clause of type T
   unknown function set in "with" clause of type T
```
which could be confusing, since "with get" and "with set" are known clauses. From now on, TRAIAN displays better messages:
```
   forbidden function get in "with" clause of type T
   forbidden function set in "with" clause of type T
```
See item 709 in the HISTORY.txt file.

A new phase named "module binding", which performs stricter checks on module identifiers, was added to TRAIAN. See item 714 in the HISTORY.txt file.

A warning was added to report situations where a variable is used and later modified in a pattern or a list of patterns. For instance, the following LNT code fragment:
```
   case X
   var N: NAT in
      C (N where N < Y, Y) ->
	 return N + Y
   ...
   end case
```
triggers the new warning:
```
   variable Y assigned after being used in "where" condition
```
See item 717 in the HISTORY.txt file.

The static detection by TRAIAN of Boolean conditions that are always true or always false was enhanced and aligned with that of LNT2LOTOS. For instance, the following tautologies are now recognized:
```
   true and false or true
   true or false == false
   false == false or true
   not (true == false)
   true or B, where B is a Boolean variable
```
This leads to more warnings. Also, certain LNT programs that were formerly accepted are now rejected, e.g.:
```
   function F (in var X : Int) : Int is
      while not (false [...] ()) loop
         X := X - 1
      end loop;
      return X
   end function
```
See item 722 in the HISTORY.txt file.

Compiler Changes

In order to align TRAIAN with LNT2LOTOS and LNT_DEPEND, the search rules for sub-modules specified in "module" clauses have been modified. From now on, TRAIAN no longer searches sub-modules in the current directory (i.e., the directory from which TRAIAN is invoked), but in the directory containing the principal LNT file. Otherwise, these files are searched in $LNTDIR/lib or $CADP/lib.
This modifies the result of the "-depend" option of TRAIAN. For instance, the command:
```
   traian -depend /CADP/demos/demo_38/DES.lnt
```
now displays:
```
   /CADP/lib/lotosnt_predefined.lnt
   /CADP/demos/demo_38/CONTROLLER.lnt
   /CADP/demos/demo_38/CHANNELS.lnt
   /CADP/demos/demo_38/TYPES.lnt
   /CADP/lib/BIT.lnt
   /CADP/demos/demo_38/DATA_PATH.lnt
   /CADP/demos/demo_38/PERMUTATION_FUNCTIONS.lnt
   /CADP/demos/demo_38/CIPHER.lnt
   /CADP/demos/demo_38/S_BOX_FUNCTIONS.lnt
   /CADP/demos/demo_38/KEY_PATH.lnt
```
Formerly, the same command would display nothing and stop with the exit code 1, unless it was launched from the directory /CADP/demos/demo_38. In such case, the commands:
```
   cd /CADP/demos/demo_38
   traian -depend DES.lnt
```
would display:
```
   /CADP/lib/lotosnt_predefined.lnt
   CONTROLLER.lnt
   CHANNELS.lnt
   TYPES.lnt
   /CADP/lib/BIT.lnt
   DATA_PATH.lnt
   PERMUTATION_FUNCTIONS.lnt
   CIPHER.lnt
   S_BOX_FUNCTIONS.lnt
   KEY_PATH.lnt
```
See item 712 in the HISTORY.txt file.

TRAIAN was made easier to use for CADP users. From now on, if the environment variable $LNTDIR is not defined, TRAIAN replaces it with the value of the environment variable $CADP, if this variable is defined. See item 713 in the HISTORY.txt file.

TRAIAN was enhanced to generate, in the LNTGEN directory, the ".mod" and ".sig" files formerly generated by LNT_DEPEND and LNT2LOTOS. See item 715 in the HISTORY.txt file.

A new option "-pidlist" was added to TRAIAN. This option, which displays the list of process identifiers defined in an LNT program, is used by EUCALYPTUS. Formerly, this option was implemented in LNT2LOTOS, but logically belongs to the functionalities provided by TRAIAN. See item 720 in the HISTORY.txt file.

Bug Fixes

An issue was fixed in the type checking phase of TRAIAN: following recent changes, TRAIAN could abort (by raising the UNEXPECTED event) if a pattern containing "any" was incorrectly typed:

   ...
   traian:    - type checking
   bin.sol64/lotosnt.c:12840: "UNEXPECTED" event raised
   routine call stack:
	CHECK_TYPE [check_type.lnt:21]
	CHECK_TYPE_M1_Mn [check_type.lnt:1108]
	CHECK_TYPE_P1_Pn [check_type.lnt:1139]
	CHECK_TYPE_B [check_type.lnt:98]
	CHECK_TYPE_DDD1_DDDn [check_type.lnt:772]
	CHECK_TYPE_DD1_DDn [check_type.lnt:756]
	CHECK_TYPE_D1_Dn [check_type.lnt:729]
	CHECK_TYPE_D [check_type.lnt:687]
	SYNTHESIS_D [check_type.lnt:1301]
	SYNTHESIS_F_CALL [check_type.lnt:1468]

See item 703 in the HISTORY.txt file.

The data-flow analysis performed by TRAIAN on "case" patterns was enhanced. Given the following LNT code fragment:
```
   function F (X: Bool, Z: T) : Bool is
      case Z in
         A | B (X) -> X := not (X)
      |  C (X) -> null
      end case;
      return X
   end function
```
TRAIAN emitted the warning:
```
   "in" parameter X modified before used (should be a local variable)
```
which was incorrect, since the first branch (with pattern A) of the "case" reads X before assigning it. From now on, TRAIAN displays the following warning:
```
   "in" parameter X modified (should be an "in var" parameter)
```
See item 710 in the HISTORY.txt file.

Another issue was fixed, which occurred for LNT programs containing multiple occurrences of the "!int_check N" pragma, with the same value of N. In such case, TRAIAN no longer emits a fatal error, but only a warning. This new behaviour is consistent with the way other similar pragmas are handled by TRAIAN. See item 718 in the HISTORY.txt file.

The following issue was fixed: when TRAIAN was invoked to process an LNT file not contained in the current directory, e.g.:
```
   traian DIR/FILE.lnt
```
it would search the libraries included by FILE.lnt (using the "library" clause) in the current directory rather than in directory DIR. See item 723 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.16 can be freely downloaded from the TRAIAN Web Page located at:

http://vasy.inria.fr/traian