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

THE CADP NEWSLETTER - Nr. 13
February 22, 2021

This newsletter is available from the CADP Home page.

Contents

1. Progress of CADP during years 2019 and 2020

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 2019 and 2020, the development of CADP has steadily progressed. Following the monthly rolling-release model established in 2013, twenty-four versions of CADP have been released in 2019 and 2020. From version 2019-a to version 2021-a, 54 bugs have been fixed and 118 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.0, 3.1, and 3.2) of TRAIAN have been released in 2020.

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

The BCG_MIN tool has a new "-sharp" option to implement sharp bisimulation, a congruence for parallel composition that takes place between divbranching and strong bisimulations.

For details, see HISTORY entries: #2623

DOC

In addition to various corrections and improvements, the manual page of the CAESAR_SOLVE_1 library has been enhanced with a new introduction, and a few former publications have been upgraded to more recent versions.

For details, see HISTORY entries: #2480 #2490 #2571 #2632

EXP

Two bugs have been fixed in the EXP.OPEN tool.

For details, see HISTORY entries: #2515 #2524

LNT

In addition to 14 bug fixes, the LNT2LOTOS translator was enhanced in many respects. It can handle larger LNT programs without stack overflow after a critical function of the compiler was rewritten in a non-recursive manner. It generates better LOTOS code in which useless parameters have been removed from auxiliary processes. Due to a refined data-flow analysis, it emits more warnings about unused parameters and useless assignments, especially in "loop" and "case" statements. It warns about dead "case" branches occurring after patterns that match all possible values. It warns about synchronized events that are not accessed in some parallel branches. A new option "-depend" allows to display the dependencies between LNT modules and it is now possible to replace the predefined LNT modules (e.g., BOOLEAN, NATURAL, etc.) with custom ones.

Also, the LNT language has progressively evolved, breaking away from some design decisions inherited from LOTOS in the 80s, to become a better language and to achieve convergence with the LOTOS NT language supported by the TRAIAN compiler.

From now on, LNT keywords must be written in lower case only: upper case is no longer accepted. Six new reserved keywords ("access", "alt", "ensure", "require", "result", and "trap") have been introduced. Six other keywords ("and", "div", "mod", "or", "rem", and "xor") have been added, which can be redefined by the user for overloaded constructor and function definitions.

From now on, LNT pragmas must be written in lower case only. Three new pragmas ("!num_bits", "!num_card", and "!version") have been introduced.

All LNT identifiers for channels must be case-insensitively different from "any". All LNT identifiers for types, events, processes, and functions having neither "out" nor "in out" parameters must be case-insensitively different from LOTOS reserved keywords (i.e., "accept", "exit", etc.).

The predefined libraries BIT, LNT_V1, and OCTET have been modified. The Boolean operators "implies" and "iff" have been renamed to "=>" and "<=>". The "and_then" and "or_else" operators are now written "and then" and "or else" (in lower case only). The predefined function "access" is now noted "element". The comparison operators "eq", "ne", "lt", "le", "gt", and "ge" are no longer available; one should use their equivalent notations "==", "!=", "<", "<=", ">", and ">=" instead. The LOTOS code generated for the predefined "ord" functions was modified to avoid GCC 6 warnings.

The syntax of LNT has also evolved. The symbol "=>" was replaced with "->" in field updates and named-style actual parameters of procedures and functions. The "with" clauses attached to modules and type definitions no longer require double quotes around function identifiers. It is no longer required to explicitly declare which constructors and functions can be called as infix operators.

A new instruction "access E1, ..., En" has been introduced, which is similar to "use X1, ..., Xn", but operates on events instead of variables.

A new "require" clause was introduced to express preconditions for LNT functions and processes. Each precondition is a Boolean expression on the input values of "in", "in var", and "in out" parameters of a function or process. Preconditions are checked upon function or process call. An exception (specified by the user or UNEXPECTED) is raised when a precondition is false. Preconditions can also be specified for external functions.

A new "ensure" clause was introduced to express postconditions for LNT functions and processes. Postconditions come with new notations, namely the "result" keyword that denotes the value returned by a function and the ".in" and ".out" qualifiers that denote the values of "in out" parameters when entering or leaving a function or process. Postconditions are checked upon function or process return. An exception (specified by the user or UNEXPECTED) is raised when a postcondition is false. Postconditions can also be specified for external functions.

The LNT2LOTOS Reference Manual has been updated to document the changes of the LNT language. The CADP demo examples have been upgraded to the latest version of LNT and modified to avoid warnings emitted by the LNT2LOTOS translator and the C compiler(s).

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 2020-LNT-KEYWORDS <directory>
   upc 2020-LNT-ACCESS <directory>
   upc 2020-LNT-PRAGMAS <directory>
   upc 2020-LNT-ARROWS <directory>
   upc 2020-LNT-REQUIRE <directory>
   upc 2020-LNT-ENSURE <directory>
   upc 2020-LNT-ALT-TRAP <directory>
   upc 2020-LNT-IMPLIES <directory>
   upc 2020-LNT-IFF <directory>
   upc 2020-LNT-WITH <directory>
   upc 2020-LNT-ANDTHEN <directory>
   upc 2020-LNT-ORELSE <directory>
   upc 2020-LNT-COMPARATORS <directory>
   upc 2020-LNT-INFIX <directory>
   upc 2020-LNT-IDENTIFIERS <directory>

For details, see HISTORY entries: #2481 #2482 #2500 #2501 #2538 #2573 #2575 #2576 #2577 #2585 #2586 #2587 #2588 #2589 #2590 #2591 #2592 #2594 #2595 #2596 #2597 #2598 #2599 #2601 #2602 #2605 #2606 #2607 #2610 #2611 #2612 #2613 #2614 #2615 #2616 #2617 #2618 #2627 #2628 #2633 #2634 #2636 #2637 #2638 #2641 #2642 #2645 #2647 #2648 #2650 #2651

LOTOS

A bug was fixed in the predefined library X_INTEGER, and the C code generated by the CAESAR compiler was modified to avoid two kinds of warnings emitted by the GCC 6.5 compiler.

For details, see HISTORY entries: #2544 #2546 #2608

MCL

In addition to seven bug fixes, the MCL v4 language was extended with a function "card" to compute the number of elements in a set of natural numbers.

A new model checker EVALUATOR 5 has been added, which is backward compatible with EVALUATOR 4 but introduces the possibility of checking probabilistic properties on the fly. EVALUATOR 5 comes with a new option "-epsilon" to specify the precision of floating-point calculations. The input language MCL v5 of EVALUATOR 5.0 extends MCL v4 with a new operator "prob", interpreted on Probabilistic Labelled Transition Systems, to compute the probability of transition sequences described using generalized regular formulas.

The MCL_EXPAND processor was upgraded from version 4.1 to 5.0, an upward compatible yet significantly larger extension (13,000 more lines of LOTOS NT code), which is called by all versions of EVALUATOR and supports the probabilistic formulas of MCL v5. MCL_EXPAND 5.0 performs vacuity checks to detect and report tautological MCL formulas of the form "< R> @", in which the regular expression R may match the empty word "nil". MCL_EXPAND 5.0 also warns about the presence of nondeterminism in the regular formulas on transition sequences given to the "prob" operator.

Two new manual pages "evaluator5" and "mcl5" have been written. The EUCALYPTUS graphical user interface was updated to give the choice between versions 3, 4, and 5 of EVALUATOR.

For details, see HISTORY entries: #2483 #2486 #2487 #2492 #2493 #2495 #2503 #2508 #2511 #2512 #2513 #2542 #2574 #2639

NUPN

The definition of the NUPN format was made more precise concerning spaces, tabulations, and character strings. The "initial place" clause was superseded by the more general "initial places" clause. Stricter semantic constraints and invariants have been formulated for the "!multiple_arcs" and "!multiple_initial_tokens" pragmas. The NUPN format was extended with a new "labels" section that gives (optional) names to places, transitions, and/or units. These changes have been implemented in the CAESAR, CAESAR.BDD, EXP.OPEN, and NUPN_INFO tools.

In addition to 13 bug fixes, CAESAR.BDD has undergone deep changes. It is now stricter, rejecting more misformed NUPN files previously accepted, and emitting better messages for transitions having no input places.

The internal data structures for representing transitions and arcs have been entirely rewritten, replacing bit matrices with adjacency lists; although both implementations have respective merits, the new implementation handles all the NUPN models that the former one handled, plus other NUPN models that could not be handled before.

The static exploration algorithm of CAESAR.BDD that computes a subset of dead places and dead transitions was enhanced to exploit the "!unit_safe" pragma. Also, this static algorithm is now invoked twice, before and after the dynamic exploration algorithm based on Binary Decision Diagrams (BDDs), reducing the number of iterations by 37%.

The "-check" option of CAESAR.BDD implements all the checks defined by the new semantic rules. It behaves faster when checking the unit safeness property of a NUPN, while no longer displaying information about dead places and dead transitions.

The "-concurrent-places" option of CAESAR.BDD (which replaces the former "-exclusive-places" option) was enhanced with several new algorithms that produce results with fewer unknown values when applied to large NUPN models whose reachable markings cannot be explored exhaustively. The output format of this option was modified in several respects and enhanced with run-length compression, leading to a disk-space compaction factor of 214 (mean value) up to 4270 (maximum observed).

The "-concurrent-units" option of CAESAR.BDD (which is no longer noted "-units") can now handle larger NUPN models, usually at the same speed as before, although it was observed to be slower on 20 particular models. The output format of this option was modified to be 12.8 times more compact.

The "-dead-transition" option of CAESAR.BDD (which is no longer noted "-dead") now benefits from the static exploration algorithm. It is faster and produces results with fewer unknown values for large NUPN models. The output format of this option was modified to be 4.8 times more compact.

The "-encodings" option of CAESAR.BDD was extended to compute four more encoding schemes suggested in [Garavel-19, Section 6.3]. The "-bits" and "-hwb" options of CAESAR.BDD now use encoding (i) by default, rather than encoding (e). The algorithms used to compute encodings (h) and (i) have been corrected. Also, encodings (f), (g), (h), and (i) now use fewer bits by taking advantage of information about idle units. The algorithms for computing idle and permanent units were enhanced, leading to significant speed improvement for various CAESAR.BDD options (e.g., "-encodings" became 15 times faster).

The "-mcc" option of CAESAR.BDD evolved to meet the requirements of the 2020 edition of the Model Checking Contest. It is now faster, computes a more accurate lower bound for the maximal number of tokens in reachable markings, recognizes trivial NUPN models, and better handles models containing both pragmas "!creator xxx" and "!unit_safe yyy" simultaneously.

Ten new options ("-dead-places", "-idle-units", "-initial-units", "-input-places", "-input-transitions", "-min-concurrency", "-max-concurrency", "-output-places", "-output-transitions", and "-permanent-units") have been added to CAESAR.BDD.

The exit status values returned by CAESAR.BDD have been modified. The environment variable $CAESAR_BDD_TIMEOUT can now be used to disable BDD-based exploration, and a new environment variable $CAESAR_BDD_ITERATIONS has been introduced to finely control this exploration.

In addition to two bug fixes, the NUPN_INFO tool has been enhanced in various ways. The Awk code for parsing the NUPN format was shortened and made faster by exploiting the new, simpler rules for spaces and tabulations and by invoking CAESAR.BDD in a more efficient way.

A new option "-canonical-nupn" was added to NUPN_INFO. This option normalizes a NUPN model by removing tabulations, extra spaces and empty lines, by sorting the lists of units, sub-units, transitions, input places, and output places, by removing useless "labels" lines, and by automatically computing the maximal label length.

A new option "-redundant-units" was added to NUPN_INFO. This option simplifies a NUPN model by eliminating its redundant units.

The CAESAR.BDD, NUPN, and NUPN_INFO manual pages have been updated to document all these changes.

For details, see HISTORY entries: #2484 #2485 #2494 #2497 #2498 #2499 #2502 #2504 #2507 #2510 #2516 #2517 #2519 #2520 #2521 #2523 #2526 #2529 #2530 #2531 #2532 #2533 #2534 #2535 #2536 #2537 #2554 #2555 #2556 #2557 #2558 #2559 #2560 #2561 #2562 #2563 #2564 #2565 #2566 #2567 #2578 #2579 #2580 #2582 #2583 #2584 #2593 #2600 #2603 #2604 #2609 #2622 #2624 #2625 #2630 #2631 #2640 #2643 #2644 #2646 #2649

OPEN/CAESAR

The "caesar.open" shell script was renamed to "lotos.open", still preserving backward compatibility. The CAESAR_GRAPH manual page that defines the OPEN/CAESAR Application Programming Interface has been updated to provide more accurate definitions of certain primitives and shorten the definition of two deprecated primitives.

For details, see HISTORY entries: #2488 #2489 #2569

PORTS

In addition to eight bug fixes and various other enhancements, all the CADP tools built using Syntax and TRAIAN (namely, EXP2C, FSP2LOTOS, LNT2LOTOS, MCL_EXPAND, and SVL) have been recompiled using the new version 3.0 of TRAIAN. The C compilers used to build the CADP tools have been upgraded to more recent versions. The source code of the CADP tools and the C code generated by these tools was modified to remove all compiler warnings.

The SunOS binaries of CADP are now compiled on SunOS 5.11 OpenIndiana and work for OpenIndiana, Solaris 11, and (possibly) Solaris 10. Various shell scripts ("cadp_echo", "cadp_indent", "tst") have been updated for OpenIndiana.

The Linux binaries of CADP are now compiled using GCC 6.3.0 instead of GCC 4.9.2 and have been upgraded to Debian 10.0. Support for older Linux versions with Glibc version less than 2.11 (e.g., Debian 5.0 Lenny) has been dropped. Also, Installator no longer proposes to install 32-bit CADP binaries on a 64-bit Linux if the 32-bit compatibility mode is missing.

The macOS binaries of CADP are now compiled using Clang 3.8.1 instead of Clang 3.5 and have been updated to support macOS 10.15 "Catalina" and recent versions of XQuartz. The 32-bit binaries, which are no longer supported by recent versions of macOS, have been removed. The instructions for installing CADP on macOS have been extended to also support the Homebrew package system, as an alternative to using MacPorts.

The instructions for installing CADP on Windows have been updated.

For details, see HISTORY entries: #2505 #2522 #2525 #2528 #2539 #2540 #2541 #2543 #2545 #2547 #2548 #2549 #2550 #2551 #2552 #2553 #2568 #2570 #2572 #2581 #2619 #2620 #2621 #2629 #2635

SVL

In addition to two bug fixes, the SVL language, the SVL compiler, and their manual pages have been updated to support version 5 of EVALUATOR and the reduction for sharp bisimulation recently introduced in BCG_MIN.

For details, see HISTORY entries: #2496 #2506 #2527 #2626

XTL

In addition to three bug fixes, a new function that converts transition labels to character strings was added to the XTL language.

For details, see HISTORY entries: #2491 #2509 #2514 #2518

3. Results of the RERS 2020 Challenge

Frédéric Lang, Wendelin Serwe (CONVECS, Grenoble, France), and Franco Mazzanti (ISTI-CNR, Pisa, Italy) have won all three gold medals for the "Parallel CTL" track of the RERS'2020 challenge organized by the Technische Universität Dortmund (Germany) and the Lawrence Livermore National Laboratory (CA, USA).

The goal of the "Parallel CTL" track was to verify 90 properties expressed in the branching-time temporal logic CTL on 9 complex concurrent systems (10 properties per system). Participants were given approximately four weeks, starting from the publication of the RERS problems, to solve these problems and submit their answers, the correct results being only known by the organizers of the RERS challenge.

In 2019, Lang and Mazzanti had correctly solved 100% of the RERS problems using the CADP tools and won all six gold medals for the "Parallel CTL" and "Parallel LTL" tracks of the RERS'2019 challenge.

In 2020, the RERS organizers, when designing their parallel problems, took specific countermeasures in order to defeat the compositional verification techniques of CADP that Lang and Mazzanti had successfully used in 2019. Although the organizers reduced the number of concurrent processes (16 instead of 70) and synchronization actions (75 instead of 234), they significantly increased the complexity of the concurrent processes themselves.

Nevertheless, Lang, Serwe and Mazzanti managed to correctly solve 88% of the "Parallel CTL" problems of the RERS'2020 challenge, only giving "don't know" answers for 11 formulas out of 90. This was done by combining the novel concept of sharp bisimulation developed for the RERS'2019 edition with a partial-model-checking approach implemented on top of CADP.

4. 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