This section summarizes the main enhancements in the various components of
CADP. For more details, please refer to the CADP
- BCG
-
A new major version 1.2 of the BCG format for storing Labelled Transition
Systems was released as part of CADP 2015-a. Following this change, various
minor residual bugs have been identified and fixed in 2015, and the type
system of XTL has been modified to require fewer explicit type coercions.
For details, see HISTORY entries:
#1993 #1994 #1996 #2004 #2008 #2016.
- CAESAR
-
In addition to a few bug fixes, the "-root" option of the CAESAR compiler
has been generalized to support process having value parameters; this makes
compositional verification easier by removing the need for introducing extra
processes having no value parameters. Also, the EXEC/CAESAR interface has
been extended with two new primitives CAESAR_KERNEL_DELAY and
CAESAR_KERNEL_EXIT().
For details, see HISTORY entries:
#2009 #2014 #2033 #2035 #2065 #2085.
- CAESAR.ADT
-
Optimizations have been introduced to generate shorter and simpler C code,
and to make sure that this C code compiles without spurious warnings.
For details, see HISTORY entries:
#2038 #2094 #2097.
- CAESAR.BDD
-
The CAESAR.BDD tool that analyzes NUPN (Nested-Unit Petri Nets) models
and serves to prepare the yearly Model Checking
Contest has been enhanced in several ways. In addition to 7 bug fixes,
14 new command-line options have been added to CAESAR.BDD ("-arcs",
"-bits", "-creator", "-density", "-encodings", "-height", "-hwb",
"-multiple-arcs", "-multiple-initial-tokens", "-places", "-redundant-units",
"-transitions", "-units", and "-width"). The output format produced by the
"-exclusive-places" option has been revised. The "-mcc" option now computes
the extended free choice property. A new option "-network nupn" was also
added to EXP.OPEN to produce NUPN models from automata networks.
Particular efforts have been put into increasing the scalability of CAESAR.BDD
for large models. Reading large NUPN files was made much faster. The
"-exclusive-places" option of CAESAR.BDD was made faster too. The size of
the largest data structure allocated by CAESAR.BDD has been divided by four.
CAESAR.BDD has also been optimized to save memory when handling NUPN models
having a simple hierarchical structure. Finally, user-specified timeouts are
better supported.
For details, see HISTORY entries:
#1991 #2000 #2054 #2055 #2056 #2057 #2058 #2059 #2061 #2062 #2063
#2068 #2069 #2073 #2077 #2078 #2081 #2083 #2089 #2091 #1941 #2093
#2102 #2104.
- DEMOS
-
The demo examples, which are a showcase for CADP, have been improved by
taking advantage of recent enhancements to CADP languages and tools.
Five demos (16, 21, 22, 36, and 38) have been rewritten from LOTOS to LNT.
A new demo 05 (airplane-ground communication protocol) has been added.
The code of many demos was updated to use the latest features of LNT, such
as "in var" parameters and "assert" statements. Demos 14 and 16 have been
greatly simplified by inlining MCL and XTL temporal logic formulas in SVL
scripts, using the "property" and "check" statements recently added to SVL.
Nine demos (02, 08, 17, 20, 27, 28, 31, 33, and 36) have been simplified by
using the new possibility to pass value parameters to LOTOS and LNT processes
directly in SVL scripts. XTL formulas have been shortened in demos 23 and 27.
Finally, demo 38 led to a publication at the MARS'15 workshop.
For details, see HISTORY entries:
#1989 #1990 #1999 #2023 #2025 #2039 #2041 #2050 #2067 #2074 #2086 #2092
#2099 #2116 #2121 #2123 #2144 #2145 #2146 #2153.
- DOC
-
Several manual pages of CADP have been made more readable by splitting each
of them into two different manual pages: one describing a given computer
language or file format (namely, EXP, GCF, NUPN, PBG, RBC, SVL, and XTL), and
another one describing the tool(s) operating on this language or format.
Also, PostScript files have been removed, making the CADP distribution
60-megabytes leaner.
For details, see HISTORY entries:
#2019 #2095 #2107 #2125 #2128 #2135 #2136.
- EXT
-
The connection to ext ernal software development tools has
progressed. The support of the LOTOS and LNT languages in the Emacs/XEmacs,
jEdit, and Vim editors has improved. More text editors are now supported,
including Nano, Notepad++, and all the text editors compliant with
GtkSourceView 3.0 (including the Gedit editor of Gnome). Pretty-printers
such as a2ps and the LaTeX "listings" package are also supported. Configuration
files for three CADP languages (MCL, SVL, and XTL) and three CADP formats
(BES, NUPN, and RBC) have been added.
For details, see HISTORY entries:
#2016 #2022 #2028 #2046 #2048 #2051 #2071 #2072 #2084 #2115 #2118 #2120
#2142 #2143 #2151.
- LNT
-
Significant effort has been devoted to improve the LNT toolchain (namely, the
LPP, LNT2LOTOS, LNT.OPEN, and LNT_CHECK tools). In addition to 22 bug fixes
(incorrect error messages, undetected overflows, wrongly-generated LOTOS code,
etc.), the LNT language has been enhanced in several aspects. The "case"
construct now supports multiple (tuple-like) expressions and patterns.
Better messages are emitted for "in" and "in out" parameters, and two new
parameter-passing modes "in var" and "out var" have been introduced to allow
finer data-flow analyses. Exceptions are better handled and a new "assert"
statement was added to LNT. The "none" channel is now implicitly predefined.
The "-root" option of LNT2LOTOS now accepts value parameters for LNT processes.
Finally, the LNT reference manual has been extended and updated at many
places.
For details, see HISTORY entries:
#2007 #2012 #2018 #2024 #2026 #2032 #2034 #2036 #2043 #2045 #2047 #2049
#2053 #2060 #2064 #2066 #2070 #2075 #2076 #2088 #2098 #2100 #2103 #2109
#2110 #2111 #2112 #2113 #2117 #2119 #2122 #2124 #2126 #2129 #2131 #2132
#2134 #2138 #2139 #2140 #2141 #2147 #2149 #2150 #2152.
- MCL
-
The CAESAR_SOLVE library was enriched with a new algorithm A9 optimized for
the Boolean equation systems generated when model checking guarded
mu-calculus formulas on acyclic Labelled Transition Systems. The EVALUATOR 3
and EVALUATOR 4 model checkers now take advantage of this new algorithm to
reduce memory consumption when operating on such acyclic Labelled Transition
Systems. The ACTL (Action-based Computation Tree Logic) library has been
made more modular, and a new library was added to provide temporal logic
operators adequate with respect to divergence-sensitive branching bisimulation.
For details, see HISTORY entries:
#2005 #2006 #2015 #2020 #2148.
- SVL
-
The SVL language was extended and made more regular in many respects. The
"property" statement of SVL was generalized and made applicable to any
statement. The "expected" statement can now be attached to any shell command.
A new "result" statement allows to store in a shell variable the output of a
verification statement. The diagnostic file was made optional in comparison,
deadlock, and livelock statements. Translation from LNT to LOTOS can now be
obtained directly using a simple SVL assignment. Hiding and renaming of
labels now work compositionnally on automata networks, without generating the
corresponding Labelled Transition Systems. SVL scripts for compositional
verification can be much shorter as it is now possible to pass value
parameters in the instantiations of LNT and LOTOS processes. Additionally,
seven bugs in SVL have been fixed.
For details, see HISTORY entries:
#1992 #1997 #1998 #2013 #2017 #2021 #2029 #2030 #2037 #2040 #2042 #2044
#2079 #2090 #2096 #2101 #2114.
- MISC
-
In addition to bug fixes in various tools (e.g., CUNCTATOR, EUCALYPTUS, TST,
XTL, etc.), the installation procedures of CADP have been revisited and
updated; in particular, work is going on and many preliminary changes have
been silently brought to ease installation of CADP on Windows.
For details, see HISTORY entries:
#1995 #2001 #2002 #2003 #2010 #2011 #2027 #2031 #2052 #2080 #2082 #2087
#2105 #2108 #2127 #2130 #2133 #2137.
We are extremely grateful to the following scientists, who provided us with
valuable feedback and advice about the use of CADP:
Back to the CADP Home Page