TRAIAN 3.12 released on December 29, 2023

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

Release Notes

TRAIAN 3.12 has been prepared by Hubert Garavel, Frederic Lang, and Wendelin Serwe. It was released three months after version 3.11 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.

With TRAIAN 3.12, the convergence between LOTOS NT and LNT with respect to incorrect LNT programs has progressed, meaning that TRAIAN became stricter in order to be aligned on LNT2LOTOS, and that the error and warning messages emitted by TRAIAN have been enhanced. Also, the C code generated by TRAIAN has improved in many respects.

TRAIAN 3.12 brings eight static-semantics changes, seven compiler changes, sixteen code-generation changes, seven library changes, one release change, and twelve bug fixes (see below their description).

Static-Semantics Changes

To further align TRAIAN with LNT2LOTOS, some static-semantics checks performed by LNT2LOTOS on synchronized events have been added to TRAIAN. From now on, if an event is stated to be synchronized by a parallel composition operator, but is not used in some branches of the parallel composition, TRAIAN emits warnings such as:
```
   synchronized event E1 not accessed in 1st "par" branch
   synchronized event E2 not accessed in 4th "par" branch
```
Same as done by LNT2LOTOS to avoid redundant warnings, this warning may supersede more general warnings such as:
```
   hidden event E1 never accessed
   event parameter E2 never accessed
```
that would be also applicable, though less informative. See item 571 in the HISTORY.txt file.

Other static-semantic checks done by LNT2LOTOS for the parallel composition have been introduced in TRAIAN. For instance, TRAIAN now emits warnings such as:
```
   event E synchronized in only one "par" branch"
```
See item 573 in the HISTORY.txt file.

The warnings issued by TRAIAN for "case" instructions have been improved in three ways:
- a) The warnings about patterns in excess, e.g.,
```
   superfluous pattern(s) after the 7th pattern
```
  were computed during TRAIAN's code-generation phase, and thus not displayed when TRAIAN was invoked (namely, from CADP by the LNT.OPEN shell script) with its "-analysis" option. This issue was addressed by performing the checks earlier, during TRAIAN's pattern-checking phase, so that the warnings are now displayed by the "-analysis" option.
- b) The detection of superfluous patterns was made more precise by examining particular cases ("X as any", "P where true", etc.) more finely. As a consequence, TRAIAN 3.12 emits more warnings about superfluous patterns than TRAIAN 3.11.
- c) From now on, if a pattern is not linear (i.e., contains several occurrences of the same free variable), TRAIAN still displays the following error:
```
   multiple occurrences of variable X in pattern
```
  but no longer attempts to check pattern exhaustiveness. Consequently, the following warning:
```
   incomplete patterns in "case" instruction
```
  is no longer emitted in presence of non-linear patterns, as it was usually misleading.
See item 577 in the HISTORY.txt file.

Taking inspiration from LNT2LOTOS, the number of warnings emitted by TRAIAN for infix operators was reduced such as "AND", "And", "OR", "Or", "Div", etc., which look like predefined operators ("and", "or", "div", etc.) but do not obey the same syntactic precedence rules as their identifiers contain upper-case letters. From now on, TRAIAN emits warnings such as:
```
   infix operator "Xor" has a different priority than built-in "xor"
```
and:
```
   missing parentheses to disambiguate priority between "AND" and "OR"
```
only when these operators are used in expressions where operator precedence really matters. For instance, no warning will be emitted for a sub-expression such as "p OR q OR r". See item 581 in the HISTORY.txt file.

The static semantics of TRAIAN was modified to make it as strict as LNT2LOTOS: from now on, any expression of the following form:
```
   V.X
```
or
```
   V .[E] X
```
is rejected if the type of the expression is declared without a "with get" clause. In such case, TRAIAN now emits the following error message:
```
   type T lacks "with get" to enable field accesses
```
This change is not backward compatible, as it may be required to introduce "with get" clauses in existing LOTOS NT programs to have them accepted by TRAIAN 3.12.
For instance, the two files "demos/demo_03/scsi.lnt" and "demos/demo_04/simproc.lnt" have been modified to insert "with get" clauses where needed. See item 584 in the HISTORY.txt file.

The static semantics of TRAIAN was modified to make it as strict as LNT2LOTOS: from now on, any expression of the form:
```
   V.{X1->V1, ..., Xn->Vn}
```
or:
```
   V .[E] {X1->V1, ..., Xn->Vn}
```
is rejected if the type of the expression is declared without a "with set" clause. In such case, TRAIAN now emits the following error message:
```
   type T lacks "with set" to enable field updates
```
This change is not backward compatible, as it may be required to introduce "with set" clauses in existing LOTOS NT programs to have them accepted by TRAIAN 3.12. See item 585 in the HISTORY.txt file.

The effect of "with" clauses was clarified for the FIRST, LAST, PRED, and SUCC functions over types defined by their list of constructors. Formerly, TRAIAN 3.11 accepted such "with" clauses but generated no C code at all for FIRST and LAST, and generated only "forward" declarations for the PRED and SUCC functions.
From now on, TRAIAN 3.12 only accepts such "with" clauses, and generates the corresponding C code for the "range" types and, among types defined by their list of constructors, for enumerations and cascade types. For other types, such "with" clauses are now rejected.
A side effect of this change is that certain verifications concerning pragmas, which were previously done during C code generation, e.g.:
```
    error: forbidden pragma !pointer for enumeration type T
```
are now done much earlier (in the function-binding phase of TRAIAN) and are thus performed when TRAIAN is invoked from CADP with its "-analysis" option. See item 595 in the HISTORY.txt file.

The static semantics of TRAIAN has been strengthened: if a type T2 defined by the list of its constructors has a clause "with STRING", then each type T1 used by (at least one) parameter of some constructor of T2 must also have a STRING : T1 → STRING function. This function may be defined either explicitly or implicitly (using another "with STRING" clause). If not, TRAIAN will now report the following error:
```
   type T1 lacks function "string" needed by "string" for type T2
```
See item 596 in the HISTORY.txt file.

Compiler Changes

The error messages emitted by TRAIAN 3.10 for sets and sorted lists have been enhanced. The former messages:

   clause "with INSERT" in type T2 requires function "==" for type T1
   clause "with INSERT" in type T4 requires function "<" for type T3

have been replaced with:

   type T1 lacks function "==" needed by set type T1
   type T3 lacks function "<" needed by sorted list type T4

See item 556 in the HISTORY.txt file.

The messages emitted by TRAIAN have been aligned with those of LNT2LOTOS: when TRAIAN is invoked on a ".lnt" file, the name of which starts with "./" (as it is the case when TRAIAN is invoked by LNT.OPEN in CADP), the name of the file is now displayed without the "./" prefix. For instance:
```
   ./test.lnt:4: limitation: processes not yet fully implemented
```
now displays as:
```
   test.lnt:4: limitation: processes not yet fully implemented
```
See item 570 in the HISTORY.txt file.

To further align TRAIAN with LNT2LOTOS, the warning:
```
   variable parameter X never used
```
emitted by TRAIAN was enhanced. From now on, this warning displays under three, more precise, forms, namely:
```
   "in" parameter X never used
   "in var" parameter X never used
   "in out" parameter X never used
```
See item 572 in the HISTORY.txt file.

A few warnings emitted by TRAIAN have been enhanced as follows:

The warning:

   variable parameter X never used

was replaced by:

   "in" parameter X never used

The warning:

   dead code after "stop" behaviour

was replaced by:

   unreachable behaviour (dead code) after "stop"

Also, the word "overwritten" was replaced by "modified" in a few warnings such as:

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

or:

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

See item 579 in the HISTORY.txt file.

The error messages emitted by TRAIAN to explain why a call to some (possibly overloaded) function F does not correspond to any function F declared in the LOTOS NT program have been enhanced. The enhancements are threefold:
- When listing function profiles, TRAIAN no longer displays "in var", as the difference between "in" and "in var" modes plays no role in resolution of function overloading.
- Similarly, TRAIAN now displays "out" instead of "out var", as the difference between "out" and "out var" modes plays no role.
- When a function is a procedure, i.e., does not return a result, TRAIAN now displays this information explicitly (as "no-result") to make it clear for the user.
See item 580 in the HISTORY.txt file.

Taking inspiration from LNT2LOTOS, the former warning of TRAIAN 3.11:
```
   "in out" parameter X never used
```
has been replaced by a more informative warning:
```
   "in out" parameter X never used nor assigned
```
See item 583 in the HISTORY.txt file.

Still taking inspiration from LNT2LOTOS, the warning emitted by TRAIAN when some "in" parameter is modified before used has been enhanced. In such case, TRAIAN previously emitted the following warning:
```
   "in" parameter X modified (should be an "in var" parameter)
```
which is now replaced by a more precise warning:
```
   "in" parameter X modified before used (should be a local variable)
```
The former warning is now used only if X is used and then modified. See item 594 in the HISTORY.txt file.

Code-Generation Changes

The C code generated by TRAIAN for the LNT_REVAPPEND function was simplified. See item 549 in the HISTORY.txt file.

In the C code generated by TRAIAN for tuple and ordinary types, old-style function prototypes have been replaced by new-style ones for the following functions:
```
   TRAIAN_EQ_<type>
   TRAIAN_NE_<type>
   TRAIAN_LT_<type>
   TRAIAN_LE_<type>
   TRAIAN_GT_<type>
   TRAIAN_GE_<type>
   TRAIAN_GET_<type>_<field> (for ordinary types only).
```
See item 552 in the HISTORY.txt file.

The C code generated by TRAIAN was shortened by removing several useless #if directives of the following form:

   #ifndef TRAIAN_POINTER_<type>
   ...
   #endif

and:

   #if !defined (TRAIAN_POINTER_<type>) && !defined
       (TRAIAN_HASH_<type>)
   #define TRAIAN_STAR_<type>(TRAIAN_0) (TRAIAN_0)
   #else
   ...
   #endif

See item 553 in the HISTORY.txt file.

The C code generated by TRAIAN for compiling pattern-matching was modified as follows: to compare a value V of type T against a nullary constructor C of T, TRAIAN no longer invokes the equality function of T:
```
   if (TRAIAN_EQ_T (V, C ())) ...
```
but invokes the matching function:
```
   if (TRAIAN_MATCH_C (V)) {
```
This change, which was required in order to enable equality functions "==" to be defined by LOTOS NT code in scheme files without causing an infinite recursion, should be invisible to TRAIAN users, except the fact that the generated C code is now faster. See item 554 in the HISTORY.txt file.

The rules for generating the name of the C function that implements the "==" function of some type T have been modified: from now on, TRAIAN uses the C identifier provided by the "!implementedby" pragma attached to this function or, if there is no such pragma, generates a C function name of the form TRAIAN_EQ_T. Formerly, TRAIAN used instead the C identifier provided by the "!comparedby" pragma, which was awkward and incompatible with the behaviour of other compilers in the CADP toolbox.
This change is not backward compatible, and may require a few manual patches in the ".fnt" or ".tnt" files to define the C functions implementing external "==" functions. See item 561 in the HISTORY.txt file.

The C code produced by TRAIAN was further modified, by generating a comparison function (or macro-definition) for each LOTOS NT type, distinct from the implementation of the "==" function, if any.
This comparison function is now invoked, instead of the equality function, in the C code generated by TRAIAN, e.g., in the lookup functions used to search for values stored in hash tables.
The library file "incl/lotosnt_predefined.h" has been extended with comparison macro-definitions for the predefined types: ADT_CMP_BOOL, ADT_CMP_NAT, ADT_CMP_INT, ADT_CMP_REAL, ADT_CMP_CHAR, and ADT_CMP_STRING. See item 562 in the HISTORY.txt file.

The readability of the generated C code was enhanced in various ways:
- removal of superfluous newlines (especially after commas),
- removal of dash lines in excess,
- removal of spaces before closing parentheses,
- insertion of missing white spaces before "!=", etc.
See item 563 in the HISTORY.txt file.

In order to align TRAIAN with LNT2LOTOS, the code generation of TRAIAN was modified as follows: for any LOTOS NT type T, TRAIAN no longer generates two C functions to implement operations "==" and "!=" for T unless:
- these functions are explicitly defined in the LOTOS NT source file, or
- these functions are implicitly defined using a "with" clause in the definition of type T.
This change is not backward compatible: existing LOTOS NT programs may need to be updated by adding "with ==" and/or "with !=" clauses where necessary. Also, a few ".tnt" files may have to be updated manually. See item 564 in the HISTORY.txt file.

The implementation of the "=" and "<>" functions was modified: for these functions, TRAIAN now generates C functions named TRAIAN_ID_* and TRAIAN_DF_*. See item 565 in the HISTORY.txt file.

The C code generated by TRAIAN to implement the comparison functions "==", "=", "!=", "<>", "<", "<=", ">", and ">=" was simplified:
- all useless casts "(ADT_BOOL)" have been removed;
- all conditions "(C ? ADT_TRUE () : ADT_FALSE ())" have been replaced by "(C)".
In file "incl/lotosnt_predefined.h", the comparison functions ADT_EQ_*, ADT_NE_*, ADT_LT_*, etc. defined for the predefined types have been simplified in the same way.
Finally, the C code generated by TRAIAN for the comparison functions "<", "<=", ">", and ">=" defined over singleton types has been optimized. See item 567 in the HISTORY.txt file.

The C code generated by TRAIAN to implement the comparison functions "<", "<=", ">", and ">=" defined over tuples and ordinary types was enhanced in several ways:
- From now on, the implementation of "<=" and ">=" no longer invokes the "==" function to compare fields, thus avoiding hidden dependencies.
- The generated C code now uses a sequence of "if ... return" instructions, which are easy to read, instead of a single "return" with a complex combination of nested " ? : " operators, which was difficult to understand.
- The new code generation algorithm used by TRAIAN no longer relies on non-terminal recursion, thus avoiding potential stack overflows when compiling large LOTOS NT programs.
See item 568 in the HISTORY.txt file.

The C code generated by TRAIAN for "case" instructions was enhanced. From now on, tautological guards in patterns (e.g., "where true") are detected and TRAIAN no longer generates superfluous C code for them, namely:7
```
   if (ADT_TRUE ()) ...
```
or
```
   goto TRAIAN_CASE_LABEL_...;
```
This removes "statement not reached" warnings emitted by the C compiler on the C code produced by TRAIAN. See item 575 in the HISTORY.txt file.

The C code generated by TRAIAN for "case" instructions having exhaustive patterns (i.e., patterns covering all possible cases) was simplified. For such instructions, TRAIAN 3.12 no longer generates dead code fragments such as:
```
   fprintf (stdout, "%s:%d:error: unexpected case in pattern
            matching\n", "FILE.lnt", LINE);
   fflush (stdout);
   raise (15);
```
intended to report cases not covered by any pattern. Measured on our LOTOS NT test suite, this change eliminates 1.6% of the 5.5 million lines of C code generated by TRAIAN. See item 578 in the HISTORY.txt file.

The C code produced by TRAIAN was further simplified: from now on, the functions or macro-definitions for field update are no longer generated for LOTOS NT types having no "with set" clause.
Measured on our LOTOS NT test suite, this change eliminates 8.9% of the 5.5 million lines of C code generated by TRAIAN. This justifies the decision of making "with set" clauses explicit and mandatory. See item 587 in the HISTORY.txt file.

The C code generated by TRAIAN for tuples and for "cascade" types (i.e., types defined as a union of enumerated types) was optimized. From now on, the C code generated by TRAIAN to implement field accesses, field updates, printing functions, string functions, and hashing over these types invokes dedicated, faster macro-definitions to select constructor fields. See item 590 in the HISTORY.txt file.

The C code produced by TRAIAN was further simplified : from now on, the TRAIAN_GET_* functions or macro-definitions for field selection are no longer generated for LOTOS NT types having no "with get" clause.
Measured on our LOTOS NT test suite, this change eliminates 2.1% of the 5 million lines of C code generated by TRAIAN. See item 591 in the HISTORY.txt file.

Library Changes

The scheme files for lists, sorted lists, and sets have been extended by adding definitions of the following functions:
- For list types: DELETE, REMOVE, and UNION;
- For sorted-list types: DELETE, INTER, MINUS, REMOVE, and UNION;
- For set types: INTER, MINUS, SUBSET, and UNION.
Consequently, TRAIAN now generates C code to implement these functions. Notice that, from a model-checking perspective, the implementation prioritizes space over time, in order to be memory efficient.
Also, these new functions come with hidden dependencies:
- "with DELETE" requires "with MEMBER"
- "with REMOVE" requires "with MEMBER"
- on sets, "with INTER" requires "with SUBSET"
- on sets, "with UNION" requires "with SUBSET"
See item 558 in the HISTORY.txt file.

The scheme files for lists, sorted lists, and sets was further extended by adding missing definitions for the functions "==", "=", "!=", and "<>".
Therefore, TRAIAN now uses these definitions to generate C code for implementing these functions. This new code is more efficient than the one formerly generated by TRAIAN 3.11, since it uses iteration rather than recursion. For instance,nsome LOTOS NT programs handling large lists (9.9 million elements) now execute normally, whereas the code generated by TRAIAN 3.11 could cause stack overflows.
Notice that, if type T2 is defined as a list (or sorted list, or set) of another type T1, then the clause "with ==" (resp. "=", "!=", or "<>") in T2 now requires the presence of the same clause "with ==" (resp. "=", "!=", or "<>") in T1, as TRAIAN 3.12 no longer implements "==" and "!=" automatically.
For sorted lists and sets, this constraint was already there, because the INSERT function requires the "==" function.
TRAIAN 3.12 will report missing definitions by issuing error messages such as:
```
  type T1 lacks function "==" needed by clause "with ==" of type T2
```
See item 566 in the HISTORY.txt file.

In file "incl/lotosnt_predefined.h", the redefinition of the free() macro was modified to avoid a "-Wempty-body" warning ("suggest braces around empty body in an 'else' statement") emitted by GCC. Such a warning occurred when compiling demo_02, for instance. See item 569 in the HISTORY.txt file.

The scheme files for sets and sorted lists have been enhanced by adding a DIFF function that computes symmetric difference, in addition to the already existing MINUS function that computes "normal" difference. See item 574 in the HISTORY.txt file.

A few definitions in file "lotosnt_predefined.h" have been modified to suppress two warnings emitted by Clang on macOS, namely:

   result of comparison of constant 128 with expression of type 'signed char'
   is always true [-Wtautological-constant-out-of-range-compare]

and

   illegal character encoding in character literal [-Winvalid-source-encoding]

See item 576 in the HISTORY.txt file.

To further align TRAIAN with LNT2LOTOS, the constructor ZERO of type Nat defined in the file "lotosnt_predefined.lnt" was renamed to "0".

This change is not backward compatible, as all occurrences of ZERO should be replaced by "0". Notice, however, that the name ZERO was not officially documented in the reference manuals of TRAIAN and LNT2LOTOS.

Besides increasing compatibility between LNT2LOTOS and TRAIAN, this change enables a more precise analysis of patterns. For instance, given the following definition:

   function F (N : NAT) : BOOL is
      case N in
         0 -> return false
      |  SUCC (any) -> return true
      end case
   end function

TRAIAN no longer emits the following (spurious) warning:

   possibly incomplete patterns in "case" instruction
   some values of type NAT, namely those of the following form:
      ZERO
   might not be matched by the given constants (an "any"
   pattern might be necessary to match the missing cases)

Also, given the following definition:

   function G (N : NAT) : BOOL is
      case N in
	 0 -> return false
      |  2 -> return true
      end case
   end function

TRAIAN 3.12 now emits a more informative warning:

   possibly incomplete patterns in "case" instruction
   some values of type NAT, namely those of the following form:
      SUCC (X : NAT)
   might not be matched by the given constants

See item 582 in the HISTORY.txt file.

In the scheme files for lists, sorted lists, and sets, the definition of the HEAD and TAIL functions have been modified to avoid using the "." operator that now requires an explicit "with get" clause. This change should be invisible to the users of TRAIAN. See item 586 in the HISTORY.txt file.

Release Changes

To further align the TRAIAN distribution with CADP, the shell-script com/traian_delete was deleted, and replaced by a new shell-script src/com/cadp_delete. See item 559 in the HISTORY.txt file.

Bug Fixes

A bug (introduced in TRAIAN 3.11) was fixed, which generated inefficient C code for nullary constructors such as NIL(): their implementation wasted memory by allocating a different chunk of memory at each constructor call, thus causing memory leaks. See item 550 in the HISTORY.txt file.

The C code generated by TRAIAN for tuple types was corrected:
- When declaring the result of some comparison functions, occurrences of the "int" type were replaced by ADT_BOOL.
- Also, missing comments /* forward */ have been added for a few functions operating on tuple types.
See item 551 in the HISTORY.txt file.

A bug was fxed in the C code generation for ordinary types having a "!card" pragma together with "==" and "!=" operations defined using a "with" clause, e.g.:
```
   type T is
      !card 4
      C1 (B: BOOL),
      C2 (N: NAT)
   with ==, !=
   end type
```
To implement the "!=" operation of such types, TRAIAN 3.11 generated a macro-definition and a function, both of which were named TRAIAN_NE_T(). This caused a syntax error when the C compiler reached the function definition:
```
   "test.c", line 641: syntax error before or at: (
   "test.c", line 641: identifier redeclared: ADT_BOOL
   etc.
```
See item 555 in the HISTORY.txt file.

In the C code generated by TRAIAN, "forward" declarations have been added for all the functions defined in scheme files (i.e., all "with" functions). This change suppresses warning and error messages such as:
```
   warning: implicit function declaration: TRAIAN_MEMBER_TI
   identifier redeclared: TRAIAN_MEMBER_TI
```
that could be emitted by the C compiler, depending in which order types and functions were declared. See item 557 in the HISTORY.txt file.

A bug was fixed: when compiling a pattern with braces (i.e., "{...}") for some type, the CONS function of which is a constructor, while the NIL function of which is not a constructor but a function defined by the user, TRAIAN 3.11 generated incorrect C code that was rejected by the C compiler, e.g.:
```
   "test.c", line 9: warning: implicit function declaration:
                          TRAIAN_MATCH_TRAIAN_FUNCTION_NIL_167
   Undefined                     first referenced
   symbol                           in file
   TRAIAN_MATCH_TRAIAN_FUNCTION_NIL_167 test.o
```
See item 560 in the HISTORY.txt file.

In order to avoid ambiguities or name clashes, some C identifiers generated by TRAIAN were modified. In essence, single underscore characters were replaced by two consecutive underscores in C identifiers (knowing that LOTOS NT identifiers must not contain consecutive underscores).
- The identifiers for field update:
```
   TRAIAN_UPDATE_<type>_<field>   -- single underscores
```
  have been renamed to:
```
   TRAIAN_UPDATE_<type>__<field>  -- double underscores
```
- The identifiers for field selection:
```
   TRAIAN_GET_<type>_<field>      -- single underscores
```
  have been renamed to:
```
   TRAIAN_GET_<type>__<field>     -- double underscores
```
- The other identifiers for field selection:
```
   TRAIAN_GET_<type>_<constructor>_<field>   -- single underscores
```
  have been renamed to:
```
   TRAIAN_GET_<type>__<constructor>__<field>  -- double underscores
```
Consequently, in file "incl/lotosnt_predefined.h", the following macro-definitions:
```
   TRAIAN_GET_ADT_NAT_SUCC_X
   TRAIAN_GET_ADT_INT_NEG_X
   TRAIAN_GET_ADT_INT_POS_X
```
have been renamed to:
```
   TRAIAN_GET_ADT_NAT__SUCC__X
   TRAIAN_GET_ADT_INT__NEG__X
   TRAIAN_GET_ADT_INT__POS__X
```
Such changes are not backward compatible, and it might be necessary to modify handwritten C files, such as ".fnt" and ".tnt" files, if they contain such identifiers. See item 588 in the HISTORY.txt file.

A bug was fixed, which occurred when the definition of a type T contained overloaded constructors having common field names, e.g.:
```
   type T is
      C (X: BOOL, Y: INT),
      C (X: BOOL, Z: REAL),
      D
   end type
```
In such case, the C code generated by TRAIAN was incorrect, as it defined two different macros named TRAIAN_GET_T__C__X, which caused warnings from the C preprocessor:
```
   macro redefined: TRAIAN_GET_T__C__X
```
From now on, in presence of overloaded constructors, TRAIAN generates unique names for the macro-definitions. These are now named TRAIAN_GET_T__C__N__X, where N ≥ 1 is the index of the constructor (here, 1 or 2) in the type definition. See item 589 in the HISTORY.txt file.

An issue was fixed in code generation: if, for some type T, the source LOTOS NT program defined an equality function == : T, T → BOOL, TRAIAN 3.11 generated a C function to implement this equality function, but also generated a useless macro-definition named TRAIAN_EQ_T. The latter is no longer produced by TRAIAN 3.12. See item 592 in the HISTORY.txt file.

The static semantic checks of TRAIAN have been strengthened as follows: if some type T2 defined by the list of its constructors has a clause "with ==" (resp. "!=", "<", "<=", etc.), then each type T1 used by (at least) one parameter of a constructor of T2 must also have a function "==" (resp. "!=", "<", "<=", etc.), which can be defined either explicitly, or implicitly using another "with" clause. If not, TRAIAN 3.12 will issue an error message of the form:
```
   type T1 lacks function "==" needed by "==" for type T2
   type T1 lacks function "<" needed by "<" for type T2
   etc.
```
In such case, TRAIAN 3.11 generated C code that did not compile properly, as it contained references to undefined comparison functions, causing warnings from the C compiler:
```
   warning: implicit function declaration: TRAIAN_EQ_T1
```
This change is healthy, but may require to manually update existing LOTOS NT programs to insert missing "with ==", etc. clauses. For instance, file "demos/demo_01/DATA_IEEE_1394.lnt" was modified accordingly. See item 593 in the HISTORY.txt file.

Two problems have been corrected in the C code generated by TRAIAN for STRING functions:
- When a type T1 defined by its constructors was equipped with a STRING : T1 → STRING function defined explicitly (and not implicitly using a "with" clause), TRAIAN 3.11 generated both this function and an extra function named TRAIAN_STRING_T1, the body of which was produced automatically. TRAIAN 3.12 no longer generates this extra function.
- 2) If type T1 was used by another type T2 (either defined by its list of constructors, or as a list, sorted list, or set of T1) having a "with STRING" clause, then the STRING : T2 → STRING function generated for T2 invoked TRAIAN_STRING_T1 instead of the STRING : T1 → STRING defined by the user. This issue was fixed in TRAIAN 3.12.
See item 597 in the HISTORY.txt file.

Another bug was fixed in the C code generated by TRAIAN for STRING functions. When mixing STRING functions defined explicitly by the user and implicitly (using "with" clauses), the generated C code could cause memory faults and core dumps at run time. The reason was that, although it is possible to invoke free() on the results returned by STRING functions defined implicitly, this is not permitted on the results of STRING functions defined explicitly. The C code generated by TRAIAN has been modified in consequence. See item 598 in the HISTORY.txt file.

The implementation of cascade types was entirely revised to address various issues:
- The NEXT function for iterating on cascade types was corrected, as it enumerated one extra value beyond the upper bound of the type domain.
- When encoding cascade types, constructors were used in the reverse order of their declaration; they are now used in their declaration order.
- When encoding cascade types, constructor parameters were considered from right to left; they are now considered from left to right.
See item 599 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.12 can be freely downloaded from the TRAIAN Web Page located at:

http://vasy.inria.fr/traian