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

THE CADP NEWSLETTER - Nr. 19
January 30, 2026

This newsletter is available from the CADP Home page.

Contents

1. Progress of CADP during year 2025

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 2025, the development of CADP has steadily progressed. Following the monthly rolling-release model established in 2013, twelve versions of CADP have been released in 2025. From version 2025-a to version 2025-l, 48 bugs have been fixed and 141 improvements have been brought.

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

Besides a minor bug fix for BCG_CMP on Windows, BCG_MIN and BCG_CMP now provide SVL with detailed information about the branching factor when these tools are halted by the operating system due to memory exhaustion.

The BCG tools, their code libraries, and their related tools have been updated to comply with the latest revision of the C language (i.e., the C23 standard published in October 2024). After these changes, all the code compiles without warning using recent C compilers. Precisely:

  • New-style prototypes have been added in all definitions of functions and functional types. The "bcg_read" and "bcg_write" manual pages have been updated to document these prototypes.
  • The code of CADP was simplified by eliminating the macro-definitions BCG_ARG_n() intended for old C compilers that did not support function prototypes. The include file "bcg_prototype.h" defining these macros is now deprecated.
  • The BCG_LIB tool was modified to generate C code function prototypes and without BCG_ARG_n() macros.

For details, see HISTORY entries: #3088 #3125 #3127 #3229

DEMOS

The two versions of the alternating-bit protocol, demo_01 and demo_02, have been merged into a single one. Demo_01 was archived, after moving its test-generation features to demo_02. Then, demo_02, which was the last CADP demo expressed in LOTOS, was translated to LNT.

Moreover, all demos have been revised in 2025 to follow the evolution of CADP languages and tools. In addition to mere syntax updates, one can report the following changes:

  • The demo_32 and demo_38 have been reorganized to take advantage of LNT virtual types.
  • Many demos have been simplified using the incrementation/decrementation operations recently introduced in LNT.
  • Many demos have been shortened by removing useless definitions of channels and functions, as well as useless "of" and "with" clauses.
  • Many demos have been simplified using the new high-level macro-definitions of the MCL standard library.
  • Many demos have been updated to use the "abstraction" operator of SVL.

Finally, all demos have been ported to C23 and additional documentation was provided for demo_04 and demo_15.

For details, see HISTORY entries: #3156 #3163 #3165 #3167 #3193 #3223 #3231 #3236 #3259 #3261

EXP

A segmentation-fault issue in EXP2C was fixed, which could arise with networks of automata containing hundreds of synchronization vectors. Also, the performance of EXP2C was significantly enhanced for composition expressions containing priority operators: the CPU time is now quadratic (rather than cubic) in the number of labels. For instance, on a network with 10,000+ distinct labels, EXP2C did not finish within more than an hour, but now terminates in 20 seconds.

For details, see HISTORY entries: #3121 #3253

LNT

In 2025, the unification of LNT and LOTOS NT was achieved, with the removal of all references to LOTOS NT in tools and documentation.

The LNT language was enhanced in many respects:

  • The ".." keyword (used in the definition of range and array types) was deprecated and replaced by the "..." keyword (used in lists and sets).

  • The former notation "!?X" for "in out" parameters was deprecated and replaced by a simpler notation "X?".

  • The syntax of LNT was made stricter, so as to ban ambiguous combinations of prefix unary operators and postfix notations, such as type conversions ("V of T"), field selections ("V.X"), field updates ("V.{X -> ...}"), and array accesses ("V1 [V2]").

  • Two new instructions "+=" and "-=" for incrementing and decrementing variables or array elements have been added. They work not only for numeric types (NAT, INT, and REAL), but also for any type with binary functions named "+" or "-", possibly raising exceptions.

  • A new iterative construct "for ... until ... by ... loop [... in] ... end loop" was introduced in both LNT functions and processes. This construct, which exists in two forms (breakable and unbreakable), is useful to enumerate the domain of enumerated types and range types without raising overflow exceptions (as it often happens with the "for ... while" loop).

  • Similar to the concept of virtual functions introduced in December 2024, LNT was enriched with virtual processes, virtual types, and virtual channels (all defined using the "!virtual" pragma). This enables one to specify generic LNT modules parameterized by types, functions, processes, and/or channels.

  • A new pragma "!library" was introduced, which can be either global to an LNT module, or local to some of its definitions. This pragma suppresses the warnings emitted by TRAIAN about functions and processes never called and/or types and channels never employed.

  • It is now possible to attach "!implementedby" pragmas to "with get" and "with set" clauses, so as to fix the names of the corresponding selector and updater functions.

Additionally, the predefined libraries of LNT have been significantly extended to increase user-friendliness and compatibility between TRAIAN and LNT2LOTOS:

  • The LNT_V1 library was enriched with 60 additional functions.
  • The BIT library was enriched with 7 additional functions.
  • The OCTET library was enriched with 2 additional functions.
  • "with min" and "with max" predefined functions are now available for all LNT types (constructor types, arrays, ranges, predicate types, lists, sorted lists, and sets).
  • "with inf" and "with sup" predefined functions are now available for LNT lists, sorted lists, and sets.
  • "with +" and "with -" predefined functions are now available for LNT range types.

The above changes (together with many other enhancements and simplifications) have been implemented in both TRAIAN and LNT2LOTOS. The editor style files have been updated accordingly. Also, the semantic checks performed by TRAIAN have been made more stringent:

  • TRAIAN now checks that module pragmas (other than "!version") appear at the beginning of each module.
  • The "!external" or "!virtual" pragmas attached to "with" functions are now rejected.
  • Data-flow analysis for array assignments is now more precise (1 new warning).
  • Irrelevant pre-conditions ("require" clauses) are now detected (6 new warnings).
  • Irrelevant post-conditions ("ensure" clauses) are now detected (9 new warnings).
  • The "return" instructions located in dead code are now verified.
  • Redundant "access" clauses in "trap" statements are now detected.
  • False conditions in "case" patterns are now detected.
  • False conditions and true conditions in "for" and "while" loops are now detected (1 new warning).
  • Event parameters (of LNT functions and processes) that are never accessed are now detected (2 new warnings).
  • "in", "out", and "in out" value parameters (of LNT functions and processes) that are never used or assigned are now detected (3 new warnings).
  • Many checks have been introduced for virtual functions, processes, types, and channels (25 new warning/error messages).
  • Types and channels defined but never employed are now detected (2 new warnings).
  • Functions and processes defined but never called are now detected (7 new warnings).
  • Useless "with get" and "with set" clauses are now detected (4 new warnings).
  • The C and LOTOS identifiers specified in "!implementedby" pragmas are now checked thoroughly.

The LNT documentation was updated accordingly and the LNT2LOTOS Reference Manual was enriched with 14 pages of examples taken from courses and exams given at ENSIMAG and Universite Grenoble Alpes. The CADP demos were modified to take advantage of these new features and compile without warnings.

The generation of LOTOS code by LNT2LOTOS improved in many ways:

  • Functions with only "in" parameters and no return type are no longer rejected.
  • "trap" instructions are no longer rejected, but partially implemented.
  • A wider class of LNT (n-ary) "par" instructions is now translated to LOTOS.
  • LNT module names identical to a LOTOS keyword are now accepted.
  • The LOTOS code generated for LNT exceptions was greatly simplified.
  • Functions "ord" and "val" are implemented more efficiently (complexity reduced from quadratic to linear).
  • LNT2LOTOS now resolves overloaded constants or nullary functions used in communication events.
  • LNT2LOTOS now resolves ellipses ("...") in event parameter lists of processes not defined in the current module.
  • LNT2LOTOS was aligned with TRAIAN for signed numeric constants and nullary functions returning array values.
  • The compatibility between the ".fnt" / ".tnt" files used by LNT2LOTOS and those used by TRAIAN increased significantly.
  • Both TRAIAN and LNT2LOTOS now have a "-main" option to determine the entry process to be used in a given LNT program.

The generation of C code by TRAIAN also improved:

  • The C code implementing the main process of an LNT program was simplified.
  • The INTER() and UNION() functions for LNT sets are now more memory-efficient.
  • The DELETE() and REMOVE() functions for LNT lists, sorted lists, and sets are more memory-efficient.
  • To be aligned with the conventions of LNT2LOTOS, the C code generated by TRAIAN for LNT functions having event parameters now places these parameters at the beginning of the list.

Additionally, 32 bugs have been fixed (16 in LNT2LOTOS, 10 in TRAIAN, two in both LNT2LOTOS and TRAIAN, one in LNT_MERGE, two in the data-type libraries, and one in the documentation).

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 2025-LNT-UNTIL <directory>
   upc 2025-LNT-DOT-DOT <directory>
   upc 2025-LNT-EXCLAIM-QUERY <directory>
   upc 2025-LNT-C-NAMES <directory>

For details, see HISTORY entries: #3089 #3091 #3093 #3094 #3095 #3096 #3097 #3099 #3103 #3105 #3107 #3108 #3109 #3111 #3113 #3115 #3116 #3118 #3119 #3122 #3123 #3124 #3126 #3128 #3129 #3131 #3133 #3135 #3140 #3145 #3147 #3148 #3150 #3151 #3152 #3153 #3154 #3155 #3157 #3159 #3160 #3161 #3162 #3164 #3166 #3168 #3169 #3170 #3173 #3175 #3178 #3179 #3181 #3182 #3185 #3187 #3190 #3192 #3195 #3196 #3198 #3199 #3200 #3201 #3202 #3203 #3204 #3205 #3206 #3207 #3208 #3209 #3210 #3211 #3212 #3213 #3215 #3216 #3217 #3218 #3220 #3221 #3222 #3224 #3225 #3226 #3227 #3232 #3233 #3234 #3235 #3237 #3238 #3240 #3241 #3242 #3243 #3244 #3246 #3248 #3249 #3250 #3251 #3252 #3255 #3257 #3258 #3260 #3262 #3264 #3265 #3267 #3271 #3272 #3273 #3274 #3275

MCL

The XTL_EXPAND preprocessor, common to the MCL and XTL languages, now supports single-line comments beginning with "--", in addition to the already supported multi-line comments delimited by "(*" and "*)".

The MCL_EXPAND preprocessor now reports data variables defined but not used in MCL formulas. Previously, such variables were reported later, in the generated C code, through cryptic warnings of the C compiler.

MCL_EXPAND now optimizes state formulas to reduce their size before translating them to the HMLR (Hennessy-Milner Logic with Recursion) intermediate form. For conjunctions of temporal formulas, these optimizations substantially improve the performance (verification time and memory consumption) of EVALUATOR. On 104 MCL V3 formulas concerned by these optimizations, the time needed to evaluate these formulas decreased by 37.5%. On 52 MCL-V4 formulas concerned by these optimizations, this time decreased by 12.2%.

Two bugs have been fixed in the "-bes" option of EVALUATOR, which caused memory faults when writing BESs containing multiple equation blocks or generated huge ".bes" files for MCL V4 formulas containing certain classes of fixpoints.

To simplify the CADP toolbox, the three model checkers EVALUATOR 3, EVALUATOR 4, and EVALUATOR 5 have been merged into a single one, EVALUATOR.

The source code of CADP model-checking tools (EVALUATOR, MCL_EXPAND, XTL_EXPAND), as well as the C code they produce, was ported to C23 by adding new-style function prototypes and modifying character constants.

The "standard.mcl" library of the MCL formula language was significantly improved by renaming two existing macro-definitions, enhancing two other ones, and introducing eight macro-definitions of common usage (DEADLOCK, NO_DEADLOCK, LIVELOCK, NO_LIVELOCK, POSSIBLE, WITHOUT_1_INEVITABLE_2, AFTER_1_WITHOUT_2_INEVITABLE_3, and AFTER_1_ONLY_2_INEVITABLE_3) that remove the need for writing lower-level mu-calculus formulas.

For details, see HISTORY entries: #3087 #3101 #3136 #3141 #3143 #3144 #3146 #3186 #3245 #3247 #3254 #3263 #3266 #3269

MISC

The following enhancements have been brought:

  • In all CADP tools having an option "-root", this option was renamed to "-main".
  • The windows of the EUCALYPTUS graphical user interface can now be resized freely.
  • The SYNTAX compiler generator used to build most CADP compilers was upgraded from version 2023 to version 2025.
  • A lexical bug was fixed in the scanner of CAESAR and CAESAR.ADT, which rejected LOTOS identifiers starting with a digit and containing the letter "l" or "L".
  • In addition to a bug fix in TGV, the command-line options of TGV were made more user-friendly. The "-csg" option was renamed to "-all". The former option "-output" was deprecated and replaced by an additional file name.
  • In the editor style files provided by CADP, the support for Sublime Text was improved and right arrows are displayed in a visually better way with LaTeX listings.

For details, see HISTORY entries: #3092 #3098 #3100 #3117 #3120 #3142 #3171 #3174 #3176 #3197 #3219 #3230

OPEN/CAESAR

The OPEN/CAESAR programming interfaces have been refined at various points:

  • In "caesar_graph", a new type CAESAR_TYPE_ITERATE_FUNCTION was introduced and used in the profile of function CAESAR_ITERATE_STATE().

  • In "caesar_cache_1": two new types CAESAR_TYPE_ORDER_FUNCTOR_CACHE_1 and CAESAR_TYPE_SUBCACHE_FUNCTOR_CACHE_1 were introduced and used in the profile of function CAESAR_CREATE_CACHE_1(), which also uses the types CAESAR_TYPE_SIZE_FUNCTION_CACHE_1 and CAESAR_TYPE_PERCENTAGE_FUNCTION_CACHE_1 at present.

  • In "caesar_solve_1": four new types CAESAR_TYPE_ITERATE_DIAGNOSTIC_FUNCTION_SOLVE_1, CAESAR_TYPE_ITERATE_FUNCTION_SOLVE_1, CAESAR_TYPE_ITERATE_STABLE_FUNCTION_SOLVE_1, and CAESAR_TYPE_LOOP_FUNCTION_SOLVE_1 have been introduced and used in the profiles of functions CAESAR_CREATE_SOLVE_1(), CAESAR_ITERATE_DIAGNOSTIC_SOLVE_1(), and CAESAR_ITERATE_STABLE_VARIABLE_SOLVE_1().

  • In "caesar_solve_2": two new types CAESAR_TYPE_ITERATE_FUNCTION_SOLVE_2 and CAESAR_TYPE_LOOP_FUNCTION_SOLVE_2 have been introduced and used in the profile of function CAESAR_CREATE_SOLVE_2().

  • In "caesar_table_1": the deprecated value CAESAR_EMPTY_AREA_1() for the formal parameter CAESAR_BASE_AREA of function CAESAR_CREATE_TABLE_1() was removed and function CAESAR_PRINT_TABLE_1(), when invoked with format 0, now displays the arity (2 or 3) of the hash function associated with the table.

Moreover, OPEN/CAESAR, EXEC/CAESAR, the OPEN/CAESAR-compliant compilers (BCG_OPEN, CAESAR, EXP.OPEN, and SEQ.OPEN), the OPEN/CAESAR application tools (e.g., CUNCTATOR, DETERMINATOR, XSIMULATOR, etc.), and their documentation have been updated to comply with C23 and compile without warnings using recent C compilers. Precisely:

  • New-style prototypes have been added in all definitions of functions and functional types.
  • All macro-definitions CAESAR_ARG_n() have been eliminated. The include file "caesar_prototype.h" defining these macros is now deprecated.
  • The former macros CAESAR_WITH_OLD_PROTOTYPES, CAESAR_WITH_NEW_PROTOTYPES, and CAESAR_PROMOTE_TO_INT() have been removed.

For details, see HISTORY entries: #3130 #3132 #3134 #3137 #3138 #3183 #3184 #3189 #3191 #3214

PORTS

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

  • The "cadp_edit" script shell was modified to take into account the fact that "wordpad.exe" and "write.exe" are no longer present on Windows 11.
  • The "cadp_more" script was modified to follow the new behaviour of the "more" and "less" commands on recent versions of Linux.
  • The "cadp_temporary" script was modified to continue working with the recent versions of "mktemp" on Windows/Cygwin.
  • The "cadp_cc" script and the two include files "caesar_area_1.h" and "caesar_system.h" were modified to work with Clang on Solaris/SunOS.

The CADP toolset can now be downloaded (manually or using INSTALLATOR) with HTTP or HTTPS, in addition to FTP, which was the only possibility available so far.

Also, all the remaining tools of CADP (e.g., BES_SOLVE, PBG, etc.) were upgraded to C23 and now compile without warnings with recent C compilers. This required many changes in the source code of these tools, in their include files distributed as part of CADP, and in the C code generated by these tools (e.g., CAESAR, CAESAR.ADT, XTL, etc.).

For details, see HISTORY entries: #3090 #3102 #3112 #3114 #3139 #3149 #3158 #3172 #3188 #3194 #3239

SVL

The syntax of the SVL language was enhanced in three ways:

  • The "|=" operator was extended to evaluate properties stored in ".mcl" and ".xtl" files. The "verify" operator, less intuitive, is now deprecated.
  • Three new keywords "end abstraction", "end generation", and "end reduction" have been introduced, which provide a structured alternative to parentheses.
  • The language was simplified, following the unification of "evalutor3", "evaluator4", and "evaluator5" in one single tool "evaluator".

In addition to three bug fixes, the SVL compiler was improved as follows:

  • SVL scripts may now be run as full-fledged programs from the command line, like any other shell script.
  • It distinguishes more clearly between errors and warnings reported by the various CADP commands invoked from SVL scripts.
  • It directly displays the messages emitted by the last CADP command that failed (as well as storing these messages in a log file).

For details, see HISTORY entries: #3104 #3106 #3110 #3177 #3180 #3228 #3256 #3268 #3270

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