Construction and Analysis of Distributed Processes
Software Tools for Designing Reliable Protocols and Systems

THE CADP NEWSLETTER - Nr. 18
February 7, 2025

This newsletter is available from the CADP Home page.

Contents

1. Progress of CADP during year 2024

This page summarizes the recent evolution of the CADP toolbox from the point of view of its community of users and software developers. Other results, including scientific advances, publications, applications of CADP to industrial problems, and new prototype tools built on top of CADP can be found in the yearly activity reports of the CONVECS team.

In 2024, the development of CADP has steadily progressed. Following the monthly rolling-release model established in 2013, twelve versions of CADP have been released in 2024. From version 2024-a to version 2024-l, 27 bugs have been fixed and 104 improvements have been brought (not counting here the bug fixes and improvements made for TRAIAN in parallel).

The diagram to the right gives the repartition of efforts between the various components of CADP. Effort was not measured in time but in the number of lines of the HISTORY file, based on the reasonable assumption that the more involved a change, the more lines needed to describe it.

2. Overview of main enhancements

This section summarizes the main enhancements in the various components of CADP. For more details, please refer to the CADP change list and to the HISTORY file provided in the CADP distribution.
BCG

In addition to bug fixes in the CAESAR_RANDOM library of OPEN/CAESAR and in the generation of throughput files by BCG_STEADY and BCG_TRANSIENT, the following enhancements have been brought:

  • The "-diag" option of BCG_CMP now invokes BISIMULATOR to produce much smaller diagnostics. BCG_CMP also received two new options "-bfs" and "-dfs", which are passed to BISIMULATOR to control how these diagnostics are generated.
  • BCG_STEADY and BCG_TRANSIENT now check check that, in their "parameter=value" options, all "parameter" names are pairwise distinct. In the throughput files generated by these tools, the columns of the second group are now sorted by alphabetic order of their labels, thus making the output deterministic for the user, who can now predict in which order the columns will appear.
  • CUNCTATOR received two new options "-thr" and "-append", similar to those of BCG_STEADY, which generate output compatible with BCG_STEADY, with results organized in columns rather than rows.
  • The BCG MONITOR graphical interface was revised in many ways. Its window was made more compact. Two new menus "File" and "View" have been added. The "Edit" menu was extended with "Zoom In", "Zoom Out", and "Normal Size" entries to increase, decrease, or reset font size. Keyboard shortcuts have been added. Finally, user settings concerning the BCG MONITOR are now automatically saved and reused for future executions.

For details, see HISTORY entries: #2966 #2968 #2996 #3003 #3007 #3008 #3022 #3029 #3031 #3076

DEMOS

In 2024, three demos have been added or fully revised:

  • The new demo_10 presents a large collection of parallel algorithms for mutual exclusion on shared-memory machines. These algorithms are described in LNT, their correctness is verified by model checking, and their performance is predicted using steady-state analysis (BCG_STEADY) or simulation (CUNCTATOR).
  • The new demo_15 presents the Erlangen mainframe, a multiprocessor system that combines challenging features: multiple waiting queues, priorities, failures/repairs, Markov-Modulated Poisson Processes, and multiway synchronizations. The performance of this system is analyzed using steady-state and transient analyses on parameterized Continuous-Time Markov Chains.
  • The former demo_40 of CADP was corrected, simplified, and translated to LNT, resulting in more readable specifications, still preserving strong bisimilarity between the LOTOS and LNT code.

Additionally, many CADP demos have been enhanced in various ways:

  • Their SVL scripts have been simplified.
  • To comply with the checks recently introduced in TRAIAN to detect LNT modules that are not self-contained, demos have been updated to add missing module imports and, if necessary, virtual LNT processes.
  • Whenever possible, each demo was enriched with a "doc" directory that contains publications related to this example.

For details, see HISTORY entries: #2984 #3015 #3019 #3027 #3032 #3033 #3067 #3074 #3082 #3083

LNT

The LNT language continued its evolution to become a better language and to achieve convergence between LNT and the LOTOS NT language supported by the TRAIAN compiler, which provides a compiler front-end for LNT and is also used to build most CADP compilers and translators.

A major step was achieved in October 2023 when TRAIAN became part of the CADP distribution. This effort was pursued in 2024, with four successive releases (3.13, 3.14, 3.15, and 3.16) of TRAIAN. In addition to 19 bug fixes, these releases enhanced TRAIAN with finer static and data-flow analyses. TRAIAN now emits more accurate and informative messages, as well as many new warnings and error messages that help to improve the quality of LNT models.

The LNT2LOTOS and TRAIAN compilers have been progressively aligned with each other, leading to changes in the definition of LNT:

  • The "select" keyword was renamed to "alt", as a tribute to Tony Hoare. The "select" keyword is now deprecated and will eventually disappear.
  • "library" directives for including LNT files are now supported by LNT2LOTOS.
  • The definition of synonym types, i.e., "type T2 is X:T1 end type" without a "where true" clause is now permitted in LNT.
  • Type pragmas of the form !implementedby "LOTOS:T" are now supported by LNT2LOTOS (but only if the LNT type is also named T).
  • Clauses "with nil" and "with cons" are now accepted in lists, sorted lists, and sets; if these clauses have attached pragmas, LNT2LOTOS takes them into account when generating LOTOS code.
  • Clauses "with diff" and "with minus" in sorted lists and sets are now handled identically by LNT2LOTOS and TRAIAN.
  • A new pragma !virtual allows to declare imported processes that are neither defined in the current module, nor in its transitively included modules.
  • Expressions of the form "V.{}" are now supported by LNT2LOTOS.
  • Patterns of the form "P where V" can now appear everywhere a pattern is accepted, and LNT2LOTOS implements a large subset of them.
  • Events of the form "E ()" are now supported by LNT2LOTOS.
  • Behaviours of the form "i where V", where V is a Boolean guard are now supported by LNT2LOTOS.
  • Empty module definitions are now syntactically accepted by LNT2LOTOS.
  • A predefined channel EXIT was introduced for LNT events that model exceptions. Such events should no longer be declared with a "raise" keyword and channel NONE.
  • The channel of the UNEXPECTED event is no longer NONE, but EXIT.
  • Channel definitions with the "raise" attribute are supported by LNT2LOTOS (but only effective, so far, for the predefined channel EXIT).
  • Events with "..." ellipses are now syntactically accepted by LNT2LOTOS, but not yet handled at the semantic level.
  • Calls to constructors, functions, and processes with named parameters are now syntactically accepted by LNT2LOTOS, but not yet handled at the semantic level.
  • "any" patterns not followed by a type identifier are now syntactically accepted by LNT2LOTOS, but not yet handled at the semantic level.
  • "trap" statements are now syntactically accepted by LNT2LOTOS, but not yet handled at the semantic level.
  • Ellipses "..." are now forbidden in field updates.
  • Clauses "with val" are now accepted only for enumerated and range types.
  • It is now forbidden to assign a "in" parameter X if "X.in" appears in an "ensure" clause.
  • In "ensure" clauses, the qualifiers "X.in" and "X.out" may now only be used if X is an "in out" parameter.
  • The ambiguity of expressions of the form "X [Y]" is now resolved using semantic information: either X is an array and Y an index, or X is a function and Y an event. The third case where X is a function returning an array and Y an index is no longer accepted and must be written either "(X) [Y]" or "X () [Y]".
  • "raise" statements with value parameters are now rejected by LNT2LOTOS at the syntactic level (as TRAIAN already did).
  • Deprecated "var" declarations combined with initializations are now rejected by LNT2LOTOS at the syntactic level.
  • Deprecated "case ... in var ... in ..." statements are now rejected by LNT2LOTOS at the syntactic level.

The tighter compatibility between TRAIAN and LNT2LOTOS, and the fact that TRAIAN is now systematically invoked before LNT2LOTOS, enabled simplifications and code factorization between the various tools for LNT:

  • 165 error messages and 23 warning messages formerly emitted by LNT2LOTOS have been suppressed, since they either were already present in TRAIAN or have been added to TRAIAN in 2024.
  • 18 error messages formerly emitted by LNT2LOTOS now display as (fatal or non-fatal) "limitations", to better indicate that the corresponding problems are not due to an incorrect LNT program, but to advanced features that LNT2LOTOS does not handle yet.
  • The removal of these static-semantics reduced by 10% the number of lines of code in LNT2LOTOS, making it noticeably faster on correct LNT programs.
  • The LNT_CHECK auxiliary shell script was removed from CADP, since TRAIAN makes it useless.
  • The LNT_DEPEND executable was also removed, since LNT module signatures and dependencies between modules are now computed by TRAIAN.
  • The LPP preprocessor was suppressed, since the translation to LOTOS of LNT constants (natural numbers, reals, characters, and strings) is now done by LNT2LOTOS instead of LPP.
  • Consequently, the "-lnt" option of LOTOS.OPEN, the "-pidlist" and "-notraian" options of LNT.OPEN, and the "-depend", "-pidlist", and "-traian" options of LNT2LOTOS have been removed.

Twelve bugs have been fixed in the various tools for LNT. New verifications and better error messages have been added to LNT_MERGE and LNT.OPEN. The following algorithmic enhancements have been brought to LNT2LOTOS:

  • The algorithm for inlining simple functions in the generated LOTOS code was revised, dividing by 15 the execution time of LNT2LOTOS on certain large examples.
  • LNT2LOTOS no longer generates dead LOTOS code when translating "B1; B2" if it detects that all the execution paths in B1 lead to deadlocks, infinite loops, breaks of an enclosing loop, or raises of events that are not trapped.
  • LNT2LOTOS no longer generates extra LOTOS code for checking that each event properly matches its channel, as such check is now done beforehand by TRAIAN.
  • LNT2LOTOS now generates modified C code not to raise the GCC 12 warnings about infinite recursion.

The progressive transformation of LNT2LOTOS into a back-end LOTOS code generator by suppressing many semantic checks already done by TRAIAN, together with the elimination of LNT_DEPEND and LPP, which performed preliminary passes on the LNT source code, led to significant speed improvement for the LNT tool chain. The time needed by LNT.OPEN to compile 13,500+ correct LNT programs was reduced from 25 hours down to 11 hours 40 minutes.

The LNT2LOTOS Reference Manual, the LNT tools, the EUCALYPTUS user interface, the editor style files for LNT, the CADP manual pages, many CADP demos, and the web sites for CADP and TRAIAN have been updated to implement and document these changes. In particular, a manual page for TRAIAN was added to CADP and there is now one single entry point gathering all information available about LNT.

The "upc" shell script was extended to ease the migration of LNT programs. These can be upgraded (automatically or semi-automatically) by invoking, in that order, the following commands: 

   upc 2024-LNT-SELECT <directory>
   upc 2024-LNT-EXIT <directory>
   upc 2024-LNT-MINUS <directory>

For details, see HISTORY entries: #2956 #2957 #2958 #2960 #2961 #2962 #2963 #2965 #2971 #2972 #2973 #2974 #2979 #2981 #2982 #2983 #2986 #2988 #2990 #2991 #2992 #2994 #2997 #2999 #3000 #3001 #3009 #3010 #3011 #3013 #3014 #3016 #3017 #3020 #3021 #3023 #3024 #3025 #3026 #3028 #3034 #3036 #3038 #3041 #3042 #3043 #3044 #3045 #3046 #3047 #3048 #3049 #3050 #3051 #3052 #3053 #3054 #3055 #3056 #3057 #3058 #3059 #3060 #3062 #3063 #3064 #3066 #3068 #3069 #3070 #3072 #3075 #3080 #3081

MCL

In addition to two bug fixes in the XTL compiler and its "radius.xtl" library, the XTL language was extended by adding "replace" functions for the predefined type "action" and for any external XTL type defined in C. These functions are useful in "for" loops to update the values of accumulator variables.

Also, the CADP distribution was reorganized by putting the predefined libraries of MCL and XTL into separate directories, and by progressively reducing the role of the EVALUATOR 3 model checker, which is superseded by EVALUATOR 4. From now on, EVALUATOR 3 is no longer invoked in the CADP demo examples but is kept to cross-check the results produced by EVALUATOR 4 on "data-less" formulas, which only manipulate strings and regular expressions.

For details, see HISTORY entries: #2985 #2993 #2995 #3035 #3061

MISC

In addition to bug fixes in FSP2LOTOS and CAESAR.INDENT, the following enhancements have been brought:

  • The format of error messages issued by FSP2LOTOS was aligned with that of LNT2LOTOS.
  • A new option "-depth N" was added to the GENERATOR tool so as to generate an LTS fragment containing all states whose distance from the initial state is at most N.

For details, see HISTORY entries: #2975 #2977 #2978 #2998 #3037

PORTS

Among many changes dictated by evolutions of operating systems and C compilers, one can mention the following ones:

  • The "mac64" version of CADP was ported to macOS 15 "Sequoia" and Xcode version 16.1. The documentation for installing CADP on macOS was updated and two spurious warnings of TST on macOS have been removed.
  • The "win64" version of CADP for Windows/Cygwin was subject to minor corrections in TST and CADP_ADJUST.
  • The "x64" version of CADP for Windows/WSL2, which had stopped working due to changes in WSL2 and/or the various Linux applications of the Microsoft Store was repaired. To do so, various scripts (INSTALLATOR, CADP_PATH, and TST) have been revised and the installation directives for CADP on Windows have been updated.
  • INSTALLATOR better detects the case where a user mistakenly launches a file "installator.shar" for an inappropriate machine architecture: preliminary checks are now made, which emit error messages to help the user understand the issue. Additionally, a color problem in INSTALLATOR's radiobuttons was fixed.
  • Style files for Visual Studio Code have been added for the various languages and file formats supported by CADP.
  • The style files for the Sublime Text editor have been enhanced to better support predefined types and case-insensitive languages.
  • The editor style files for MCL5 and SVL, and the EMACS style files for LNT have been updated to reflect the latest changes brought to these languages.
  • A long-term work was undertaken to upgrade the source code of CADP so that it compiles without warning using C24, the latest revision of the C language. As of April 2024, 15% of the CADP programs and code libraries had been upgraded. In this context, CAESAR.ADT was modified to generate C code with C24-compliant prototypes for function definitions.

For details, see HISTORY entries: #2964 #2967 #2970 #2976 #2980 #2987 #2989 #3012 #3030 #3039 #3040 #3077 #3078 #3073 #3079 #3084 #3085 #3086

SVL

Besides two bug fixes in the "-network" option of EXP.OPEN when used to produce NUPN files, and in the expansion by SVL of "leaf" and "root leaf" reduction operators, the compositional verification tools of CADP have been enhanced as follows:

  • The SVL language was extended to support "condensed" priority behaviours of the form "prio L1, ..., Ln in ..." or "prio all but L1, ..., Ln in ...".
  • The SVL language now permits to control the generation of diagnostics by passing options to BCG_CMP, namey "comparison using M ..." where M is either "bfs" or "dfs".
  • A memory leak that occurred when SVL called EXP2C with the "-smart" option was removed, significantly improving the time and memory performances of EXP2C.
  • When a "cut" operator is applied to an explicit LTS in the context of a stochastic comparison, SVL automatically converts the result to a BCG file and no longer displays a warning.
  • SVL emits clearer error messages when file extensions are not specified.
  • To provide for concise SVL scripts, the library of predefined SVL functions has been enriched with a new function SVL_ECHO. Also, the two library functions SVL_RECORD_FOR_CLEAN and SVL_RECORD_FOR_SWEEP now handle multiple arguments.

For details, see HISTORY entries: #2959 #2969 #3002 #3004 #3005 #3006 #3018 #3065 #3071

3. Acknowledgements

We are extremely grateful to the following scientists, who provided us with valuable feedback and advice about the use of CADP:

and all other persons we may forget.

Back to the CADP Home Page