|
| 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 |
|
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.
Listen to the CADP 2001 "Ottawa" release sound
The VASY team of INRIA Rhone-Alpes is pleased to announce the availability of a new release of the CADP protocol engineering toolbox, which includes contributions from the VERIMAG laboratory, the PAMPA team of INRIA Rennes/IRISA, and the FMT group at the University of Twente.
The new version of CADP is named 2001 "Ottawa" and dated July 13, 2001. It supersedes all previous versions of CADP.
We are happy to dedicate CADP 2001 "Ottawa" to Professor Luigi Logrippo and his research team at the University of Ottawa, who are actively promoting formal methods, especially LOTOS, in the telecommunication industry.
This is a brief chronology of past events:
The new release CADP 2001 "Ottawa" delivers a total of 85 bug fixes and 86 improvements. First of all, it contains 5 new tools: BCG_MIN, EVALUATOR 3.0, OCIS, SVL, and TGV.
A new tool named BCG_MIN was added to CADP. Jointly developed by the VASY team and Holger Hermanns (University of Twente), BCG_MIN implements various minimization algorithms for graphs encoded in the BCG format. It can be used to minimize several kinds of BCG graphs:
According to Prof. Jan-Friso Groote, BCG_MIN is "the best implementation of the standard [i.e.,Groote & Vaandrager] algorithm for branching bisimulation" (in J.F. Groote and J.C. van de Pol, State space reduction using partial tau-confluence, report SEN-R0008, CWI, Amsterdam).
The probabilistic LTS model of BCG_MIN generalizes many theoretical models published in the literature, including Discrete Time Markov Chains, Discrete Time Markov Reward Models, Alternating Probabilistic LTS, Discrete Time Markov Decision Processes, Generative Probabilistic LTS, Reactive Probabilistic LTS, and Stratified Probabilistic LTS.
The stochastic LTS model of BCG_MIN generalizes many theoretical models published in the literature, including Continuous Time Markov Chains, Continuous Time Markov Reward Models, Continuous Time Markov Decision Processes, Interactive Markov Chains, Timed Processes for Performance (TIPP) Models, Performance Evaluation Process Algebra (PEPA) Models, and Extended Markovian Process Algebra (EMPA) Models.
The BCG_MIN tool was integrated into EUCALYPTUS (together with ALDEBARAN and FC2TOOLS). It can be accessed by clicking on an LTS file (e.g., a BCG file) and then selecting "Reduce".
A new version 3.0 of the EVALUATOR tool has been developed. EVALUATOR 3.0 performs on-the-fly verification of regular alternation-free mu-calculus formulas on Labelled Transition Systems, which are represented implicitly according to the Open/Caesar API (Application Programming Interface). Compared to the previous version 2.0, EVALUATOR 3.0 brings major improvements:
Moreover, EVALUATOR 3.0 has been optimized in order to work more efficiently when verifying temporal formulas on explicit LTSs encoded as BCG files. Due to these optimizations, the memory consumption and the execution time of EVALUATOR 3.0 have been reduced by up to 5% and 20%, respectively.
In particular, the diagnostics obtained for derived "pure" branching-time logics like CTL and ACTL fully explain the semantics of their operators. EVALUATOR 3.0 may also serve to search regular execution sequences in the LTS, by asking for diagnostics of regular formulas.
For the end-user, the practical use of EVALUATOR 3.0 is illustrated in several ways. Seven demo examples are included in CADP 2001 "Ottawa". Three libraries are also available that encode the operators of the ACTL temporal logic as well as a set of generic temporal property patterns defined by Prof. Matthew Dwyer from Kansas State University. Finally, the EUCALYPTUS graphical user interface has been adapted to support EVALUATOR 3.0.
A new interactive, graphical simulator named OCIS (Open/Caesar Interactive Simulator) was added to CADP. Designed to replace the venerable Xsimulator tool, OCIS enables visualization and error detection during the design phase of systems containing parallelism and asynchronous communication between tasks. Its main features are:
OCIS was designed to be language-independent as much as possible and should therefore be usable for any specification language or formalism interfaced with the Open/Caesar API.
OCIS can be invoked from the command-line with the same syntax as any other Open/Caesar application program. It can also be started directly from the EUCALYPTUS graphical user-interface using the "Execute / Advanced Simulation" menu.
A new tool named SVL (Script Verification Language) was added to CADP. The SVL language and its associated compiler target at simplifying and automating the verification of LOTOS programs. SVL behaves as a tool-independent coordination language on top of the CADP and FC2 tools, in the same way as EUCALYPTUS is a tool-independent graphical user interface.
SVL offers high-level operators for generation, parallel composition, minimization, label hiding, label renaming, abstraction, comparison, and model-checking of Labelled Transition Systems. It supports several methods of verification (e.g., enumerative, compositional, and on-the-fly), which can be easily combined together.
A compiler for SVL has been developed, which translates an SVL verification scenario into a Bourne shell script, which will perform all the operations needed to execute the verification scenario, e.g., invoking verification tools with appropriate options and parameters, generating intermediate files, etc.
SVL has been used in several case-studies: most of the CADP demo examples (19 demos over a total of 29) take advantage of SVL readability and conciseness. In most cases, SVL allows the user to get rid of auxiliary files formerly used to perform the verification, including Makefiles, shell-scripts, as well as ".exp", ".hide", ".rename", and ".sync" files, all of which are generated automatically from one simpler, shorter ".svl" file.
Because of its expressiveness and robustness, SVL subsumes totally the ".des" format and the DES2AUT tool used in previous versions of CADP. Although the DES2AUT tool is kept in CADP 2001 "Ottawa" for compatibility purpose, it might be removed from future versions of CADP. Therefore, migrating compositional verification scenarios from DES2AUT to SVL is strongly advised.
The SVL tool was integrated into the EUCALYPTUS graphical user interface.
The latest version of the TGV (Test Generation based on Verification technology) tool, jointly developed by the PAMPA team of INRIA Rennes/IRISA and the Verimag laboratory, has been integrated into the CADP toolbox (with the help of the VASY team). TGV is a tool for the automatic generation of test suites from formal specifications. These test suites are used to assess the conformance of a protocol implementation with respect to the formal specification of this protocol. TGV takes two main inputs:
To produce conformance test suites automatically, TGV applies algorithms coming from verification technology. Test generation is done "on-the-fly" on the synchronous product of the specification with the test purpose; this product allows to avoid state explosion by exploring only the subset of the protocol specification permitted by the test purpose. The test cases generated by TGV are Labelled Transition Systems (encoded in ".aut" or ".bcg" format), the transitions of which carry test verdicts such as PASS, FAIL, and INCONCLUSIVE. More information on TGV...
TGV was integrated in the EUCALYPTUS user-interface. It can be launched easily by clicking on a ".lotos", ".aut", ".bcg", or ".exp" file and then selecting the "Generate tests" menu.
Besides introducing new tools, CADP 2001 "Ottawa" also brings significant improvements to existing tools:
CADP 2001 "Ottawa" can be used on the following computers/operating systems:
Note 1: Support for older versions of Linux (such as Debian 1, RedHat 4.*, RedHat 5.*) has been discontinued in February 2000, according to a technical enquiry conducted among all the users of CADP.
Note 2: CADP 2001 "Ottawa" is the last version of CADP available for Sparc stations running SunOS 4.1, Solaris 2.5, Solaris 2.6, and Solaris 7. Future versions will only support Solaris 8 or higher. CADP might continue to work on older Solaris versions, but we do not commit to this.
In principle, we maintain a strong compatibility between successive versions of CADP. However, changes are sometimes needed to allow progress. We review the changes introduced in CADP 2001 "Ottawa":
The following scientists have participated to the development of CADP 2001 "Ottawa":
We are extremely grateful to the following scientists, who provided us with valuable feedback and advice about the use of CADP:
Number: 600
Date: Thu Jan 28 14:59:20 MET 1999
Report: Christophe Discours and Radu Mateescu (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: com/bcg_draw, man/manl/bcg_draw.l,
com/bcg_edit, man/manl/bcg_edit.l
Nature: Two new options ("-fg" and "-bg") have been added to BCG_DRAW
and BCG_EDIT, in order to control the way windows are launched.
This extension is fully backward compatible.
Number: 601
Date: Wed Feb 10 14:35:49 MET 1999
Author: Hubert Garavel (INRIA/VASY)
Files: com/bcg_open, com/caesar.open, com/exp.open, com/fc2open
Nature: These four shell-scripts have been modified in order to
introduce the $OPEN_CAESAR_COMMAND variable, which will be
used by forthcoming OPEN/CAESAR tools.
Number: 602
Date: Fri Feb 26 09:47:20 MET 1999
Report: Alain Le Guennec (IRISA/PAMPA)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar
Nature: The C code generated by "caesar -open" was slightly changed,
in order to declare the CAESAR_FORMAT parameter of function
CAESAR_FORMAT_STATE(), whose declaration was missing. This
change is upward compatible.
Number: 603
Date: Thu Mar 18 18:00:36 MET 1999
Report: Axel Belinfante (Univ. of Twente), Hubert Canon (IRISA/PAMPA),
Alain Le Guennec (IRISA/PAMPA), Radu Mateescu (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/libcaesar.a, man/manl/caesar_table_1.l,
doc/Garavel-92-a.ps
Nature: A subtle bug was fixed in the "caesar_table_1" library of
the OPEN/CAESAR environment, which could cause some programs
to explore too many redundant states. A typical problem
reported was that "generator" would generate too many states.
This problem only occured when CAESAR_HASH_SIZE_STATE() was
strictly less than CAESAR_SIZE_STATE() and when function
CAESAR_CREATE_TABLE_1() was invoked by giving the value
CAESAR_SIZE_STATE to its parameter CAESAR_BASE_SIZE and
the (default) value NULL for its CAESAR_HASH parameter. In
such case, the caesar_table_1 library would invoke the
CAESAR_0_HASH() function provided by the caesar_hash library.
This function would perform hashing on the entire base fields
including non-hashable parts such as pointers (precisely,
hashing was applied to CAESAR_SIZE_STATE() bytes instead of
merely CAESAR_HASH_SIZE_STATE() bytes). This could have the
consequence that identical states were considered to be
different.
This problem was fixed by slightly modifying the semantics
of the CAESAR_CREATE_TABLE_1() function. The number and
types of the arguments of this function are unchanged.
The changes are such that the CAESAR_CREATE_TABLE_1()
now behaves so as to avoid the aforementionned problems.
Except very pathological cases, this change is upward
compatible: existing OPEN/CAESAR programs do not have to
be modified. However, using the new libcaesar.a library
is likely to improve their performances by reducing the
number of states (as identical states previously considered
to be different are now recognized as equal).
Number: 604
Date: Thu Apr 8 12:15:12 MET DST 1999
Author: Hubert Garavel (INRIA/VASY)
Files: com/xeuca, src/eucalyptus/*
Nature: From the EUCALYPTUS user-interface, the manual pages of the
Fc2Tools are now correctly displayed.
Number: 605
Date: Tue May 11 21:13:45 MET DST 1999
Authors: Hubert Garavel and Aldo Mazzilli (INRIA/VASY)
Files: com/xeuca, src/eucalyptus/xeuca_*,
src/eucalyptus/eucalyptus.tcl src/eucalyptus/xeucarc_standard
Nature: The EUCALYPTUS user-interface has been ported to Windows.
During this process, several improvements have been brought:
- The EUCALYPTUS windows can now be resized.
- When saving preferences, the current size and position
of the EUCALYPTUS window is now registered in the
$HOME/.xeucarc file.
- A "File / Reset Preferences" menu was added to restore
the default settings of EUCALYPTUS in the $HOME/.xeucarc
file.
- When one tries to launch a window that is already open,
the window pops up in the foreground (previously, a
message "This window is already opened" was displayed
in the right window).
- It is now possible to destroy an EUCALYPTUS sub-window
from the window manager (by sending the WM_DELETE event
under X-windows, or by clicking the "cross" button
on the top right corner, under Windows). Previously,
EUCALYPTUS did not catch events sent by the window
manager (destroying a window and trying to open it
again would lead to the message "This window is already
opened").
- The "View / Change Presentation" windows has now two
columns instead of one.
- The URLs of the "Web" button have been updated.
- The "duplex" program is not longer used by EUCALYPTUS.
- In the "Options" menu, some default options were not
set.
Number: 606
Date: Thu Jun 17 20:01:35 MET DST 1999
Authors: Hubert Garavel and Marc Herbert (INRIA/VASY)
Files: man/manl/caesar.indent.l, man/manl/declarator.l
Nature: Some errors and inconsistencies have been removed from the
manual pages of CAESAR.INDENT and DECLARATOR tools.
Number: 607
Date: Wed Jun 23 19:07:56 MET DST 1999
Author: Radu Mateescu (INRIA/VASY)
File: bin.*/xtl_expand
Nature: A bug was fixed in the handling of character string constants
that spread across several lines (i.e., contain sequences
backslash-newline). In the presence of these strings, the
whitespace between tokens was sometimes completely suppressed
during macro-expansion, thus leading to erroneous output.
Number: 608
Date: Thu Jun 24 09:46:40 MET DST 1999
Authors: Radu Mateescu and Mihaela Sighireanu (INRIA/VASY)
Files: bin.*/xtl_expand, bin.*/mcl_expand, bin.*/evaluator.a,
man/manl/evaluator.l, src/xtl/*.mcl, src/eucalyptus/*,
demos/demo{01,02,15,20,21,22}/*.mcl,
Nature: A new version 3.0 of the EVALUATOR tool has been developed.
This OPEN/CAESAR tool performs on-the-fly verification of
regular alternation-free mu-calculus formulas on Labelled
Transition Systems.
The tool consists of two modules: a binary called mcl_expand
and a new version of the library evaluator.a. Compared to the
previous version, EVALUATOR 3.0 brings major improvements:
- The input specification language of EVALUATOR 3.0 is more
powerful than the one of EVALUATOR 2.0.
Action formulas can now contain any combination of boolean
operators and basic predicates over transition labels (which
can be now given also as UNIX regular expressions over
character strings).
Regular transition sequences can be now succinctly described
using regular formulas built from action formulas and the
usual regular expression operators.
It is also possible now to define macro operators
parameterized by formulas and to group them into separate
libraries that may be included in the main specification.
The input language accepted by EVALUATOR 3.0 is defined in
the "evaluator" manual page. In general, EVALUATOR 3.0
still accepts *.mcl files containing formulas written for
EVALUATOR 2.0, but emits warnings to indicate obsolete
syntax. However, old-fashioned action formulas such as:
"!SEND|RECV"
should now be written as:
not ("SEND" or "RECV")
- The model-checking algorithm of EVALUATOR 3.0 is more
efficient. It uses a new on-the-fly boolean resolution
algorithm, which has a much better average complexity than
the algorithm by Fernandez-Mounier used in EVALUATOR 2.0.
The new algorithm explores less states before deciding the
truth value of the formula. This leads sometimes to dramatic
reductions (several orders of magnitude) of the execution
time.
- The diagnostics generated by EVALUATOR 3.0 are better.
Diagnostics are portions of the LTS explaining either the
satisfaction or the refutation of a formula: if the formula
is false, a diagnostic is a counterexample; if the formula
is true, a diagnostic is an example. In particular, the
diagnostics obtained for derived "pure" branching-time
logics like CTL and ACTL fully explain the semantics of
their operators. EVALUATOR 3.0 may also serve to search
regular execution sequences in the LTS, by asking for
diagnostics of regular formulas.
The manual page ('man evaluator') has been entirely rewritten.
The EUCALYPTUS graphical user-interface has been adapted to
support EVALUATOR 3.0.
All the demo files *.mcl containing mu-calculus formulas have
been adapted for the new input language syntax used by
EVALUATOR 3.0.
The macro expander xtl_expand has been extended in order to
handle properly the new syntax of .mcl files.
In addition, two libraries containing temporal operators
defined in regular alternation-free mu-calculus have been
added to those already present in $CADP/src/xtl:
- actl.mcl defines the ACTL temporal logic, and
- actl_patterns.mcl defines a set of property patterns
in ACTL.
These two libraries can be used for on-the-fly verification
of ACTL formulas and are equipped with relevant diagnostic
production features.
Number: 609
Date: Thu Jun 24 16:52:14 MET DST 1999
Author: Radu Mateescu (INRIA/VASY)
Files: src/xtl/path.xtl, src/xtl/nondet.xtl
Nature: Two new XTL library files have been added:
- path.xtl allows to compute and print on standard output
the shortest path from the initial state of the LTS to
(a state of) a given state set
- nondet.xtl uses the primitives of path.xtl to print the
shortest path leading to a nondeterministic state
These new primitives are useful for obtaining simple
diagnostic information about the LTSs coded in BCG format.
Number: 610
Date: Mon Jun 28 16:04:55 MET DST 1999
Author: Hubert Garavel (INRIA/VASY)
Files: com/xeuca, src/eucalyptus/*
Nature: The VISCOPE tool, which is no longer maintained nor
distributed by the PAMPA project, has been removed from the
EUCALYPTUS graphical user interface.
Number: 611
Date: Fri Jul 2 10:59:20 MET DST 1999
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_labels
Nature: The options -tmp, -uncompress, -compress, -register, -short,
-medium, and -size are now handled by the BCG_LABELS tool.
Number: 612
Date: Thu Jul 29 19:10:23 MET DST 1999
Authors: Radu Mateescu (INRIA/VASY)
Files: bin.*/xtl_expand
Nature: A bug was fixed in the search of *.mcl and *.xtl files that
are included in XTL and EVALUATOR source files using the
library ... end_library construct.
Number: 613
Date: Tue Jul 13 09:12:21 MET DST 1999
Report: Volker Braun (Univ. of Dortmund)
Authors: Marc Herbert and Hubert Garavel (INRIA/VASY)
Files: man/manl/*, man/html, man/ps
Nature: The CADP manual pages are now available, not only in the
Unix manual format (i.e., nroff), but also as PostScript
and HTML files.
Number: 614
Date: Tue Jul 13 10:48:29 MET DST 1999
Report: Axel Belinfante (Univ. of Twente), Joel Faedi (Univ. Henri
Poincare, Nancy)
Author: Hubert Garavel (INRIA/VASY)
Files: gc/bin.*/libgc.a
Nature: The previous version 4.10 of the Boehm-Demers garbage collector
used in the CADP distribution did not work under Solaris 7.
This caused CAESAR to abort during the simulation phase if the
"-gc" option was selected:
STACK_GROWS_DOWN is defd, but stack appears to grow up
sp = 0xffbef56c, GC_stackbottom = 0x0
stack direction 3
Abort - core dumped
The problem was solved by upgrading to version 4.14, which
is the most recent version available.
Number: 615
Date: Wed Jul 28 14:29:13 MET DST 1999
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar
Nature: A minor bug was fixed in optimization E5, which caused
CAESAR to core dump in some very special circumstances.
Number: 616
Date: Thu Aug 12 15:15:01 MET DST 1999
Author: Hubert Garavel (INRIA/VASY)
Files: doc/Pecheur-99.ps
Nature: A new paper was added in the 'doc' directory. This paper is
a shorter version of a previous paper, Pecheur-98.ps
Number: 617
Date: Wed Aug 18 17:25:24 MET DST 1999
Authors: Hubert Garavel and Aldo Mazzilli (INRIA/VASY)
Files: tcl-tk/*, com/bcg_edit, com/xeuca, com/installator,
bin.*/xsimulator.a, bin.*/libBCG_IO.a, xsimulator/text.tcl
Nature: The version of TCL-TK used for CADP was upgraded from Tcl
version 7.6 and Tk version 4.3 to Tcl/Tk version 8.0.4, and
later to Tcl/Tk version 8.2. So doing, a number of changes
have been brought to CADP:
- tcl-tk/bin.*/libtcl.a was replaced with libtcl8.2.so
- tcl-tk/bin.*/libtk.a was replaced with libtk8.2.so
- tcl-tk/bin.*/wish was upgraded
- tcl-tk/bin.*/expectk was removed (see below #631)
- a shell tcl-tk/com/wish was added
- a shell tcl-tk/com/tixwish was added
- a Windows version was added in tcl-tk/bin.win32
As a consequence of using shared libraries and removing
expectk, the size of the tcl-tk directory has significant
decreased: TCL/TK 8.0.4 would use 11849 Mbytes, whereas
TCL/TK 8.2 only uses 8476 Mbytes, including the added Windows
binaries.
As another consequence, the size of the binaries 'xsimulator'
created when the XSIMULATOR tool is invoked has been reduced
(from about 2 Megabytes to 90 Kbytes)
All the CADP tools using TCL/TK (i.e., EUCALYPTUS, BCG_EDIT,
MONITOR, INSTALLATOR, XSIMULATOR) have been updated to use
the new shell-script.
Number: 618
Date: Wed Aug 25 18:22:44 MET DST 1999
Author: Hubert Garavel (INRIA/VASY)
Files: com/bcg_open, com/caesar.open, com/exp.open, com/fc2open
Nature: All the OPEN/CAESAR shell-scripts have been updated to
handle LD_LIBRARY_PATH information.
Number: 619
Date: Wed Aug 25 19:02:12 MET DST 1999
Authors: Hubert Garavel and Aldo Mazzilli (INRIA/VASY)
Files: INSTALLATION_0, INSTALLATION_*
Nature: A new file, INSTALLATION_0, was added to explain how to
configure a Windows system before installing CADP.
The other installation files have been updated to take
into account the fact that Windows is now supported.
Number: 620
Date: Thu Sep 16 15:30:45 MET DST 1999
Author: Radu Mateescu (INRIA/VASY)
Files: incl/X_STRING.h
Nature: A mistake was corrected in file incl/X_STRING.h: "<>" was
replaced with "!="
Number: 621
Date: Fri Sep 17 18:47:57 MET DST 1999
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/caesar.adt
Nature: A bug, which caused CAESAR.ADT to core dump in some rare
circumstances when analyzing formal sorts, was fixed.
Number: 622
Date: Fri Sep 24 16:16:40 MET DST 1999
Report: Sebastien Gelgon (BULL/CP8)
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: bin.*/caesar, bin.*/caesar.adt
Nature: The previous versions of CAESAR and CAESAR.ADT emitted
cryptical messages, such as:
file ``.t'' may be out of date (check its contents)
or
file ``.f'' may be out of date (check its contents)
when reading the ".f", ".t" or ".h" files (which contain
implementation in C of LOTOS sorts and operations) if version
information was missing in these files.
The rules regarding version information are the following:
- Each ".t" file should start with a line of the form
#define CAESAR_ADT_EXPERT_T x.y
where x.y is equal to the number of the version of CAESAR.ADT
for which the ".t" file was (hand-)written (e.g., x.y = 5.0).
- Each ".f" file should start with a line of the form
#define CAESAR_ADT_EXPERT_F x.y
where x.y is equal to the number of the version of CAESAR.ADT
for which the ".f" file was (hand-)written (e.g., x.y = 5.0).
- Each hand-written ".h" file (i.e., ".h" files generated by
CAESAR.ADT are not concerned by this rule) should start with
a line of the form
#define CAESAR_ADT_EXPERT x.y
where x.y is equal to the number of the version of CAESAR.ADT
available when the ".h" file was developed (e.g., x.y = 5.0).
CAESAR and CAESAR.ADT insist on having these definitions
by emitting warning messages if CAESAR_ADT_EXPERT_T,
CAESAR_ADT_EXPERT_F, or CAESAR_ADT_EXPERT are not properly
specified. The reason for this is to force users to stamp
their hand-written data implementation files with version
numbers, so that future versions of CAESAR and CAESAR.ADT
will be able to ensure backward compatibility if the
interfacing conventions are modified.
If version information is missing from a file, then
CAESAR and CAESAR.ADT assume that these files are old-
fashioned files, compatible with CAESAR.ADT 4.1. A first
warning is then emitted:
macro CAESAR_ADT_EXPERT_T not defined in file ``.t''
(default value: 4.1)
Then, a second warning is emitted, as there have been
incompatible changes in interface conventions since
CAESAR.ADT 4.1:
file ``.t'' seems obsolete according to the value of
CAESAR_ADT_EXPERT_T
check and upgrade its contents as explained in the
file $CADP/HISTORY.txt
To avoid these warnings, one should simply define
#define CAESAR_ADT_EXPERT_T 5.0
#define CAESAR_ADT_EXPERT_F 5.0
#define CAESAR_ADT_EXPERT 5.0
at the beginning of ".t", ".f" and hand-written ".h" files,
respectively.
Number: 623
Date: Fri Sep 24 17:35:33 MET DST 1999
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: bin.*/caesar.adt, incl/X_STRING.h,
demos/demo_04/EXP.t
Nature: The C code generated by CAESAR.ADT for complex types
(records and discriminated unions) was significantly
improved.
Previously, all these types were implemented as pointers
to records or to discriminated unions (the so-called "boxed"
representation).
The new version of CAESAR.ADT attempts to implement all non-
recursive types directly as records or discriminated unions
(the so-called "unboxed" representation).
In the case of mutually recursive types, CAESAR.ADT uses
heuristics that attempt to implement as pointers a minimal
number of types, in order to break all circular dependencies.
However, the user has the possibility to break himself/herself
the circular dependencies by specifying whether a type should
be implemented by a pointer or not.
To specify that a type T should not be implemented as a
pointer, the user should add a directive of the form
#define CAESAR_ADT_HASH_T 0
in the ".t" file.
To specify that a type T should be implemented as a pointer,
the user should add a directive of the form
#define CAESAR_ADT_HASH_T 1
in the ".t" file.
By default, if no such directive is given, CAESAR.ADT will
do its best to implement T as a non pointer type.
If there is a cyclical dependency between types that the user
has forced to be implemented as non-pointer types, then
CAESAR.ADT will stop with an error message.
This improvement required important changes in the internal
organization of CAESAR.ADT. From now on, the ".t" file will
always be read (during the "type survey" phase) if it exists
in the current directory, even if there is no LOTOS sort
declared with a "(*! external *)" attribute or without
associated constructor operation.
This improvement leads to important memory savings for usual
data structures such as records, packets, protocol data units,
etc. For instance, in a SCSI-2 example studied at INRIA,
the C code generated by the previous version of CAESAR.ADT
required more the 955 Mbytes, whereas the C code generated
by the new version only uses 7 Mbytes!
As a consequence, for an external type T, the macro-definition
#define CAESAR_ADT_POINTER_T
specifying that T is a pointer type (see above #235) is no
longer well-adapted. It should be replaced by the following
macro-definition:
#define CAESAR_ADT_UNCANONICAL_T
stating that values of type T are not represented under
normal form. This can occur if T is a pointer type, but
also in other cases, for instance if T is a record containing
pointer fields or a record with uninitialized padding bits
between the fields, etc (and so on recursively).
By default, if CAESAR_ADT_UNCANONICAL_T is not defined for
an external type, it is assumed that values of type T are
canonical (i.e., represented under normal form), thus
enabling bit string comparison and hashing on these values.
If the user forgets to define CAESAR_ADT_UNCANONICAL_T when
appropriate, this can result in state explosion in exhaustive
and on-the-fly verification, as identical values could yield
different hash-code values, thus leading to consider identical
states to be different. However, this risk was preferred to
the burden of defining an opposite macro CAESAR_ADT_CANONICAL_T
for each external canonical type T. Therefore, the user should
be careful when defining non-canonical, external types.
If T is not an external type, CAESAR.ADT will automatically
define CAESAR_ADT_UNCANONICAL_T if appropriate, as a part
of the implementation of T in C. CAESAR.ADT will emit a
warning if the user attempts to define CAESAR_ADT_UNCANONICAL_T
for a non external type.
For backward compatibility, any existing macro-definition
#define CAESAR_ADT_POINTER_T
is understood as
#define CAESAR_ADT_UNCANONICAL_T
However, the latter is the recommended form.
All the ".t" files enclosed in the CADP release that defined
CAESAR_ADT_POINTER_T have been updated accordingly.
Number: 624
Date: Thu Sep 23 19:18:47 MET DST 1999
Report: Alain Le Guennec (IRISA/PAMPA)
Authors: Radu Mateescu and Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a
Nature: A bug was fixed in the BCG_OT_READ_BCG_END() function,
which stopped unexpectedly (with a message of the form
"bcg_transition: complete_edge_table not implemented")
if the access_mode parameter in the corresponding call of
BCG_OT_READ_BCG_BEGIN() had the value 4, for instance when
using the iterator BCG_OT_ITERATE_P_LN on a BCG file opened
with access_mode equal to 4 (see "man bcg_read" for details).
Number: 625
Date: Wed Sep 29 17:52:32 MET DST 1999
Report: Alain Le Guennec (IRISA/PAMPA)
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: bin.*/libBCG.a
Nature: When attempting to use an iterator not compatible with the
access_mode parameter given to BCG_OT_READ_BCG_BEGIN() when
BCG graph was opened, the BCG library emitted a cryptic message
of the form
bcg_transition: illegal iteration for object
The message has been improved, e.g.,
illegal iteration for a graph opened with access mode 0
or:
illegal iteration for a graph opened with access mode
different from 4
(see also item #634 below).
Number: 626
Date: Thu Sep 30 15:41:44 MET DST 1999
Author: Radu Mateescu and Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a, man/manl/bcg_read.l, man/manl/bcg_write.l
src/open_caesar/generator.c, src/open_caesar/reductor.c
Nature: The functions for reading and writing BCG files, i.e., the
two functions BCG_OT_READ_BCG_BEGIN() from the "bcg_read"
API and BCG_IO_WRITE_BCG_BEGIN() from the "bcg_write" API
have been enhanced: if the name of the file to open for
reading or writing is not suffixed by ".bcg", then the
".bcg" suffix will be added automatically.
This new feature simplifies the development of tools based
upon the BCG technology. For instance, the "generator" and
"reductor" tools have been simplified accordingly.
This change is upward compatible, except in the special case
where the "bcg_write" API was used to create BCG files without
a ".bcg" extension. This special case should not occur, as the
"bcg_write" manual page specified that a ".bcg" suffix had to
be given when invoking BCG_IO_WRITE_BCG_BEGIN().
Number: 627
Date: Thu Sep 30 15:54:46 MET DST 1999
Report: Bruno Hondelatte and Pierre Kessler (INRIA/VASY)
Author: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: bin.*/libBCG.a, bin.*/libBCG_IO.a, bin.*/libbcg_*.a,
bin.*/bcg_io, incl/bcg_*.h,
man/manl/bcg_read.l, man/manl/bcg_write.l
Nature: The "bcg_read" and "bcg_write" interfaces for reading and
writing BCG files (see "man bcg_read" and "man bcg_write"
for details) have been improved in order to offer enhanced
convenience and flexibility to the user.
First, the error messages emitted when failing to open a BCG
file (for either reading or writing) have been made more
readable than the previous (cryptical) messages of the form
"fopen error in BCG_OPEN" and "fopen error in BCG_OPEN_BINARY".
Second, the function BCG_OT_READ_BCG_BEGIN() has been modified
in such a way that, if the opening of a BCG file fails, the
execution of the program will not be aborted. By default, the
previous behaviour is retained: if the BCG file is unreadable
an error message will be emitted and the program will stop.
From now on, it is also possible, in this case, that function
BCG_OT_READ_BCG_BEGIN() returns normally with its bcg_graph
parameter set to NULL to report an opening failure. This new
behaviour can be obtained by invoking the new function
BCG_OT_READ_BCG_SURVIVE (BCG_TRUE);
before invoking BCG_OT_READ_BCG_BEGIN().
Third, the function BCG_IO_WRITE_BCG_BEGIN() has been modified
in such a way that, if the opening of a BCG file fails, the
execution of the program will not be aborted. By default, the
previous behaviour is retained: if the BCG file is unwritable
an error message will be emitted and the program will stop.
From now on, it is also possible, in this case, that function
BCG_IO_WRITE_BCG_BEGIN() returns normally a boolean result
to report whether the BCG file could be open or not. This new
behaviour can be obtained by invoking the new function
BCG_IO_WRITE_BCG_SURVIVE (BCG_TRUE);
before invoking BCG_IO_WRITE_BCG_BEGIN().
This change is upward compatible in the sense that existing
tools based upon the BCG technology do not have to be modified
and will keep their current behaviour (with improved error
messages). However, new tools can take advantage of the new
features to recover from file opening errors.
Number: 628 Date: Thu Sep 30 19:26:31 MET DST 1999 Author: Aldo Mazzilli (INRIA/VASY) Files: incl/X_NATURAL.h Nature: The "X_NATURAL.h" file was modified to compile under Windows.
Number: 629
Date: Thu Sep 30 19:48:24 MET DST 1999
Report: Judi Romijn (Univ. Nijmegen), Jie Dai (University of Idaho),
Wayne Liu (Univ. of Waterloo)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.sun5/hostinfo
Nature: The "hostinfo" binary provided in CADP 97b could core dump on
some Solaris 7 systems (but not all). It was replaced with an
upgraded version.
Number: 630
Date: Fri Oct 1 11:55:30 MET DST 1999
Authors: Aldo Mazzilli and Hubert Garavel (INRIA/VASY)
Files: com/bcg_edit, src/bcg_edit
Nature: The BCG_EDIT command has been ported to Windows. A few changes
have been brought to enable the port:
- The grid has now blue lines instead of grey dotted lines
- With a two-button mouse, the middle button can be obtained
by pressing the Shift key together with the right button
- Consequently, the bindings Shift + middle button and
Shift + right button are now longer devoted to region
selection, for which purpose Shift + left button remains
the only permitted binding.
Number: 631
Date: Sat Oct 1 18:05:10 MET DST 1999
Report: Axel Belinfante (Univ. Twente), Paulo Carreira (Oblog, Lisboa),
Laurent Mounier (VERIMAG, Grenoble), Elie Najm (ENST, Paris)
Authors: Aldo Mazzilli and Hubert Garavel (INRIA/VASY)
Files: com/installator, src/installator, src/com. src/eucalyptus
Nature: The Installator tool has been ported to Windows. So doing, it
has been deeply modified to achieve architecture independance:
- The new Installator no longer uses Expectk, which was not
available on Windows. It uses the plain Tcl/Tk "wish"
interpreter.
- The new Installator uses the FTP client written in Tcl/Tk
by Steffen Traeger.
- The script-shells used by installator have been renamed and
moved from $CADP/src/installator/com to $CADP/src/com.
These changes should be transparent to the end-user. They
were motivated by the need to factorize common shell-scripts
between Eucalyptus and Installator.
More precisely, the Eucalyptus shells xeuca_crlf, xeuca_edit,
xeuca_mail, xeuca_postscript, xeuca_print, xeuca_web have
been renamed into cadp_crlf, cadp_edit, cadp_mail, etc.
and moved to $CADP/src/com.
The shells run_mv, run_tst, and run_mail have been removed.
The shell install_logname was added. The shells cadp_version,
run_setup, run_rfl, run_df, and run_uncompress have been
renamed into install_version, install_setup, install_rfl,
etc., modified, and moved to $CADP/src/com.
Many other improvements and new features have been introduced:
- On machines without access to FTP, the new Installator emits
a proper error message ; the previous version would block
with an error message `child process exited abnormally' when
Installator was checking what the latest version of CADP
available.
- The new Installator emits an error message in advance if the
user tries to install CADP on a disk with unsufficient space.
The previous version would start the installation and then
stop with an "Error while decompressing" message.
- If the "logname" command was displaying an empty string
(which should not occur in fact), the previos versions would
block with an error message "cannot execute child process".
- There is an automatic focus in the password window.
- There is an explicit message stating that multiples
architectures (sun4, sun5, iX86, etc.) can be selected.
- The blue progression bars used during FTP transfer now
behave properly (with the previous version, the bars
sometimes exceeded 100%, so that they would start from
0% again, which was strange, but harmless).
- On Unix machines, the new Installator checks whether the
sendmail daemon is running or not. If not, a warning is
emitted and Installator does not attempt to send the
prototype license file.
- On Windows machines, the new Installator uses the Blat
mail sending client, a public domain software by Mark Neal,
Pedro Mendes, Gilles Vollant, and Tim Charron.
- The new Installator allows to specify a return e-mail address
to which the CADP team will send the license file. This can
be useful for users installing CADP as "root" (under Unix)
or "administrator" (under Windows) who want the license to
be sent back to their "real" e-mail address.
- The e-mail address "[email protected]" was replaced with
"[email protected]" (both are identical).
- If e-mail cannot be sent properly, the new Installator emits
a error message and saves the prototype license file in the
user's home directory.
Number: 632
Date: Wed Oct 20 15:39:57 MET DST 1999
Author: Hubert Garavel (INRIA/VASY)
Files: tcl-tk/*
Nature: The version of TCL/TK shipped within CADP was upgraded to
8.2.1, which is the most recent version until now, in order
to fix some disorders noticed with Installator when using
version 8.2.
Number: 633
Date: Wed Oct 27 09:34:30 MET DST 1999
Report: Lynne Blair (Lancaster University), Alain Le Guennec (IRISA),
Solofo Ramangalahy (IRISA)
Author: Hubert Garavel
Files: installator.shar
Nature: On Linux RedHat 6.0, installator would issue error messages:
% /bin/sh installator.shar
: not a legal variable name
: not a legal variable name
'nstallator.shar: syntax error near unexpected token `in
'nstallator.shar: installator.shar: line 6:
Although the reason of this problem is still unclear, the
shell-script installator.shar was modified to avoid the
use of lines commented out using ':'.
Number: 634
Date: Wed Oct 27 09:56:17 MET DST 1999
Authors: Radu Mateescu and Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a
Nature: Two error messages have been added, allowing to handle
properly the two error situations described below:
- When an iterator on the successors (for instance,
BCG_OT_ITERATE_P_LN()) is used on a BCG object transition
previously opened using BCG_OT_READ_BCG_BEGIN() with
access_mode equal to 2, the following error message will be
issued:
"bcg_transition: illegal iteration for a graph opened
with access mode 2"
- When an iterator on the predecessors (for instance,
BCG_OT_ITERATE_N_PL()) is used on a BCG object transition
previously opened using BCG_OT_READ_BCG_BEGIN() with
access_mode equal to 1, the following error message will be
issued:
"bcg_transition: illegal iteration for a graph opened
with access mode 1"
These two error situations were not captured properly by the
bcg_read interface and caused the applications to core dump.
Number: 635
Date: Wed Oct 27 11:03:22 MET DST 1999
Author: Radu Mateescu and Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a, bin.*/libBCG_IO.a, bin.*/libbcg_draw.a,
bin.*/libbcg_open.a, incl/bcg_iterator.h
Nature: A bug was fixed in the implementation of the "bcg_read" API:
for BCG files opened with access mode 4, the iterator on
the predecessors of a given state were not computed properly
(exactly as if the set of predecessors was empty).
Number: 636
Date: Wed Oct 27 14:38:31 MET DST 1999
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/xtl, src/xtl/nondet.xtl
Nature: Two bugs were fixed in the variable linking phase of the
XTL compiler. The XTL library "nondet.xtl" was also slightly
modified (without introducing any semantic change)
according to these bug fixes.
Number: 637
Date: Wed Oct 27 19:28:29 MET DST 1999
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/xtl, bin.*/libXTL.a, man/manl/xtl.l
Nature: The XTL 1.1 tool has been improved, leading to a new version
XTL 1.2, which allows the user to import external types and
functions in an XTL specification (see the XTL manual page
"man xtl" for details).
This improvement allows to use in an XTL specification complex
data types such as arrays, matrices, lists, trees, etc. and
complex operations such as vector-matrix multiplication, tree
traversals, etc. In particular, this enables the development of
XTL libraries implementing temporal logics whose model-checking
algorithms require complex numerical computations, as this is
the case for probabilistic temporal logics.
Besides declaring external types and functions in an XTL
specification, the user must also provide an implementation
in C of these types and functions that will be integrated to
the C code generated by the XTL tool from the specification.
The declaration of an external type is done as follows:
type MyType
! implementedby "MYTYPE"
! comparedby "CMP_MYTYPE"
! enumeratedby "ITR_MYTYPE"
! printedby "PRT_MYTYPE"
end_type
where the pragma '! implementedby' specifies the name of the
corresponding C type; '! comparedby' specifies the equality
operator for the type; '! enumeratedby' specifies an iterator
for enumerating values of the type; and '! printedby' specifies
a function for printing a value of the type in a file.
The declaration of an external function is done as follows:
func MyFunc (MyType1, MyType2) : MyType
! implementedby "MYFUNC"
end_func
where the pragma '! implementedby' specifies the name of the
corresponding C function.
The implementation in C of external data types and functions
provided by the user can be integrated in two different ways
in an XTL specification.
- The external types and functions may be implemented in
(one or more) C files file1.c, ..., filen.c that will
be directly included in the C code generated by XTL.
In this case, the following directive must be used in the
XTL specification:
include "file1.c", ..., "filen.c" end_include
- The external types and functions may be implemented in
(one or more) separate libraries libLIB1.a, ..., libLIBn.a
together with (one or more) interfaces file1.h, ..., filem.h
that will be linked with the C code generated by XTL.
In this case, the following directives must be used in the
XTL specification:
include "file1.h", ..., "filem.h" end_include
flag "-Ldir -lLIB1 -lLIB2 ... -lLIBn" end_flag
The flag ... end_flag directive also allows to specify other
compiling and link-editing options (e.g., -Idir) for the C
compiler.
Number: 638
Date: Fri Oct 29 14:43:26 MET 1999
Authors: Moez Cherif (INRIA/VASY), Hubert Garavel (INRIA/VASY), Holger
Hermanns (Univ. of Twente)
Files: bin.*/bcg_min, man/manl/bcg_min.l
Nature: A new tool named "bcg_min" was added to the CADP distribution.
This tool performs minimization of Labelled Transition Systems
modulo strong and branching bisimulation.
Compared to Aldebaran 6.4, BCG_MIN offers the following
advantages and new features:
- BCG_MIN can handle larger graphs (e.g., several hundreds
thousands of states, several millions of transitions);
- BCG_MIN uses BCG as its native format, thus leading to
speed improvement (because ".bcg" files are much smaller
than ".aut" files);
- BCG_MIN uses the algorithm by Groote and Vaandrager for
computing branching bisimulation, which is usually more
efficient than the BDD-based method used in Aldebaran 6.4;
- BCG_MIN (with option "-class") prints equivalence classes
in a user-friendly way, by relating the state numbers of
the minimized graph to the state numbers of the original
graph. In the case of branching equivalence, the tau-cycles
are properly displayed.
- Last but not least, BCG_MIN supports not only standard
Labelled Transitions, but also "probabilistic" LTSs
and "stochastic" LTSs (i.e,, Discrete Time and Continuous
Time Markov Decision Processes).
See the manual page ("man bcg_min" for details).
Number: 639 Date: Thu Nov 11 16:19:30 MET 1999 Author: Hubert Garavel (INRIA/VASY) Files: doc/Garavel-Sighireanu-99.ps, doc/=README.txt Nature: A new publication was added to the "doc" directory.
Number: 640
Date: Wed Dec 8 11:03:37 MET 1999
Report: Fabrice Baray (ISIMA/LIMOS, France),
Paulo Jorge Fernandez (Oblog, Portugal)
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/xtl
Nature: Two bugs were fixed in the XTL compiler. The first one (the
unexpected detection of a multiple variable declaration during
the variable linking phase) occurred when several quantifiers
"exists" and/or "forall" with "among" clauses were nested.
The second one (compile-time errors in the C code generated by
XTL) occurred because XTL had not been updated after the
changes brought to the BCG iterators (see #634 and #635 above).
Number: 641
Date: Thu Jan 6 17:58:10 MET 2000
Report: Brian Ross (University of Glasgow, Scotland)
Author: Hubert Garavel (INRIA/VASY)
Files: com/rfl
Nature: A "Year 2000" bug has been fixed, which caused the RFL script
to generate licenses for period 1900-1901.
Number: 642
Date: Wed Jan 19 11:24:55 MET 2000
Author: Hubert Garavel (INRIA/VASY)
Files: demos/demo_19/start, demos/demo_19/graphics/startsimu
Nature: The demo_19 has been updated to work with the latest version
of TCL/TK shipped within CADP.
Number: 643
Date: Wed Jan 19 11:43:15 MET 2000
Author: Hubert Garavel and Moez Cherif (INRIA/VASY)
Files: src/installator/installator.tcl, src/eucalyptus/eucalyptus.tcl,
src/bcg_edit/bcg_edit.tcl, src/monitor/main.tcl,
src/xsimulator/main.tcl, demos/demo_19/graphics/startsimu
Nature: All the TCL/TK scripts of CADP have been updated in order to
reflect some changes of the latest version of TCL/TK. In
particular, the bgerror procedure must now be defined in
each TCL/TK application; otherwise, one can see messages
of the form:
bgerror failed to handle background error.
...
Error in bgerror: invalid command name "bgerror"
Number: 644
Date: Fri Jan 21 10:45:31 MET 2000
Report: Alain le Guennec (IRISA)
Author: Hubert Garavel (INRIA/VASY)
Files: doc/Garavel-92-a.ps, man/*/caesar_graph.*
Nature: The manual page for the "caesar_graph.h" API has been improved
in two ways:
- In the "CAESAR-specific note" attached to functions
CAESAR_DUMP_LABEL() and CAESAR_STRING_LABEL(), the
function name CAESAR_DUMP_LABEL() was incorrect; it has
been replaced with CAESAR_PRINT_LABEL().
- The definition of functions CAESAR_HASH_STATE() and
CAESAR_HASH_LABEL() has been reinforced to stress the fact
that the results of these functions *must be* in the range
0..CAESAR_MODULUS-1.
Number: 645
Date: Fri Jan 21 11:03:47 MET 2000
Report: Alain le Guennec (IRISA)
Author: Hubert Garavel (INRIA/VASY)
Files: src/declarator.c
Nature: The Declarator program was strengthened by adding tests that
check whether the results of functions CAESAR_HASH_STATE() and
CAESAR_HASH_LABEL() is in the range 0..CAESAR_MODULUS-1.
Number: 646
Date: Fri Jan 21 11:41:53 MET 2000
Report: Alain le Guennec (IRISA)
Author: Hubert Garavel (INRIA/VASY)
Files: src/monitor/main.tcl
Nature: The BCG monitor did not work properly if the graph would
have labels containing a dot ('.') character. This problem
was fixed.
Number: 647
Date: Fri Jan 21 18:07:02 MET 2000
Authors: Moez Cherif and Hubert Garavel (INRIA/VASY)
Files: src/eucalyptus/eucalyptus.tcl
Nature: In the EUCALYPTUS user-interface, several problems created
by the new version of TCL/TK have been fixed:
- Using the Cancel buttons would result in error messages
- Using the "Browse" button would erase the current file entry
- Using the Cancel button in a "Browse" window would not
restore the initial values.
Number: 648
Date: Mon Jan 24 18:52:26 MET 2000
Authors: Thierry Jeron, Pierre Morel, Severine Simon (IRISA) with the
help of Hubert Garavel, Moez Cherif, Marc Herbert (INRIA/VASY)
Files: bin.*/tgv.a, man/*/tgv.*, demos/demo_01, demos/demo_09,
src/eucalyptus/eucalyptus.tcl
Nature: The latest version of the test generation tool TGV developed
by Thierry Jeron, Pierre Morel, Severine Simon (IRISA) has been
integrated to the CADP toolbox. TGV is a tool for automatic
generation of test cases for conformance testing developed by
the Verimag laboratory and the PAMPA project of INRIA/IRISA.
The VASY team provided help for integrating TGV within CADP
and porting it to several architectures.
The most recent version of TGV is fully compatible with the
CADP tools. It is built on the Open/Caesar open architecture,
and thus can be applied to various languages (LOTOS, UML...).
Test purposes can be submitted to TGV either in ".aut" or
".bcg" format. The test cases produced by TGV can be either
in ".aut" or ".bcg" files. TGV now takes advantage of the
Caesar_Hide_1 and Caesar_Rename_1 libraries of Open/Caesar.
A manual page is available (see "man tgv"). The existing
examples demo_01 and demo_09 have been enhanced to show
use cases of the TGV tool.
The EUCALYPTUS graphical interface has been enhanced to
allow an easy access to the TGV tool (click on the
"Generate tests..." option on a .lotos, .bcg, .aut or .exp
graph).
Number: 649
Date: Tue Feb 1 19:05:29 MET 2000
Report: Solofo Ramagalahy (IRISA/PAMPA)
Authors: Moez Cherif and Hubert Garavel (INRIA/VASY)
Files: src/bcg_edit/bcg_edit.tcl
Nature: A bug that occured when trying to move the initial state of
a graph with 1 state and 0 transition has been fixed.
Number: 650
Date: Tue Feb 1 19:21:15 MET 2000
Report: Alain Le Guennec (IRISA/PAMPA)
Authors: Moez Cherif and Hubert Garavel (INRIA/VASY)
Files: src/monitor/main.tcl
Nature: The label window of the BCG monitor has been made resizable
both horizontally and vertically. An horizontal scrollbar has
also been added.
Number: 651
Date: Tue Feb 1 19:26:30 MET 2000
Author: Radu Mateescu (INRIA/VASY)
Files: doc/Mateescu-00-a.ps, doc/=README.txt
Nature: A new publication regarding EVALUATOR 3.0 was added to the
"doc" directory.
Number: 652
Date: Mon Feb 21 16:27:03 MET 2000
Report: Paulo Carreira (Oblog, Lisboa)
Authors: Marc Herbert and Hubert Garavel (INRIA/VASY)
Files: bin.iX86/indent, bin.win32/indent, src/com/cadp_indent,
bin.*/caesar.adt
Nature: The "indent" program provided in $CADP/bin.iX86 did not work
properly (some large C files were truncated). Because recent
versions of Linux (such as RedHat 6.1) provide "indent" (see
the "indent" package), this program is not longer included in
CADP.
Given that the different versions of "indent" on various
platforms have different options, a shell-script named
"cadp_indent" has been developed to provide a portable
command across various platforms. CAESAR.ADT no longer invokes
"indent" directly, but invokes "cadp_indent" instead.
A version of "indent" compiled for Windows has been added in
"bin.win32".
Number: 653
Date: Tue Feb 22 15:17:39 MET 2000
Author: Hubert Garavel (INRIA/VASY)
Files: gc/bin.*/libgc.a, bin.*/caesar.adt, bin.*/caesar
Nature: Item #614 above reports that the garbage collector library
was upgraded from version 4.10 to 4.14 in order to cope with
the Solaris 7 operating system.
Unfortunately, all the beta-versions of CADP 99 issued between
July 1999 and the beginning of March 2000 have a problem with
garbage collection.
Due to a mistake in setting compiler options, the garbage
collector was not interfaced properly with the other tools:
even if the "-gc" option was given to CAESAR and "caesar.open",
garbage collection would not occur. This error was silent: the
tools functioned normally, except that garbage collector was
never activated, potentially leading to excessive memory
consumption.
This problem was discovered when porting the garbage collection
library to Windows. Correct versions of the library have been
put in the CADP distribution. For various reasons, it was also
necessary to change the interface conventions used by CAESAR
and CAESAR.ADT to activate garbage collection. This required
to modify the C code generated by CAESAR.ADT.
If you are using a version of CADP between beta-version 99-a
to 99-f included, it is strongly advised to upgrade to beta-
version 99-g or upper.
If you have ``.h'' files generated by a previous version
of CADP, it is recommended to remove them and generate them
again. You can recognize ``.h'' files generated by the new
version CAESAR.ADT as they check a macro-definition named
CAESAR_ADT_GARBAGE_COLLECTION and invoke function GC_malloc().
Obsolete ``.h'' files do not contain these two identifiers.
The Windows version of the garbage collection library has
also been added to CADP.
Number: 654
Date: Fri Feb 25 12:02:39 MET 2000
Authors: Hubert Garavel (INRIA/VASY), Laurent Mounier (VERIMAG),
Severine Simon (INRIA/PAMPA)
Files: bin.iX86/*, gc/bin.iX86/*, tcl-tk/bin.iX86/*, games/bin.iX86/*
Nature: The Linux binaries and libraries contained in the CADP package
have been ported from libc5 to libc6, in order to follow the
evolutions of the GNU C library. This should allow CADP to run
on recent versions of Linux without compatibility packages.
For more information about libc5 and libc6, you can consult
http://www.inrialpes.fr/vasy/cadp/patches97b.html
Number: 655
Date: Mon Mar 6 11:37:59 MET 2000
Author: Marc Herbert and Hubert Garavel (INRIA/VASY)
Files: bin.sun5/caesar, bin.sun5/caesar.adt, bin.sun5/caesar.indent,
bin.sun5/mcl_expand, bin.sun5/xtl
Nature: A minor bug was fixed in the libraries of the SYNTAX compiler
generator which affected the sun5 (Solaris 2.*) platform only.
Due to this bug, the error messages produced by CAESAR,
CAESAR.ADT, CAESAR.INDENT, MCL_EXPAND, and XTL in case of
syntax error were less detailed than for other platforms
(the erroneous lines in the source code were not always
displayed).
Number: 656
Date: Thu Mar 9 10:56:00 MET 2000
Report: Solofo Ramangalahy (INRIA/PAMPA)
Author: Hubert Garavel (INRIA/VASY)
Files: src/open_caesar/executor.c
Nature: When the Executor program is started with option (2), the
seed of the pseudo-random number generator is initialized with
the system clock, i.e., the number of seconds elapsed since
January, 1st, 1970. This could create problems when two
successive executions of Executor where started very closely
in time (i.e., were distant from less than one second, a
situation likely to happen as machines are getting faster).
In this case, the two executions would share the same seed.
To avoid this problem, a "sleep(1)" statement has been inserted
in Executor, so that two successive executions are separated
by at least one second and, thus, have different seeds.
Number: 657
Date: Wed Mar 22 09:08:23 MET 2000
Report: Severine Simon (INRIA/PAMPA), MIhaela Sighireanu (LIAFA, Paris)
Authors: Moez Cherif and Hubert Garavel (INRIA/VASY)
Files: com/bcg_edit, src/bcg_edit/bcg_edit.tcl
Nature: The BCG_EDIT tool has been improved in several ways:
(1) Checks have been implemented to prevent the user from
moving states and (control points of) transitions (either
straight or curved) out of the window.
(2) A more robust error detection mechanism allows BCG_EDIT
to recover when the "Preview" or "Print" command fails.
(3) The new version of BCG_EDIT allows to resize the window
within minimal and maximal size boundaries.
(4) The new version of BCG_EDIT does not abort if one invokes
"bcg_edit foo.bcg", where the file "foo.bcg" does not exist.
(5) The new version of BCG_EDIT no longer stops if the C
compiler (invoked by BCG_LIB when reading a BCG file) emits
warning messages such as "gcc: file path prefix ... never
used".
(6) The new version of BCG_EDIT no longer stops if the
environment variable $CADP_CC is not set.
(7) The new version BCG_EDIT does some heuristic checks to
verify that a ".ps" file to be read is not an ordinary
PostScript file, but a graph layout encoded in the BCG-PSF
format.
(8) The grid is now aligned with the top left corner of
the white window; it no longer overlaps the grey margin.
(9) The "<Return>" (or "<Enter>") key is now active in
the sub-windows opened by "Preview", "Print", "Load PS",
"Load BCG", etc. It works for files and directories.
Number: 658
Date: Wed Mar 22 12:38:55 MET 2000
Authors: Severine Simon (INRIA/PAMPA), Hubert Garavel (INRIA/VASY)
Files: bin.*/tgv.a, man/manl/tgv.l
Nature: An improved version of TGV (TGV version 1.1) has been
introduced in CADP. The improvements brought by TGV 1.1
are the following:
- Non-deterministic test purposes are now accepted.
- Two new options "-keeplock" and "-outprior" have been added
(see the "tgv" manual page for detailed information).
- A bug that would cause occasional core dump has been
fixed.
The "tgv" manual page has been updated. The EUCALYPTUS
graphical user-interface was updated accordingly.
Number: 659
Date: Thu Apr 20 17:31:07 MET DST 2000
Authors: Severine Simon (INRIA/PAMPA)
Files: bin.*/tgv.a
Nature: A bug in "-timer" option of TGV was fixed. Previously, in the
test cases produced with option "-timer", some START/CANCEL of
timers could be useless. Specially, the transition
"START TAC, TNOAC; COMMENT(TNOAC<TAC)"
was replaced by a simpler transition
"START TNOAC"
as it was useless to start TAC in this case.
Number: 660
Date: Thu Apr 6 17:37:51 MET DST 2000
Report: Paulo Carreira (Oblog, Lisboa), Ludovic Kuty (Univ. Liege)
Author: Hubert Garavel (INRIA/VASY)
Files: com/rfl
Nature: In the license file produced by "rfl", the line
contrat de mise a` disposition
has been replaced with
contrat de mise a disposition
to avoid problems with some mailers that dropped the back-quote
character silently, thus causing a global checksum error
Number: 661
Date: Thu Apr 6 19:22:45 MET DST 2000
Report: Holger Hermanns (Univ. of Twente)
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/xtl
Nature: A bug was fixed in the code generation phase of XTL. The bug
consisted in initializing a global variable with a non-constant
value in the C code generated by XTL, which did not compile
with the standard C compiler on iX86 (Linux) platforms, e.g.:
xtl : expansion de ``prop''
xtl : analyse syntaxique de ``prop''
xtl : analyse semantique de ``prop''
xtl : - reification
xtl : - liaison des types
xtl : - liaison des variables
xtl : - liaison des fonctions
xtl : - typage des expressions
xtl : traduction en C de ``prop''
xtl : creation de la bibliotheque dynamique de ``brp_protocol''
xtl : compilation C de ``prop''
/tmp/xtl_3840.c:34: initializer element is not constant
#052 erreur pendant la phase de compilation C :
compilation C de ``/tmp/xtl_3840.c'' echouee
abandon
Number: 662
Date: Tue Apr 25 13:04:53 MET DST 2000
Report: Marc Herbert (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: demos/demo_17/Makefile_compo, demos/demo_24/Makefile
Nature: The Makefile_compo file of demo_17 would erase the file
SERVICE_WITHOUT_CRASHES.bcg, which is needed for verification.
The Makefile of demo_24, when given option "cleanall" would
erase the source LOTOS programs. This problem was fixed and
the "cleanall" option was renamed into "clean".
Number: 663
Date: Tue May 9 20:30:00 MET DST 2000
Report: Lynn Blair (Lancaster University, UK)
Richard Harrison (Lancaster University, UK),
Le Duc Hoa (Univ. Toulouse 1, France),
Brian Ross (Univ. of Glasgow, UK),
Cesar Viho (INRIA/PAMPA)
Author: Hubert Garavel (INRIA/VASY)
Files: src/installator/*, installator.shar, installator.com,
INSTALLATION_0
Nature: Several problems reported in the most recent versions of
Installator for Windows and Linux have been fixed:
- The new versions of Installator emit an error message if one
tries to execute them on a wrong machine architecture, e.g.:
this version of Installator was designed for architecture
iX86; it cannot be executed on architecture sun5
- For Windows systems, the file "installator.shar" was renamed
into "installator.com", because Internet Explorer does not
recognize the ".shar" suffix as a special file and displays
it directly in the browser window. Changing ths ".shar"
suffix to ".com" makes Internet Explorer not display the
contents, and propose to execute it or to save it to a file.
- For Windows systems with Cygwin32, the INSTALLATION_0 file
was extended with a "ln -s gunzip uncompress" instruction,
as the "uncompress" command is not present by default in
Cygwin beta-version 20.1.
- For Windows systems with Cygwin32, the CADP documentation now
mentions that the environment variable CYGIWN must be set to
"binmode" before invoking Installator, otherwise all calls
to "uncompress" will fail with the following error message:
uncompress: stdin: corrupt input
restore of xxx failed
because "\n" are replaced with "\r\n" if the variable CYGWIN
is not set to "binmode".
- For Linux systems, the new version of Installator is careful
enough to override the "noclobber" option that might have
been set by the user (when set, this option would make
Installator fail).
- For Linux systems, the new version of Installator fixes a bug
that would (sometimes) cause the following error messages:
: command not found
: not a legal variable name
(this bug was due to the fact that the shell code generated
by the "shar" command of the "sharutils" package is not
accepted by the "bash" shell used by Linux).
- For Linux systems, the new version of Installator fixes a bug
that would (sometimes) cause the following error messages:
bgerror failed to handle background error.
Original error: syntax error in expression
"double(round((double(93%)/(1024))*10))/10"
Error in bgerror: invalid command name "bgerror"
(this bug was due to the fact that de "df" command of Linux
is not Posix-compliant by default).
Number: 664
Date: Tue May 23 18:26:15 MET DST 2000
Report: Moez Cherif (INRIA/VASY)
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: bin.*/libBCG.a, incl/bcg_predefined_declarations.h,
bcg_read_1.h, bcg_write_1.h
Nature: A portability problem was fixed in the BCG format with respect
to the encoding of floating point numbers (which, so far, are
mostly used for probabilistic and stochastic LTSs). The
encoding is not the same on little-endians and big-endians
machines, with the consequence that BCG graphs with floating-
point numbers could not be read properly on Solaris if they had
created on Linux, and vice-versa.
This problem was solved by adopting the same byte-ordering for
all the architectures. Two new functions BCG_READ_REAL() and
BCG_WRITE_REAL() have been introduce to achieve portability.
This change is upward compatible, except for BCG graphs that
have been generated on Linux and that contain floating-point
numbers: these graphs should be regenerated.
Number: 665
Date: Tue May 23 19:07:59 MET DST 2000
Report: Irina Smarandache (INRIA/VASY)
Authors: Radu Mateescu and Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a
Nature: Minor bugs have been fixed in the BCG library, which occurred
when trying to build non connected BCG graphs (i.e., BCG graphs
with states that cannot be reached from the initial state, which
is not so usual in model-checking verification). In particular,
one bug was detected in the edge table of type 4: using this
table for non-connected graphs would cause memory accesses past
the bounds of an array. This error was not visible to the
end-user; it was revealed using the Purify software.
Number: 666
Date: Tue May 23 19:32:28 MET DST 2000
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/libBCG.a
Nature: A minor bug was fixed in the BCG library. In the function
BCG_DELETE_OBJECT_TRANSITION(), there could be several calls
to function BCG_DELETE_EDGE_TABLE_2() to delete the same table,
which was more or less equivalent to deallocate several times
the same memory area. This error was not visible to the
end-user; it was revealed by the Purify software.
Number: 667
Date: Thu May 25 12:01:13 MET DST 2000
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: man/manl/caesar_graph.l, man/manl/bcg_write.l,
doc/Garavel-92-a.ps, doc/Tock-95.ps,
src/open_caesar/declarator.c, bin.*/libBCG_IO.a
Nature: The OPEN/CAESAR Reference Manual was modified to prohibit
both newline ('\n') and carriage-return ('\r') characters in
label strings produced by the functions CAESAR_PRINT_LABEL(),
CAESAR_DUMP_LABEL(), and CAESAR_STRING_LABEL(). Previously,
only carriage-returns were prohibited, which was a mistake.
This change should have no impact, as the existing OPEN/CAESAR-
compliant implementations obey this restriction already.
Moreover, most OPEN/CAESAR libraries and tools assume implictly
that labels cannot be split across several lines.
The "declarator" tool was modified, so as to check that labels
strings produced by functions CAESAR_DUMP_LABEL() and
CAESAR_STRING_LABEL() do not contain '\n' nor '\r' characters.
Similarly, the "bcg_write" API has been modified to express the
same restriction: the labels strings passed to the function
BCG_IO_WRITE_BCG_EDGE() should not contain newline or carriage-
return characters. The implementation of BCG_IO_WRITE_BCG_EDGE()
was modified so as to raise a fatal error if this pre-condition
is violated.
Finally, the Reference Manual of the BCG PostScript Format (see
doc/Tock-95.ps) has been updated accordingly: it is now
specified that a <Label> should not contain newline or
carriage-return characters.
Number: 668
Date: Thu May 25 19:23:01 MET DST 2000
Report: Alain Le Guennec (INRIA/PAMPA)
Authors: Hubert Garavel, Marc Herbert, and Radu Mateescu (INRIA/VASY)
Files: bin.*/libbcg_draw.a
Nature: The PostScript code generated by BCG_DRAW was incorrect when
a label string contained unbalanced parentheses, e.g., "GET(1".
This problem was fixed by quoting properly the parentheses and
back-quote characters in the PostScript code generated by
BCG_DRAW.
Number: 669
Date: Wed Jun 7 20:33:45 MET DST 2000
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_labels
Nature: A minor bug was fixed: when invoking commands such as:
bcg_labels -hide H.hid F
or:
bcg_labels -rename R.ren F
with a file F.bcg present in the current directory, the result
of "bcg_labels" was stored into a file named F (without ".bcg"
extension) while file F.bcg was left unchanged.
Number: 670
Date: Fri Jun 9 18:02:13 MET DST 2000
Report: Mirna Bognar (Vrije Universiteit, Amsterdam, The Netherlands)
Author: Radu Mateescu (INRIA/VASY)
Files: src/xtl/ctl.xtl
Nature: A bug in the macro-definition of the AX() operator was fixed,
which caused a syntax error in the XTL files that used the
ctl.xtl library. More precisely,
macro AX (F : stateset) : stateset = Dia (true) and
Box (F) end_macro
should read:
macro AX (F) = Dia (true) and Box (F) end_macro
Number: 671
Date: Tue Jun 13 11:23:45 MET DST 2000
Report: Jan Friso Groote (CWI, The Netherlands),
Solofo Ramangalahy (INRIA/PAMPA)
Authors: Moez Cherif, Hubert Garavel, and Marc Herbert (INRIA/VASY)
Files: src/eucalyptus/*
Nature: Several improvements and bug fixes have been brought to the
EUCALYPTUS graphical user-interface.
(a) The new BCG_MIN tool (see above #638) was integrated into
EUCALYPTUS. It can be accessed by clicking on an LTS file
(e.g., a ".bcg" file) and then selecting "Reduce".
(b) The semantics of the "Reduce" window was modified: there
is now an exclusive choice between "Reduce using BCG_MIN",
"Reduce using Aldebaran", and "Reduce using Fc2Tools". In
the previous version, both choices "Reduce using Aldebaran"
and "Reduce using Fc2Tools" were active by default, which
seemed to be a bit confusing, especially if different
equivalence relations were selected for Aldebaran and
Fc2Tools.
(c) Similarly, exclusive choices have been introduced in all
contexts where several tools can be used for the same task:
- comparison using bisimulations (Aldebaran and Fc2Tools)
- temporal logics (Evaluator 3.0 and XTL)
- deadlock detection
- livelock detection
etc.
(d) A major improvement was brought to Eucalyptus. The previous
version was basically intended to be "mono-threaded": only
a single tool could be used at a time. For instance, when
clicking on a file F1.bcg, then opening the "Reduce" window,
then clicking on file F2.bcg, and finally clicking "OK" in
the "Reduce" window would reduce F2.bcg instead of F1.bcg.
This problem was due to the fact that the last selected file
was stored in a global variable shared by all the windows.
The new version of EUCALYPTUS solves this problem, as it is
designed to be "multi-threaded": each window has a local
variable to store its selected file, which allows, for
instance, to reduce a file F1.bcg while visualizing another
file F2.bcg at the same time. However, it is forbidden to
launch the same action in parallel, e.g., to reduce graphs
F1.bcg and F2.bcg at the same time: in such case, a warning
message is emitted.
(e) If the "Help" window was previously iconified, it pops up
in the foreground when the user clicks on the "Help" button
again.
(f) When clicking on "Help/Tool Versions" and then on
"Help/Help Index", strage "\t\t\t" characters would appear
in the Help window. This minor problem was solved.
(g) When displaying the manual pages of the Fc2Tools, erroneous
'\b' would appear. This problem was solved.
(h) In the new version of EUCALYPTUS, the icon of the parent
directory ".." is always located on the left upper corner
of the left window.
(i) The new version of EUCALYPTUS displays a better error
message when the user clicks on the icon of a directory
that cannot be read or accessed.
(j) A bug was fixed in EUCALYPTUS on Linux: clicking on a
symbolic link to a directory, then on the ".." directory
would leave the interface in an inconsistent state. This
problem was due to the fact that, under Linux by default,
the "cd" command does not behave as expected with respect
to symbolic links. The problem was fixed by creating the
"$CADP/com/src/cadp_shell" shell-script. This modification
was applied to Installator as well.
(k) With the new version of EUCALYPTUS, the version number of
CADP is also displayed in the menu bar (together with the
version number of EUCALYPTUS).
(l) When executing the Fc2Tools, the superflous messages of
the form:
--- fc2min: blocks 1
--- fc2min: blocks 2
--- fc2min: blocks 3
etc.
are now filtered by EUCALYPTUS.
(m) On the icons of the left window, it is now possible to
use the 2nd and 3rd buttons of the mouse (in addition to
the 1st button). The manual page was updated accordingly.
Number: 672
Date: Fri Jun 16 22:35:28 MET DST 2000
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: bin.win32/*, com/*, man/*
Nature: The BCG tools have been ported to Windows. In particular,
the "libbcg_io.a" library was renamed into "libbcg_iodyn.a"
in order to avoid a naming conflict with the other library
"libBCG_IO.a" (as Windows filenames are case-unsensitive).
The pseudo-library "bin.win32/libm.a" was added and the
BCG manual pages have been updated.
Number: 673
Date: Tue Jun 27 09:49:36 MET DST 2000
Report: Yaroslav Usenko (CWI, The Netherlands)
Author: Hubert Garavel (INRIA/VASY)
Files: com/src/xeuca_convert
Nature: A bug was fixed in the "xeuca_convert" shell-script used
by the EUCALYPTUS graphical-interface to perform automatic
format conversion between various formats of LTSs (e.g.,
from .bcg files and vice-versa. This bug was only noticeable
on Linux systems, where it generated an error message of the
form:
cut: invalid byte or field list
Try `cut --help' for more information
and caused invalid format conversions.
Number: 674
Date: Wed Jun 28 11:24:12 MET DST 2000
Report: Alain Le Guennec (INRIA/PAMPA)
Authors: Moez Cherif, Hubert Garavel, and Marc Herbert (INRIA/VASY)
Files: bin.*/libbcg_draw.a, src/bcg_edit/bcg_edit.tcl,
Nature: BCG_DRAW and BCG_EDIT did not handle properly the case of BCG
graphs with labels containing either the backslash character
(e.g., "GATE !\") or containing parentheses that are not
balanced (e.g., "GATE !("). This problem is now solved.
Number: 675
Date: Wed Jun 28 11:24:12 MET DST 2000
Author: Moez Cherif (INRIA/VASY)
Files: com/src/xeuca_convert
Nature: Another bug was fixed in "xeuca_convert": when the input file
to convert was empty, the error code returned was incorrect
("exit 0" instead of "exit 1").
Number: 676
Date: Fri Jul 7 16:35:22 MET DST 2000
Author: Marc Herbert and Hubert Garavel (INRIA/VASY)
Files: com/bcg_draw, bin.*/libbcg_draw.a, src/bcg_draw/*,
src/com/cadp_postscript, src/com/cadp_psbox,
man/*/bcg_draw.l, INSTALLATION_2, com/tst
Nature: The BCG_DRAW tool was ported to Windows. This required several
changes:
- A new environment variable $CADP_PS_INTERPRETER was defined
(see its definition in the INSTALLATION_2 file).
- The "cadp_postscript" shell-script was modified to support
the Gswin32/Gsview software for Windows.
- A new script "cadp_psbox" was introduced to compute the
bounding box of PostScript files. The files
"src/bcg_draw/bcg_draw_bounding_box.ps" and
"src/bcg_draw/bcg_draw_showpage.ps" have been removed as
they are useless now. The new bounding box computation is
now 10-20% times faster.
- Both "cadp_postscript" and "cadp_psbox" have been enhanced
so that, when $CADP_PS_VIEWER or $CADP_PS_INTERPRETER are not
defined, the PostScript tools are searched in the value of
$PATH as well as in several plausible default locations.
- The "bcg_draw" manual page was updated accordingly.
- The "tst" script was extended to check the value of both
variables $CADP_PS_VIEWER and $CADP_PS_INTERPRETER.
Number: 677
Date: Thu Jul 13 10:37:44 MET DST 2000
Author: Moez Cherif and Hubert Garavel (INRIA/VASY)
Files: com/bcg_edit, src/bcg_edit/*,
Nature: The behaviour of BCG_EDIT was improved (especially with respect
to large graphs that take time to load):
- When invoked, the new version of BCG_EDIT immediatly displays
an empty, white window with a grid.
- When loading a graph, the new version of BCG_EDIT displays
the states and edges progressively (instead of waiting until
the whole graph is loaded). The "watch" cursor is displayed
and the menus are frozen while loading the graph.
Number: 678
Date: Mon Jul 31 14:40:09 MET DST 2000
Report: Alain Le Guennec (INRIA/PAMPA)
Author: Hubert Garavel and Moez Cherif (INRIA/VASY)
Files: src/open_caesar/terminator.c
src/open_caesar/simulator.i, src/xsimulator/main.tcl
bin.*/exhibitor.a, bin.*/xsimulator.a
Nature: Several Open/Caesar tools (Exhibitor, Terminator, Simulator,
and Xsimulator) invoked "CAESAR_FORMAT_LABEL (1)" to obtain
detailed information about hidden labels. This worked well in
the case of LOTOS, but not for other Open/Caesar compliant
compilers (such as the UMLAUT compiler for UML), for which
CAESAR_MAX_FORMAT_LABEL () is equal to 0 (which is permitted
by the "caesar_graph" API). All the aforementioned tools have
been modified to solve the problem.
Number: 679
Date: Thu Aug 24 20:45:29 MET DST 2000
Report: Alain Le Guennec (INRIA/PAMPA), Radu Mateescu (INRIA/VASY),
Severine Simon (INRIA/PAMPA)
Author: Hubert Garavel (INRIA/VASY)
Files: doc/Garavel-92.ps, man/*/caesar_graph.*
Nature: Several typographic corrections have been brought to the
reference documentation of the "caesar_graph" API. This should
result in a better document, especially for new readers. The
most significant changes are the following:
- There is a better separation between LOTOS-specific notes
and the rest of the text (which is independent from LOTOS).
- The notions of "gate" and "experiment offers" in labels
are now defined explicitly.
- It is now clearly specified that CAESAR_ITERATE_STATE() does
not allocate its parameters CAESAR_S2 and CAESAR_L.
- It is now forbidden for all the functions and procedures
specified in the Open/Caesar API to perform side-effect
input/output operations affecting the standard input and
standard output. In particular, debugging information should
be sent to the standard error or, preferably, to a named log
file. Otherwise, some Open/Caesar application programs that
rely on the standard input and output might not function
properly if the graph module performs conflicting accesses
to the standard input or the standard output.
Number: 680
Date: Tue Aug 29 00:03:53 MET DST 2000
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_io, bin.*/bcg_labels, bin.*/bcg_min,
incl/bcg_file_1.h
Nature: A bug was fixed in the tools BCG_IO, BCG_LABELS, and
BCG_MIN, which occured when these tools were called with the
same input and output files (e.g., "bcg_min -strong foo.bcg").
This bug was twofold:
- It could be the case that the "foo.bcg" file was read and
written at the same time. This problem was solved using an
intermediate temporary file.
- When replacing the input file with the output one, the dynamic
library [email protected] was left unchanged in the current directory.
This could be a problem, because [email protected] was related to the
original file, but not the modified one. The solution is to
remove [email protected].
Number: 681
Date: Tue Aug 29 00:07:53 MET DST 2000
Report: Nicolas Zuanon (BULL/DYADE)
Author: Hubert Garavel (INRIA/VASY)
Files: com/caesar.aldebaran
Nature: In the "caesar.aldebaran" shell-script used for compositional
verification, minimization of BCG graphs is now performed using
BCG_MIN rather than Aldebaran.
Number: 682
Date: Wed Aug 30 11:43:17 MET DST 2000
Authors: Holger Hermanns (Univ. of Twente), Hubert Garavel and Moez
Cherif (INRIA/VASY)
Files: bin.*/bcg_min, man/*/bcg_min.*
Nature: The BCG_MIN tool was improved and modified:
- The syntax of probabilistic and stochastic labels was
simplified: these labels are now written "rate 2.0" and
"prob 0.5" (instead of "rate !2.0" and "prob !0.5" as
formerly). The manual page was updated.
- An existing BCG graph FILE.bcg can be upgraded to the new
label syntax using the following command:
bcg_labels -rename -partial UPGRADER.ren FILE.bcg
where file "UPGRADER.ren" has the following contents:
---------------------------------
rename
"[ ]*rate[ ]*![ ]*" -> "rate "
"[ ]*prob[ ]*![ ]*" -> "prob "
---------------------------------
- The parsing of probabilistic and stochastic labels has been
made faster. In the new version of BCG_MIN, labels are parsed
only once, even if they occur in several transitions.
- The new version of BCG_MIN issues an error message when
option "-prob" or "-rate" is set and when the graph contains
a label containing only spaces or blank characters.
Number: 683
Date: Thu Aug 31 22:07:29 MET DST 2000
Author: Hubert Garavel (INRIA/VASY)
Files: incl/bcg_standard.h
Nature: The following line:
#include <varargs.h>
was deleted from file "bcg_standard.h". This line caused
problems with Linux because <varargs.h> is uncompatible
with <stdargs.h> and C++'s <stream.h>. Applications using
<varargs.h> should include it directly, instead of relying
directly on "bcg_standard.h".
Number: 684
Date: Mon Sep 4 12:41:51 MET DST 2000
Report: Howard Bowman (University of Kent at Canterbury, UK)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar, bin.*/caesar.adt
Nature: A cryptic error message of CAESAR and CAESAR.ADT:
variable or constant operation 10 was not declared
was replaced by a more informative one:
operation 10 used in value:
X + 10
the profile of which might be:
-> NAT
was not declared
Number: 685
Date: Wed Sep 20 17:00:45 MET DST 2000
Report: Radu Mateescu (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: man/*/caesar_edge.*, man/*/bcg_read.*
Nature: The manual pages were modified to specify that the C
instructions "break" and "continue" can be used in the loops
built using the iterators exported by the "bcg_read" and
"caesar_edge" APIs.
Number: 686
Date: Wed Sep 20 19:21:23 MET DST 2000
Report: Holger Hermanns (Univ. of Twente),
Thierry Jeron (INRIA/PAMPA),
Sheldon Lee Wen (Univ. of Lethbridge),
Jacques Sincennes (Univ. of Ottawa)
Authors: Hubert Garavel and Marc Herbert (INRIA/VASY)
Files: bin.iX86/*, bin.win32/*
Nature: Some CADP tools did not work properly on laptop computers
running Linux or Windows, because when these computers are
connected to or disconnected from the Internet, their IP address
changes dynamically. This problem was solved. A similar problem
was solved regarding the computation of "hostid" on Linux.
Number: 687
Date: Tue Oct 24 10:58:20 MET DST 2000
Report: Moez Cherif (INRIA/VASY), Nicolas Zuanon (BULL/DYADE)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a
Nature: A bug was fixed, which caused some BCG tools to emit the
following error message
bcg_temporary: error in BCG_CLEANUP
followed by a core dump.
Number: 688
Date: Tue Oct 24 12:15:24 MET DST 2000
Authors: Holger Hermanns (Univ. of Twente), Moez Cherif and Hubert
Garavel (INRIA/VASY)
Files: bin.*/bcg_min, man/*/bcg_min.*
Nature: The BCG_MIN tool was improved:
- The new version handles mixed labels of the form:
"label ; rate 2.0"
and
"label ; prob 0.5"
in which a "normal" label is combined with stochastic or
probabilistic data. The manual page of BCG_MIN was updated
and significantly improved to describe this change.
- Some error messages have been made more explanative, e.g.:
bcg_min: error when parsing label "rate 0.0000001"
rate value should be strictly positive
(comparisons are done with precision epsilon = 0.001000)
bcg_min: error when parsing label "prob 0.0000001"
probability value should belong to the range ]0..1]
(comparisons are done with precision epsilon = 0.001000)
Number: 689
Date: Fri Oct 27 11:26:36 MET DST 2000
Report: Moez Cherif (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: src/open_caesar/simulator.i, src/open_caesar/simulator.c,
bin.*/xsimulator.a
Nature: The SIMULATOR and XSIMULATOR tools did not work properly in
some cases: when the computation of a transition going out from
the current state failed (because the evaluation of a data
expression raised an exception, i.e., a signal 15), the
simulators would still permit to proceed to the next state,
which caused a core dump. This problem was fixed: moving to
the next state is now forbidden.
Moreover, on Solaris 2.*, only the first signal 15 was
caught; subsequent signals 15 were not, causing the simulators
to stop abruptly. This second problem was also fixed.
Number: 690
Date: Sat Oct 28 23:28:20 MET DST 2000
Author: Hubert Garavel (INRIA/VASY)
Files: src/com/cadp_cc, bin.*/*, com/bcg_draw, com/bcg_info,
com/bcg_open, com/caesar.open, com/exp.open, com/fc2open,
com/tst, INSTALLATION_2
Nature: To achieve portability of CADP to Windows, the conventions
regarding the C compiler (and namely the environment variable
$CADP_CC) have been deeply revised. There were indeed a problem
with the former semantics of $CADP_CC: when $CADP_CC was not
defined, its default value was "cc". On Windows/Cygwin32, there
is no "cc" command, only "gcc"; moreover, it was not sufficient
to set "$CADP_CC" to "gcc", as more compiler options (e.g.,
"-mno-cygwin" and linking options) had to be provided when
invoking the C compiler.
A new shell-script "cadp_cc" was developed. This script invokes
the C compiler, using the $CADP_CC environment variable, if it
is defined to fetch the C compiler, or, if not, attempting to
locate the C compiler automatically.
All the CADP tools and shell-scripts have been modified to
invoke "cadp_cc" systematically (instead of "${CADP_CC:-cc}"
as previously).
The "cadp_cc" script simplifies the configuration task by the
end-users, as in most cases, it is no longer needed to set the
$CADP_CC environment variable (this variable should only be set
if the operating system is Solaris, if the Sun C compiler is
not installed and if the Gcc compiler can not be accessed from
the $PATH and not installed in a standard location).
The INSTALLATION_2 file was updated to reflect these changes.
The "tst" command was modified to check the value of $CADP_CC.
Number: 691
Date: Sat Oct 28 23:28:20 MET DST 2000
Report: Marc Herbert (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: com/tst, src/com/cadp_edit, src/com/cadp_web,
INSTALLATION_2
Nature: The installation procedure was simplified. It is no longer
advised to set the environment variable $LD_LIBRARY_PATH,
unless on Solaris 2. The INSTALLATION_2 file and the "tst"
shell-script have been enhanced to reflect these changes. In
particular, on Solaris 2 machines, the new version of "tst"
checks whether "/usr/lib" and "/usr/openwin/lib" are listed in
$LD_LIBRARY_PATH.
Number: 692
Date: Sun Oct 29 16:32:28 MET 2000
Report: Marc Herbert (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: src/com/cadp_cpp, com/tst, demos/demo_19/start,
INSTALLATION_2
Nature: A new shell-script named "cadp_cpp" was developed, which
invokes the C preprocessor depending on the architecture rather
than invoking "cpp" directly (which is not recommended on GNU
environments). Demo 19 was modified to use this new script.
The installation directives given in file INSTALLATION_2 have
been simplified. On Solaris 2 machines, it is no longer needed
to include "/usr/ccs/lib" in the $PATH because "cpp" will be
located and invoked directly by "cadp_cpp". On Linux machines,
for the same reason, it is no longer required to include "/lib"
in the $PATH.
The "tst" command was simplified: it no longer checks the
availability of the "cpp" and "ld" commands.
Number: 693
Date: Wed Nov 1 09:39:14 MET 2000
Report: Hubert Rappold (University College Dublin, Ireland),
Solofo Ramangalahy (INRIA/PAMPA)
Author: Hubert Garavel (INRIA/VASY)
Files: com/tst, INSTALLATION_2
Nature: The "tst" shell-script was enhanced to emit a warning
message when run on an obsolete version of Linux, especially
a Debian release whose number is < 2.2 or a RedHat release
whose number is < 6.0. Those obsolete versions of Linux have a
bogus C library (e.g. libc6 version glibc2.0.7 on Debian 2.1)
that cause $CADP/tcl-tk/bin.iX86/wish to abort with core dump.
Number: 694
Date: Wed Nov 1 15:29:03 MET 2000
Report: Solofo Ramangalahy (INRIA/PAMPA)
Authors: Hubert Garavel and Marc Herbert (INRIA/VASY)
Files: com/tst, INSTALLATION_2
Nature: The installation directives given in file INSTALLATION_2 have
simplified. On Linux and Windows systems, it is no longer
recommended to set the environment variable $MANPATH. The "tst"
shell-script was enhanced to display the value of $MANPATH and
to emit a warning if this variable is set when not appropriate.
Number: 695
Date: Thu Nov 2 11:01:32 MET 2000
Report: Solofo Ramangalahy (INRIA/PAMPA)
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/evaluator.a
Nature: A bug was fixed in the EVALUATOR model-checker. This bug
caused a segmentation fault when the name of the .mcl file
containing the formula to evaluate was given as an absolute
pathname (i.e., starting with "/"). The problem did not occur
in the common case where a relative pathname was used.
Number: 696
Date: Fri Nov 3 16:41:20 MET 2000
Authors: Moez Cherif, Hubert Garavel, Bruno Hondelatte, and Pierre
Kessler (INRIA/VASY)
Files: bin.*/ocis.a, tcl-tk/com/tixwish, tcl-tk/bin.*/tix*,
tcl-tk/lib-tix, src/eucalyptus/eucalyptus.tcl
Nature: A new simulator named "OCIS" (Open/Caesar Interactive
Simulator) was added to the CADP release. This simulator
reliens upon the Tix extension of Tcl-Tk, which has been
included in the CADP release. OCIS can be invoked with the
same syntax as any other Open/Caesar application program.
It can also be started from the EUCALYPTUS graphical
user-interface using the "Execute / Advanced Simulation" menu.
Number: 697
Date: Fri Nov 3 19:21:05 MET 2000
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: bin.*/bcg_*, bin.*/libBCG.a, bin.*/libbcg_*, com/bcg_*,
bin.*/caesar, bin.*/caesar.adt, bin.*/xtl, com/xeuca,
demos/demo_05/Makefile, demos/demo_12/Makefile,
demos/demo_16/=READ_ME.txt, demos/demo_19/start,
man/*/bcg*, man/*/caesar.*, man/*/caesar.adt.l,
man/*/xeuca.*, man/*/xtl.*, INSTALLATION_2
Nature: For all the CADP tools having a "-cc" option (namely the
BCG tools, CAESAR, CAESAR.ADT, and XTL), the semantics of the
argument following "-cc" has been modified.
Previously, the argument following "-cc" was assumed to be a
C compiler name possibly followed by compiler options (e.g.,
-cc 'gcc -O -lm'). From now on, the compiler name must not be
specified, as it is determined by the "cadp_cc" shell-script
and the environment variable CADP_CC. Therefore, the argument
following "-cc" can only be a list of compiler options (e.g.,
-cc '-O -lm').
All the manual pages and demo examples have been updated.
The EUCALYPTUS graphical user-interface has been updated too:
the "Execution Files" and "C Compiler" windows for CAESAR,
CAESAR.ADT, and XTL have been renamed into "Miscellaneous
Options" and "C Compiler Options" respectively.
Number: 698
Date: Tue Nov 7 11:42:31 MET 2000
Report: Axel Belinfante and Jan Tretmans (Univ. of Twente),
Nicolas Zuanon (BULL/DYADE)
Author: Hubert Garavel (INRIA/VASY)
Files: src/eucalyptus/eucalyptus.tcl
Nature: The format of the .xeucarc file used by EUCALYPTUS had a
defect: the Screen_Background image was stored with an absolute
pathname (this caused a problem when moving the .xeucarc file
from one machine to another one). Moreover, the EUCALYPTUS
interface did not start if the value of Screen_Background
refers to a non-existing file.
This problem was solved. The value of Screen_Background is no
longer be stored as an absolute pathname if the background
image is located in $CADP/src/eucalyptus/frames. Additionally,
if the value of Screen_Background does not refer to an existing
image file, then EUCALYPTUS will start with the default image
"clouds1.gif".
Number: 699 Date: Tue Nov 7 14:49:02 MET 2000 Author: Hubert Garavel (INRIA/VASY) Files: bin.*/libBCG.a Nature: In some circumstances, the dynamic library [email protected] associated to a BCG file FILE.bcg could become out-of-date with respect to FILE.bcg (for instance, after a command such as: mv TEST.bcg FILE.bcg which modifies FILE.bcg but not [email protected]). This would leave the user's environment in an inconsistent state. The identification string contained in each dynamic library [email protected] associated to a BCG file FILE.bcg has been enriched with additional information (including the version number of the BCG environment, the device number, the inode number, and the time of last modification of FILE.bcg). So, every upgrade of the BCG environment or any modification of FILE.bcg will render [email protected] obsolete, so that [email protected] will be regenerated as soon as a BCG tool is applied to FILE.bcg.
Number: 700
Date: Wed Nov 8 10:41:11 MET 2000
Report: Frederic Lang (INRIA/VASY)
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/bcg_io, bin.*/libBCG_IO.a
Nature: A bug was fixed in the BCG_IO tool: the translation to the FC2
format was incorrect when the LTS to translate had a single
state and no transitions (the FC2 format generated was
syntactically incorrect).
Number: 701
Date: Wed Nov 8 17:38:39 MET 2000
Report: Christophe Discours (INRIA/VASY), Nicolas Zuanon (BULL)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/exp2c, bin.*/libexpopen.a
Nature: A bug was fixed in the EXP.OPEN tool: the "behaviour" keyword
of the EXP format was not taken into account, so that labels
strings were always handled in a case-sensitive way.
Number: 702
Date: Thu Nov 9 10:47:48 MET 2000
Report: Radu Mateescu (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: com/bcg_open, com/exp.open, com/fc2open
Nature: A bug was fixed in various shell-scripts: BCG_OPEN, EXP.OPEN,
and FC2OPEN fetched ".o" and ".a" file in a wrong directory
($SRC instead of $BIN).
Number: 703
Date: Thu Nov 9 12:35:36 MET 2000
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/evaluator.a
Nature: The EVALUATOR model-checker has been improved in order to work
more efficiently when verifying temporal formulas on explicit
LTSs encoded as BCG files. The optimisations have been made
by taking plain advantage of the functionalities offered by
the BCG environment. As a result, the memory consumption and
the execution time of EVALUATOR have been reduced by up to
5% and 20%, respectively.
Number: 704
Date: Thu Nov 9 14:29:12 MET 2000
Report: Holger Hermanns (Univ. of Twente)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a
Nature: The low-level BCG functions have been modified: every time
a BCG file FILE.bcg is open for writing (this can be done using
the BCG_OPEN_BINARY() or BCG_IO_WRITE_BCG_BEGIN() functions),
all the existing dynamic libraries named [email protected], [email protected]...
(if any) will be removed. This removal will clean the user's
environment automatically.
Number: 705
Date: Thu Nov 9 18:45:42 MET 2000
Authors: Judi Romijn (Univ. of Nijmegen), Radu Mateescu (INRIA/VASY)
Files: demos/demo_27
Nature: A new demo (Philip's HAVi Protocol) was added to the CADP
distribution.
Number: 706
Date: Mon Nov 13 15:34:53 MET 2000
Report: Hubert Garavel (INRIA/VASY), Radu Grosu (SUNY Stony Brook, USA)
Author: Radu Mateescu (INRIA/VASY)
Files: demos/demo_01/*.{mcl,xtl}, demos/demo_02/*.{mcl,xtl}
Nature: The demos demo_01 and demo_02 (Alternating Bit Protocol without
and with data values, respectively) have been improved in order
to allow a better understanding of temporal logic properties.
The temporal formulas stating the correctness of the LOTOS
specifications, written in XTL and in regular alternation-free
mu-calculus (the input language of EVALUATOR), have been
simplified: the old, monolithic formulas have been split into
several smaller formulas, each one expressing a simpler
property of the protocol. For completeness, the old formulas
were also kept, but rewritten using simpler notations.
Number: 707
Date: Mon Nov 13 17:54:59 MET 2000
Author: Hubert Garavel (INRIA/VASY)
Files: com/tst, INSTALLATION_2
Nature: The "tst" shell-script was ported to Windows and enhanced to
perform additional verifications:
- It displays and checks the values of $EDITOR, $NAVIGATOR,
$CADP_PS_VIEWER, and $CADP_PS_INTERPRETER.
- It checks more deeply the value of $CADP_CC. In particular,
it warns the user about the use of "/usr/ucb/cc" on sun4 and
sun5, as stated in the file INSTALLATION_2.
- On Windows systems, it performs various verifications to
ensure that the version of Cygwin installed is up to date
and has been patched appropriately to remove known bugs.
- It checks that the license is valid, that the user's "umask"
value, and that the user's shell startup file (".bashrc",
".profile", ".cshrc"...) executes correctly, does not write
to the standard output, and does not overwrite the value of
the $PATH variable (all these configuration problems have
proven to create problems when installing or running the CADP
tools).
Number: 708
Date: Mon Nov 14 11:02:13 MET 2000
Report: Sari Mannynsalo (Nokia Research Center, Finland)
Author: Hubert Garavel (INRIA/VASY)
Files: com/tst, INSTALLATION_2
Nature: The new version of "tst" warns about the incompatibilities
between multiple versions of CADP installed on the same
machine, especially the case where the $CADP variable points
to one version of CADP whilst the $PATH variable gives access
to commands that belong to another version of CADP.
Number: 709
Date: Wed Nov 15 19:23:15 MET 2000
Report: Solofo Ramangalahy (IRISA/PAMPA), Radu Mateescu (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/bcg_io, bin.*/bcg_min, man/*/bcg_io.*, man/*/bcg_min.*,
src/eucalyptus/eucalyptus.tcl, src/com/xeuca_convert
Nature: The "-parse" option of BCG_IO, BCG_MIN, and TGV was a bit
confusing: selecting this option meant that labels would not be
parsed. Moreover, the "-parse" option of BCG_IO could only be
used when the input file was in Aldebaran format (but not when
the input file was in SEQUENCE format, for instance), although
this option mainly concerns the output file in BCG format (not
the input file).
In BCG_IO, two new options named "-parse" and "-unparse" have
been introduced to control the production of output files in
BCG format. Option "-parse" (resp. "-unparse") specifies that
labels will be parsed (resp. will not be parsed) when building
the output BCG file. By default, labels are parsed. In
particular, the new version of BCG_IO can be used to parse or
unparse the labels of an existing BCG file.
The "-parse" option of BCG_IO associated to input files in
Aldebaran format becomes obsolete, but is kept (with its
previous semantics) for backward compatibility. Using this
option is strongly discouraged as it may disapear from further
CADP releases.
The "Convert" functionality of the EUCALYPTUS user interface
was updated accordingly. It now offer the choice between two
formats: "BCG (With Label Parsing)" and "BCG (Without Label
Parsing)". A bug in the "xeuca_convert" shell-script that
occurred when generating "-ascii -small" and "-fc2 -verbose"
formats was fixed.
The "-parse" option of BCG_MIN was removed: from now on, the
labels of the minimized LTS produced by BCG_MIN are parsed iff
they were already parsed in the original LTS to minimize.
The manual pages of BCG_IO or BCG_MIN have been updated.
Number: 710
Date: Wed Nov 22 11:49:18 MET 2000
Authors: Radu Mateescu and Irina Smarandache (INRIA/VASY)
Files: demos/demo_{08,11,20}/REL_REL_FIFO.lib
Nature: The demos demo_08, demo_11, and demo_20 on the rel/REL
protocol have been improved by eliminating a data type
TABLE that was defined in the file REL_REL_FIFO.lib but
not used in the LOTOS specification.
Number: 711
Date: Wed Nov 29 14:32:56 MET 2000
Author: Hubert Garavel (INRIA/VASY)
Files: doc/Garavel-Viho-Zendri-00.ps
Nature: A new paper (describing how LOTOS and the CADP tools can be
used for system-level design of hardware systems) was added to
the CADP release.
Number: 712
Date: Mon Dec 11 11:14:32 MET 2000
Report: Ghassan Chehaibar (BULL/DYADE)
Authors: Hubert Garavel (INRIA/VASY) and Laurent Mounier (VERIMAG)
Files: bin.*/projector.a, bin.*/aldebaran, bin.*/exp2c,
bin.*/libexpopen.a
Nature: A bug was fixed in the PROJECTOR tool: when generating an
LTS file with more than 10,000,000 states and 10,000,000
transitions, the ".aut" file generated by PROJECTOR was not in
a proper format: the first line ("des") would overwrite the
second line. The same change was made in ALDEBARAN and
EXP.OPEN.
Number: 713
Date: Mon Dec 11 16:32:19 MET 2000
Authors: Hubert Garavel (INRIA/VASY) and Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran, bin.*/exp2c, bin.*/libexpopen.a
Nature: The new version 6.5 of ALDEBARAN reads and writes BCG files
directly. The previous version 6.4 of ALDEBARAN could read BCG
files, but only by translating them implicitly to ".aut" files
using the BCG_IO tool. This translation step was slow and is
now avoided by a direct use of the "bcg_read"/"bcg_write"
interface.
The new versions of ALDEBARAN and EXP.OPEN now accept ".exp"
files containing leaf automata encoded in an other format than
".aut". In particular, leaf automata can be encoded in BCG
format, which is read directly using the "bcg_read" interface.
Finally, ALDEBARAN and EXP.OPEN have been enhanced to read
other formats than ".aut" and ".bcg", for instance ".fc2" and
".seq" (the translation is done implicitly using BCG_IO).
Number: 714
Date: Tue Dec 12 10:12:19 MET 2000
Authors: Hubert Garavel (INRIA/VASY) and Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: An inappropriate error message of ALDEBARAN was removed.
When invoked on a non-existent file FILE.bcg,
aldebaran -info FILE.bcg
no longer displays
Aldebaran fatal error: Unknown implementation file type
but
Aldebaran fatal error: cannot read file "FILE.bcg"
Number: 715
Date: Tue Dec 12 11:32:56 MET 2000
Report: David Jacquemin (INRIA/VASY)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: In the ".aut" format, the initial state must always be numbered
zero. The previous version 6.4 of ALDEBARAN could give an
incorrect result when trying to minimize a ".aut" file in which
the initial state of the LTS was different from zero. This
problem is fixed: in such case, the new version of ALDEBARAN
prints an an error message ("the initial state must always be
numbered 0") and stops.
Number: 716
Date: Tue Dec 12 17:12:19 MET 2000
Report: Christophe Discours, Radu Mateescu (INRIA/VASY) and
Wayne Biao Liu (University of Waterloo, Ontario, Canada)
Authors: Hubert Garavel (INRIA/VASY) and Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: A bug was fixed in ALDEBARAN: when taking a ".bcg" file
as input and producing a minimized ".aut" file as output, the
previous version of ALDEBARAN forgot to surround labels with
double quotes ("..."): as a consequence, the generated ".aut"
files could not be parsed by BCG_IO.
Moreover, ALDEBARAN and BCG_IO did not interpret the ".aut"
format with exactly the same conventions. Both tools have been
aligned, so that ALDEBARAN now follows the same conventions
as BCG_IO. In particular, two labels with the same string are
now considered as identical, whether surrounded by double
quotes or not: for instance, A and "A" are identical, i and "i"
are identical, etc.
Number: 717
Date: Tue Dec 12 19:04:31 MET 2000
Report: Marc Herbert (INRIA/VASY)
Authors: Hubert Garavel (INRIA/VASY) and Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: A bug was fixed in ALDEBARAN: due to a buffer overflow, the
"-output FILENAME.bcg" option would not work on Linux: instead
of generating a BCG file named "FILENAME.bcg", ALDEBARAN
would generate a file named "FILENAME.bcg^A" (where ^A is the
<Control-A> character) containing corrupted lines in ".aut"
format. This bug would cause demo_15, demo_16, and demo_25
to fail on Linux.
Number: 718
Date: Thu Dec 14 09:44:20 MET 2000
Report: Hubert Garavel (INRIA/VASY)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: A bug was fixed in ALDEBARAN: when invoked with not enough
arguments, as in:
aldebaran -path
or
aldebaran -path 1
the previous version of ALDEBARAN would abort with a core dump.
The new version prints a proper error message:
"Aldebaran fatal error: Command -path needs 2 arguments"
Number: 719
Date: Thu Dec 14 11:43:41 MET 2000
Report: Charles Pecheur (INRIA/VASY)
Authors: Hubert Garavel (INRIA/VASY) and Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: In the previous version of ALDEBARAN, the "-dead" option
printed at most 20 deadlock states. The new version of
ALDEBARAN prints all the existing deadlock states.
Number: 720
Date: Thu Dec 14 14:02:38 MET 2000
Report: Izak van Langevelde (CWI)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: A mistake was fixed in ALDEBARAN diagnostic messages:
when comparing two non-equivalent graphs modulo observation
equivalence, the diagnostic printed was:
"LTSs 1.aut and 2.aut are not related modulo safety preorder."
The new version of ALDEBARAN prints the correct diagnostic:
"LTSs 1.aut and 2.aut are not related modulo observational
equivalence."
Number: 721
Date: Thu Dec 14 15:53:48 MET 2000
Report: Hubert Garavel (INRIA/VASY)
Author: Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran
Nature: Another mistake was fixed in ALDEBARAN diagnostic messages:
when comparing on the fly two non-equivalent graphs modulo
branching bisimulation ("-pequ -fly"), the diagnostics
generated by ALDEBARAN were incorrect (wrong sequences, wrong
state numbers).
Number: 722
Date: Thu Dec 14 16:50:00 MET 2000
Authors: Hubert Garavel and Marc Herbert (INRIA/VASY)
Files: bin.*/aldebaran, man/*/aldebaran.*,
src/eucalyptus/eucalyptus.tcl
Nature: The default value of ALDEBARAN's "-bddsize" option was
increased from 4 to 64 Mbytes, so as to reflect the increased
capabilities of modern hardware. The manual page was updated.
In the EUCALYPTUS user-interface, it is now possible to select
the value of bddsize in the range 0...690 (the former range
was 0...64).
A cryptic error message of ALDEBARAN:
"Error : Sorry: bdd::not enough memory"
was enhanced:
"Error : Sorry, not enough memory allocated for BDDs.
Use -bddsize option to increase the amount of memory".
Number: 723
Date: Thu Dec 14 17:47:12 MET 2000
Authors: Aline Senart and Laurent Mounier (VERIMAG)
Files: bin.*/aldebaran, man/*/aldebaran.*
Nature: Three new options "-pmin -std", "-pequ -std" and "-pcla -std"
have been added to ALDEBARAN: these options allow to reduce
and compare graphs modulo branching bisimulation, using the
algorithm of Groote and Vaandrager.
Number: 724
Date: Fri Dec 15 16:50:00 MET 2000
Authors: Hubert Garavel and Laurent Mounier (INRIA/VASY)
Files: bin.*/aldebaran
Nature: When invoked on an erroneous ".aut" file that happened to
be empty, the previous version of ALDEBARAN would abort with
a core dump. This problem is fixed now: in such case, a proper
error message will be displayed:
"Aldebaran fatal error: invalid descriptor line in file "F.aut"
Number: 725
Date: Mon Dec 18 15:20:51 MET 2000
Report: Solofo Ramangalahy (IRISA)
Author: Radu Mateescu (INRIA/VASY)
Files: man/manl/evaluator.l
Nature: The manual page of EVALUATOR 3.0 has been improved by defining
more precisely the relative priorities of all boolean and
regular operators contained in temporal formulas.
Number: 726
Date: Mon Dec 18 16:23:52 MET 2000
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: src/eucalyptus/eucalyptus.tcl
Nature: The EUCALYPTUS user-interface has been enriched with new
livelock detection features:
- A "Find livelocks" menu entry was added for ".lotos" and
".LOTOS" files (livelocks are searched on-the-fly using
EVALUATOR 3.0).
- For ".exp" files, one can now search for livelocks using
EVALUATOR 3.0 as an alternative to Aldebaran.
- For ".aut", ".bcg", ".fc2", and ".seq" files, one can now
search for livelocks using EVALUATOR 3.0 as an alternative
to Aldebaran and Fc2Tools.
Number: 727
Date: Tue Dec 19 17:23:14 MET 2000
Report: Gavril Godza (Polytechnic University of Bucarest, Romania),
Frederic Perret (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.win32/libBCG.a, bin.win32/bcg_min
Nature: A bug of BCG_MIN on Windows was fixed: when typing
bcg_min -strong SOURCE.bcg DEST.bcg
if the file DEST.bcg already existed, it was not modified:
instead, SOURCE.bcg file was modified, exactly as if the
following command had been typed:
bcg_min -strong SOURCE.bcg
Number: 728
Date: Tue Dec 19 19:21:42 MET 2000
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/caesar
Nature: A significant change has been brought to the Petri net model
used internally by the CAESAR compiler (this model was defined
formally in [Garavel-89-c] and later summarized in the paper
[Garavel-Sifakis-90]). In this model, the action attached to
a transition is executed before evaluating the offer attached
to the transition.
This model has been extended by introducing the notion of
"reactions" attached to transitions, i.e., various actions
(variable assignment and/or variable reinitialization) that
are executed after evaluating the offer. The optimizations
operating on the Petri net model have been modified in
consequence. This extension of the network model leads to
important improvements in CAESAR 6.0:
- On many LOTOS examples, the numbers of places, transitions,
and variables of the network models generated by CAESAR are
are significantly reduced using the new model. For instance,
on an example given by Elie Najm, the number of places
decreases from 17 down to 4, the number of transitions from
60 down to 47, and the number of variables from 16 to 1.
- The reduction of the network size often causes a reduction
in size of the corresponding Labelled Transition System.
The reduction factor can be several orders of magnitude.
For instance, in the example given by Elie Najm, the size
of the corresponding LTS is reduced from 304,305 states
down to 83 states and 1,434,070 transitions down to 364
transitions.
- As a consequence, the LTS generation is also faster. On
several LOTOS examples studied by Fabrice Baray, the new
version of CAESAR is 150 times faster than the previous
one (the LTS size being approximately the same).
These improvements take place in most cases. However, in
some rare cases, the size of the network does not decrease
uniformly: for instance, the number of variables may increase
while the numbers of places and transitions decrease. In
other cases, the number of states in the LTS may decrease
while the number of transitions in the Petri net increases.
But these problems remain very minor statistically and should
not hide the benefits obtained in all other cases.
Finally, in a few cases, the speed in LTS generation may
decrease significantly. This is especially the case for
the example given in demo_19, which now runs very slowly
using CAESAR 6.0. This can be explained as follows: the
network model generated with CAESAR 6.0 is smaller in size,
but the number of epsilon-transitions has increased (while
the total number of transitions was decreasing). In the
future, this problem will be solved by implementing a new
semantics for epsilon-transitions (in preparation).
Number: 729
Date: Wed Jan 3 17:30:38 MET 2001
Authors: Hubert Garavel, Marc Herbert, Frederic Lang (INRIA/VASY)
Files: com/svl, bin.*/svl_kernel, src/svl/standard, man/*/svl.*
Nature: A new tool named SVL ("Script Verification Language") was
added to the CADP toolbox. The SVL language and its associated
compiler target at simplifying and automating the multiple
operations required for compositional verification of LOTOS
programs.
The syntax and semantics of the SVL language, as well as the
documentation of the SVL compiler are defined in the SVL
manual page (see "man svl").
The SVL tool distributed in CADP is SVL 2.0, which is an
entirely new tool. A previous version SVL 1.0 was used
internally by the VASY team, but never distributed externally.
The SVL language subsumes two other formalisms previously
used in CADP: the ``.des'' format and the ``.exp'' format.
In particular, the ``.des'' format and the DES2AUT tool are
totally replaced by the SVL approach. The DES2AUT tool and
the ``caesar.aldebaran'' shell-script are kept to preserve
compatibility, but might be removed in future versions of
CADP. Therefore, migrating from DES2AUT to SVL is strongly
advised.
On the other hand, the ``.exp'' format is kept, as several
CADP tools (ALDEBARAN, EXP2C, EXP2FC2) will continue using
this format. It is likely that SVL will make the ``.exp''
format less visible to the end users as the ``.exp'' files
will be generated automatically by the SVL compiler.
Number: 730
Date: Thu Jan 4 09:38:51 MET 2001
Authors: Hubert Garavel and Frederic Lang (INRIA/VASY)
Files: man/*/aldebaran.l
Nature: Several corrections have been brought to the ALDEBARAN manual
page:
- The ``-hide'' option no longer requires that hiding
files have a ``.hide'' extension. Any extension is
permitted, but ``.hid'' and ``.hide'' are the ones
recognized by the EUCALYPTUS interface.
- The ``-rename'' option no longer requires that renaming
files have a ``.rename'' extension. Any extension is
permitted, but ``.ren'' and ``.rename'' are the ones
recognized by the EUCALYPTUS interface.
- The rule for selecting the default method has refined:
method ``-std'' is not always the default method; in
some cases defined in the manual, ``-bdd'' or ``-fly''
can be the default.
- It is now specified that, when using ``-pequ -fly'',
one of the two filenames must be a completely generated
LTS that does not contain any "tau" transition.
Number: 731
Date: Mon Jan 8 11:50:40 MET 2001
Authors: Frederic Lang and Hubert Garavel (INRIA/VASY)
Files: bin.*/aldebaran, bin.*/exp2fc2, bin.*/exp2c,
bin.*/libexpopen.a, man/*/aldebaran.l, demos/*/*.exp
Nature: The syntax of ``.exp'' files has been enhanced:
- It is now possible to enclose file names between double
quotes. This allows to use non-alphanumeric characters
in file names, exactly as in SVL. The previous syntax
of filenames (without double quotes) is kept for
backward compatibility, but its use is now discouraged.
- It is now permitted to use parentheses in the behaviour
expressions contained in an ``.exp'' file.
- The syntax of the ``hide'' operator was made stricter:
according to the previous definition of the ``.exp''
format, it was possible to hide not only using gate
names, but also character strings, e.g.,
hide "gate !offer" in ...
The EXP2C and EXP2FC2 rejected those character strings
in ``.exp'' files. ALDEBARAN accepted them syntactically
but did not process them. The new syntax only accept gate
names in the ``hide'' operator. It is worth noticing that
the SVL language accepts both gate names, character
strings, and even regular expressions in its hiding
operator.
The ALDEBARAN, EXP2C, and EXP2FC2 have been modified to
implement these changes.
Number: 732
Date: Wed Jan 10 13:09:06 MET 2001
Author: Frederic Lang (INRIA/VASY)
Files: bin.*/exp2fc2
Nature: Due to a porting issue, the Linux version of EXP2FC2 could
loop indefinitely. This problem was fixed.
Number: 733
Date: Wed Jan 10 14:47:17 MET 2001
Report: Marc Herbert and Stephane Martin (INRIA/VASY)
Author: Frederic Lang (INRIA/VASY)
Files: bin.*/aldebaran
Nature: The parser for ``.exp'' files contained in ALDEBARAN has been
corrected. The previous parser accepted empty behaviours (and,
in particular, empty ``.exp'' files), which caused ALDEBARAN
to make a core dump.
Number: 734
Date: Fri Jan 12 12:14:12 MET 2001
Author: Frederic Lang (INRIA/VASY)
Files: bin.*/exp2c, bin.*/exp2fc2, man/*/aldebaran.*
Nature: The syntax of ``.exp'' files has been modified in two ways:
- The ``hide'' operator has been given a lower precedence
than the parallel composition operators
- The parallel composition operators have been made
associative to the right.
Due to these modifications, the conventions for ``.exp'' files
are now fully aligned with LOTOS. The definition of the
``.exp'' format in the ALDEBARAN manual page was updated.
The ALDEBARAN tool has been left unchanged in this respect
as it already implemented the new conventions. The EXP2C
and EXP2FC2 tools have been modified accordingly.
Number: 735
Date: Fri Jan 12 12:29:17 MET 2001
Authors: Frederic Lang and Hubert Garavel (INRIA/VASY)
Files: bin.*/aldebaran, man/*/aldebaran.*
Nature: The parser for ``.exp'' files contained in ALDEBARAN has been
modified so as to allow hiding operators only at the top level
of a composition expression. The previous version of the parser
allowed hiding operators occuring as operands of parallel
composition operators, which ALDEBARAN does not handle properly
(contrary to EXP2C and EXP2FC2). The definition of the ``.exp''
format in the ALDEBARAN manual page has been made more precise
in this respect.
Number: 736
Date: Fri Jan 12 17:56:41 MET 2001
Report: Wayne Liu (Univ. of Waterloo) and Marc Herbert (INRIA/VASY)
Authors: Hubert Garavel, Frederic Lang (INRIA/VASY), and Laurent
Mounier (VERIMAG)
Files: bin.*/aldebaran, man/*/aldebaran.*
demos/demo_10/=README.txt, demos/demo_11/=README.txt
Nature: The option ``-exp2aut'' of ALDEBARAN did not work well and
would sometimes abort with an error message of the form:
bcg_edge: previous state not increasing in BCG_WRITE_EDGE
This problem was solved by removing the ``-exp2aut'' option
from ALDEBARAN, as this option was redundant with the EXP2AUT
and GENERATOR tools, which provide the same functionality.
Instead of invoking
aldebaran -exp2aut INPUT.exp -output OUTPUT.bcg
one should now invoke:
exp.open INPUT.exp generator [-monitor] OUTPUT.bcg
Demos 10 and 11 have been updated to avoid using ``-exp2aut''.
Number: 737
Date: Fri Jan 12 19:21:10 MET 2001
Report: Marc Herbert (INRIA/VASY)
Authors: Frederic Lang and Hubert Garavel (INRIA/VASY)
Files: bin.*/exp2c
Nature: EXP2C would fail with an error message of the form:
exp2c: Error found in !
if the ``.exp'' file referred to an LTS file having incorrect,
unexpected contents, e.g., a ``.bcg'' file containing anything
but a BCG graph (for instance, a text file). This problem was
fixed.
Number: 738
Date: Fri Feb 2 13:00:34 MET 2001
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/caesar.adt
Nature: A bug was fixed in CAESAR.ADT: the iteration macro generated
for a single-value type T1 did not work if this type T1 was
used in another tuple type T2 (i.e., if T2 contained a field
of type T1). Due to this bug, the iteration macro for T2
did not iterate correctly over all values of tye T2.
Number: 739
Date: Thu Feb 8 19:33:39 MET 2001
Authors: Moez Cherif, Frederic Lang, and Hubert Garavel (INRIA/VASY)
Files: man/*/ocis.*
Nature: A manual page for the OCIS simulator has been produced. This
page is best viewed in HTML form (so as to display screen
snapshots, which cannot be seen when typing "man svl").
Number: 740
Date: Fri Feb 16 09:41:49 MET 2001
Report: David Fernandes Cruz Moura (Univ. Federal do Rio de Janeiro)
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: demos/demo_{01,02,15}/verify-all-requirements
Nature: A bug in the scripts that perform repeated calls of EVALUATOR
was fixed: the calls to the evaluator binary file (which was
created in the current directory) have been preceded by './'
in order to handle the case when the user's $PATH variable
does not include the current directory.
Number: 741
Date: Wed Feb 21 16:38:42 MET 2001
Report: Frederic Perret and Nicolas Zuanon (DYADE)
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/evaluator.a
Nature: The parser used in the back-end of EVALUATOR 3.0 has been
improved in order to avoid stack overflow errors of yacc.
These errors occurred during the analysis of input files
containing large formulas (several thousand operators) and
was caused by the left recursion of some grammar rules. These
rules have been rewritten using right recursion (of course,
without changing the recognized language), which does not
cause the overflow error anymore.
Number: 742
Date: Tue Mar 13 19:37:15 MET 2001
Report: Nissim Etrog (Technion, Israel), Volker Braun (Univ. of
Dortmund)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.sun5/aldebaran
Nature: ALDEBARAN would make a segmentation fault and a core dump
on some (but not all) machines running Solaris 7. The reason
was that the ALDEBARAN binary program for Sparc was statically
linked (in fact, it was only dynamically linked against the
libdl.so.1 library). The new binary is fully dynamically
linked and is a compliant SPARC binary.
Number: 743
Date: Thu Mar 15 15:27:31 MET 2001
Report: David Kendall (Univ. of Northumbria, Newcastle upon Tyne, UK)
Author: Hubert Garavel (INRIA/VASY)
Files: tcl-tk/com/tixwish, tcl-tk/bin.iX86
Nature: The Linux version of the OCIS simulator worked well on
RedHat 6.* distributions, but not on RedHat 7.* ones: it
failed with an error message of the form:
$CADP/tcl-tk/bin.iX86/tixwish: error while loading shared
libraries: libtix4.1.8.0.so: cannot open shared object
file: No such file or directory
This problem was caused the absence of dynamic libraries
needed to execute the ``tixwish'' binary distributed in
$CADP/tcl-tk/bin.iX86. This binary was replaced with a more
recent one and the appropriate libraries have been added to
the CADP distribution.
Number: 744
Date: Mon Mar 19 20:12:02 MET 2001
Report: Greg Eakman (Boston University), Bruno Ondet (INRIA/VASY)
Authors: Hubert Garavel (INRIA/VASY) with the help of Ernie Boyd
Files: src/com/cadp_cc, src/windows/gcc-crtdll-specs
Nature: The BCG tools did not work with the recent version 1.1.8
of the Cygwin software. They would fail with an error
message of the form:
seek must be permitted for a bcg_file in BCG_OPEN_BINARY
This problem was due to a recent change in the GCC compiler
version 2.95.2-6 (the option -mno-cygwin now links against
the MSVCRT library instead of the CRTDLL library) which
caused an incompatibility in the data structures used by
the fstat() function. The ``cadp_cc'' shell-script was
modified so as to continue linking against CRTDLL.
Number: 745
Date: Tue Mar 20 09:55:14 MET 2001
Report: Bruno Ondet (INRIA/VASY)
Author: Hubert Garavel (INRIA/VASY)
Nature: An error was fixed in the EUCALYPTUS graphical user
interface, the menu "Find a Path Leading to a State ..."
would stock its results in a ``.aut'' file instead of a
``.seq''. This problem was solved.
Number: 746
Date: Mon Mar 26 17:09:04 MET DST 2001
Report: Stephane Bordier (Univ. Paris XI Orsay), Nicolas Zuanon
(BULL/DYADE)
Author: Frederic Perret and Hubert Garavel (INRIA/VASY)
Files: bin.*/ocis.a, src/ocis/ocis.tcl
Nature: Several improvements have been made to the OCIS simulator:
- OCIS is now launched as a background process, so as
not to block the EUCALYPTUS graphical user-interface
when launching OCIS from the "Advanced Simulation".
- In the window open by the "Save", the "Save" and
"Ignore" buttons have been renamed into "Yes" and "No",
respectively.
- The default file "noname.bcg" for saving scenarios has
been renamed into "untitled.bcg". Also, when executing
the commands "New", "Load", "Reset" and "Quit", the
user can now choose a different name for saving the
current scenario.
- When the OCIS window is destroyed from the window manager
(by clicking on the button with a cross), a window now
pops up to ask the user if the current scenario should
be saved.
Number: 747
Date: Mon Mar 26 19:25:37 MET DST 2000
Author: Hubert Garavel (INRIA/VASY)
Files: doc/Garavel-Mateescu-Smarandache-01
Nature: A new paper on massively parallel model-checking was added
to the CADP distribution.
Number: 748
Date: Thu Mar 29 16:22:19 MET DST 2001
Authors: Frederic Lang and Hubert Garavel (INRIA/VASY)
Files: demos/=READ_ME.txt, demos/demo_01, demos/demo_10,
demos/demo_11, demos/demo_17, demos/demo_18, demos/demo_20,
demos/demo_25, demos/demo_27
Nature: To benefit from the new SVL tool, all the CADP demo examples
related to compositional verification have been modified so as
to use SVL. Concretely, all ``.des'' and ``.exp'' files, as
well as Makefiles and ``.rename'' files, have been eliminated
and replaced with (simpler and shorter) ``.svl'' files. The
corresponding =README.txt files have been updated accordingly.
Also, demo_25 has been improved by performing LTS minimization
according to branching bisimulation (using the BCG_MIN tool)
instead of observational equivalence (using the ALDEBARAN
tool). So doing, the time needed for verification is
significantly reduced.
Number: 749
Date: Mon Apr 9 14:38:10 MET DST 2001
Author: Hubert Garavel (INRIA/VASY)
Files: src/com/xeuca_man
Nature: In the Windows version of EUCALYPTUS, the "Help" menu could
fail because the GNU "man" compresses manual pages in the
"catl" directory using gzip. The "xeuca_man" shell-script
was modified to invoke gunzip when appropriate.
Number: 750
Date: Mon Apr 9 14:46:26 MET DST 2001
Author: Hubert Garavel (INRIA/VASY)
Files: com/bcg_draw, src/com/cadp_postscript
Nature: In several occasions, the Windows version of BCG_DRAW would
fail because the PostScript file generated by BCG_DRAW could
be removed before being displayed by Ghostview. This problem
occurred randomly: it was probably caused by a race condition
in the Cygwin "bash" shell. Several shell scripts have been
modified to avoid this problem.
Number: 751
Date: Mon Apr 9 15:44:16 MET DST 2001
Author: Hubert Garavel (INRIA/VASY)
Files: gc/bin.*/libgc.a
Nature: The garbage collector library was upgraded from version
4.14 to version 5.3 in order to solve a bug that caused
"caesar -gc" to create segmentation violations on Windows.
Number: 752
Date: Tue Apr 10 15:42:17 MET DST 2001
Report: Gavril Godza (Polytechnic University of Bucharest, Romania)
Author: Hubert Garavel (INRIA/VASY)
Files: com/xeuca, src/com/eucalyptus
Nature: Several problems have been fixed in the Windows version of
the EUCALYPTUS graphical user interface:
- It is now possible to enter directories (folders) the name
of which contains spaces (e.g., "Documents and Settings",
"Program Files", etc.)
- The new version of EUCALYPTUS carefully avoids creating
file names starting with "//", as these names have a
different meaning in Windows than in Unix.
- The new version of EUCALYPTUS no longer displays spurious
white lines in the right window.
- The "Visualize" menu for labelled transition systems has
been simplified and reorganized (see item #610 above).
"Draw in 2 dimensions" and "Edit in 2 dimensions" have
have been renamed into "Edit" and "Draw", respectively.
Number: 753
Date: Tue Apr 10 15:52:50 MET DST 2001
Report: Eric Madelaine (INRIA Sophia Antipolis)
Author: Hubert Garavel (INRIA/VASY)
Files: bin.*/libBCG.a, bin.*/bcg_io
Nature: A bug was fixed in the Windows version of BCG_IO: due to an
error in string allocation, some ``.aut'' files generated by
BCG_IO could contain spurious <control-D> characters.
Number: 754
Date: Tue Apr 10 20:41:24 MET DST 2001
Author: Radu Mateescu (INRIA/VASY)
Files: incl/caesar_table_1.h
Nature: In the declaration of CAESAR_CREATE_TABLE_1(), the type of
the argument CAESAR_PRINT was not aligned on the Open/Caesar
reference manual. This type was changed from
void (*) (CAESAR_TYPE_FILE, CAESAR_TYPE_TABLE_1)
to
void (*) (CAESAR_TYPE_FILE, CAESAR_TYPE_POINTER)
This change is upward compatible for all Open/Caesar appli-
cations, as CAESAR_TYPE_TABLE_1 is defined as a synonym of
CAESAR_TYPE_POINTER.
Number: 755
Date: Wed Apr 11 19:02:04 MET DST 2001
Authors: Massimo Zendri (BULL/DYADE), Hubert Garavel and Frederic
Lang (INRIA/VASY)
Files: demos/demo_28, demos/=README.txt
Nature: A new demo example (describing a simple cache coherency
protocol) has been added to the CADP distribution.
Number: 756
Date: Wed Apr 18 11:21:49 MET DST 2001
Report: Benoit Fraikin (Universite de Sherbrooke, Canada)
Author: Radu Mateescu (INRIA/VASY)
Files: src/xtl/mu_calculus.xtl
Nature: A minor error in a comment ("lfp" instead of "gfp") was
fixed.
Number: 757
Date: Fri Apr 27 14:32:21 MET 2001
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: bin.*/bcg_labels
Nature: BCG_LABELS assumed that the initial state of the input graph
was always 0. This problem was solved and BCG_LABELS now
takes into account the initial state of the input graph.
Number: 758
Date: Fri Apr 27 17:44:38 MET 2001
Authors: Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files: bin.*/bcg_io
Nature: BCG_IO did not handle properly some FC2 graphs (those for
which the initial state was different from 0 and specified
using a declaration of the form ``hX>Y'' rather than
``h"initial">Y'', where X is an entry in the logics table
of the FC2 file and Y is the number of the initial state.
This problem was solved if X=0 (assuming that the entry 0
in the logics table is "initial"). The new version of BCG_IO
should accept all FC2 files generated from Esterel programs
using the OCFC2 tool.
Number: 759
Date: Mon Jun 6 17:10:21 MET DST 2001
Author: Frederic Perret (INRIA/VASY)
Files: bin.*/ocis.a, src/ocis/ocis.tcl
Nature: The preferences specified in the OCIS startup file .ocisrc
were not taken into account. This problem was fixed.
Number: 760
Date: Thu Jun 7 12:22:48 MET DST 2001
Author: Hubert Garavel (INRIA/VASY)
Files: src/eucalyptus/eucalyptus.tcl, src/com/xeuca_ps
The EUCALYPTUS graphical interface has been improved in
three ways:
- In the menu of commands applicable to explicit LTSs, a
new command "Display Labels" was added: it prints all the
labels attached to the transitions of an LTS.
- The "Kill" button of the right window was not functioning
properly on Windows. This issue is solved.
- The options specific to CAESAR.ADT ("-trace", "-debug"...)
that the user can set using the "Options" menu were only
passed to CAESAR.ADT when this tool was invoked directly,
but not when CAESAR.ADT was called indirectly by the
"caesar.open" script. This problem was fixed.
Number: 761
Date: Thu Jun 7 16:46:47 MET DST 2001
Report: Frederic Lang (INRIA/VASY)
Author: Radu Mateescu (INRIA/VASY)
Files: bin.*/evaluator.a, bin.*/xtl, bin.*/xtl_expand
Nature: A bug was fixed in the XTL_EXPAND, XTL and EVALUATOR tools:
the preprocessed files (with extension ".xm" or ".xp")
produced by XTL_EXPAND are created in the current directory
instead of the directory in which the input file (with
extension ".xtl" or ".mcl") is located. This avoids file
opening errors when the directory of the input file is
unwritable.
Number: 762
Date: Thu Jun 7 18:01:29 MET DST 2001
Author: Hubert Garavel (INRIA/VASY)
Files: demos/demo_19/=READ_ME.txt, demos/demo_19/start,
demos/demo_19/graphics/startsimu
Nature: Various changes have been brought to the demo_19 example in
order to adapt it to Windows.
Number: 763
Date: Thu Jun 14 18:26:42 MET DST 2001
Authors: Frederic Lang and Hubert Garavel (INRIA/VASY)
Files: demos/demo_06, demos/demo_21, demos/demo_22, demos/demo_23,
demos/demo_24, demos/demo_26
Nature: Six more demo examples have been simplified in order to take
advantage of the new SVL technology. The Makefiles used
previously in these examples have been replaced by shorter,
simpler SVL files.
Number: 764
Date: Mon Jun 25 12:55:30 MET DST 2001
Authors: Frederic Lang and Hubert Garavel (INRIA/VASY)
Files: bin.*/des2aut, bin.*/exp2c, bin.*/libexp.open,
bin.*/projector.a
Nature: A subtle bug was fixed in the CADP tools for compositional
verification: when an ``.exp'' file started with the keyword
``behaviour'' (meaning that all lower-case letters in labels
must be converted to upper-case letters in order to achieve
case-unsensitivy in labels), there was a problem if the
leaves of the behaviour expression contained in the ``.exp''
file were LTSs generated by the PROJECTOR tool: the special
labels of the form ":fail:*" generated by PROJECTOR were
converted to upper-case and thus were not eliminated by the
``-interfaceuser'' option of EXP.OPEN. To avoid the problem,
the special labels have been renamed into ":FAIL:*" so as
to remain invariant when upper-case conversion is applied.
Number: 765
Date: Thu Jun 25 14:36:55 MET DST 2001
Report: Hubert Garavel (INRIA/VASY)
Authors: Frederic Lang (INRIA/VASY)
Files: bin.*/svl_kernel, src/svl/standard, man/*/svl.*,
demos/demo_01, demos/demo_02, demos/demo_14, demos/demo_15,
demos/demo_20, demos/demo_21, demos/demo_22
Nature: The SVL language has been enriched with a new statement
(``verify''), which allows to evaluate mu-calculus formulas
using the EVALUATOR 3.0 tool.
The examples demo_01, demo_02, demo_15, demo_20, demo_21,
and demo_22 have been greatly simplified by using the new
``verify'' instruction, which allowed in particular to get
rid of the ad hoc shell-scripts used previously, namely
"verify-all-requirements" and "verify-all-properties".
The readability of demo_14 was significantly improved by
removing all the ``.hide'' and ``.rename'' files and by
using the ``hide'' and ``rename'' operators of SVL instead.
Also, in most examples, the verification commands
contained in the =READ_ME.txt files and/or various shell-
scripts have been gathered at a single place (in the
``.svl'' files).
Number: 766
Date: Thu Jul 5 11:16:39 MEST 2001
Author: Radu Mateescu (INRIA/VASY)
Files: src/xtl/actl_pattern.mcl, src/xtl/mcl_pattern.mcl,
src/xtl/READ_ME
Nature: A new EVALUATOR 3.0 library "mcl_pattern.mcl" has been added
and the previous library "actl_pattern.mcl" has been extended.
These libraries encode the generic property patterns defined
by Prof. Matthew Dwyer (Kansas State University) in regular
alternation-free mu-calculus and in ACTL, respectively.
Number: 767 Date: Mon Jul 9 13:09:32 MEST 2001 Author: Hubert Garavel (INRIA/VASY) Files: man/*/installator.*, man/*/tst.* Nature: Two manual pages for INSTALLATOR and TST have been added.
Number: 768
Date: Mon Jul 9 17:45:41 MEST 2001
Authors: Manuel Aguilar, Hubert Garavel, and Radu Mateescu (INRIA/VASY)
Files: demos/demo_29
Nature: A new demo example (dynamic reconfiguration protocol for
agent-based applications) was added to the CADP toolbox.
Number: 769
Date: Thu Jul 12 16:55:48 MEST 2001
Report: Radu Mateescu (INRIA/VASY)
Authors: Hubert Garavel and Frederic Lang (INRIA/VASY)
Files: src/com/cadp_rm, demos/*, com/svl, src/svl/standard
Nature: A minor problem was fixed for the Windows/Cygwin platform.
The executable files created by Open/Caesar (such as
"executor", "evaluator"...) could not be removed, as the
Cygwin GCC compiler would add ".exe" extension to their names
(e.g., "executor.exe", "evaluator.exe"...). To solve this
problem, a new script "cadp_rm" was introduced, which performs
file deletion in a portable way across platforms. Several
demo examples and the SVL compiler have been modified to use
this new shell-script.
Number: 770
Date: Fri Jul 13 12:12:11 MEST 2001
Authors: Hubert Garavel, Frederic Lang, Radu Mateescu et al (INRIA/VASY)
Files: doc/Aguilar-Garavel-et-al-01.ps, doc/Garavel-Lang-01.ps
Nature: Two new papers have been added: one describes a case-study
done with EVALUATOR 3.0, and the other presents the principles
of SVL.
Back to the CADP Home Page