|
| 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.
The VASY team of 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 97b "Liège" and is dated January 27, 1999. It supersedes all previous versions of CADP.
We are happy to dedicate CADP 97b "Liège" to Professor André Danthine who recently retired, after a brilliant academic carrier at the University of Liège. In addition to his prominent research works in telecommunications, Professor Danthine has been actively supporting formal methods (especially, LOTOS and E-LOTOS) for communication protocols.
The name "Liège" was also chosen because the first beta-version 97b-1 was demonstrated in this city, and because the Research Unit in Networking (now headed by Guy Leduc) plays a significant role in formal specification and validation of real systems.
This is a brief chronology of past events:
In a few words, the main characteristics of CADP 97b "Liège" are:
Additionally, the new release CADP 97b "Liège" brings many other features:
The following scientists have participated to the development of CADP 97b "Liège":
We are extremely grateful to the following scientists, who provided us with valuable feedback and advice about the beta-versions of CADP 97b "Liège":
People interested in LOTOS world-wide should also consult the WELL Page maintained by Prof. Ken Turner (University of Stirling, Scotland, UK).
Number: 484
Date: Fri Jun 27 15:10:08 MET DST 1997
Report: Ghassan Chehaibar (Bull/Dyade)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar.adt
Nature: When analyzing external types, CAESAR.ADT displayed the
following error message:
caesar.adt: syntax analysis of ``rcc''
caesar.adt: ...
caesar.adt: external type survey of ``rcc''
#005 bug :
unavailable option in this software
caesar.adt: ...
This message was meaningless, and it is no longer displayed.
Number: 485
Date: Fri Jun 27 16:29:07 MET DST 1997
Report: Mark Jorgensen (INRIA/VASY)
Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files: com/xeuca, src/eucalyptus/*
Nature: Clicking on a ".aut" file and choosing "Execute/Standard
simulation" did not work properly because an intermediate BCG
file was erased too early. This bug is now fixed.
Number: 486
Date: Fri Jun 27 17:25:37 MET DST 1997
Report: Mark Jorgensen (INRIA/VASY), Valerie Roy (INRIA/MEIJE) and
Robert de Simone (INRIA/MEIJE)
Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files: bin.*/bcg_io, bin.*/libBCG_IO.a
Nature: The FC2 files generated by BCG_IO had slight differences with
respect to the FC2 format accepted by the Fc2Tools developed
in the MEIJE project (especially with respect to "tau"-transi-
tions). These differences have been removed.
Number: 487
Date: Wed Jul 2 14:33:06 MET DST 1997
Report: Francois Germeau (Univ. of Liege)
Author: Hubert Garavel (INRIA/VASY)
Files: com/exp.open
Nature: The "exp.open" shell-script did not have execute permission,
which caused a problem when invoking this program.
Number: 488
Date: Mon Jul 7 20:26:39 MET DST 1997
Report: Ghassan Chehaibar (BULL/DYADE)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a, bin.*/bcg_io, bin.*/bcg_draw, bin.*/aldebaran
Nature: A bug in the BCG library was fixed, which caused the following
symptoms in BCG_IO, BCG_DRAW and ALDEBARAN (only when the
environment variable $CADP_CC was set to "gcc"):
(1) $ bcg_io foo.bcg foo.aut
==> bcg_io stopped after issuing the following message:
bcg_io: wrong number of parameters
bcg_dynamic: dynamic program error
(2) $ bcg_draw foo.bcg
==> ghostview was not launched and a core dump occurred
(3) $ aldebaran -bmin foo.bcg
==> a core dump occurred
Number: 489
Date: Tue Jul 8 11:39:17 MET DST 1997
Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files: demos/demo_04
Nature: The demo_04 (systolic arrays computing convolution product)
was improved for a better use of CAESAR.ADT functionalities,
especially with the importation of external types and functions
that are written in C. Also, the statistics have been updated.
Number: 490
Date: Tue Jul 22 12:15:36 MET DST 1997
Report: Hubert Garavel (INRIA/VASY)
Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files: src/eucalyptus/eucalyptus.tcl
Nature: A bug was fixed in the Eucalyptus graphical interface: when
the Aldebaran format or the Graph format were selected for
LTS generation, this selection remained later when the OPEN/
CAESAR tools were invoked, causing error messages of the form:
#016 error :
option ``-open'' is incompatible with graph generation
quit
Also, the "-monitor" option is now unselected automatically
when the Aldebaran format or Graph format is selected for
LTS generation.
Finally, several CAESAR options have been moved from the
"Generate LTS" panel to the "Options" menu. These options
are: "Optimization V3", "Optimization V4", "Optimization E7",
"Optimization Safety", "Optimization Gradual", and "Petri Net
Printing".
Number: 491
Date: Fri Jul 25 20:14:36 MET DST 1997
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_io
Nature: One of the BCG_IO functionalities (translation of LTSs into
pseudo-LOTOS code) did not work properly. This minor problem
was solved.
Number: 492
Date: Fri Jul 25 20:19:56 MET DST 1997
Authors: David Jacquemin and Hubert Garavel (INRIA/VASY)
Files: bcg.*/bcg_io, man/manl/bcg_io.l
Nature: The BCG_IO tool was extended so as to allow the translation of
an LTS into the simple SEQUENCE format (see "man exhibitor"
for a definition of this format). The translation is only
possible if the LTS has no circuits and if all its states
(with the possible exception of the initial state) have at
most one outgoing edge.
Number: 493
Date: Tue Jul 29 12:21:19 MET DST 1997
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar, bin.*/caesar.adt, incl/X_*.h, demos/*/*.t
Nature: In the ``.h'' files produced by the new version of CAESAR.ADT,
there is, for each type T, a macro-definition of the form:
#define CAESAR_ADT_SCALAR_T
iff variables of type T can be assigned the null value "0".
This macro-definition is used by CAESAR to decide whether a
variable X of type T can be reset by a simple assignment
(i.e., X = 0) or by a call to the C function "memset()".
Currently, this macro is defined by CAESAR.ADT for all the
C types generated from LOTOS sorts: integers, enumerations,
tuples (i.e., pointers to structs), and discriminated unions
(i.e., pointers to unions of structs).
On the opposite, this macro is not defined automatically for
external types: the user should define it selectively for
all external types T that allow the "0" value. Typical
examples of types T for which this macro should not be
defined are: structures, unions and arrays.
Forgetting to define this macro when appropriate is totally
harmless: the only drawback is that CAESAR will use the
"memset()" instead of an assignment, which is slightly less
efficient.
Some of the hand-written ``.h'' and ``.t'' files contained in
the ``incl'' and ``demos'' directories have been updated
accordingly.
Number: 494
Date: Tue Jul 29 15:31:33 MET DST 1997
Author: Hubert Garavel (INRIA/VASY)
Files: com/upc, com/rfl, com/tst, com/bcg_open, com/bcg_open,
com/exp.open
Nature: The shells scripts listed above have been updated to remove
some Solaris specific features that would prevent them to
work under Linux.
Number: 495
Date: Tue Aug 5 16:56:03 MET DST 1997
Report: Ghassan Chehaibar (BULL/DYADE)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/exp2c, bin.*/libexpopen.a
Nature: Several bugs were fixed, which could caused EXP.OPEN to
improperly manage the labels of LTS composition expresion.
Moreover, the number of distinct labels allowed has been
extended to 4000.
Number: 496
Date: Wed Aug 6 18:56:44 MET DST 1997
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_io, bin.*/libbcg_io.a, bin.*/libBCG_IO.a
The BCG_IO tool was modified in order to allow a smoother
translation between various formats:
- When translating a BCG graph into the Aldebaran format,
double quotes in labels are now replaced by single quotes;
a warning is emitted in such case.
- When translating a BCG graph into the Sequence format,
double quotes in labels are now replaced by single quotes;
a warning is emitted in such case.
- When translating a BCG graph into the Viscope format,
a message is emitted when commas are replaced by semicolons.
- When translating a BCG graph into the FC2 format, double
quotes are added around the labels, except for those labels
that already have double quotes inside (in such case, it is
likely that the label comes from an FC2 graph, e.g., has
the form "a"."b").
Number: 497
Date: Mon Aug 25 19:22:32 MET DST 1997
Authors: Hubert Garavel and David Jacquemin (INRIA/VASY)
Files: bin.*/bcg_io, bin.*/libbcg_io.a, bin.*/libBCG_IO.a
Nature: A minor bug was fixed in the translation into the FC2 format:
when given the "-verbose" option, the previous version of
BCG_IO printed ``hook "main"'' instead of ``hook "main">0''.
Also, in order to allow the FC2 files generated by BCG_IO to
be used with the Fc2Link tool, the new version of BCG_IO adds
a declaration of the form ``struct "filename"''.
Number: 498
Date: Tue Aug 26 20:31:30 MET DST 1997
Report: Radu Mateescu (INRIA/VASY)
Author: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: man/manl/bcg.l, man/windex, man/whatis
Nature: The BCG manual page has been modified in order to be correctly
indexed in the "windex" file: this page can now be accessed by
typing "man bcg" or "man BCG".
Number: 499
Date: Wed Aug 27 16:00:22 MET DST 1997
Report: Radu Mateescu (INRIA/VASY)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: Several minor bugs were fixed in ALDEBARAN regarding the
parsing of the command line (in particular when some options
were used with incorrect arguments).
Number: 500
Date: Wed Aug 27 16:04:02 MET DST 1997
Report: Mark Jorgensen (INRIA/VASY)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: Moreover, the "-live" option did not work properly when
applied to ".exp" files. This problem is now solved.
Number: 501
Date: Wed Aug 27 17:09:27 MET DST 1997
Report: Francois Germeau (Univ. de Liege, Belgium)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran, man/manl/aldebaran.l
Nature: A new option, "-labels", was added to ALDEBARAN. This option
defines the maximum number of distinct labels allowed in an
LTS (or in a composition of LTSs). The ALDEBARAN man page was
updated.
Number: 502
Date: Wed Aug 27 11:12:02 MET DST 1997
Authors: David Jacquemin and Hubert Garavel (INRIA/VASY)
Files: bcg.*/bcg_io, man/manl/bcg_io.l
Nature: The BCG_IO tool was extended so as to accept FC2 files as
input. The manual page has been updated accordingly.
Number: 503
Date: Thu Aug 28 18:04:18 MET DST 1997
Report: Radu Mateescu (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*.gcc
Nature: The two directories $CADP/bin.sun4.gcc and $CADP/bin.sun5.gcc
containing libraries compiled with the GCC compiler have been
removed, because they were not used actually. This makes the
CADP release simpler and lighter (1.5 less Megabytes).
Number: 504
Date: Thu Aug 28 21:46:17 MET DST 1997
Report: Radu Mateescu (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: incl/X_NATURAL.h
Nature: Three #include declarations have been added in X_NATURAL.h
in order to declare properly the functions kill() and getpid().
Number: 505
Date: Wed Sep 3 10:49:59 MET DST 1997
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/xtl, bin.*/xtl_expand, bin.*/libXTL.a, incl/xtl_*.h,
src/xtl/*, man/manl/xtl.l, com/rfl, VERSION
Nature: The CADP toolbox was enriched with a new tool named XTL
(an acronym for "eXecutable Temporal Language").
The XTL tool allows to evaluate temporal logic formulas
on graphs encoded in the BCG format. This tool offers the
following features:
- XTL supports several temporal logics widely used. Currently,
the following temporal logics are supported: HML, CTL, ACTL,
LTAC, as well as the modal mu-calculus. All of them can be
directly used by end-users to verify properties on BCG
graphs.
- Compared to other model-checkers, XTL is more expressive,
because it allows to handle the data values contained in
states and transition labels. These values can be used in
temporal formulas, assigned to variables, etc.
- Moreover, XTL is extensible. A user can define his/her own
temporal logic, as a library of operators written in XTL.
This is the way in which the currently available formalisms
(HML, CTL, ACTL, LTAC and modal mu-calculus) are implemented.
- Finally, XTL can also be used for other purpose than
evaluation of temporal formulas. Because it is a functional
programming language, it allows to perform any computation
on BCG graphs: for instance, it can compute the branching
factor of a graph, print its list of labels, etc.
For more details, see the manual page (by typing "man xtl")
and the predefined XTL libraries (in directory $CADP/src/xtl).
Number: 506
Date: Wed Sep 3 20:14 MET DST 1997
Author: Radu Mateescu (INRIA/VASY)
Files: demos/demo_21, demos/demo_22
Nature: Two new demo examples have been added to illustrate the use
of the XTL tool for verifying properties of distributed
algorithms in the LTAC temporal logic:
- demo_21 presents Peterson's mutual exclusion algorithm
- demo_22 presents Dekker's mutual exclusion algorithm
Number: 507
Date: Wed Sep 3 20:44 MET DST 1997
Author: Radu Mateescu (INRIA/VASY)
Files: demos/demo_01, demos/demo_02, demos/demo_16
Nature: Three existing demos have been improved in order to illustrate
the use of the XTL tool:
- In demo_01 and demo_02, a new file "bitalt.xtl" expresses the
properties of the alternating bit protocol (written as a
combination of mu-calculus and LTAC temporal logic).
- In demo_16, a new file "prop.xtl" expresses the properties
of the Philips Bounded Retransmission Protocol (written as
ACTL temporal logic formulas).
Also, the size of the BRP protocol has been enlarged to
take advantage of the speed increase in CAESAR: the number
of retransmissions was set to 3 and the message length was
set to 4.
Number: 508
Date: Fri Sep 5 16:16:37 MET DST 1997
Report: Massimo Zendri (BULL/DYADE)
Author: Mark Jorgensen (INRIA/VASY)
Files: bin.*/xsimulator.a
Nature: Xsimulator did not work properly if the $PATH variable of
the user did not contain "." (the current directory). This
problem is now solved.
Number: 509
Date: Tue Sep 9 10:29:19 MET DST 1997
Authors: Hubert GARAVEL (INRIA/VASY) and Laurent MOUNIER (VERIMAG)
Files: bin.*/exhibitor.a, bin.*/evaluator.a, bin.*/projector.a
Nature: The Exhibitor, Evaluator, and Projector libraries exported
objects generated by Lex/Yacc (e.g., yyparse, yytext, etc.)
which could create conflicts when linking with other code.
From now on, unique names are used.
Number: 510
Date: Wed Sep 10 10:22:58 MET DST 1997
Report: Ghassan Chehaibar (BULL/DYADE)
Author: Hubert Garavel (INRIA/VASY) and Laurent Mounier (VERIMAG)
Files: com/bcg_open, com/exp.open, man/manl/bcg_open.l
Nature: The previous versions of "bcg_open" and "exp.open" tried to
optimize CPU time by avoiding recompilations. However, the
optimization scheme was not precise enough, so that some
object files were reused incorrectly in some cases (especially
when using advanced compositional verification techniques).
The two tools have been modified so that they no longer try
to avoid recompilations. We do not expect this change to cause
any substantial decrease of performance, as "bcg_lib" already
avoids recompilations (in a safe way), and as most OPEN/CAESAR
tools are now shipped in archive format ("*.a" files). The
"bcg_open" manual page was updated to reflect this change.
Number: 511
Date: Wed Sep 10 11:02:10 MET DST 1997
Authors: Patrick Wendel, Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files: INSTALLATION, com/installator, src/installator, com/rfl,
tcl-tk/bin.*/expectk, tcl-tk/COPYRIGHT_EXPECT
Nature: A new installation procedure was designed for CADP. The main
changes are the following:
- A new program, named Installator, has been added to the
CADP toolbox. Installator is an computer-aided assistant
that will help CADP users to install and upgrade their
CADP software. Installator has been designed in the same
vein as "setup" programs in PC/Windows software and we
hope that CADP users will find it useful and convenient.
- The RFL program was adapted: new options have been added,
which are used by Installator.
- The "expectk" program version 5.24 (developed by Don Libes
at NIST, version 5.24) was added to the CADP release (in
binary form).
- As regards the FTP distribution of CADP, the notion of
"full" distribution was suppressed, because it was not used
by Installator. From now on, only the "splitted" distribution
will be retained, allowing a more flexible support of
multiple architectures/operating systems.
- The distribution of CADP by magnetic tapes was removed,
because everybody seems to prefer the distribution by FTP.
- The INSTALLATION file was modified to describe the new
installation procedure.
Number: 512
Date: Wed Sep 10 12:11:48 MET DST 1997
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar
Nature: There have been internal changes in CAESAR, in order to prepare
future evolutions of this tool (especially, state space
reduction). These changes are not visible to the users, but
two of them are worth mentioning:
- The format of the ".net" file was slightly modified (the
"unites quittees" clauses have been changed into "variables
annulees" clauses).
- In the C code generated by CAESAR, the preprocessor variable
CAESAR_IGNORE_ESCAPE was renamed into CAESAR_NO_CLEARANCE.
Number: 513
Date: Wed Sep 10 14:27:51 MET DST 1997
Report: Radu Mateescu (INRIA/VASY)
Author: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: bin.*/libBCG.a
Nature: A minor bug was fixed in the BCG format: the exponentiation
operator '**', previously declared as prefix at the source
language level, is now declared as infix. This bug had no
effect for any of the existing BCG tools and was revealed by
the newly introduced XTL tool.
When applying the XTL tool on BCG graphs generated with older
versions of CADP (i.e., version 97a or older), this problem
will not be noticeable, unless the XTL program invokes the
exponentation '**' in infix notation. Should this problem
happen, then generate your BCG file again, or upgrade it
using the following sequence of commands:
bcg_io FILE.bcg FILE.aut
bcg_io -aldebaran -parse FILE.aut FILE.bcg
rm FILE.aut
Number: 514
Date: Wed Sep 10 15:00:48 MET DST 1997
Authors: Mihaela Sighireanu and Radu Mateescu (INRIA/VASY)
Files: demos/demo_23
Nature: A new demonstration example was added to the CADP release:
the IEEE 1394 high performance serial bus ("Firewire").
Number: 515
Date: Wed Sep 10 15:19:24 MET DST 1997
Author: Mark Jorgensen (INRIA/VASY)
Files: src/eucalyptus/eucalyptus.tcl, src/eucalyptus/xeucarc_standard
com/xeuca_convert
Nature: Several fixes and major improvements have been done in the
EUCALYPTUS 2.3 Graphical User-Interface:
(a) The conversion of .aut, .seq and .bcg files to the
PostScript and encapsulated PostScript formats didn't work.
This problem is now solved.
(b) The reduction of .exp files with ALDEBARAN was stored in
a .exp file instead of a .aut file. This problem is now
solved.
(c) A minor typo caused the interface to stop when calling
the TESTGEN tool two successive times on the same file.
(d) The Fc2Tools developed by the Meije group at INRIA-Sophia
Antipolis have been integrated in the EUCALYPTUS toolset.
Like ALDEBARAN, it is now possible to apply these tools
to any automaton file, whatever its format (.bcg, .aut,
.fc2, .seq). All the underlying conversions are done
implicitly by EUCALYPTUS.
(e) Reciprocally, it is now possible to use the ALDEBARAN,
BCG and OPEN/CAESAR tools on automata encoded in the
.fc2 format. All the underlying conversions are done
implicitly.
(f) The file conversions between the various automata formats
have been optimised. EUCALYPTUS now maintains a database
to remember if a file has already been converted to a
format, in order to avoid multiple conversions.
Furthermore, the new conversions introduced in BCG_IO
(i.e., .fc2 to .bcg converter, and .bcg to .seq converter)
have been integrated in the interface.
(g) The "Compare..." window for automata is now smaller than
the previous one, with only one filebox instead of three.
(h) The "Evaluate mu-calculus formulas..." window is
now called "Verify temporal formulas...", and offers
the choice between the OPEN/CAESAR Evaluator tool
and/or the XTL tool (for automata only).
(i) The "Find deadlocks..." menus have been merged into
a unique window proposing the choice between all the
tools that can be used for this operation (Exhibitor,
Terminator, ALDEBARAN, Fc2Tools).
(j) The "Find livelocks..." window now proposes the choice
between ALDEBARAN and Fc2Tools.
(k) The menu that appears when clicking on a .lotos file has
been simplified. Some of the choices are now proposed in
a sub-menu that appears when choosing "More" in the menu.
(l) Two ALDEBARAN options, "-labels" and "-path", are now
supported by the EUCALYPTUS interface. In particular, it
is now possible to search for a path leading to a state
identified by its state number.
(m) The "Web" button now gives access to the CADP Frequently
Asked Questions page, to the CADP Patches page, and to
the Fc2Tools page.
(n) The "View" / "Change Presentation" windows was enhanced
so as to allow object files (.o) and BCG dynamic libraries
(*@1.o, *@2.o, etc.) to be hidden.
(o) An "Evaluator" entry was created in the "Options" menu.
This entry allows to set the verbosity and hash table
size values for Evaluator
(p) Within EUCALYPTUS, it is now possible to mail a file
to a specified e-mail address.
(q) The manual pages for Des2Aut, Projector and the Fc2Tools
are now available on-line from the "Help" button of
EUCALYPTUS.
(r) In "View" / "Change Presentation", the "Other files"
options has been fixed: previously it displayed all files
in the current directory; currently, it displays only
the files that do not belong to the aforementioned
file categories (Directories, Extended LOTOS Specs, etc.)
(s) It is now possible to save user preferences into the
startup file "$HOME/.xeucarc". This is done by clicking
the File / Save Preferences menu.
Number: 516
Date: Thu Sep 11 12:13:59 MET DST 1997
Report: Patrick Wendel (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: INSTALLATION_1, INSTALLATOR_2, INSTALLATOR_3, INSTALLATOR_4,
src/installator
Nature: The INSTALLATION file was too large and not convenient for
use with INSTALLATOR. It was splitted in four separate files:
- INSTALLATION_1 describes the assisted installation procedure
- INSTALLATION_2 describes user customizations
- INSTALLATION_3 describes the Request for License procedure
- INSTALLATION_4 describes the manual installation procedure
Installator was updated to take advantage of these conventions.
For backward compatibility (especially with the manual pages),
a symbolic link INSTALLATION pointing to INSTALLATION_2 was
created.
Number: 517
Date: Tue Sep 16 13:44:59 MET DST 1997
Report: Charles Pecheur (INRIA/VASY)
Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files: com/bcg_info
Nature: The "bcg_info" shell-script was modified so as to avoid the
creation of a (sometimes huge) temporary file in /tmp. The
modified version uses pipes instead.
Number: 518
Date: Tue Sep 16 14:22:18 MET DST 1997
Report: Ghassan Chehaibar (BULL/DYADE)
Author: Laurent Mounier (VERIMAG)
Files: man/manl/des2aut.l
Nature: The manual page for Des2Aut was updated: the new page specifies
that gate names are case-sensitive, adds a missing rule:
<behaviour> ::= '('<behaviour>')'
and adds a missing comma in the non-terminal <gate-list>.
Number: 519
Date: Tue Sep 16 15:14:12 MET DST 1997
Report: Ghassan Chehaibar (BULL/DYADE)
Author: Laurent Mounier (VERIMAG)
Files: com/exp.open
Nature: In some cases, the "exp.open" shell-script did not work under
Solaris 2.* (due to a non-standard behaviour of the "basename"
command in Solaris 2.*). This problem has been fixed both for
Solaris 1.* and Solaris 2.*.
Number: 520
Date: Thu Sep 18 16:29:26 MET DST 1997
Authors: David Jacquemin, Mark Jorgensen and Hubert Garavel (INRIA/VASY)
Files: bin.*/exp2fc2, man/manl/exp2fc2.l,
src/eucalyptus/eucalyptus.tcl, src/eucalyptus/com/xeuca_fc2info
Nature: A new tool named "exp2fc2" was added to the CADP toolbox.
This tool translates an ".exp" file into an FC2 file describing
a set of communicating processes. This allows to apply the
FC2 tools to an ".exp" file. A manual page was written for
this new tool ("man exp2fc2"). The EUCALYPTUS graphical
interface was modified accordingly.
Number: 521
Date: Tue Sep 23 18:08:58 MET DST 1997
Author: Hubert Garavel (INRIA/VASY)
Files: src/open_caesar/generator.c, src/open_caesar/reductor.c
Nature: The source code of Generator and Reductor was modified to
avoid the use of the non-POSIX signal SIGSYS, which does not
exist in Linux.
Number: 522
Date: Wed Sep 24 17:24:30 MET DST 1997
Authors: Khalid Laksiouar (INRIA/MEIJE), Mark Jorgensen and
Hubert Garavel (INRIA/VASY)
Files: com/fc2open, man/manl/fc2open.l, man/manl/*or.l
src/eucalyptus/eucalyptus.tcl,
Nature: A new tool, named FC2OPEN, was added to the CADP toolbox and
to the FC2Tools toolbox developed in the MEIJE project of
INRIA Sophia-Antipolis. This new tool allows to apply all
OPEN/CAESAR tools to FC2 files, either the FC2 files that
represent sequential automata, or the FC2 files that describe
networks of parallel processes.
For technical reasons, the FC2OPEN tool is splitted between
the CADP and FC2Tools toolboxes, and requires both toolboxes
to function. The other part of FC2OPEN is a binary program
named "fc2open2c", which will be shipped with version 1.2
and higher of FC2Tools. The environment variable $FC2DIR
should be set and point to the directory where the FC2Tools
are installed.
A manual page was written for this new tool ("man fc2open").
The manual pages of all OPEN/CAESAR tools (e.g., terminator,
executor, etc.) were updated to mention the possibility of
using FC2OPEN.
The EUCALYPTUS graphical interface was modified accordingly.
If the $FC2DIR variable is not set, EUCALYPTUS will not use
the "fc2open" tool, and will try instead to convert the FC2
file into a BCG file, which will only work if the FC2 file
represents a sequential automaton.
Number: 523
Date: Thu Oct 2 10:50:24 MET 1997
Authors: Mark Jorgensen (INRIA/VASY), Hubert Garavel (INRIA/VASY),
Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran, bin.*/exp2c, bin.*/exp2fc2,
bin.*/libexpopen.a, man/manl/aldebaran.l
Nature: The ".exp" format has been extended. Previously, the LTSs
composing the network (i.e., the leaves of the composition
expression) had to be ".aut" files. The new version also
allows these LTSs to be encoded in other formats, e.g. BCG,
FC2, SEQUENCE, etc. This is done by invoking the BCG_IO tool
to perform the appropriate conversions. The definition of
the ".exp" format (type "man aldebaran") was updated. All
tools that accept ".exp" files as input (ALDEBARAN, EXP2C,
EXP2FC2) have been subsequently modified.
Number: 524
Date: Mon Oct 6 16:37:34 MET DST 1997
Report: Mark Jorgensen (INRIA/VASY)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: A bug was fixed, which caused "aldebaran -info" to core dump
when applied to ".exp" files.
Number: 525
Date: Mon Oct 6 18:08:02 MET DST 1997
Author: Hubert Garavel (INRIA/VASY)
Files: usr
Nature: Following the results of the technical enquiry conducted in
the CADP Newsletter #3 (September 1997), the "usr" directory
was removed from the CADP distribution. Indeed:
- The "pre" and "post" programs for interfacing the SEDOS
toolkit with CADP are now useless, because the SEDOS simulator
HIPPO is no longer maintained nor distributed.
- The "deadlock" program for finding deadlocks in ".aut" files
can now be replaced by a joint use of BCG_OPEN and EXHIBITOR,
or the "-dead" option of ALDEBARAN.
This makes the CADP release 850 kbytes leaner. The contents of
the "usr" directory can still be obtained by sending a request
to "caesar@imag.fr". However, the "pre", "post", and "deadlock"
programs will no longer be maintained, nor ported to other
architectures / operating systems.
Number: 526
Date: Tue Oct 7 12:26:26 MET DST 1997
Author: Charles Pecheur (INRIA/VASY)
Files: doc/Pecheur-97.ps, doc/:READ_ME
Nature: A new publication entitled "Specification and Verification of
the CO4 Distributed Knowledge System Using LOTOS" was added
to the CADP release.
Number: 527
Date: Thu Oct 23 17:51:39 MET DST 1997
Report: Ghassan Chehaibar (BULL/DYADE)
Author: Mark Jorgensen (INRIA/VASY)
Files: tcl-tk/bin.*/duplex
Nature: A bug was fixed, which caused the graphical user-interface
EUCALYPTUS to block when the output of some commands was
too long.
Number: 528
Date: Fri Oct 24 12:10:19 MET DST 1997
Report: Charles Pecheur (INRIA/VASY)
Author: Mark Jorgensen (INRIA/VASY)
Files: src/installator/*
Nature: Several bug fixes and improvements have been made in the
Installator program:
- Installator would block if $CADP_TMP was set to the current
directory ("."). This problem was fixed
- For a first-time installation, Installator will propose
"./cadp" as the default directory for installing CADP
- Installator now checks the type of Unix to invoke the "df"
command with appropriate options
- When the untar/uncompress operation is done, a beep is
produced to wake up the user
- When the RFL is done, a beep is also produced
Number: 529
Date: Tue Oct 28 16:49:14 MET 1997
Authors: Bruno Vivien, Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files: bin.*/caesar.indent, man/manl/caesar.indent.l, src/eucalyptus/*
Nature: A LOTOS pretty-printer named "caesar.indent" has been added
to the CADP toolset. This pretty-printer was developed with
the PARADIS tool of the SYNTAX compiler generator (SYNTAX is
a registered trademark of INRIA).
A manual page is available (type "man caesar.indent"). This
pretty-printer is accessible from the EUCALYPTUS graphical
interface by clicking on a ".lotos" file and selecting the
"More" / "Indent" menu.
Number: 530
Date: Tue Oct 28 19:23:09 MET 1997
Report: Charles Pecheur (INRIA/VASY)
Author: Radu Mateescu (INRIA/VASY)
Files: bin.sun*/xtl_expand
Nature: A bug was fixed in the XTL expander, which caused, in certain
cases, to erroneously detect and signal recursion between macro
definitions.
Number: 531
Date: Tue Oct 28 19:23:09 MET 1997
Author: Radu Mateescu (INRIA/VASY)
Files: bin.sun*/xtl
Nature: Several bugs were corrected in the XTL tool, concerning bad
code generation for Sun4 machines. Also, a small typing error
in the "xtl" manual page has been corrected.
Number: 532
Date: Tue Oct 28 19:23:09 MET 1997
Author: Radu Mateescu (INRIA/VASY)
Files: src/xtl/ltac.xtl
Nature: The definition of "FAIR (A, B)" (which is the action-based
version of the "FAIR" operator defined by Queille and Sifakis)
was corrected.
Number: 533
Date: Tue Oct 28 20:52:21 MET 1997
Report: Fabio Paterno (CNUCE-CNR, Pisa, Italy)
Authors: Radu Mateescu and Hubert Garavel (INRIA/VASY)
Files: bin.*/xtl
Nature: The XTL compiler was modified to use always the $CADP/com/arch
command (instead of the /bin/arch command that exists under
Solaris). This solves a potential problem occurring when
CADP users do not configure their $PATH variable properly.
Number: 534
Date: Fri Oct 31 17:48:34 MET 1997
Authors: Charles Pecheur (INRIA/VASY)
Files: demos/demo_24
Nature: A new demonstration example was added to the CADP release:
the CO4 protocol for distributed knowledge bases.
Number: 535
Date: Fri Nov 7 12:42:43 MET 1997
Report: Fabio Paterno and Carmen Santoro (CNUCE-CNR, Pisa, Italy)
Authors: Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files: installator.shar
Nature: The self-extracting program "installator.shar" was updated
to detect if another Installator is already running, or if
a previous execution of Installator crashed without cleaning
up.
Number: 536
Date: Mon Dec 1 18:40:48 MET 1997
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar, man/manl/caesar.l, src/eucalyptus/eucalyptus.tcl
Nature: CAESAR was modified to avoid unecessary recompilations when
given either the "-open" option (OPEN/CAESAR mode) or the
"-exec" option (EXEC/CAESAR mode). Precisely, CAESAR will not
regenerate "filename.c" if this file already exists in the
current directory and if it has been modified more recently:
- than the corresponding LOTOS file ("filename.lotos",
"filename.lot", or "filename.l"),
- than any LOTOS library transitively included (using the
"library" clause) in this LOTOS file,
- and than any C file transitively included (using the
"#include" clause) in "filename.c" itself.
The CAESAR manual page was updated accordingly. The EUCALYPTUS
user interface was modified to give access to "-force" option.
Number: 537
Date: Mon Dec 1 18:47:44 MET 1997
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar.adt, man/manl/caesar.adt.l,
src/eucalyptus/eucalyptus.tcl
Nature: CAESAR.ADT was modified to avoid unecessary recompilations.
Precisely, CAESAR.ADT will not regenerate "filename.h" if
this file already exists in the current directory and if it
has been modified more recently:
- than the corresponding LOTOS file ("filename.lotos",
"filename.lot", or "filename.l"),
- than any LOTOS library transitively included (using the
"library" clause) in this LOTOS file,
- than any C file transitively included (using the
"#include" clause) in "filename.h" itself.
- than the file named "filename.t" if this file exists in
the current directory,
- and than the file named "filename.f" if this file exists
in the current directory.
The CAESAR.ADT manual page was updated accordingly. The
EUCALYPTUS user interface was modified to give access to
"-force" option.
Number: 538
Date: Tue Dec 2 13:07:32 MET 1997
Author: Mark Jorgensen (INRIA/VASY)
Files: com/xeuca, src/eucalyptus/*
Nature: Following the results of the Technical Enquiry that was
enclosed in the CADP Newsletter #3, the TESTGEN and TETRA
tools are no longer integrated within the EUCALYPTUS graphical
user interface.
Number: 539
Date: Tue Dec 2 16:29:43 MET 1997
Author: Hubert Garavel (INRIA/VASY)
Files: com/caesar.open
Nature: The "caesar.open" shell-script was entirely rewritten in order
to take advantage of the recent improvements in CAESAR and
CAESAR.ADT (see above items #536 and 537). The new solution
has several benefits:
- The previous version of "caesar.open" tried to optimize
CPU time by avoiding recompilations. However, the dependency
analysis was approximate, so that object files could be,
in some cases, reused incorrectly. From now on, the
dependency analysis is accurate. This bug fix is similar
to bug fix #510 for "bcg_open" and "exp.open".
- "caesar.open" no longer relies upon the generation of a
Makefile. It is faster, more portable, and allows to handle
properly the cases where input filenames (".lotos", ".c",
".a", or ".o") contain special characters (e.g., semicolons)
not allowed in Makefiles. In the previous version of
"caesar.open", for instance, filenames containing semicolons
generated the following error message:
make: Fatal error in reader: /tmp/caesar.open.makefile.29719,
line 24: Extra `:', `::', or `:=' on dependency line
- The new version of "caesar.open" is much closer to the
other similar shell-scripts ("bcg_open", "exp.open", and
"fc2open"), which could enable (in the future) to merge
all these scripts into a single one.
Number: 540
Date: Tue Dec 2 17:27:05 MET 1997
Author: Charles Pecheur (INRIA/VASY)
Files: src/xtl/actl.xtl
Nature: The definition in XTL of the "AU_A_B" operator of the ACTL
temporal logic was incorrect. It has been fixed.
Number: 541
Date: Tue Dec 16 15:41:49 MET 1997
Report: Marc Herbert (LIP-LHPC, Lyon, France)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.sun5/*
Nature: Two problems have been fixed, which would create core dumps
and/or SIGALRM signals if the duration specified in the LICENSE
file was less than one month.
Number: 542
Date: Thu Dec 18 15:25:37 MET 1997
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar
Nature: A bug was fixed, which would cause CAESAR 5.2 to core dump
when the "-graph" option was used.
Number: 543
Date: Fri Jan 16 20:54:14 MET 1998
Report: Mark Jorgensen (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar
Nature: A bug was fixed, which caused CAESAR to generate illegal
C code under Linux, leading to the following error message
from the C compiler:
/tmp/caesar_xxx.c: In function `CAESAR_STANDARD_LOOP':
/tmp/caesar_xxx.c: parse error before character 0204
Number: 544
Date: Wed Jan 28 16:17:29 MET 1998
Report: Ghassan Chehaibar (BULL/DYADE)
Author: Hubert Garavel (INRIA/VASY)
Files: src/eucalyptus/eucalyptus.tcl
Nature: A bug was fixed in the EUCALYPTUS user-interface: by default,
CAESAR, CAESAR.ADT, and CAESAR.OPEN were always invoked with
option "-warning" (thus preventing warnings from being
displayed), even if warnings were selected in the Options menu.
Number: 545
Date: Wed Feb 4 18:27:56 MET 1998
Author: Hubert Garavel (INRIA/VASY)
Files: doc/Garavel-98, doc/:READ_ME, doc/biblio.bib
Nature: A new publication entitled "OPEN/CAESAR: An Open Software
Architecture for Verification, Simulation, and Testing"
was added to the CADP release. This report provides an
introduction and overview of the OPEN/CAESAR environment.
Number: 546
Date: Fri Feb 13 15:48:14 MET 1998
Report: Charles Pecheur (INRIA/VASY)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/exp2c, bin.*/libexpopen.a
Nature: A bug was fixed, which caused Exp.Open to behave incorrectly
on ".exp" files containing several instances of the same
".aut" file, e.g.:
cell ||| cell ||| cell
Number: 547
Date: Fri Feb 13 15:52:51 MET 1998
Report: Axel Belinfante (Univ. of Twente, The Netherlands),
Zoltan Meggyesi (CERN, Geneva, Switzerland)
Author: Hubert Garavel (INRIA/VASY)
Files: installator.shar packages
Nature: The "installator.shar" self-extracting archives were modified
in order to avoid a problem for users which invoke the GNU
"gettext" command instead of the Solaris "/bin/gettext" one:
under these circumstances, the "-beta" option was not taken
into account by Installator. This problem is now solved.
Number: 548
Date: Wed Feb 18 17:11:33 MET 1998
Author: Marius Bozga (VERIMAG)
Files: bin.*/evaluator.a
Nature: Diagnostic sequences are now computed for both evaluation
strategies (i.e., the "local" one and the "global" one).
This feature did not exist in the previous version for the
global evaluation strategy.
Number: 549
Date: Wed Feb 18 17:20:23 MET 1998
Report: Ghassan Chehaibar (Bull)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: A bug was fixed in the algorithm used in ALDEBARAN
for deciding on-the-fly if two LTSs are branching bisimilar
(the "-fly -pequ" options were concerned).
Number: 550
Date: Wed Feb 18 17:26:14 MET 1998
Report: Hubert Garavel (INRIA/VASY)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/exp2c, bin.*/libexpopen.a
Nature: The length of the filenames that can be used in a .exp
file has been augmented up to 128 characters. The previous
limitation was not always sufficient for handling the .exp
files generated by DES2AUT (for instance in demo_20).
Number: 551
Date: Mon Feb 23 10:29:14 MET 1998
Author: Charles Pecheur (INRIA/VASY)
Files: src/xtl/misc.xtl, src/xtl/walk.xtl, src/xtl/walk_actl.xtl,
src/xtl/walk_print_nice.xtl
Nature: New XTL libraries have been added, which provide detailed
diagnostics (annotated execution sequences) justifying the
result of the evaluation of CTL and ACTL temporal logic
formulas.
Number: 552
Date: Mon Feb 23 10:30:14 MET 1998
Author: Charles Pecheur (INRIA/VASY)
Files: demos/demo_25
Nature: A new demo was added: it deals with the verification of
a CFS (Cluster File System) using CAESAR, ALDEBARAN,
EXP.OPEN and XTL.
Number: 553
Date: Mon Feb 23 10:14:35 MET 1998
Report: Mark Jorgensen (INRIA/VASY)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/projector.a
Nature: A minor bug, which prevented projector to generate BCG files,
has been corrected.
Number: 554
Date: Mon Feb 23 16:10:47 MET 1998
Report: Ghassan Chehaibar (Bull)
Author: Jean-Pierre Krimm (VERIMAG)
Files: bin.*/des2aut
Nature: The preliminary phase of des2aut (i.e., hidden gate
distribution over parallel compositions) was erroneous
in some cases. This problem has been corrected.
Number: 555
Date: Tue Feb 24 19:04:22 MET 1998
Report: Hubert Garavel (INRIA/VASY)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: The diagnostic sequences generated by aldebaran from the
two LTSs under comparison were improperly swapped in
some cases when using the ``-fly'' options. This problem
has been corrected.
Number: 556
Date: Mon Mar 2 19:37:53 MET 1998
Report: Charles Pecheur (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar
Nature: A bug was fixed in CAESAR, which could cause (in some cases)
the generation of incorrect LTSs (especially, LTSs with too
many transitions). This bug occured because CAESAR tried to
optimize a given variable by turning it both into a constant
and a register (local variable) at the same time.
Number: 557
Date: Tue Mar 3 15:27:59 MET 1998
Author: Hubert Garavel (INRIA/VASY)
Files: demos/demo_15/:READ_ME, demos/demo_15/verify-all-requirements
Nature: The demo_15 was improved in order:
- to use BCG files directly (instead of generating .aut
files first and then translating them to .bcg files)
- to avoid a meaningless error message
Number: 558
Date: Mon Mar 9 11:40:31 MET 1998
Author: Hubert Garavel (INRIA/VASY)
Files: com/bcg_info, bin.sun*/lib_bcg_info.a, man/manl/bcg_info.l,
src/eucalyptus/eucalyptus.tcl
Nature: An official "bcg_info" tool was introduced in the CADP
release. This new tool replaces the previous undocumented
versions of "bcg_info". A manual page is provided, which
is available through the Help button of the EUCALYPTUS
graphical user-interface.
Number: 559
Date: Wed Mar 11 14:21:47 MET 1998
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCGI_IO.a, bin.*/bcg_io
Nature: A bug was fixed, which caused "bcg_io" to core dump on
Solaris 2, when given the "-squiggles" option.
Number: 560
Date: Mon Mar 16 12:33:57 MET 1998
Report: Judi Romijn (CWI, The Netherlands)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a, man/manl/bcg_write.l, man/manl/bcg_read.l
incl/bcg_transition.h, incl/bcg_edges.h, incl/bcg_user.h,
Nature: An API (programming interface) to read BCG graphs was made
available and documented (see "man bcg_read" for details).
Also, the "bcg_write" man page was enhanced with an example.
Number: 561
Date: Tue Mar 17 11:28:46 MET 1998
Author: Hubert Garavel (INRIA/VASY)
Files: com/caesar.aldebaran
Nature: The "caesar.aldebaran" shell-script was modified in order to
invoke "caesar" with option "-more /bin/cat". This avoids a
deadlock in the EUCALYPTUS user interface.
Number: 562
Date: Tue Apr 14 10:50:27 MET DST 1998
Report: Elie Najm (ENST, Paris)
Author: Hubert Garavel (INRIA/VASY)
Files: installator.shar
Nature: The directory "/usr/openwin/lib" was added to $LD_LIBRARY_PATH
in order to have proper dynamic libraries under Solaris 2.*
Number: 563
Date: Tue Apr 14 11:25:12 MET DST 1998
Report: Laurence Pierre (Universite de Marseille and TIMA)
Author: Hubert Garavel
Files: com/installator, installator.shar
Nature: A bug was fixed, which would (under some circumstances) cause
an error message of the form: "error in Tcl script : can't
read env(LOGNAME) no such element in array".
Number: 564
Date: Tue Apr 14 19:23:28 MET DST 1998
Report: Bruno Hondelatte and Pierre Kessler (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar, bin.*/caesar.adt
Nature: A minor bug was fixed, which could cause CAESAR.ADT and CAESAR
to emit a "Broken Pipe" message under some circumstances
(this message was annoying, but harmless).
Number: 565
Date: Tue Apr 14 19:55:25 MET DST 1998
Report: Jacques Sincennes (University of Ottawa)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.sun4/caesar, bin.sun4/caesar.adt, bin.*/libcaesar.a
Nature: A bug was fixed, which could cause CAESAR.ADT and CAESAR
to emit the following error messages under SunOS 1.* machines:
/usr/local/gnu/lib/gcc-lib/sparc/2.7.2/include/netinet/in.h:106:
parse error before `u_char'
/usr/local/gnu/lib/gcc-lib/sparc/2.7.2/include/netinet/in.h:107:
parse error before `u_short'
Number: 566 Date: Wed Apr 15 22:29:37 MET DST 1998 Report: Charles Pecheur (INRIA/VASY) Author: Radu Mateescu (INRIA/VASY) Files: XTL Nature: Two minor bugs in XTL 1.1 have been fixed.
Number: 567
Date: Wed Apr 15 23:40:03 MET DST 1998
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: BCG
Nature: A bug was fixed in the low layers of the BCG library, which
caused some BCG tools and XTL to core dump under Linux. This
bug was not visible for Solaris users.
Number: 568
Date: Thu Apr 16 17:47:15 MET DST 1998
Author: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: BCG
Nature: Subtle changes have been made in the BCG libraries and
include files in order to ensure portability of the BCG files
across various architectures. This means that BCG files should
independent from the processor/architecture, so that they can
be created and read identically under SunOS, Solaris, and
Linux environments.
These changes are upward compatible and should be almost
invisible to the user.
BCG files generated with any previous version of CADP on
Solaris are still valid and can be reused without change.
However, BCG files generated with beta-versions 97b-* of
CADP on Linux are invalid: they should be destroyed and
generated again with the latest version of CADP.
Number: 569
Date: Fri Apr 17 12:46:34 MET DST 1998
Report: Charles Pecheur (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: BCG,
man/manl/bcg_write.l, man/manl/bcg_io.l, man/manl/xtl.l,
demo_01/:READ_ME, demo_02/:READ_ME, demo_13/*.bcg,
demo_16/:READ_ME, demo_21/Makefile, demo_22/Makefile,
demo_23/Makefile, demo_25/Makefile,
src/eucalyptus.tcl
Nature: The "bcg_write" API (Application Programming Interface) has
been improved. The interface itself (see "man bcg_write.l")
remains unchanged, however, its effects are different.
From now on, all the character strings passed to function
BCG_IO_WRITE_BCG_EDGE() are parsed in order to infer the
structure and contents of the labels, so that the generated
BCG files should contain more precise type information.
The rules for label parsing are described in a section
(entitled "Technical Note on Label Parsing") of the
"bcg_write.l" manual page.
As a consequence, the contents of the BCG graphs produced
using the "bcg_write" API will be slightly different from
those generated with previous versions of CADP. In most
cases, the difference should not be visible by the user
(see the "bcg_write.l" manual page for a discussion about
label normalization).
Because this change is done in the BCG library, it applies
to all the CADP tools that generate BCG files, including
CAESAR, ALDEBARAN, BCG_IO, Generator, Reductor, etc.
As regards BCG_IO: the previous version of BCG_IO would
not perform label parsing unless when reading an ".aut"
file with the "-parse" option selected. From now on, the
behaviour is reversed: label parsing will be the default
behaviour, except when reading an ".aut" file with the
"-parse" option selected.
The EUCALYPTUS graphical interface and the demos using
XTL have been updated not to use the "-parse" option
any longer.
Label parsing is especially of interest when using the XTL
model-checker, which allows to take advantage of the types
and typed values defined in BCG files. This improvement
will allow to use consistently the XTL model-checker on
all the BCG files generated by CADP tools.
Note: the BCG files generated with previous versions of CADP
should be re-generated for a proper use of XTL, except if
they were produced from a ".aut" file using the previous
version of BCG_IO with the "-parse" selected. An old BCG
file, say FILE.bcg, can be upgraded to a new one using the
following sequence of commands:
bcg_io FILE.bcg FILE.aut
rm FILE.bcg FILE@1.o
bcg_io FILE.aut FILE.bcg
Number: 570
Date: Mon Apr 20 20:40:58 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: src/eucalyptus/eucalyptus.tcl
Nature: The EUCALYPTUS Graphical Interface was improved:
- by providing the "Indent" command for ".lib" files
- by setting the "-monitor" option active by default for
the Generator tool.
Number: 571
Date: Tue Apr 21 14:25:35 MET DST 1998
Report: Massimo Zendri (Bull/DYADE)
Authors: Charles Pecheur and Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar
Nature: For very large descriptions (e.g., about 20 processes in
parallel), CAESAR could signal a deadlock in states from
which transitions could actually be fired. This bug was
caused by the overflow of an integer variable, declared
as an "unsigned short", although its value could go beyond
65,536. This bug was fixed.
Number: 572
Date: Thu May 7 19:21:37 MET DST 1998
Authors: Christophe Discours and Hubert Garavel (INRIA/VASY)
Files: bin.*/libcaesar.a, bin.*/exhibitor.a,
incl/caesar_regexp.h, incl/caesar_hide_1.h,
incl/caesar_rename_1.h.
Nature: The OPEN/CAESAR library was enriched with three new libraries:
"caesar_regexp", "caesar_hide_1", and "caesar_rename_1".
These libraries offer high-level support for handling regular
expressions, hiding labels and renaming labels.
The Exhibitor tool was modified to take advantage of these
new librairies.
Number: 573
Date: Fri May 15 10:11:48 MET DST 1998
Authors: Hubert Garavel, Charles Pecheur, and Mihaela
Sighireanu (INRIA/VASY)
Files: doc/garavel-Sighireanu-98a.ps, doc/Pecheur-98.ps, doc/:READ_ME
Nature: Two new papers, entitled "Advanced Modelling and Verification
Techniques Applied to a Cluster File System" and "Towards a
Second Generation of Formal Description Techniques -- Rationale
for the Design of E-LOTOS", were added to the CADP release.
Number: 574
Date: Sat May 16 14:19:06 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_io
Nature: A bug was fixed, which would cause (in a few cases) BCG_IO
to stop with an error message of the form: "wrong number of
parameters".
Number: 575
Date: Sat May 16 16:37:20 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_io
Nature: The translation algorithm used by the BCG_IO tool to read
automata encoded in the FC2 automata and to translate them
into other formats was extended, so as to accept FC2 files
in which the initial state is not specified (i.e., when
there is no "initial>" directive. Such FC2 files can be
generated using the Autograph/Atg tool. The previous version
of BCG_IO would "core dump" on such incomplete FC2 files.
The new version of BCG_IO assumes that, if the initial state
is not specified, then state 0 is the initial state.
Number: 576
Date: Thu May 28 13:03:26 MET DST 1998
Report: Radu Mateescu (CWI/SEN2)
Author: Hubert Garavel (INRIA/VASY)
Files: src/eucalyptus.tcl
Nature: A bug was fixed in the EUCALYPTUS Graphical User Interface,
which caused XTL to be improperly invoked when the $CADP_CC
environment variable was set to a complex string such as
"gcc -I/usr/include".
Number: 577
Date: Thu Jun 4 12:29:19 MET DST 1998
Report: Axel Belinfante (Univ. of Twente), Elie Najm (ENST, Paris)
Author: Hubert Garavel (INRIA/VASY)
Files: com/rfl
Nature: The old version of RFL would stop as soon as an invalid host
was detected. The new version will try all hosts, and print
the list of invalid hosts (if any) before stopping
Number: 578
Date: Thu Jun 4 17:39:45 MET DST 1998
Report: Axel Belinfante (Univ. of Twente)
Author: Hubert Garavel (INRIA/VASY)
Files: src/installator/run_mail, installator.shar
Nature: From now on, Installator will also send a copy of the LICENSE
file to the person that is running Installator, so that
Installator users are aware of the results of the RFL. This
will also help to detect situations in which the "mail"
command does not work properly.
Number: 579
Date: Fri Jun 5 10:28:00 MET DST 1998
Report: Axel Belinfante (Univ. of Twente)
Authors: Hubert Garavel and Pierre Kessler (INRIA/VASY)
Files: src/eucalyptus/eucalyptus.tcl, src/eucalyptus/com/xeuca_ps
Nature: Various problems have been fixed in the "Kill Window" of
EUCALYPTUS:
- When resizing the Kill window, the subwindow listing the
processes did not resize as well. This is now the case,
so that the user can display more information about
processes to kill.
- An error message of the form:
"ps: no controlling terminal
while executing
"exec ps | tail +2"
invoked from within ...
could be printed on Solaris 2.* when clicking on the Kill
button if "/bin" was before "/usr/ucb" in the $PATH variable.
This problem is now solved.
- The Kill window did not display processes without a
controlling terminal. This problem is now solved.
Number: 580
Date: Fri Jun 12 09:58:47 MET DST 1998
Authors: (many)
Files: doc/Mateescu-Garavel-98.ps, doc/Kahlouche-Viho-Zendri-98.ps
doc/Mateescu-98-b.ps
Nature: Three new papers have been added, that present the XTL and
TGV-LOTOS tools.
Number: 581
Date: Fri Aug 14 17:48:32 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: man/manl/caesar_hide_1.l, man/manl/caesar_rename_1.l,
doc/Garavel-92-a.ps, man/manl/aldebaran.l,
src/eucalyptus/eucalyptus.tcl,
Nature: The manual pages for the new OPEN/CAESAR libraries
"caesar_hide_1" and "caesar_rename_1" have been added.
The OPEN/CAESAR Reference Manual was updated accordingly.
The ALDEBARAN User Manual was updated to refer the new manual
pages "caesar_hide_1" and "caesar_rename_1", which give an
accurate description of the formats for hiding and renaming
files.
The Help window of the EUCALYPTUS graphical interface was
similarly updated to refer the new manual pages "caesar_hide_1"
and "caesar_rename_1".
Number: 582
Date: Fri Aug 14 17:48:58 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: man/manl/caesar_table_1.l, man/manl/caesar_version.l,
doc/Garavel-92-a.ps
Nature: The documentation of the following functions:
CAESAR_SEARCH_TABLE_1()
CAESAR_SEARCH_AND_PUT_TABLE_1()
CAESAR_COMPARE_VERSION()
CAESAR_MATCH_VERSION()
was improved and made more precise. For these functions that
return a boolean result of type CAESAR_TYPE_BOOLEAN, the text
fragments "a result different from 0" and "a result equal to 0"
have been replaced by "CAESAR_TRUE" and "CAESAR_FALSE",
respectively.
Note: this change is totally upward compatible. No modification
of existing OPEN/CAESAR applications is needed.
Number: 583
Date: Fri Aug 14 19:45:58 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: com/bcg_info, bin.*/libbcg_info.a, man/manl/bcg_info.l
Nature: A new option ('-size') was added to the BCG_INFO tool, that
displays the size of a BCG graph (number of states and edges)
under a single line.
Number: 584
Date: Fri Aug 14 19:49:35 MET DST 1998
Authors: Mihaela Sighireanu (INRIA/VASY) and Ken Turner (Univ. of
Stirling, Scotland)
Files: demos/demo_26
Nature: A new demo (formal verification of a example of enterprise
information systems) was added to the CADP distribution.
Number: 585
Date: Mon Aug 17 11:58:47 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: com/caesar.aldebaran
Nature: The "caesar.aldebaran" command was extended so as to handle
".bcg" files as well as ".aut" files.
Number: 586
Date: Tue Aug 18 15:00:04 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: demo_18/transit_node.exp
Nature: The ".exp" file contained in demo_18 was syntactically
incorrect, which resulted in an error message of the form:
exp.open: Generating transit_node.c ...
exp2c: syntax error !
*** Error code 1
This ".exp" file (which was indeed a ".des" file, suitable
for DES2AUT but not EXP.OPEN) was replaced with a correct one.
Number: 587
Date: Wed Aug 19 12:05:17 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: demos/*
Nature: All the demo exemples have been revisited and improved in
several respects. The READ_ME files have been updated and
the commands have been simplified to take advantage of the
most recent features in CADP.
Number: 588
Date: Wed Aug 19 12:18:50 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: */:READ_ME
Nature: All the files previously named ':READ_ME' have been renamed
either into 'READ_ME' or into '=READ_ME.txt', because the
':' character cannot be part of file names under Windows.
This would create problems for people attempting to download
the demo examples from the VASY FTP server.
Number: 589
Date: Tue Aug 25 18:00:05 MET DST 1998
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a, bin.*/libBCG_IO.a
Nature: A bug was fixed, which caused the BCG library to issue an
error message of the form:
bcg_write_1: wrong natural size in BCG_WRITE_UNSIGNED
when attempting to generate a graph with only one label and
with label parsing activated (which is now the case by default,
see "man bcg_write" for details).
Number: 590
Date: Wed Aug 26 11:58:16 MET DST 1998
Report: Christophe Discours (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_io
Nature: A minor bug was fixed, which caused BCG_IO to issue an error
message of the form:
bcg_file_area: area is missing file in BCG_COPY_AREA
when invoked with the same BCG file as input and output
argument, e.g.:
bcg_io FILE.bcg FILE.bcg
Number: 591
Date: Thu Aug 27 13:04:58 MET DST 1998
Report: Charles Pecheur (INRIA/VASY)
Authors: Christophe Discours and Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_labels, man/manl/bcg_labels.l, demo_25
Nature: A new tool named BCG_LABELS was introduced. This tool allows
to perform an arbitrary combination of hiding and renaming
operations on the labels of a BCG graph. See the "bcg_labels"
manual page for more information.
The demo_25 was simplified in order to take advantage of this
new tool.
The EUCALYPTUS graphical user-interface was updated to allow
access to the BCG_LABELS tool: when clicking on an LTS file
(in BCG or .aut format), two new commands "Hide Labels..."
and "Rename Labels..." are now available.
Number: 592
Date: Mon Aug 31 15:38:15 MET DST 1998
Report: Guy Tremblay (Universite du Quebec a Montreal, Quebec, Canada)
Author: Hubert Garavel (INRIA/VASY)
Files: com/rfl
Nature: The RFL command was modified to make it independent from
the value of the LC_TYPE environment variable.
Number: 593
Date: Wed Sep 30 13:56:25 MET DST 1998
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/xtl
Nature: A minor bug was fixed, concerning the printing of messages
by xtl when called with the -verbose option (when the tool
was called from the xeuca interface, the results of temporal
formula evaluation were printed before the informative messages
issued by the xtl tool).
Number: 594
Date: Fri Nov 20 18:35:56 MET 1998
Report: Ji He (University of Stirling, Dept. of Computing and Maths)
Author: Radu Mateescu (INRIA/VASY)
Files: man/manl/xtl.l
Nature: A minor mistake in the XTL manual was corrected, namely the
translations of the "forall" and "exists" constructs in terms
of the "for" expression were permuted.
Number: 595 Date: Wed Jan 20 16:12:54 MET 1999 Author: Mihaela Sighireanu (INRIA/VASY) Files: doc/Sighireanu-Turner-98.ps, doc/Kahlouche-Viho-Zendri-99.ps Nature: Two new papers have been added in the doc directory.
Number: 596
Date: Mon Jan 25 18:28:13 MET 1999
Report: Patricia Bournai (IRISA)
Author: Hubert Garavel (INRIA/VASY)
File: com/rfl
Nature: The bug fix #592 (see above) was not sufficient. A different
fix has been implemented.
Number: 597
Date: Mon Jan 25 19:45:01 MET 1999
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/libcaesar.a, man/manl/caesar_hide_1.l,
doc/Garavel-92-a.ps, incl/caesar_hide_1.h, incl/caesar_regexp.h
Nature: The "caesar_hide_1" library has been extended to allow
hiding based on "gate matching". This new functionality
emulates the hiding operator of LOTOS.
To do so, the last parameter of function CAESAR_CREATE_HIDE_1()
has been modified. Previously, it was a parameter named
CAESAR_PARTIAL_MATCH of type CAESAR_TYPE_BOOLEAN. From now
on, it is named CAESAR_KIND and is of type CAESAR_TYPE_NATURAL.
The "gate matching" facility can be obtained by giving
the value 2 to the last parameter CAESAR_KIND of function
CAESAR_CREATE_HIDE_1 ().
This change requires a slight modification of existing code:
in any call to function CAESAR_CREATE_HIDE_1(), the value of
the last parameter should be replaced: CAESAR_FALSE should be
replaced with 0, CAESAR_TRUE should be replaced with 1.
Number: 598
Date: Tue Jan 26 10:12:23 MET 1999
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/libcaesar.a, man/manl/caesar_rename_1.l,
doc/Garavel-92-a.ps
Nature: The "caesar_rename_1" library has been extended to allow
renaming based on "gate matching". This new functionality
emulates the renaming operator that exist in modern formal
description techniques such as E-LOTOS and LOTOS NT.
The "gate matching" facility can be obtained by giving
the value 3 to the last parameter CAESAR_KIND of function
CAESAR_CREATE_RENAME_1 ().
This change is totally upward compatible: existing code does
not need to be modified.
Number: 599
Date: Wed Jan 27 10:59:12 MET 1999
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_labels, man/manl/bcg_labels.l
Nature: The BCG_LABELS command has been extended to incorporate the
recently introduced "gate matching" facilities (see #597 and
#598 above). It is now possible to write:
bcg_labels -hide -gate FILE.hid ...
and/or
bcg_labels -rename -gate FILE.ren ...
The manual page has been updated.
VERSION 97b "Liege"
Back to the CADP Home Page