CADP Change List

This page lists the recents changes brought to the CADP toolbox. For more details about particular changes, please refer to the corresponding items in the HISTORY file of the CADP distribution.

Item numbers in red (e.g., "#1758") indicate changes that are not compatible with earlier versions of CADP and may require manual intervention to adapt existing scripts and specifications (see the $CADP/HISTORY file for details). If a red item number is followed by a star (e.g., "#2064*"), this means that the changes can be performed automatically using the "upc" tool provided by CADP (the use of this tool is explained in the $CADP/HISTORY file). As a general rule, we avoid breaking compatibility without good justification.

2017-02-13 - Change List for CADP Version 2017-b "Sophia Antipolis"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2276 Improvement From now on, the variables and exceptions of LNT belong to two different name spaces
#2277 Bug fix BES_SOLVE could corrupt its buffer containing statistics for distributed BES resolution
#2278 Bug fix In LNT functions, calling a function with one exception parameter required an "eval" keyword
#2279 Improvement The simple "loop" operator (without label or while condition) is now allowed in LNT functions
#2280 Improvement The "-stat" option of BES_SOLVE generates better diagnostics for distributed BES resolution
#2281 Bug fix LNT2LOTOS could generate incorrect LOTOS code for "case" statements in LNT functions
#2282 Bug fix The distributed BES resolution of BES_SOLVE did not halt properly on memory exhaustion
#2283 Improvement LNT2LOTOS now uses significantly less memory when translating "if-then-else" statements
#2284 Improvement The LOTOS, LNT, and C files of demo_12 (MAA) have been extensively revised and shortened

2017-01-13 - Change List for CADP Version 2017-a "Sophia Antipolis"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2271 Bug fix LNT2LOTOS failed to compile long sequences of "assert" or "return" intersparsed with "if"
#2272 Improvement Some LNT source files of demo_19 have been simplified and enriched with comments
#2273 Improvement A new predefined library OCTETVALUES with byte constants for LOTOS and LNT has been added
#2274 Improvement The LOTOS and LNT source files of demo_12 have been further revised and greatly simplified
#2275 Improvement LNT2LOTOS uses less stack space when translating long sequences of actions or process calls

2016-12-13 - Change List for CADP Version 2016-l "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2258 Bug fix The code of the CAESAR_NETWORK library contained minor defects, which have been fixed
#2259 Bug fix There were random characters in one error message of the CAESAR_NETWORK library
#2260 Improvement The CAESAR_NETWORK library checks that worker processes operate in disjoint directories
#2261 Bug fix The X_NATURAL.h/X_INTEGER.h include files caused a GCC "-Wformat=" warning on Windows
#2262 Improvement TST now displays better messages when a CADP-related environment variable is unset or empty
#2263 Improvement The LNT code of demo_12 has been simplified and enriched with canonical unit tests
#2264 Improvement The CAESAR_NETWORK library checks that worker processes do not use their parent's directory
#2265 Bug fix BCG_IO caused stack overflow when translating long execution paths into the SEQUENCE format
#2266 Improvement BCG_IO generates much more concise pseudo-LOTOS code when translating long execution paths
#2267 Bug fix On localized (non-English) versions of Linux, CADP_MEMORY could fail, causing table overflows
#2268 Bug fix The distributed termination algorithm of CAESAR_NETWORK froze if a worker crashed too early
#2269 Bug fix Invoking "LNT.OPEN -root P P.lnt" (with the same name P) resulted in an empty transition system
#2270 Bug fix LNT2LOTOS went slow and could exhaust memory when compiling long sequences of "assert"

2016-11-13 - Change List for CADP Version 2016-k "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2251 Bug fix LNT2LOTOS did not generate the "CAESAR_ADT_SCALAR_%s" macro for LNT range types
#2252 Improvement The CADP publication list and tutorial page have been completed and better organized
#2253 Improvement CADP has been ported to the latest version 10.12 "Sierra" of Apple's macOS operating system
#2254 Bug fix Installation of CADP on macOS did not handle XQuartz versions that do not install in /usr/X11R6
#2255 Bug fix SVL could emit a warning that observational reduction is not available, which was incorrect
#2256 Bug fix With recent Cygwin versions, INSTALLATOR could give invalid ACLs to the text files of CADP
#2257 Improvement CADP now works on Windows even when Cygwin is not installed in the root directory C:/

2016-10-13 - Change List for CADP Version 2016-j "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2244 Bug fix The skeleton C code produced by the "-external" option of CAESAR could contain invalid type casts
#2245 Improvement The LNT syntax was extended so that functions now accept exception parameters in the named style
#2246 Bug fix RFL would emit spurious error messages when invoked without setting the $CADP variable
#2247 Improvement Several predefined MCL libraries for EVALUATOR have been modified to generate better diagnostics
#2248 Bug fix Since CADP 2016-f (June 2016), the BCG tools could misparse real numbers, setting them to zero
#2249 Improvement The EUCALYPTUS graphical interface now supports the recent "-numeral" option of CAESAR.ADT
#2250 Bug fix EUCALYPTUS incorrectly tried to avoid calls to CAESAR.ADT by considering file timestamps only

2016-09-13 - Change List for CADP Version 2016-i "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2237 Improvement TST gives more informative diagnostics when "uudecode" is missing on Linux
#2238 Bug fix The C code generated by XTL for a printing function caused a GCC "-Wformat" warning
#2239 Bug fix On Solaris, the LPP-preprocessor line buffer was limited to 1024 characters only
#2240 Bug fix XTL caused a GCC "-Wunused-variable" warning when handling legacy BCG 1.0 files
#2241 Improvement LNT2LOTOS now accepts LNT process calls with identical actual gate parameters
#2242 Improvement Calls to user-defined LNT functions now use explicit, checked exception parameters
#2243 Improvement The "-external" option of CAESAR better documents the type profile of visible gates

2016-08-26 - Change List for CADP Version 2016-h "Oxford"

HISTORY file item Type Summary
#2228 Improvement The LNT syntax now allows to freely combine array accesses, field accesses, and field updates
#2229 Bug fix CAESAR and CAESAR.ADT performed incomplete checks for renamed sorts and operations
#2230 Improvement The LNT syntax for constant functions that may raise exceptions has been extended
#2231 Bug fix Error messages of CAESAR and CAESAR.ADT could list overloaded functions more than once
#2232* Improvement CAESAR and CAESAR.ADT generate new C identifiers for special LOTOS ops w/o "implementedby"
#2233* Improvement CAESAR and CAESAR.ADT generate shorter C identifiers for LOTOS sorts w/o "implementedby"
#2234* Improvement CAESAR and CAESAR.ADT generate shorter C identifiers for LOTOS ops w/o "implementedby"
#2235* Improvement The C identifiers for CAESAR.ADT testers, selectors, and iterators have been regularized
#2236 Improvement CAESAR and CAESAR.ADT now warn about obsolete ".h", ".f", and ".t" files (i.e., version < 2.5)

2016-07-13 - Change List for CADP Version 2016-g "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2220 Improvement For numeral sorts, CAESAR.ADT 5.5 now generates iterators over 0...255 rather than 0...254
#2221 Improvement The syntax modes provided for text editors now support the new "use" keyword of LNT
#2222 Bug fix For numeral sorts, CAESAR.ADT mishandled negative values of CAESAR_ADT_HASH_...
#2223 Improvement For numeral sorts, CAESAR.ADT now accept extra values given to CAESAR_ADT_HASH_...
#2224 Improvement CAESAR.ADT has a new option "-numeral" to specify how numeral sorts are implemented
#2225* Improvement The LNT syntax for declaring functions that raise exceptions has been modified
#2226 Improvement CAESAR and CAESAR.ADT forbid using the "inline" and "restrict" C11 keywords as identifiers
#2227 Improvement OCIS (invoked with its "-tty" option) now works when the standard output is block-buffered

2016-06-13 - Change List for CADP Version 2016-f "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2208 Improvement In type libraries, bcg_character_scan() was rewritten and may return different error codes
#2209 Improvement In type libraries, bcg_string_scan() was simplified and may return different error codes
#2210 Improvement The installation guidelines for Windows now discuss the 64-bit Cygwin installer
#2211 Improvement The rules for parsing labels in the BCG_WRITE manual page have been improved
#2212 Improvement EXP.OPEN can emit three new warnings concerning the generalized "par" operator
#2213 Improvement SVL now supports the general "par" operator with degrees in synchronization interfaces
#2214 Improvement In type libraries, bcg_raw_scan() was deeply modified to support escape sequences
#2215 Improvement In type libraries, the bcg_real_scan() function now detects overflows and underflows
#2216 Bug fix The distributed verification tools had stopped working in CADP 2016-e "Oxford"
#2217 Improvement The LNT language has been enriched with a new statement "use X1, ..., Xn"
#2218 Bug fix LNT2LOTOS could generate incorrect-syntax LOTOS code for LNT modules named "TEST"
#2219 Improvement A list of selected publications about CADP was prepared and a new paper was added

2016-05-13 - Change List for CADP Version 2016-e "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2195 Bug fix Two issues have been fixed in the OPEN/CAESAR communication library for distributed processes
#2196 Improvement The CADP binaries have been made faster on Mac OS X, Windows, and certain versions of Linux
#2197 Improvement New includes avoid warnings about popen/pclose on Windows with the latest Mingw GCC compiler
#2198 Improvement The INSTALLATION_WINDOWS directives were updated to follow recent changes in Cygwin packages
#2199 Improvement The CADP tools have been modified to properly work on Windows using the 64-bit version of Cygwin
#2200 Bug fix EXECUTOR, SIMULATOR, and TERMINATOR did not work from block-buffered shells (e.g., Mintty)
#2201 Improvement The "-silent" and "-verbose" options of CAESAR.OPEN and LNT.OPEN have a more intuitive semantics
#2202 Improvement The five pictures of the DISTRIBUTOR manual page have been replaced with more accurate ones
#2203 Improvement The local interfaces of the EXP language have been extended and unified with the global interfaces
#2204 Improvement The "par" operator of EXP was extended with a new "#1" clause that signals non-synchronized actions
#2205 Improvement The "par" operator of EXP was extended with a new "#0" clause that prevents actions from firing
#2206 Improvement The INSTALLATION_2 directives now forbid spaces and non-ASCII characters in the $CADP pathname
#2207 Improvement The OPEN/CAESAR includes define two new types CAESAR_TYPE_ARGC and CAESAR_TYPE_ARGV

2016-04-13 - Change List for CADP Version 2016-d "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2178 Improvement The LOTOS manual page has been expanded from 12 to 27 pages
#2179 Improvement Two small enhancements have been brought to CAESAR.ADT
#2180 Bug fix CAESAR and CAESAR.ADT did not forbid identifiers named "ENDLIB"
#2181 Improvement The CAESAR and CAESAR.ADT manual pages have been extended
#2182 Bug fix Most CADP manual pages contained various HTML, nroff, and PDF issues
#2183 Bug fix Section titles in three manual pages were truncated to six words at most
#2184 Bug fix On Mac OS X 10.10 or higher, XTL emitted a "-Wformat-security" warning
#2185 Bug fix On Mac OS X 10.10 or higher, Installator and TST warned about /etc/hostconfig
#2186 Bug fix On Mac OS X 10.10 or higher, CAESAR.ADT reported "indent" failures
#2187 Bug fix TST incorrectly displayed that the default value of $CADP_LANGUAGE is "french"
#2188 Improvement Installator no longer proposes to install CADP in /tmp/cadp or /private/tmp/cadp
#2189 Improvement The installation guide has been updated for OS X "Yosemite" and "El Capitan"
#2190 Bug fix CAESAR.ADT did not forbid equations for non-constructors defined by renaming
#2191 Improvement CADP manual pages now contain URLs to the corresponding CADP publications
#2192 Improvement The EVALUATOR manual page has been split, leading to new MCL3 manual page
#2193 Improvement Demo 05 now takes advantage of LNT's "case" instruction with multiple patterns
#2194 Improvement The LNT2LOTOS reference manual has been enhanced at several places

2016-03-13 - Change List for CADP Version 2015-c "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2166 Improvement The warning and error messages of LNT2LOTOS now adopt the same format as GCC
#2167 Improvement A new option "-initial-places" has been added to CAESAR.BDD
#2168 Bug fix SVL did not always take into account that filenames are case-insensitive on Windows
#2169 Bug fix When directly invoked with a wrong number of options, EXP2C caused a core dump
#2170 Improvement Type-mismatch error messages of LNT2LOTOS now mention file names and line numbers
#2171 Improvement The manual pages for CAESAR and CAESAR.ADT have been extended
#2172 Improvement The CADP tools have been ported to Windows 10
#2173 Improvement LNT2LOTOS messages on non-exhaustive cases now give file names and line numbers
#2174 Bug fix The CADP manual pages did not display properly on Windows/Cygwin
#2175 Improvement The EVALUATOR 4 manual page has been split, leading to a standalone page for MCL
#2176 Improvement Demo 16 was slightly modified to avoid a warning about synchronization without effect
#2177 Improvement A manual page describing the subset of LOTOS accepted by CADP has been written

2016-02-13 - Change List for CADP Version 2016-b "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2154 Bug fix LNT.OPEN did not always erase its temporary directories "/tmp/lnt.*"
#2155 Improvement The "-mcc" option of CAESAR.BDD has a slightly modified output
#2156 Improvement One may now import predefined LNT modules located in "$CADP/lib"
#2157 Improvement 75 publications have been removed from CADP, saving 22 megabytes
#2158 Improvement Bitwise operators have been added to the LOTOS library OCTET
#2159 Improvement Two predefined LNT libraries, BIT and OCTET, have been added
#2160 Improvement An MCL property to check primality has been added to demo 36
#2161 Improvement Demo 12 (MAA) has been translated from LOTOS to LNT
#2162 Improvement Demo 31 (SCSI-2) has been translated from LOTOS to LNT
#2163 Improvement A new option "-initial-tokens" has been added to CAESAR.BDD
#2164 Improvement The "-mcc" option of CAESAR.BDD exploits (sub-)conservativeness
#2165 Improvement The "!multiple_initial_tokens" NUPN pragma accepts 64-bit numbers

2016-01-13 - Change List for CADP Version 2016-a "Oxford"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2141 Improvement A new construct "assert V [raise E]" is now available in LNT processes
#2142 Improvement Configuration files for the Notedpad++ text editor are now provided
#2143 Improvement More filter files for the a2ps pretty printer have been added
#2144 Improvement demo 23 was modified to avoid Gcc "-Wunused-but-set-variable" warnings
#2145 Improvement A useless "let" definition in XTL property 4 of demo 23 was removed
#2146 Improvement Two useless "let" definitions in an XTL property of demo 29 have been removed
#2147 Improvement From now on, the empty channel "none" is implicitly predefined in LNT
#2148 Bug fix EVALUATOR 4 failed to evaluate MCL V3 temporal-logic formulas on Windows
#2149 Bug fix Sometimes LNT2LOTOS did not erase temporary files "/tmp/lnt2lotos_root_*"
#2150 Bug fix LNT2LOTOS emitted cryptic warnings for non-exhaustive "case"s in functions
#2151 Bug fix Configuration files for LaTeX listings mishandled LNT, LOTOS, and MCL comments
#2152 Improvement A new construct "assert V [raise E]" is now available in LNT functions
#2153 Improvement Demos 16, 19, 29, and 38 have been enhanced with LNT "assert" constructs

2015-12-13 - Change List for CADP Version 2015-l "Stony Brook"

HISTORY file item Type Summary
#2124 Improvement LNT now supports "case" with multiple expressions and patterns (case E1, E2, E3 in...)
#2125 Improvement The definition of the RBC format was moved to a separate manual page
#2126 Improvement The predefined library of LNT was enriched with a unary "+" operator on integers
#2127 Bug fix The TST script emitted "cadp_where: No such file or directory" warnings on Windows
#2128 Improvement Two separate manual pages for the XTL language and compiler are now provided
#2129 Bug fix LNT2LOTOS could emit imprecise line numbers for incorrect "case" statements
#2130 Improvement The installation directives for CADP on Windows have been updated and simplified
#2131 Bug fix The "raise" statement of LNT had no effect when invoked in LNT processes
#2132 Bug fix LNT2LOTOS could emit "internal error" messages when compiling bogus LNT code
#2133 Improvement installator.shar is now downloaded with wget or curl rather than with the user's browser
#2134 Bug fix The error messages of LNT2LOTOS for wrongly typed gates were imprecise or incomplete
#2135 Improvement Two separate manual pages have been added to define the GCF and PBG formats
#2136 Improvement All PostScript files have been removed, making the CADP distribution 60-Mbyte leaner
#2137 Improvement For CADP on Windows, the meaning of the environment variable $CADP_TMP has changed
#2138 Improvement The vocabulary in the LNT2LOTOS Reference Manual was made more uniform
#2139 Improvement LNT2LOTOS now displays source-code line numbers when exceptions are raised
#2140 Bug fix GCC 4.7.3 could emit spurious warnings when compiling CADP includes on Windows

2015-11-13 - Change List for CADP Version 2015-k "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2106 Bug fix Some BCG tools could loop forever if a label contained only white spaces
#2107 Improvement The manual pages of EXP.OPEN and SVL have been split into shorter pages
#2108 Improvement The cadp_cc script avoids an issue with the 32-bit Solaris SunCC compiler
#2109 Bug fix The LNT library did not detect overflows in natural and integer constants
#2110 Improvement The dot character (".") is no longer permitted in LNT special identifiers
#2111 Improvement LNT2LOTOS generates better code for nat./int. constants having leading zeros
#2112 Bug fix In LNT the smallest integer (e.g., -2^31) caused overflow errors at run time
#2113 Improvement The LNT language now allows a "+" sign before integer and real constants
#2114 Bug fix Lines of the SVL log file were in disorder if $CADP_TIME was set to "memtime"
#2115 Improvement Syntax modes for the Nano editor have been made available as part of CADP
#2116 Improvement The demos 21 and 22 (Peterson and Dekker) have been translated to LNT
#2117 Bug fix The C implementation of the integer "mod" operator of LNT was incorrect
#2118 Improvement Syntax modes for the XTL language have been added for CADP-supported editors
#2119 Bug fix The C code produced by LNT2LOTOS could cause a GCC warning for -2^31
#2120 Improvement Syntax modes for the jEdit editor have been enhanced and/or added to CADP
#2121 Improvement The SVL script of demo 36 has been made more concise and parametric
#2122 Bug fix LNT2LOTOS generated different LOTOS code on Solaris and Linux machines
#2123 Improvement The demo 36 of CADP (Erathostenes sieve) has been translated to LNT

2015-10-13 - Change List for CADP Version 2015-j "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2093 Bug fix CAESAR.BDD did not properly halt BDD computations when receiving an interrupt signal
#2094 Improvement Three optimizations have been brought to the C code generated by CAESAR.ADT
#2095 Improvement Two papers on compositional verification and distributed code generation have been added
#2096 Improvement A new statement of the form "FILE.lotos" = "FILE.lnt" has been added to the SVL language
#2097 Improvement CAESAR.ADT now generates warning-free C code for comparing values of singleton types
#2098 Improvement The LPP preprocessor was simplified by removing support for ".lotos" and ".lib" files
#2099 Improvement The demo_38 (Data Encryption Standard) was enhanced and simplified in four ways
#2100 Improvement The LNT2LOTOS manual has been enhanced at many places (Chp 2, 3 and Annexes B, F)
#2101 Bug fix Two irrelevant warnings emitted by SVL have been suppressed
#2102 Bug fix The -mcc option of CAESAR.BDD generated incorrect values for three structural properties
#2103 Improvement A new "out var" mode (symmetric of "in var") for passing parameters was added to LNT
#2104 Improvement The -mcc option of CAESAR.BDD now computes the "extended free choice" property
#2105 Improvement The INSTALLATION_2 file and TST script now support cc 5.13 from Oracle Solaris Studio 12

2015-09-13 - Change List for CADP Version 2015-i "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2087 Bug fix Some CADP compilers did segmentation faults due to a bug in the SYNTAX compiler generator
#2088 Bug fix Option "-pidlist" of LNT2LOTOS emitted wrong output upon automatic syntax-error recovery
#2089 Improvement The "-exclusive-option" of CAESAR.BDD has been made 57% (possibly much more) faster
#2090 Bug fix When minimizing composition expressions, SVL could wrongly remove or regenerate BCG files
#2091 Improvement The "-concurrent-units" option of CAESAR.BDD has been made faster (between 24% and 40%)
#2092 Improvement demo_38 was translated from LOTOS to LNT, leading to shorter code and smaller state spaces

2015-08-27 - Change List for CADP Version 2015-h "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2071 Bug fix The LaTeX-listings file for the RBC format did not properly handle the "#" and ".." symbols
#2072 Improvement The EMACS configuration files for the LNT and SVL files have been enhanced
#2073 Improvement A standalone manual page has been introduced to define the NUPN format
#2074 Bug fix In demo_38, three algebraic equations defining the S-boxes of the DES were incorrect
#2075 Bug fix LNT2LOTOS could generate invalid LOTOS code for single-branch parallel composition
#2076 Bug fix LNT2LOTOS did not handle user-defined functions whose name was a one-digit number
#2077 Bug fix CAESAR.BDD now uses the CUDD timeout features to avoid random segmentation faults
#2078 Improvement The "-exclusive-places" option of CAESAR.BDD now interprets $CAESAR_BDD_TIMEOUT
#2079 Bug fix SVL could incorrectly erase certain generated BCG files when they were still needed
#2080 Improvement The BIT and X_BIT predefined LOTOS libraries have been enriched with new operators
#2081 Improvement The output of CAESAR.BDD's "-exclusive-places" option is more compact and informative
#2082 Bug fix When comparing LTSs on the fly using EUCALYPTUS, a file selection window did not open
#2083 Bug fix The "-mcc" option of CAESAR.BDD could report that the number of markings was infinite
#2084 Improvement Configuration files (Emacs, Gedit, Vim, LaTeX listings) are provided for the NUPN format
#2085 Improvement The sample "main.c" file for rapid prototyping using EXEC/CAESAR was made more generic
#2086 Improvement The demo_38 (DES encryption standard) was simplified and more thoroughly verified

2015-07-13 - Change List for CADP Version 2015-g "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2066 Improvement A new "in var" keyword was added to LNT to declare "in" parameters that can be assigned
#2067 Improvement Seven demos of CADP have been updated to use the new "in var" parameter mode of LNT
#2068 Bug fix When checking unit safeness CAESAR.BDD emitted fatal error messages rather than warnings
#2069 Improvement Other error messages of CAESAR.BDD have been turned into mere warnings and enhanced
#2070 Bug fix Since CADP 2015-e, LNT2LOTOS could generate invalid LOTOS code that did not compile

2015-06-13 - Change List for CADP Version 2015-f "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2053 Bug fix The bibliography was missing from the LNT2LOTOS reference manual
#2054 Improvement CAESAR.BDD now accepts "!unit_safe" pragmas followed by tool names and versions
#2055 Improvement The "-vlpn" option of CAESAR.BDD was removed and a "-encodings" option was added
#2056 Improvement CAESAR.BDD avoids unit-matrix allocation when handling NUPNs with simple hierarchy
#2057 Bug fix The CUDD library used in CAESAR.BDD was upgraded from version 2.4.1 to 2.5.1
#2058 Improvement Twelve new options for fastly querying NUPN files have been added to CAESAR.BDD
#2059 Bug fix CAESAR.BDD could do segmentation faults on large NUPNs due to multiply overflows
#2060 Improvement Several dataflow-related warning messages of LNT2LOTOS have been enhanced
#2061 Improvement CAESAR.BDD is much faster (e.g., 30 min. -> 25 sec.) when parsing large NUPN files
#2062 Improvement A "-redundant-units" option was added to CAESAR.BDD with relaxed constraints
#2063 Improvement The size of CAESAR.BDD's largest data structure (incidence matrix) was divided by 4
#2064* Improvement The "inout" keyword of LNT has been deprected and should now be written "in out"
#2065 Bug fix CAESAR.OPEN did not take into account the $CADP_TIME variable in certain cases

2015-05-13 - Change List for CADP Version 2015-e "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2042 Improvement SVL now accepts LNT process instantiations with gate parameters in the named style
#2043 Bug fix LNT2LOTOS generated superfluous ">> exit" code, causing warnings about potential deadlocks
#2044 Improvement The "hide" and "rename" operators are now handled more compositionally by SVL
#2045 Improvement LNT2LOTOS emits better warnings when ``inout'' parameters are assigned before used
#2046 Bug fix The EMACS configuration file for LNT and LNT did not handle multiline comments properly
#2047 Improvement The dynamic semantics of LNT (Annex B of the reference manual) has been simplified
#2048 Improvement Syntax modes for the BES and RBC formats are now provided for all CADP-supported text editors
#2049 Improvement LNT2LOTOS emits better warnings when "in"/"inout" parameters are never used and/or assigned
#2050 Improvement The demo 16 (Philips' Bounded Retransmission Protocol) has been translated to LNT
#2051 Improvement Syntax modes for GtkSourceView 3.0 editors (such as "gedit") are now available as part of CADP
#2052 Bug fix Running TST on Cygwin produced "sed" warnings (expression #1, char 1: unknown command: `^')

2015-04-13 - Change List for CADP Version 2015-d "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2029 Bug fix EXP2C and SVL rejected carriage-return characters in ".exp" and ".svl" source files
#2030 Bug fix SVL incorrectly expanded mixes of generalized parallel composition and total hiding of regular expressions
#2031 Bug fix XTL could stop with a "memory shortage" system error when comparing tuple values
#2032 Improvement Various error messages emitted by LNT2LOTOS have been made clearer
#2033 Bug fix The "-root" option of CAESAR did not detect the use the internal gate "i" as an actual parameter
#2034 Bug fix The "-root" option of LNT2LOTOS did not properly handle three particular cases
#2035 Bug fix Since CADP 2015-b the "-root" option of CAESAR forbade non-injective gate relabellings
#2036 Improvement The "-root" option of LNT2LOTOS and LNT.OPEN now support value parameters for LNT processes
#2037 Improvement SVL has been extended to support value parameters for LNT processes
#2038 Bug fix CAESAR.OPEN triggered spurious warnings when invoked with options "-infix", "-nupn", or "-prefix"
#2039 Improvement Demos 28 and 35 have been simplified using the new "-root" option of CAESAR and LNT2LOTOS
#2040 Improvement Typing rules in XTL now require less explicit coercions for Natural/Integer and String/Raw disambiguation
#2041 Improvement The new demo 05 now features the compositional verification of an airplane-ground communication protocol

2015-03-26 - Change List for CADP Version 2015-c "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#2012 Improvement The LPP preprocessor can now be invoked as a POSIX pipe
#2013 Bug fix SVL "verify" and "|=" statements could fail to produce diagnostics in AUT or SEQ formats
#2014 Improvement The "-root" option of CAESAR now supports LOTOS processes having value parameters
#2015 Improvement CAESAR_SOLVE has a new resolution algorithm A9 optimized for acyclic equation blocks
#2016 Improvement LOTOS and LNT editing with Vim was improved, and support for MCL and SVL was added
#2017 Improvement In SVL, diagnostic files are now optional for the "deadlock" and "livelock" statements
#2018 Bug fix LNT2LOTOS emitted redundant error messages for non-declared actual gate parameters
#2019 Bug fix The BISIMULATOR and LNT2LOTOS manual pages have been corrected at two places
#2020 Improvement EVALUATOR 3 and 4 exploit the new algorithm A9 and now accept the "-acyclic -bfs" option
#2021 Improvement In SVL scripts, processes can now be passed value parameters (in addition to gates)
#2022 Improvement Syntax-highlighting support for MCL and SVL is now provided for Emacs/XEmacs
#2023 Improvement Demos 02, 08, 20, and 31 have been shortened using CAESAR's enhanced "-root" option
#2024 Improvement The "-root" option of LNT2LOTOS accepts processes not declared in the principal module
#2025 Improvement Demos 17, 27, 33, and 36 have been simplified using the new "-root" option of CAESAR
#2026 Bug fix LNT2LOTOS mishandled processes without gates and with named-style value parameters
#2027 Bug fix Core dumps would occur when running CUNCTATOR on 64-bit Solaris for Intel processors
#2028 Improvement LOTOS, LNT, MCL, and SVL can now be typeset using the LaTeX listings package

2015-02-26 - Change List for CADP Version 2015-b "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1989 Improvement demo 16 was made more readable by inlining its XTL formulas into the SVL script
#1990 Improvement demo 03 has been archived because it was too old and too simple
#1991 Bug fix CAESAR.BDD could halt with a segmentation fault on some very large (e.g., 28 Mbytes) NUPN models
#1992 Improvement The "property" statement of SVL has been generalized to arbitrary commands
#1993 Improvement BCG_CMP, BCG_MIN, PROJECTOR, and GENERATOR now call BCG_IO_WRITE_BCG_ABORT() if needed
#1994 Bug fix Since CADP 2015-a, incorrect BCG files could be generated when label parsing was disabled
#1995 Improvement The TST shell script now better detects potential installation problems related to the LICENSE file
#1996 Bug fix BCG_CMP halted with a segmentation fault if its second command-line BCG argument had no transition
#1997 Improvement The expressiveness of the SVL language was enhanced with a new "result" statement
#1998 Improvement The "expected" statement of SVL can now be attached to arbitrary shell commands
#1999 Improvement demo 14 has been streamlined and enriched with value-passing temporal formulas written in MCL
#2000 Improvement EXP.OPEN can now convert EXP composition expressions into NUPNs (Nested-Unit Petri Nets)
#2001 Improvement The CADP installation directives for Windows incorporate the latest changes in Cygwin packages
#2002 Bug fix With the latest Cygwin, TST emitted a spurious warning "Command ls -l displays results on 11 columns"
#2003 Bug fix Since CADP 2015-a, INSTALLATOR failed on Windows ("Installator was blocked by Windows UAC")
#2004 Bug fix BCG_CMP produced different diagnostics when run on different (e.g., 32- vs 64-bits) architectures
#2005 Improvement The ACTL library for EVALUATOR was extended and modularized by identifying the ACTL\X fragment
#2006 Improvement An EVALUATOR 4 library of formulas preserving divergence-sensitive branching bisimulation was added
#2007 Bug fix LNT2LOTOS could generate incorrect LOTOS code that was later rejected by CAESAR and CAESAR.ADT
#2008 Bug fix Since CADP 2015-a, the BCG tools could no longer handle a few legacy BCG (version 1.0) files
#2009 Improvement Since CADP 2015-a, CAESAR.OPEN could in some cases mishandle the "-monitor" option of GENERATOR
#2010 Bug fix Closing parentheses that were missing have been added in three XTL libraries
#2011 Improvement INSTALLATOR now accepts spaces (e.g., added by cut-and-paste) around the CADP download password

2015-01-26 - Change List for CADP Version 2015-a "Stony Brook"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1943 Bug fix Two hidden bugs have been fixed in the BCG libraries and include files
#1944 Improvement New BCG files have been made more compact by removing obsolete legacy code
#1945 Improvement The BCG include files for manipulating label gates have been deeply reorganized
#1946 Improvement All CADP tools now print integers with their "+" or "-" sign to distinguish them from naturals
#1947 Improvement BCG and XTL have a new predefined type named NATURAL for (unsigned) natural numbers
#1948 Bug fix The BCG_WRITE parser for natural and integer numbers did not detect overflows and underflows
#1949 Improvement XTL now writes all its messages to the standard output rather than the standard error
#1950 Bug fix The BCG_WRITE API failed to parse character values and detect invalid escape sequences
#1951 Bug fix The BCG_WRITE parser did not handle "!" characters in offers, nor extra spaces between offers
#1952 Improvement All CADP tools now print double quotes around strings and display unprintable characters in octal
#1953 Improvement The BCG_IO parser no longer replaces double quotes by simple quotes in label strings
#1954 Improvement BCG and XTL have a new predefined type named RAW to store values of unknown types
#1955 Bug fix Label gates are now recognized by the BCG_WRITE API only if they have an identifier syntax
#1956 Improvement BCG_IO has been significantly enhanced and now supports version 2014 of the AUT format
#1957 Improvement The BCG_WRITE API uses a new type BCG_TYPE_DATA_FORMAT with its associated constants
#1958 Improvement Many internal data structures and undocumented APIs of the BCG library have been simplified
#1959 Improvement The print() function for XTL strings behaves differently, and a new printf() function was added
#1960 Improvement Many functions of the BCG dynamic libraries now pass parameters and results more efficiently
#1961 Improvement Version 1.2 of BCG no longer stores the '\0' characters that terminate STRING and RAW values
#1962 Improvement The BCG_WRITE API provides a new abort primitive to remove unfinished BCG files
#1963 Improvement Version 1.2 of BCG reduces file size with variable-length encodings for STRING and RAW values
#1964 Bug fix The "walk_print_nice" XTL library caused a GCC "zero-length gnu_printf format string" warning
#1965 Improvement The deprecated combination of options "-aldebaran -parse" for BCG_IO has been removed
#1966 Improvement When translating from BCG to BCG, BCG_IO upgrades old graphs to the latest BCG version 1.2
#1967 Improvement The XTL for quoting internal identifiers of the BCG graph has changed from `xxx` to $xxx
#1968 Bug fix XTL_EXPAND did not expand macros whose arguments contained: let, if, case, exists, or forall
#1969 Bug fix On Linux, XTL emitted warnings "comparison...always false" for BCG graphs with no transitions
#1970 Bug fix Enumerating predecessor states could loop forever on BCG graphs read with access mode 4
#1971 Improvement Using the characters '[', ']', and '|' in XTL identifiers is no longer allowed
#1972 Bug fix The XTL compiler did not type properly certain abbreviated iterators over integers
#1973 Improvement The syntax and typing rules for natural and integer numbers in XTL have been extended
#1974 Improvement XTL now warns when no label in the BCG graph has enough fields to match an XTL offer
#1975 Improvement XTL_EXPAND (and thus XTL and EVALUATOR) now warns about dubious uses of macros
#1976 Improvement Some XTL and MCL macros in demos 02, 23, 26, and 31 have been renamed to avoid warnings
#1977 Bug fix On Solaris, XTL emitted "statement not reached" warnings for BCG graphs with no transitions
#1978 Improvement Backquoted strings `...` now denote XTL values having the RAW type
#1979 Bug fix XTL could run out of memory when compiling certain incorrect XTL specifications
#1980 Improvement The format of the NUPN section in PNML files generated by CAESAR.BDD was simplified
#1981 Bug fix A bug recently introduced in the "cadp_ln" script could prevent INSTALLATOR from working
#1982 Improvement XTL now warns when no label in the BCG graph has the required type to match an XTL offer
#1983 Improvement The string notation "..." of XTL can also be used to denote values of the RAW type
#1984 Improvement XTL now examines labels of the BCG graph to better resolve typing ambiguities in XTL offers
#1985 Bug fix SVL incorrectly optimized certain nested combinations of "hide" and "cut" operators
#1986 Improvement The caesar.open script now invokes CAESAR rather than GENERATOR whenever possible
#1987 Improvement Predefined XTL libraries have been simplified and extended with new macros
#1988 Improvement Demos 16, 17, 21, 22, 23, 24, 25, 26, 27, 30, and 40 have been made simpler and more readable

2014-12-13 - Change List for CADP Version 2014-l "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1930 Improvement SVL now has four shell variables to automatically include libraries in inlined MCL and XTL formulas
#1931 Improvement The library of macros for EVALUATOR 3 and 4 has been enriched with twelve useful macros
#1932 Improvement Demos 20 and 40 have been simplified by using new SVL features and EVALUATOR macros
#1933 Improvement Memory needed to store value expressions in CAESAR and CAESAR.ADT has been reduced by 14%
#1934 Improvement Demos 01, 02, 29, 31, 34, and 39 now rely on inlined SVL properties and feature MCL V4 formulas
#1935 Bug fix Skeleton C code generated by CAESAR's "-external" option could contain incorrect calls to va_arg()
#1936 Bug fix SVL logs could display unecessary double quotes on Solaris because of a portability issue
#1937 Improvement Upon completion EXEC/CAESAR frees all allocated memory to avoid Valgrind's memory-leak warnings
#1938 Bug fix SVL generated incorrect MCL files for inlined formulas evaluated several times
#1939 Improvement LNT has been extended with a new "only if" statement to concisely express guarded commands
#1940 Bug fix At the end of smart reduction EXP.OPEN emitted wrong warnings regarding the number of BCG files
#1941 Improvement CAESAR.BDD now generates two new LaTeX macros needed for the Model Checking Contest 2015
#1942 Improvement Configuration files for a2ps, Emacs, jEdit and Vim now support the new "only if" statement of LNT

2014-11-26 - Change List for CADP Version 2014-k "Amsterdam"

HISTORY file item Type Summary
#1913 Improvement SVL has a new statement "|=" enabling MCL and XTL formulas to be inlined directly in SVL scripts
#1914 Improvement The type-survey phase of CAESAR now rejects out-of-bound constants (even unused) at compile-time
#1915 Bug fix One-value iterator generated by FSP2LOTOS caused Integer to be treated like a singleton type
#1916 Improvement The output of SVL "deadlock" and "livelock" statements has been made tool-independent
#1917 Improvement Optimization E3 of CAESAR was strengthened, leading to reductions in LTS and network sizes
#1918 Bug fix SVL and ALDEBARAN did not store in designated files the diagnostics produced by EXHIBITOR
#1919 Improvement Options -clean and -sweep of SVL now emit a warning message if no log file can be found
#1920 Bug fix Option V9 of CAESAR caused "unexpected multiple definition in a transition action" error messages
#1921 Improvement SVL no longer uses ALDEBARAN as the default tool for checking deadlocks and livelocks
#1922 Improvement A new library of useful MCL macros has been added for EVALUATOR version 3 and 4
#1923 Improvement SVL has two new statements, "property" and "check", for high-level equivalence and model checking
#1924 Improvement Optimization V2 of CAESAR has been revised and a new optimization V8 has been added
#1925 Bug fix Invoking EXHIBITOR from SVL together with CAESAR.OPEN or LNT.OPEN could lose standard input
#1926 Bug fix TGV did not work in CADP 2014-i and 2014-j due to a version number mismatch issue
#1927 Bug fix SVL "rename" statements containing "\1", "\2", etc. could fail on (32- and 64-bit) Linux
#1928 Improvement demos 20, 23, and 40 use the new "property" statement of SVL and show value-passing MCL formulas
#1929 Improvement SVL no longer stops when a "verify" or "|=" statement fails due to an incorrect MCL or XTL formula

2014-10-26 - Change List for CADP Version 2014-j "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1903 Bug fix Incorrect definition of bcg_aldebaran_gate_print() would prevent some XTL programs from compiling
#1904 Improvement Several SVL error messages have been simplified by removing information related to obsolete tools
#1905 Bug fix The EMACS configuration file for LNT was misnamed and gave incorrect coloring for assignments
#1906 Improvement The "verify" statement of SVL has a new "with" clause to specify which CADP model checker to use
#1907 Bug fix Two bugs (real, but apparently harmless) have been fixed in optimizations E3 and V9 of CAESAR
#1908 Improvement The "verify" statement of SVL has been extended to support properties expressed in XTL
#1909 Improvement Optimization V4 of CAESAR now removes guards "V1 = V2" if the sort of V1 and V2 is a singleton
#1910 Improvement A configuration file for LNT syntax highlighting and coloring in the VIM editor have been added
#1911 Improvement A new optimization V7 of CAESAR simplifies all guards of the form "V = TRUE" or "TRUE = V"
#1912 Improvement YASnippet templates have been added to enable autocompletion for LNT in EMACS

2014-09-26 - Change List for CADP Version 2014-i "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1893 Improvement The ALDEBARAN manual page was shortened by removing obsolete information about version 6.6
#1894 Improvement Option -verif of the TGV tool was simplified and the TGV manual page was enhanced
#1895 Improvement The AUT format has been generalized and a new manual page about this format has been written
#1896 Bug fix BCG_CMP could sometimes stop with error message: "cannot translate to SEQUENCE format"
#1897 Improvement The TGV tool has been made (about 5%) faster using an algorithmic optimization
#1898 Bug fix The diagnostics of BCG_CMP sometimes failed to explain why two graphs are not equivalent
#1899 Improvement The tag attached by PROJECTOR to unfirable transitions changed from ":FAIL:" to "fail:"
#1900 Improvement TGV now uses BCG_IO to read/write AUT files, thus enabling labels larger than 1024 characters
#1901 Improvement Six new scientific papers have been added to the CADP distribution and web site
#1902 Bug fix TGV did not check whether test purposes encoded in the BCG format were deterministic or not

2014-08-26 - Change List for CADP Version 2014-h "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1886 Improvement The catalog of CADP-related papers has been reorganized and made more concise
#1887 Improvement The LNT language has been enriched with a "!representedby" pragma for processes
#1888 Improvement Three new papers have been added to the documentation of CADP
#1889 Bug fix File INSTALLATION_2 and the CAESAR.ADT/CAESAR manual pages misdefined the default value of $CADP_LANGUAGE
#1890 Bug fix CAESAR and CAESAR.ADT did not properly embed certain command-line options in the generated C code
#1891 Bug fix Since CADP 2014-g, the BCG tools have been emitting "incompatible pointer types passing" warnings on Mac OS X
#1892 Bug fix On Mac OS X 10.8 and higher, BCG_DRAW did not display PS files ("Preview: converting PS failed" error)

2014-07-13 - Change List for CADP Version 2014-g "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1866 Improvement SVL now accepts LNT-style comments "-- ..." in addition to LOTOS-style comments "(* ... *)"
#1867 Improvement SVL now accepts LNT-style "end hide", "end rename", "end cut", and "end prio" keywords
#1868 Improvement BCG_CMP no longer displays an empty line before its TRUE/FALSE verdicts
#1869 Improvement Two obscure warnings emitted by SVL have been clarified
#1870 Improvement SVL now accepts LNT-style channel identifiers in its "hide" and "cut" operators
#1871 Improvement CAESAR.BDD "-mcc" and "-vlpn" options follow the new conventions of the Model Checking Contest
#1872 Improvement The LNT library was enriched was eight predefined operations on character-type values
#1873 Improvement The SVL scripts of demos 18, 28, 29, 30, 32, and 35 have been upgraded to adopt the LNT style
#1874 Improvement The demos 14 and 15 (Plain Old Telephony System) have been simplified and one equation corrected
#1875 Improvement CAESAR and CAESAR.ADT implement relaxed rules to bind sorts at LOTOS specification top level
#1876 Improvement The definitions of types ADT_CHAR and BCG_TYPE_BOOLEAN have been made uniform
#1877 Improvement The label parsing algorithm of BCG_WRITE now recognizes character-type values
#1878 Bug fix LNT2LOTOS emitted wrong "not used later" warnings for variables assigned just before "end hide"
#1879 Improvement The demos 14 and 15 have been translated to LNT and demo 15 was merged into demo_14
#1880 Bug fix BCG_EXPAND did not properly handle both escape sequences \\ and \"
#1881 Bug fix LNT2LOTOS evaluated in the wrong order the various predicates related to LNT rendezvous
#1882 Improvement Six new include files help handling predefined types uniformly across LOTOS, LNT, BCG, and XTL
#1883 Improvement Character-type values contained in BCG files are now printed exactly as those of LNT specifications
#1884 Improvement LNT string-type values stored in OPEN/CAESAR tables are now printed exactly as ordinary strings
#1885 Improvement BCG_GRAPH now handles particular cases where there are no labels, or the bag or fifo size is zero

2014-06-13 - Change List for CADP Version 2014-f "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1844 Improvement The obsolete scripts EXP2FC2 and XEUCA_FC2INFO have been removed from CADP
#1845 Improvement The LNT2LOTOS Reference Manual has been updated and enhanced at many places
#1846 Bug fix LNT hexadecimal constants 0xA...0xF caused run-time errors if NAT or INT types were 16-bit large or more
#1847 Bug fix LNT least integer -2^(N-1), where N is the number of bits of the INT type, caused a run-time error
#1848 Improvement The "toolspecific" attributes of PNML files generated by CAESAR.BDD have been simplified
#1849 Improvement The printing function for the LNT CHAR type now handles nonprintable characters properly
#1850 Improvement LNT_CHECK no longer emits warnings for certain functions containing several "return" statements
#1851 Improvement The OPEN/CAESAR and LNT2LOTOS Reference Manuals now contain PDF links that ease navigation
#1852 Improvement LNT2LOTOS now rejects those LNT functions containing infinite loops without "break" or "return"
#1853 Improvement LNT2LOTOS performs less demanding filename checks when an LNT module is named "TEST"
#1854 Improvement The messages displayed by LNT.OPEN have been made much more concise
#1855 Improvement The SVL scripts of CADP demos now use $DEFAULT_PROCESS_FILE rather than $DEFAULT_LOTOS_FILE
#1856 Bug fix LNT2LOTOS generated wrong LOTOS code when a "case" variable had the same name as an outer variable
#1857 Improvement The "-root P" option LNT.OPEN now works even if process P is not defined in the principal module
#1858 Bug fix LNT2LOTOS could emit spurious "X unused" warnings for "case" branches of the form "P (X) where C (X)"
#1859 Bug fix LNT2LOTOS could generate mistyped LOTOS code for expressions "V of T" with T range or predicate type
#1860 Improvement demo_18 (Transit Node message router) has been cleaned up and translated to LNT
#1861 Improvement LNT2LOTOS now emits a warning if an "inout" process parameter is never assigned in that process
#1862 Bug fix LNT2LOTOS evaluated rendezvous Boolean guards and channel typing predicates in the wrong order
#1863 Improvement The printing function for the LNT STRING type now handles nonprintable characters properly
#1864 Improvement SVL now accepts filenames in multiple directories (i.e., filenames that may contain "/")
#1865 Improvement LNT2LOTOS now emits a warning if an "inout" function parameter is never assigned in that function

2014-05-13 - Change List for CADP Version 2014-e "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1827 Improvement ALDEBARAN now invokes BCG_CMP rather than BISIMULATOR whenever it is possible
#1828 Improvement The BPN (Basic Petri Net) format of CAESAR.BDD has been renamed into NUPN (Nested-Units Petri Nets)
#1829 Improvement A new option "-exclusive-places" has been added to CAESAR.BDD
#1830 Improvement LNT2LOTOS now warns about unused variables in "case" statements of LNT processes
#1831 Bug fix LNT2LOTOS did not generate all LOTOS operations needed for external infix LNT functions
#1832 Improvement Modified "!multiple_initial_tokens" pragma allowed to enhance CAESAR.BDD options "-mcc" and "-vlpn"
#1833 Bug fix CAESAR.BDD wrongly computed strongly connected components in presence of multiple initial tokens
#1834 Bug fix LNT2LOTOS could emit false positives when determining unused "in" and "inout" function parameters
#1835 Improvement Options "-mcc" and "-vlpn" of CAESAR.BDD give more precise results for Live and Reversible properties
#1836 Improvement LNT2LOTOS now warns about certain local variables assigned in LNT functions and not used later
#1837 Improvement The input language of LNT2LOTOS is now officially called "LNT" rather than "LOTOS NT"
#1838 Bug fix The X_NATURAL and X_INTEGER libraries did not perform overflow/underflow checking correctly
#1839 Improvement Overflow/underflow checks for naturals and integers are now activated by default in LNT2LOTOS
#1840 Improvement The demo 12 has been enhanced in various ways and now includes overflow/underflow checking
#1841 Improvement The EXECUTOR tool has been equipped with "-hide" and "rename" options
#1842 Bug fix INSTALLATION_MACOS directives for setting a static hostname on Mac OS X 10.6 - 10.7 did not work
#1843 Improvement The LNT Reference Manual was shortened by 32 pages by moving its Appendix F to the HISTORY file

2014-04-13 - Change List for CADP Version 2014-d "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1812 Improvement Options "-mcc" and "-vlpn" of CAESAR.BDD now compute behavioural properties
#1813 Improvement LNT2LOTOS now warns about useless assignments to variables in LNT processes
#1814 Bug fix In presence of several initial places, CAESAR.BDD miscomputed dead places and transitions
#1815 Improvement Option "-check" of CAESAR.BDD now displays the number of reachable markings at each iteration
#1816 Improvement OPEN/CAESAR and EXEC/CAESAR define CAESAR_TYPE_BOOLEAN as unsigned rather than signed
#1817 Bug fix CADP_CC could not find strtof() function when linking with old versions 2.5 and 2.7 of Glibc
#1818 Improvement DECLARATOR now properly catches interrupt signals
#1819 Improvement CAESAR.BDD now recovers from interrupt signals and premature termination
#1820 Bug fix TST did not completely solve the PTRACE issue with Yama on Ubuntu
#1821 Bug fix On Ubuntu, the title bar of EUCALYPTUS was displayed using an oversized font
#1822 Improvement Execution time of CAESAR.BDD can be bound using environment variable $CAESAR_BDD_TIMEOUT
#1823 Improvement The filename following the "-mcc" option of CAESAR.BDD has become optional
#1824 Improvement LNT2LOTOS now warns about local variables declared in LNT functions but never used
#1825 Bug fix LPP was missing a "-more" option that ought to be set upon invocation by LNT.OPEN
#1826 Improvement LNT_DEPEND displays better error messages for circular or missing module dependencies

2014-03-13 - Change List for CADP Version 2014-c "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1790 Improvement LNT2LOTOS now warns about local variables declared in LNT processes but never used
#1791 Improvement The predefined types and functions of XTL can now be used to define temporal operators directly in C
#1792 Improvement LNT2LOTOS no longer emits two redundant warnings about "i" gates in synchronization lists
#1793 Improvement CAESAR.BDD implements stricter static semantics checks on the BPN format
#1794 Improvement LNT2LOTOS avoids C warning "comparison of unsigned expression >= 0 is always true" for range types
#1795 Improvement CAESAR.BDD supports the extension of the BPN format to initial markings containing several places
#1796 Improvement LNT2LOTOS no longer emits redundant messages for functions with only "in" parameters and no result
#1797 Improvement The "-check" option of CAESAR.BDD statically and dynamically checks if reachable markings are unit-safe
#1798 Improvement Three simplifications have been brought to the LOTOS code generated by LNT2LOTOS
#1799 Improvement LNT2LOTOS avoids C warning "comparison is always false..." for LNT range types with a single element
#1800 Improvement LNT2LOTOS now warns about certain local variables assigned in LNT processes and not used later
#1801 Bug fix On Mac OS X and Windows, some CADP tools could display "no_address instead of no_address" and halt
#1802 Improvement One can now write "||" for action products (rather than "*") in EXP synchronization vectors
#1803 Improvement CAESAR and CAESAR.ADT now perform type inference for the value parameters of LOTOS processes
#1804 Improvement EXP2C generates better messages that help users to understand how smart reduction proceeds
#1805 Improvement LNT2LOTOS avoids C warnings for LNT arrays having only one element
#1806 Improvement EXP2C provides more explanative messages when some synchronizations of actions are impossible
#1807 Improvement CAESAR and CAESAR.BDD implement the four pragmas recently introduced in the BPN format
#1808 Improvement When possible, EXP2C avoids introducing auxiliary labels that make it difficult to follow smart reduction
#1809 Bug fix The "-unit" option of CAESAR.BDD could produce results differing from those stated in the manual page
#1810 Bug fix LNT2LOTOS could generate incorrect LOTOS code later rejected by CAESAR and CAESAR.ADT
#1811 Bug fix The EUCALYPTUS graphical user-interface could freeze if LNT2LOTOS would emit too many messages

2014-02-13 - Change List for CADP Version 2014-b "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1772 Bug fix On Windows TST could fail locating the C compiler when $CADP_CC was set and CADP not installed
#1773 Bug fix On Mac OS X with MallocScribble, option -diag of BCG_CMP could stop without generating diagnostics
#1774 Improvement CAESAR uses 4 byte less per place and per transition (32 bits) and 8 byte less per transition (64 bits)
#1775 Improvement CAESAR.ADT generates shorter, better C code by recognizing "V = V =>" equation premisses
#1776 Improvement LNT2LOTOS generates simpler LOTOS code for predicate types, "card" functions, and channel checks
#1777 Improvement LNT2LOTOS now emits warnings about unused "in" or "inout" function parameters
#1778 Improvement LNT2LOTOS produces LOTOS code that no longer causes "unused parameter" warnings from gcc -Wall
#1779 Improvement Optimization E1 of CAESAR now detects and removes disconnected or unreachable network parts
#1780 Improvement CAESAR.BDD now handles Basic Petri Nets, the root unit of which has no places
#1781 Improvement The -check and -vlpn options of CAESAR.BDD have been enhanced and a new -mcc option was added
#1782 Bug fix Option -diag of BCG_CMP could do segmentation faults or generate incomplete diagnostics
#1783 Improvement The syntax of the "par" operator in SVL and EXP languages was aligned on the "par" syntax in LNT
#1784 Bug fix LNT2LOTOS could generate incorrect LOTOS specifications rejected by CAESAR and CAESAR.ADT
#1785 Bug fix On Solaris EXP2C silently ignored the "priority" operator of the EXP language
#1786 Improvement LNT2LOTOS now emits warnings about unused "in" or "inout" process parameters
#1787 Bug fix LNT2LOTOS now emits an error when a gate occurs twice in a "par" synchronization list
#1788 Improvement LNT2LOTOS now emits a warning when a gate occurs in only one "par" synchronization list
#1789 Improvement CAESAR optimally handles true and false conditions in LOTOS action prefixes and guards

2014-01-13 - Change List for CADP Version 2014-a "Amsterdam"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1761 Bug fix On Ubuntu TST emitted a warning with an incorrect pathname "/bin/sysctl"
#1762 Improvement SVL emits further warnings when a user-given interface is incorrect
#1763 Improvement CAESAR.BDD better checks BPN files and breaks long lines in its PNML output
#1764 Improvement CADP support for Sparc, Itanium, and PowerPC processors is discontinued
#1765 Improvement CADP_INDENT better recovers from crashes of the "indent" programs
#1766 Improvement LNT2LOTOS avoids generating LOTOS files with lines longer than 2500 chars
#1767 Bug fix LNT_DEPEND emitted "tr: Illegal byte sequence" on Mac OS X "Snow Leopard"
#1768 Bug fix BCG_MIN with -observational and -class crashed in absence of internal action
#1769 Bug fix The -class option of BCG_MIN could produce incorrect class information
#1770 Improvement Outdated LOTOS examples have been moved to a new folder "demos/archive"
#1771 Bug fix LNT.OPEN no longer emits irrelevant warnings about deadlock on "exit" gates

2013-12-13 - Change List for CADP Version 2013-l "Zurich"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

This version of CADP will be the last one for Sparc, Itanium, and PowerPC processors (i.e., architectures "sun5", "sun64", "ia64", and "macOS"). Support for these architectures will be discontinued in 2014. The few persons still using CADP on these architectures will be notified individually by e-mail.

HISTORY file item Type Summary
#1747 Improvement Changed the C code generated by XTL to avoid a CLANG "-Wparentheses-equality" warning on mac86
#1748 Bug fix In SVL, hiding was improperly propagated under the LNT generalized parallel composition operator
#1749 Improvement Made CAESAR.BDD slightly faster, enhanced its error messages, and introduced a new "-check" option
#1750 Bug fix LNT2LOTOS wrongly translated "case"s in processes if the Nat type domain had been restricted too much
#1751 Bug fix LNT_DEPEND emitted "unsupported option -n" warnings on Mac OS X 10.6
#1752 Bug fix LNT2LOTOS could generate incorrect LOTOS code for LNT processes with no gate parameters
#1753 Improvement All C functions corresponding to LOTOS operations on natural numbers are now suffixed with "_NAT"
#1754 Improvement LOTOS types IntegerNumber and Integer are no longer identical and now have different signatures
#1755 Improvement Added "div", "mod", and "rem" operations on integers in the predefined LOTOS and LNT libraries
#1756 Improvement Added new tool BCG_CMP providing fast comparison for LTSs and discrete/continuous-time Markov chains
#1757 Improvement Enhanced the "Compare..." menu of the EUCALYPTUS user interface to support the new BCG_CMP tool
#1758 Improvement Option "-class" of BCG_MIN can (and must) now be followed by a filename (or "-" for standard output)
#1759 Improvement Extended the SVL language and compiler to support the new BCG_CMP tool
#1760 Bug fix LNT2LOTOS produced misleading error messages for undeclared gates G used as folows: "G (...) where ..."

2013-11-13 - Change List for CADP Version 2013-k "Zurich"

Acknowledgements are due to the following scientists, who provided valuable feedback taken into account for this version of CADP:

HISTORY file item Type Summary
#1724 Bug fix Option "-iso" of CAESAR did not deactivate the "(*! atomic *)" special comments
#1725 Improvement Changed LNT2LOTOS translator to avoid GCC 4.* warnings ("variable "CAESAR_REGISTER_..." set but not used")
#1726 Bug fix The SVL script of demo_32 contained a tautological comparison ("scenario_S3.bcg" == "scenario_S3.bcg")
#1727 Bug fix The LNT exponentiation operator "**" on real numbers was incorrectly implemented
#1728 Improvement Modified CAESAR and CAESAR.ADT not to emit useless "cascading" type-error messages for undeclared variables
#1729 Improvement CAESAR and CAESAR.ADT emit better error messages for mistyped value expressions in "let" and "ofsort" contexts
#1730 Improvement CAESAR and CAESAR.ADT emit better error messages for non-Boolean guards with a non-declared TRUE operator
#1731 Improvement RFL and INSTALLATOR have been made faster by trying ssh/scp before rsh/rcp
#1732 Improvement New options "-parse" and "-unparse" have been added to GENERATOR to enable/disable BCG label parsing
#1733 Bug fix Type-checking errors for LOTOS equation lists were printed in reverse order by CAESAR and CAESAR.ADT
#1734 Bug fix LNT2LOTOS generated mistyped LOTOS code for patterns containing a constructor of range or predicate type
#1735 Bug fix SVL recovered improperly when the strong minimization of an EXP composition expression failed
#1736 Improvement Entirely revised INSTALLATION_MACOS directives for installing CADP on Mac OS X, adding support for XCode 5.0.1
#1737 Bug fix RFL and TST emitted "expr: syntax error ... [: too many arguments" on Mac OS X
#1738 Improvement Changed the C code generated by CAESAR to avoid a CLANG "-Wparentheses-equality" warning on mac86
#1739 Improvement More explanative error messages for LNT programs containing mistyped gates
#1740 Improvement Modified CADP_CC to remove two CLANG "argument unused" warnings about "-fno-tree-sra" and "-multiply_defined"
#1741 Improvement Changed LNT2LOTOS and its library to avoid GCC 4.2 warnings ("unknown option after '#pragma GCC diagnostic' kind")
#1742 Improvement Added observational equivalence reduction to BCG_MIN and restored ALDEBARAN's "-omin" and "-ocla" options
#1743 Improvement Faster BCG_MIN (linear instead of quadratic complexity in a subroutine) for graphs with a high branching factor
#1744 Bug fix Semantic bug in CAESAR_SOLVE's algorithm A1, causing incorrect results by EVALUATOR 3 and 4 with "-bfs" option
#1745 Improvement Modified CADP_MEMORY to avoid a "dyld: DYLD_ ... is setuid or setgid" warning on Mac OS X 10.8 "Mountain Lion"
#1746 Improvement Ported INSTALLATOR and TST to Mac OS X 10.9 "Mavericks", from which "/usr/bin/gnutar" has been removed

Previous versions

Former changes to CADP (items ranging from #001 to #1723) are described in the HISTORY file of the CADP distribution.


Version 1.98 last updated on 2017/02/16 16:29:27

Back to the CADP Home Page