The CONVECS team is pleased to announce
that version 3.11 of the TRAIAN compiler for LOTOS NT is available.
With TRAIAN 3.11, the convergence between LOTOS NT and LNT is complete. Measured on a test suite of 13,600+ correct LNT programs totalling more than 9 million non-blank lines of LNT code, TRAIAN 3.11 syntactically accepts 100% of these programs and semantically accepts 100% of them (whereas TRAIAN 3.10 accepted 93.5% of them).
TRAIAN 3.11 brings three language changes, three compiler changes, three code-generation changes, fourteen library changes, one release change, and seven bug fixes (see below their description).
type T is range ... of T' end typeor
type T is X:T' where ... end typeand E is of type T', then "E of T" means "T (E)", i.e., the conversion of expression E from type T' to type T.
type T1 is range 0..255 of nat end type type T2 is X:T1 where X * X < 100 end typeone can write "0 of T1", "1 of T2", etc., or equivalently "T1 (0)", "T2 (T1 (1))", etc.
Consequently, many LOTOS NT or LNT programs formerly rejected by TRAIAN are now accepted. See item 541 in the HISTORY.txt file.
limitation: types not yet fully implementedwhen an input LOTOS NT program contains sets or sorted lists, and generates C code for the functions defined in the scheme files of these types. See item 522 in the HISTORY.txt file.
limitation: types not yet fully implementedSee item 547 in the HISTORY.txt file.
function HEAD [EMPTY : NONE] (X : LNT_T1) : LNT_T2 function TAIL [EMPTY : NONE] (X : LNT_T1) : LNT_T1in addition to the already existing ones:
function HEAD (X : LNT_T1) : LNT_T2 function TAIL (X : LNT_T1) : LNT_T1Consequently, the expansion phase of TRAIAN has been modified to handle the case where a scheme file contains overloaded functions, such as HEAD and TAIL, which exist under the same name, with and without event parameter.
See item 523 in the HISTORY.txt file.
The existing LOTOS NT programs that invoke CARD functions defined in "with" clauses should be updated to define such functions explicitly. See item 524 in the HISTORY.txt file.
The existing LOTOS NT programs that invoke the LENGTH function on sets should be updated accordingly, so as not to be rejected by TRAIAN with the following message:
error: unknown function length in "with" clause of type SETSee item 525 in the HISTORY.txt file.
function ISEMPTY (X : STRING) : BOOL function NTH (X : STRING, N : NAT) : CHARhave been renamed into, respectively:
function EMPTY (X : STRING) : BOOL function ELEMENT (X1 : STRING, X2: NAT) : CHARby analogy with the EMPTY and ELEMENT functions defined on "list", "set", and "sorted list" types.
Users are advised to upgrade their LOTOS NT programs by running the following command:
traian_upc 2023-LOTNT-PREDEFINED [<file> or <directory>]which will rename functions where appropriate. See item 527 in the HISTORY.txt file.
function PRED [RANGE_ERROR: NONE] (X : BOOL) : BOOL function PRED [RANGE_ERROR: NONE] (X : NAT) : NAT function PRED [RANGE_ERROR: NONE] (X : INT) : INT function PRED [RANGE_ERROR: NONE] (X : CHAR) : CHAR function SUCC [RANGE_ERROR: NONE] (X : BOOL) : BOOL function SUCC [RANGE_ERROR: NONE] (X : NAT) : NAT function SUCC [RANGE_ERROR: NONE] (X : INT) : INT function SUCC [RANGE_ERROR: NONE] (X : CHAR) : CHARMoreover, the semantics of the PRED and SUCC functions (with or witout a RANGE_ERROR event parameter) has been modified as follows. Formerly, when invoked on the smallest (resp. largest) value of the BOOL, NAT, INT, or CHAR type, the PRED (resp. SUCC) function returned this value. From now on, they raise an exception, which is either the actual event passed to the RANGE_ERROR parameter, or UNEXPECTED if the RANGE_ERROR parameter is absent. See item 532 in the HISTORY.txt file.
function CARD (X : BOOL) : NAT function CARD (X : NAT) : NAT function CARD (X : INT) : NAT function CARD (X : CHAR) : NAT function ORD (X : BOOL) : NAT function ORD (X : NAT) : NAT function ORD (X : INT) : NAT function ORD (X : CHAR) : NATas well as the eight C functions implementing them, namely: ADT_CARD_BOOL(), ADT_CARD_NAT(), ADT_CARD_INT(), ADT_CARD_CHAR(), ADT_ORD_BOOL(), ADT_ORD_NAT(), ADT_ORD_INT(), and ADT_ORD_CHAR(). See item 533 in the HISTORY.txt file.
function CHAR [RANGE_ERROR : NONE] (X : INT) : CHAR function CHAR (X : INT) : CHARhave been removed from the predefined library of TRAIAN, together with the two C functions ADT_TO_CHAR_INT() and TRAIAN_LIB_TO_CHAR_INT() implementing them. Indeed, these functions were useless, since there already exist two similar functions:
function CHAR [RANGE_ERROR : NONE] (X : NAT) : CHAR function CHAR (X : NAT) : CHARand one does not want to introduce in LOTOS NT the fruitless notion of signed characters. See item 534 in the HISTORY.txt file.
From now on, whenever a "set of T" or "sorted list of T" type
is defined, the two functions
== : T, T → bool
and
< : T, T → bool
must be defined for type T.
This change, combined with item 542 above, fixes an issue that existed in former versions of TRAIAN. From now, both expressions {1, 2} and {2, 1} are equal for "set" and "sorted list" types, whereas they were formerly different. See item 543 in the HISTORY.txt file.
function CHAR [RANGE_ERROR : NONE] (X : STRING) : CHAR function CHAR (X : STRING) : CHAR function STRING (X : STRING) : STRINGthe latter being an identity function. See item 545 in the HISTORY.txt file.
"test.c", line 207: duplicate case in switch: 1See item 520 in the HISTORY.txt file.
function F (X : nat) : bool is ... function F (in var X : nat) : bool is ...as well as the following ones:
function G (out X : nat) is ... function G (out var X : nat) is ...However, if functions F or G were invoked, TRAIAN emitted an error message: "ambiguous call to overloaded function". Thus, the issue only occurred with functions never called.
From now on, TRAIAN considers that "in var" and "out var" are identical to "in" and "out", respectively, and rejects the two above definitions, with error messages such as:
function F is already defined with the same profile at ... function G is already defined with the same profile at ...See item 526 in the HISTORY.txt file.
scheme_list.lnt:170: error: variable N may be uninitializedSee item 537 in the HISTORY.txt file.
For many years, TRAIAN has been used to develop compilers, including those of the CADP toolbox.
At present, TRAIAN is also increasingly used to check LNT specifications of
concurrent systems, allowing to catch mistakes not detected by the
"lightweight"
approach of the LNT2LOTOS
translator. Given that LOTOS NT and LNT have been merged in one single
language, we plan to integrate soon TRAIAN in the CADP toolbox, where it
will provide a full-fledged compiler front-end for the LNT language.
TRAIAN 3.11 can be freely downloaded from the TRAIAN Web Page located at: