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.
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:
- Holger Hermanns (Saarland University, Germany)
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:
- Lucie Muller (LIG, Univ. Grenoble Alpes, France)
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 C24 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:
- Daniele Gorla (Sapiensa University, Rome, Italy)
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:
- Pierre Boullier (INRIA/CONVECS)
- Tamme Edmunds (RWTH Aachen University, Aachen, Germany)
- Akram Idani (LIG, Grenoble, France)
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:
- Alex Arnold (York University, Toronto, Canada)
- Ruth Bezabeh (York University, Toronto, Canada)
- Shaharyar Choudhry (York University, Toronto, Canada)
- Rafael Dolores (York University, Toronto, Canada)
- Joshua Genat (York University, Toronto, Canada)
- Erika Grandy (York University, Toronto, Canada)
- Suraj Gupta (INRIA/CONVECS)
- Madison Hartley (York University, Toronto, Canada)
- Mate Korognai (York University, Toronto, Canada)
- James Le (York University, Toronto, Canada)
- Irsa Nasir (York University, Toronto, Canada)
- Zachary Ross (York University, Toronto, Canada)
- Gwen Salaun (INRIA/CONVECS)
- Suha Siddiqui (York University, Toronto, Canada)
- Joseph Spagnuolo (York University, Toronto, Canada)
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:
- Marck-Edward Kemeh (Univ. Grenoble Alpes, France)
- Oussama Oulkaid (Univ. Grenoble Alpes, France)
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:
- Meriem Ouederni (IRIT-INP Toulouse, France)
- Gwen Salaun (INRIA/CONVECS)
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:
- Marck-Edward Kemeh (Univ. Grenoble Alpes, France)
- Franco Mazzanti (ISTI-CNR, Pisa, Italy)
- Oussama Oulkaid (Univ. Grenoble Alpes, France)
- Vincent Ribot (Univ. Grenoble Alpes, France)
- Jolahn Vaudey (Univ. Grenoble Alpes, France)
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:
- Pierre Boullier (INRIA/CONVECS)
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:
- Marco Bernardo (University of Urbino, Italy)
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 |
Former changes to CADP (items ranging from #001 to #1723) are described in the HISTORY file of the CADP distribution.
Version 1.251 last updated on 2024/10/13 12:41:10
Back to the CADP Home Page