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

THE CADP NEWSLETTER - Nr. 14
February 11, 2022

This newsletter is available from the CADP Home page.

Contents

1. Progress of CADP during year 2021

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 2021, the development of CADP has steadily progressed. Following the monthly rolling-release model established in 2013, twelve versions of CADP have been released in 2021. From version 2021-a to version 2021-l, 34 bugs have been fixed and 77 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.3, 3.4, and 3.5) of TRAIAN have been released in 2021. 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 ALDEBARAN script (which calls BCG_MIN and BCG_CMP) and two bug fixes in BCG_EDIT, the implementation of sharp reduction in BCG_MIN was enhanced by using a new signature-based partition-refinement algorithm that computes sharp-equivalence classes and performs full minimization with respect to sharp bisimulation, thus replacing the partial-reduction algorithm formerly implemented in BCG_MIN.

The BCG_CMP tool was also enhanced with this new algorithm so to compare two labelled transition systems modulo sharp bisimulation.

For details, see HISTORY entries: #2693 #2694 #2708 #2710 #2729

FSP

The FSP2LOTOS compiler now accepts the definition of local processes named ERROR or STOP, but only if they have a non-empty set of parameters.

For details, see HISTORY entries: #2659

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.

The priority rules for LNT infix operators have changed to reduce the need for parentheses and make LNT expressions closer to mathematical notations. The predefined LNT operator for string concatenation, formerly noted "+", was renamed to "&", which is the notation used in LOTOS NT, but also in Ada, AppleScript, and VisualBasic. The predefined function "is_empty" was renamed to "IsEmpty". The syntax of the "case" instruction was simplified by removing an extra "in" keyword. All LNT pragmas of the form !representedby "xxx" are now deprecated and replaced by pragmas of the form !implementedby "LOTOS:xxx". Also, the pragmas of the form !implementedby "xxx" can be equivalently written !implementedby "C:xxx", meaning that xxx is an identifier of the C language (same for !comparedby, !printedby, and !iteratedby).

In addition to seven bug fixes in LNT2LOTOS, one bug fix in LNT_DEPEND, and one bug fix in UPC, the LNT2LOTOS translator has been refined to emit new warnings about ambiguous or potentially erroneous situations: expressions combining different infix Boolean operators without parentheses; expressions combining different user-defined infix operators without parentheses; expressions using user-defined operators such as "AND", "And", "OR", etc. that do not enjoy the same precedence as the builtin operators "and", "or", etc.; patterns using "any T" without parentheses on the left-hand side of an infix operator; channel fields that are not given names; etc.

The LNT2LOTOS Reference Manual has been updated to document the changes of LNT, and the CADP demo examples have been upgraded to the latest version of LNT. Also, the demos 07, 08, 09, 20, 34, 37, and 39 of CADP have been translated from LOTOS to LNT.

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 2021-LNT-PRIORITIES <directory>
   upc 2021-LNT-UPPER-INFIX <directory>
   upc 2021-LNT-ISEMPTY <directory>
   upc 2021-LNT-CASE-VAR <directory>
   upc 2021-LNT-REPRESENTEDBY <directory>
   upc 2021-LNT-CHANNELS <directory>
   upc 2021-LNT-ANY <directory>

For details, see HISTORY entries: #2652 #2654 #2655 #2657 #2660 #2661 #2665 #2667 #2669 #2670 #2671 #2705 #2706 #2707 #2716 #2717 #2720 #2725 #2730 #2735 #2738 #2739 #2740 #2741 #2742 #2743 #2744 #2745 #2748 #2753 #2754 #2755

LOTOS

In addition to 5 bug fixes, the CAESAR and CAESAR.ADT compilers now reject C identifiers that collide with the reserved keywords of the C99 and C11 versions of the C language, and generate C code that complies with the activation by default of the "-fno-common" option in Gcc 10.

For details, see HISTORY entries: #2675 #2678 #2679 #2680 #2697 #2700 #2737 #2747

NUPN

In addition to three bug fixes, the CAESAR.BDD tool was enhanced in multiple ways.

New internal data structures have been introduced to store the transitions going in and out of each place. Although this new implementation consumes more memory, it is (usually two times) faster on large NUPNs.

The BDD exploration of reachable markings was made more efficient by no longer attempting to fire transitions known to be dead. The standard "sift" strategy for the dynamic reordering of BDDs has been replaced with a more efficient strategy ("group sift"), in which only the binary variables that encode the same NUPN unit can be permuted during reordering. Also, a new criterion (based on the number of BDD nodes rather than on the number of transitions) to enable dynamic reordering has been introduced, which better reflects the intrinsic complexity of a NUPN.

These changes, combined to other enhancements, increased the performance of many CAESAR.BDD options, including "-concurrent-places", "-concurrent-units", "-dead-places", "-dead-transitions", "-mcc", "-trivial", etc., which have been made faster and, possibly, more precise.

CAESAR.BDD now accepts NUPNs with an empty initial marking. It has been also extended with three new options "-place-order", "-transition-order", and "-unit-order" intended to characterize NUPNs that are equivalent modulo net isomorphism. These options have been continuously improved during year 2021 in order to better detect symmetries.

In addition to three bug fixes, the NUPN_INFO tool was enhanced in various ways. Its Awk code was made simpler and more modular by factoring fragments of code shared by several options. The tool was significantly extended to put NUPNs under a canonical form that helps detecting duplicate models in large collections of Petri nets and NUPNs.

Two new options "-essential-nupn", which removes pragmas and labels from NUPNs, and "-precanonical-nupn" have been added to NUPN_INFO.

Six new options "-place-permute", "-place-renumber", "-transition-permute", "-transition-renumber", "-unit-permute", and "-unit-renumber" have also been added.

Three new options "-place-sort", "-transition-sort", and "-unit-sort" (which reuse the results computed by the options "-place-order", "-transition-order", and "-unit-order" of CAESAR.BDD) have also been added to NUPN_INFO.

The behaviour of the "-canonical-nupn" option of NUPN_INFO has been strengthened by invoking all the aforementioned options in combination, and a new option "-normal-nupn" was added to retain the former behaviour of the "-canonical-nupn" option.

The manual pages for CAESAR.BDD, NUPN_INFO, and the NUPN format have been updated accordingly and modified at various places to resolve ambiguities.

For details, see HISTORY entries: #2653 #2681 #2682 #2683 #2684 #2685 #2686 #2687 #2688 #2689 #2690 #2691 #2692 #2695 #2698 #2699 #2702 #2703 #2718 #2719 #2721 #2731 #2733 #2734 #2749 #2750 #2751 #2757 #2759 #2760 #2761

PORTS

In addition to nine bug fixes (including two in EUCALYPTUS, two in INSTALLATOR, and two in TST), the CADP tools have been enhanced in many ways.

The CADP tools (as well as the CADP, CONVECS, and VASY web sites) have been updated to use, whenever possible, the HTTPS protocol instead of the FTP and HTTP protocols.

CADP no longer uses "compress" and ".Z" files as its default compression. Installator now uses "gzip", and support for "xz" compression was added.

INSTALLATOR no longer proposes the obsolete protocols RSH and RCP. RFL now supports the Oarsh/Oarcp commands for deployment on large clusters, such as Grid 5000.

Concerning Linux: CADP was adapted to support recent Linux distributions based on Glibc 2.32. Various changes were done to avoid warnings emitted by versions 7, 8, 9, and 11 of the Gcc compiler. The TST script prints finer information about virtualization and hypervisors and the user's preferred browser is now automatically detected. A new documentation file INSTALLATION_LINUX was added.

Concerning macOS: CADP was ported to macOS 11 "Big Sur" and macOS 12 "Monterey". Also, various changes were made to avoid warnings that appeared with Xcode 13 and XQuartz 2.8.1. The instructions for installing CADP on macOS have been updated and simplified.

Concerning Windows: CADP was adapted to work on the Linux distributions available from the Microsoft Store and running on top of Windows/WSL2 (Windows Subsystem for Linux); both X servers VcXsrv and KeX are supported. Also, the Windows/Cygwin version of CADP was enhanced by using Microsoft Edge by default for HTML and PDF documents, and by avoiding an issue with the version 4.4.12(3) of GNU bash currently shipped with Cygwin. Support for the obsolete versions 7 and 8 of Windows was dropped.

For details, see HISTORY entries: #2656 #2662 #2663 #2664 #2666 #2668 #2672 #2673 #2674 #2676 #2677 #2701 #2704 #2711 #2712 #2713 #2714 #2715 #2722 #2723 #2724 #2726 #2727 #2728 #2732 #2736 #2746 #2752 #2756 #2758 #2762

SVL

In addition to one bug fix, the SVL language, the SVL compiler, and their manual pages have been extended to support comparison of LTSs modulo sharp bisimulation, which was recently introduced in BCG_CMP.

For details, see HISTORY entries: #2658 #2696

XTL

The XTL compiler now rejects C identifiers that collide with the reserved keywords of the C99 and C11 versions of the C language.

For details, see HISTORY entries: #2697

3. Innovation Prize

On November 23, 2021, during a solemn ceremony at the French Academy of Sciences, Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe received, the Innovation Prize of Inria - Académie des Sciences - Dassault Systèmes.

This Prize of 20,000 euros was awarded to the four scientists of the CONVECS team (LIG laboratory, CNRS, Grenoble INP, Inria, Université Grenoble Alpes) for their long-term research work on formal methods for modelling and verifying complex systems with asynchronous concurrency. The team is developing languages for concurrent systems, compiling techniques for these languages, and verification algorithms for these systems. These results have been implemented in software tools coherently integrated in a toolbox named 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