CADP Change List

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.

2025年11月13日 - Change List for CADP Version 2025-k "Montreal"

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

HISTORY file item Type Summary
#3227 Improvement It is no longer mandatory to insert "of T" clauses in all overloaded LNT communication offers
#3228 Bug fix On Windows (with Cygwin), the "-clean" option of SVL sometimes omitted erasing certain files
#3229 Improvement SVL displays helpful messages if BCG_CMP or BCG_MIN abort due to large branching factors
#3230 Improvement The CADP style files for LaTeX listings now display the "->" symbols in a visually better way
#3231 Improvement Five CADP demos were simplified by removing useless "of" clauses in communication offers
#3232 Improvement The "!library" pragmas of LNT now apply only to the files in which they are directly present
#3233 Bug fix TRAIAN could reject LNT increment/decrement statements with event lists containing "..."
#3234 Improvement Three scripts for LNT were simplified by removing the $LNT_LOCATION environment variable
#3235 Improvement TRAIAN emits warnings about LNT functions that are never called (or never "really" called)
#3236 Improvement Twenty CADP demos were modified to avoid TRAIAN's warnings about useless LNT functions
#3237 Improvement LNT supports "!library" pragmas attached to specific channels, functions, processes, and types
#3238 Bug fix LNT2LOTOS could generate wrong LOTOS code for communication offers with "where" clauses

2025年10月13日 - Change List for CADP Version 2025-j "Montreal"

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

HISTORY file item Type Summary
#3210 Improvement TRAIAN reports "out" and "in out" function / process parameters that are never "really" used
#3211 Improvement Naming conventions in LNT2LOTOS ".fnt" / ".tnt" files have been further aligned with TRAIAN
#3212 Improvement LNT2LOTOS translated LNT functions named "!=" to "/=", at the risk of causing name clashes
#3213 Improvement Channels never employed (i.e., channels defined but not used) are now detected by TRAIAN
#3214 Improvement CAESAR, CAESAR.ADT, and EXP.OPEN no longer use the deprecated file "caesar_prototype.h"
#3215 Improvement TRAIAN now forbids C identifiers starting with the "CAESAR_" (in addition to "TRAIAN_") prefix
#3216 Improvement LNT has a new "!library" pragma to inhibit warnings about unused channels / processes / types
#3217 Improvement LNT types never employed (i.e., types defined but not used) are now detected by TRAIAN
#3218 Improvement LNT processes never called (i.e., processes defined but not used) are now detected by TRAIAN
#3219 Bug fix The "-dfs" option of EXHIBITOR was no longer working since CADP 2025-h (August 13, 2025)
#3220 Bug fix LNT2LOTOS generated iteration macros for "range" and "where" (i.e., predicate) types only
#3221 Bug fix LNT2LOTOS mistranslated some "where" clauses in LNT patterns containing non-constructors
#3222 Improvement LNT2LOTOS now accepts LNT module names (case-insensitively) identical to a LOTOS keyword
#3223 Improvement Ten CADP demos have been revised to avoid TRAIAN's new warnings about useless definitions
#3224 Improvement LNT2LOTOS implements field update functions with extra premisses to avoid a Clang warning
#3225 Bug fix The potential continuations located after a "trap" were not taken into account by LNT2LOTOS
#3226 Bug fix LNT2LOTOS wrongly translated communications E (X -> ?C), where C is a nullary constructor

2025年09月13日 - Change List for CADP Version 2025-i "Montreal"

HISTORY file item Type Summary
#3194 Bug fix Various changes have been brought to increase the portability of CADP to the "sol64" architecture
#3195 Improvement The predefined library of LNT was enriched with * and ** functions that may raise exceptions
#3196 Improvement The C code for the LNT strings was revised to avoid Clang's "-Winvalid-source-encoding" warnings
#3197 Bug fix On a few Linux laptops, the CADP license did not work if the laptop was connected to the network
#3198 Bug fix LNT_MERGE failed to search LNT libraries (such as BIT.lnt and OCTET.lnt) in directory $CADP/lib
#3199 Improvement The translation algorithm of LNT2LOTOS is now able to handle a larger class of LNT "par" operators
#3200 Bug fix LNT2LOTOS produced syntactically wrong LOTOS code for LNT programs with external types only
#3201* Improvement Naming conventions in ".fnt" / ".tnt" files for LNT2LOTOS have been aligned with those of TRAIAN
#3202 Improvement The two predefined libraries BIT.lnt and OCTET.lnt have been enriched with nine new functions
#3203 Improvement Conversion functions from Bool to Nat / Int / Real have been added to the predefined library of LNT
#3204 Bug fix The predefined library of LNT caused Gcc "-Wformat" warnings when enlarging the ADT_NAT type
#3205 Improvement TRAIAN emits new warnings for function/process event parameters that are never "really" accessed
#3206 Improvement Backward-compatibility code introduced in 2011 was removed from the predefined library of LNT
#3207 Bug fix LNT2LOTOS translated LNT functions named "=" to "==", potentially causing LOTOS name clashes
#3208 Improvement TRAIAN also emits new warnings for function/process "in" parameters that are never "really" used
#3209 Improvement LNT2LOTOS now supports calls to external processes with ellipses in their list of event parameters

2025年08月13日 - Change List for CADP Version 2025-h "Montreal"

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

HISTORY file item Type Summary
#3172 Improvement INSTALLATOR now mentions cadp.inria.fr rather than ftp.inrialpes.fr in its messages
#3173 Bug fix LNT2LOTOS generated wrong LOTOS code for patterns calling FIRST/LAST functions
#3174 Bug fix Running TGV with "-verif" and "-verbose" options displayed wrong transition numbers
#3175 Improvement The LNT2LOTOS translator now partially implements the "trap" statements of LNT
#3176 Improvement The command-line syntax for launching TGV is now simpler and more user-friendly
#3177 Bug fix SVL looped forever on the "par {$X} in ... end par" clause of the demo_33 of CADP
#3178 Improvement TRAIAN emits more warnings for LNT loops whose condition is always false or true
#3179 Bug fix LNT2LOTOS mishandled certain !implementedby "LOTOS:special-identifier" pragmas
#3180 Improvement The SVL language supports "end abstraction", "end generation", and "end reduction"
#3181 Improvement Given "type T1 is range ... of T2", LNT now generates a function T1: [Exit] T2 -> T1
#3182 Improvement The LNT library now offers 10 overloaded versions of the concatenation operator "&"
#3183 Improvement The OPEN/CAESAR manual pages were updated to use new-style function prototypes
#3184 Improvement The "caesar_table_1" library of OPEN/CAESAR was both simplified and enhanced
#3185 Improvement The predefined VAL() function on LNT range types was removed as it was little used
#3186 Improvement MCL_EXPAND produces new-style C function prototypes to avoid Clang-19 warnings
#3187 Improvement The predefined library of LNT now implements 4 new functions on Nat and Int types
#3188 Improvement XTL avoids warnings from Clang-19 by producing new-style C function prototypes
#3189 Improvement The EXEC/CAESAR and OPEN/CAESAR files now use new-style C function prototypes
#3190 Improvement LNT no longer offers the Real: [Exit] Nat -> Real and Real: [Exit] Int -> Real functions
#3191 Improvement EXP2C, CAESAR, and LNT2LOTOS now generate C code with new-style prototypes
#3192 Improvement LNT now supports predefined (unary or binary) "+" and "-" functions on range types
#3193 Improvement Demos 02, 12, 19, 31, and 38 have been updated to use new-style function prototypes

2025年07月13日 - Change List for CADP Version 2025-g "Montreal"

HISTORY file item Type Summary
#3156 Improvement The demo_01 of CADP was archived, since it was too simple and subsumed by demo_02
#3157 Improvement The data-flow analyses of TRAIAN better takes into account the existence of dead code
#3158 Bug fix A few typing errors were fixed in X_STRING.h and the C code generated by CAESAR.ADT
#3159 Bug fix For strings in patterns, LNT2LOTOS produced LOTOS code found wrong by CAESAR.ADT
#3160 Improvement LNT2LOTOS no longer rejects functions having only "in" parameters and no return type
#3161 Bug fix TRAIAN halted on function/process calls with "..." covering "in var"/"out var" parameters
#3162 Improvement Some LOTOS and C code generated by LNT2LOTOS was moved to LNT_V1.lib/LNT_V1.h
#3163 Improvement The demo_02 of CADP (alternating bit protocol) has been translated from LOTOS to LNT
#3164 Improvement TRAIAN emits more warnings about redundant "access" instructions in "trap" operators
#3165 Improvement The SVL files of 8 demos use the parallel operators of LNT rather than those of LOTOS
#3166 Improvement TRAIAN now recognizes false guards when analyzing exhaustiveness of "case" patterns
#3167 Improvement Test-case generation features using the TGV tool have been added to demo_02 of CADP
#3168 Improvement LNT now has predefined FIRST and LAST functions for types BOOL, NAT, INT, and CHAR
#3169 Improvement The data-flow analysis of TRAIAN recognizes "for" / "while" loops with false conditions
#3170 Improvement LNT2LOTOS now implements 23 predefined LNT functions that might raise exceptions
#3171 Improvement The "-csg" option of TGV (an acronym for "Complete Sub-Graph") was renamed to "-all"

2025年06月13日 - Change List for CADP Version 2025-f "Montreal"

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

HISTORY file item Type Summary
#3138 Improvement The include file caesar_prototype.h, no longer useful, is now deprecated
#3139 Bug fix Two defects have been fixed in the win64 (Cygwin) version of CADP
#3140 Bug fix LNT2LOTOS issued unreadable messages about nonexistent included files
#3141 Improvement EVALUATOR, MCL_EXPAND, and XTL have been made compliant with C23
#3142 Improvement All CADP compilers have been upgraded to use the 2025 version of SYNTAX
#3143 Bug fix MCL_EXPAND could wrongly warn about unused variables in MCL V5
#3144 Improvement The C code generated by MCL_EXPAND could trigger compiler warnings
#3145 Improvement The data-flow analysis of TRAIAN for array assignments is now more precise
#3146 Bug fix EVALUATOR could abort when printing BESs with multiple equation blocks
#3147 Bug fix TRAIAN could core dump on very long file names, e.g., in "module" clauses
#3148* Improvement Passing an "in out" parameter X in LNT is now noted "X?" instead of "!?X"
#3149 Improvement The source code of all CADP tools complies with the C23 revision of ISO C
#3150 Bug fix Syntax-error recovery could lead TRAIAN to emit non-intuitive messages
#3151 Improvement TRAIAN now warns about irrelevant "require" clauses in LNT programs
#3152 Improvement TRAIAN also warns about meaningless "ensure" clauses in LNT programs
#3153 Improvement LNT now has MIN and MAX functions on Bool, Char, Real, and String types
#3154 Improvement "with MIN" and "with MAX" functions are now supported on all LNT types
#3155 Improvement LNT now supports "with INF" and "with SUP" functions for lists and sets

2025年05月13日 - Change List for CADP Version 2025-e "Montreal"

HISTORY file item Type Summary
#3130 Improvement The symbolic link CAESAR.OPEN, which had been deprecated since 2020, was removed
#3131 Bug fix A bug was fixed in LNT2LOTOS's translation of "for...until" loops with "break" in processes
#3132 Improvement All macros CAESAR_ARG_n() have been removed from the OPEN/CAESAR interface files
#3133* Improvement The LNT language was simplified by removing the ".." symbol, merged with the "..." symbol
#3134 Improvement All macros CAESAR_PROMOTE_TO_INT() were removed from OPEN/CAESAR interfaces
#3135 Improvement The LNT language was enriched with incrementation/decrementation instructions (+= and -=)
#3136 Improvement MCL_EXPAND warns about variables defined but not used in MCL value-passing formulas
#3137 Improvement New functional types have been introduced in some OPEN/CAESAR programming interfaces

2025年04月13日 - Change List for CADP Version 2025-d "Montreal"

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

HISTORY file item Type Summary
#3115 Improvement The "-root" options of LNT2LOTOS and LNT.OPEN have been renamed to "-main"
#3116 Improvement All occurrences of "lotosnt" and "lotnt" in CADP file names have been removed
#3117 Improvement The "-root" options of CAESAR and CAESAR.OLD have been renamed to "-main"
#3118 Improvement All error messages in data type libraries have been aligned with those of TRAIAN
#3119 Improvement The LNT language was extended with "!virtual" functions for parameterization
#3120 Improvement The "-root" options of FSP2LOTOS and FSP.OPEN have been renamed to "-main"
#3121 Improvement EXP2C is considerably faster when handling priorities on LTSs having many labels
#3122 Improvement Ten functions in LOTOS/LNT data type libraries now halt when called improperly
#3123 Improvement Four obsolete functions have been removed from LOTOS/LNT data type libraries
#3124* Improvement TRAIAN now warns when the deprecated "select" keyword is used in place of "alt"
#3125 Improvement The BCG include files have been simplified by removing all BCG_ARG_n() macros
#3126 Improvement The LNT language has a new "for...until" loop adapted to enumerated/range types
#3127 Improvement The BCG tools and 70% of CADP tools now comply with the C23 revision of ISO C
#3128 Bug fix The code produced by LNT2LOTOS called a function with 1 argument instead of 2
#3129 Improvement LNT floating-point values are now printed with a larger number of decimal digits

2025年03月13日 - Change List for CADP Version 2025-c "Montreal"

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

HISTORY file item Type Summary
#3102 Improvement The CADP distribution can now be downloaded using HTTPS or HTTP (in addition to FTP)
#3103 Improvement On entire LNT programs, TRAIAN warns about virtual declarations with no actual processes
#3104 Improvement SVL scripts can be run directly from the command line using Unix's shebang mechanism
#3105 Improvement The DELETE and REMOVE functions of TRAIAN's list and set schemes use less memory
#3106 Improvement From now on, SVL directly displays the output of the last executed command that failed
#3107 Improvement In TRAIAN's set scheme, the INTER and UNION functions are now more memory-efficient
#3108 Improvement TRAIAN reports useless virtual declarations when the actual processes are already present
#3109 Bug fix Ellipses ("...") could be omitted in TRAIAN's error messages about mistyped process calls
#3110 Improvement The ambiguous "errors or warnings" messages from SVL have been made more precise
#3111 Bug fix TRAIAN performs stricter checks on !implementedby "LOTOS:..." pragmas for LNT processes
#3112 Improvement INSTALLATOR now uses HTTPS or HTTP for downloads-uploads, as an alternative to FTP
#3113 Bug fix When translating an LNT function named ">>", LNT2LOTOS generated invalid LOTOS code
#3114 Improvement INSTALLATOR no longer displays many-digit fractional numbers for available disk space

2025年02月14日 - Change List for CADP Version 2025-b "Montreal"

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

HISTORY file item Type Summary
#3087 Bug fix CAESAR_SOLVE_1 produced huge BES files for some MCL4 fixpoint formulas
#3088 Bug fix On Windows only, BCG_CMP displayed its "FALSE" or "TRUE" verdict twice
#3089 Bug fix LNT2LOTOS generated wrong LOTOS code for any LNT constructor named "="
#3090 Improvement On Windows, CADP_EDIT tries to replace Wordpad and Write with Notepad
#3091 Improvement LNT2LOTOS generates much smaller LOTOS code for "ord" and "val" functions
#3092 Improvement The CADP_EDIT script searches whether the Sublime Text editor is available
#3093 Improvement TRAIAN and LNT2LOTOS now require that module pragmas appear firstly
#3094 Bug fix TRAIAN and LNT2LOTOS lexically rejected some special identifiers of LNT
#3095 Improvement LNT2LOTOS is now aligned with TRAIAN for interpreting expressions F [E]
#3096 Improvement TRAIAN has a "-main" option to select an entry-point process not called MAIN
#3097 Improvement LNT2LOTOS now thoroughly checks the argument passed to its "-root" option
#3098 Bug fix CAESAR and CAESAR.ADT lexically rejected some special identifiers of LOTOS
#3099 Improvement The LNT2LOTOS Reference Manual was enriched with didactic LNT examples
#3100 Improvement The panes of the EUCALYPTUS graphical user interface can now be resized
#3101 Improvement MCL and XTL have been extended to accept line-comments starting with "--"

2025年01月13日 - Change List for CADP Version 2025-a "Montreal"

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

HISTORY file item Type Summary
#3077 Improvement INSTALLATOR now detects when it is launched on a wrong architecture
#3078 Improvement CADP has been ported to macOS 15 "Sequoia" and Xcode version 16.1
#3079 Improvement The C code generated by CAESAR.ADT now uses C23 function prototypes
#3080 Improvement TRAIAN was upgraded to version 3.16, bringing better static verification
#3081 Improvement LNT2LOTOS now supports TRAIAN's "library" directive for file inclusion
#3082 Improvement Four corrections and code simplifications have been brought to demo_10
#3083 Improvement demo_17 was revised to obey static semantics rules for virtual processes
#3084 Improvement The CADP style files for Sublime Text (in ext directory) have been enhanced
#3085 Bug fix Two minor issues have been fixed in the win64 version of CADP for Cygwin
#3086 Improvement The ext directory of CADP now provides an extension for Visual Studio Code

2024年12月13日 - Change List for CADP Version 2024-l "Eindhoven"

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

HISTORY file item Type Summary
#3065 Bug fix SVL did wrong "[root] leaf" reduction for "par" operators in "partial/total hide"
#3066 Improvement Version 3.16 beta 7 of TRAIAN checks whether LNT modules are self-contained
#3067 Improvement Demos 10, 11, 27, 38, and 39 were modified to have self-contained modules only
#3068 Bug fix Given an incorrect LNT file as input, LNT_MERGE displayed no error message
#3069 Bug fix LNT2LOTOS generated invalid C code for range bounds containing underscores
#3070 Improvement The LPP preprocessor was removed after moving its functionality to LNT2LOTOS
#3071 Improvement SVL now supports condensed notations "prio [all but] ..." for priority operators
#3072 Improvement The "-pidlist" option of LNT2LOTOS was removed and transferred to TRAIAN
#3073 Improvement The "whatis" file of CADP man pages was shortened and the "windex" file removed
#3074 Improvement The demo_24 (Web services for negotiation) was translated from LOTOS to LNT
#3075 Improvement The LNT language was extended with "!virtual" processes for parameterization
#3076 Improvement The BCG MONITOR now permits changes of font size and saves user preferences

2024年11月13日 - Change List for CADP Version 2024-k "Eindhoven"

HISTORY file item Type Summary
#3047 Improvement From now on, LNT2LOTOS should only be invoked on correct LNT programs
#3048 Improvement LNT2LOTOS no longer generates extra LOTOS code for checking channel types
#3049 Bug fix LNT2LOTOS rejected underscores in LNT identifiers: 0_1A, 0_23, 0_x4, 19_23, etc.
#3050 Bug fix LNT2LOTOS generated wrong code for "with get/set" clauses of predicate types
#3051 Improvement The LNT2LOTOS parser has been extended to support events of the form E()
#3052 Improvement LNT2LOTOS syntactically accepts patterns of the form "P where V" everywhere
#3053 Bug fix The code generated by LNT2LOTOS sometimes lacked infixed "INSERT" functions
#3054 Bug fix LNT2LOTOS generated wrong code for function P ... !implementedby "LOTOS:P"
#3055 Improvement At present, LNT2LOTOS no longer rejects type T ... !implementedby "LOTOS:T"
#3056 Improvement The "-pidlist" option of LNT2LOTOS no longer creates the LNTGEN directory
#3057 Bug fix LNT2LOTOS generated wrong code for process P ... !implementedby "LOTOS:P"
#3058 Improvement TRAIAN was upgraded to version 3.16 beta 5, bringing numerous enhancements
#3059 Improvement The "-depend" option of LNT_DEPEND has been superseded by that of TRAIAN
#3060 Improvement LNT_MERGE now properly checks whether all included LNT files can be found
#3061 Improvement The EVALUATOR 3 model checker is now replaced everywhere by EVALUATOR 4
#3062 Improvement The LNT_DEPEND tool, now useless, was removed from the CADP distribution
#3063 Improvement LNT2LOTOS now generates LOTOS code for large classes of "P where V" patterns
#3064 Improvement The LNT language now supports the definition of Ada-like derived types (synonyms)

2024年10月13日 - Change List for CADP Version 2024-j "Eindhoven"

HISTORY file item Type Summary
#3041 Improvement LNT2LOTOS no longer rejects duplicated module pragmas !nat_bits, etc.
#3042 Improvement The message displayed by LNT2LOTOS for limitations was made clearer
#3043* Improvement LNT2LOTOS's "diff" function for sets and sorted lists is now noted "minus"
#3044 Improvement TRAIAN was upgraded to version 3.15, with better messages and analyses
#3045 Improvement 12 LNT2LOTOS errors redundant with those of TRAIAN have been removed
#3046 Improvement LNT2LOTOS now avoids translating dead LNT code into dead LOTOS code

2024年09月13日 - Change List for CADP Version 2024-i "Eindhoven"

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

HISTORY file item Type Summary
#3034 Improvement 20 LNT2LOTOS errors redundant with those of TRAIAN have been removed
#3035 Bug fix XTL library "radius.xtl" caused a Gcc "-Wunused-but-set-variable" warning
#3036 Improvement 3 former error messages of LNT2LOTOS have been turned into limitations
#3037 Improvement A new option "-depth N" was added to the OPEN/CAESAR GENERATOR tool
#3038 Improvement TRAIAN was upgraded to version 3.15 beta 5, with better error messages
#3039 Improvement The CADP INSTALLATION directives for Windows/WSL have been enhanced
#3040 Bug fix INSTALLATOR displayed confusing radiobuttons when $CADP was not set

2024年08月13日 - Change List for CADP Version 2024-h "Eindhoven"

HISTORY file item Type Summary
#3021 Improvement LNT2LOTOS now supports tau-transitions with Boolean guards ("i where V")
#3022 Improvement The BCG_CMP / BCG_MIN manual pages give more bibliographic references
#3023 Improvement 3 former error messages of LNT2LOTOS have been turned into limitations
#3024 Bug fix The data-flow analysis of LNT2LOTOS could reject correct LNT programs
#3025 Improvement Compatibility between LNT2LOTOS and TRAIAN progressed in several ways
#3026 Improvement 26 LNT2LOTOS errors redundant with those of TRAIAN have been removed
#3027 Improvement The SVL scripts of CADP demos 04, 10, 15, 31, and 39 have been simplified
#3028 Improvement TRAIAN was upgraded to version 3.15 beta 4, with better errors and warnings
#3029 Bug fix The CAESAR_RANDOM library did not properly initialize its printing format
#3030 Improvement The editor style file was updated to handle all keywords of MCL-V5 and SVL
#3031 Improvement CUNCTATOR now has the same "-thr" / "-append" options as BCG_STEADY
#3032 Bug fix A few minor issues have been fixed in demo_10 (mutual exclusion protocols)
#3033 Improvement The demo_10 of CADP has been enhanced and simplified in various respects

2024年07月13日 - Change List for CADP Version 2024-g "Eindhoven"

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

HISTORY file item Type Summary
#3011 Improvement 6 LNT2LOTOS error and warning messages have been turned into limitations
#3012 Improvement The editor style files have been extended for the ".f", ".fnt", ".t", and ".tnt" files
#3013 Improvement The grammar of LNT2LOTOS was extended to be aligned on that of TRAIAN
#3014 Improvement TRAIAN was upgraded to version 3.14, with better static / data-flow analyses
#3015 Improvement A new demo_15 (Erlangen mainframe multiprocessor system) was introduced
#3016 Bug fix LNT2LOTOS did not parse pragma integer arguments preceded by a "+" sign
#3017 Improvement A new manual page for TRAIAN was introduced into the CADP distribution
#3018 Improvement The SVL predefined library was extended with a new function BCG_ECHO()
#3019 Improvement A new demo_10 (mutual exclusion algorithms for shared memory) was added
#3020 Improvement 20 LNT2LOTOS errors redundant with those of TRAIAN have been removed

2024年06月13日 - Change List for CADP Version 2024-f "Eindhoven"

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

HISTORY file item Type Summary
#2997 Improvement Support for two deprecated LNT constructs was removed from LNT2LOTOS
#2998 Bug fix Items #2982 and #2983 of the HISTORY file provided two mispelled UPC keys
#2999 Improvement 12 LNT2LOTOS error and warning messages have been turned into limitations
#3000 Improvement Inlined LOTOS function generation by LNT2LOTOS was made 15 times faster
#3001 Improvement 28 LNT2LOTOS errors redundant with those of TRAIAN have been removed
#3002 Improvement The cleaning and sweeping functions of SVL now support several parameters
#3003 Bug fix Column labels of BCG_STEADY/BCG_TRANSIENT were not clearly separated
#3004 Improvement SVL emits a better message when a shell variable is used without file extension
#3005 Bug fix The "-network" option of EXP.OPEN could produce syntactically wrong NUPNs
#3006 Improvement SVL no longer emits a warning when comparing the result of a "cut" operator
#3007 Improvement Columns in BCG_STEADY/BCG_TRANSIENT throughput files are now sorted
#3008 Improvement BCG_STEADY/BCG_TRANSIENT check that parameters are pairwise distinct
#3009 Improvement TRAIAN was upgraded to version 3.14 beta 9, with better errors and warnings
#3010 Improvement The LNT syntax accepted by LNT2LOTOS was made closer to that of TRAIAN

2024年05月13日 - Change List for CADP Version 2024-e "Eindhoven"

HISTORY file item Type Summary
#2986 Improvement From now on, LNT.OPEN always invokes TRAIAN before invoking LNT2LOTOS
#2987 Improvement The style file for EMACS/XEMACS was upgraded to the latest version of LNT
#2988 Improvement LNT2LOTOS now stops after syntax analysis in case of lexical or syntactic error
#2989 Improvement 15% of the source code of CADP now complies with the C23 revision of ISO C
#2990 Bug fix LPP improperly translated numbers in "assert", "ensure", and "require" clauses
#2991 Improvement TRAIAN was upgraded to version 3.14 beta 4, with better errors and warnings
#2992 Improvement 12 LNT2LOTOS warnings redundant with those of TRAIAN have been removed
#2993 Bug fix XTL generated incorrect C code for iterations that "apply" an external function
#2994 Improvement LNT2LOTOS no longer displays 19 error messages already emitted by TRAIAN
#2995 Improvement A "replace" function was added for the "action" type and external types of XTL
#2996 Bug fix BCG_TRANSIENT invoked with "-thr -append FILE" halted if FILE pre-existed

2024年04月13日 - Change List for CADP Version 2024-d "Eindhoven"

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

HISTORY file item Type Summary
#2980 Improvement The instructions in INSTALLATION_2 are more explanative
#2981 Improvement The version of TRAIAN within CADP was upgraded to 3.13
#2982* Improvement The former "select" keyword of LNT has been renamed to "alt"
#2983* Improvement LNT exceptions must be declared using the new channel "exit"
#2984 Improvement Many CADP demos have been enriched with published papers
#2985 Improvement The MCL standard libraries are now located in $CADP/src/mcl

2024年03月13日 - Change List for CADP Version 2024-c "Eindhoven"

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

HISTORY file item Type Summary
#2967 Improvement The TST shell script and the Linux installation file now better deal with Windows/WSL2
#2968 Improvement The BCG_CMP tool has two new options "-bfs" and "-dfs" for generating diagnostics
#2969 Improvement SVL now supports "bfs" and "dfs" attributes passed to BCG_CMP when it is invoked
#2970 Improvement The TST shell script was modified to avoid emitting two spurious warnings on macOS
#2971 Improvement LNT2LOTOS now avoids useless-assignment warnings redundant with those of TRAIAN
#2972 Bug fix The LNT.OPEN shell script randomly concealed a few TRAIAN error/warning messages
#2973 Improvement TRAIAN was upgraded to version 3.13 beta 5, bringing better error/warning messages
#2974 Improvement LNT2LOTOS now supports "with NIL" and "with CONS" clauses for list and set types
#2975 Bug fix FSP2LOTOS could generate output EXP files in obsolete, syntactically incorrect format
#2976 Improvement The CADP distribution has been enhanced by adding or removing some files/directories
#2977 Improvement FSP2LOTOS error/warning messages are aligned on those of LNT2LOTOS and TRAIAN
#2978 Bug fix Since CADP 2023-e, the CAESAR.ADT pretty-printer failed on 5% of input LOTOS files
#2979 Improvement LNT2LOTOS now emits better error/warning messages for "with" clauses of LNT types

2024年02月13日 - Change List for CADP Version 2024-b "Eindhoven"

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

HISTORY file item Type Summary
#2956 Improvement Two warnings of LNT2LOTOS are no longer displayed after invoking TRAIAN
#2957 Bug fix On sol64 (Solaris), LPP rejected LNT strings having more than 1024 characters
#2958 Improvement LNT.OPEN displays more informative error messages when some tool has failed
#2959 Improvement The "-smart" option of EXP.OPEN was enhanced by removing a memory leak
#2960 Improvement The grammar for "any" patterns of LNT2LOTOS was aligned on that of TRAIAN
#2961 Improvement LNT2LOTOS no longer displays 6 warnings redundant with the ones of TRAIAN
#2962 Bug fix The include files of LNT2LOTOS caused warnings about signed chars on macOS
#2963 Improvement TRAIAN was upgraded to version 3.13 beta 2, which brings finer static analysis
#2964 Bug fix On recent versions of Windows with WSL2, CADP had stopped working properly
#2965 Improvement LNT2LOTOS produces C code that avoids GCC 12 infinite-recursion warnings
#2966 Improvement The diagnostics of BCG_CMP have been enhanced by invoking BISIMULATOR

2024年01月13日 - Change List for CADP Version 2024-a "Eindhoven"

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

HISTORY file item Type Summary
#2944 Improvement 32-bit binaries for Windows/Cygwin("win32") have been dropped from CADP
#2945 Bug fix LNT2LOTOS mistranslated some LNT "case" behaviours containing "break"
#2946 Bug fix The "bcg_type_character" and "ADT_CHAR" types of CADP are now unsigned
#2947 Improvement LNT2LOTOS does a finer data-flow analysis of "for" loops in LNT functions
#2948 Improvement The LNT library provides FIRST/LAST functions for booleans and characters
#2949 Improvement LNT2LOTOS implements "with FIRST/LAST" clauses on cascade LNT types
#2950 Improvement The demo_23 (IEEE 1394 Link Layer) was translated from LOTOS to LNT
#2951 Improvement The version of TRAIAN shipped with CADP was upgraded from 3.11 to 3.12
#2952 Improvement A few LNT files demo_24 have been updated to avoid TRAIAN 3.12 warnings
#2953 Improvement LNT2LOTOS handles "with PRED/SUCC" clauses on miscellaneous LNT types
#2954 Bug fix LNT2LOTOS mishandled "with !=" clauses in presence of user-defined "=="
#2955 Bug fix EXP2C could cause stack overflow on large expressions involving priorities

2023年12月13日 - Change List for CADP Version 2023-l "Aachen"

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

HISTORY file item Type Summary
#2931 Improvement SVL now generates shorter log files that enable a fully exhaustive cleanup
#2932 Bug fix On macOS, SVL could generate a large temporary file until the disk was full
#2933 Bug fix The XSIMULATOR tool had stopped working on macOS since January 2023
#2934 Improvement From now on, SVL retries LTS reduction only in case of memory shortage
#2935 Improvement The graphical tools of CADP now support recent versions of macOS/XQuartz
#2936 Improvement CADP has been ported to macOS 14 "Sonoma", with documentation updates
#2937 Improvement The error and warning messages of SVL now provide file and line information
#2938 Improvement Libraries and documentation of LNT2LOTOS and TRAIAN have been aligned
#2939 Improvement 5 warnings of LNT2LOTOS are no longer displayed after invoking TRAIAN
#2940 Improvement The LOTOS specifications of demo_23 ("Firewire") have been further simplified
#2941 Improvement LNT2LOTOS now supports field selection with an explicit exception parameter
#2942 Improvement LNT2LOTOS now supports field update with an explicit exception parameter
#2943 Bug fix Upon exception raise, LNT2LOTOS converted file names to the upper case

2023年11月13日 - Change List for CADP Version 2023-k "Aachen"

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

HISTORY file item Type Summary
#2916 Improvement LNT.OPEN ensures a better co-operation between TRAIAN and LNT2LOTOS
#2917 Bug fix LNT2LOTOS did not give line numbers of non-exhaustive "case" instructions
#2918 Improvement 5 warnings of LNT2LOTOS were turned into fatal errors (as TRAIAN does)
#2919 Bug fix LNT2LOTOS emitted "behaviour is unreachable" warnings multiple times
#2920 Improvement LNT2LOTOS displays more precise line numbers for variable parameters
#2921 Improvement The demo_24 (CO4 distributed knowledge system) was translated to LNT
#2922 Improvement The LOTOS specification of demo_25 has been further shortened by 27%
#2923 Improvement The demo_23 (FireWire bus protocol) has been simplified in various ways
#2924 Improvement The demo_25 (cluster file system) was translated from LOTOS to LNT
#2925 Improvement A few includes have been simplified and modified to avoid Clang warnings
#2926 Bug fix LNT2LOTOS mistranslated some LNT "case" behaviours containing "raise"
#2927 Bug fix LNT2LOTOS mistranslated some LNT "case" behaviours containing "break"
#2928 Improvement 9 warnings of LNT2LOTOS are no longer displayed after invoking TRAIAN
#2929 Bug fix The mac64 executable of TRAIAN 3.11 reported improper syntax errors
#2930 Improvement TST and CADP_CC were updated to better support recent macOS versions

2023年10月13日 - Change List for CADP Version 2023-j "Aachen"

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

HISTORY file item Type Summary
#2910 Improvement The -prob/-rate options of BCG_MIN now delete the dead states they may create
#2911 Bug fix Algorithms A10 and A11 of CAESAR_SOLVE could generate wrong diagnostics
#2912 Improvement The library of LNT2LOTOS was extended with a Char : String -> Char function
#2913 Bug fix Algorithm A8 of CAESAR_SOLVE could generate incorrect counterexamples
#2914 Bug fix The -root option of LNT2LOTOS tolerated extra code located after "end module"
#2915 Improvement TRAIAN 3.11 now provides a full-fledge, stricter compiler front-end for LNT

2023年09月13日 - Change List for CADP Version 2023-i "Aachen"

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

HISTORY file item Type Summary
#2903 Improvement CADP_POSTSCRIPT searches for Atril/Evince before Ghostview
#2904 Improvement Memory consumption of BES_SOLVE was reduced by 10-50%
#2905 Improvement The LNT library was extended with 5 new predefined functions
#2906 Bug fix An error recently introduced in CADP_INDENT was hotfixed
#2907 Improvement SVL messages better detail probabilistic/stochastic reductions
#2908 Improvement The LNT library was extended with 8 new predefined functions
#2909 Improvement An obscure error message of SVL was made more informative

2023年08月26日 - Change List for CADP Version 2023-h "Aachen"

HISTORY file item Type Summary
#2901 Improvement CADP was updated to run on Solaris 11.4 with the latest versions of Oracle C compiler
#2902 Bug fix On Solaris 11, CADP_INDENT could truncate the C code generated by CAESAR.ADT

2023年07月26日 - Change List for CADP Version 2023-g "Aachen"

HISTORY file item Type Summary
#2890 Improvement The syntax and manual of LNT have been aligned with TRAIAN 3.10
#2891 Improvement All the "with" functions of an external LNT type are now external
#2892 Bug fix LNT2LOTOS looped forever if an external type had a "last" function
#2893 Improvement The "with" functions of a non-external LNT type may now be external
#2894 Bug fix LNT_CHECK could emit "tr: misplace sequence asterisk" warnings
#2895* Improvement The LNT operator "/=" should now be written either "!=" or ""
#2896 Improvement From now on, the LNT operator "==" may alternatively be noted "="
#2897 Improvement The predefined LNT function "card" was removed for all LNT types
#2898 Improvement The predefined LNT function "length" on sets was renamed to "card"
#2899* Improvement The LNT functions isEmpty and nth are named empty and element
#2900 Improvement The CADP tools have been ported to Windows 11 (running Cygwin)

2023年06月13日 - Change List for CADP Version 2023-f "Aachen"

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

  • Gwen Salaun (INRIA/CONVECS)
  • Suraj Gupta (INRIA/CONVECS)

HISTORY file item Type Summary
#2883 Bug fix The implementation in C of one function of the X_STRING library was revised
#2884 Bug fix The EUCALYPTUS interface now pre-selects the MAIN process of LNT programs
#2885 Bug fix The EUCALYPTUS interface could trigger "bad variable name" errors at run time
#2886 Bug fix BES_SOLVE ignored the "unique" and "mode N" pragmas contained in BES files
#2887 Improvement The LNT syntax in LNT2LOTOS was aligned on that of the TRAIAN compiler
#2888 Improvement CADP now avoids the new "-Wdeprecated-non-prototype" warnings of Xcode 14.3
#2889 Improvement An LNT "!card" pragma was inserted in demo_16 to lower memory consumption

2023年05月12日 - Change List for CADP Version 2023-e "Aachen"

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

  • Suraj Gupta (INRIA/CONVECS)

HISTORY file item Type Summary
#2876 Bug fix The instructions for installing Cygwin's GCC on win64 were outdated
#2877 Bug fix XTL could generate wrong C code for handling values of type string
#2878 Bug fix On win64, OCIS halted with an "invalid program name" error message
#2879 Improvement The BCG monitor is much faster for graphs with many different labels
#2880 Bug fix On Windows, launching OCIS failed to open the simulator window
#2881 Improvement On Linux, XTL could generate C code that triggered GCC warnings
#2882 Improvement CADP packages and demos are now ".tar.gz" (instead of ".tar.Z") files

2023年04月13日 - Change List for CADP Version 2023-d "Aachen"

HISTORY file item Type Summary
#2867 Improvement The C implementation of two functions of the X_STRING library was enhanced
#2868 Improvement Include files for portability of BCG and OPEN/CAESAR have been streamlined
#2869 Bug fix EVALUATOR 4 and 5 could produce wrong verdicts when using GCC on SunOS
#2870 Bug fix The "-parallel" option of BES_SOLVE could fail copying on remote machines
#2871 Bug fix Algorithm A9 of BES_SOLVE failed when applied to multiple equation blocks
#2872 Bug fix The "-diag" option of BES_SOLVE could abort when invoked with algorithm A8
#2873 Bug fix Since March 2023, the INTEGERNUMBER.lib file was not compiling properly
#2874 Bug fix EVALUATOR 5's "-acyclic" option produced illegal C code for MCL-V5 formulas
#2875 Improvement The win64 port of CADP (64-bit Windows PE32+ binaries) has been completed

2023年03月13日 - Change List for CADP Version 2023-c "Aachen"

HISTORY file item Type Summary
#2856 Improvement An INSERT() function is now defined automatically for each LNT "list" type
#2857* Improvement The implementation of LNT "set" types was modified to be more efficient
#2858 Improvement "with" clauses can now define equality and order relations on LNT "set" types
#2859* Improvement The "sorted set" types of LNT are now removed and replaced by "set" types
#2860 Improvement LNT2LOTOS is stricter about NIL, CONS, and INSERT in "with" clauses
#2861 Bug fix The {...} notation for LNT "set" types did not always behave as expected
#2862* Improvement One may no longer define LNT constructors named {} (rather than NIL)
#2863 Improvement Unary special operators in LNT patterns must be called with parentheses
#2864 Improvement The implementation of the LNT functions gcd() and scm() was made faster
#2865* Improvement The LNT functions NatToInt() and IntToNat() are now named Int() and Nat()
#2866 Bug fix With CADP 2023-b, the "-graph" option of CAESAR had stopped working

2023年02月13日 - Change List for CADP Version 2023-b "Aachen"

HISTORY file item Type Summary
#2851 Improvement INSTALLATOR could emit "stray \ before white space" warnings
#2852 Bug fix LNT_NAME no longer converts filenames to upper case on Windows
#2853 Improvement TCL-TK and TIX have been upgraded to versions 8.6.13 and 8.4.3
#2854 Improvement XSIMULATOR has been upgraded and given a new appearance
#2855 Improvement Porting CADP to 64-bit Windows progressed and is halfway through

2023年01月13日 - Change List for CADP Version 2023-a "Aachen"

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

  • Nicolas Amat (LAAS-CNRS, Toulouse, France)
  • Reyhane Falanji (Univ. Grenoble Alpes, France)
  • Florian Gallay ((Univ. Grenoble Alpes, France)
  • Gwen Salaun (INRIA/CONVECS)
  • Katsumi Wasaki (Shinsu University, Nagano, Japan)

HISTORY file item Type Summary
#2843 Improvement LNT2LOTOS warns about external LNT functions with specified LOTOS names
#2844 Improvement CADP now supports Macs with ARM processors, as well as macOS 13 "Ventura"
#2845 Improvement The "-concurrent-places" option of CAESAR.BDD was made faster in two ways
#2846 Improvement demo_33 (randomized consensus protocol) was translated from LOTOS to LNT
#2847 Improvement 32-bit CADP binaries for Solaris and OpenIndiana ("sol86") have been dropped
#2848 Improvement The LOTOS code of demo_24 was shortened by 21%, still preserving semantics
#2849 Bug fix EVALUATOR now checks all results returned by memory allocation functions
#2850 Improvement The LNT language now features a predefined function "subset" for set inclusion

2022年12月13日 - Change List for CADP Version 2022-l "Kista"

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

  • Salim Chehida (LIG, Univ. Grenoble Alpes, France)

HISTORY file item Type Summary
#2834 Bug fix The 2022-LNT-EXCLAIM key of UPC failed to remove "!" symbols before strings
#2835 Improvement The syntax of LNT restricts the use of "{}" for function and constructor names
#2836 Improvement The documentation of CADP was enhanced and updated at three different places
#2837 Improvement LNT2LOTOS tolerates multiple identical !implementedby "LOTOS:..." pragmas
#2838 Improvement LNT2LOTOS rejects external LOTOS functions with "out" or "in out" parameters
#2839 Improvement The EUCALYPTUS interface now pre-selects the MAIN process of LNT programs
#2840 Improvement On Windows, EUCALYPTUS can now launch Emacs without the "not a tty" error
#2841 Improvement LNT2LOTOS no longer generates LOTOS code for external LOTOS functions
#2842 Improvement The CAESAR_SOLVE library was enriched with two new algorithms A10 and A11

2022年11月12日 - Change List for CADP Version 2022-k "Kista"

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

  • Reyhane Falanji (Univ. Grenoble Alpes, France)
  • Florian Gallay (Univ. Grenoble Alpes, France)
  • Gwen Salaun (INRIA/CONVECS)

HISTORY file item Type Summary
#2826* Improvement In LNT, output offers should no longer be preceded by the "!" symbol
#2827 Improvement The UPC shell script now removes LNT definitions of "none" channels
#2828 Improvement LNT2LOTOS warnings about deprecated syntax provide line numbers
#2829 Bug fix The UPC shell script did not properly handle lines ending with CR-LF
#2830 Improvement The LNT model of demo_30 (Hubble telescope) is now more readable
#2831 Bug fix cadp_cc and many other scripts have been adapted to Macs with ARM
#2832 Improvement The demo_27 of CADP (Philips' HAVi protocol) was translated to LNT
#2833 Improvement The GC garbage collection library was upgraded from v7.6.4 to v8.2.2

2022年10月13日 - Change List for CADP Version 2022-j "Kista"

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

  • Quentin Nivon (INRIA/CONVECS)

HISTORY file item Type Summary
#2822 Improvement "!implementedby" pragmas of LNT functions may no longer contain %s, %d, %i, %u...
#2823* Improvement LNT module names must match their file names case-sensitively (not insensitively)
#2824* Improvement From now on, "with update" is forbidden in LNT and has been replaced by "with set"
#2825 Bug fix On Linux Mint 21, TST would emit a spurious "Please upgrade to Debian 2.2" warning

2022年09月13日 - Change List for CADP Version 2022-i "Kista"

HISTORY file item Type Summary
#2818 Improvement demo_27 was simplified by removing unused variables and factoring code
#2819* Improvement The "eval" keyword of LNT was made optional in three situations out of four
#2820 Bug fix LNT_DEPEND ignored all module names prefixed by "module", "is", or "with"
#2821 Improvement LNT forbids functions with special identifiers and "out" parameters or no result

2022年08月26日 - Change List for CADP Version 2022-h "Kista"

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

  • Nicolas Amat (LAAS-CNRS, Toulouse, France)
  • Reyhane Falanji (Univ. Grenoble Alpes, France)
  • Florian Gallay (Univ. Grenoble Alpes, France)
  • Fabio Somenzi (University of Colorado, USA)

HISTORY file item Type Summary
#2810 Improvement The "arch" script and the CADP binaries for macOS have been enhanced
#2811 Improvement The "while" and "for" loops of LNT now support optional "break" labels
#2812 Improvement CAESAR.BDD now relies on version 3.1.0 (rather than 3.0.0) of CUDD
#2813 Improvement The demo_26 of CADP has been enhanced and simplified in many ways
#2814 Improvement The demo_26 (invoicing case study) was translated from LOTOS to LNT
#2815 Bug fix LNT_MERGE did not handle the module pragmas of LNT sub-modules
#2816 Bug fix LNT_MERGE did not handle the !num_*, !upgrade, and !version pragmas
#2817 Improvement C and LOTOS identifiers in LNT pragmas are checked by LNT2LOTOS

2022年07月13日 - Change List for CADP Version 2022-g "Kista"

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

  • Nicolas Amat (LAAS-CNRS, Toulouse, France)

HISTORY file item Type Summary
#2802 Bug fix If an error occurred, LNT_MERGE could leave incomplete output files
#2803 Bug fix LNT_MERGE produced duplicate occurrences of LNT module pragmas
#2804 Improvement "Divergence-sensitive branching bisimulation" was renamed to "divbranching"
#2805 Improvement Initial changes have been done towards a 64-bit Windows version of CADP
#2806 Improvement Former "sharp" equivalence was split into "sharp" and "divsharp" equivalences
#2807 Improvement LNT2LOTOS now warns about dead code that follows loops in LNT processes
#2808 Improvement Instructions have been given to run CADP on Macs with ARM processors
#2809 Improvement LNT2LOTOS warns about "in var" process parameters assigned before use

2022年06月13日 - Change List for CADP Version 2022-f "Kista"

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

  • Celine Deknop (UC Louvain, Belgium)
  • Lucie Muller (INRIA/CONVECS, France)

HISTORY file item Type Summary
#2796 Improvement The style files for GNOME editors have been updated to support Gtk4 and Gtk5
#2797 Improvement The win32 version of INSTALLATOR was adapted to recent versions of GNU tar
#2798 Improvement The instructions for installing Cygwin and CADP on Windows have been updated
#2799 Improvement The cadp_cygwin.com script (and CADP) no longer rely on the "ed" command
#2800 Bug fix Execution of the SVL script of demo_11 failed abruptly on Windows/Cygwin
#2801 Improvement demo_31 was modified, so that CADP no longer relies on the "bc" command

2022年05月25日 - Change List for CADP Version 2022-e "Kista"

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

  • Luca Di Stefano (INRIA/CONVECS)
  • Reyhane Falanji (Univ. Grenoble Alpes, France)
  • Florian Gallay (Univ. Grenoble Alpes, France)

HISTORY file item Type Summary
#2789 Improvement The recently added LNT_MERGE tool was revised and enhanced in many ways
#2790 Improvement The demo_04 (systolic convolution product) was translated from LOTOS to LNT
#2791 Bug fix In the X_BIT library, (*! external *) comments were missing for AND, OR, XOR
#2792 Bug fix In the BCG_READ manual page, the type of BCG_OT_NB_STATES() was wrong
#2793 Improvement "!pointer" pragmas are forbidden for LNT types isomorphic to natural numbers
#2794 Improvement The ext directory of CADP now provides style files for the Sublime Text editor
#2795 Improvement LNT2LOTOS was modified to avoid Gcc "-Wunused-but-set-variable" warnings

2022年04月13日 - Change List for CADP Version 2022-d "Kista"

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

  • Luca Di Stefano (INRIA/CONVECS)
  • Philippe Ledent (STMicroelectronics, Grenoble, France)
  • Katsumi Wasaki (Shinshu University, Nagano, Japan)

HISTORY file item Type Summary
#2783 Improvement The "-unit-order" option of CAESAR.BDD was made more effective and faster
#2784 Improvement The "-place-order" option of CAESAR.BDD was also significantly enhanced
#2785 Bug fix Since March 2022, some CADP binaries for Linux reported "no available license"
#2786 Improvement LNT2LOTOS now verifies the arguments of the "!bits" and "!card" pragmas
#2787 Improvement Two new type pragmas "!pointer" and "!nopointer" have been introduced in LNT
#2788 Improvement A new tool LNT_MERGE for multi-module LNT programs was added to CADP

2022年03月13日 - Change List for CADP Version 2022-c "Kista"

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

  • Pierre Bouvier (INRIA/CONVECS)

HISTORY file item Type Summary
#2775 Improvement The "-signature" and "-unit-order" options of CAESAR.BDD have been enhanced
#2776 Bug fix Since Nov. 2021, DISTRIBUTOR (iX86) failed for Glibc versions less than 2.28
#2777 Improvement All CADP include files now use the standard Booleans defined in <stdbool.h>
#2778 Improvement "bool", "false", and "true" may no longer be used as C names in LOTOS and XTL
#2779 Improvement All CADP compilers are built using the latest versions of SYNTAX and TRAIAN
#2780 Improvement The C code generated by CAESAR triggers less warnings from the Sparse tool
#2781 Improvement The C code generated by CAESAR.ADT triggers less warnings from Splint
#2782 Bug fix CAESAR.ADT's "-trace" option produced wrong C code for names containing "\"

2022年02月12日 - Change List for CADP Version 2022-b "Kista"

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

  • Pierre Bouvier (INRIA/CONVECS)

HISTORY file item Type Summary
#2763 Improvement Files of demo_24 and demo_26 were renamed for their translation to LNT
#2764 Bug fix LNT2LOTOS forgot to verify the "where" clauses of LNT predicate types
#2765 Bug fix There were three variable declarations with incorrect types in demo_09
#2766 Improvement LNT types with the "!external" pragma may now have empty definitions
#2767 Improvement "-signature" and "-signature-multiple" options were added to CAESAR.BDD
#2768 Improvement LNT functions with the "!external" pragma may now have empty bodies
#2769* Improvement Binary/hexa/octal LNT constants must start with (lower case) "0b"/"0o"/"0x"
#2770* Improvement The mantissas of LNT real constants may no longer start nor end with a dot
#2771 Improvement The syntax of LNT was extended to allow underscores in numeric constants
#2772* Improvement Useless zeros are forbidden on the left of LNT integer and real constants
#2773 Improvement Two new options "-arcs-pt" and "-arcs-tp" have been added to CAESAR.BDD
#2774 Improvement In library files, the macros ADT_*_INTERFACE_ONLY have been renamed

2022年01月14日 - Change List for CADP Version 2022-a "Kista"

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

  • Pierre Bouvier (INRIA/CONVECS)
  • Maxime Denis (CNAM, Paris, France)
  • Roumeissa Khennaoui (Univ. Constantine, Algeria)
  • Lucie Muller (INRIA/CONVECS)

HISTORY file item Type Summary
#2747 Bug fix The ".h" files generated by CAESAR.ADT had wrong version numbers
#2748 Improvement The demo_08 (rel/REL protocol, ex-demo_20) was translated to LNT
#2749 Improvement CAESAR.BDD uses "group sift" strategy for BDD dynamic reordering
#2750 Improvement The manual pages of NUPN, NUPN_INFO, etc. have been enhanced
#2751 Improvement A new option "-precanonical-nupn" was added to the NUPN_INFO tool
#2752 Bug fix INSTALLATOR failed for recent GNU-tar versions (e.g., Ubuntu 21.10)
#2753 Bug fix With !string_card pragma, LNT2LOTOS generated wrong LOTOS code
#2754 Bug fix LNT_DEPEND could list the included LNT modules in a wrong order
#2755 Bug fix LNT2LOTOS did incorrect data-flow analysis for process parameters
#2756 Bug fix Some options of CADP_PATH failed on Windows with 64-bit Cygwin
#2757 Improvement The 3 options "-*-order" of CAESAR.BDD now sort their output lines
#2758 Improvement CADP_REPLACE was modified to avoid a bug of GNU-bash 4.4.12(3)
#2759 Improvement The 3 options "-*-order" of CAESAR.BDD are now much more precise
#2760 Bug fix CAESAR.BDD's "-transition-order" option did wrong differentiations
#2761 Improvement The "-trivial" option of CAESAR.BDD was made significantly faster
#2762 Improvement File "bcg_type.h" of BCG was changed to suppress GCC 11 warnings

2021年12月13日 - Change List for CADP Version 2021-l "Saarbruecken"

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

  • Lidaou Denis Assati (Polytech Nice, France)
  • Almer Bolatov (Saarland University, Germany)
  • Pierre Bouvier (INRIA/CONVECS)
  • Marius Hollinger (Saarland University, Germany)
  • Heinrich Ody (Saarland University, Germany)

HISTORY file item Type Summary
#2734 Improvement CAESAR.BDD uses a new criterion to trigger dynamic reordering of BDDs
#2735* Improvement LNT2LOTOS now warns about LNT channels defined with anonymous fields
#2736 Bug fix The style files for EMACS caused an "unescaped character literals" error
#2737 Bug fix CAESAR's "-open" option wrongly implemented CAESAR_FORMAT_LABEL()
#2738* Improvement In LNT, "any T" must now be parenthesized on the left of infix constructors
#2739 Improvement The demo_07 (car overtaking protocol) was translated from LOTOS to LNT
#2740 Improvement The demo_09 (Initiator Responder protocol) has been translated to LNT
#2741 Improvement The demo_34 (computer integrated manufacturing) was translated to LNT
#2742 Improvement The demo_37 (Open Distributed Processing trader) was translated to LNT
#2743 Improvement The demo_39 (turntable system for drilling products) was translated to LNT
#2744 Improvement The demo_08 and demo_20 (rel/REL protocol) were enhanced and simplified
#2745 Improvement In demo_26 (invoicing case study), all ".lot" files now have a ".lotos" extension
#2746 Bug fix TST emitted spurious warnings if CADP pathnames in $PATH ended with "/"

2021年11月14日 - Change List for CADP Version 2021-k "Saarbruecken"

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

  • Nicolas Amat (LAAS-CNRS, Toulouse, France)
  • Pierre Bouvier (INRIA/CONVECS)
  • Nicole Levy (CNAM, Paris, France)

HISTORY file item Type Summary
#2726 Bug fix Since CADP 2021-j, CADP_HOSTNAME failed ("reason 3a") on macOS
#2727 Improvement The CADP code now compiles without warnings using Apple's Xcode 13.1
#2728 Improvement CADP has been ported to the latest macOS version: macOS 12 "Monterey"
#2729 Bug fix BCG_EDIT stopped if the environment variable $PRINTER was undefined
#2730 Improvement The CADP demos have been modified to give names to all channel fields
#2731 Bug fix CAESAR.BDD could do segmentation faults when the BDD timeout expired
#2732 Improvement The CADP code now compiles without warnings using GCC version 7 or 8
#2733 Improvement CAESAR.BDD was generalized to handle NUPNs having zero initial places

2021年10月26日 - Change List for CADP Version 2021-j "Saarbruecken"

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

  • Pierre Bouvier (INRIA/CONVECS)
  • Nicole Levy (CNAM Paris, France)

HISTORY file item Type Summary
#2718 Improvement The "-unit-order" option of CAESAR.BDD uses 48 fields instead of 46
#2719 Improvement CAESAR.BDD was made faster by introducing extra data structures
#2720 Bug fix LNT2LOTOS' data-flow analysis now examines pre/post-conditions
#2721 Improvement The manual page that defines the NUPN format is now more precise
#2722 Improvement It is no longer required to install "gnutar" for using CADP on macOS
#2723 Improvement CADP was modified to support verson 2.8.1 of XQuartz on macOS
#2724 Improvement Setting a static hostname for CADP on macOS was made simpler
#2725 Improvement UPC can automatically insert field names in LNT channel definitions

2021年09月13日 - Change List for CADP Version 2021-i "Saarbruecken"

HISTORY file item Type Summary
#2707 Bug fix LNT2LOTOS checked infix-operator priorities improperly in array assignments
#2708 Bug fix Options "-bcla", "-ocla", and "-pcla" of ALDEBARAN printed spurious warnings
#2709 Bug fix When invoked with option "-icla" or "-scla", ALDEBARAN failed unexpectedly
#2710 Bug fix The "BCG PostScript Format" entry in the "Help" menu of BCG_EDIT failed
#2711 Improvement The "installator.shar" file containing INSTALLATOR is now 30%-35% smaller
#2712 Bug fix The "OPEN/CAESAR" entry in EUCALYPTUS's "Help" menu did not work
#2713 Improvement The old "compress" and "uncompress" commands are no longer used in CADP
#2714 Improvement BES_SOLVE, BISIMULATOR, and EVALUATOR now support "xz" compression
#2715 Improvement The graphical tools of CADP warn better if the $DISPLAY variable is not set
#2716 Improvement The !implementedby "x" pragmas of LNT can be written !implementedby "C:x"
#2717* Improvement LNT's !representedby "x" pragmas are now written !implementedby "LOTOS:x"

2021年08月26日 - Change List for CADP Version 2021-h "Saarbruecken"

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

  • Luca Di Stefano (INRIA/CONVECS)

HISTORY file item Type Summary
#2703 Improvement The "-unit-order" option of CAESAR.BDD better distinguishes between similar units
#2704 Bug fix EXP.OPEN has been failing on x64 machines since CADP 2021-g (July 26, 2021)
#2705 Improvement Appendix E of the LNT2LOTOS manual was updated with respect to Traian 3.4
#2706 Improvement LNT2LOTOS no longer emits warnings about unused values of "in out" parameters

2021年07月26日 - Change List for CADP Version 2021-g "Saarbruecken"

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

  • Pierre Bouvier (INRIA/CONVECS)

HISTORY file item Type Summary
#2698 Bug fix The "place-order"/"-unit-order" options of CAESAR.BDD did wrong calculations
#2699 Improvement The "place-order"/"-unit order" options of CAESAR.BDD are now more precise
#2700 Bug fix The "-version" option of CAESAR.OLD incorrectly returned 6.1 instead of 6.10
#2701 Improvement The RFL shell script now supports the "oarsh"/"oarcp" commands of Grid 5000
#2702 Improvement The "-*-order" options of CAESAR.BDD display equal elements on the same line

2021年06月13日 - Change List for CADP Version 2021-f "Saarbruecken"

HISTORY file item Type Summary
#2689 Improvement Option "-unit-order" of CAESAR.BDD now executes faster on certain classes of NUPNs
#2690 Bug fix The "-place-permute" option of NUPN_INFO produced NUPNs with wrong place labels
#2691 Improvement CAESAR.BDD and NUPN_INFO have two new options "-place-order" and "-place-sort"
#2692 Bug fix The "-normal-nupn/-canonical-nupn" options of NUPN_INFO did not sort initial places
#2693 Improvement The "-sharp" option of BCG_MIN now performs full (rather than partial) minimization
#2694 Improvement BCG_CMP has a new option "-sharp" to compare two LTSs modulo sharp bisimulation
#2695 Improvement The "-unit-order" option of CAESAR.BDD was strengthened with additional criteria
#2696 Improvement The SVL language and compiler support LTS comparison modulo sharp bisimulation
#2697 Improvement CAESAR, CAESAR.ADT, and XTL now forbid using C99 and C11 reserved keywords

2021年05月12日 - Change List for CADP Version 2021-e "Saarbruecken"

HISTORY file item Type Summary
#2677 Bug fix TST did not properly warn about attempts at running CADP on WSL version 1
#2678 Bug fix The "-warning" option of CAESAR dit not filter out certain warning messages
#2679 Improvement The "-nupn" option CAESAR now stops right after generating the ".nupn" file
#2680 Bug fix CAESAR and CAESAR.ADT could generate C identifiers with name clashes
#2681 Bug fix The "-redundant-removal" option NUPN_INFO forgot to renumber place labels
#2682 Improvement NUPN_INFO was extended with 3 options "-{place,transition,unit}-renumber"
#2683 Improvement CAESAR.BDD was extended with 2 options "-transition-order" and "-unit-order"
#2684 Improvement Yet another new option "-essential-nupn" has been added to NUPN_INFO
#2685 Improvement NUPN_INFO was extended with one more option named "-place-permute"
#2686 Improvement NUPN_INFO was extended with two more options "-transition-{permute,sort}"
#2687 Improvement NUPN_INFO was extended with two more options "-unit-{permute,sort}"
#2688 Improvement The "-canonical-nupn" option of NUPN_INFO performs stronger normalization

2021年04月12日 - Change List for CADP Version 2021-d "Saarbruecken"

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

  • Seyed Morteza Babamir (University of Kashan, Iran)
  • Luca Di Stefano (INRIA/CONVECS)
  • Saeed Doostali (University of Kashan, Iran)
  • Ajay Krishna Muroor (INRIA/CONVECS)
  • Hauke Pribnow (Univ. Muenster, Germany)
  • Lucas F. Salvador (Princeton Univ., New Jersey, USA)

HISTORY file item Type Summary
#2666 Improvement CADP was ported to Linux x64 machines running on Windows/WSL2
#2667 Bug fix The "2021-LNT-CASE-VAR" option of UPC could do incorrect translations
#2668 Improvement Four OPEN/CAESAR applications no longer cause GCC 9.3 warnings
#2669 Bug fix LNT2LOTOS implemented an overly restrictive syntax for post-conditions
#2670 Bug fix LNT2LOTOS mis-translated external functions with pre/post-conditions
#2671 Bug fix LNT2LOTOS looped forever on external functions with "out" arguments
#2672 Improvement The installation procedure for CADP on Linux is now fully documented
#2673 Bug fix The "Find Livelock" option of EUCALYPTUS did not execute properly
#2674 Improvement INSTALLATOR and RFL no longer rely on the old RSH and RCP protocols
#2675 Improvement The C code generated by CAESAR.ADT was made compliant with GCC 10
#2676 Improvement On Windows, CADP_PDF and CADP_WEB now invoke Microsoft Edge

2021年03月14日 - Change List for CADP Version 2021-c "Saarbruecken"

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

  • Justus Fasse (Univ. Grenoble Alpes, France)
  • Gwen Salaun (INRIA/CONVECS)
  • Luca di Stefano (INRIA/CONVECS)
  • Hamza Tamenaoul (ENSIMAG - Grenoble INP, Grenoble, France)
  • Sean Watters (University of Strathclyde, Glasgow, UK)

HISTORY file item Type Summary
#2657 Improvement LNT2LOTOS warns about missing parentheses for user-defined infix operators
#2658 Bug fix SVL did not optimally propagate "hide" and "cut" under parallel composition
#2659 Bug fix FSP2LOTOS forbad local processes (with parameters) named ERROR or STOP
#2660 Improvement The predefined LNT operator "+" for string concatenation was renamed to "&"
#2661* Improvement The predefined LNT function "is_empty" on strings was renamed to "IsEmpty"
#2662 Improvement CADP has been adapted and ported to the latest version of macOS 11 "Big Sur"
#2663 Improvement The INSTALLATOR tool is now available through HTTPS, and not only via FTP
#2664 Improvement CADP has been ported to Linux distributions with Glibc 2.32 (e.g., Ubuntu 33)
#2665* Improvement Redundant "in" keywords have been removed from the LNT "case" instructions

2021年02月13日 - Change List for CADP Version 2021-b "Saarbruecken"

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

  • Pierre Bouvier (INRIA/CONVECS)

HISTORY file item Type Summary
#2652 Improvement LNT2LOTOS warns about missing parentheses in Boolean expressions
#2653 Improvement The CAESAR.BDD tool has been enhanced in three different ways
#2654* Improvement The LNT language now has 6 levels of priorities for the infix operators
#2655 Improvement LNT2LOTOS warns about user-defined operators named "AND", "Or"...
#2656 Improvement The TST shell script is now distributed via HTTPS and not only via FTP

2021年01月13日 - Change List for CADP Version 2021-a "Saarbruecken"

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

  • Pierre Bouvier (INRIA/CONVECS)

HISTORY file item Type Summary
#2649 Improvement CAESAR.BDD's "-concurrent-places" option produces even more "0" values
#2650 Improvement In LNT, "AND", "OR", "AND THEN", "OR ELSE" are now written in lower case
#2651* Improvement "and", "div", "or", "mod", "rem", and "xor" have become reserved LNT keywords

2020年12月13日 - Change List for CADP Version 2020-l "Aalborg"

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

  • Pierre Bouvier (INRIA/CONVECS)
  • Luca Di Stefano (INRIA/CONVECS)

HISTORY file item Type Summary
#2639 Improvement The MCL language was extended with a function "card" over natural sets
#2640 Improvement The data structures of CAESAR.BDD for storing arcs have been redesigned
#2641* Improvement The "and_then" operator of LNT is now written "and then", as in Ada
#2642* Improvement The "or_else" operator of LNT is now written "or else", as in Ada too
#2643 Improvement A new environment variable was added to control CAESAR.BDD's iterations
#2644 Improvement CAESAR.BDD's "-concurrent-places" option now produces more "0" values
#2645 Improvement The predefined library of LNT no longer depends on other LOTOS libraries
#2646 Improvement CAESAR.BDD's "-concurrent-places" option also produces more "1" values
#2647* Improvement The LNT operators "eq", "ne", "lt", "le", "gt", and "ge" have been suppressed
#2648* Improvement The syntax "_..._" for declaring infix functions in LNT is no longer required

2020年11月13日 - Change List for CADP Version 2020-k "Aalborg"

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

  • Justus Fasse (Univ. Grenoble Alpes, France)

HISTORY file item Type Summary
#2631 Improvement CAESAR.BDD's options "-input-transitions" and "-output-transitions are faster
#2632 Bug fix The picture describing the asynchronous circuit of demo_38 has been corrected
#2633* Improvement From now on, "alt" and "trap" are new LNT keywords reserved for future use
#2634 Improvement The deprecated "=>" symbol (now written "->") is no longer tolerated in LNT
#2635 Bug fix TST displayed an error message on Linux distributions with no "arch" command
#2636* Improvement From now on, in LNT, Boolean implication is noted "=>" instead of "implies"
#2637* Improvement From now on, in LNT, Boolean equivalence is noted "<=>" rather than "iff"
#2638* Improvement In LNT "with" clauses, function names are no longer surrounded by double quotes

2020年10月14日 - Change List for CADP Version 2020-j "Aalborg"

HISTORY file item Type Summary
#2626 Improvement From now on, the SVL language and compiler support sharp bisimulation
#2627 Bug fix The LNT2LOTOS Reference Manual was corrected and made more readable
#2628 Bug fix LNT2LOTOS could generate incorrect LOTOS code for certain "as" patterns
#2629 Improvement CADP no longer contains the deprecated mac86 binaries for 32-bit macOS
#2630 Improvement CAESAR.BDD makes stricter checks on NUPNs with "!multiple_*" pragmas

2020年09月26日 - Change List for CADP Version 2020-i "Aalborg"

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

  • Ben Weintraub (Northeastern University, USA)

HISTORY file item Type Summary
#2621 Improvement The directives for installing CADP on macOS have been simplified
#2622 Improvement The CAESAR.BDD tool has been extended with four new options
#2623 Improvement BCG_MIN can now reduce BCG graphs modulo sharp bisimulation
#2624 Bug fix The "-mcc" option of CAESAR.BDD could give incorrect results
#2625 Improvement Eight options of the CAESAR.BDD tool have been made faster

2020年08月26日 - Change List for CADP Version 2020-h "Aalborg"

HISTORY file item Type Summary
#2617* Improvement LNT has a new "ensure" clause for postconditions on functions and processes
#2618 Bug fix On macOS, LNT_DEPEND could make intermittent segmentation faults
#2619 Improvement Several CADP programs and shell scripts now search for XQuartz in /opt/X11
#2620 Bug fix On 64-bit macOS, OCIS did not launch XQuartz automatically when needed

2020年07月26日 - Change List for CADP Version 2020-g "Aalborg"

HISTORY file item Type Summary
#2614 Improvement The UPC shell-script can now rename former LNT identifiers named "require"
#2615 Improvement LNT2LOTOS now emits more warnings for useless assignments to LNT variables
#2616 Bug fix LNT2LOTOS could generate invalid LOTOS code when translating LNT processes

2020年06月13日 - Change List for CADP Version 2020-f "Aalborg"

HISTORY file item Type Summary
#2609 Bug fix The "-concurrent-places" option of CAESAR.BDD did not apply all its optimizations
#2610 Improvement LNT.OPEN now supports the two recent pragmas "!num_bits" and "!num_card"
#2611 Improvement The two terms "gate" and "exception" have been replaced by "event" in LNT
#2612 Improvement In demos 29 and 32, warnings about non-exhaustive cases have been suppressed
#2613* Improvement LNT has a new "require" clause for preconditions on functions and processes

2020年05月14日 - Change List for CADP Version 2020-e "Aalborg"

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

  • Pierre Bouvier (INRIA/CONVECS)
  • Hugues Evrard (Google, London, UK)
  • Ajay Krishna Muroor (INRIA/CONVECS)

HISTORY file item Type Summary
#2592 Improvement LNT2LOTOS warns about gates listed in synchronization interfaces but not actually accessed
#2593 Improvement The "-concurrent-places" option of CAESAR.BDD uses additional static detection rules
#2594 Improvement The editor style files for LNT have been updated to reflect the latest language enhancements
#2595* Improvement From now on, all pragmas of the LNT language must be written in lowercase letters only
#2596 Bug fix The C code generated by LNT2LOTOS for "case" instructions could trigger GCC warnings
#2597 Improvement LNT2LOTOS now warns about catch-all "case" patterns that do not occur in last position
#2598 Improvement An LNT2LOTOS function was derecursived, enabling larger LNT programs to be processed
#2599 Bug fix The LOTOS code generated by LNT2LOTOS for loops containing "return"s was incorrect
#2600 Improvement Setting $CAESAR_BDD_TIMEOUT to 0 disables marking graph exploration in CAESAR.BDD
#2601 Bug fix LNT2LOTOS did not issue an error when pragma "!int_bits" was followed by a negative value
#2602 Improvement Two module pragmas "!num_bits" and "!num_card" have been added to the LNT language
#2603 Improvement CAESAR.BDD's static exploration algorithm was fully rewritten to perform better and faster
#2604 Improvement The "-dead-places"/"-dead-transitions" options of CAESAR.BDD are faster and more effective
#2605* Improvement In LNT, the symbol "=>" (sometimes confusing with logical implication) was replaced by "->"
#2606 Bug fix LNT2LOTOS could reject meaningful programs having infinite loops in "select" statements
#2607 Bug fix LNT2LOTOS could generate wrong LOTOS code for loops containing "disrupt" statements
#2608 Bug fix The IntToNat() function of the X_INTEGER library did not properly handle negative values

2020年04月13日 - Change List for CADP Version 2020-d "Aalborg"

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

  • Pierre Bouvier (INRIA/CONVECS)

HISTORY file item Type Summary
#2578 Improvement The manual pages for CAESAR.BDD and NUPN better document the !multiple_* pragmas
#2579 Improvement CAESAR.BDD now returns the exit status 6 when the input NUPN is not unit safe
#2580 Improvement The "-check" option of CAESAR.BDD is more consistent when the NUPN is not unit safe
#2581 Improvement CADP binaries for iX86, x64, win32, and mac64 are now built using GCC 6.3 and Clang 3.8
#2582 Improvement The "-mcc" option of CAESAR.BDD was enhanced when !creator and !unit_safe are present
#2583 Bug fix The "-hwb" option of CAESAR.BDD did not return the output specified in its manual page
#2584 Bug fix The "-concurrent-places" option of CAESAR.BDD could return wrong results upon timeout
#2585 Improvement LNT2LOTOS requires some classes of LNT identifiers to be distinct from LOTOS keywords
#2586* Improvement From now on, reserved keywords of the LNT language must be written in lowercase letters
#2587 Improvement From now on, LNT2LOTOS now forbids channel identifiers named "ANY", "Any", etc.
#2588 Improvement For the ORD function of tuples, LNT2LOTOS generates code that causes no GCC warning
#2589* Improvement The predefined function "access" of LNT for sets and lists has been renamed to "element"
#2590 Improvement The LNT language has a new "access" statement to suppress warnings about unused gates
#2591 Improvement demo_11 was enhanced to take advantage of the "access" statement of the LNT language

2020年03月13日 - Change List for CADP Version 2020-c "Aalborg"

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

  • Abdelouahab Chibah (LIG/SLIDE, Grenoble, France)
  • Hugues Evrard (Google, London, UK)
  • Sihem Amer-Yahia (LIG/SLIDE, Grenoble, France)

HISTORY file item Type Summary
#2571 Bug fix The LNT2LOTOS Reference Manual did not properly define the "remove" function
#2572 Improvement All the CADP tools based upon SYNTAX are now built using the TRAIAN 3.0 compiler
#2573 Bug fix LNT2LOTOS mishandled loops with an "if" having a nonterminating "then" and no "else"
#2574 Bug fix An incorrect optimization of MCL_EXPAND could cause wrong results of EVALUATOR
#2575 Bug fix LNT2LOTOS could trigger spurious warnings about impossible rendezvous on "exit" gate
#2576 Improvement LNT2LOTOS now accepts the "!version" module pragma also supported by TRAIAN 3.0
#2577 Improvement The "with" clause of LNT now makes double quotes around function names optional

2020年02月13日 - Change List for CADP Version 2020-b "Aalborg"

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

  • Pierre Bouvier (INRIA/CONVECS)

HISTORY file item Type Summary
#2568 Bug fix Some CADP tools aborted on Solaris 11.4 due to an "old ioctl()-based /proc" issue
#2569 Improvement For clarity and consistency, the CAESAR.OPEN tool was renamed to LOTOS.OPEN
#2570 Improvement From now on, all the CADP executables for SunOS are compiled on OpenIndiana

2020年01月13日 - Change List for CADP Version 2020-a "Aalborg"

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

  • Pierre Bouvier (INRIA/CONVECS)

HISTORY file item Type Summary
#2562 Improvement The half matrix computed by CAESAR.BDD's "-concurrent-places" option was slightly modified
#2563 Improvement The "-concurrent-places" option of CAESAR.BDD generates a matrix with less unknown values
#2564 Improvement The "-mcc" option of CAESAR.BDD computes a better lower bound for the concurrency degree
#2565 Bug fix CAESAR.BDD's "-mcc" option could compute a wrong upper bound for the concurrency degree
#2566 Bug fix The "-density" option of CAESAR.BDD made a division by zero on NUPNs having no transition
#2567 Improvement Two options "-min-concurrency" and "-max-concurrency" have been added to CAESAR.BDD

2019年12月13日 - Change List for CADP Version 2019-l "Pisa"

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

  • Fabio Somenzi (Univ. of Colorado, USA)

HISTORY file item Type Summary
#2555 Bug fix The "-check" and "-mcc" options of CAESAR.BDD could display numbers of markings equal to "-1"
#2556 Improvement The "-mcc" option of CAESAR.BDD now uses a faster algorithm to compute \IsModelLoopFree
#2557 Improvement The "-dead-places" option of CAESAR.BDD uses a complementary algorithm to deliver better results
#2558 Improvement The "-dead-transitions" option CAESAR.BDD was also strengthened with a complementary algorithm
#2559 Improvement The "-mcc" option CAESAR.BDD has been adapted to the 2020 edition of the Model Checking Contest
#2560 Improvement The "-check" option of CAESAR.BDD no longer warns about dead places and dead transitions
#2561 Improvement The diagonal of the matrix produced by CAESAR.BDD's "-concurrent-places" option has changed

2019年11月13日 - Change List for CADP Version 2017-k "Pisa"

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

  • Muhammad Atif (University of Lahore, Pakistan)
  • Pierre Bouvier (INRIA/CONVECS)

HISTORY file item Type Summary
#2547 Improvement The instructions for installing CADP on Windows have been updated
#2548 Improvement The XEUCA_TERM script was enhanced and renamed CADP_XTERM
#2549 Bug fix On Linux without "xterm", "OCIS's "Open shell windows" did not work
#2550 Bug fix The CADP_EDIT shell script could fail on Linux without "xterm"
#2551 Improvement On Linux, TST no longer complains when "xterm" is not installed
#2552 Improvement INSTALLATOR no longer offers a button to edit the ".rhosts" file
#2553 Improvement On 64-bit Linux, INSTALLATOR no longer proposes 32-bit binaries
#2554 Improvement CAESAR and NUPN_INFO now enforce the new-style NUPN syntax

2019年10月13日 - Change List for CADP Version 2019-j "Pisa"

HISTORY file item Type Summary
#2544 Improvement With GCC 6.5, CAESAR no longer triggers a "-Wmaybe-uninitialized" warning
#2545 Improvement CADP_ECHO was modified to work around an Illumos/OpenIndiana problem
#2546 Improvement With GCC 6.5, CAESAR no longer raises a "-Wunused-but-set-variable" warning

2019年09月13日 - Change List for CADP Version 2019-i "Pisa"

HISTORY file item Type Summary
#2539 Bug fix On SunOS, CADP_INDENT could truncate ".h" files located on remote ZFS file systems
#2540 Improvement On SunOS, the TST shell script no longer warns about the absence of /opt/SUNWspro
#2541 Improvement Many CADP tools have been modified to avoid recent compiler warnings on OpenIndiana
#2542 Bug fix MCL_EXPAND produced invalid C code for MCL v5 formulas with both "prob" and "<...>@"
#2543 Improvement INSTALLATOR will no longer offer to install 32-bit executables on macOS 10.15 "Catalina"

2019年08月26日 - Change List for CADP Version 2019-h "Pisa"

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

  • Pierre Bouvier (INRIA/CONVECS)

HISTORY file item Type Summary
#2529 Improvement The "-concurrent-units" option of CAESAR.BDD now uses a compressed output format
#2530 Improvement The "-dead-transitions" option of CAESAR.BDD uses a compressed output format too
#2531 Improvement CAESAR.BDD has been enriched with a new option named "-idle-units"
#2532 Bug fix The "-bits", "-hwb", and "-mcc" options CAESAR.BDD used encoding (e) rather than (i)
#2533 Bug fix CAESAR.BDD's "-mcc" option could core dump on NUPN models having transition labels
#2534 Improvement The "-mcc" option of CAESAR.BDD sets \HasModelNestedUnits only for non-trivial NUPNs
#2535 Improvement CAESAR.BDD better reports transitions with no input place and at least one output place
#2536 Improvement CAESAR.BDD's options "-bits", "-encodings", "-hwb", "-mcc", and "-permanent" are faster
#2537 Improvement A new option "-dead-places" has been added to CAESAR.BDD to detect unreachable places
#2538 Bug fix In some cases, LNT2LOTOS could translate LNT parallel composition operators improperly

2019年07月13日 - Change List for CADP Version 2019-g "Pisa"

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

  • Pierre Bouvier (INRIA/CONVECS)
  • Franco Mazzanti (ISTI-CNR, Pisa, Italy)
  • Gwen Salaün (INRIA/CONVECS)

HISTORY file item Type Summary
#2514 Bug fix On Linux, XTL caused a "double free or corruption" error on certain incorrect XTL files
#2515 Bug fix EXP.OPEN ignored leading spaces in patterns when hiding or renaming labels
#2516 Bug fix Two options of CAESAR.BDD caused segmentation faults (core dump) upon timeout
#2517 Improvement The "-dead-transitions" option of CAESAR.BDD uses a more compact output format
#2518 Bug fix XTL did not terminate when needed the evaluation of "forall" and "exists" expressions
#2519 Improvement The "-concurrent-unit" option of CAESAR.BDD uses a more concise output format
#2520 Improvement CAESAR.BDD now has two new options ("-initial-units" and "-permanent-units")
#2521 Improvement The "-encodings", "-bits", and "-hwb" options of CAESAR.BDD consider permanent units
#2522 Improvement MCL_EXPAND and TST have been updated to support the forthcoming Debian 10 release
#2523 Bug fix The "-check" option CAESAR.BDD displayed wrong messages for NUPN files with labels
#2524 Bug fix The "-nupn" option of EXP.OPEN generated files with syntactically incorrect labels
#2525 Bug fix On recent macOS versions, Apple's System Integrity Protection blocked XSIMULATOR
#2526 Improvement The "-exclusive-places" option of CAESAR.BDD was turned into "-concurrent-places"
#2527 Bug fix SVL could wrongly interpret LOTOS or LNT gate parameters as file patterns of the shell
#2528 Bug fix On 64-bit macOS, OCIS aborted with "Error in startup script: Can't find a usable Init.tcl"

2019年06月13日 - Change List for CADP Version 2019-f "Pisa"

HISTORY file item Type Summary
#2505 Improvement The INSTALLATION directives for macOS now handle Homebrew, in addition to MacPorts
#2506 Bug fix The SVL compiler sometimes propagated the "hide" and "cut" meta-operators incorrectly
#2507 Improvement The NUPN format has been extended to give optional labels to places, transitions, and units
#2508 Bug fix When normalizing probabilities, EVALUATOR 5 could be harmed by rounding errors
#2509 Improvement The XTL language has a new function that converts transition labels to character strings
#2510 Bug fix NUPN_INFO could return exit code 1 although its produced output was correct
#2511 Bug fix EVALUATOR 5 did not detect the case where all outgoing transitions have probability zero
#2512 Improvement The error messages of EVALUATOR 5 concerning probability assignments have been enhanced
#2513 Improvement MCL_EXPAND now performs vacuity checks for formulas "< R > @" when R matches "nil"

2019年05月13日 - Change List for CADP Version 2019-e "Pisa"

HISTORY file item Type Summary
#2496 Improvement The SVL language has been extended to support the probabilistic formulas of MCL 5
#2497 Improvement The NUPN_INFO tool and its manual page have been enhanced in several ways
#2498 Improvement NUPN_INFO can normalize NUPN files by using its new "-canonical-nupn" option
#2499 Bug fix The "-redundant-removal" option of NUPN_INFO could produce invalid NUPN files
#2500 Bug fix LNT_DEPEND could cause segmentation faults on certain architectures (e.g., x64)
#2501 Bug fix LNT_DEPEND could generate repetitive messages and false-positive warnings
#2502 Improvement The NUPN format definition now has more restrictive rules for spaces and tabulations
#2503 Improvement MCL_EXPAND emits fewer warnings about nondeterminism in probabilistic formulas
#2504 Bug fix The parser of CAESAR.BDD could loop infinitely on certain truncated NUPN files

2019年04月13日 - Change List for CADP Version 2019-d "Pisa"

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

  • Pierre Bouvier (INRIA/CONVECS)
  • Philippe Ledent (INRIA/CONVECS)

HISTORY file item Type Summary
#2490 Improvement Various bibliography files shipped with CADP have been updated and corrected
#2491 Bug fix XTL made a segmentation fault when assigning String fields of anonymous tuples
#2492 Bug fix Option "-expand" of EVALUATOR4 could only open files in the current directory
#2493 Improvement The new probabilistic model checker EVALUATOR5 has been added to CADP
#2494 Bug fix The parser of CAESAR.BDD was too laxist and accepted illegal NUPN files
#2495 Improvement The EUCALYPTUS user interface supports EVALUATOR 4 and EVALUATOR 5

2019年03月13日 - Change List for CADP Version 2019-c "Pisa"

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

  • Enrico Magnano (FBK, Torino, Italy)

HISTORY file item Type Summary
#2485 Improvement The "-exclusive-places" option of CAESAR.BDD now uses a compressed format for its output
#2486 Improvement The MCL_EXPAND 4.1 compiler has been replaced by a new version MCL_EXPAND 5.0
#2487 Bug fix MCL_EXPAND 4.1 could generate invalid C code for MCL formulas containing <{... ?x:T}+> P(x)
#2488 Improvement The CAESAR_GRAPH manual page better defines CAESAR_FORMAT_{STATE, LABEL}
#2489 Improvement The CAESAR_GRAPH manual page better defines CAESAR_BODY_{STATE, LABEL}

2019年02月13日 - Change List for CADP Version 2019-b "Pisa"

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

  • Armen Inants (INRIA/CONVECS)
  • Jules Lefrère (MOSIG/HECS)

HISTORY file item Type Summary
#2480 Improvement The CADP manual pages have been extended and corrected at various places
#2481 Improvement A new "-depend" option was added to LNT.OPEN, LNT2LOTOS, and LNT_DEPEND
#2482 Improvement LNT_DEPEND now supports the redefinition of standard LNT libraries by the users
#2483 Bug fix EVALUATOR4 core dumped on formulas having undefined type names prefixed by "A"
#2484 Improvement A new option "-redundant-removal" has been added to NUPN_INFO

2019年01月13日 - Change List for CADP Version 2019-a "Pisa"

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

  • Yann Genevois (INRIA/VASY)
  • Armen Inants (INRIA/CONVECS)

HISTORY file item Type Summary
#2475 Improvement A standalone manual page describing the simple and full SEQ formats has been written
#2476 Improvement A manual page defining the BES (Boolean Equation Systems) format has been written
#2477 Improvement A CAESAR_SOLVE_2 library was added to solve Linear Equation Systems on the fly
#2478 Bug fix The former LNT_DEPEND shell script was slow and mishandled nested LNT comments
#2479 Improvement The Help page of the EUCALYPTUS graphical user interface was updated and enhanced

2018年12月13日 - Change List for CADP Version 2018-l "Uppsala"

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

  • David N. Jansen (Radboud Universiteit, The Netherlands)
  • Thomas Lambolais (Ecole des Mines, Alès, France)

HISTORY file item Type Summary
#2467 Improvement A new option "-depend" has been added to EXP2C and EXP.OPEN
#2468 Bug fix XTL could core dump on external types without !printedby or !comparedby
#2469 Improvement The CADP toolbox has been ported to SunOS 5.11 OpenIndiana ("Hipster")
#2470 Bug fix XTL could generate incorrect C code for external functions
#2471 Bug fix With GNU-indent on Solaris, cadp_indent did not remove *~ backup files
#2472 Improvement INSTALLATOR now emits better messages about stable and beta versions
#2473 Improvement A new option "-trivial" has been added to the CAESAR.BDD tool
#2474 Improvement The INSTALLATION_MACOS directives for macOS have been enhanced

2018年11月13日 - Change List for CADP Version 2018-k "Uppsala"

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

  • Lina Marsso (INRIA/CONVECS)
  • Franco Mazzanti (ISTI-CNR, Pisa, Italy)

HISTORY file item Type Summary
#2457 Improvement CAESAR.BDD now distinguishes "redundant" and "void" units, forbidding the latter
#2458 Bug fix The "-trivial-units" option of NUPN_INFO could ignore some "!unit_safe" pragmas
#2459 Improvement The SVL manual page now better describes the list of predefined shell variables
#2460 Improvement CAESAR.BDD has been extended with five new options to query NUPN units
#2461 Improvement The CADP_TEMPORARY script has a new "-t" option enabling new uses
#2462 Bug fix LNT2LOTOS could generate incorrect LOTOS code for LNT exception parameters
#2463 Improvement The NUPN_INFO tool now implements the "place-fusion" abstraction
#2464 Bug fix The 64-bit binaries of CADP compilers could cause segmentation faults on macOS
#2465 Improvement The error and warning messages of most CADP compilers have been unified
#2466 Improvement A new option "-void-removal" has been added to NUPN_INFO

2018年10月13日 - Change List for CADP Version 2018-j "Uppsala"

HISTORY file item Type Summary
#2449 Bug fix The CAESAR_GRAPH manual page was out of date wrt CAESAR_TYPE_FORMAT
#2450 Improvement LNT2LOTOS now forbids attaching "!external" pragmas to constructors
#2451 Improvement A thorough tutorial/survey on compositional verification has been provided
#2452 Improvement Six new options "-min-*" and "-max-*" have been added to the CAESAR.BDD tool
#2453 Improvement A new tool NUPN_INFO with its option "-trivial-units" has been added to CADP
#2454 Bug fix FSP.OPEN and LNT.OPEN could generate non-unique names for temporaries
#2455 Improvement The CADP toolbox has been ported to version 10.14 "Mojave" of macOS
#2456 Improvement The CADP shell scripts no longer modify the environment variable $USER

2018年09月13日 - Change List for CADP Version 2018-i "Uppsala"

HISTORY file item Type Summary
#2441 Improvement demo_11 has been enhanced in several respects and made 4-5 minutes faster
#2442 Bug fix XTL made a segmentation fault when comparing or printing values of external types
#2443 Bug fix Since CADP 2018-h, option "-clean" of SVL could display a spurious "executing..." line
#2444 Bug fix The XTL compiler forgot to erase ".xp" files in case of lexical or syntactic errors
#2445 Improvement Empty lines are now removed from the output of SVL's "livelock"/"deadlock" statements
#2446 Improvement XTL now checks all the C identifiers specified in the pragmas "!implementedby", etc.
#2447 Improvement It is now permitted to have "empty" SVL properties consisting only of shell commands
#2448 Improvement The SVL script of demo_17 now uses LNT operators and parameterized SVL properties

2018年08月26日 - Change List for CADP Version 2018-h "Uppsala"

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

  • Lian Apostol (INRIA/CONVECS)
  • Etienne Lantreibecq (STMicroelectronics, Grenoble)
  • Lina Marsso (INRIA/CONVECS)

HISTORY file item Type Summary
#2434 Improvement The demo_06 better shows the mapping between TLS 1.3 specs and LNT code
#2435 Improvement The demo_17 (distributed leader election protocol) was translated to LNT
#2436 Bug fix EXP.OPEN generated ".sync" files without escaping special characters .[]*\^$
#2437 Improvement A new macro SVL_COMMAND_FOR_CLEAN was added for SVL's -clean option
#2438 Improvement A new demo_11 (STMicroelectronics' Dynamic Task Dispatcher) has been added
#2439 Improvement Many demos now take advantage of the SVL_COMMAND_FOR_CLEAN macro
#2440 Bug fix On Windows, CONTRIBUTOR halted on "Unable to create the archive" error

2018年07月13日 - Change List for CADP Version 2018-g "Uppsala"

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

  • Gianluca Barbon (INRIA/CONVECS)
  • Hermann Felbinger (Graz University of Technology, Austria)
  • Hana Mkaouar (ENIS, Tunisia)

HISTORY file item Type Summary
#2427 Improvement EVALUATOR and XTL have a new option "-depend" that displays library dependencies
#2428 Bug fix CAESAR and CAESAR.ADT could face buffer overflow when including 256 libraries
#2429 Bug fix Since CADP 2018-f, TGV had stopped working due to protection violation
#2430 Bug fix CAESAR and CAESAR.ADT sometimes displayed incorrect file names for included files
#2431 Improvement CAESAR and CAESAR.ADT have a new option "-depend" to display library dependencies
#2432 Bug fix Since CADP 2018-f, EVALUATOR 3 and 4 could fail on certain versions of Ubuntu
#2433 Improvement The new SCRUTATOR tools allows pruning labelled transition systems on the fly

2018年06月13日 - Change List for CADP Version 2018-f "Uppsala"

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

  • Lina Marsso (INRIA/CONVECS)

HISTORY file item Type Summary
#2422 Improvement MCL v3 formulas of some demos have been modified to avoid MCL_EXPAND warnings
#2423 Improvement EVALUATOR3 now implements the option operator "?" in MCL v3 formulas
#2424 Bug fix For some MCL v4 formulas, MCL_EXPAND triggered a GCC "-Wtype-limits" warning
#2425 Improvement A new demo_06 (Transport Layer Security 1.3 handshake protocol in LNT) was added
#2426 Improvement TGV has a new "-self" option and its manual page has been enhanced

2018年05月26日 - Change List for CADP Version 2018-e "Uppsala"

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

  • Marlena Olszewska (AGH University of Science and Technology, Krakow, Poland)
  • Natalia Kuczma (AGH University of Science and Technology, Krakow, Poland)

HISTORY file item Type Summary
#2412 Improvement Two new overarching manual pages for MCL and EVALUATOR have been added
#2413 Improvement In MCL v3 (EVALUATOR 3), operator "@" now has the same syntax as in MCL v4
#2414 Improvement SVL can now compute "deadlock" and "livelock" statements using EVALUATOR 3 and 4
#2415 Improvement In MCL v3 (EVALUATOR 3), operator "." now has higher precedence than operator "|"
#2416 Improvement EVALUATOR 3 and EVALUATOR 4 now share the same MCL_EXPAND pre-processor
#2417 Improvement EVALUATOR displays better error messages for MCL formulas with alternation > 1
#2418 Improvement The Help window of the EUCALYPTUS graphical user interface has been enhanced
#2419 Improvement TST detects two new situations in which the LICENSE file is not properly installed
#2420 Improvement EVALUATOR 3 now displays clearer error messages if invoked on an MCL v4 formula
#2421 Improvement The CADP toolbox has been ported to the Oracle Solaris 11 operating system

2018年04月26日 - Change List for CADP Version 2018-d "Uppsala"

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

  • Lina Marsso (INRIA/CONVECS)

HISTORY file item Type Summary
#2407 Bug fix MCL_EXPAND sent obscure messages for incorrect MCL formulas containing "library" clauses
#2408 Improvement A new option "-source file:line" has been added to XTL and XTL_EXPAND
#2409 Improvement A new option "-source file:line" was added to EVALUATOR 3 and EVALUATOR 4
#2410 Improvement The SVL compiler emits better error messages in case of erroneous MCL or XTL formulas
#2411 Improvement demo_12 (Message Authenticator Algorithm) is now better documented by a scientific article

2018年03月13日 - Change List for CADP Version 2018-c "Uppsala"

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

  • Lian Apostol (INRIA/CONVECS)
  • Hugues Evrard (Imperial College, London, UK)
  • Alexander Graf-Brill (Saarland University, Germany)
  • Franco Mazzanti (ISTI/CNR, Pisa, Italy)
  • Jan Staunton (University of York, UK)

HISTORY file item Type Summary
#2400 Improvement A 64-bit version of CADP for macOS is now available (architecture name: "mac64")
#2401 Bug fix On Windows, INSTALLATOR failed to detect if it ran with administrator privilege
#2402 Improvement cadp_cygwin.com now properly checks if it executes with administrator privilege
#2403 Improvement By default, OCIS always sets the environment variable $CADP_TMP to "/tmp"
#2404 Bug fix The -mcc option of CAESAR.BDD could compute \HasModelNestedUnits wrongly
#2405 Improvement The GC library was upgraded from v6.8 to v7.6.4, avoiding some crashes on Solaris
#2406 Bug fix Invoked with options -exec -external, CAESAR would loop forever on 64-bit Linux

2018年02月13日 - Change List for CADP Version 2018-b "Uppsala"

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

  • Lian Apostol (INRIA/CONVECS)
  • Søren Enevoldsen (Aalborg University, Denmark)
  • Holger Hermanns (Saarland University, Germany)

HISTORY file item Type Summary
#2383 Improvement BCG_STEADY/BCG_TRANSIENT now accept continuous-time Markov chains having only one state
#2384 Bug fix Since CADP 2018-a, INSTALLATOR partly failed on Windows ("Error while executing chmod")
#2385 Improvement The installation web page now recommends erasing installator.shar before downloading a new copy
#2386 Improvement The OPEN/CAESAR manual pages now specify full prototypes for higher-order function parameters
#2387 Bug fix On Windows, INSTALLATOR and TST emitted spurious warnings when Cygwin is not installed in C:/
#2388 Improvement EVALUATOR now reports line numbers in source ".mcl" files rather than intermediate ".xm" files
#2389 Improvement The "-thr" option of BCG_STEADY/BCG_TRANSIENT is no longer always selected by default
#2390 Improvement Line numbers are now more precise in the warning and error messages emitted by LNT2LOTOS
#2391 Improvement The "-thr" option of BCG_STEADY/BCG_TRANSIENT warns when no rate transition has a label
#2392 Improvement When pre-processing ".mcl" files, MCL_EXPAND 3 and MCL_EXPAND 4 now use less memory
#2393 Bug fix Due to rounding errors, BCG_STEADY/BCG_TRANSIENT could flag probabilities greater than 1
#2394 Bug fix EVALUATOR 3 forgot to remove the intermediate ".xm" files generated from incorrect ".mcl" files
#2395 Bug fix BCG_STEADY/BCG_TRANSIENT confused state numbers (0..n) and vector/matrix indexes (1..n+1)
#2396 Improvement Probabilistic loops are now rejected (rather than ignored) by BCG_STEADY/BCG_TRANSIENT
#2397 Improvement DISTRIBUTOR now triggers global distributed termination as soon as a local state table overflows
#2398 Bug fix More precise line numbers are now displayed in the warning and error messages of EVALUATOR 3
#2399 Improvement DISTRIBUTOR uses a better naming scheme when generating its log files on remote machines

2018年01月13日 - Change List for CADP Version 2018-a "Uppsala"

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

  • Lian Apostol (INRIA/CONVECS)
  • Anne-Lise Courbis (Ecole des Mines d'Alès, France)

HISTORY file item Type Summary
#2373 Improvement BCG_MERGE emits better error messages and sends them to stdout rather than stderr
#2374 Improvement A new option "-v" was added to SVL so as to set variables from the command line
#2375 Improvement TST now warns if not invoked from the Windows drive on which CADP has been installed
#2376 Improvement Preliminary changes have been made in scripts towards a 64-bit Windows version of CADP
#2377 Bug fix On Windows with Cygwin not installed in C:/, CADP_POSTSCRIPT would not locate Evince
#2378 Improvement All include files named "X_*.h" have been enhanced, and three of them shortened
#2379 Improvement On Windows, it is no longer needed to set $CADP_TMP to the result of "cadp_path -tmp"
#2380 Improvement TST now displays information about virtualization and the behaviour of Cygwin pipes
#2381 Bug fix On Windows with Cygwin not installed in C:/, INSTALLATOR failed to set file permissions
#2382 Bug fix On Windows, TST reported a non-existent problem: "Cygwin version is obsolete (bug #3)"

2017年12月13日 - Change List for CADP Version 2017-l "Sophia Antipolis"

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

  • Anne-Lise Courbis (Ecole des Mines, Alès, France)
  • Zhen Zhang (Utah State University, USA)

HISTORY file item Type Summary
#2364 Bug fix Since CADP 2017-i, SVL could stop abruptly when executing some "grep" commands
#2365 Bug fix MCL_EXPAND 4 could abort with error #006 when processing some incorrect MCL files
#2366 Improvement From now on, XTL_EXPAND displays stricter warnings about macros in XTL and MCL files
#2367 Bug fix CADP no longer worked on Windows after Cygwin changes modifying the behaviour of pipes
#2368 Improvement XTL libraries and demo_14 have been modified to avoid the new warnings of XTL_EXPAND
#2369 Bug fix Some CADP tools did not work properly on Windows when Cygwin was not installed in C:/
#2370 Bug fix On 64-bit Linux, BCG_MIN.OLD (i.e., version 1.7) systematically aborted (internal error #1)
#2371 Improvement MCL_EXPAND 4 now displays better warning and error messages, with accurate line numbers
#2372 Improvement BCG_MERGE and the CAESAR_NETWORK library have been reshaped to compile with Clang

2017年11月13日 - Change List for CADP Version 2017-k "Sophia Antipolis"

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

  • Alexander Graf-Brill (Saarland University, Germany)
  • Franco Mazzanti (ISTI/CNR, Pisa, Italy)
  • Nazmus Sakib (Utah State University, USA)
  • Jan Staunton (University of York, UK)

HISTORY file item Type Summary
#2354 Improvement A recent publication describing the history of LNT has been added
#2355 Bug fix CAESAR and CAESAR.ADT could access an array out of its bounds
#2356 Improvement The TST shell script better recognizes Linux distributions such as CentOS
#2357 Improvement The definition of ADT_FBY() in the X_ACTION library has been enhanced
#2358 Bug fix Since CADP 2017-e, the demos 19 and 38 no longer worked on macOS
#2359 Bug fix The CAESAR_NETWORK library could incorrectly reject correct ".gcf" files
#2360 Improvement Preliminary steps have been done towards a 64-bit macOS version of CADP
#2361 Improvement Pragma "external" is no longer a reserved keyword of the LNT language
#2362 Improvement CADP now supports Apple computers running macOS 10.13 "High Sierra"
#2363 Improvement EUCALYPTUS better supports various Linux desktops: Gnome, MATE, etc.

2017年10月13日 - Change List for CADP Version 2017-j "Sophia Antipolis"

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

  • Aymane Bouzafour (Tiempo, Montbonnot, France)

HISTORY file item Type Summary
#2342 Improvement LPP now adds implicit ".lnt" extensions to its input and output file names
#2343 Bug fix LPP now forbids non-alphanumeric characters in its input and output file names
#2344 Bug fix The SIGSEGV signal was improperly handled in the OPEN/CAESAR library
#2345 Bug fix OCIS would crash if an exception was raised while firing an initial transition
#2346 Improvement A new type pragma "!bits N" replacing "!card -N" was added to the LNT language
#2347 Improvement Pragmas "comparedby", "printedby", etc. are no longer LNT reserved keywords
#2348 Bug fix Since CADP 2017-i, the "-diag" option of Evaluator 4 caused link-edit errors
#2349 Bug fix TGV did not properly check whether all its calls to malloc() return NULL or not
#2350 Improvement The LNT2LOTOS translator now warns about gates declared but never used
#2351 Improvement The instructions for installing CADP no longer discuss Windows XP and Vista
#2352 Bug fix The list of LNT keywords was outdated in the documentation and editor style files
#2353 Improvement Style files for the EXP format of CADP are now provided for various text editors

2017年09月13日 - Change List for CADP Version 2017-i "Sophia Antipolis"

HISTORY file item Type Summary
#2329 Improvement The OPEN/CAESAR library was enriched with CAESAR_TYPE_FORMAT and its related primitives
#2330 Improvement OPEN/CAESAR functions CAESAR_FORMAT_xxx and CAESAR_MAX_FORMAT_xxx have evolved
#2331 Improvement The OPEN/CAESAR API, compilers, and application tools also evolved in the same way as #2330
#2332 Bug fix Pragma numeric values starting with a zero were incorrectly translated to C by LNT2LOTOS
#2333 Bug fix The CAESAR_NETWORK library did not consider user names when comparing directories
#2334 Improvement The BCG and OPEN/CAESAR include files have been simplified by factorizing portability code
#2335 Improvement The cadp_indent script now recovers from some failures of the Solaris "indent" command
#2336 Improvement The -debug option of SVL now stops as soon as some command exits with a non-zero status
#2337 Bug fix Several memory-allocation errors possibly leading to buffer overflows were present in TGV
#2338 Improvement TGV now executes silently by default, unless it is invoked with its new option -verbose
#2339 Improvement A new option -monitor was added to TGV to supervise the progress of test-case generation
#2340 Bug fix EXP.OPEN could emit incorrect warnings about probabilistic and stochastic transitions
#2341 Bug fix The -verif option of TGV could stop abruptly with an error message related to BCG_WRITE_EDGE

2017年08月26日 - Change List for CADP Version 2017-h "Sophia Antipolis"

HISTORY file item Type Summary
#2320 Bug fix In the OPEN/CAESAR manual, the CAESAR_FORMAT_STATE() primitive was incorrectly specified
#2321 Bug fix LNT2LOTOS did not always check semantic constraint (PE3) for gate parameters of function calls
#2322 Improvement The documentation for LNT2LOTOS and REDUCTOR has been enhanced
#2323 Bug fix LNT2LOTOS did not implement checks for the semantic constraints (COM3), (FE2), and (H3)
#2324 Improvement The cadp_cc shell script now takes care of the $MALLOC_DEBUG variable on Solaris
#2325 Improvement Several error messages displayed by LNT2LOTOS have been enhanced in various ways
#2326 Bug fix A memory allocation bug in CAESAR.ADT caused unfrequent core dumps on 32-bit Solaris
#2327 Improvement LNT2LOTOS emits better error messages for uninitialized variables used in Boolean guards
#2328 Improvement The CAESAR_NETWORK library for distributed verification tools displays better error messages

2017年07月26日 - Change List for CADP Version 2017-g "Sophia Antipolis"

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

  • Aymane Bouzafour (Tiempo, Montbonnot, France)
  • Wellison Raul Mariz Santos (Univ. Rio Grande do Norte, Brazil)
  • Enno Ruijters (University of Twente, The Netherlands)
  • Gianni Zampedri (FBK, Torino, Italy)

HISTORY file item Type Summary
#2306 Improvement An overview publication about DLC (Distributed LNT Compiler) has been added
#2307 Improvement The "-ratebranching" option of EXP.OPEN was split into two options "-rate -branching"
#2308 Improvement EXP.OPEN's error messages about synchronization vectors now give a precise line number
#2309 Bug fix SVL could invoke EXP2C without passing the options contained in $EXP_OPEN_OPTIONS
#2310 Bug fix The static semantics of LNT did not require formal gate parameters to be pairwise distinct
#2311 Improvement SVL now warns if $EXP_OPEN_OPTIONS contains the deprecated "-ratebranching" option
#2312 Improvement SVL now warns if $EXP_OPEN_OPTIONS contains incompatible partial-order reduction options
#2313 Improvement One can now invoke RFL with no option to prepare a license for the current machine only
#2314 Improvement The LNT2LOTOS Reference Manual has been extensively revised, enhanced, and simplified
#2315 Improvement SVL no longer infers a partial-order reduction option if $EXP_OPEN_OPTIONS contains one
#2316 Improvement CADP now better supports recent versions of Linux, such as Ubuntu 16.04.2 and Debian 9
#2317* Improvement The definition of LNT processes was modified to unify both concepts of gates and exceptions
#2318 Improvement The demo_05 has been adapted to obey the unification of gates and exceptions in LNT
#2319 Improvement LNT2LOTOS now checks directly if the gates used in a "par" operator have been declared

2017年06月13日 - Change List for CADP Version 2017-f "Sophia Antipolis"

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

  • Sarah Chabane (University of Boumerdes, Algeria)
  • Laurent Georget (Centrale/Supelec, Rennes, France)
  • Raquel Oliveira (IRIT, Toulouse, France)

HISTORY file item Type Summary
#2300 Improvement LNT2LOTOS now supports a new pragma "!card" to trigger hash-consing for LNT types
#2301 Bug fix File extensions were improperly handled by EXP.OPEN when opening its input files
#2302 Improvement EXP.OPEN now warns about empty labels and labels containing only blanks
#2303 Improvement The CADP_CC script now works with Ubuntu 17.04 and GCC-6 position-independent code
#2304 Improvement EXP.OPEN displays better warnings when probabilistic or stochastic labels are synchronized
#2305 Improvement Two new options "-prob" and "-rate" have been added to modify EXP.OPEN's behaviour

2017年05月13日 - Change List for CADP Version 2017-e "Sophia Antipolis"

HISTORY file item Type Summary
#2295 Improvement LPP now implements LNT character strings in a more efficient manner
#2296 Improvement The OPEN/CAESAR signal-handling primitives have been modified and enriched
#2297 Bug fix The OPEN/CAESAR library failed to properly execute handlers for signal SIGSEGV
#2298 Improvement CAESAR and CAESAR.ADT now explain errors during evaluation of constants
#2299 Bug fix Option "-comments" of CAESAR and CAESAR.ADT failed on long LOTOS identifiers

2017年04月26日 - Change List for CADP Version 2017-d "Sophia Antipolis"

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

  • Lina Marsso (INRIA/CONVECS)

HISTORY file item Type Summary
#2290 Bug fix CAESAR.ADT had a memory error that showed up on Solaris for very large LOTOS specifications
#2291 Improvement LNT2LOTOS now optimizes "if-then-else" statements containing duplicated assignments
#2292 Improvement LNT2LOTOS further optimizes functions containing many "assert" intertwined with assignments
#2293 Improvement On CentOS, the TST shell script now displays properly the Glibc version number
#2294 Improvement The LNT specification of demo_12 was enriched with the test vectors of [ISO 8731-2:1992, Table 6]

2017年03月27日 - Change List for CADP Version 2017-c "Sophia Antipolis"

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

  • Lina Marsso (INRIA/CONVECS)

HISTORY file item Type Summary
#2285 Improvement The LNT and LOTOS specifications of the MAA (demo_12) have been further enhanced
#2286 Bug fix In rare cases, LNT2LOTOS could generate wrong LOTOS code for "case" statements
#2287 Improvement The LNT and LOTOS specifications of the Production Cell (demo_19) have been simplified
#2288 Improvement The LNT2LOTOS translator was enhanced to better handle large LNT functions
#2289 Improvement The LNT2LOTOS translator now optimizes the generated LOTOS conditional equations

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:

  • Lina Marsso (INRIA/CONVECS)

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:

  • Lina Marsso (INRIA/CONVECS)

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:

  • Anne-Lise Courbis (Ecole des Mines d'Alès, France)
  • Hugues Evrard (INRIA/CONVECS)
  • Paula-Andrea Lago-Martinez (LIG, Grenoble, France)
  • Jules Lefrere (Univ. Grenoble Alpes, France)
  • Lina Marsso (INRIA/CONVECS)
  • Marcin Szpyrka (AGH University of Science and Technology, Krakow, Poland)

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:

  • Anne-Lise Courbis (Ecole des Mines, Alès, France)
  • Alexander Graf-Brill (Saarland University)
  • Thomas Lambolais (Ecole des Mines, Alès, France)
  • Hauke Pribnow (Univ. Muenster, Germany)
  • Ken Turner (University of Stirling, Scotland, UK)

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:

  • Paula-Andrea Lago-Martinez (LIG/SIGMA, Grenoble, France)

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:

  • Hugues Evrard (INRIA/CONVECS)

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:

  • Hauke Pribnow (Univ. Muenster, Germany)

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:

  • Hugues Evrard (INRIA/CONVECS)
  • Hauke Pribnow (Univ. Muenster, Germany)

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:

  • Pierre Gaufillet (IRT St Exupery, Toulouse, France)
  • Matthias Güdemann (INRIA/CONVECS)
  • Pascal Poizat (LIP6, Paris, France)
  • Hauke Pribnow (Univ. Muenster, Germany)
  • Maciej Szymkat (AGH University of Science and Technology, Krakow, Poland)

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:

  • Gérard Berry (Collège de France, Paris)
  • Hauke Pribnow (Univ. Münster, Germany)

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:

  • Hugues Evrard (INRIA/CONVECS)
  • Hernan Ponce de Leon (Aalto University, Finland)

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:

  • Benoît Barbot (LACL, Universite Paris-Est Creteil, France)

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:

  • Hugues Evrard (INRIA/CONVECS)
  • Eric Leo (INRIA/CONVECS)

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:

  • Eric Leo (INRIA/CONVECS)
  • Gianluca Barbon (INRIA/CONVECS)

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:

  • Jose Manuel Colom (Universidad de Zaragoza, Spain)
  • Maciej Koutny (Newcastle University, UK)
  • Eric Leo (INRIA/CONVECS)
  • Manuel Silva (Universidad de Zaragoza, Spain)
  • Zhen Zhang (University of Utah, USA)

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:

  • Pierre Boullier (INRIA/ALPAGE, Roquencourt, France)
  • Fabio Somenzi (University of Colorado, USA)

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:

  • Eric Leo (INRIA/CONVECS)
  • Gwen Salaun (INRIA/CONVECS)

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:

  • Hernan Ponce de Leon (Aalto University, Finland)

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:

  • Fatma Jebali (INRIA/CONVECS)

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:

  • Yin Chaoran (North China University of Technology, Beijing, China)
  • Hugues Evrard (INRIA/CONVECS)
  • Eric Leo (INRIA/CONVECS)
  • Julian Jacques Maurer (Saarland University, Germany)
  • Jose-Ignacio Requeno (INRIA/CONVECS)

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:

  • Fatma Jebali (INRIA/CONVECS)
  • Damien Thivolle (INRIA/VASY)

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:

  • Hugues Evrard (INRIA/CONVECS)
  • Eric Leo (INRIA/CONVECS)
  • Zhen Zhang (University of Utah, USA)

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:

  • Soraya Arias (INRIA Grenoble, France)
  • Eric Leo (INRIA/CONVECS)
  • Guillaume Maudoux (Universitée Catholique de Louvain, Belgium)
  • Jens Meyer (Saarland University, Germany)
  • Xiaoxiao Yang (RWTH Aachen, Germany)

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:

  • Soraya Arias (INRIA Grenoble, France)
  • Holger Hermanns (Saarland University, Germany)
  • Eric Leo (INRIA/CONVECS)
  • Stephan Merz (INRIA Nancy, France)
  • Hana Mkaouar (ENIS, Tunisia)
  • Sylvain Rampacek (Univ. de Bourgogne, France)
  • Xiaoxiao Yang (RWTH Aachen, Germany)

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:

  • Hugues Evrard (INRIA/CONVECS)

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:

  • Hugues Evrard (INRIA/CONVECS)

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:

  • Felix Freiberger (Saarland University, Germany)
  • Holger Hermanns (Saarland University, Germany)
  • Raquel Oliveira (LIG, Grenoble, France)
  • Xiaoxiao Yang (RWTH Aachen, Germany)

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:

  • Pedro d'Argenio (University of Cordoba, Argentina)
  • Pascal Poizat (LIP6, Paris, France)

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:

  • Hugues Evrard (INRIA/CONVECS)

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:

  • Alexander Graf-Brill and Julian Maurer (Saarland University, Germany)

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:

  • Ludovic Apvrille (Telecom ParisTech, Sophia-Antipolis, France)
  • Marie-Dominique Cabanne (LAAS-CNRS, Toulouse, France)
  • Kevin Corre (INRIA Rennes, France)
  • Monika Heiner (Brandenbourg University of Technology, Cottbus, Germany)
  • Nuno Oliveira (Universidade do Minho, Braga, Portugal)
  • Antonella Santone (Universita del Sannio, Benevento, Italy)

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:

  • Javier Garcia (Universidad Politechnica de Valencia, Spain)
  • Guido Josquin (University of Twente, The Netherlands)
  • Raquel Oliveira (LIG, Grenoble, France)
  • Dimitris Vekris (University Paris Est, France)
  • David M. Williams (Free University Amsterdam, The Netherlands)

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:

  • Ludovic Apvrille (Telecom ParisTech, Sophia-Antipolis, France)
  • Alexander Graf-Brill (Saarland University, Germany)
  • Hugues Evrard (INRIA, Grenoble, France)
  • Alexandre Hamez (ISAE, Toulouse, France)
  • Lom Messan Hillah (LIP6, Paris, France)
  • Raquel Oliveira (LIG, Grenoble, France)
  • Gwen Salaün (Grenoble INP, Grenoble, France)

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:

  • Alexander Graf-Brill (Saarland University, Germany)
  • Alexandre Hamez (ISAE, Toulouse, France)
  • Lom Messan Hillah (LIP6, Paris, France)
  • Raquel Oliveira (LIG, Grenoble, France)

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:

  • Javier Garcia (Universidad Politechnica de Valencia, Spain)
  • Alexander Graf-Brill (Saarland University, Germany)
  • Abderahman Kriouile (STMicroelectronics, Grenoble, France)
  • Raquel Oliveira (LIG, Grenoble, France)
  • Francois Vernadat (LAAS-CNRS, Toulouse, France)
  • Zhen Zhang (University of Utah, USA)

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:

  • Alexandre Hamez (ISAE, Toulouse, France)
  • Raquel Oliveira (LIG, Grenoble, France)
  • Zhen Zhang (University of Utah, USA)

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:

  • Rabea Ameur-Boulifa (Telecom ParisTech, Paris, France)
  • Raquel Oliveira (LIG, Grenoble, France)
  • Francois Vernadat (LAAS-CNRS, Toulouse, France)
  • Zhen Zhang (University of Utah, USA)

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.283 last updated on 2025年11月14日 11:10:50

Back to the CADP Home Page

AltStyle によって変換されたページ (->オリジナル) /