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.

Release Notes

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).

Language Changes

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.

1. 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.


2. 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.


3. 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)
   

   instead of:

      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)
   

   instead of:

      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 warning.
   
   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 command:

      traian_upc 2022-LOTNT-EVAL [<file> or <directory>]
   

   which will remove "eval" keywords where appropriate. See item 421 in the HISTORY.txt file.


4. 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);
   

   or even:

      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.


5. 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.


6. 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, transitively. See item 428 in the HISTORY.txt file.


7. 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.


8. 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.


9. 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.


10. 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"
       end type
    

    Such pragmas were syntactically rejected by TRAIAN 3.7. The compiler also ensures that "!external" pragmas are not attached to such "with" clauses. See item 436 in the HISTORY.txt file.


11. 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.


12. 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:
    • 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 or Int.
    See item 439 in the HISTORY.txt file.


13. 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
       end function
    

    then "+1" and "+(1)" would give two different values. See item 444 in the HISTORY.txt file.

Static-Semantics Changes

1. 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.


2. 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 available yet. See item 410 in the HISTORY.txt file.


3. 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
      in value:
          X [3]
      the left-hand value has non-array type Nat
   
      non-natural array index
      in instruction:
          X [true] := 0
      the bracketed array index has type BOOL instead of NAT
   
      array assigned with incorrect type
      in instruction:
           X [0] := 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.


4. 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.


5. 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.


6. 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.


7. 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"
      end function
   

   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)
   

   or

      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.


8. 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.


9. 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
         loop
            null
         end loop
      end function
   

   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.

Compiler Changes

1. 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.


2. A new option "-analysis" was added to TRAIAN. This option halts the execution before code generation. See item 424 in the HISTORY.txt file.

Release Changes

1. 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 Linux. See item 411 in the HISTORY.txt file.


2. The "traian_cc" shell script was modified to invoke:
   • 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.
   See item 412 in the HISTORY.txt file.


3. 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.


4. 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.


5. 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.


6. The demo_04 was deeply revised in many ways:
   
   
   • 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.
   
   
   See item 443 in the HISTORY.txt file.

Bug Fixes

1. 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 number. See item 418 in the HISTORY.txt file.


2. 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.


3. 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 [...] (...)
      end process
   
      process P2 [E : any] (X : nat) is
         E (X);
         P1 [...] (...)
      end process
   

   See item 432 in the HISTORY.txt file.


4. 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;
         return true
      end function
   
      function G : bool is
         var X : nat in
            return F (...);
            use X
         end var
      end function
   

   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.


5. 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 following definition:

      function F (in var X : int) is
         while true [...] () loop
            X := X - 1
         end loop
     end function
   

   now displays an "infinite loop" warning. See item 435 in the HISTORY.txt file.


6. Another bug was fixed in data-flow analysis. Spurious warnings about useless assignments 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 into account. See item 440 in the HISTORY.txt file.

Future Work

TRAIAN will continue to evolve, our goal being to merge LOTOS NT and LNT in one single language.

Download

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