|
| 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 |
| CADP Resources |
|
VLPN Benchmarks
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.
We are pleased to announce the availability of the latest version of CADP. This version is named "Z" and is dated December, 6, 1996. You will find enclosed the information for downloading version Z of CADP using FTP.
As many of you have asked us for more information about CADP, this is a short report about past and current events:
We hope that you will enjoy this new version.
Fernandez-Garavel-Kerbrat-Mounier-Mateescu-Sighireanu-96: paper
describing the toolbox and its components, presented at
CAV'96. This paper completes the previous one and summarizes
the latest features of CADP at the time it was written.
[4 pages]
Garavel-96: paper describing the Eucalyptus toolset, which embodies
CADP and other LOTOS tools [PostScript form only]
[13 pages]
Abstract :
This article presents the essential features of a
protocol engineering environment, the EUCALYPTUS toolbox, which
has been developed or improved in the framework of two
successive European-Canadian projects EUCALYPTUS-1 and
EUCALYPTUS-2. This toolbox is based on the formal description
technique LOTOS standardized by ISO. It offers a wide range of
functionalities, including simulation, compilation,
verification and test case generation for LOTOS descriptions.
Chehaibar-Garavel-Mounier-Tawbi-Zulian-96: specification and
verification of the bus arbiter of Bull's Powerscale
architecture
[20 pages, PostScript form only]
Abstract :
This paper presents the results of an industrial
case-study concerning the use of formal methods for the
validation of hardware design. The case-study focuses on
PowerScale, a multiprocessor architecture based on PowerPC
micro-processors and used in Bull's Escala series of servers
and workstations (PowerScale and Escala are registered
trademarks of Bull. PowerPC is a registered trademark of the
International Business Machines Corporation).
The specification language LOTOS (ISO International
Standard 8807) was used to describe formally the main
components of this architecture (processors, memory controller
and bus arbiter).
Four correctness properties were identified, which
express the essential requirements for a proper functioning of
the arbitration algorithm, and formalized in terms of
bisimulation relations (modulo abstractions) between finite
labelled transition systems.
Using the compositional and on-the-fly model-checking
techniques implemented in the CADP (CAESAR/ALDEBARAN) toolbox,
the correctness of the arbitration algorithm was established
automatically in a few minutes
Mateescu-96: specification and validation of Philips' bounded
retransmission protocol
[31 pages, PostScript form only]
Abstract:
This paper reports about the formal specification and
verification of a Bounded Retransmission Protocol (Brp) used
by Philips in one of its products.
We started with the descriptions of the Brp service
(i.e., external behaviour) and protocol written in the muCRL
language by Groote and van de Pol. After translating them in
the Lotos language, we performed verifications by
model-checking using the Cadp (Caesar/Aldebaran) toolbox.
The models of the Lotos descriptions were generated
using the Caesar compiler (by putting bounds on the data
domains) and checked to be branching equivalent using
the Aldebaran tool.
Alternately, we formulated in the ACTL temporal logic
a set of safety and liveness properties for the Brp protocol
and checked them on the corresponding model using our Xtl
generic model-checker.
Garavel-Mounier-96: specification and verification of several
leader election algorithms
[35 pages, PostScript form only]
Abstract :
This report deals with the formal specification and
verification of distributed leader election algorithms for a
set of machines connected by a unidirectional ring network.
Starting from an algorithm proposed by Le Lann in 1977, and
its variant proposed by Chang and Roberts in 1979, we study
the robustness of this class of algorithms in presence of
unreliable communication medium and/or unreliable machines.
We suggest various improvements of these algorithms in order
to obtain a fully fault-tolerant protocol.
These algorithms are formally described using the ISO
specification language LOTOS and verified (for a fixed number
of machines) using the CADP (CAESAR/ALDEBARAN) toolbox.
Model-checking and bisimulation techniques allow the
verification of these non-trivial algorithms to be carried out
automatically.
Garavel-Sighireanu-96-a: On the introduction of exceptions in E-LOTOS
[16 pages, PostScript form only]
Abstract :
The advantages of exception handling are well-known and
several sequential or parallel programming languages provide
exception handling mechanisms. Unfortunately, none of the three
standardized Formal Description Techniques (ESTELLE, LOTOS, and
SDL) supports exceptions.
In 1992, Quemada and Azcorra pointed out the need for
structuring protocol descriptions with exceptions and proposed
to extend LOTOS with a so-called ``generalized termination and
enabling'' mechanism.
In this report, we show that their proposal is not
fully appropriate for a compositional description of complex
systems. We propose a simpler exception mechanism for LOTOS,
for which we provide a syntactic and semantic definition.
We show that this exception mechanism is very
primitive, as it allows several existing LOTOS operators to be
expressed as special cases. We also suggest additional
operators, such as symmetric sequential composition and
iteration, which can be derived from the exception mechanism.
Please, note that the CADP team is now located in two different buildings. Our new addresses, telephone numbers, fax numbers, and e-mail addresses are given below.
In spite of this geographical bi-localization, we expect to maintain and develop the CADP toolbox. To contact us using e-mail, you can use the common e-mail address: "caesar@imag.fr", which remains unchanged.
Address:
INRIA Rhone-Alpes / Dyade
655, avenue de l'Europe
F-38330 Montbonnot Saint-Martin
FRANCE
Tel: +(33) 4 76 61 52 00 <standard>
+(33) 4 76 61 52 02 Ghassan Chehaibar G.Chehaibar@dyade.fr
+(33) 4 76 61 52 24 Hubert Garavel Hubert.Garavel@inria.fr
+(33) 4 76 61 53 94 Mark Jorgensen Mark.Jorgensen@inria.fr
+(33) 4 76 61 52 83 Radu Mateescu Radu.Mateescu@inria.fr
+(33) 4 76 61 52 98 Charles Pecheur Charles.Pecheur@inria.fr
+(33) 4 76 61 52 89 Mihaela Sighireanu Mihaela.Sighireanu@inria.fr
+(33) 4 76 61 52 83 Bruno Vivien Bruno.Vivien@inria.fr
Fax: +(33) 4 76 61 52 52
Address:
VERIMAG
Centre Equation
2, avenue de Vignate
F-38610 Gieres
FRANCE
Tel: +(33) 4 76 63 48 48 <standard>
+(33) 4 76 63 48 52 Marius Bozga Marius.Bozga@imag.fr
+(33) 4 76 63 48 53 Jean-Claude Fernandez Jean-Claude.Fernandez@imag.fr
+(33) 4 76 63 48 59 Alain Kerbrat Alain.Kerbrat@imag.fr
+(33) 4 76 63 48 52 Laurent Mounier Laurent.Mounier@imag.fr
+(33) 4 76 63 48 51 Joseph Sifakis Joseph.Sifakis@imag.fr
Fax: +(33) 4 76 63 48 50
Number: 294
Date: Wed Jun 1 20:53:11 MET DST 1994
Files: bin.*/caesar, bin.*/caesar.adt
Nature: The "-more" option (needed for integrating CAESAR and
CAESAR.ADT into the EUCALYPTUS graphical user-interface) has
been added.
Number: 295
Date: Thu Jun 2 21:31:13 MET DST 1994
Files: com/caesar.open
Nature: The "caesar.open" program has been extended so as to accept
the "-cc" and "-more" options. A related bug was fixed.
Number: 296
Date: Wed Jun 8 18:31:33 MET DST 1994
Files: com/caesar.open, doc/Garavel-92-a.ps
Nature: The notion of "explicit include mode" has been suppressed.
From now on, there are only two modes available: "(implicit)
include mode" and "link mode". Several bugs related to the
(implicit) include mode have been fixed. The documentation
has been updated.
Number: 297
Date: Wed Jun 8 18:40:52 MET DST 1994
Files: com/caesar.open, man/caesar.open.l
Nature: The "caesar.open" program no longer attempts to guess
automatically whether link mode or include mode should be
used. This approach was not compatible with recent changes.
From now on, two options '-link' and '-include' are available
to select either link or include mode. By default, link mode
is selected. The manual page has been updated accordingly.
Number: 298
Date: Wed Jun 8 19:08:38 MET DST 1994
Files: incl/caesar_version.h, man/caesar_version.l,
doc/Garavel-92-a.ps, bin.*/libcaesar.a, bin.*/caesar, com/upc
Nature: The "caesar_version" library of OPEN/CAESAR has been modified
so that the OPEN/CAESAR environment can be used with other
languages/tools than LOTOS/CAESAR.
The "caesar_version" library no longer checks that the version
of CAESAR which generated the "spec.c" program is up to date.
On the opposite, the "spec.c" program generated by CAESAR
(or by another tool) will check that the "caesar_version"
library is up to date. Therefore, the "caesar_version" library
is now independent from the CAESAR tool.
Changes: function CAESAR_GRAPH_VERSION() was moved to file
"caesar_graph.h"; two parameters have been added to function
CAESAR_CHECK_VERSION(); the semantics of CAESAR_MATCH_VERSION()
has changed. The "upc" conversion program has been modified
so as to flag these changes.
Consequences: these modifications should be transparent to all
user programs, unless they use the "caesar_version" library.
But the tools that generate the "spec.c" program have to be
adapted, especially the invocation of CAESAR_CHECK_VERSION()
in CAESAR_INIT_GRAPH(). The CAESAR compiler has been modified
accordingly.
Number: 299
Date: Wed Jun 8 20:19:17 MET DST 1994
Files: bin.{sun3,sun4}/caesar, bin.{sun3,sun4}/libcaesar.a,
incl/caesar_*.h, man/caesar_*.l, doc/Garavel-92-a.ps,
src, src/open_caesar/*.c, com/caesar.open, com/upc
Report: Renaud Ruffiot (VERIMAG)
Nature: The OPEN/CAESAR programming interfaces have been modified in
order to be independent from LOTOS. All "hidden" dependencies
(implementation details related to LOTOS) have been removed so
as to allow other languages/compilers than LOTOS/CAESAR to be
connected to OPEN/CAESAR.
The main changes mostly affect "caesar_graph.h". They are
described below:
(1) From now on, the C code generated by CAESAR with "-open"
option #defines the macro CAESAR_IMPLEMENTATION_GRAPH
and includes the file "caesar_graph.h" (thus transitively
including "caesar_standard.h" and "caesar_version.h").
(2) The two functions CAESAR_GRAPH_COMPILER() and
CAESAR_VERSION_COMPILER() have been added to
"caesar_graph.h".
(3) The following primitives in "caesar_graph.h" are now
defined as macro-definitions (with names starting with
"CAESAR_HINT_...") in an unambiguous way:
CAESAR_SIZE_STATE()
CAESAR_HASH_SIZE_STATE()
CAESAR_ALIGNMENT_STATE()
CAESAR_SIZE_LABEL()
CAESAR_HASH_SIZE_LABEL()
CAESAR_ALIGNMENT_LABEL()
(4) The following primitives in "caesar_graph.h" are now
defined as functions (and no longer as array-based
macro-definitions):
CAESAR_TRANSITION_LABEL()
CAESAR_VISIBLE_LABEL()
CAESAR_GATE_LABEL()
CAESAR_HIDDEN_GATE_LABEL()
CAESAR_CARDINAL_LABEL()
CAESAR_RANK_LABEL()
(5) The following primitives in "caesar_graph.h" are now
#defined and, therefore, no longer need to be implemented
in the C code generated by CAESAR with "-open" option:
CAESAR_CREATE_STATE()
CAESAR_DELETE_STATE()
CAESAR_COPY_STATE()
CAESAR_CREATE_LABEL()
CAESAR_DELETE_LABEL()
CAESAR_COPY_LABEL()
(6) The semantics of function CAESAR_STRING_LABEL() has
changed: from now on, each call to this function erases
the string computed and returned during the previous call.
Also, if the function fails, it no longer returns a NULL
pointer but aborts the program.
(7) The semantics of function CAESAR_TRANSITION_LABEL() has
changed: from now on, it returns a string (and no longer
an integer).
(8) The OPEN/CAESAR application files, previously located in
src/*.c, have been moved in src/open_caesar/*.c.
All related files have been accordingly updated.
The changes (1)-(5) do not affect the application programs
(located in src/open_caesar). The CAESAR compiler functioning
in open mode (with "-open" option) has been adapted in order
to be compatible with the new OPEN/CAESAR interfaces. All
other compilers generating C code for OPEN/CAESAR should be
adapted as well.
The changes (6)-(7) slightly affect the application programs,
as well as the CAESAR compiler itself. The "upc" migration
program has been adapted to flag the application programs
that need to be adapted. The CAESAR compiler with "-open"
mode has been adapted too.
The OPEN/CAESAR Reference Manual and the corresponding manual
pages have been updated to reflect these changes. There is
now a clear separation between features related to LOTOS
and CAESAR, and features independent from any language and
compiler. This should leave a maximal freedom for the
implementors wanting to connect their compilers to OPEN/CAESAR.
Number: 300
Date: Thu Jun 9 19:46:09 MET DST 1994
Files: src/open_caesar/declarator.c
Nature: An new OPEN/CAESAR application program named "declarator" has
been written. This program can be used to test if the "spec.c"
generated by a tool is correct or not. The "declarator"
program attempts to exercise all features described in the
"caesar_graph.h" interface.
Number: 301 Date: Thu Jun 9 20:29:07 MET DST 1994 Files: incl/caesar_standard.h Nature: A bug was fixed in the definition of CAESAR_PROTEST().
Number: 302
Date: Mon Jun 13 12:39:16 MET DST 1994
Report: Laurent Mounier, Arnaud Fevrier, Thomas Koch, Thomas Lambolais
Files: bin.*/caesar, bin.*/caesar.adt
Nature: CAESAR.ADT has been improved in order to give a better error
diagnostic when a sort cannot be enumerated. The old message
was:
...
caesar: simulation of ``gsm''
caesar: - simulator production
caesar: - simulator compilation
"gsm.c", line 1946: syntax error at or near symbol {
"gsm.c", line 1988: syntax error at or near symbol {
...
#156 error in file ``.h'' during simulation:
simulator program is rejected by the C compiler
quit
The new message is:
...
caesar: simulation of ``gsm''
caesar: - simulator production
caesar: - simulator compilation
caesar: - simulator execution
caesar: - graph dump for ``gsm'' using ``aldebaran'' format
#200 theoretical limitation :
domain of an infinite (or complex) sort cannot be enumerated
no available iterator for sort VLRACT [409]
#172 system error during simulation:
termination on SOFTWARE_TERMINATION signal (files completed)
quit
Number: 303
Date: Sat Jun 25 11:51:26 MET DST 1994
Report: Eric Valade (ALCATEL Lannion)
Files: bin.*/libcaesar.a, bin.*/caesar
Nature: The hash-code computation for labels was incorrect: two
identical labels could have different hash-codes. Functions
CAESAR_HASH_LABEL() and CAESAR_LABEL_0_HASH() have been
modified.
Number: 304
Date: Wed Jul 6 19:48:18 MET DST 1994
Report: Mats Kindahl (University of Uppsala)
Files: bin.*/libcaesar.a, bin.*/caesar
Nature: Hashing functions CAESAR_HASH_STATE(), CAESAR_HASH_LABEL(),
CAESAR_0_HASH() were incorrect and have been fixed.
Number: 305
Date: Thu Jul 7 19:29:15 MET DST 1994
Report: Christian Schneiter (VERIMAG)
Files: bin.*/caesar
Nature: A bug in optimization V2, which caused core dump, has been
fixed.
Number: 306
Date: Mon Jul 11 13:30:52 MET DST 1994
Files: bin.*/caesar, bin.*/caesar.adt
Nature: Thanks to Mihaela Sighireanu, the static semantics phase of
the CAESAR and CAESAR.ADT compilers has been updated. The
computation of type signatures was previously conformant
to the Draft International Standard of LOTOS. It is now
conformant to the current version of the standard, the
ISO International Standard 8807. As a consequence, more
correct LOTOS programs are now accepted and the combination
of renaming and actualization is now properly dealt with.
Number: 307 Date: Fri Jul 29 17:16:00 MET DST 1994 Files: lib/X_REAL.lib Nature: The importation of type NaturalNumber has been removed.
Number: 308 Date: Fri Aug 5 13:20:59 MET DST 1994 Files: bin.*/caesar Nature: A bug in optimization E5 has been fixed.
Number: 309
Date: Mon Aug 8 11:07:43 MET DST 1994
Files: bin.*/caesar
Nature: The warnings emitted when CAESAR finds "unreachable processes"
are now suppressed if the "-root" option is present on the
command-line.
Number: 310
Date: Fri Aug 12 17:53:24 MET DST 1994
Report: Claire Loiseaux (VERIMAG)
Files: incl/X_NATURAL.h
Nature: The file "X_NATURAL.h" was modified in order to be compatible
with the "gcc" compiler for use with C++ programs.
Number: 311
Date: Sat Aug 13 13:21:42 MET DST 1994
Files: bin.*/caesar
Nature: The optimizations are now executed and chained together in a
much faster way.
Number: 312
Date: Mon Sep 26 14:03:50 MET 1994
Files: bin.*/caesar, bin.*/caesar.adt
Nature: Special comments of the form (*! ... *) are now defined at
the syntactic level, instead of the lexical level. There are
more semantic verifications regarding the contents of these
comments.
As a consequence, an existing bug (occurrence of the '$'
character in some C identifiers generated automatically by
CAESAR and CAESAR.ADT) has been fixed.
The spelling of C identifiers might have changed (e.g.,
CAESAR_ADT_FUNC_23 might be renamed in CAESAR_ADT_FUNC_35).
If this problem occurs, the ``.h'' files produced by old
versions of CAESAR.ADT should be regenerated using the new
version of CAESAR.ADT.
Number: 313
Date: Wed Oct 12 20:03:13 MET 1994
Files: com/caesar.open, src/open_caesar/generator.c,
src/open_caesar/reductor.c, src/open_caesar/xsimulator.c
Nature: The "caesar.open" shell-script has been modified: it parses
the contents of the "user.c" program in order to determine
auxiliary options for the C pre-processor, the C compiler and
the link editor. These options are expressed in "user.c"
using directives of the form:
static char *CPPFLAGS = "@(#)CPPFLAGS = ..."
static char *CFLAGS = "@(#)CFLAGS = ..."
static char *LDFLAGS = "@(#)LDFLAGS = ..."
Number: 314
Date: Wed Oct 12 20:03:13 MET 1994
Files: bin.*/bcg_expand, bin.*/bcg_io, bin.*/bcg_lib,
bin.*/libBCG.a, bin.*/libBCG_IO.a, bin.*/libbcg_draw.a,
bin.*/libbcg_io.a, bin.*/libbcg_open.a,
com/bcg_draw, com/bcg_open,
incl/bcg_*.h, src/bcg_draw/*.ps
man/manl/bcg.l, man/manl/bcg_draw.l, man/manl/bcg_io.l,
man/manl/bcg_lib.l, man/manl/bcg_open.l
Nature: A complete software environment named BCG (standing for
"Binary-Coded Graphs") has been added to the CADP toolset.
This software is described in the corresponding manual pages
"man/manl/bcg_*.l".
Number: 315
Date: Wed Oct 12 20:04:08 MET 1994
Files: src/open_caesar/generator.c, src/open_caesar/reductor.c
Nature: The "generator" and "reductor" programs of OPEN/CAESAR have
been modified: they now produce Labelled Transition Systems
encoded in the BCG format (instead of producing Labelled
Transition Systems in pseudo-ALDEBARAN format, which was
almost useless).
Number: 316
Date: Tue Oct 25 13:27:31 MET 1994
Files: src/open_caesar/xsimulator.c
Nature: A bug was fixed, which caused "xsimulator" to core dump when
the window given by the $DISPLAY environment variable could
not be opened.
Number: 317
Date: Mon Nov 14 16:15:07 MET 1994
Files: src/open_caesar/executor.c, src/open_caesar/exhibitor.c,
src/open_caesar/terminator.c, man/manl/aldebaran.l
Nature: The diagnostic sequences produced by the OPEN/CAESAR tools
"executor", "exhibitor", and "terminator" are now displayed
using the SEQUENCE format. This format is described in the
ALDEBARAN manual page.
Number: 318
Date: Thu Nov 17 13:20:32 MET 1994
Files: src/open_caesar/exhibitor.c, man/manl/exhibitor.l
Nature: The exhibitor program has been improved in many ways:
* The algorithm now looks for "shortest" execution sequences.
* The ``-'' option was added, which allows to input an
execution sequence described using the SEQUENCE format.
* The new option ``-only'' provides new rules for hiding
labels.
* The new option ``-depth'' provides an upper bound on the
length of execution sequences to be searched.
* The new options ``-none'', ``-all'', ``-first'', and
``-decr'' allow to control the execution sequences displayed.
All these changes are upward compatible.
Number: 319
Date: Thu Nov 17 13:21:07 MET 1994
Files: src/open_caesar/terminator.c, man/manl/terminator.l
Nature: The terminator program has been improved in many ways:
* The algorithm was improved in order to find more accurate
execution sequences.
* The algorithm now looks for "shortest" execution sequences.
* The new option ``-depth'' provides an upper bound on the
length of execution sequences to be searched.
* The new options ``-none'', ``-all'', ``-first'', and
``-decr'' allow to control the execution sequences displayed.
All these changes are upward compatible.
Number: 320
Date: Fri Nov 18 12:10:57 MET 1994
Files: bin.*/libcaesar.a, incl/caesar_edge.c, man/manl/caesar_edge.l,
doc/Garavel-92-a.ps,
Nature: The "edge" library of OPEN/CAESAR has been enriched with two
new functions CAESAR_COPY_EDGE() and CAESAR_COPY_EDGE_LIST().
Number: 321
Date: Fri Nov 18 13:11:07 MET 1994
Files: bin.*/libcaesar.a, incl/caesar_stack_1.c,
man/manl/caesar_stack_1.l, doc/Garavel-92-a.ps,
Nature: The "stack_1" library of OPEN/CAESAR has been enriched with two
new functions CAESAR_PURGE_STACK_1() and CAESAR_COPY_STACK_1().
Number: 322
Date: Sat Nov 19 14:20:57 MET 1994
Files: bin.*/libcaesar.a, incl/caesar_diagnostic_1.c,
man/manl/caesar_diagnostic_1.l, doc/Garavel-92-a.ps,
Nature: A new library ("diagnostic_1") has been added to OPEN/CAESAR.
Number: 323
Date: Mon Nov 21 21:05:50 MET 1994
Files: src/open_caesar/predictor.c
Nature: The predictor program has been improved: the amount of memory
available is now computed using the UNIX command "pstat".
Number: 324
Date: Sat Nov 26 20:35:53 MET 1994
Files: bin.*/caesar, bin.*/caesar.adt, com/caesar.aldebaran,
com/caesar.open, com/caesar.xesar
Nature: All the LOTOS tools in the CADP package have been adapted
in order to accept LOTOS files with various suffixes: ".lotos",
".lot", and ".l": this will improve compatibility with other
existing LOTOS tools, such as those developed in the LOTOSPHERE
and EUCALYPTUS projects.
Number: 325
Date: Mon Dec 19 11:45:44 MET 1994
Files: man/manl/declarator.l, man/manl/executor.l,
man/manl/exhibitor.l, man/manl/generator.l,
man/manl/predictor.l, man/manl/reductor.l,
man/manl/simulator.l, man/manl/terminator.l,
man/manl/xsimulator.l
Nature: Manual pages have been provided for all the OPEN/CAESAR
application tools contained in the CADP package: declarator,
executor, exhibitor, generator, predictor, reductor, simulator,
terminator, and xsimulator.
Number: 326
Date: Tue Dec 20 14:46:17 MET 1994
Files: com/caesar.autograph
Nature: The "caesar.autograph" shell-script has been removed, since
it was no longer useful: the new version of AUTOGRAPH (atgV3)
no longer uses the ".sa" format, but the ".fc2" and ".atg"
formats. The new "bcg_io" tool should be used to replace
"caesar.autograph" as explained below:
(1) How can I apply AUTOGRAPH to a ".aut" file?
bcg_io FILE.aut FILE.fc2
atg FILE.fc2
(2) How can I apply AUTOGRAPH to a ".bcg" file?
bcg_io FILE.bcg FILE.fc2
atg FILE.fc2
(3) How can I apply AUTOGRAPH to a ".lotos" file?
caesar.open FILE.lotos generator
bcg_io FILE.bcg FILE.fc2
atg FILE.fc2
Number: 327
Date: Tue Dec 20 14:46:17 MET 1994
Report: Roland Groz (CNET), Mark Ardis (AT&T)
Files: com/aldebaran.msc, man/manl/aldebaran.msc.l,
demos/demo_09/:READ_ME
Nature: The "aldebaran.msc" shell-script was bugged in several ways:
therefore, it has been removed from the CADP package. It is
replaced by the new "bcg_open" and "exhibitor". The previous
command:
aldebaran.msc FILE_1.aut FILE_2.msc
should be replaced by the following ones:
bcg_io FILE_1.aut FILE_1.bcg
bcg_open FILE_1.bcg exhibitor -only - < FILE_2.msc
The new approach has several advantages:
- it is faster;
- it computes the shortest execution sequence matching
FILE_2.msc;
- it displays the hidden gates corresponding to "i"
actions;
It can even be applied "on-the-fly" to LOTOS programs (instead
of labelled transition systems):
caesar.open FILE_1.lotos exhibitor -only - < FILE_2.msc
Also, the ".msc" suffix was changed into ".seq".
Number: 328
Date: Wed Jan 18 20:31:45 MET 1995
Report: Charles Pecheur (Univ. of Liege)
Files: bin.*/hostinfo, com/rfl
Nature: The RFL shell-script has been deeply modified and binary
programs named "hostinfo" have been introduced in order to
remove a configuration problem for stations with multiple
IP addresses.
Number: 329
Date: Wed Jan 18 20:31:45 MET 1995
Files: com/arch, com/caesar.open
Nature: Shell-scripts have been added or modified in order to deal
with non BSD Unix systems (especially Solaris 2.*).
Number: 330
Date: Wed Mar 22 20:01:35 MET 1995
Report: Roland Groz (CNET)
Files: bin.*/caesar
Nature: A subtle bug was fixed in optimization U2, which caused a
core dump when using CAESAR.
Number: 331
Date: Fri Mar 24 17:06:53 MET 1995
Report: Claude Jard (IRISA)
Files: bin.*/aldebaran
Nature: Problems occured when processing .exp files containing
uppercase and lowercase labels. This was fixed, considering
that .exp files are case-sensitive unless explicitely
mentioned by the keyword "behaviour" (or "behavior") at the
beginning.
Number: 332 Date: Thu Apr 6 11:48:34 MET DST 1995 Files: bin.*/caesar Nature: A bug in optimization E5 has been fixed.
Number: 333 Date: Wed Apr 19 10:16:05 MET DST 1995 Report: Alain Kerbrat (Bull-IMAG) Files: bin.*/bcg_io Nature: The FC2 graphs generated by bcg_io were sometimes incorrect.
Number: 334
Date: Fri May 5 18:44:30 MET DST 1995
Report: Laurent Mounier (VERIMAG)
Files: demo_07/overtaking.hide, demo_07/overtaking.rename,
demo_08/rel_rel.hide, demo_11/rel_rel.hide
Nature: The ".hide" and ".rename" files of demos #7, #8 and #11 were
incorrect with respect to ALDEBARAN's behaviour, and have been
corrected.
Number: 335
Date: Fri May 12 12:35:05 MET DST 1995
Files: bin.*/caesar
Nature: The optimization V3 has been modified, so as to perform
"symbolic" constant detection (i.e., constant detection
without C code generation) in the case where the generation
or compilation of C code for optimization V3 failed.
Number: 336 Date: Fri May 12 12:36:18 MET DST 1995 Files: bin.*/caesar, man/manl/caesar.l Nature: A "-trigger" option was added to CAESAR.
Number: 337
Date: Fri May 12 14:38:48 MET DST 1995
Files: bin.*/caesar
Nature: The order in which optimizations are applied has been
carefully re-designed. With the new ordering, the average
number of optimizations applied has been reduced of 22%,
thus resulting in speed increase, without increase in the
size of generated networks or graphs. In a few cases, the
generated graphs are even smaller.
Number: 338
Date: Mon May 15 20:03:14 MET DST 1995
Files: com/bcg_open, com/caesar.open,
man/manl/bcg_open.l, man/manl/caesar.open.l
Nature: The "caesar.open" and "bcg_open" commands have been extended
so as to accept ".o" files (instead of ".c" files) as
arguments.
Number: 339
Date: Wed May 24 11:08:40 MET DST 1995
Files: bin.*/evaluator.o, man/manl/evaluator.l
Nature: An "on-the-fly" evaluator for branching-time mu-calculus and
LTAC temporal logic has been added to the CADP toolbox. It
can be used with "caesar.open" and "bcg_open".
Number: 340
Date: Wed May 31 19:20:43 MET DST 1995
Report: Jean-Claude Fernandez, Laurent Mounier (VERIMAG)
Files: demo_06/*, demo_11/*
Nature: A bug was fixed in demo_11 (compositional rel/REL). demo_06
was modified accordingly.
Number: 341
Date: Fri Jun 23 20:58:55 MET DST 1995
Files: com/caesar.open, com/upc
Nature: The commands "caesar.open" and "upc" have been modified to
work also under Solaris 2.x
Number: 342
Date: Sat Jun 24 10:33:39 MET DST 1995
Files: bin.*/caesar, bin.*/caesar.adt, ./INSTALLATION
man/manl/caesar.l, man/manl/caesar.adt.l
Nature: Two environment variables, $CADP_LANGUAGE and $CADP_CC, have
been added to CAESAR and CAESAR.ADT. They allow to select
which language is used for diagnostics ("french" or "english")
and which C compiler is used ("cc", "gcc", etc.). The
installation manual and on-line manual pages have been updated.
Number: 343
Date: Mon Jun 26 16:21:00 MET DST 1995
Files: (many)
Nature: For Solaris 2.x portability reasons, the default value of the
C compiler is now "cc" instead of "/bin/cc". Similarly, the
default value of the C pretty-printer is now "indent" instead
of "/bin/indent". Users will have to set their $PATH variables
properly.
Number: 344
Date: Fri Jun 30 12:25:40 MET DST 1995
Files: bin.*/caesar, bin.*/caesar.open, gc/*,
man/manl/caesar.l, man/manl/caesar.open.l
Nature: Thanks to Mihaela Sighireanu, the Boehm-Demers garbage
collector has been interfaced with the CADP toolbox.
A "-gc" option has been added to CAESAR and CAESAR.OPEN.
By reusing the memory allocated for abstract data types,
this option allows larger LOTOS descriptions to be processed.
Number: 345
Date: Mon Jul 17 19:06:22 MET DST 1995
Report: Mihaela Sighireanu (VERIMAG)
Files: bin.*/caesar, bin.*/caesar.adt
Nature: In the front-end of CAESAR and CAESAR.ADT, parameterized types
were implemented according to the DIS ("Draft International
Standard") semantics. For instance, the standard LOTOS library
could not be compiled. The new version of CAESAR and CAESAR.ADT
is now fully conformant with the IS ("International Standard")
semantics. The DIS semantics is no longer available.
Number: 346
Date: Mon Jul 17 20:11:02 MET DST 1995
Report: Mihaela Sighireanu (VERIMAG)
Files: bin.*/caesar, bin.*/caesar.adt, doc/Garavel-Sighireanu.ps
man/manl/caesar.l, man/manl/caesar.adt.l
Nature: An error was identified in the IS semantics for parameterized
semantics and an appropriate solution was suggested (see
$CADP/doc/Garavel-Sighireanu.ps for a detailed explanation).
This solution has been implemented in CAESAR and CAESAR.ADT
as the default semantics. However, the IS semantics is also
retained and can be obtained by giving the "-iso" option
to CAESAR and CAESAR.ADT.
Number: 347
Date: Sun Jul 30 13:10:48 MET DST 1995
Report: Mihaela Sighireanu (VERIMAG)
Files: bin.*/caesar, bin.*/caesar.adt
Nature: There was an error in the front-end of CAESAR and CAESAR.ADT,
with respect to static semantics checking. When binding sorts
in behaviour expressions, all types without formal sorts in
their signature were taken into account. Similarly, when
binding operations in behaviour expression, all types without
formal operations in their signature were taken into account.
From now on, when binding sorts or operations, only those
types that have neither formal sorts nor formal operations
in their signatures are taken into account.
Number: 348
Date: Sun Jul 30 16:29:25 MET DST 1995
Files: src/xsimulator.c, x11/*
Nature: The OPEN/CAESAR "xsimulator" program was modified in order
to be ported to Sun5 machines running Solaris 2.*. The
non-standard "Xaw3d" (3-dimension widgets) was replaced with
the standard "Xaw" library. The "Ximag" library was
accordingly updated.
Number: 349
Date: Fri Aug 11 14:14:07 MET DST 1995
Report: Radu Mateescu (VERIMAG)
Files: incl/X_BOOLEAN.h
Nature: The following implementations of boolean operators in C:
#define ADT_XOR(X1,X2) ((X1) != (X2))
#define ADT_IMPLIES(X1,X2) ((X1) <= (X2))
#define ADT_IFF(X1,X2) ((X1) == (X2))
#define ADT_EQ_BOOL(X1,X2) ADT_IFF (X1, X2)
#define ADT_NE_BOOL(X1,X2) ADT_XOR (X1, X2)
were erroneous (they assumed that "true" was implemented
by 1, which might not be the case in general) and have been
corrected.
Number: 350
Date: Wed Sep 6 11:47:37 MET DST 1995
Report: Ghassan Chehaibar (Bull)
Files: lib/Y_ENUMERATION.lib
Nature: The 'enumerated type' example given in "lib/Y_ENUMERATION.lib"
was unclear and too specific of OSI protocols. It has been
replaced with a simpler and more general example, from which
CAESAR.ADT can produce optimal C code.
Number: 351
Date: Fri Sep 8 20:22:34 MET DST 1995
Report: Richard H. Carver ((George Mason University, Fairfax, USA)
Dirk Keck (IND, University of Stuttgart, Germany)
Serge Robinson (INT, Evry, France)
Files: com/rfl
Nature: The RFL command has been improved in many ways:
(1) When preparing an RFL for the local machine, it uses
"sh" and "cp" instead of "rsh" and "rcp", which does
not require any configuration in the ".rhosts" file.
(2) The error messages have been improved.
(3) Comments are displayed as target machines are examined.
(4) RFL now checks whether the $CADP variable is properly
set on each target machine.
(5) TFL now checks whether the architecture of each target
machines is supported by the CADP distribution.
(6) A "-f" option was added, which allows to reuse the
list of machines mentioned in an already existing
LICENSE file (see the INSTALLATION file).
Number: 352
Date: Wed Sep 13 15:05:16 MET DST 1995
Report: Jian Chen (George Mason University, Fairfax, USA)
Files: ./INSTALLATION
Nature: The incorrect command:
alias caesar.adt caesar -english
was replaced with:
alias caesar.adt caesar.adt -english
Number: 353
Date: Wed Sep 13 18:38:32 MET DST 1995
Files: ./INSTALLATION
Nature: The INSTALLATION manual has been deeply revisited.
It integrates the new mechanisms for supporting multiple
architectures (especially the "split" FTP distribution).
Number: 354
Date: Wed Sep 13 20:11:10 MET DST 1995
Report: Mats Kindahl (Univ. Uppsala)
Files: ./INSTALLATION
Nature: A bug was fixed in the INSTALLATION file. The command:
setenv MANPATH $MANPATH:$CADP/man
that caused problems with csh ("Variable syntax") and tcsh
("Unknown variable modifier") has been corrected.
Number: 355
Date: Wed Oct 18 18:42:26 MET 1995
Files: com/bcg_edit, src/bcg_edit/*.tcl, tcl-tk/*
Nature: Thanks to Louis-Pascal Tock, a new tool ("bcg_edit") has been
added to the BCG environment. This tool is a user-friendly,
TCL-TCK based, graphical editor, which allows to modify
interactively the graphical representation of BCG graphs.
Number: 356
Date: Thu Oct 19 18:47:02 MET 1995
Files: com/exp.open, bin.*/exp2c, bin.*/libexpopen.a,
man/manl/exp.open.l
Nature: A new tool called exp.open has been added. This tool allows to
apply OPEN/CAESAR to ".exp" files, by translating ".exp" files
into an OPEN/CAESAR graph module. (see the exp.open manual for
more informations).
Number: 357
Date: Mon Oct 23 16:32:54 MET 1995
Files: doc/*
Nature: New papers have been added in the "doc" directory:
doc/Mounier-94.ps
doc/Kerbrat-94.ps
doc/Garavel-95-a.ps
doc/Garavel-Sighireanu-95.ps
doc/Kerbrat-BenAtallah-95.ps
doc/Tock-95.ps
The READ_ME and biblio.bib files have been updated.
Number: 358
Date: Tue Nov 21 13:20:24 MET 1995
Report: Ghassan Chehaibar (Bull)
Files: bin.*/caesar
Nature: CAESAR's algorithm for determining which transitions can be
fired from a given marking has been entirely revisited. The
new algorithm significantly reduces the size of the C programs
generated by CAESAR with options "-e7", "-open", "-simulator",
and all other options for generating graphs in a given format.
For instance, the size of the C code generated from the
description in LOTOS of Bull's Pegasus architecture has been
significantly reduced: from 30 Mbytes with the old algorithm
down to 8.3 Mbytes with the new one.
Similarly, the size of the C code generated from the LOTOS
description of the Airbus A340 Flight Warning Computer was
reduced from 6 Mbytes down to 4.2 Mbytes.
Number: 359
Date: Wed Nov 22 16:50:40 MET 1995
Files: bin.*/aldebaran
Nature: Operator ``||'' (full synchronisation) has been introduced
in the .exp format.
Number: 360
Date: Thu Nov 30 16:38:55 MET 1995
Files: demos/demo_12, demos/demo_13, demos/demo_14
Nature: Three new demos have been added to the toolbox:
- demo_12 : Message Authentication Algorithm
- demo_13 : a collection of BCG graphs to be displayed
using BCG_DRAW
- demo_14 : a Plain Old Telephony System (POTS)
Number: 361
Date: Thu Nov 30 17:02:43 MET 1995
Files: com/tst, ./INSTALLATION
Nature: A new shell-command "tst" was added to the CADP toolbox.
This command checks whether the CADP software is properly
installed. It can be helpful to locate installation problems.
Its usage is described in the INSTALLATION file.
Number: 362
Date: Thu Dec 14 15:12:08 MET DST 1995
Report: Hubert Garavel (VERIMAG)
Files: bin.*/aldebaran
Nature: A bug in ALDEBARAN's diagnostics was fixed. For the
``+*equ'' options, the action names ending the diagnostic
sequences were incorrect.
Number: 363
Date: Wed Dec 20 07:43:33 MET 1995
Files: bin.*/aldebaran
Nature: Data structures used for implementing the Paige/Tarjan
algorithm have been optimized. In particular, labelled
transition systems with numerous distinct labels can
be much more efficiently processed.
Number: 364
Date: Thu Jan 4 18:45:35 MET 1996
Files: bin.*/caesar, man/manl/caesar.l
Nature: The "-root" option of CAESAR was improved in order to generate
much smaller graphs. As a consequence of this improvement,
it is no longer allowed for a process P to have value-
parameters, if this process P is to be used in a "-root P"
or "-root P [G1, ..., Gn]" option. CAESAR's manual page was
updated accordingly.
Number: 365
Date: Fri Jan 12 19:04:17 MET 1996
Files: com/swapsize, src/predictor.c
Nature: A new shell-command "swapsize" was added to the CADP toolbox.
This command displays the amount of memory (swap) available.
The OPEN/CAESAR "predictor" program was modified to use the
(architecture-independent) command "swapsize".
Number: 366
Date: Fri Jan 19 18:06:22 MET 1996
Files: bin.*/caesar, man/manl/caesar.l
Nature: A new option "-bcg" was added to CAESAR, which allows CAESAR
to generate BCG graphs directly. Option "-graph" is no longer
a default option; option "-bcg" becomes the default instead.
Number: 367
Date: Thu Jan 25 11:45:26 MET 1996
Files: bin.*/aldebaran, man/manl/aldebaran.l
Nature: Thanks to a new option "-output" (see aldebaran manual
for more informations) ALDEBARAN has been connected
to the BCG format: it can now read BCG files (using an
horrible kludge to be fixed in later releases) and produce
a BCG file as output (after an LTS reduction).
Number: 368
Date: Thu Jan 25 11:45:26 MET 1996
Files: bin.*/aldebaran, man/manl/aldebaran.l
Nature: For compatibility reasons the ".aut" files produced by
ALDEBARAN are no longer automatically sorted when using
the "-exp2aut" options. On the other hand, the "-sort"
option has been added (see aldebaran manual for more
informations).
Number: 369
Date: Tue Mar 12 16:35:07 1996
Report: Guy Leduc (Univ. Liege)
Files: bin.*/aldebaran
Nature: A bug was fixed. The on-the-fly computation of branching
bisimulation was incorrect in some cases, especially in
presence of "tau" circuits in one of the LTSs.
Number: 370
Date: Thu Apr 25 15:05:44 MET DST 1996
Report: Jean-Pierre Krimm (VERIMAG)
Files: bin.*/exp2c, bin.*/libexpopen.a
Nature: A bug was fixed in exp.open. The LTSs used in the ".exp"
files were incorrectly read, and therefore the graph module
generated by exp.open was sometimes erroneous.
Number: 371
Date: Mon Apr 29 18:25:18 MET DST 1996
Files: src/predictor.c
Nature: A missing "exit (0)" statement was added at the end of the
predictor program.
Number: 372
Date: Tue May 21 17:38:50 MET DST 1996
Report: Christophe Broult (SEPT)
Files: bin.*/caesar, bin.*/caesar.adt
Nature: In the previous versions of CAESAR and CAESAR.ADT, the maximal
number of include files (".lib" files) was limited to 32,
resulting in the following error message:
#022 error during analysis:
too many include files
quit
This maximal value was raised to 128.
Number: 373
Date: Tue Jun 4 19:32:31 MET DST 1996
Files: bin.sun3, bin.sun3.gcc, *.sun3.*
Nature: We decided to discontinue support for SUN 3 hardware platforms,
as the license mechanism informed us that no SUN 3 machine
was still running CADP. This makes the new CADP release much
lighter.
Number: 374
Date: Mon Jun 3 19:49:02 MET DST 1996
Files: bin.*/caesar, bin.*/caesar.adt
Nature: Three inconsistencies in the error messages displayed by
CAESAR and CAESAR.ADT (with respect to library inclusion)
have been identified and fixed.
Number: 375
Date: Tue Jun 4 20:14:02 MET DST 1996
Files: doc/*
Nature: New papers have been added in the "doc" directory:
doc/Fernandez-Mounier-95.ps
doc/Garavel-Fernandez-et-al-96.ps
doc/Garavel-Mounier-96.ps
The READ_ME and biblio.bib files have been updated.
Number: 376
Date: Mon Jun 10 19:22:14 MET DST 1996
Report: bin.*/caesar, man/manl/caesar.l
Nature: A new option "-gradual" was added to CAESAR. This option
applies the optimizations gradually when generating the
network. By default, the optimizations are applied only
after the network is fully generated. Using this option,
the optimizations are applied to each sub-network generated
from each operand of a parallel composition operator.
This option is slower, but it can be useful for dealing with
larger LOTOS descriptions and/or for generating smaller
networks. For instance, the network generated for the
LOTOS description of Airbus A-340 Flight Warning Computer
has 1,377 places, 3,411 transitions and 664 variables
without "-gradual" option, and only 1,173 places, 2,473
transitions, and 597 variables with "-gradual" option.
Number: 377
Date: Tue Jun 11 12:34:01 MET DST 1996
Report: Jean-Michel Hufflen (Univ. de Franche-Comte, France)
Files: bin.*/caesar
Nature: The C code generated by CAESAR has been modified to be
conformant with ANSI C. This will avoid the warnings
which were previously displayed when using "cc" under
Solaris 2.*, e.g.:
"bitalt.c", line 289: warning: semantics of ">>"
change in ANSI C; use explicit cast
or:
"bitalt.c", line 509: warning: semantics of "%"
change in ANSI C; use explicit cast
Number: 378
Date: Tue Jun 11 14:31:28 MET DST 1996
Report: Andreas Ulrich (Univ. Madgeburg, Germany)
Files: bin.*/caesar.adt, demos/demos_*/*.t
Nature: The iterators generated by CAESAR.ADT have been slightly
modified in two ways:
- They have been moved after the #include directive that
includes the ".t" file (they were previously defined
before the #include directive). Therefore, if the user
wants to provide his/her own iterator, it is no longer
necessary to #undef the iterator generated by CAESAR.ADT
- They are now enclosed between #ifndef ... #endif clauses,
not to override the user-defined iterators contained in
the ".t" files, if any.
The ".t" files provided in CADP demos have been simplified
accordingly (the #undef directives have been removed).
Number: 379
Date: Tue Jun 11 18:32:51 MET DST 1996
Report: Dirk O. Keck (IND, University of Stuttgart, Germany),
Andreas Ulrich (Univ. Madgeburg, Germany)
Files: src/executor.c
Nature: The "executor" program did not compile properly under Solaris
2.* unless "/usr/libucb" was included in "LD_LIBRARY_PATH".
The new version of executor solves the problem by using the
SVR4 compatible functions "rand()" and "srand()", rather than
the BSD functions "random()" and "srandom()".
Number: 380
Date: Wed Jun 12 11:35:55 MET DST 1996
Files: bin.*/aldebaran, man/manl/aldebaran.l
Nature: The new option "-path" has been added. It computes
the shortest path (from the initial state) to a given
state in an LTS. See aldebaran manual for more informations.
Number: 381
Date: Wed Jun 12 11:35:55 MET DST 1996
Report: Muffy Thomas (Univ. Glasgow, UK),
Lars-Ake Fredlund (SICS, Sweden)
Files: man/manl/evaluator.l
Nature: The manual page for "evaluator" was improved.
Number: 382
Date: Wed Jun 12 16:29:49 MET DST 1996
Report: Christophe Broult (SEPT and Univ. Caen, France)
Files: bin.*/aldebaran
Nature: Two problems have been fixed:
- The new version of ALDEBARAN does not core dump when
the character strings of the labels are too long
- The maximal number of distinct labels accepted by ALDEBARAN
was raised from 2,000 up to 4,000
Number: 383
Date: Wed Jun 12 17:00:12 MET DST 1996
Files: com/caesar.open
Nature: The "caesar.open" shell was adapted to support the new "-iso",
"-bcg" and "-gradual" options of CAESAR and/or CAESAR.ADT
Number: 384 Date: Fri Jun 28 16:31:27 MET DST 1996 Files: man/manl/*or.l Nature: The manual pages for the OPEN/CAESAR tools have been updated.
Number: 385 Date: Fri Jun 28 16:33:46 MET DST 1996 Files: com/caesar.open, com/bcg_open, com/exp.open Nature: A minor bug was fixed in these shells.
Number: 386
Date: Fri Jun 28 20:37:37 MET DST 1996
Files: bin.*/xsimulator.a, src/open_caesar/xsimulator,
tcl-tk/bin.*/libtcl.a, tcl-tk/bin.*/libtk.a,
tcl-tk/bin.*/duplex, man/manl/xsimulator.l
Nature: Thanks to Mark Jorgensen, a new version of Xsimulator has been
added to CADP. This new version, written in Tcl-Tk, replaces
the former one, based on raw Xlib programming. The new version
is fully compatible with the previous one, but contains several
improvements:
- It works without problems on Solaris 2.*. The minor problems
noticed with the previous version (warnings when compiling
the C code with a strict ANSI compiler, need to add libucb.o
in $LD_LIBRARY_PATH, etc.) are now solved.
- Only the transitions going out from the current state are
highlighted and can be selected.
- The new version of Xsimulator should be easier to port on
different machine architectures.
The following files and directories have been removed from the
CADP release: src/open_caesar/xsimulator.c and x11. The
manual pages have been updated.
Number: 387
Date: Wed Jul 3 12:11:27 MET DST 1996
Files: com/caesar.open, com/bcg_open, com/exp.open,
man/manl/caesar.open.l, man/manl/bcg_open.l,
man/manl/exp.open.l
Nature: These 3 shells scripts have been modified in order to accept
OPEN/CAESAR application programs given in form of archive files
(with suffix ".a"). The manual pages have been updated to
reflect the change
Number: 388
Date: Fri Jul 5 11:57:06 MET DST 1996
Report: Ghassan Chehaibar (Bull),
Mirela Sechi Moretti Annoni Notare (UFSC, Brazil)
Files: INSTALLATION
Nature: The directives contained in the INSTALLATION manual have
been updated to fix some problemes specific to Solaris 2.*
(especially with the "chown" command, which is not located in
the same directory in Solaris 1.* and Solaris 2.*)
Number: 389
Date: Mon Jul 29 16:48:57 MET DST 1996
Files: com/tst
Nature: The 'tst' shell-script was improved to detect the (potentially
hazardous) situations in which:
- the default "arch" command does not return the same
value as "$CADP/com/arch" (which is the case under
Solaris 2.5, where "arch" returns "sun4")
- the default "make" command provided by SunSoft is
overriden by another "make" command (e.g., the
BSD-make, or the GNU-make). This might create
problems with CAESAR.OPEN and the EUCALYPTUS 1.*
Graphical User Interface
- the default "cpp" command provided by SunSoft is
overriden by another "cpp" command (e.g., the
GNU-make). This might create problems with the
EUCALYPTUS 1.* Graphical User Interface
- the default "ld" command provided by SunSoft is
overriden by another "ld" command (e.g., the
GNU-make). This might create problems.
Number: 390
Date: Thu Aug 1 14:32:59 MET DST 1996
Report: Mirela Sechi Moretti Annoni Notare (UFSC, Brazil),
Alain Kerbrat (Verimag)
Files: bin.*/aldebaran, bin.*/bcg_*
Nature: A bug was fixed, which caused Aldebaran (and BCG tools) issue,
under Solaris 2.*, an error message of the form:
sh: /usr/local/cadp/bin.sun4/bcg_expand: not found
if the $PATH variable was configured in such a way that the
Solaris `arch` command was called in place of $CADP/com/arch.
Number: 391
Date: Mon Aug 5 11:49:24 MET DST 1996
Files: incl/caesar_*.h, src/open_caesar/*, bin.*/libcasesar.a,
bin.*/caesar, bin.*/libbcg_open.a, bin.*/exp2c,
doc/Garavel-92-a.ps, man/manl/caesar_*.l
Nature: A new type CAESAR_TYPE_STRING (equivalent to 'char *') has
been added in "caesar_standard.h". The profile of the
following functions has been modified to use this new type:
CAESAR_GRAPH_COMPILER()
CAESAR_TRANSITION_LABEL()
CAESAR_GATE_LABEL()
CAESAR_HIDDEN_GATE_LABEL()
CAESAR_DUMP_LABEL()
CAESAR_STRING_LABEL()
CAESAR_CREATE_DIAGNOSTIC()
The include files, libraries, documentation, application
programs, as well as CAESAR, BCG_OPEN and EXP.OPEN have
been modified accordingly. This change is strictly upward
compatible and should be transparent to all existing programs.
Number: 392
Date: Mon Aug 5 12:27:13 MET DST 1996
Files: incl/caesar_*.h, src/open_caesar/*, bin.*/libcaesesar.a,
bin.*/caesar, bin.*/libbcg_open.a, bin.*/exp2c,
doc/Garavel-92-a.ps, man/manl/caesar_*.l
Nature: A new type CAESAR_TYPE_FILE (equivalent to 'FILE *') has
been added in "caesar_standard.h". The profile of the
following functions has been modified to use this new type:
CAESAR_PRINT_STATE_HEADER()
CAESAR_PRINT_STATE()
CAESAR_DELTA_STATE()
CAESAR_PRINT_LABEL()
CAESAR_PRINT_BITMAP()
CAESAR_CREATE_DIAGNOSTIC_1()
CAESAR_PRINT_EDGE()
CAESAR_PRINT_EDGE_LIST()
CAESAR_PRINT_STACK_1()
CAESAR_CREATE_TABLE_1()
CAESAR_PRINT_TABLE_1()
CAESAR_PRINT_VERSION()
The include files, libraries, documentation, application
programs, as well as CAESAR, BCG_OPEN and EXP.OPEN have
been modified accordingly. This change is strictly upward
compatible and should be transparent to all existing programs.
Number: 393
Date: Fri Aug 23 18:50:45 MET DST 1996
Files: bin.*/libcaesesar.a, man/manl/caesar_table_1.h,
doc/Garavel-92-a.ps,
Nature: In function CAESAR_PRINT_TABLE_1() of OPEN/CAESAR's
"caesar_table_1" library, when the printing format specified
by CAESAR_FORMAT_TABLE_1() is equal to 1 or 2, the mark
fields (if any) are not longer printed in hexadecimal.
The printing function specified when creating the table
should be responsible for printing the mark fields under
some appropriate (and more readable) form.
Number: 394
Date: Thu Aug 29 11:48:26 MET DST 1996
Files: incl/caesar_diagnostic_1.h, bin.*/libcaesesar.a,
man/manl/caesar_diagnostic_1.l, doc/Garavel-92-a.ps,
src/open_caesar/terminator.c, upc
Nature: There have been three changes in OPEN/CAESAR's "diagnostic_1"
library:
- A new function CAESAR_EMPTY_DIAGNOSTIC_1() was added.
- The profile of function CAESAR_BACKTRACK_DIAGNOSTIC_1() has
been modified in order to allow a more general use of this
function, namely in the case of breadth-first searches.
Formerly, the second argument of this fonction was a stack:
CAESAR_TYPE_STACK_1 CAESAR_K;
It has been replaced with an integer denoting the depth of
the stack:
CAESAR_TYPE_NATURAL CAESAR_DEPTH;
Consequently, all former invocations of this function:
CAESAR_BACKTRACK_DIAGNOSTIC_1 (d, k)
should be replaced with:
CAESAR_BACKTRACK_DIAGNOSTIC_1 (d, CAESAR_DEPTH_STACK_1 (k))
The "upc" program warns the user about this change.
- The semantics associated to CAESAR_NONE_DIAGNOSTIC_1 has
been slightly modified in order to make it a more useful
option.
Number: 395
Date: Wed Sep 4 18:54:22 MET DST 1996
Files: incl/caesar_graph.h, man/manl/caesar_graph.l,
doc/Garavel-92-a.ps,
bin.*/caesar, bin.*/libbcg_open.a, bin.*/exp2c,
src/open_caesar/declarator.c, src/open_caesar/simulator.i
Nature: OPEN/CAESAR's graph interface "caesar_graph.h" has been
modified in order to be even more independent from the
LOTOS language and to solve several programming difficulties.
The following changes have been brought:
#1 The semantics of the three functions CAESAR_PRINT_LABEL(),
CAESAR_DUMP_LABEL() and CAESAR_STRING_LABEL() has slightly
changed. The result of these functions no longer depends on
the current label format set using CAESAR_FORMAT_LABEL().
Therefore, these functions always produce a canonical
ASCII form for the labels.
#2 The two existing functions CAESAR_TRANSITION_LABEL() and
CAESAR_HIDDEN_GATE_LABEL() have been removed. They are re-
placed by a new function named CAESAR_INFORMATION_LABEL(),
which is simpler to use and independent from LOTOS. The
function CAESAR_FORMAT_LABEL() is now used to select the
type of informations sent by CAESAR_INFORMATION_LABEL().
These changes should be transparent to most OPEN/CAESAR
application programs:
- Programs that do not call CAESAR_FORMAT_LABEL() or only
call CAESAR_FORMAT_LABEL(0) remain unaffected by change #1
- Programs that do not call CAESAR_TRANSITION_LABEL() nor
CAESAR_HIDDEN_GATE_LABEL() remain unaffected by change #2.
- Programs that call either CAESAR_FORMAT_LABEL(1) or call
CAESAR_HIDDEN_GATE_LABEL() should now rely upon the new
function CAESAR_INFORMATION_LABEL() with format 1 for
obtaining source-level information about hidden gates.
- Programs that call CAESAR_TRANSITION_LABEL() should now
rely upon CAESAR_INFORMATION_LABEL() with format 2 for
obtaining source-level information about transitions.
The "upc" shell-script can be used for a simple diagnostic
of the required changes.
Several other components of the CADP toolbox have been
upgraded to reflect these changes, namely: CAESAR, BCG_OPEN,
EXP.OPEN, upc, declarator, simulator, and xsimulator.
Number: 396
Date: Thu Sep 5 10:45:12 MET DST 1996
Report: Alain Kerbrat (VERIMAG)
Files: bin.*/evaluator.o
Nature: A bug, which caused Evaluator to core dump under Solaris 2.*,
was fixed.
Number: 397
Date: Thu Sep 5 11:34:20 WET DST 1996
Report: Ghassan Chehaibar (Bull),
Jean-Charles Henrion et Guy Leduc (Univ. Liege)
Files: bin.*/exhibitor.a, bin.*/libcaesar.a, bin.*/aldebaran,
bin.*/libBCG_IO.a, doc/Garavel-92-a.ps, demos/demo_09
src/caesar_open/executor.c, src/caesar_open/terminator.c
man/manl/caesar_stack_1.l, caesar/manl/caesar_diagnostic_1.l
man/manl/aldebaran.l, man/manl/bcg_io.l, man/manl/executor.l,
man/manl/exhibitor.l, man/manl/terminator.l
Nature: The previous version of exhibitor (V1) has been replaced with
a new version (V2). Version V1 had two problems:
- It did not generate the shortest sequence. In some cases,
it produced a very long sequence (e.g. 200 transitions)
whereas a much shorter one (e.g. 20 transitions) existed.
- In some cases, it aborted (core dump) because the execution
stack used by the recursive procedure was overflown during
depth-first search.
Version V2 brings major improvements:
- The SEQUENCE format used to specify the sequence to be
searched has been significantly improved in exhibitor V2.
The new SEQUENCE format allows sophisticated patterns,
involving boolean operators and regular expressions.
Its syntax and semantics are formally described in
exhibitor's manual page,
- It implements two search algorithms: a depth-first one
(which generalizes and improves the algorithm used in V1),
and a breadth-first one, able to find shortest sequences.
Other changes between V1 and V2 are the following:
- With V2, it is no longer possible to specify the sequence
to be searched as command-line arguments, because the new
SEQUENCE format is more complex: the sequence must be
stored in a ".seq" file. The "-" option of V1 has been
removed (as it is the unique option in V2).
- The "-only" option of V1 has been removed. It is replaced,
in a more general way, by the pattern features provided
by the new SEQUENCE format.
- There are several new options in V2 (see exhibitor's manual
page).
- The new SEQUENCE language can characterize deadlock states
(using the <deadlock> keyword) and can therefore be used
to find the shortest sequence leading to a sink state.
- In addition to the introduction new features, the syntax of
the SEQUENCE language has changed with respect to the
definitions of labels (which should now be enclosed between
double-quotes "...") and comments.
- exhibitor V2 is distributed as a binary archive located in
"bin.*/exhibitor.a". The source code of exhibitor V1 is
kept in the "old" directory.
OPEN/CAESAR's libraries have been upgraded to support the
new SEQUENCE format. These changes should be transparent
to all application programs. They concern:
- the effects of the two functions CAESAR_FORMAT_STACK_1()
and CAESAR_PRINT_STACK_1() of OPEN/CAESAR's "caesar_stack_1"
library,
- the recommended actual parameters for the function
CAESAR_CREATE_DIAGNOSTIC_1() of OPEN/CAESAR's
"caesar_diagnostic_1" library.
Several other components of the CADP toolbox have been
upgraded to support the new SEQUENCE format, namely:
ALDEBARAN, BCG_IO, executor, and terminator.
The manual pages for executor, exhibitor, and terminator
incorrectly refered to the ALDEBARAN manual page for a
description of the SEQUENCE format. This has been fixed.
The manual page for ALDEBARAN has been also updated.
The :READ_ME and *.seq files of the demo_09 have been
updated to exhibitor V2 and to the new SEQUENCE format.
Number: 398
Date: Thu Sep 5 14:04:04 WET DST 1996
Report: Mirela Sechi Moretti Annoni Notare (UFSC, Brazil)
Files: src/open_caesar/executor.c
Nature: The modification made to port "executor" under Solaris 2.*
(see above bug fix #379) was not sufficient, since the rand()
does not behave identically in SVR4 and BSD. This caused an
error message of the form:
#945 error in function CAESAR_ITEM_EDGE_LIST [caesar_edge.c:894]
incorrect value for argument CAESAR_N
quit
This bug was fixed: "executor" should now run properly both
under SunOS 1.* and SunOS 2.*
Number: 399
Date: Tue Sep 10 12:45:34 MET DST 1996
Report: Jean-Pierre Krimm (VERIMAG)
Files: bin.*/libcaesar.a, incl/caesar_standard.h,
man/manl/caesar_standard.l, doc/Garavel-92-a.ps
src/caesar_open/*, com/upc
Nature: The undocumented macros CAESAR_ASSERT() and CAESAR_PROTEST()
previously defined in "caesar_standard.h" have changed: the
new versions have less parameters and should be used only
to report unexpected internal errors, mainly assertion
violations.
Two new functions CAESAR_ERROR() and CAESAR_WARNING() have
been introduced in "caesar_standard.h" and "libcaesar.a"
to report errors to the user (using parameters identical to
those of "printf").
CAESAR_ASSERT(), CAESAR_PROTEST(), CAESAR_ERROR(), and
CAESAR_WARNING() are now documented in OPEN/CAESAR manual
pages and reference manual.
The "upc" shell-script warns the user about these changes.
All the OPEN/CAESAR application programs ("executor", etc.)
distributed within CADP have been upgraded.
To upgrade software making use of the previous, undocumented
macros CAESAR_ASSERT() and CAESAR_PROTEST(), the following
steps should be observed:
- The "main" function should be declared with "argv" and "argc"
parameters, in the usual way (see for instance the C code
given in "src/open_caesar/executor.c").
- The first instruction of "main" should be the following:
CAESAR_TOOL = argv[0];
- Each call of the form:
CAESAR_ASSERT (A, B, C, D);
where D == NULL, should be simply replaced with:
CAESAR_ASSERT (A);
because parameter B (error code) is useless and because
parameter C (tool name) is now automatically supplied by
the global variable CAESAR_TOOL.
- Each call of the form
CAESAR_ASSERT (A, B, C, D);
where D != NULL, should be simply replaced with
if (!A) CAESAR_ERROR (D);
- Each call of the form:
CAESAR_PROTEST (B, C, D);
where D == NULL, should be simply replaced with:
CAESAR_PROTEST ();
- Each call of the form
CAESAR_PROTEST (B, C, D);
where D != NULL, should be simply replaced with:
CAESAR_ERROR (D);
Number: 400
Date: Wed Sep 11 17:10:53 MET DST 1996
Files: bin.*/libcaesar.a, bin.*/exhibitor.a,
src/open_caesar/terminator.c, src/open_caesar/simulator.i,
man/manl/caesar_stack_1.l, man/manl/caesar_diagnostic_1.l,
man/manl/exhibitor.l, man/manl/terminator.l,
doc/Garavel-92-a.ps
Nature: In the manual pages of the "stack_1" and "diagnostic_1", the
definition of ``stack depth'' and ``diagnostic size'' was
somehow ambiguous. It is now clearly stated that these values
are computed in number of states, not in number of transitions.
Several subtle bugs have been fixed in the implementation of
OPEN/CAESAR's "diagnostic_1" module, with respect to the
computation of depths.
The tools "exhibitor", "simulator", and "exhibitor" have been
modified: the argument of "-depth" option is considered to be
a number of transitions (not a number of states). Although this
convention is not the same as for OPEN/CAESAR's "stack_1" and
"diagnostic_1" libraries, it is more intuitive from the user
point of view and it is consistent with the behaviour of
"executor". The manual pages have been updated.
Number: 401
Date: Wed Sep 18 17:59:57 MET DST 1996
Files: bin.*/evaluator.a
Nature: The OPEN/CAESAR verification tool "evaluator" is now contained
in files "bin.*/evaluator.a" instead of "bin.*/evaluator.o".
From the user's point of view, this change should be fully
transparent.
Number: 402
Date: Thu Sep 19 11:03:19 MET DST 1996
Files: doc/*
Nature: New papers and research reports have been added in the 'doc'
directory:
- Chehaibar-Garavel-et-al-96
- Fernandez-Garavel-et-al-96
- Fernandez-Jard-Jeron-et-al-96-a
- Fernandez-Jard-Jeron-et-al-96-b
- Garavel-96
- Garavel-Mounier-96
- Garavel-Sighirea-96-a
- Mateescu-96
Also, new bibliographic references of interest have been added:
- Fredlund-Orava-96
- Korver-96
- Schieferdecker-96
Number: 403 Date: Mon Sep 30 19:44:17 MET 1996 Files: demos/demo_16, demos/demo_17 Nature: Two new demos have been added to the CADP package.
Number: 404
Date: Sun Oct 6 18:23:32 MET 1996
Files: com/xeuca, com/tst, src/eucalyptus/*
Nature: Thanks to Jean-Michel Frume, a new version of of the EUCALYPTUS
Graphical User-Interface is now available. This new version
(version 2.0) is written in TCL/TK, and supersedes the previous
versions (versions 0.*, 1.0, or 1.1) written in XtPanel.
The new version 2.0 brings significant improvements. Regarding
backward compatibility, the following remarks are of interest.
They only apply if you have already installed the EUCALYPTUS
Graphical User-Interface (versions 0.*, 1.0 or 1.1) on your
site:
- From now on, version 2.0 of EUCALYPTUS is included in the
CADP distribution: when installing CADP (beta-version Z-s or
higher), you implicitly install the EUCALYPTUS Graphical-User
Interface (version 2.0 or higher).
- To upgrade from EUCALYPTUS 0.* or 1.* to EUCALYPTUS 2.0, we
recommend the following procedure:
(1) Edit your startup file(s) (.cshrc, .profile, and/or
.tcshrc) and remove the definition of the "EUCALYPTUS"
environment variable and the definition of the "xeuca"
alias. For instance, in a .cshrc file, you should remove
the two following lines (if they are present):
setenv EUCALYPTUS pathname_of_the_Eucalyptus_directory
alias xeuca $EUCALYPTUS/com/xeuca
(2) Remove also the directory containing the obsolete version
of the EUCALYPTUS Graphical User Interface. This directory
was previously referenced by the $EUCALYPTUS variable.
(3) If you already have a "$HOME/.eucarc" file, you should
remove it or convert it to a "$HOME/.xeucarc" file,
according to the new format (you can find examples in
$CADP/src/eucalyptus/xeucarc_*). The existence of an
obsolete ".eucarc" file is detected by the "tst" command.
Number: 405
Date: Thu Oct 10 13:11:01 1996
Report: Hubert Garavel (INRIA)
Files: bin.*/aldebaran
Nature: A bug, which caused "aldebaran -live file.bcg" to core dump
has been fixed.
Number: 406
Date: Sat Oct 26 18:39:00 MET 1996
Files: tcl-tk/*, bin.*/xsimulator.a
Nature: The obsolete versions of TCL/TK (TCL 7.4 and TK 4.0) included
in CADP have been replaced with the most recent versions
currently available (TCL 7.6 and TK 4.2).
The Xsimulator program has been updated in order to work
properly with the new version of TCL/TK.
Number: 407
Date: Mon Oct 28 11:09:32 MET 1996
Files: src/open_caesar/deadlock.c
Nature: In directory $CADP/src/open_caesar, the symbolic link
"deadlock.c" pointing to "terminator.c" for backward
compatibility reason lasting from year 1992 (see entry
#176 in this file) has been removed.
Number: 408
Date: Fri Nov 15 10:53:36 MET DST 1996
Files: bin.*/des2aut, man/manl/des2aut.l
Nature: A new tool has been added for compositional generation.
Taking as inputs a composition expression describing a
network of communicating LTSs and a behavioral relation,
it incrementally produces the minimized global LTS
corresponding to this composition expression.
Composition expressions are described using an extension
of the EXP format which offers the two following features:
- elementary LTSs can be given either as ".aut" files,
or ".exp" files, or Lotos processes.
- a semi-composition operator is available to restrict
the behaviour of a sub-expression with respect to its
environment (represented by an interface LTS).
Number: 409
Date: Fri Nov 15 15:09:07 MET DST 1996
Files: bin.*/projector.a, man/manl/projector.l
Nature: A new tool has been added in the CADP toolbox to compute
"on-the-fly" the semi-composition of an implicit LTS with
respect to a given interface. It can be used either with
caesar.open, bcg_open or exp.open. See the "projector"
manual for more information.
Number: 410
Date: Fri Nov 15 17:00:05 MET DST 1996
Files: bin.*/exp2c, bin.*/libexpopen.a
Nature: The exp.open tool has been extended to process LTSs
obtained by semi-composition with user-given interfaces.
This new feature is mainly used by the des2aut tool for
compositional generation (see "exp.open" and "des2aut" manual
pages for more information).
Number: 411
Date: Tue Nov 19 19:29:59 MET 1996
Report: Hubert Garavel (INRIA)
Files: bin.*/aldebaran
Nature: A bug was fixed in aldebaran: the on-the-fly computation of
branching bisimulation (option "-fly -pequ") was incorrect
in some cases.
Number: 412
Date: Mon Nov 25 20:14:17 MET 1996
Files: src/open_caesar/simulator.c, src/open_caesar/simulator.i
Nature: Two mistakes have been fixed in the OPEN/CAESAR simulator:
- A typo ("atgv" instead of "argv") was fixed
- The "hidden" gate corresponding to "i"-transitions was
not printed, even with label format equal to 1.
Number: 413
Date: Mon Nov 25 21:26:19 MET 1996
Files: src/xsimulator/*
Nature: Four improvements and/or bug fixes have been made in the
OPEN/CAESAR xsimulator:
- The xsimulator window is now created as a background process
- The size of the xsimulator window was reduced so has to fit
in monitors smaller than 21-inches
- The label format radiobutton is now initialized correctly
(with 1 instead of 0)
- The "hidden" gate corresponding to "i"-transitions was
not printed, even with label format equal to 1.
Number: 414
Date: Mon Dec 2 16:49:43 MET 1996
Files: com/bcg_draw, com/bcg_edit, bin.*/xsimulator.a
Nature: From now on, the windows created by "bcg_draw", "bcg_edit" and
"xsimulator" are started as background processes (rather than
forground processes). This ensures a better integration of
these tools in the EUCALYPTUS graphical user-interface.
Number: 415
Date: Mon Dec 2 17:59:41 MET 1996
Files: com/xeuca, src/eucalyptus/*, man/manl/xeuca.l
Nature: Version 2.0 of the EUCALYPTUS graphical user-interface
(and all subsequent intermediate version 2.0a, 2.0b, ...
2.0v, 2.0w) have been replaced with a new version 2.1:
- All known bugs have been corrected
- Many new features have been introduced
- A manual page ((type "man xeuca") is now available
Number: 416
Date: Mon Dec 2 18:17:10 MET 1996
Report: Bruno Vivien (INRIA Rhone-Alpes)
Files: ./INSTALLATION
Nature: The explanations given in the INSTALLATION file have been
clarified in some points. Also, two new environment variables
($EDITOR and $NAVIGATOR) have been introduced.
Number: 417
Date: Tue Dec 3 14:48:25 MET 1996
Files: ./ADDRESSES, ./doc/:READ_ME
Nature: The new addresses, telephone numbers, fax numbers and e-mail
addresses of the CADP team are given in file $CADP/ADDRESSES.
Number: 418
Date: Tue Dec 3 17:31:01 MET 1996
Report: Bruno Vivien (INRIA Rhone-Alpes)
Files: com/tst
Nature: The "tst" command was improved in several ways:
- it does better verification about the "arch" command
- it eases the migration from previous versions 0.* and
1.* of EUCALYPTUS to EUCALYPTUS 2.1 (by detecting
obsolete features)
- it verifies the $EDITOR and $NAVIGATOR variables
- it checks for the existence of the "tee" command
Number: 419
Date: Tue Dec 3 17:35:30 MET 1996
Report: Toma Macavei (INT, Evry, France)
Files: doc/:READ_ME
Nature: For each PostScript or DVI file contained in the 'doc'
directory, the ':READ_ME' file indicates the corresponding
number of pages.
Number: 420
Date: Tue Dec 3 17:41:25 MET 1996
Report: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: A bug was fixed, which caused ALDEBARAN to core dump when
invoked with the "-path" option.
Number: 421
Date: Tue Dec 3 17:42:23 MET 1996
Report: Olivier Bonaventure (University of Liege)
Files: bin.*/aldebaran
Nature: A bug was fixed, which caused ALDEBARAN to return wrong
results when comparing two BCG files (since the unique
numbers assigned to all labels in both BCG files are not
necessarily the same).
Back to the CADP Home Page