TRAIAN: A Compiler for LNT Specifications

TRAIAN 3.16 is available for download (December 27, 2024)

• 1. The LNT language
• 2. The TRAIAN compiler
• 3. Release notes for TRAIAN
• 4. Download the latest version of TRAIAN
• 5. Related publications
• 6. Credits

1. The LNT language

LNT (formerly named "LOTOS NT", where "NT" stands for "New Technology") is a computer language that belongs to a family of languages originating from LOTOS and E-LOTOS. For complementary information about LOTOS, E-LOTOS, and LNT, read this article and the tutorial page of CADP.

Formal methods are often advocated as suitable formalisms for the specification of telecommunication protocols and distributed systems. The definition of LOTOS (ISO/IEC International Standard 8807) in 1989 was a major attempt at standardizing a formal method based on process calculi and algebraic data types.

The definition of LNT at INRIA Grenoble (formerly INRIA Rhône-Alpes) was undertaken as a side activity of the work initiated in 1992 by the ISO/IEC Committee for producing a revision of the LOTOS standard, which led to the adoption of E-LOTOS (Enhanced LOTOS, ISO/IEC International Standard 15437) in 2001.

LNT is a second generation Formal Description Technique that combines strong theoretical foundations with language features suitable for a wider acceptance by industry.

At INRIA Grenoble, LNT is intensively used for compiler construction. Thirteen compilers and translators (AAL, ATLANTIF, CHP2LOTOS, CTRL2BLK, EXP.OPEN, FSP2LOTOS, GRL2LNT, LNT2LOTOS, MCL_EXPAND, NTIF, PIC2LNT, SVL, and TRAIAN itself) have been written in LNT.

TRAIAN is a compiler for LNT developed at INRIA Grenoble, initially by the VASY team, then by the CONVECS team.

The name TRAIAN was chosen in honor of the Roman emperor (a successor of CAESAR) who funded Romania.

Until version 2.9, TRAIAN was developed using SYNTAX and FNC-2, two compiler generation tools designed at INRIA Rocquencourt.

Since version 3.0, TRAIAN is developed using SYNTAX and most of its source code (80%) is written in LNT itself, meaning that TRAIAN compiles itself by bootstrapping. It performs the following tasks:

• Lexical and syntactic analysis of LNT specifications
• Identifier binding
• Type checking
• Other static analyses
• Generation of C code for LNT type definitions
• Generation of C code for LNT function definitions

3. Release notes for TRAIAN

• TRAIAN 1.0 was released on September 8, 1998. Its main functionalities were syntax and semantic checking. To our knowledge, it was the first tool dedicated to (a variant of) the E-LOTOS language. The development of this tool was of great help in our contributions to the standardization of E-LOTOS.

• TRAIAN 2.0 was released on February 29, 2000. In addition to many bug fixes (about 45), new functionalities have been added, such as a C code generator for the data part of LNT. The compiler has also been ported to new operating systems, including Linux 2.0 and Windows. Several demo examples have been added, including a example that shows how a compiler can be constructed using a combination of SYNTAX and TRAIAN.

• TRAIAN 2.1 was released on November 14, 2000. This maintenance release fixes a few bugs in the compiler and provides a revised version of the LOTOS NT user manual.

• TRAIAN 2.2 was released on November 5, 2002. This maintenance release fixes a few bugs in the compiler, includes new versions of the garbage collector library, and adds documentation in PDF format.

• TRAIAN 2.3 was released on May 5, 2003. This release fixes five bugs in the compiler, implements more efficiently various classes of data types and provides the ability of splitting LOTOS NT specifications into separate files.

• TRAIAN 2.4 was released on June 8, 2004. This release fixes two bugs in the compiler and adds support for Mac OS operating system.

• TRAIAN 2.5 was released on October 6, 2005. This release fixes four bugs in the compiler. TRAIAN scripts and C libraries have been ported to machines based on Intel's Itanium IA64 architecture.

• TRAIAN 2.6 was released on February 27, 2008. This release fixes fifteen bugs in the compiler and improves the C code generated in two respects:
  • It no longer produces warnings when compiled with recent C compilers using the strictest code-checking options. Thus, TRAIAN users will only get warnings relevant to their LOTOS NT code.
  • TRAIAN scripts, predefined includes, and C libraries have been ported to mainstream 64-bit architectures (Sparc V9 stations running Solaris 10, Intel IA64 machines running 64-bit Linux, and Intel EMT64/AMD64 machines running 64-bit Linux).

• TRAIAN 2.7 was released on November 26, 2012. This release fixes six bugs in the compiler, its libraries, and its documentation. Also, the compatibility with CADP and its LNT2LOTOS translator was enhanced.

• TRAIAN 2.8 was released on February 29, 2016. This release brings the following changes:
  • A dedicated memory allocator makes TRAIAN more efficient on large LOTOS NT specifications (especially, those using 3-4 GB RAM, some of which grew too large to be processed by Traian 2.7); the new version of TRAIAN is faster (between 17% and 44% faster, 36% on the average) and uses less memory (between 18% and 32%) on large specifications.
  • Support for less-used architectures (MacOS/PowerPC, Linux/Itanium, Solaris/Sparc) has been dropped.
  • LOTOS NT-specific configuration files have been added for the following editors and pretty-printers: a2ps, gtk3, LaTeX listings, nano, npp, and vim. The configuration files for emacs and jEdit have also been updated.
  • Source code files for TRAIAN have been made available in the "src" directory.

• TRAIAN 2.9 was released on February 28, 2018. This release brings the following changes:
  • The source code of TRAIAN has been reduced by 40% and the executables by 50%.
  • TRAIAN now handles larger LOTOS NT specifications within the 4GB memory limit.
  • A new macro TRAIAN_ADT_INTERFACE_ONLY is now supported in include files.
  • External functions are now allowed to return a non-void result.
  • The "enum" and "record" keywords (syntactic sugar) have been deprecated.
  • Support for 64-bit macOS executables (x86-64) was added.
  • The GC garbage collector was upgraded from version 6.8 to version 7.6.4.
  • Various mistakes have been fixed in the LOTOS NT user manual.
  • Non-implemented LOTOS NT features are now marked in violet in the manual.

• TRAIAN 3.0 was released on February 29, 2020. TRAIAN was entirely rewritten; most of its code is now written in LOTOS NT, and compiles itself by bootstrapping. The new version is highly compatible with the previous one, but brings major enhancements:
  • Native 64-bit binaries are now available, thus eliminating the former 4GB memory limit.
  • The memory and time needed to compile large LOTOS NT programs have been reduced drastically.
  • The compiler produces shorter and clearer error messages.
  • Nineteen compiler bugs have been corrected.

• TRAIAN 3.1 was released on June 29, 2020. This release is both a consolidation release, which fixes a few bugs, and a transition release, which evolves the LOTOS NT language to bring it closer to the LNT language of the CADP toolbox.

• TRAIAN 3.2 was released on October 29, 2020. This release brings language changes intended to further align the LOTOS NT and LNT languages, as well as improvements in the C code generator.

• TRAIAN 3.3 was released on February 28, 2021. This release brings further language changes to align the LOTOS NT and LNT languages, as well as improvements to the compiler front-end and its C code generator.

• TRAIAN 3.4 was released on June 29, 2021. This release brings further language changes to align the LOTOS NT and LNT languages, as well as bug fixes and enhancements to the C code generator.

• TRAIAN 3.5 was released on October 29, 2021. This release brings further language changes to align the LOTOS NT and LNT languages, as well as major enhancements to the data-flow analysis performed by TRAIAN.

• TRAIAN 3.6 was released on February 28, 2022. This release brings further language changes to align the LOTOS NT and LNT languages, as well as enhancements to the C code generator.

• TRAIAN 3.7 was released on June 30, 2022. This release brings further language changes to align the LOTOS NT and LNT languages, and introduces data-flow analysis for LOTOS NT processes.

• TRAIAN 3.8 was released on October 29, 2022. This release brings further language changes to align the LOTOS NT and LNT languages and introduces 64-bit binaries of TRAIAN for Windows.

• TRAIAN 3.9 was released on February 28, 2023. This release achieves a nearly complete convergence between the LOTOS NT and LNT languages, making it possible to start using TRAIAN for checking LNT specifications of concurrent systems.

• TRAIAN 3.10 was released on June 30, 2023. This is a consolidation release that, in addition to bug fixes, brings extended support for external types and functions, library and code-generation enhancements, as well as better warning and error messages.

• TRAIAN 3.11 was released on September 29, 2023. This release achieves convergence between the LOTOS NT and LNT languages with respect to correct programs. In addition to bug fixes, it also brings enhanced support for sets and sorted lists.

• TRAIAN 3.12 was released on December 29, 2023. This release progresses convergence between the LOTOS NT and LNT languages with respect to incorrect programs, and improves C code generation in many respects.

• TRAIAN 3.13 was released on March 30, 2024. This release brings a new syntax for the "select" and "trap" constructs, as well as enhancements to static analysis and code generation.

• TRAIAN 3.14 was released on June 30, 2024. This release focuses on static analysis and increased convergence with LNT2LOTOS, as the semantic checks of LNT2LOTOS are progressively migrated to TRAIAN.

• TRAIAN 3.15 was released on September 29, 2024. This release pursues the progressive migration to TRAIAN of the semantic checks formerly done by LNT2LOTOS. Following a systematic review and comparison with the checks implemented in LNT2LOTOS, the error and warning messages displayed by TRAIAN are now more complete and informative.

• TRAIAN 3.16 was released on December 27, 2024. This is a consolidation release that completes the migration to TRAIAN of all static semantic checks formerly implemented in LNT2LOTOS. This release also introduces the concept of virtual processes that enable generic modules parameterized by processes.

4. Download the latest version of TRAIAN

The following computer architectures and operating systems are currently supported by TRAIAN:

• iX86 : PC (Intel/AMD x86) running 32-bit Linux
• x64 : PC (Intel/AMD x86-64) running 64-bit Linux
• sol64 : PC (Intel, 64-bit mode) running OpenIndiana or Solaris 11
• mac64 : Mac (Intel, 64-bit mode) running Mac OS X 10.4 or higher
• win32 : PC (Intel/AMD x86) running Windows (with Unix-like adds-on)
• win64 : PC (Intel/AMD x86-64) running Windows (with Unix-like adds-on)

The latest version of the TRAIAN compiler is version 3.16 released on December 27, 2024.

It is available for download from the VASY Web site:

• First, read the copyright notice

• Second, read the installation procedure

• Third, download the TRAIAN package, either in tar-gzipped format or zipped format. The tar-gzipped format is suitable for Unix users and the zipped format is suitable for Windows users. However, both packages are the same and contain the binaries for all the supported architectures/systems (Unixes and Windows).

• The SHA256 checksum of the tar-gzipped package is

  0f12e7e4b653121a40361e238f85930ee1ff5721fdcf50f075b28ca166f8f919  traian.tar.gz
  

  and the SHA256 checksum of the zipped package is

  996dd747f411967b06b8cea15ed3f95dadca6ea82d83bf8eb48e6b558f5c44fb  traian.zip
  

As of January 2025, newer versions of TRAIAN will be distributed as part of the monthly releases of the CADP toolbox. This new approach is a consequence of the ever tighter integration between LNT2LOTOS and TRAIAN.

Please contact cadp@inria.fr for any question or comment about TRAIAN.

LNT User's Manual (Version 3.16)
Mihaela Sighireanu (with updates by Alban Catry, David Champelovier, Hubert Garavel, Frédéric Lang, Guillaume Schaeffer, Wendelin Serwe, and Jan Stöcker)
December 2024, 88 pages.


From LOTOS to LNT
Hubert Garavel, Frédéric Lang, and Wendelin Serwe
October 2017, 29 pages.

About TRAIAN 2

Contribution à la définition et à l'implémentation du langage E-LOTOS
Mihaela Sighireanu
January 1999, PhD thesis, 300 pages.



Etude et réalisation d'un compilateur E-LOTOS à l'aide du générateur de compilateurs SYNTAX/FNC-2
Bruno Vivien
December 1997, in French, 150 pages.

Other references

An exhaustive list of references concerning LNT is available here.

6. Credits

Until version 2.9, TRAIAN has been written by Mihaela Sighireanu, Xavier Bouchoux, David Champelovier, Claude Chaudet, Nicolas Descoubes, Hubert Garavel, Yves Guerte, Marc Herbert, Rémi Hérilier, Alain Kaufmann, Frédéric Lang, Vincent Powazny, Wendelin Serwe, and Bruno Vivien. Acknowledgements are also due to Fabrice Baray, Estelle Dumas, Radu Mateescu, Gwen Salaün, Damien Thivolle, and Sai-Srikar Kasi for their valuable remarks about TRAIAN.

Since version 3.0, TRAIAN is being developed by Hubert Garavel, Frédéric Lang, and Wendelin Serwe.

Back to the VASY Home Page