This newsletter is available from the CADP Home page.
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.
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
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
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:
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:
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
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
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
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
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
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
We are extremely grateful to the following scientists, who provided us with valuable feedback and advice about the use of CADP: