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 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.
For details, see HISTORY entries: #2623
For details, see HISTORY entries: #2480 #2490 #2571 #2632
For details, see HISTORY entries: #2515 #2524
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-ACCESS upc 2020-LNT-PRAGMAS upc 2020-LNT-ARROWS upc 2020-LNT-REQUIRE upc 2020-LNT-ENSURE upc 2020-LNT-ALT-TRAP upc 2020-LNT-IMPLIES upc 2020-LNT-IFF upc 2020-LNT-WITH upc 2020-LNT-ANDTHEN upc 2020-LNT-ORELSE upc 2020-LNT-COMPARATORS upc 2020-LNT-INFIX upc 2020-LNT-IDENTIFIERS
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
For details, see HISTORY entries: #2544 #2546 #2608
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
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
For details, see HISTORY entries: #2488 #2489 #2569
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
For details, see HISTORY entries: #2496 #2506 #2527 #2626
For details, see HISTORY entries: #2491 #2509 #2514 #2518
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 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.
We are extremely grateful to the following scientists, who provided us with valuable feedback and advices about the use of CADP: