TRAIAN 3.14 released on June 30, 2024

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

Release Notes

TRAIAN 3.14 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.13 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. Recently, TRAIAN 3.13 became part of CADP 2024-d, TRAIAN 3.14 beta-4 became part of CADP 2024-e, and TRAIAN 3.14 beta-9 became part of CADP 2024-f.

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

Language Changes

The semantics of exceptions was generalized. Formerly, exceptions were events declared with the predefined channel EXIT, which had a special meaning.
The grammar of LNT has been extended to enable channels to be declared with a "raise" attribute. For instance, the EXIT channel is now defined as follows in "lotosnt_predefined.lnt":
```
   channel EXIT is
      raise ()
   end channel
```
This attribute indicates that EXIT is a channel dedicated to exceptions. It is possible to declare several such channels, so that the criterion is no longer whether the name of the channel is "EXIT", but whether it has the "raise" attribute. In practice, this change should be invisible to most users.
The TRAIAN reference manual has been updated and a few error messages have been modified accordingly. For instance:
```
   event E declared with channel C instead of EXIT
   event E has channel C instead of EXIT
   event E should not have channel EXIT
```
become:
```
   event E declared with non-"raise" channel C
   event E has non-"raise" channel C
   event E should not have "raise" channel EXIT
```
See item 627 in the HISTORY.txt file.

TRAIAN was further aligned on LNT2LOTOS by suppressing the tolerance for deprecated "case ... in var in ... end case" constructs. Formerly, TRAIAN emitted the following warning for such constructs:
```
   "case ... in var" is deprecated and should be replaced by "case ... var" (3 occurrences found) 
```
From now on, such constructs are rejected syntactically, as they have been deprecated since March 2021. LNT programs with such constructs can be updated automatically by invoking "traian_upc" with key 2021-LOTNT-CASE-VAR. See item 638 in the HISTORY.txt file.

The grammar of TRAIAN was modified to resolve a syntactic ambiguity on expressions having the form "X [Y]", where X and Y are two identifiers. Formerly, such expressions could be interpreted in three different ways:
1. X is a variable of array type and Y is an index variable;
2. X is a nullary function and Y is an event;
3. X is a nullary function returning an array and Y is an index variable.
From now on, the 3rd option is excluded. To obtain this option, one should now write either X () [Y] or (X) [Y], which is safer and more readable.
Furthermore, TRAIAN now solves the syntactic ambiguity between the 1st and 2nd options by using semantic information gained during the identifier binding phases.
For instance, the following program, which was formerly rejected, is now accepted by TRAIAN:
```
   function F [E : exit] : bool is
      raise E
   end function

   process MAIN [G: any, E : exit] is
      G (F [E]) -- no more error: variable or function E is
                -- not defined
   end process
```
The error messages have also been enhanced. If X is not a variable and Y is not an event, but a variable, then TRAIAN emits the following error message:
```
   array X is not declared
```
rather than:
```
   event Y is not declared
```
See item 651 in the HISTORY.txt file.

The grammar of TRAIAN was modified to further align it on that of LNT2LOTOS. From now on, the presence of ellipses in field updates is forbidden, as such ellipses were useless (i.e., their presence has the same effect as their absence). One should therefore replace:
```
   V.{...} with either V.{} or V
```
and:
```
   V.{X1 -> V1, X2 -> V2, ...} with V.{X1 -> V1, X2 -> V2}
```
Consequently, the former warning of TRAIAN:
```
   superfluous "..." after all fields have been listed
```
has been removed. See item 657 in the HISTORY.txt file.

Static-Semantics Changes

TRAIAN was made stricter with respect to channel verifications that contain several profiles with the same types, e.g.:
```
   channel C is
      (X1: Nat, X2: Int),
      (Y1: Int, Y2: Nat),
      (Z2: Nat, Z1: Int)
   end channel
```
From now on, TRAIAN detects such channel definitions and rejects them with the following error message:
```
  channel profile with identical types already declared at PROG.lnt:12
```
See item 625 in the HISTORY.txt file.

The checks done by the static-semantics analysis of TRAIAN have been enhanced. In presence of clauses such as:
```
   if false then ...
   ... elsif false then ...
   while false loop ...
   for ... while false by ... loop ...
```
TRAIAN emits a new warning:
```
   condition always false
```
Similarly, in presence of clauses such as:
```
   if true then ...
   ... elsif true then ...
   while true loop ...
   for ... while true by null loop ...
```
TRAIAN emits a new warning:
```
   condition always true
```
Note that loops such as "for X := 0 while true by X := X + 1" are meaningful, so that the warning is only emitted if both "while true" and "by null" are present.
Also, new warnings are emitted if dead code follows such clauses. See item 630 in the HISTORY.txt file.

The number of warnings displayed by TRAIAN for the modified priorities of infix operators have been reduced. These warnings are no longer displayed during the expansion phase of TRAIAN but, more logically, in the expression checking phase, which takes place later than the expansion phase. Consequently, these warnings will no longer appear if a fatal error (e.g., undeclared variable) is detected by the earlier phases. See item 631 in the HISTORY.txt file.

The warnings emitted by TRAIAN concerning the modified priorities of infix operators have been further modified, in order to align the messages of TRAIAN on those emitted by LNT2LOTOS.
As a consequence of the tighter integration of LNT2LOTOS and TRAIAN, the new messages no longer refer to the changes implemented in TRAIAN 3.3 but to those implemented in LNT2LOTOS (January 2021). The following modifications have been brought:
1. Messages such as:
```
   WARNING: "*" takes priority over "+" since Traian 3.3
```
  have been changed to:
```
   WARNING: "*" takes priority over "+" since February 2021
```
  since the users of CADP are not expected to know about earlier versions of TRAIAN.
2. Messages such as:
```
   see item #259 of $LNTDIR/HISTORY.txt for more information on the above warning(s)
```
  have been changed to:
```
   pragma !update "2021-b" can be used to silence this warning
```
  since the users of CADP are not expected to read the HISTORY.txt file of TRAIAN.
3. In certain cases, TRAIAN now emits fewer warnings. For instance, on the following expression X == Y and not (Z), the following warning was suppressed:
```
   "and" no longer takes priority over "==" since ...
```
  Similar warnings have also been suppressed, e.g.:
```
   "and" no longer takes priority over "or" since ...
   "and" no longer takes priority over "<" since ...
   "=" no longer takes priority over "+" since ...
   "or" no longer takes priority over "==" since ...
```
4. In other cases, TRAIAN now emits more warnings as before, e.g.:
```
   "+" takes priority over "<" since ...
   "-" takes priority over "==" since ...
   "*" takes priority over "+" since ...
   "OR" takes priority over "==" since ...
   "xOr" takes priority over "=>" since ...
   etc.
```
See item 632 in the HISTORY.txt file.

The static semantics of TRAIAN was modified to further reduce the number of warnings emitted by TRAIAN concerning the modified priorities of infix operators. From now on, the information obtained from type checking and overloaded function binding is used to reduce ambiguities. Given an expression:
```
	V1 op V2 op' V3
```
a warning is only emitted when both expressions:
```
	(V1 op V2) op' V3
```
and:
```
	V1 op (V2 op' V3)
```
are correctly typed. If not, TRAIAN assumes that there is no ambiguity on the intentions of the programmer, so that no warning is needed. For instance, the following warnings are no longer displayed:
```
   "+" takes priority over "<" since ...
   "-" takes priority over "==" since ...
   "==" takes priority over "and" since ...
   "<" takes priority over "or" since ...
```
However, certain warnings cannot be removed using type information, e.g.:
```
   "*" takes priority over "+" since ...
```
See item 634 in the HISTORY.txt file.

The following error message of TRAIAN:

   pragma !... already present

in order to make it more explicit (as was done by LNT2LOTOS):

   pragma !... already present for this function
   pragma !... already present for this type
   pragma !... already present for this process

See item 635 in the HISTORY.txt file.

Several error messages of TRAIAN have been enhanced, taking inspiration from LNT2LOTOS, the former error messages of which were sometimes more precise. Namely:

   variable X is already declared at ...

becomes, in processes and functions:

   parameter X is already declared at ...

   variable X is already declared at ...

becomes, in channel definitions:

   channel parameter E is already declared at ...

   ".in" improperly used with "out" parameter X

becomes:

   invalid ".in" qualifier for "out" parameter X

   "result" improperly used outside function returning a result

becomes:

   "result" only allowed in functions that return a result

   multiple fields X with different types in definition of channel C

becomes:

   field X declared with a different type at ...

   constructor function C is already declared at ...

becomes:

   constructor function C is already declared with the same profile at ...

Also, in many error messages, the adjectives "illegal" and "not defined" have been changed to "invalid" and "not declared", respectively. See item 636 in the HISTORY.txt file.

Warnings have been added for "where false" and "where true" guards present in nondeterministic assignments and "case" patterns:
```
   condition always true
```
and
```
   condition always false
```
or
```
   condition always false (behaviour equivalent to "stop")
```
The data flow analysis has been enhanced to consider that nondeterministic assignments with a "where false" condition are equivalent to "stop". Consequently, such assignments trigger new warnings:
```
   unreachable behaviour (dead code) after "stop"
```
Another consequence is that TRAIAN may accept programs that were formerly rejected, because it now ignores more dead code fragments. See item 637 in the HISTORY.txt file.

The data flow analysis of TRAIAN was enhanced to take into account the presence of conditionals "if false" and "elsif false" (which already trigger a warning "condition always false"). The new analysis is more precise. Certain programs that were rejected are now accepted, e.g., the following one:

   function F() : bool is
      if false then
         null
      else
         return true
      end if
      -- no more error: function F may terminate without
      -- returning a value
   end function

Conversely, certain programs that were accepted are now rejected, as TRAIAN detects more infinite loops in functions and more dead code in processes:

   function F (in var X : Int) : Int is
      while true loop
         if X < 0 then
	    X := X - 1
         elsif false then
	    return X
         end if
      end loop
      -- new error: function looping infinitely
   end function

   function F() : bool is
      if false then
         null
      else
         return true
      end if;
      return false
      -- new warning: unreachable instruction (dead code)
      -- after "return"
   end function

See item 639 in the HISTORY.txt file.

TRAIAN was modified to check that "raise" channels are only declared with empty profiles, i.e, do not have any fields. For instance, given the following channel:
```
   channel C is
      raise (X : NAT)
   end channel
```
TRAIAN emits the following error message:
```
   limitation: non-empty profile for a "raise" channel
```
This is a temporary limitation that we expect, with time, to remove, thus allowing exceptions to have parameters. See item 640 in the HISTORY.txt file.

A new TRAIAN phase, named "event checking", was added, which performs additional checks that were present in LNT2LOTOS but not yet in TRAIAN. Hence, new error messages are now emitted:

 - event "E" occurs twice in "access"
 - event "E" occurs twice in synchronized events
 - predefined event "UNEXPECTED" may not occur in "access"
 - predefined event "i" may not occur in synchronized events
 - predefined event "UNEXPECTED" may not occur in synchronized events

See item 641 in the HISTORY.txt file.

The data-flow analysis of TRAIAN was enhanced by taking into account the presence of "where false" in patterns. From now on, TRAIAN ignores "case" branches whose condition is always false. This impacts the data flow analysis, but also checks related to the exhaustiveness of case patterns.
On the one hand, the new version of TRAIAN may now accept programs that were formerly rejected. For instance, a "case" statement that assigns a variable X in all its branches but one branch with a "where false" condition is now accepted, whereas it was rejected with an error message such as:
```
   variable X may be uninitialized
```
On the other hand, TRAIAN now emits new warnings and error messages about incomplete patterns in "case" instructions and, also, because it detects more infinite loops, e.g.:
```
   process P [PRINT: any] (X: Nat) is
      case X var Y: Nat in
         Y where false -> use Y
      |  any -> stop
      end case;
      PRINT (true)
      -- new warning: unreachable behaviour (dead code) after "stop"
   end process

   function F (X: Nat) : Bool is
      loop L in
         case X var Y: Nat in
	    Y where false -> use Y; break L
         |  any -> null
         end case
      end loop;
      -- new error: function looping infinitely
      return true
   end function
```
See item 642 in the HISTORY.txt file.

The static semantics of TRAIAN was enhanced to take into account the presence of "if true" and "elsif true" constructs. In such cases, TRAIAN now does a more precise calculation of continuations, which leads to better warning messages (especially those about dead code). See item 643 in the HISTORY.txt file.

A new TRAIAN phase, named "process checking", was added, which issues warnings for "alt" and "par" constructs that have only one operand:
```
   warning: superfluous "alt" with only one branch
   warning: superfluous "par" with only one branch
```
See item 644 in the HISTORY.txt file.

The checks done by TRAIAN on event parameters in function and process calls with named parameters have been strengthened. Formerly, TRAIAN did not implement all the checks done by LNT2LOTOS. For instance, certain calls such as:
```
   F [E -> E1, E -> E2] (...)
```
were either not detected or rejected with an obscure message:
```
   function F called with incorrect profile
```
From now, the following message is emitted:
```
   multiple occurrences of event parameter E before "->"
```
See item 647 in the HISTORY.txt file.

A new warning message was added to TRAIAN:
```
   warning: empty module
```
that is emitted when a module contains no definition of type, channel, function, or process. See item 648 in the HISTORY.txt file.

Many warning and error messages of TRAIAN have been enhanced to be as informative as those of LNT2LOTOS. For instance:

   invalid value 4 for pragma !nat_check

becomes:

   invalid value 4 for pragma !nat_check (0 or 1 expected)

   invalid value 0 for pragma !bits

becomes:

   invalid value 0 (less than 1) for pragma !bits

   invalid value 1 for pragma !card

becomes:

   invalid value 1 (less than 2) for pragma !card

   range lower bound with incorrect type

becomes:

   range lower bound -1 is not a constant of type NAT

   in pragma !..., C identifier X already defined

becomes:

   in pragma !..., C identifier "X" already employed at ...

See item 649 in the HISTORY.txt file.

Taking inspiration from LNT2LOTOS, the following error message of TRAIAN: function F may return without assigning "out" parameter X Formerly, this message was emitted only once for function F, and the line number given was that of the definition of F. From now on, this message is emitted as many times as there are "return" instructions not preceded by an assignment to X, and only for those faulty "return" instructions. See item 650 in the HISTORY.txt file.

The data-flow analyses of TRAIAN for functions and processes have been compared and aligned. As a consequence, TRAIAN now accepts programs that were formerly rejected.

TRAIAN no longer complains about uninitialized variables in functions, when these variables are used in dead code (e.g., in the condition of an "if", "case", "while", etc.)

TRAIAN does a finer analysis of "trap" clauses and no longer rejects the following programs:

   function F (X: bool, out var Y: bool) : bool is
      trap
         E2: exit -> Y := false
      |  E3: exit -> Y := true
      in
         if X then
	    raise E3
         else
	    raise E2
         end if
      end trap;
      return Y
      -- no more error: function F may return without assigning parameter Y
   end function

   process P [G: any] (X: bool, out Y: bool) is
      trap
         E1: exit -> Y := true
      |  E2: exit -> Y := false
      |  E3: exit -> G (false)
      in
         if X then
	    raise E1
         else
	    raise E2
         end if
      end trap
      -- no more error: process P may return without assigning parameter Y
   end process

See item 652 in the HISTORY.txt file.

The error messages emitted by TRAIAN for non-linear patterns have been enhaced. For instance, given the communication event:

   G (?X, 12 of Int, ?X)

TRAIAN no longer displays:

   multiple occurrences of variable X in pattern

but displays:

   variable X modified in both 1st and 3rd receive offers

which is more informative.

Also, given the following "case" instruction:

   case A, B, C in
      X, C1 (Y), C2 (X) -> ...
      ...
   end case

TRAIAN no longer displays:

   multiple occurrences of variable X in pattern

but displays:

   variable X modified both in 1st and 3rd patterns

See item 653 in the HISTORY.txt file.

The static analysis checks done by TRAIAN on "with get" and "with set" clauses have been strengthened. Formerly, TRAIAN did not implement all the checks done by LNT2LOTOS on such clauses. For instance, TRAIAN did not check that the !implementedby pragmas attached to such clauses declared valid C or LOTOS identifiers, nor that these identifiers were pairwise distinct. From now on, the pragmas attached to "with get" and "with set" clauses are checked as strictly as all other pragmas. See item 654 in the HISTORY.txt file.

The data flow analysis of TRAIAN was enhanced to produce error messages having the same precision as those of LNT2LOTOS. From now on, TRAIAN makes a distinction between those variables that are certainly not initialized and those that are potentially not initialized. Both are incorrect, but TRAIAN now emits different error messages, i.e.:
```
   variable X is uninitialized
```
and:
```
   variable X may be uninitialized
```
See item 655 in the HISTORY.txt file.

A new warning was introduced in TRAIAN:
```
   superfluous "..." after all offers have been listed
```
that is emitted when an event is used with an ellipsis although all fields of the channel profile for this event are already covered by explicit input or output offers. See item 658 in the HISTORY.txt file.

Code-Generation Changes

The C code generated by TRAIAN has been enhanced by moving the inclusion of the ".fnt" file, if any, after (rather than before) the "/* forward */" declarations of functions defined in LNT. This enables one to invoke these functions in the ".fnt" file (assuming that these functions are declared with an !implementedby pragma). See item 626 in the HISTORY.txt file.

The C code generated by TRAIAN for the PRED functions of numeral types, and for the PRED and SUCC functions of enumerated types was enhanced. From now on, TRAIAN generates macro-definitions that are hygienic, i.e., have all their arguments properly enclosed between parentheses. Additionally, the C code generated for tuple types that have no updater functions has been enhanced by removing useless "dashed" comment lines. See item 629 in the HISTORY.txt file.

Release Changes

The style file "lnt-aux.el" for EMACS and XEMACS was updated to reflect the progressive unification between the LOTOS NT and LNT languages:
- Obsolete comments that differentiated LNT2LOTOS from TRAIAN have been removed.
- The "alt" keyword is now supported.
- The "for" loops are now indented in a better way.
- The new "trap" syntax is supported; "trap" constructs are now indented in the same manner as "case" constructs.
Also, the configuration and READ_ME files for various editors have been updated so that files with extensions ".fnt" and ".tnt" can be recognized as source C files. See item 628 in the HISTORY.txt file.

Bug Fixes

An error was fixed in the C code generated for cascade types that have at least one constructor with a non-alphabetic name (e.g., "+", "<", etc.). In such case, TRAIAN generated macro-definitions:
```
   #define TRAIAN_BOUND_>_172 1
   #define TRAIAN_BOUND_+_173 4
```
that prevented the generated C code to compile properly. From now on, TRAIAN generates correct C code, e.g.:
```
   #define TRAIAN_BOUND_FUNC_172 1
   #define TRAIAN_BOUND_FUNC_173 4
```
See item 633 in the HISTORY.txt file.

An issue was solved concerning LNT pragmas with empty identifiers, e.g.:

   !comparedby "C:"
   !implementedby "LOTOS:"

for which TRAIAN emitted misleading error messages:

   in pragma !compared, invalid C identifier (keyword or standard macro of the C language)
   in pragma !implementedby, invalid LOTOS identifier (keyword of the LOTOS language)

From now on, TRAIAN displays more informative messages:

   invalid string "" for pragma !comparedby (not a C identifier)
   invalid string "" for pragma !implementedby (not a LOTOS identifier)

See item 645 in the HISTORY.txt file.

Various problems were corrected in the parsing and analysis of certain pragmas.
1. From now on, the arguments of the following pragmas:
```
   !bits
   !card
   !int_bits
   !nat_bits
   !nat_inf
   !nat_sup
   !num_card
   !num_bits
```
  are parsed as unsigned integers rather than signed ones. Negative numbers and numbers preceded by a "+" sign are now syntactically rejected. The reference manual of TRAIAN has been updated accordingly to use NATURAL instead of INTEGER for the type of these arguments.
2. Consequently, the arguments of pragmas !nat_inf and !nat_sup are now stored as unsigned integers, which enables larger values such as 2^32 - 1 to be specified.
3. The former error message of TRAIAN:
```
   error: too large natural constant
```
  was not appropriate for signed integers, such as the arguments of the !int_inf and !int_sup pragmas. It has been split into two different messages:
```
   limitation: out-of-bound natural constant
   limitation: out-of-bound integer constant
```
  The use of "limitation" makes it clear that it is not an error in the source program, but rather a limitation of the compiler.
4. To parse pragma arguments, TRAIAN no longer uses the atoi() function, which silently truncated large numbers. For instance, the following pragma:
```
   !card 111111111111111111111111111111111111111111
```
  no longer triggers a message:
```
   illegal value -954437177 for pragma !card
```
  and terminates the execution of TRAIAN with the UNEXPECTED exception, but triggers a proper error message:
```
   out-of-bound natural constant 1111111111111111111111...
```
5. From now on, pragmas such as:
```
   !int_inf 1_0_0
   !int_sup 1_0_2
```
  are treated like:
```
   !int_inf 100
   !int_sup 102
```
  whereas they were formerly recognized as:
```
   !int_inf 1
   !int_sup 1
```
See item 646 in the HISTORY.txt file.

The following mistake was fixed in data flow analysis: TRAIAN did not detect the case where a variable, in a "for" loop or a "while" loop, was assigned only when leaving the loop using a "break" but not when leaving the loop upon normal termination (i.e., when the loop condition becomes false). Consequently, the following incorrect programs, which are now rejected by TRAIAN, were accepted:

   function F (in var X1: bool, X2: bool, out Y: bool) is
      if not (X1) then
         Y := false
      end if;
      while X1 loop L in
         if X2 then
	    Y := true;
	    break L
         end if;
         X1 := false
      end loop
      -- Y not initialized if X1 = true and X2 = false
   end function

   process P (in var X1: bool, X2: bool, out Y: bool) is
      for if not (X1) then Y := false end if
          while X1 
          by null
       loop L in
         if X2 then
	    Y := true;
	    break L
         end if;
         X1 := false
      end loop
      -- Y not initialized if X1 = true and X2 = false
   end process

See item 656 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.14 can be freely downloaded from the TRAIAN Web Page located at:

http://vasy.inria.fr/traian