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) have been written in LNT.
2. The TRAIAN compiler
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.
4. Download the latest version of TRAIAN
TRAIAN is not part of the CADP toolbox and must be installed separately.
The current version of the TRAIAN compiler is version 3.15 released on September 29, 2024.
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)
TRAIAN is available for download from the VASY FTP server:
Please contact cadp@inria.fr for any question or comment about TRAIAN.
5. Related publications
About TRAIAN 3
LNT User's Manual (Version 3.15)
Mihaela Sighireanu (with updates by Alban Catry, David Champelovier, Hubert Garavel, Frédéric Lang, Guillaume Schaeffer, Wendelin Serwe, and Jan Stöcker)
September 2024, 88 pages.
From LOTOS to LNT
Hubert Garavel, Frédéric Lang, and Wendelin Serwe
October 2017, 29 pages.
About TRAIAN 2
Other references
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
