This newsletter is available from the CADP Home page. A few URLs in this page have been updated in November 2011.
The VASY team at INRIA Rhone-Alpes / DYADE and the VERIMAG laboratory are pleased to announce the availability of a new release of their protocol engineering toolbox CADP (CAESAR/ALDEBARAN Development Package).
This new version is named 97a "Twente" and is dated June, 6, 1997. It supersedes the existing one (Version Z dated December, 6, 1996).
Following the tradition set by some important software companies to give city names to their software, we have chosen to label Version 97a of CADP with the name "Twente", because this new version was demonstrated publicly for the first time during the TACAS'97 Workshop organized in April 1997 at the University of Twente (The Netherlands), and because we acknowledge the major role played by the University of Twente in the development of formal methods in general, and LOTOS in particular.
Compared to version Z, version 97a "Twente" of CADP brings significant progress. It provides 28 bugs fixes and introduces 34 improvements and new features, for instance:
The EUCALYPTUS v2.2 graphical interface has been made more robust, after months of intensive use by INRIA scientists and by hundreds of students in several engineering schools.
CAESAR has been made faster: on several large examples, we noticed that the graph generation time was divided by a factor ranging from 2 to 160.
CAESAR has a new functioning mode (named EXEC/CAESAR) for generating C code to be directly embedded in application programs.
CAESAR has a simplified interface (a lot of useless options have been removed).
CAESAR.ADT has a new "-external" option for generating skeletons of ".f" and ".t" files.
The new version of EVALUATOR is more efficient and implements two different strategies for local and global evaluation of modal mu-calculus formulas. The syntax of mu-calculus formulas has been extended with new operators.
There is a new MONITOR tool for monitoring in real-time the generation of graphs encoded in the BCG format. This tool is invoked by the "-monitor" option of CAESAR, GENERATOR, and REDUCTOR.
When graph generation is interrupted by the user, all files are now closed properly, in order to allow verification on the partial graphs already generated.
There is now a "LOTOS mode" to be used with the EMACS and XEMACS editors.
A lot of minor portability issues have been solved and the installation procedure has been enhanced.
Three new demos are provided: two of them illustrate compositional verification; the third one demonstrates the use of EXEC/CAESAR on the famous "Production Cell" case-study proposed by FZI Karlsruhe.
You may find a detailed list of bug fixes and improvements below. We hope that you will enjoy this new version.
CADP'97 - Status, Applications, and Perspectives
This article gives an overview of the most recent features implemented in CADP (CAESAR/ALDEBARAN Development Package), a toolbox dedicated to the design and verification of communication protocols and distributed systems. Besides the description of the new features, this paper also lists the latest applications of CADP to industrial case-studies and mentions the current research directions for improving CADP.
Compositional State Space Generation from Lotos Programs
This paper describes a compositional approach to gnerate the labeled transition system representing the behaviour of a Lotos program by repeatedly alternating composition and reduction operations on subsets of its processes. To restrict the size of the intermediate LTSs generated, we generalize to the LOTOS parallel composition operator the results proposed in [Graf-Steffen-90], which consist in representing the environment of a process as an interface, i.e., a set of "autorized" execution sequences/ This generalization allows to handle both user-given interfaces and automatically computed ones. This compositional method has been implemented within the CADP toolbox and experimented on several realistic case studies.
Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus ("FireWire"): an Experiment with E-LOTOS
[37 pages, PostScript form only]
This paper deals with the description in E-LOTOS of the asynchronous Link layer protocol of the IEEE-1394 Standard and its verification using model-checking. The E-LOTOS descriptions are based on both the standard and the mu-CRL description written by Luttik. The verifications are performed using the CADP (CAESAR/ALDEBARAN) toolbox. We translate the E-LOTOS descriptions in LOTOS using the TRAIAN tool, and then we generate the underlying LTS models using the CAESAR compiler. We formally express in the ACTL temporal logic the five correctness properties of the Link layer protocol stated by Luttik in natural language and we verify them on the LTS models using the XTL model-checker. We detect and correct a potential deadlock caused by the ambiguous semantics of the state machines given in the standard, which can be misleading for implementors of the IEEE-1394 protocol.
At this site, you will find two helpful ressources:
He would appreciate receiving URLs from any research groups (preferably) or individuals with pages mentioning LOTOS activities.
In order to provide a better support to our many users, we would like to know on what machines you would like to use the CADP toolbox. This information will guide us, in our choices in the porting of CADP on other platforms. This questionnaire concerns registered users as well as people who would like to use the toolbox.
On which configuration(s) would you need to use CADP ? (Please, do not list all the kinds of machines your organization has bought, but only the type of machines on which you would really like to use the CADP tools). . Sun / Solaris 2.5 [Y / N] . Sun / SunOS 4.1.x [Y / N] . Sun / Linux [Y / N] . SGI / Irix [Y / N] . HP / HP-UX [Y / N] . Alpha / OSF/1 [Y / N] . IBM / AIX *.* [Y / N] . PC / ELF versions of Linux [Y / N] . PC / a.out versions of Linux [Y / N] . PC / Windows 95 [Y / N] . PC / Windows NT 4.0 [Y / N] . Other please precise If you use CADP on a Sun workstation running SunOs 4.1.x, how long do you plan to do so ? Do you plan to migrate to Solaris in the near future ? Would you mind if we discontinue the support of SunOS 4.1.x ?Please send your replies to Mark.Jorgensen@inria.fr. We appreciate your help.
Number: 422 Date: Mon Dec 16 16:03:51 MET 1996 Author: Laurent Mounier (VERIMAG) Files: bin.*/projector.a Nature: The libraries of the Projector tool did not work properly and have been updated.
Number: 423 Date: Mon Dec 16 18:23:09 MET 1996 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/xsimulator.a Nature: A minor bug fix was made in the Xsimulator tool.
Number: 424 Date: Sun Dec 22 20:57:27 MET 1996 Report: Guy Tremblay (Universite du Quebec a Montreal), J. Sincennes (University of Ottawa) Author: Hubert Garavel (INRIA/VASY) Files: INSTALLATION Nature: In the INSTALLATION file, the $ARCH variable was renamed in $CADP_ARCH, in order to avoid conflicts with some $ARCH variable which may also exist in some startup shells. This change is intended to new users only; if you are currently using $ARCH, you do not have to modify your startup file. Explanations regarding the difference between architectures "sun4" and "sun5" have been added.
Number: 425 Date: Mon Jan 6 17:09:45 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar.adt Nature: A minor bug was fixed in CAESAR.ADT. In the ``.h'' file generated by CAESAR.ADT, when a ``.t'' file (external types) is to be included, the comments describing the expected contents of the ``.t'' file were disseminated at various places in the ``.h'' file. Now, they are gathered altogether at the place where the ``.t'' file is included.
Number: 426 Date: Wed Jan 8 14:27:23 MET 1997 Report: Ghassan Chehaibar (Bull/Dyade) Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar.adt, man/manl/caesar.adt.l Nature: A new option, ``-external'', was added to CAESAR.ADT. When invoked with this option, CAESAR.ADT generates two prototype files, which can be used as a model for the ``.t'' file (external types) and the ``.f'' file (external functions). These files are to be completed by hand. The CAESAR.ADT manual page was updated accordingly.
Number: 427 Date: Wed Jan 29 14:42:28 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: ./INSTALLATION Nature: The installation directive: chown -R root $CADP chgrp -R wheel $CADP did not work under Solaris 2 (the "wheel" group only exists in Solaris 1). They have been replaced with: chown -R 0 $CADP chgrp -R 0 $CADP This should work both under Solaris 1 and 2.
Number: 428 Date: Fri Jan 31 11:42:55 MET 1997 Report: Charles Pecheur (INRIA/VASY) Author: Hubert garavel (INRIA/VASY) Files: bin.*/bcg_io Nature: The BCG_IO tool did not work properly under some restricted versions of Solaris 2.5 (limited to dynamic libraries). When invoked with some specific options, error messages were displayed, e.g.: > bcg_io TEST.bcg TEST.aut > ld: fatal: library -lc: not found > ld: fatal: File processing errors. No output written to ... > Segmentation Fault (core dumped) This problem also occurred in ALDEBARAN, which silently invokes BCG_IO to perform format conversions: > aldebaran -bddsize 4 -info foo.bcg > ld: fatal: library -lsocket: not found > ld: fatal: library -lnsl: not found > ld: fatal: library -lelf: not found > ld: fatal: library -lc: not found > ld: fatal: File processing errors. No output written to ... > Segmentation Fault - core dumped This problem was fixed.
Number: 429 Date: Thu Feb 6 08:41 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: ./INSTALLATION Nature: The installation directive for setting $LD_LIBRARY_PATH worked for "csh", but not "tcsh". The new directive should work for both "csh" and "tcsh". Also, "/usr/lib" was added to the list of directories that we recommend to be present in $LD_LIBRARY_PATH.
Number: 430 Date: Thu Feb 6 14:53:03 MET 1997 Authors: Mark Jorgensen (INRIA/VASY), Laurent Mounier (VERIMAG) Files: doc/:READ_ME Nature: The :READ_ME file has been enriched with the abstracts of the papers. An HTML version is now available on the CADP web site.
Number: 431 Date: Mon Feb 10 17:10:11 MET 1997 Author: Mark Jorgensen (INRIA/VASY) Files: com/xeuca, src/eucalyptus/eucalyptus.tcl Nature: The EUCALYPTUS graphical user-interface was improved in two ways: appropriate fonts are specified explicitly (this avoids random font replacements on some X-terminals) and colors have been added. Both fonts and colors can be customized by the user using the ~/.xeucarc file.
Number: 432 Date: Mon Feb 17 09:37:21 MET 1997 Authors: Hubert Garavel, Radu Mateescu, Mihaela Sighireanu (INRIA/VASY) Files: lib/INTEGERNUMBER.lib, lib/INTEGER.lib, lib/X_INTEGER.lib, incl/X_INTEGER.h Nature: A new datatype library has been developed, which models signed integer numbers. This library is available under two different forms: - ``INTEGERNUMBER.lib'' (also ``INTEGER.lib'' as a shorthand) contains ``pure'' abstract data type definitions for integer numbers. It can be compiled by CAESAR.ADT - ``X_INTEGER.lib'' contains data type definitions, for which all types and functions are declared to be external. The corresponding C implementation is provided in file incl/X_INTEGER.lib
Number: 433 Date: Mon Feb 17 11:51:36 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: com/caesar.aldebaran Nature: The previous version of "caesar.aldebaran" relied upon the the "-n" option of the "echo" command, an option which no longer exists in Solaris 2.*. This has been fixed.
Number: 434 Date: Mon Feb 17 12:14:21 MET 1997 Report: Jacques Sincennes (University of Ottawa) Author: Hubert Garavel (INRIA/VASY) Files: com/tst Nature: The warning message given by "tst" when "/bin/arch" overrides "$CADP/com/arch" in the $PATH has been suppressed (more precisely, it has been extremely softened), because this situation does not create problems. Also, the new version of "tst" checks for the availability of UNIX command "head" and "tail".
Number: 435 Date: Mon Feb 17 15:53:15 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: com/upc Nature: The "upc" program was modified to take into account the new form of CADP version names (97a, etc., after A, B, ...Z). Also, an "echo -n" statement was made portable across different Unix versions.
Number: 436 Date: Thu Feb 20 19:02:15 MET 1997 Author: Mihaela Sighireanu (INRIA/VASY) Files: emacs/lotos-mode.el Nature: A "LOTOS-mode" for editing LOTOS descriptions using Emacs and XEmacs has been added to the CADP release. This mode allows keywords and comments to be displayed in different fonts/colors. It also provides shorthands for entering quickly LOTOS constructs (types, processes, ...) and supports compiler invocation within Emacs and XEmacs.
Number: 437 Date: Tue Feb 25 15:27:14 MET 1997 Report: Charles Pecheur (INRIA/VASY) Author: Mark Jorgensen (INRIA/VASY) Files: src/eucalyptus/eucalyptus.tcl Nature: In EUCALYPTUS, ELUDO was not launched properly if the option "Use_Non_Standard_Library" had been selected before clicking on "Execute / Symbolic simulation". For instance, if the "is.x" library had been selected, ELUDO tried to fetch library "is.x.x". This has been fixed.
Number: 438 Date: Thu Feb 27 14:48:07 MET 1997 Author: Laurent Mounier (VERIMAG) Files: demos/demo_18 Nature: A new demo (the Transit Node message router used in the European project SPECS) was added to the CADP distribution,
Number: 439 Date: Tue Mar 4 13:09:26 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar, incl/caesar_kernel.h, src/exec_caesar/main.c man/manl/caesar.l Nature: A new option ("-exec") has been added to CAESAR. In addition to the two existing modes for CAESAR: graph generation ("-bcg", "-aldebaran", "-graph") and on-the-fly exploration ("-open"), this option introduces a third mode: the execution mode. Using this option, CAESAR produces an executable C module, which can be used to control a real "reactive" system. This code has to be completed with hand-written C routines corresponding to the observable gates of the LOTOS description. The interface of the C code generated with "-exec" is defined in "$CADP/incl/caesar_kernel.h" and a typical main routine is available in "$CADP/src/exec_caesar/main.c". For an example, see #461 below.
Number: 440 Date: Mon Mar 10 15:39:46 MET 1997 Report: Charles Pecheur (INRIA/VASY), Arnaud Fevrier (ENST), Elie Najm (ENST) Author: Mark Jorgensen and Hubert Garavel (INRIA/VASY) Files: src/eucalyptus/eucalyptus.tcl, src/eucalyptus/xeucarc_standard Nature: Several fixes and improvements have been done in EUCALYPTUS: (a) The size of xterm's created from "xeuca" is now parameterized by a $Xterm_Options variable defined in the .xeucarc file. This variable can also be used to pass various options to xterm. (b) An error message is now displayed when one tries to launch the Viscope tool, if it is not installed (c) In the Files / Change Directory menu, the buttons corresponding to the directories of non-installed tools are now made inactive (in grey). (d) In the Applications menu, there is now a single editor button, corresponding to the $EDITOR variable (e) "xeuca" no longer creates an xterm window when launching editors such as emacs, xemacs, textedit, etc. that have their own xterm window. On the opposite, an xterm is still created for "vi". (f) The names of the temporary files created by "xeuca" have been made unique, in order to avoid conflicts between concurrent or successive "xeuca" sessions. (g) "xeuca" now detects the backup files (foo~ and #foo#) created by emacs and xemacs and gives them a grey icon. (h) When the "Help" button is pressed and the Help window is already opended, the Help window is popped up.
Number: 441 Date: Mon Mar 10 18:40:45 MET 1997 Report: Arnaud Fevrier (ENST) Author: Hubert Garavel (INRIA/VASY) Files: INSTALLATION Nature: Various setup details listed in the INSTALLATION file have been improved: (a) For the C-shell, a test was added to detect whether the $LD_LIBRARY_PATH is set or not. (b) The $EDITOR variable is not overriden if previously defined. (c) The $NAVIGATOR variable is not overriden if previously defined. (d) An attempt is made to position CADP_CC automatically (either to "cc" or "gcc" depending upon the context).
Number: 442 Date: Tue Mar 11 12:12:34 MET 1997 Report: Mihaela Sighireanu (INRIA/VASY) Author: Hubert Garavel (INRIA/VASY) Files: com/tst Nature: Two bugs that caused "tst" to halt abruptly when $CADP_CC was set to "cc -g" have been fixed. Also, the new version of "tst" detects properly the situations where $CADP is set to a dummy value.
Number: 443 Date: Fri Mar 14 16:46:27 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar, bin.*/caesar.adt, man/manl/caesar.l, man/manl/caesar.adt.l, src/eucalyptus Nature: The two options "-berkeley" and "-systemV" were no longer meaningful in 1997. They have been removed from CAESAR, CAESAR.ADT and EUCALYPTUS. The manual pages have been updated.
Number: 444 Date: Mon Mar 17 10:19:12 MET 1997 Report: Axel Belinfante (Univ. of Twente), Ghassan Chehaibar (Bull/Dyade) Mark Jorgensen (INRIA/VASY) Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar, man/manl/caesar.l Nature: The tenporary files generated by CAESAR during its type survey phase, its optimization phase (optimizations E7, V3, V4, V7) and its simulation phase are now created in the $CADP_TMP directory (instead of the current directory). The manual page for CAESAR has been updated. In particular, this solves a problem reported by several OPEN/CAESAR users: > caesar.open: using link mode > caesar.open: file ``xxx.c'' was not generated using > ``caesar -open'' This problem happened when CAESAR stopped (due to an error in hand-written C code for data types) leaving a temporary ".c" file in the current directory. This ".c" file had to be deleted manually before restarting "caesar.open". The problem came from the fact that the temporary ".c" files and the final output ".c" file generated by "caesar -open" shared the same file name.
Number: 445 Date: Mon Mar 17 10:19:12 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar.adt, man/manl/caesar.adt.l Nature: Similarly, the temporary files produced by CAESAR.ADT during its external type survey phase are now created in the $CADP_TMP directory (instead of the current directory). The "..c" files have been renamed in ".c" files. The manual page for CAESAR.ADT has been updated.
Number: 446 Date: Mon Mar 17 11:23:34 MET 1997 Report: Charles Pecheur (INRIA/VASY) Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar, bin.*/caesar.adt Nature: The following diagnostic message produced by CAESAR and CAESAR.ADT: > the body of process P  has functionality: > F1 > whereas its declaration requires functionality: > F2 was not correct (functionnalities F1 and F2 had to be permuted). This problem is fixed now.
Number: 447 Date: Mon Mar 17 15:57:15 MET 1997 Report: Charles Pecheur (INRIA/VASY), Muffy Thomas (Univ. of Glasgow) Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar Nature: A warning message of the form: > "xx.c", line 498: warning: improper pointer/integer > combination: op "=" that occurred when invoking CAESAR on a Solaris 2.x with $CADP_CC pointing to /usr/ucb/cc has been fixed (the problem comes from the fact that function tmpfile() is not declared in /usr/ucbinclude/stdio.h)
Number: 448 Date: Mon Mar 17 17:54:34 MET 1997 Report: Charles Pecheur and Mihaela Sighireanu (INRIA/VASY) Author: Hubert Garavel (INRIA/VASY) Files: bin.*/exhibitor.a Nature: A bug in "exhibitor -dfs" was fixed, which caused Exhibitor to stop with the following error message: > ./exhibitor: assertion violation at line 65 of > file "exhibitor_dfs.c"
Number: 449 Date: Wed Mar 19 15:46:37 MET 1997 Files: bin.*/evaluator.a, man/manl/evaluator.l Author: Marius Bozga (VERIMAG) Nature: A new version of EVALUATOR was issued, improving the previous version on several points: - The data structures used to store the product states has been improved. The physical memory needed during the evaluation is reduced up to 40% for large examples. - Two different evaluation strategies are now available: a local one, which is an improvement of the strategy implemented in the previous version, and a global one, based on a single exploration of the whole product graph. The former is particularly efficient when the formula under evaluation is false (and it provides a diagnostic), while the latter usually offers better results when the formula is true (depending on the structure of the LTS). - The syntax of mu-calculus formulas has been extended: label sets can now be specified using boolean "not" and "or" operations on labels. The EVALUATOR manual page has been updated.
Number: 450 Date: Wed Mar 19 16:34:21 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar, com/caesar.open, com/caesar.xesar, src/eucalyptus, man/manl/caesar Nature: Seven command-line options have been removed from CAESAR: -auto, -mec, -pipn, -scan, -squiggles, -xesar and -xesar.old because they were no longer useful (either corresponding tools are no longer maintained, or in the particular case of Auto/Autograph, a new graph format (FC2) is in use). This removal simplifies the code of CAESAR (which becomes 660-lines leaner), the documentation and the graphical user-interface. If needed, the corresponding graph formats (.auto.pro, .dp3, .ge3, .gra, .graph, .m0, .mec, .scan and .tai) can still be obtained by generating a BCG file first, then converting it to the desired graph format using "bcg_io". Of course, the following options are still supported: -aldebaran, -bcg, -graph, -exec and -open The manual page for CAESAR was updated. The EUCALYPTUS graphical user-interface was updated. The "caesar.xesar" shell-script (lasting from November 1994) has been removed since it was no longer useful. The "caesar.open" shell was updated.
Number: 451 Date: Wed Mar 19 17:10:55 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: man/whatis, man/windex Nature: The index files for the CADP manual pages (named "whatis" for "sun4" and "windex" for "sun5") are generated. This should allow "man -k" to work properly.
Number: 452 Date: Fri Mar 21 11:47:51 MET 1997 Report: Mihaela Sighireanu (INRIA/VASY) Author: Hubert Garavel (INRIA/VASY) Files: gc/* Nature: The Boehm-Demers garbage collector has been upgraded. The previous version (V4.3 dated December, 23, 1994) has been replaced with the latest version available (V4.10 dated February, 19, 1996).
Number: 453 Date: Thu Mar 21 14:37:31 MET 1997 Report: Antony de Jacquier (Universite Libre de Bruxelles) Authors: Alain Kerbrat and Laurent Mounier (VERIMAG) Files: bin.*/aldebaran Nature: The default suffixes for filenames given in the command line of ALDEBARAN or in a composition expression have been modified. From now on, ALDEBARAN first looks for a ".aut" file, then for a ".bcg" file, and finally for a ".exp" file. Thus, it becomes possible to use an LTS stored in a "foo.aut" file within the "foo.exp" composition expression.
Number: 454 Date: Fri Mar 21 15:09:34 MET 1997 Report: Charles Pecheur (INRIA/VASY) Authors: Mark Jorgensen and Hubert Garavel (INRIA/VASY) Files: bin.*/duplex Nature: Two problems have been fixed: - No error message was displayed when Xsimulator could not be started (due to a missing X font, or to an "xhost -" setup, or to some other initialization reason). - Same problem for "xeuca" (the EUCALYPTUS graphical user interface)
Number: 455 Date: Fri Mar 22 10:23:14 MET 1997 Report: Hubert Garavel Author: Alain Kerbrat and Laurent Mounier (VERIMAG) Files: bin.*/aldebaran Nature: A warning has been suppressed in ALDEBARAN: it improperly complained when an LTS stored in "a .aut" file contained a single state and no transition.
Number: 456 Date: Mon Mar 24 15:54:57 MET 1997 Report: Charles Pecheur (INRIA/VASY) Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY) Files: src/open_caesar/simulator.i Nature: The simulation code (common to "simulator" and "xsimulator") has been extended to catch the situation where an error occurs during the evaluation of an ADT expression, which usually results in the following error message: #212 error in file ``.h'' : unexpected case (not defined by the equations) in operation F [...] implemented by function CAESAR_ADT_FUNC_F [...] In the previous version, "simulator" would immediately exit in such case. The situation was even worse with "xsimulator", that would exit and destroy its window before the above error message could be read. The new versions of "simulator" and "xsimulator" gracefully recover from this situation, allowing the user to backtrack to previous states or from the initial state.
Number: 457 Date: Mon Mar 24 18:10:09 MET 1997 Report: Charles Pecheur (INRIA/VASY) Authors: Mark Jorgensen and Hubert Garavel (INRIA/VASY) Files: bin.*/duplex Nature: The following problem was fixed: "xsimulator" was blocked when too many (i.e., several hundreds) transitions were fired from the current state. The new version recovers from this situation by giving an error message and printing only the first hundreds of transitions (skipping the remaining ones).
Number: 458 Date: Tue Mar 25 12:38:38 MET 1997 Report: Charles Pecheur (INRIA/VASY) Author: Hubert Garavel (INRIA/VASY) Files: src/eucalyptus/eucalyptus.tcl Nature: In some cases (when an option such as -first, -all, etc. was specified), the "terminator" tool was invoked incorrectly from the EUCALYPTUS user-interface (i.e., the option was specified twice). This bug has been solved.
Number: 459 Date: Tue Mar 25 12:46:19 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: src/eucalyptus/eucalyptus.tcl Nature: The "Files" and "Applications" menus of EUCALYPTUS have been renamed and reorganized into two menus ("File" and "View"), which are more logical and closer to standard conventions.
Number: 460 Date: Tue Mar 25 14:23:06 MET 1997 Report: Ilona Schubert (GMD-FOKUS, Germany) Author: Hubert Garavel (INRIA/VASY) Files: com/rfl Nature: A test was added to "rfl" to detect the cases where the startup file of the login shell (e.g. ".cshrc" or ".profile") does "echo" statements on its standard output. This prevents "rsh" (and consequently "rfl") from working properly.
Number: 461 Date: Tue Mar 25 17:20:39 MET 1997 Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY) Files: demos/demo_19 Nature: A new demo (the famous "Production Cell" and its animated Tcl/Tk interface) was added to the CADP release. It demonstrates how LOTOS and EXEC/CAESAR can be used to program controllers.
Number: 462 Date: Tue Mar 25 18:10:35 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: src/eucalyptus/eucalyptus.tcl Nature: A bug was fixed in EUCALYPTUS: the "Edit in 2 dimensions" button for PostScript files invoked an improper command.
Number: 463 Date: Wed Mar 26 11:24:54 MET 1997 Report: Marius Bozga and Laurent Mounier (VERIMAG) Author: Hubert Garavel (INRIA/VASY) Files: bin.*/libbcg_open.a Nature: The implementation of CAESAR_STRING_LABEL() provided by BCG_OPEN was inefficient, because each call to this function allocated a fragment of memory that could never be freed (according to the conventions defined in "caesar_graph.h"). This bug has been fixed.
Number: 464 Date: Wed Mar 26 11:59:36 MET 1997 Author: Laurent Mounier (VERIMAG) Files: doc/Krimm-Mounier-97.dvi, doc/Krimm-Mounier-97.ps, doc/biblio.bib Nature: A new paper on compositional verification was added in the "doc" directory.
Number: 465 Date: Wed Mar 26 18:21:09 MET 1997 Author: Hubert Garavel (INRIA/VASY) Files: src/eucalyptus/eucalyptus.tcl Nature: The EUCALYPTUS graphical-user interface has been extended to support the new version of evaluator (see #449 above).
Number: 466 Date: Thu Mar 27 11:11:04 MET 1997 Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY) Files: bin.*/caesar, bin.*/lib_BCG_IO.a, incl/bcg_write.h src/open_caesar/generator.c, src/open_caesar/reductor.c, src/eucalyptus/eucalyptus.tcl, src/monitor/main.tcl, com/caesar.open, man/manl/caesar.l, man/manl/generator.l, man/manl/reductor.l, man/manl/bcg_write.l Nature: A new functionality has been added to the BCG library: it is now possible to monitor in real-time the generation of a BCG graph: this is done using a Tcl-Tk window, which displays the current number of states, the current number of transitions, the list of labels, etc. (see below improvement #468 for details on how this functionality can be accessed from a C program). An option "-monitor" has been added to CAESAR, Generator and Reductor: when invoked, this option launches the Tcl-Tk monitor window. Note: the "-monitor" option is CPU-consuming, but not much memory-expensive (since a "pipe" is used for interprocess communication). The EUCALYPTUS user-interface and the corresponding manual pages have been updated to integrate this new functionality.
Number: 467 Date: Thu Mar 27 12:32:00 MET 1997 Author: Laurent Mounier (VERIMAG) Files: demos/demo_20 Nature: A new demo about the DES2AUT, PROJECTOR and EVALUATOR tools (compositional verification of the rel/REL protocol with 4 stations) has been added.
Number: 468 Date: Tue Apr 1 16:56:13 MET DST 1997 Author: Hubert Garavel (INRIA/VASY) Files: incl/bcg_io_write_bcg.h, bin.*/libBCG_IO.a, bin.*/caesar, src/open_caesar/generator.c, src/open_caesar/reductor.c, com/upc, man/manl/bcg_write.l Nature: The C programmation interface for generating BCG files has been simplified and enhanced. The main change affects the list of the parameters for functions BCG_IO_WRITE_BCG_BEGIN() and BCG_IO_WRITE_BCG_END(). The meaning of the new parameters is described in the "bcg_write.l" manual page. To take advantage of the new "bcg_io_write_bcg.h" interface and the new "libBCG_IO.a" library, adaptations of the existing programs are necessary. The pre-existing calls: BCG_IO_WRITE_BCG_BEGIN (<filename>, <code>, <comment string>); ... BCG_IO_WRITE_BCG_END (<nb_states>, <initial state>, <nb edges>, <sort>); should be replaced with the following ones: BCG_IO_WRITE_BCG_BEGIN (<filename>, <initial state>, <code'>, <comment string>, <monitor>); ... BCG_IO_WRITE_BCG_END (); where: - <filename> and <comment string> should be kept unchanged. - <initial state> should be moved from one function to the other. - <nb states> and <nb edges> should be removed: these two values are now handled automatically by the BCG library. This will prevent application programs from generating inconsistent BCG files by supplying erroneous numbers of states and edges. Application programs no longer need to compute <nb states> and <nb edges> themselves. - <code'> should be equal to 1 or 2 (see the manual page). - <sort> should be removed (it is no longer useful). - <monitor> is a boolean that indicates whether the Tcl-Tk monitoring window should be started. CAESAR, Generator, Reductor, and the "upc" shell-script have been updated accordingly.
Number: 469 Date: Tue Apr 1 18:04:42 MET DST 1997 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/bcg_io Nature: In version Z, the format of the ".aut" files generated by ALDEBARAN had been modified unilaterally. Before version Z, the edges in ".aut" files generated by ALDEBARAN were always sorted by increasing number of the "from-states". Since version Z, some options of ALDEBARAN produce ".aut" files that are not sorted, e.g.: des (0, 6, 7) (0, F, 6) (4, E, 5) (0, C, 3) (1, B, 2) (3, D, 4) (0, A, 1) This situation causes problems in various places. In particular BCG_IO could not deal with non-sorted ".aut" files, which led to the following error message: bcg_edge: previous state are not increasing in BCG_WRITE_EDGE The new version of BCG has been modified to tackle non-sorted ".aut" files. However, the BCG files now produced from ".aut" files are now less compact than before (technically, their edge area is encoded with format 1 instead of format 2). Therefore, the recommended policy is to use BCG files rather than ".aut" files. In particular, it is better to generate directly a BCG file from CAESAR, rather than generating a ".aut" file first and convert it later to a BCG file. Note: An unsorted ".aut" file can be sorted using the following command: bcg_io unsorted.aut sorted.aut
Number: 470 Date: Tue Apr 1 18:34:23 MET DST 1997 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/bcg_io Nature: The previous version of the BCG_IO tool did not parse the simple SEQUENCE format correctly: for instance, lines starting with a letter were rejected, whereas they should be ignored silently. This problem is now solved.
Number: 471 Date: Wed Apr 2 09:48:25 MET DST 1997 Report: Radu Mateescu and Mihaela Sighireanu (INRIA/VASY) Author: Hubert Garavel (INRIA/VASY) Files: bin.*/libBCG_IO.a, bin.*/caesar src/open_caesar/generator.c, src/open_caesar/reductor.c Nature: CAESAR, Generator and Reductor have been modified to close properly the BCG file being generated when an interrupt signal is received, or when the "stop" button of the BCG monitor is pressed. This will prevent from having incomplete (therefore inconsistent) BCG files left in the working directory.
Number: 472 Date: Wed Apr 2 16:14:40 MET DST 1997 Report: Ghassan Chehaibar (Bull/Dyade) Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar Nature: The ".aut" file generated by CAESAR was left in an inconsistent state upon receipt of an interrupt signal. This problem is now solved.
Number: 473 Date: Wed Apr 2 16:25:04 MET DST 1997 Report: Radu Mateescu and Mihaela Sighireanu (INRIA/VASY) Author: Hubert Garavel (INRIA/VASY) Files: bin.*/caesar, man/manl/caesar.l Nature: Previously, the ".net" file was generated either if the "-network" was given on the command-line, or if none of the following primitives was selected: "-bcg", "-aldebaran", "-open", "-exec". This behaviour was felt to be confusing, although it was justified by "historical" considerations. The new behaviour is simpler: the ".net" is generated iff the "-network" option is given on the command-line. ------------------------------------------------------------------------------- BUG FIX Number: 474 Date: Mon Apr 7 19:23:35 MET DST 1997 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/*bcg*, bin.*/*BCG* Nature: The "-Bstatic" option is no longer supplied by the BCG tools and libraries when they invoke the C compiler. This removes a compiler warning occurring when "gcc" is used instead of "cc": gcc: file path prefix `static' never used
Number: 475 Date: Thu Apr 17 12:45:07 MET DST 1997 Report: Charles Pecheur (INRIA/VASY) Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY) Files: incl/caesar_hash.h Nature: Due to an error in a #define statement, the two hash-functions: CAESAR_STATE_1_HASH() and CAESAR_STATE_2_HASH() used by Terminator were in fact identical, which limited the scope of deadlock search. This bug was fixed.
Number: 476 Date: Thu Apr 17 15:45:23 MET DST 1997 Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY) Files: bin.*/libcaesar.a, incl/caesar_hash.h, man/manl/caesar_hash.l doc/Garavel-92-a.ps Nature: The CAESAR_0_HASH() function of the OPEN/CAESAR library was replaced by a faster hash function (the algorithms are totally different and the hash values returned are also different). The previous hash function is still available, but with different names: CAESAR_3_HASH() and CAESAR_STATE_3_HASH().
Number: 477 Date: Wed Apr 23 12:47:52 MET DST 1997 Report: Ghassan Chehaibar (Bull/Dyade) Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY) Files: bin.*/caesar Nature: The C code generated by CAESAR has been carefully examined and improved in order to increase its execution speed. Ten optimizing transformations have been applied, leading to a considerable reduction of the time needed to fire the transitions (this time has been roughly divided by 9!). In addition to this, the size of the state hash table has been enlarged (from 8,329 entries to 131,071 entries). From now on, the user can control this value, which is controlled by a pre-processor directive of the form: #define CAESAR_STATE_HASH_SIZE ... Similarly, the user gets control over the size of the position hash table, using the following firective: #define CAESAR_POSITION_HASH_SIZE ... The combination of these changes leads to a much faster version of CAESAR. Depending on the examples, the new version of CAESAR can be from 2 times to 160 times faster, as shown in the table below (all these data have been obtained on an Ultra-Sparc-1 143 MHz with 256 Mbytes of RAM): EXAMPLE CAESAR 5.1 CAESAR 5.2 speedup CO4 (Ch. Pecheur) 6 min. 2 min. 40 sec. 2.3 demo_17/EXPERIMENT_14.lotos 3 min. 13 sec. 1 min. 03 sec. 3 demo_08/rel_rel.lotos 58 min. 24 sec. 9 min. 43 sec. 6 demo_11/rel_rel.lotos 1 hour 52 min. 12 min. 59 sec. 8.6 demo_07/overtaking.lotos 3 min. 11 sec. 20 sec. 9.6 demo_17/EXPERIMENT_12.lotos 40 min. 20 sec. 2 min. 45 sec. 15 demo_14/pots.lotos 13 min. 37 sec. 54 sec. 15 demo_17/EXPERIMENT_11.lotos 8 hours 17 min. 12 min. 40 sec. 39 demo_16/brp_protocol.lotos 7 min. 55 sec. 6 sec. 79 IEEE 1394 (M. Sighireanu) 83 hours 29 min. 55 min. 30 sec. 90 demo_18/transit_node.lotos 46 hours 8 min. 17 min. 10 sec. 161
Number: 478 Date: Wed Apr 23 15:49:42 MET DST 1997 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/libcaesar.a Nature: Some of the optimizations made for CAESAR (see #477 above) have been also applied to the OPEN/CAESAR library.
Number: 479 Date: Fri Apr 25 11:56:49 MET DST 1997 Author: Radu Mateescu (INRIA/VASY) Files: demos/demo_01, demos/demo_02 Nature: These two demo examples have been enhanced with examples of correctness properties written in mu-calculus and verified using Evaluator.
Number: 480 Date: Thu May 2 13:14:40 MET DST 1997 Report: Michael Kishinevsky (University of Aizu) Author: Hubert Garavel (INRIA/VASY) Files: com/rfl Nature: The "rfl" command has been made more robust, in order to work even if the user-specific startup files (.cshrc, .profile, etc.) do not include "/usr/ucb/bin" in the $PATH variable. The new "rfl" command makes less assumptions about user- specific configuration.
Number: 481 Date: Tue May 6 10:50:33 MET DST 1997 Report: Laurent Mounier (VERIMAG), Charles Pecheur (INRIA/VASY) Author: Mark Jorgensen (INRIA/VASY) Files: src/eucalyptus/eucalyptus.tcl Nature: Two bug fixes in the EUCALYPTUS Graphical User-Interface: - Under some circumstances, the "OK" buttons of the ALDEBARAN comparison window, the Evaluator window, etc. could be enabled even if no automaton file or mu-calculus file had been selected previously. They are now always disabled until a proper selection takes place. - In some cases, the "Kill" button refused to work, by displaying messages of the form "It is too late to kill the process" or "There is no process to kill". These messages are no loger displayed: instead a window is opened, in which the user can select one or several processes to kill.
Number: 482 Date: Fri May 23 12:11:54 MET DST 1997 Report: Charles Pecheur (INRIA/VASY) Author: Hubert Garavel (INRIA/VASY) Files: com/tst Nature: The "tst" command has been modified to produce warnings under Solaris 2.* when - "/usr/ucb/cc" is used as the C compiler (in place of "/opt/SUNWspro/bin/cc") - "/usr/ucb/ld" is used as the link editor (in place of "/opt/SUNWspro/bin/ld") because we noticed that the use of "/usr/ucb/cc" would make Xsimulator to core dump.
Number: 483 Date: Mon May 26 18:22:32 MET DST 1997 Author: Hubert Garavel (INRIA/VASY) Files: doc Nature: Two new papers have been added to the CADP release - Garavel-Jorgensen-et-al-97.ps - Sighireanu-Mateescu-97.ps
VERSION 97a "Twente"