TRAIAN 3.17 released on August 29, 2025

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

Release Notes

TRAIAN 3.17 has been prepared by Hubert Garavel, Frederic Lang, and Wendelin Serwe, with the help of Pierre Boullier and Abdelilah Mejdoubi. It was released eight months after version 3.16 of TRAIAN.

TRAIAN 3.17 brings five language changes, twelve static-semantics changes, six compiler changes, five code-generation changes, thirteen library changes, five release changes, and seven bug fixes (see below their description).

These changes have been progressively integrated in the successive versions of TRAIAN distributed as part of the CADP toolbox between January and August 2025.

Language Changes

The LNT language was enriched with a "!virtual" pragma for (non-constructor) functions, which is similar to the "!virtual" pragma for processes. TRAIAN was extended to accept and take into account this pragma. Doing so, many error and warning messages have been introduced or enhanced, e.g.:
- error: virtual function F is already declared at ...
- error: virtual function F has different parameter names at ...
- error: virtual function F has different parameter types at ...
- error: virtual declaration without actual function F
- error: forbidden constructor for virtual function F at ...
- warning: useless virtual declaration for actual function F present at ...
- warning: "in var" parameter X of virtual function F should be an "in" parameter
See item 744 in the HISTORY.txt file.

The LNT language was extended with a new kind of loop, which exists in two forms, the unbreakable one:
```
   for ... until ... by ... loop
      ...
   end loop
```
and the breakable one:
```
   for ... until ... by ... loop ... in
      ...
   end loop
```
These loops can be used both in functions and processes. They are useful to enumerate the domain of enumerated types and range types. For instance, given the following definition:
```
   type T is
      range 1 .. 99 of NAT
      with =, SUCC
   end type
```
one can easily enumerate all values of type T using a "for-until" loop:
```
   var N: T in
      for N := 1 of T until N = 99 of T by N := SUCC (N) loop
         ...
      end loop
   end var
```
whereas the following "for-while" loop:
```
   var N: T in
      for N := 1 of T while N <= 99 of T by N := SUCC (N) loop
         ...
      end loop
   end var
```
would raise an overflow when computing SUCC (N) for N = 99.
Consequently, "until" becomes a new reserved keyword of LNT. Users are thus advised to update their LNT programs. This can be done automatically by typing the following command:
```
   traian_upc 2025-LNT-UNTIL <directory>
```
which will recursively explore the contents of the specified <directory>, look for ".lnt" files, and automatically rename identifiers named "until".
The C code generator of TRAIAN, the LNT User's Manual, and the editor style files have been updated to handle these new "for-until" loops. See item 746 in the HISTORY.txt file (related to CADP HISTORY item #3126).

The LNT language was simplified by merging the two symbols ".." (used in the definition of range and array types) and "..." (used in lists and sets). From now on, the ".." symbol (inherited from Pascal and Ada) is replaced by "...". The ".." symbol is marked as deprecated and will be removed in the future. At the moment, TRAIAN still accepts it, but emits the following warning:
```
   ".." is deprecated and should be replaced by "..."
```
Users are thus advised to update their LNT programs. This can be done automatically by typing the following command:
```
   traian_upc 2025-LNT-DOT-DOT <directory>
```
which will recursively explore the contents of the specified <directory>, look for ".lnt" files, and automatically replace ".." with "...". See item 747 in the HISTORY.txt file (related to CADP HISTORY item #3133).

The LNT language was enriched with new instructions for incrementing and decrementing variables or array elements. The syntax of these instructions is the following:
```
   X += V
   X += [E1, ..., En] V
   X -= V
   X -=[E1, ..., En] V
   X [V0] += V
   X [V0] +=[E1, ..., En] V
   X [V0] -= V
   X [V0] -=[E1, ..., En] V
```
The instructions work for numeric types (NAT, INT, and REAL) but also for any type with binary functions named "+" or "-". These functions may raise exceptions (hence, the presence of event lists E1, ..., En).
Semantically, these instructions can be seen as shorthands. "X += V" means "X := X + V", "X += [E1, ..., En] V" means "X := X +[E1, ..., En] V", etc.
This change is backward compatible, except for existing LNT specifications containing functions named "+=" or "-=". In such case, the functions must be renamed, since "+=" and "-=" are now reserved keywords.
Contrary to the C language, other shorthands than "+=" and "-=" (e.g., "*=", "/=", or even "and=", "or=", "mod=", "rem=", etc.) have not been added to LNT, since they would be much less used than "+=" and "-=".
The C code generator of TRAIAN was extended to handle these new increment/decrement constructs in function definitions. See item 748 in the HISTORY.txt file (related to CADP HISTORY item #3135).

The syntax of LNT for "in out" parameters of functions and processes was simplified. So far, these parameters were noted "!?X". From now on, they are noted "X?" (notice the query character occurs after the identifier). Consequently, the "!" character is now reserved for LNT pragmas. The former syntax "!?X" is still accepted for some time, but is deprecated and triggers the following warning:
```
   "!?X" for in-out parameters is deprecated and should be replaced by "X?" (79 occurrences)
```
Users are thus advised to update their LNT programs. This can be done automatically by typing the following command:
```
   traian_upc 2025-LNT-EXCLAIM-QUERY <directory>
```
which will recursively explore the contents of the specified <directory>, look for ".lnt" files, and replace "!?X" by "X?" automatically. See item 753 in the HISTORY.txt file (related to CADP HISTORY item #3148).

Static-Semantics Changes

To enhance the readability of LNT programs, TRAIAN now checks that all module pragmas (possibly excepted the "!version" pragmas) appear at the beginning of the module, before any definition of type, channel, function, or process. If not, TRAIAN emits new warnings, such as:
```
   pragma "!int_bits" should be at the start of module
   pragma "!nat_bits" should be at the start of module
   etc.
```
Notice also that "!version" pragmas may appear everywhere, especially in files included using the "library" directive. See item 727 in the HISTORY.txt file (related to CADP HISTORY item #3093).

When invoked with options "-c" or "-lotos", which indicate that code is to be generated for a complete LNT program), TRAIAN now detects each definition of a virtual process, for which no corresponding actual process is available, and emits the following error message:
```
   virtual declaration without actual process P
```
See item 736 in the HISTORY.txt file (related to CADP HISTORY item #3103).

TRAIAN now detects each superfluous declaration of a virtual process P, i.e., the case where an actual process P is either defined in the current module or defined in a transitively included module. In such case, TRAIAN now emits the following warning message:
```
   useless virtual for actual process P declared at FILE:LINE
```
See item 739 in the HISTORY.txt file (related to CADP HISTORY item #3108).

Various warning and error messages emitted by TRAIAN have been enhanced:
1. When an imported module or library cannot be found, TRAIAN now displays a more detailed message, e.g.:
```
  error: module file "F.lnt" is readable neither in "." nor "/opt/TRAIAN/lib"
  error: library file "F.lnt" is readable neither in "." nor "/opt/TRAIAN/lib"
```
  whereas, formerly, it would only report that "F.lnt" was not readable.
2. When a "with" function is defined with pragmas "!external" or "!virtual", e.g.:
```
   type T is
      set of NAT
      with == !external !implementedby "EQ"
   end type
```
  TRAIAN now emits a specific error message:
```
   forbidden pragma !external for "with" function ==
```
  which is clearer than the formerly emitted message:
```
   non-empty, non-null definition for external function ==
```
3. TRAIAN now emits a warning when the deprecated keyword "select" is used:
```
   "select" is deprecated and should be replaced by "alt" (12 occurrences found)
```
  The replacement of "select" by "alt" can be performed automatically by calling the shell script "traian_upc" with its 2024-LOTNT-SELECT key.
See item 745 in the HISTORY.txt file (related to CADP HISTORY item #3124).

The data-flow analysis performed by TRAIAN on array types was made more precise. From now on, each assignment of the form "X [V0] := V" no longer counts as a use of the array variable X. This change causes new warnings, which are relevant, about useless, full assignments to array variables. For instance, the following LNT program triggers a new warning:
```
  type T is array [0 ... 1] of Nat end type
  function F () is
     var A : T in
        -- in this function, A is assigned twice but not used
        A := T (0, 0); -- new warning "useless assignment"
        A [0] := 1 -- old warning "useless assignment" remains
     end var
  end function
```
See item 751 in the HISTORY.txt file (related to CADP HISTORY item #3145).

TRAIAN was enhanced to warn about irrelevant "require" clauses, i.e., "require" clauses whose Boolean expression does not refer to any "in" parameter of the current process or function. In such case, TRAIAN now emits warnings such as:

   "require" clause for process P with no "in" parameter (should be an "assert")
   "require" clause irrelevant to the "in" parameter of process P (should be an "assert")
   "require" clause irrelevant to the "in" parameters of process P (should be an "assert")
   "require" clause for function F with no "in" parameter (should be an "assert")
   "require" clause irrelevant to the "in" parameter of function F (should be an "assert")
   "require" clause irrelevant to the "in" parameters of function F (should be an "assert")

The case where the Boolean expression is constant ("false" or "true") is already covered by a specific warning message. See item 755 in the HISTORY.txt file (related to CADP HISTORY item #3151).

TRAIAN was also enhanced to warn about irrelevant "ensure" clauses, i.e., "ensure" clauses whose Boolean condition does not refer to any "out" parameter, nor to the ".out" value of any "in out" parameter, nor to the "result" of the current function or process. In such case, TRAIAN now emits a warning, the form of which depends on the "out"/"in out" parameters and/or result of the current function or process, e.g.:

   "ensure" clause for process P with no "out" parameter (should be an "assert")
   "ensure" clause irrelevant to the "out" parameter of process P (should be an "assert")
   "ensure" clause irrelevant to the "out" parameters of process P (should be an "assert")
   "ensure" clause for function F with no "out" parameter and no result (should be an "assert")
   "ensure" clause irrelevant to the result of function F (should be an "assert")
   "ensure" clause irrelevant to the "out" parameter of function F (should be an "assert")
   "ensure" clause irrelevant to the "out" parameter and result of function F (should be an "assert")
   "ensure" clause irrelevant to the "out" parameters of function F (should be an "assert")
   "ensure" clause irrelevant to the "out" parameters and result of function F (should be an "assert")

The case where the Boolean expression is constant ("false" or "true") is already covered by a specific warning message. See item 757 in the HISTORY.txt file (related to CADP HISTORY item #3152).

The data-flow algorithms of TRAIAN have been enhanced in several respects:
1. The warnings emitted for "in" and "in var" parameters have been aligned across functions and processes.
2. In dead code, some fatal errors are replaced by non-fatal warnings. For instance:
```
   error: variable X is uninitialized
```
  may be changed to:
```
   warning: variable X may be uninitialized
```
  and:
```
   error: function F may return without assigning "out" parameter X
```
  may be changed to:
```
   warning: function F may return without assigning "out" parameter X
```
  Consequently, certain LNT programs formerly rejected by TRAIAN are now accepted (with warnings).
3. Due to a finer analysis of dead code, some warnings are no longer displayed, e.g.:
```
   variable X may be uninitialized
```
  or:
```
   "in var" parameter X modified before used (should be a local variable)
```
  since TRAIAN now excludes dead paths from its analysis of branching points ("alt", "case", and "if").
4. Conversely, new warnings may now be displayed for "return" instructions located in dead code, e.g.:
```
   variable X may be uninitialized
```
  or:
```
   function F may return without assigning "out" parameter X
```
The general policy is that dead code in LNT is not a lawless zone, in which the user could write blatantly incorrect code. On the one hand, dead code is already checked, so that syntax errors, undefined identifiers, and wrongly typed expressions are rejected. On the other hand, even if some data-flow errors in dead code are no longer considered to be fatal, warnings are still emitted to prevent abuses in dead-code zones. See item 762 in the HISTORY.txt file (related to CADP HISTORY item #3157).

TRAIAN was enhanced to better check the presence of redundant "access" directives in the instructions or behaviours located after the "in" keyword of "trap...end trap". In such situations, TRAIAN now emits more warnings of the form:
```
   event E is already accessed (superfluous "access")
```
See item 764 in the HISTORY.txt file (related to CADP HISTORY item #3164).

TRAIAN was enhance to produce more precise results when analyzing the exhaustiveness of "case" patterns. TRAIAN now specifically recognizes those patterns whose Boolean guard is always false (the patterns whose Boolean guard is always true were already taken into account) and, consequently, states more often that the patterns of a "case" are (certainly) "incomplete", rather than "possibly incomplete". See item 765 in the HISTORY.txt file (related to CADP HISTORY item #3166).

The data-flow analysis of TRAIAN was refined to recognize "for" loops and "while" loops, the Boolean guard of which is always false. The bodies of such loops are now marked as dead code, leading to more precise warning and error messages. In such situations, TRAIAN emits a new warning:
```
   loop body is never executed
```
See item 767 in the HISTORY.txt file (related to CADP HISTORY item #3169).

The data-flow analysis of TRAIAN was enhanced in order to display "condition always true" warning for every "for...until" loop whose condition is always true. See item 769 in the HISTORY.txt file (related to CADP HISTORY item #3178).

Compiler Changes

TRAIAN was modified as follows: formerly, when an LNT program had a single (non-virtual) process, TRAIAN considered it as the entry point, even if this process was not called "MAIN". This is no longer the case: to have a simpler semantics, this process must be called "MAIN", otherwise TRAIAN (unless given the "-analysis" option) emits the following error message:
```
   no main process found (define one or use "-main" option)
```
Consequently, TRAIAN has been equipped with a "-main" option. Syntactic and semantic checks have been added, which verify that the argument of this option is correct (binding, type checking, parameter checking, etc.). See item 729 in the HISTORY.txt file (related to CADP HISTORY item #3096).

The C code generator of TRAIAN was adapted to produce C code (i.e., an "int main()" function) for the LNT process designated by the "-main" option, if present. TRAIAN was also extended to accept a "-main null" option; in such case, TRAIAN does not complain if the LNT program contains several processes, none of which is called MAIN, and does not generate C code. See item 732 in the HISTORY.txt file.

Formerly, the C code generator of TRAIAN rejected (as a limitation) LNT programs that contained several processes. From now on, TRAIAN generates C code for such programs if one process is designated as principal using the "-main" option, or else if no "-main" option is given but there exists a process named "MAIN". Consequently, the following messages displayed by TRAIAN:
```
   limitation: processes not yet fully implemented
```
no longer refer to the first line of the second process defined in the LNT process, but to the first line on which a behaviour construct not yet supported by TRAIAN (e.g., "alt" operator, "par" operator, process call, etc.) occurs. See item 733 in the HISTORY.txt file.

Formerly, if there was only one process in an LNT program, it was automatically considered as the main process. This is no longer the case: the "-analysis" option of TRAIAN still accept this LNT program, but the "-c" and "-lotos" options of TRAIAN now reject it, unless the unique process is is called "MAIN" or is designated by the "-main" option.
Therefore, this change is not backward compatible, as the new version of TRAIAN is less permissive. In LNT programs that contain a single process, this process should be renamed to "MAIN" manually. See item 734 in the HISTORY.txt file.

TRAIAN was simplified as follows: from now on, the three options "-analysis", "-c", and "-lotos" are mutually exclusive. See item 735 in the HISTORY.txt file.

The release of SYNTAX used to build TRAIAN was upgraded from a 2023 to a 2025 version. Consequently, TRAIAN was upgraded to use the most recent programming interfaces of SYNTAX. This change should be transparent to most users; yet, error recovery performed by TRAIAN on syntactically incorrect LNT files may be slightly different with TRAIAN 3.17. See item 749 in the HISTORY.txt file (related to CADP HISTORY item #3142).

Code-Generation Changes

The C code generated by TRAIAN was simplified by removing useless C code from the main LNT process (this code was produced to handle the exceptions raised by some event parameters of the main process, even when these parameters could not raise exceptions). See item 731 in the HISTORY.txt file.

The C code generated by TRAIAN was also simplified by removing from this code all pathnames containing $CADP or $LNTDIR. See item 743 in the HISTORY.txt file.

In the C code generated by TRAIAN, extra pragmas were added to disable the -Wswitch-default option of GCC. Indeed, the C code produced by TRAIAN contains "switch" statements with "default" case, because they already cover all possible cases. See item 750 in the HISTORY.txt file.

The C code generated by TRAIAN for LNT functions having event parameters was modified, in order to align it with the conventions used by LNT2LOTOS. From now on, in any C function produced by TRAIAN, the C function parameters corresponding to LNT event parameters, if any, come first, whereas they would formerly come last, after the C parameters corresponding to LNT value parameters. Consequently, many function definitions contained in file "lnt_predefined.h", which implements all predefined functions of LNT, have been modified. Users may have to update manually their ".fnt" files that implement external functions, so as to permute function parameters. See item 761 in the HISTORY.txt file.

The C code generated by TRAIAN for the main() function implementing the principal process of an LNT program was further simplified. TRAIAN now generates less C code if this principal process does not contain any visible event having the channel EXIT. Incidentally, this removes a GCC warning. See item 768 in the HISTORY.txt file.

Library Changes

The DELETE() and REMOVE() functions for LNT lists, sorted lists, and sets were revised to make them more efficient in memory. These functions now invoke the MEMBER() function, actually named LNT_MEMBER(), to avoid allocating memory when this is not necessary. TRAIAN was modified to automatically import the LNT_MEMBER() function when this is necessary. See item 737 in the HISTORY.txt file (related to CADP HISTORY item #3105).

The INTER() and UNION() functions for LNT sets were also revised to make them more efficient in memory. These functions now invoke the SUBSET() function, actually named LNT_SUBSET(), to avoid allocating memory when this is not necessary. TRAIAN was modified to automatically import the LNT_SUBSET() function when this is necessary. See item 738 in the HISTORY.txt file (related to CADP HISTORY item #3107).

The LNT language was extended with eight predefined library functions. To complete the already existing functions:
```
   MIN : NAT, NAT -> NAT
   MAX : NAT, NAT -> NAT
   MIN : INT, INT -> INT
   MAX : INT, INT -> INT
```
the following new functions have been added:
```
   MIN : BOOL, BOOL -> BOOL
   MAX : BOOL, BOOL -> BOOL
   MIN : REAL, REAL -> REAL
   MAX : REAL, REAL -> REAL
   MIN : CHAR, CHAR -> CHAR
   MAX : CHAR, CHAR -> CHAR
   MIN : STRING, STRING -> STRING
   MAX : STRING, STRING -> STRING
```
This change is likely to break existing LNT programs that already define MIN or MAX functions with the same profiles. In such case, the user-defined functions should be removed if they are identical to the new library functions, or renamed if their semantics is different. See item 758 in the HISTORY.txt file (related to CADP HISTORY item #3153).

LNT was further enhanced by introducing predefined MIN and MAX functions for all types (constructor types, arrays, ranges, predicate types, lists, sorted lists, and sets). These functions can easily be obtained by specifying "with min" and/or "with max" clauses in type definitions. See item 759 in the HISTORY.txt file (related to CADP HISTORY item #3154).

The LNT language was enriched with predefined INF and SUP functions that compute, respectively, the least and greatest elements of a list, sorted list, or set. If the list or set is empty, an exception is raised. These functions are meant to bring LNT closer to the B language, which has predefined functions for computing minimum and maximum values in a set. See item 760 in the HISTORY.txt file (related to CADP HISTORY item #3155).

The LNT library of predefined functions was enriched with eight nullary functions:
```
   FIRST : -> BOOL
   LAST : -> BOOL
   FIRST : -> NAT
   LAST : -> NAT
   FIRST : -> INT
   LAST : -> INT
   FIRST : -> CHAR
   LAST : -> CHAR
```
In a few cases, this change is not backward compatible. For instance, if E is an event declared with channel "any" and if FIRST denotes a nullary function of some user-defined type T, then the following behaviour:
```
   E (FIRST)
```
is no longer accepted, since FIRST is now overloaded, and should be replaced with:
```
   E (FIRST of T)
```
See item 766 in the HISTORY.txt file (related to CADP HISTORY item #3168).

The range types of the LNT language have been extended as follows. For any LNT type of the form:
```
   type T1 is range ... of T2
```
a conversion function:
```
   T1 : T2 -> T1
```
was already generated automatically. From now on, another conversion function:
```
   T1 : [Exit] T2 -> T1
```
is generated, which takes an explicit event parameter that denotes the exception to be triggered if the conversion fails. See item 770 in the HISTORY.txt file (related to CADP HISTORY item #3181).

The predefined library of LNT was enriched with 10 overloaded versions of the string concatenation function "&". In addition to the already existing function:

   & : STRING, STRING -> STRING

the library now supports:

   & : BOOL, STRING -> STRING is
   & : NAT, STRING -> STRING is
   & : INT, STRING -> STRING is
   & : REAL, STRING -> STRING is
   & : CHAR, STRING -> STRING is

and:

   & : STRING, BOOL -> STRING is
   & : STRING, NAT -> STRING is
   & : STRING, INT -> STRING is
   & : STRING, REAL -> STRING is
   & : STRING, CHAR -> STRING is

These new functions make it easier to display output messages such as:

   PRINT ("the probability for " & N & " elements is " & P)

Formerly, one had to write String (N) and String (P) instead of N and P. See item 771 in the HISTORY.txt file (related to CADP HISTORY item #3182).

The LNT language was simplified by removing the predefined function VAL() on range types. From now on, it is no longer allowed to specify "with VAL" on a range type. Indeed, this function (inspired by the CHR() function of Pascal) was seldom used, as it could be easily obtained by other means:
- For a type T defined as "type T is range M...N of Nat" or "type T is range M...N of Int", the value VAL (X) was simply equal to T (X + M).
- For a type T defined as "type T is range M...N of Char", the value VAL (X) was equal to T (Char (X + Nat (M))).
See item 772 in the HISTORY.txt file (related to CADP HISTORY item #3185).

The predefined library of LNT with 4 new functions that may raise exceptions:

   + : [Exit] Nat, Nat -> Nat
   - : [Exit] Int -> Int
   + : [Exit] Int, Int -> Int
   - : [Exit] Int, Int -> Int

This change might not be backward compatible. For instance, the following process definition:

   process MAIN [UNDERFLOW : Exit, PRINT : any] is
      PRINT (1 -[UNDERFLOW] 2)
   end process

was formerly accepted, but is now rejected:

   in behaviour: PRINT (1 -[UNDERFLOW] 2)
   offer 1 -[UNDERFLOW] 2 may have several types NAT|INT,
   one of which should be chosen using an "of" coercion

Indeed, one must insert either "of Nat" or "of Int" after constants 1 and/or 2. See item 773 in the HISTORY.txt file (related to CADP HISTORY item #3187).

The predefined library of LNT was simplified by removing two functions:
```
   Real : [Exit] Nat -> Real
   Real : [Exit] Int -> Real
```
which were indeed useless, given that Reals are implemented using the "double" type of C, so that no exception may occur when converting Nats or Ints to Reals. See item 774 in the HISTORY.txt file (related to CADP HISTORY item #3190).

The implementation of the following arithmetic functions of the LNT predefined library was enhanced:
```
   + : Nat, Nat -> Nat
   + : [Exit] Nat, Nat -> Nat
   * : Nat, Nat -> Nat
   * : [Exit] Nat, Nat -> Nat
   ** : Nat, Nat -> Nat
   ** : [Exit] Nat, Nat -> Nat
   + : Int, Int -> Int
   + : [Exit] Int, Int -> Int
   - : Int -> Int
   - : [Exit] Int -> Int
   - : Int, Int -> Int
   - : [Exit] Int, Int -> Int
   * : Int, Int -> Int
   * : [Exit] Int, Int -> Int	
   ** : Int, Nat -> Int
   ** : [Exit] Int, Nat -> Int	
```
Formerly, these operations did not check for overflow or underflow (as usual with the C language) and, thus, never raised the corresponding events. At present, some partial overflow/underflow checks have been implemented.
A more precise implementation will be provided when as the "checked" arithmetic operations of the recent C23 standard will be available on all platforms and compilers. See item 775 in the HISTORY.txt file.

The set of predefined functions that can invoked on LNT range types using a "with" clause was enriched. This required many changes in TRAIAN:
1. A scheme file may now include another scheme file (and so on, transitively) using the "library" directive of LNT.
2. A scheme file may now have several clauses "with !version" due to "library" inclusions.
3. A scheme file may now define functions named LNT_T1, etc. and invoke these functions in other functions.
4. The scheme file "scheme_range.lnt" was complemented with three auxiliary scheme files named "scheme_range_char.lnt", "scheme_range_int.lnt", and "scheme_range_nat.lnt", each of which defines functions specific to ranges of Chars, Nats, and Ints, respectively.
For any type T defined as "range ... of Char", the following predefined functions are now available:
```
   + : T, Nat -> T
   + : [Exit] T, Nat -> T
   - : T, Nat -> T
   - : [Exit] T, Nat -> T
```
For any type T defined as "range ... of Nat", the following predefined functions are now available:
```
   + : T, T -> T
   + : [Exit] T, T -> T
   - : T, T -> T
   - : [Exit] T, T -> T
```
For any type T defined as "range ... of Int", the following predefined functions are now available:
```
   + : T -> T
   + : T, T -> T
   + : [Exit] T, T -> T
   - : T -> T
   - : [Exit] T -> T
   - : T, T -> T
   - : [Exit] T, T -> T
```
See item 776 in the HISTORY.txt file (related to CADP HISTORY item #3192).

Release Changes

The style files for the Sublime Text editor have been enhanced. From now on, the predefined types of LNT are recognized and displayed with a specific color. See item 724 in the HISTORY.txt file (related to CADP HISTORY item #3084).

Style files for the support of LNT in Visual Studio Code have been added. See item 725 in the HISTORY.txt file (related to CADP HISTORY item #3086).

The explanations to install the LNT style files for Sublime Text have been enhanced. See item 726 in the HISTORY.txt file (related to CADP HISTORY item #3092).

A new shell script "src/com/cadp_temporary" used by the -main option of TRAIAN was added to the TRAIAN release. See item 730 in the HISTORY.txt file.

To complete the unification of the LOTOS NT and LNT languages, all files whose named contained "lotosnt" have been renamed as follows:
- bin.*/lotosnt_exceptions.o -> bin.*/lnt_exceptions.o
- incl/lotosnt_exceptions.h -> incl/lnt_exceptions.h
- incl/lotosnt_hash.h -> incl/lnt_hash.h
- incl/lotosnt_predefined.h -> incl/lnt_predefined.h
- lib/lotosnt_predefined.lnt -> lib/lnt_predefined.lnt
- src/lotosnt_exceptions.c -> src/lnt_exceptions.c
See item 742 in the HISTORY.txt file (related to CADP HISTORY item #3119).

Bug Fixes

The scanner of TRAIAN was modified to accept all the "special identifiers" of LNT, i.e., identifiers starting with a digit and followed by letters, digits, and/or underscores. Formerly, TRAIAN accepted most of these identifiers, but rejected those starting with a natural number or a real number without a dot, followed immediately by the lower-case letter "i", "l", or "w". For instance, the following identifiers were rejected: 1long, 123i4, 1e1w, etc. These issues have been fixed. See item #728 in the HISTORY.txt file (related to CADP HISTORY item #3094).

TRAIAN was modified to solve the following issue: when an LNT process was called with parameters of incorrect types and had an ellipsis ("...") in the list of its event parameters, the error message emitted by TRAIAN omitted the ellipsis, e.g., mentioned:
```
    P [Z -> C, X -> A, Y -> B] (0, 1)
```
instead of:
```
   P [Z -> C, X -> A, Y -> B, ...] (0, 1)
```
See item #740 in the HISTORY.txt file (related to CADP HISTORY item #3109).

TRAIAN was revised to strengthen its checks on the !implementedby "LOTOS:..." pragmas for LNT processes. Formerly, TRAIAN did for the processes the same checks as for functions, and thus accepted identifiers such as 12, 1A2, ++, <<, etc. that were valid function identifiers, but invalid process identifiers. From now on, TRAIAN applies stricter checks on !implementedby "LOTOS:..." pragmas for LNT processes than on those for LNT functions. See item #741 in the HISTORY.txt file (related to CADP HISTORY item #3111).

TRAIAN could abort with a segmentation fault if the file names included using the "module" clause were too long. This problem could also occur with file names given on the command line, but not with files included using the "library" directive. This issue was solved. TRAIAN now checks the size of all included file names and emits a proper error message if these names are too long:
```
   limitation: too long ".lnt" file name in list of included
   modules (maximum length is 1023)
```
See item #752 in the HISTORY.txt file (related to CADP HISTORY item #3147).

The behaviour of TRAIAN when parsing syntactically incorrect "library" clauses was enhanced. Formerly, given an incorrect directive:
```
   library FILE end library
```
instead of the correct directive:
```
   library "FILE" end library
```
the error recovery mechanism of SYNTAX would replace the 'F' of 'FILE' with '"', triggering the following error message:
```
   library FILE end library
           ^
        warning: the invalid character "F" is replaced by "\""
```
Then, TRAIAN would try to open a file named 'ILE', which did not exist. To avoid this situation, which proved to be confusing for end users, the error recovery mechanism is now disabled when parsing "library" directives. See item #754 in the HISTORY.txt file (related to CADP HISTORY item #3150).

A missing implementation for the ABS() function on REAL numbers was added. This function was declared in file "lnt_predefined.lnt" but not implemented in "lnt_predefined.h". See item #756 in the HISTORY.txt file.

The following issue was fixed: when invoked on an LNT program that defines a function or a process with an "in var" or "out var" parameter X and invokes this function or process with an ellipsis "..." encompassing this parameter X, TRAIAN halted abruptly by raising the UNEXPECTED event. See item #763 in the HISTORY.txt file (related to CADP HISTORY item #3161).

Future Work

For many years, TRAIAN has been used to develop compilers, including those of the CADP toolbox.

Since October 2023, it also serves to analyze formal specifications of concurrent systems, as part of the CADP toolbox.

We are working to further deepen the co-operation between TRAIAN and the LNT2LOTOS translator of CADP.

Download

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

http://vasy.inria.fr/traian