TRAIAN 3.8 released on October 29, 2022
The CONVECS team is pleased to announce
that version 3.8 of the TRAIAN compiler for LOTOS NT is available.
TRAIAN 3.8 has been prepared by Hubert Garavel, Frederic Lang, and
Wendelin Serwe. It was released four months after version 3.7 of TRAIAN.
TRAIAN 3.8 brings
thirteen language changes,
nine static-semantics changes,
two compiler changes,
six release changes,
and six bug fixes
(see below their description).
TRAIAN 3.8 introduces various changes to the LOTOS NT language in order to
further align it with the LNT language supported by the
CADP toolbox. The LOTOS NT Reference Manual
and the demo examples have been updated to reflect these changes.
LOTOS NT was extended to permit (optional) loop identifiers for the
"for" and "while" loops, so as to allow these loops to be
interrupted by "break" clauses.
See item 416 in the HISTORY.txt file.
The syntax of LOTOS NT was extended with the clause "raise E ()", which
is equivalent to "raise E".
See item 420 in the HISTORY.txt file.
The syntax of LOTOS NT was simplified by removing three out of four situations
where the "eval" keyword is mandatory.
From now on, in LOTOS NT functions and processes, calls to functions that
return a result should be written:
X := F [E1, ..., Em] (A1, ..., An)
eval X := F [E1, ..., Em] (A1, ..., An)
where each Ai is either an "in" parameter (i.e., "Vi"), an "out"
parameter (i.e., "?Xi"), or an "in out" parameter (i.e., "!?Xi").
Also, in LOTOS NT functions, calls to functions that do not return a result
should now be written:
F [E1, ..., Em] (A1, ..., An)
eval F [E1, ..., Em] (A1, ..., An)
In these three situations, occurrence of a (now useless) "eval" keyword
will trigger a new warning:
"eval" before function call in instructions (or behaviours) is deprecated and should be removed
For the moment, the "eval" keyword is still mandatory when calling a
function without result in a LOTOS NT process, and does not trigger such a
Since the syntax of LOTOS NT has been extended to accept function calls
without "eval", a new verification phase (called "context checking")
has been added to TRAIAN, so as to reject function calls performing side
effects where side effects are not allowed. For instance, the following code
fragments are now syntactically accepted:
return G (?X)
X := any NAT where F (?X, Y)
if F (?X, Y) then ...
but rejected with a new error message:
forbidden argument "?X" causing side effect in value
Users are advised to upgrade their LOTOS NT programs by running the following
traian_upc 2022-LOTNT-EVAL [<file> or <directory>]
which will remove "eval" keywords where appropriate.
See item 421 in the HISTORY.txt file.
New restrictions have been introduced on functions whose name is a special
identifier (i.e., is made up of non-alphanumeric characters, such as "+", "*",
"&", etc.). From now on, these functions must return a result and should
not have "out", "out var" or "in out" parameters
(implying that these functions can only be called in the context of
expressions, and thus perform no side effects). Improper definitions are
syntactically accepted but rejected during static-semantics checking.
Indeed, the removal of "eval" keywords opens the way to instructions such as:
+ (a, b);
a + b;
The new restrictions avoid such a potentially misleading syntax. This
change is incompatible, in the sense that certain LOTOS NT specifications
may, after removing "eval" keywords, become incorrect. The solution is
to manually rename the offending functions, e.g., renaming "+" into "PLUS".
See item 426 in the HISTORY.txt file.
The syntax of LOTOS NT was modified to require that keywords "library"
and "end library" are written in the lower case exclusively.
See item 427 in the HISTORY.txt file.
The syntax of LOTOS NT was extended with a "module M (M1, ..., Mn) ..."
clause, which imports in M the modules M1, ..., Mn and their dependences,
See item 428 in the HISTORY.txt file.
TRAIAN was modified to ensure that, for each file "F.lnt" starting with a
"module M ..." clause, the module name M is case-sensitively equal to
the file name F (except in the particular case where M is equal to "test",
"Test", "TEST", etc.). Formerly, M had to be case-insensitively equal to F;
from now on, the comparison is case-sensitive. This new constraint is
perfectly logical, since in a clause
"module M (M1, ..., Mn) ...", the module names M1, ..., Mn already
had to be case-insensitively equal to their respective file names.
See item 429 in the HISTORY.txt file.
The syntax of LOTOS NT was enhanced by allowing functions and processes to be
called with named event parameters (in addition to positional event parameters,
which were already supported). As for named variable parameters, named event
parameters also support ellipses ("...").
See item 430 in the HISTORY.txt file.
The syntax of LOTOS NT types and modules was extended to allow the
"with get" and "with set" clauses. The expansion phase of
TRAIAN was also modified to take these clauses into account.
See item 434 in the HISTORY.txt file.
The syntax of LOTOS NT types was extended to support "!implementedby"
pragmas attached to the functions defined in "with" clauses, e.g.:
type T is
A, B, C
with < !implementedby "LOTOS:<" !implementedby "C:LT"
Such pragmas were syntactically rejected by TRAIAN 3.7. The compiler also
ensures that "!external" pragmas are not attached to such
See item 436 in the HISTORY.txt file.
The syntax of output communication offers was simplified. Previously, such
offers could be written either "V" or "!V". From now on, the syntax "!V" is
no longer supported, so that one must write "G (V)" instead of "G (!V)".
See item 438 in the HISTORY.txt file.
The syntax of LNT was enhanced to allow the definition of functions whose
identifiers start with a digit, e.g., 0, 1,
123, 456_789, 3e10, 0b11_0001,
0x1AF3, 01T22, etc.
Such identifiers are often used in LNT programs. Such an extension enables to
define types with numeric constants, e.g., the type Bit with its two constants
0 and 1, or abstracted versions of the numeric types Int, Nat, and Real.
Several rules constrain functions having such identifiers:
See item 439 in the HISTORY.txt file.
These functions must return a result.
If the identifier is identical to some numeric constant, the function must
return a type different from the potential types of this constant. For
instance, a function named "3E4" may not return a result of type
Real, and a function named "12" may not return a result of type Nat
The predefined library of LOTOS NT was extended with two identity functions:
function + (X : INT) : INT
function + (X : REAL) : REAL
Having these functions predefined will prevent users from defining them,
therefore avoiding semantic ambiguities. For instance, if users could define:
function + (X : INT) : INT is
return X + 1
then "+1" and "+(1)" would give two different values.
See item 444 in the HISTORY.txt file.
TRAIAN was modified to avoid displaying several times redundant messages
about undefined types when analyzing functions generated automatically
during the expansion phase.
See item 409 in the HISTORY.txt file.
The support of array types in TRAIAN progressed as follows: for each array
type T with N elements of type T', a constructor T : T', ..., T' -> T is
automatically defined, as well as a function T : T' -> T, which builds
an array, all the elements of which are initialized to the same value.
Static-semantics checks that the bounds of arrays define non-empty intervals
have also been implemented. However, generation of C code for arrays is not
See item 410 in the HISTORY.txt file.
Various static-semantics checks on array accesses have been introduced. For
instance, TRAIAN now displays new error messages such as:
array access applied to non-array value
the left-hand value has non-array type Nat
non-natural array index
X [true] := 0
the bracketed array index has type BOOL instead of NAT
array assigned with incorrect type
X  := true
the type T of X is an array of nat but the right-hand value has type BOOL
See item 414 in the HISTORY.txt file.
The algorithm used by TRAIAN to analyse nested loops, which had an exponential
cost in time, was revised. The new algorithm has a linear cost in time, is
thus faster, and also uses less memory. For instance, on a LOTOS NT program
having 61 nested loops, the old algorithm took more than 54 minutes and used
110 GB of memory on an x64 machine, whereas the new algorithm takes 0.04 second
and uses only 19 MB of memory.
See item 415 in the HISTORY.txt file.
The data-flow analysis performed by TRAIAN for the loops interrupted by
"break" clauses was enhanced. From now on, uses of variables afer
"break" clauses are no longer taken into account, which leads to
new warnings such as:
useless assignment to X
when a variable assigned before a "break" clause is neither used before
the "break" nor after the end of the loop.
See item 417 in the HISTORY.txt file.
TRAIAN was modified to emit a better warning when an "in" parameter of
an LOTOS NT function or process is assigned. Previously, the warning was:
"in" parameter X overwritten before used (should be a local variable)
From now on, the warning is:
"in" parameter X modified (should be an "in var" parameter)
See item 419 in the HISTORY.txt file.
Following the (partial) removal of the "eval" keyword, the data-flow
analysis rules of TRAIAN were adapted to the new situation, as LOTOS NT
programs that were previously rejected are now valid, e.g.:
function G [E1, E2 : none] (out X, Y : nat) is
X := F [E1, E2] (1, ?Y) -- without "eval"
From now on, if the right-hand side of an assignment is a function call with
"out" or "in out" parameters, the data-flow analysis considers
these parameters as modified. Moreover, new verifications have been added to
detect unwanted uses of "out" or "in out" parameters, e.g.:
X := F [E1, E2] (?X)
Y := F [E1, E2] (?X, ?X)
which are rejected with new error messages:
- result variable X also used as "[in] out" parameter
- multiple occurrences of variable X in "[in] out" parameters
See item 422 in the HISTORY.txt file.
The static-semantics contraints concerning the
!implementedby "LOTOS:..." pragmas have been relaxed.
From now on, when TRAIAN is invoked with its "-lotos" option, it no
longer requires that each external type and external function has such a
pragma. This suppresses spurious warnings emitted for the predefined
LOTOS NT library, whose functions are declared with
!implementedby "C:..." pragmas, but not with
!implementedby "LOTOS:..." pragmas.
See item 425 in the HISTORY.txt file.
The data-flow analysis of TRAIAN was strengthened. Given a function or a
process with "out" or "in out" parameters, or a function
returning a result, an error message is now emitted if TRAIAN detects that
this function or process always falls into an infinite loop, with no
possibility of returning normally or raising an event. Previously, only a
warning was emitted in such case. For instance, given the following function:
function F : BOOL is
TRAIAN now emits an error message:
error: function with result but looping forever
rather than a mere warning:
warning: function with result but no normal termination
See item 437 in the HISTORY.txt file.
Two new options "-c" and "-lotos" have been added to the
TRAIAN compiler. These options instruct TRAIAN to generate C code or LOTOS
code. The default option is "-c".
See item 423 in the HISTORY.txt file.
A new option "-analysis" was added to TRAIAN. This option halts
the execution before code generation.
See item 424 in the HISTORY.txt file.
The demo_01 was modified to rename the SIG_ACK() function, which conflicted
on Windows with a library function having the same name, to SIG_ACKN().
Also, in the ".zip" file containing the TRAIAN distribution, the demo
Makefiles no longer contain carriage returns, which caused problems on
See item 411 in the HISTORY.txt file.
The "traian_cc" shell script was modified to invoke:
See item 412 in the HISTORY.txt file.
- cc with option -m64 on architecture sol64;
- gcc with option -m32 or -m64 on architectures iX86 and x64;
- gcc with option -no-pie on architectures iX86 and x64;
- the Mingw32 version of gcc on Windows.
The TRAIAN distribution was ported to 64-bit Windows (architecture "win64"),
in addition to the existing support for 32-bit Windows (architecture "win32").
A new directory "bin.win64" was added and many shell scripts (e.g., "arch",
"traian_cc", "traian_indent", "traian_which", etc.) were extended. To use
the "win64" architecture, the environment variable $CADP_BITS should be
set to 64.
See item 413 in the HISTORY.txt file.
The READ_ME file of demo_02 was updated by replacing dead URLs with valid ones.
The LOTOS NT code of demo_02 was also updated to meet the requirements set
by recent versions of TRAIAN (e.g., the replacement of "!pointer 211"
with "!card 211").
See item 441 in the HISTORY.txt file.
The demo_03, which had been removed from the TRAIAN distribution in February
2020, was restored. The LOTOS NT source code of this demo was updated and
the comments present in this code have been translated to English.
See item 442 in the HISTORY.txt file.
The demo_04 was deeply revised in many ways:
See item 443 in the HISTORY.txt file.
- The READ_ME file has been updated. All files have been pretty-printed and
made more readable.
- In the main.c file, three declarations of global variables (sxstdout,
sxstderr, and sxtty) have been removed to avoid errors (multiple definitions
of symbols) reported by some C compilers.
- The SIMPROC compiler now generates C code after performing its analyses.
Integer numbers are now translated properly. The generated C code displays
all global variables when the execution of the SIMPROC program terminates,
so that the computed results can be observed.
- The sample SIMPROC programs, which had been removed in February 2020,
have been restored, and two new programs (ackermann.sim and fibonacci.sim)
have been added.
- The Makefile has been enhanced. It first builds the SIMPROC compiler,
then uses it to compile and execute all the sample SIMPROC programs.
The scanner and parser of TRAIAN were modified to get rid of undesirable
lexical and syntactic constraints on LOTOS NT. From now on, when declaring
an "array" or "range" type, it is no longer required to insert
a mandatory space (or comment) between the lower bound of the interval and
the ".." keyword that follows this bound. Previously, a space or comment was
mandatory, otherwise the lower bound was parsed as the beginning of a real
See item 418 in the HISTORY.txt file.
Another bug was fixed in the TRAIAN parser: the LOTOS NT fragment "- [...] N",
where N is a natural number, was understood as the negative integer "-N"
rather than a call to the "-" function with exception parameters.
See item 431 in the HISTORY.txt file.
An issue was fixed, which caused TRAIAN to reject correct LOTOS NT programs.
In a process P, when a call to a function or process contained an ellipsis
("...") covering a variable X declared as a parameter of P, TRAIAN would
wrongly indicate that this variable X was not declared. For instance, the
following code fragment was rejected:
process P1 [E : any] (X : nat) is
P2 [...] (...)
process P2 [E : any] (X : nat) is
P1 [...] (...)
See item 432 in the HISTORY.txt file.
Missing static-semantics checks have been added in functions invoked with
ellipsis ("...") parameters. In the context of function calls that are not
allowed to perform side effects, TRAIAN did not check, after expanding the
ellipsis, that the implicit parameters corresponding to the ellipsis were
only "in" parameters, and accepted "out" or "in out"
parameters unduly. For instance, the following code fragment:
function F (out X : nat) : bool is
X := 1;
function G : bool is
var X : nat in
return F (...);
is now rejected with the following error message:
forbidden argument "?X" causing side effect in value (when expanding "...")
See item 433 in the HISTORY.txt file.
The data-flow analysis of TRAIAN was strengthened. Previously, "true",
"true ()", and "true (...)" were all recognized as the TRUE
constant. From now on, "true [...]", "true [...]()" and
"true [...] (...)" are also recognized as the TRUE constant. The
same changes have been done also for the FALSE constant. For instance, the
function F (in var X : int) is
while true [...] () loop
X := X - 1
now displays an "infinite loop" warning.
See item 435 in the HISTORY.txt file.
Another bug was fixed in data-flow analysis. Spurious warnings about useless
assignements were emitted when an input variable of some event was only used
in the Boolean guard attached to this event, e.g.,
G (?X) where X != 0
From now on, the fact that X is used in the Boolean guard is properly taken
See item 440 in the HISTORY.txt file.
With TRAIAN 3.8, the convergence between LOTOS NT and LNT has steadily
progressed. Measured on a test suite of 13,400+ correct LNT programs,
TRAIAN 3.8 syntactically accepts 97.4% of them, whereas TRAIAN 3.7 only
accepted 47.6% of them.
TRAIAN will continue to evolve, our goal being to merge LOTOS NT and LNT
in one single language.
TRAIAN 3.8 can be freely downloaded from the
TRAIAN Web Page located at: