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

THE CADP NEWSLETTER - Nr. 15
January 27, 2023

This newsletter is available from the CADP Home page.

Contents

1. Progress of CADP during year 2022

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

In parallel to the development of CADP, significant effort has been devoted to a complete rewrite of the TRAIAN compiler used to build most CADP compilers and translators. Three versions (3.6, 3.7, and 3.8) of TRAIAN have been released in 2022. Our project is to progressively unify LNT and the LOTOS NT language supported by TRAIAN to eventually include in CADP a future version of TRAIAN, which will provide a native compiler front-end for LNT.

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 a bug fix in the BCG_READ manual page, the vocabulary and option names for BCG_CMP and BCG_MIN was clarified as follows. The "-divbranching" option is now documented as "divergence-preserving branching bisimulation" rather than divergence-sensitive branching bisimulation". The existing option "-sharp" was renamed to "-divsharp" ("divergence-preserving sharp bisimulation"), whereas "-sharp" now implements the variant of sharp bisimulation that does not preserve divergences. A similar change was done in SVL, which now distinguishes between "sharp reduction", "divsharp reduction", "sharp comparison", and "divsharp comparison".

For details, see HISTORY entries: #2792 #2804 #2806

DEMOS

In addition to a bug fix in demo 09, the demos 04, 26, 27, and 33 have been enhanced and translated from LOTOS to LNT. Also, the LOTOS code of demo 24 was shortened by 21%, still preserving its semantics, and the LNT code of demo 30 was made more readable.

For details, see HISTORY entries: #2763 #2765 #2790 #2813 #2814 #2818 #2830 #2832 #2846 #2848

LNT

The LNT language has continued its evolution to become a better language and to achieve convergence with the LOTOS NT language supported by the TRAIAN compiler. In 2022, the following changes have been brought to LNT:

  • An LNT type with the "!external" pragma may now have an empty body.
  • An LNT function with the "!external" pragma may now have an empty (rather than "null") body.
  • Binary constants must start with "0b" rather than "0B", as the letter "B" could be mistaken for an eight.
  • Octal constants must start with "0o" rather than "0O", as the letter "O" could be mistaken for a zero.
  • Similarly, hexadecimal constants must start with "0x" rather than "0X".
  • The mantissa of a real number may no longer start with a dot, e.g., ".01" should be written "0.01".
  • The mantissa of a real number may no longer end with a dot, e.g., "12." should be written "12.0".
  • Non-null numbers may no longer start with a zero, e.g., "03.4" should be written "3.4" (but "0.8e5" is still valid).
  • Two new type pragmas "!pointer" and "!nopointer" have been introduced.
  • LNT types isomorphic to natural numbers may no longer have a "!pointer" pragma.
  • "while" and "for" loops may now have an optional label that can be used in "break" statements.
  • The use of the "eval" keyword is now optional (and discouraged) in three situations out of four.
  • Any function whose name is a special identifier (e.g., +, *, etc.) must now return a result and have no "out", "out var", or "in out" parameter.
  • Function pragmas must carry valid C identifiers and may no longer contain "%s" (identifier name substitution), nor "%d", "%i", "%u", etc. (positional number substitution).
  • LNT module identifiers must be identical to their respective file names; the comparison is now case-sensitive (formerly, it was case-insensitive).
  • The "with update" clause, which was duplicating "with set", has been suppressed.
  • The "!" symbol is no longer allowed in output offers, e.g., "PRINT (!X)" must now be written "PRINT (X)".
  • "{}" cannot anymore be used as the name of a non-constructor function.
  • "{}" cannot anymore be used as the name of a constructor with parameters.
  • Set types are now equipped with a predefined operation "subset" that checks set inclusion.

The LNT2LOTOS Reference Manual and the LNT tools have been updated to document and implement these changes. 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 2022-LNT-BIN-HEX-OCT <directory>
   upc 2022-LNT-REALS <directory>
   upc 2022-LNT-LEADING-ZEROS <directory>
   upc 2022-LNT-EVAL <directory>
   upc 2022-LNT-MODULE <directory>
   upc 2022-LNT-UPDATE <directory>
   upc 2022-LNT-EXCLAIM <directory>
   upc 2022-LNT-NONE <directory>

A new tool named LNT_MERGE was added, which takes as input an LNT program, possibly made up of several LNT modules, and produces as output an LNT program that consists in one single LNT module. The ".fnt" and ".tnt" files, if any, are also merged. This tool is useful to package multi-module LNT programs into non-regression test suites.

In addition to seven bug fixes (one in LNT2LOTOS, one in LNT_DEPEND, one in UPC, and four in LNT_MERGE), the LNT2LOTOS translator has been enhanced as follows:

  • It checks that the value given for the "!bits" pragma is greater than zero.
  • It checks that the value given for the "!card" pragma is greater than one.
  • It generates LOTOS code that no longer causes GCC warnings for certain exhaustive LNT patterns.
  • It warns about dead code located after an infinite "loop" without "break" clause in LNT processes.
  • It warns about "in var" process parameters assigned before used in an infinite "loop" without "break".
  • It checks that, in "C:xxx" pragmas, all identifiers "xxx" are distinct and are not C keywords.
  • It checks that, in "LOTOS:xxx" pragmas, all identifiers "xxx" are distinct and are not LOTOS keywords.
  • It now provides source-code line numbers for warnings about deprecated LNT syntactic features.
  • It warns about LNT functions declared with both !external and !implementedby "LOTOS:xxx" pragmas, since identifier "xxx" is (temporarily) ignored.
  • It no longer generates LOTOS code for such LNT functions.
  • It (temporarily) forbids such LNT functions that have "out" or "in out" parameters.
  • It (temporarily) forbids such LNT functions that have pre- ("require") or post-conditions ("ensure").

For details, see HISTORY entries: #2764 #2766 #2768 #2769 #2770 #2771 #2772 #2774 #2786 #2787 #2788 #2789 #2793 #2795 #2802 #2803 #2807 #2809 #2811 #2815 #2816 #2817 #2819 #2820 #2821 #2822 #2823 #2824 #2826 #2827 #2828 #2834 #2835 #2837 #2838 #2841 #2843 #2850

LOTOS

In addition to a bug fix in the X_BIT library causing warnings from CAESAR.ADT, the CAESAR and CAESAR.ADT compilers for LOTOS have been enhanced as follows.

It is no longer allowed in special comments to use "bool", "false", or "true" as names of C external functions.

The C code generated by CAESAR was modified to reduce the number of warnings generated by the Sparse code checker.

The C code generated by CAESAR.ADT was modified to reduce the number of warnings generated by the Splint code checker.

The C code generated by CAESAR.ADT for LOTOS operations whose names contain the "\" (backslash) character no longer causes warnings from Gcc.

For details, see HISTORY entries: #2778 #2780 #2781 #2782 #2791

MCL

In addition to a bug fix regarding memory allocation in the EVALUATOR model checker, the CAESAR_SOLVE_1 Boolean resolution library was enriched with two new on-the-fly algorithms, named A10 and A11. These algorithms are based on a depth-first search of the dependency graph between Boolean variables. Algorithm A10 (resp. A11) is specialized for solving disjunctive (resp. conjunctive) equation blocks of minimal (resp. maximal) fixed point sign, in the case where a single invocation of the algorithm is requested on the block. Algorithms A10 and A11 consume less memory than their counterparts A3 and A4, which allow multiple invocations on the same equation block.

For details, see HISTORY entries: #2842 #2849

MISC

The source code of all the CADP tools, as well as the C code generated by these tools, have been updated to systematically use the "bool" type and the "false" and "true" constants defined in "stdbool.h".

All the CADP tools are now built using the latest version of the SYNTAX compiler generator and the most recent version of TRAIAN. Also, the garbage collector invoked by CAESAR was upgraded from version 7.6.4 to version 8.2.2.

The EUCALYPTUS graphical user interface, when operating on an LNT file, now pre-selects the MAIN process by default, hereby saving clicks from the user.

The style files for GNOME text editors (Gedit, Pluma, etc.) have been modified to work, not only with Gtk3, but also Gtk4 (more recent) and Gtk5 (forthcoming).

Style files intended to the Sublime Text editor have been added for the various languages and file formats supported by CADP.

The documentation of CADP was updated and enhanced at various places.

For details, see HISTORY entries: #2777 #2779 #2794 #2796 #2833 #2836 #2839

NUPN

The CAESAR.BDD tool has been upgraded to version 3.1.0 of CUDD. The tool has been extended with four new options: "-arcs-pt", "-arcs-tp", "-signature", and "-signature-multiple"; the two latter options display a NUPN checksum that is invariant by any permutation of places, transitions, and/or units.

The existing options "-place-order" and "-unit-order" have been enhanced to be faster and produce shorter, yet more discriminative results. The "-concurrent-places" of CAESAR.BDD was also made faster.

For details, see HISTORY entries: #2767 #2773 #2775 #2783 #2784 #2812 #2845

PORTS

In addition to six bug fixes (three on Linux, two on Windows, one on macOS), the CADP tools received specific enhancements targeted to various processors and operating systems.

Concerning macOS: CADP was ported to macOS 13 "Ventura" and support was added for running CADP on Apple machines with an ARM processor.

Concerning SunOS: Support for the "sol86" architecture (32-bit executables for Solaris and OpenIndiana) has been discontinued, since the "sol64" architecture (64-bit executable) is deemed to be sufficient.

Concerning Windows: The instructions for installing CADP on Windows/Cygwin have been updated and simplified, removing dependencies on old-fashioned tools, such as "bc" and "ed". Support for recent versions of GNU-tar (e.g., version 1.34) was added. The EUCALYPTUS graphical user interface was modified to avoid issues when launching the Cygwin version of EMACS. Finally, preliminary changes to support 64-bit Windows executables have been undertaken.

For details, see HISTORY entries: #2776 #2785 #2797 #2798 #2799 #2800 #2801 #2805 #2808 #2810 #2825 #2829 #2831 #2840 #2844 #2847

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