|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
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.
Garavel-Jorgensen-Mateescu-Pecheur-Sighireanu-Vivien-97
CADP'97 - Status, Applications, and Perspectives
[6 pages]
Abstract:
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.
Krimm-Mounier-97
Compositional State Space Generation from Lotos Programs
[20 pages]
Abstract:
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.
Sighireanu-Mateescu-97
Validation of the Link Layer Protocol of the IEEE-1394
Serial Bus ("FireWire"): an Experiment with E-LOTOS
[37 pages, PostScript form only]
Abstract:
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 [9] 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"
Back to the CADP Home Page