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

THE CADP NEWSLETTER - Nr. 17
February 4, 2024

This newsletter is available from the CADP Home page.

Contents

1. Progress of CADP during year 2023

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

Since 2016, 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. Our project is to progressively unify LNT and the LOTOS NT language supported by TRAIAN. Four versions (3.9, 3.10, 3.11, and 3.12) of TRAIAN have been released in 2023. The two latter versions have been included in CADP to provide a 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.
BES

In 2023, a data base of 10,500+ Boolean Equation Systems (BESs) has been prepared, on which the CAESAR_SOLVE_1 library and the BES_SOLVE tool have been tested systematically. This effort led to six bug fixes: the "unique" and "mode N" pragmas contained in BES files were ignored; the "-parallel" option of BES_SOLVE could fail if a non-writable BES_SOLVE binary was already present on some remote machine; the resolution algorithm A8 could stop with a "memory shortage" error; the resolution algorithm A9 could halt with a segmentation fault; the resolution algorithms A8, A10, and A11 could generate incorrect diagnostics.

Also, the memory used for resolution was reduced by a factor between 10% and 50% by better dimensioning the internal table that stores Boolean variables.

For details, see HISTORY entries: #2870 #2871 #2872 #2886 #2904 #2911 #2913

DEMOS

In 2023, the demos of CADP evolved as follows:

  • The memory efficiency of demo 16 was enhanced by adding a "!card" type pragma.
  • The LOTOS code of demos 23 and 25 was shortened, without loss of functionality, by 42% (from 2090 down to 1208 non-blank lines) and 27% (from 767 down to 560 non-blank lines), respectively.
  • Demos 23, 24, and 25 have been translated from LOTOS to LNT, still preserving strong bisimilarity.
  • The introduction of the TRAIAN compiler in CADP (see below) revealed hidden mistakes in demos 11, 26, and 38, which have been corrected. Also, demos 04, 08, and 32 have been enhanced to get rid of (relevant) warnings emitted by TRAIAN, leading to more readable code.

For details, see HISTORY entries: #2889 #2921 #2922 #2923 #2924 #2940 #2950 #2952

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. A major step was achieved in 2023 when version 3.11 of TRAIAN (and later, version 3.12) was integrated in the CADP distribution. Such integration brings two major benefits for the users of LNT:

  • TRAIAN provides a full-fledged, native compiler front-end for LNT. TRAIAN is stricter than LNT2LOTOS, as it detects errors that LNT2LOTOS cannot catch because of its "lightweight" translation approach. For instance, TRAIAN does complete type checking, whereas LNT2LOTOS does not check types, simply generating LOTOS code and deferring type-checking duties to the LOTOS compilers CAESAR.ADT and CAESAR.

  • The error and warning messages emitted by TRAIAN are easier to understand, since they refer to the LNT source code, while many messages of LNT2LOTOS refer to the generated LOTOS code.

The integration of TRAIAN in CADP is done by the LNT.OPEN shell script, which (unless it is called with the new "-notraian" option) invokes TRAIAN before invoking LNT2LOTOS. LNT.OPEN no longer invokes LNT_CHECK as the warning messages of TRAIAN about incomplete "case" statements are more informative than those of LNT_CHECK. If TRAIAN detects a fatal error, then LNT.OPEN stops and does not invoke LNT2LOTOS.

In 2023, the following changes have been brought to the LNT language:

  • The syntax of LNT patterns was restricted: it is no longer allowed to write two (or more) consecutive unary operators without using parentheses.
  • It is now forbidden to define constructors named "{}".
  • "sorted set" types have been removed from LNT; set types should be used instead.
  • If a type T2 defined by its constructors has a "with F" clause (where F is an equality relation, an order relation, or the STRING function), then each type T1 used by (at least) one parameter of a constructor of T2 must also have an F function, which is defined explicitly or implicitly (i.e., as a "with F" clause in type T1).
  • If a type T2 is defined as a list, sorted list, or set of another type T1, then the latter type must have appropriate equality and/or order relations, as specified in the TRAIAN scheme files.
  • "with =" clauses are now allowed for all LNT types if one wishes equality functions noted "=" rather than "==".
  • "with" clauses defining equality and (lexicographic) order relations are now permitted for set types, as well as all other LNT types.
  • The "with LENGTH" clause of set types must now be noted "with CARD".
  • "with CARD" clauses are now forbidden for all LNT types but sets, as the meaning formerly given to these CARD functions was counter-intuitive.
  • "with NIL" and "with CONS" clauses are now forbidden for all LNT types.
  • "with INSERT" clauses are new forbidden for all LNT types but lists, sorted lists, and sets.
  • Each function declared in the "with" clause of a non-external type may now have an "!external" pragma.
  • Each function declared in the "with" clause of an external type is now considered as external and may have an "!implementedby" pragma.

The LNT_V1 library of predefined LNT types was also modified to further align LNT2LOTOS and TRAIAN:

  • The constructor ZERO of type NAT is now noted "0".
  • The function IsEmpty: String → Bool was renamed to Empty.
  • The function nth: String, Nat → Char was renamed to Element.
  • The function NatToInt: Nat → Int was renamed to Int.
  • The function IntToNat: Int → Nat was renamed to Nat.
  • Eighteen new functions have been added to the library:
              Char : Nat → Char
              Char : String → Char
              First : → Bool
              First : → Char
              Int : Real → Int
              Int : String → Int
              Last : → Bool
              Last : → Char
              Nat : Char → Nat
              Nat : String → Nat
              Pred: Bool → Bool
              Pred: Char → Char
              Pred: Nat → Nat
              Real : Int → Real
              Real : Nat → Real
              String : Bool → String
              Succ: Bool → Bool
              Succ: Char → Char

    The LNT2LOTOS Reference Manual and the LNT tools have been updated to document and implement these changes. The editor style files for LNT and many CADP demos have been also updated. 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 2023-LNT-SET-ORDER <directory>
   upc 2023-LNT-SORTED-SET <directory>
   upc 2023-LNT-NIL <directory>
   upc 2023-LNT-NAT-INT <directory>
   upc 2023-LNT-NE <directory>
   upc 2023-LNT-PREDEFINED <directory>

    Fourteen bugs have been fixed: one in LNT_CHECK, one in LNT_NAME, two in the predefined libraries, and ten in the LNT2LOTOS translator (one in syntax analysis, three in static semantics and data flow analysis, three in LOTOS code generation, and three in error messages). To increase its interoperability with TRAIAN, the LNT2LOTOS translator was enhanced as follows:

    • The grammar used for the syntax analysis of LNT2LOTOS was modified to be aligned with that of TRAIAN.
    • Sets are implemented more efficiently, the worst-case complexity of set equality becoming linear instead of quadratic.
    • Five warnings of LNT2LOTOS have been turned into fatal errors, as they were already considered as fatal errors by TRAIAN.
    • Fourteen warnings of LNT2LOTOS redundant with those of TRAIAN are no longer emitted when LNT2LOTOS is invoked after TRAIAN (i.e., with its new "-traian" option).
    • LNT2LOTOS displays more precise line numbers in its warnings about function and process parameters.
    • The data-flow analysis of the "for" loops in LNT functions has been revised to produce additional warnings (similar to the ones emitted by TRAIAN).
    • LNT2LOTOS now forbids using "/=" instead of "!=" or "<>" to denote inequality.
    • LNT2LOTOS no longer defines a function MEMBER: T1, T2 → BOOL for any type T2 defined as set of T1.
    • LNT2LOTOS now generates a LOTOS function INSERT: T1, T2 → T2 for any type T2 defined as list of T1.
    • LNT2LOTOS now supports "with FIRST" and "with LAST" clauses in cascade types, and generates LOTOS code for them.
    • LNT2LOTOS now supports "with PRED" and "with SUCC" clauses in ranges, enumerations, and cascade types, and generates LOTOS code for them.
    • LNT2LOTOS now supports field-selection and field-update expressions with event parameters, i.e., LNT expressions of the form "V .[E] X" and "V .[E] {X → V', ...}", where E is an event (possibly the UNEXPECTED exception).

    For details, see HISTORY entries: #2852 #2856 #2857 #2858 #2859 #2860 #2861 #2862 #2863 #2865 #2873 #2887 #2890 #2891 #2892 #2893 #2894 #2895 #2896 #2897 #2898 #2899 #2905 #2908 #2912 #2914 #2915 #2916 #2917 #2918 #2919 #2920 #2926 #2927 #2928 #2938 #2939 #2941 #2942 #2943 #2945 #2946 #2947 #2948 #2949 #2951 #2953 #2954

    • MISC

    In addition to seven bug fixes in CAESAR (invoked with its "-graph" option), EUCALYPTUS, EVALUATOR 4 and 5 (on Solaris architecture only), EXP.OPEN (on large composition expressions containing priority operators), MCL_EXPAND (when invoking EVALUATOR 5 with its "-acyclic" option on probabilistic formulas), and XTL (when manipulating label fields of type String), various enhancements have been brought to the following CADP tools:

    • The BCG monitor was made much faster when generating labelled transition systems containing many different labels.
    • BCG_MIN (unless when called with its "-class" option) now removes, before undertaking probabilistic or stochastic minimization, all states and transitions that are unreachable due to the "maximal progress" assumption.
    • XTL no longer emits warnings on Linux when evaluating an XTL program on a BCG file containing no transitions.
    • The two functions ADT_GCD_NAT() and ADT_SCM_NAT() of the natural number library now use faster algorithms that are less prone to numeric overflow.
    • In CADP, better file compression is now achieved using "gzip" instead of "compress".

    For details, see HISTORY entries: #2864 #2866 #2869 #2874 #2877 #2881 #2879 #2882 #2884 #2885 #2910 #2955

    PORTS

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

    • Update of shell scripts to use modern PostScript viewers (e.g., Atril and Evince) and to avoid warnings emitted by recent versions of GNU grep.
    • Update of shell scripts and documentation to support Solaris 11 and recent versions of Oracle's C compiler; with these changes, CADP properly runs on Solaris 11.4.
    • Updates of scripts, include files, and documentation to avoid warnings emitted by the recent versions of Clang and to support macOS 14 "Sonoma", Xcode version 14.3, and recent versions of XQuartz.
    • Complete port of CADP to 64-bit Windows, with an upgrade of TCL/TK/TIX to their latest versions and subsequent adaptation of the CADP graphical tools (XSIMULATOR, OCIS); progressive migration from 32-bit to 64-bit Windows executables, the latter eventually replacing the former since they are faster; support of Windows 11 and the most recent versions of Cygwin.

    For details, see HISTORY entries: #2851 #2853 #2854 #2855 #2867 #2868 #2875 #2876 #2878 #2880 #2883 #2888 #2900 #2901 #2902 #2903 #2906 #2925 #2929 #2930 #2933 #2935 #2936 #2944

    SVL

    In addition to a bug fix for the macOS version of SVL, various enhancements have been brought:

    • SVL now produces shorter log files that better take into account user interrupts and run-time errors.
    • The error and warning messages issued by SVL have been aligned on those of other CADP compilers and now provide line numbers.
    • Better error and warning messages are emitted when reduction fails for some probabilistic or stochastic equivalence, and when both variables $DEFAULT_LOTOS_FILE and $DEFAULT_PROCESS_FILE are undefined.
    • SVL only retries reduction (using a stronger equivalence relation) when this is possibly fruitful.

    For details, see HISTORY entries: #2907 #2909 #2931 #2932 #2934 #2937

    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