Construction and Analysis of Distributed Processes
Software Tools for Designing Reliable Protocols and Systems

THE CADP NEWSLETTER - Nr. 4
January 27, 1999

This newsletter is available from the CADP Home page. A few URLs in this page have been updated in November 2011.


Contents

1. Availability of CADP version 97b "Liège"

The VASY team of INRIA Rhone-Alpes / DYADE and the VERIMAG laboratory are pleased to announce the availability of a new release of their protocol engineering toolbox CADP (CAESAR/ALDEBARAN Development Package).

This new version is named 97b "Liège" and is dated January 27, 1999. It supersedes all previous versions of CADP.

We are happy to dedicate CADP 97b "Liège" to Professor André Danthine who recently retired, after a brilliant academic carrier at the University of Liège. In addition to his prominent research works in telecommunications, Professor Danthine has been actively supporting formal methods (especially, LOTOS and E-LOTOS) for communication protocols.

The name "Liège" was also chosen because the first beta-version 97b-1 was demonstrated in this city, and because the Research Unit in Networking (now headed by Guy Leduc) plays a significant role in formal specification and validation of real systems.

This is a brief chronology of past events:

1.a. Technical features

In a few words, the main characteristics of CADP 97b "Liège" are:

We now review the most important improvements for each CADP tool:

Additionally, the new release CADP 97b "Liège" brings many other features:

1.b. How to upgrade to CADP 97b "Liège"?

1.c. Credits and acknowledgements

The following scientists have participated to the development of CADP 97b "Liège":

We are extremely grateful to the following scientists, who provided us with valuable feedback and advices about the beta-versions of CADP 97b "Liège":

and all other persons we may forget.

2. On-line demonstrations of CADP available at ETI

The CADP developers support the ETI (Electronic Tool Integration) project. ETI is an electronic component of the Springer International Journal on Software Tools for Technology Transfer (STTT).

It provides a refereed, interactive tool repository that enables STTT subscribers to experiment with individual tools, made accessible through a graphical user-interface.

As the result of a collaborative work between INRIA and the University of Dortmund, the CADP tools have been integrated in the ETI repository, where they can be accessed on-line and applied to various examples.

3. Interested in E-LOTOS? Download the TRAIAN compiler

E-LOTOS (Enhanced LOTOS) is a new formal method for the specification of communication protocols and distributed systems. The definition of E-LOTOS is reaching completion at ISO/IEC.

The VASY team is actively contributing to the definition and improvement of the E-LOTOS standard.

Additionally, the VASY team is developing the TRAIAN compiler, which is now available for free download from the VASY FTP server.

4. Recent information related to CADP

We have recently updated:

People interested in LOTOS world-wide should also consult the WELL Page maintained by Prof. Ken Turner (University of Stirling, Scotland, UK).

5. Detailed list of changes for CADP version 97b "Liège"


VERSION 97a "Twente"
BUG FIX
Number:         484
Date:           Fri Jun 27 15:10:08 MET DST 1997
Report:         Ghassan Chehaibar (Bull/Dyade)
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/caesar.adt

Nature:         When analyzing external types, CAESAR.ADT displayed the 
                following error message:

                        caesar.adt: syntax analysis of ``rcc''
                        caesar.adt: ... 
                        caesar.adt: external type survey of ``rcc''
                        #005 bug :
                             unavailable option in this software
                        caesar.adt: ...

                This message was meaningless, and it is no longer displayed. 

BUG FIX
Number:         485
Date:           Fri Jun 27 16:29:07 MET DST 1997
Report:         Mark Jorgensen (INRIA/VASY)
Authors:        Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files:          com/xeuca, src/eucalyptus/*

Nature:         Clicking on a ".aut" file and choosing "Execute/Standard
                simulation" did not work properly because an intermediate BCG
                file was erased too early. This bug is now fixed. 

BUG FIX
Number:         486
Date:           Fri Jun 27 17:25:37 MET DST 1997
Report:         Mark Jorgensen (INRIA/VASY), Valerie Roy (INRIA/MEIJE) and
                Robert de Simone (INRIA/MEIJE)
Authors:        Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files:          bin.*/bcg_io, bin.*/libBCG_IO.a

Nature:         The FC2 files generated by BCG_IO had slight differences with
                respect to the FC2 format accepted by the Fc2Tools developed
                in the MEIJE project (especially with respect to "tau"-transi-
                tions). These differences have been removed.

BUG FIX
Number:         487
Date:           Wed Jul  2 14:33:06 MET DST 1997
Report:         Francois Germeau (Univ. of Liege)
Author:         Hubert Garavel (INRIA/VASY)
Files:          com/exp.open

Nature:         The "exp.open" shell-script did not have execute permission,
                which caused a problem when invoking this program.

BUG FIX
Number:         488
Date:           Mon Jul  7 20:26:39 MET DST 1997
Report:         Ghassan Chehaibar (BULL/DYADE)
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/libBCG.a, bin.*/bcg_io, bin.*/bcg_draw, bin.*/aldebaran

Nature:         A bug in the BCG library was fixed, which caused the following
                symptoms in BCG_IO, BCG_DRAW and ALDEBARAN (only when the
                environment variable $CADP_CC was set to "gcc"):

                (1) $ bcg_io foo.bcg foo.aut
                    ==> bcg_io stopped after issuing the following message:
                    bcg_io: wrong number of parameters
                    bcg_dynamic: dynamic program error

                (2) $ bcg_draw foo.bcg 
                    ==> ghostview was not launched and a core dump occurred

                (3) $ aldebaran -bmin foo.bcg 
                    ==> a core dump occurred

IMPROVEMENT
Number:         489
Date:           Tue Jul  8 11:39:17 MET DST 1997
Authors:        Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files:          demos/demo_04

Nature:         The demo_04 (systolic arrays computing convolution product)
                was improved for a better use of CAESAR.ADT functionalities,
                especially with the importation of external types and functions
                that are written in C. Also, the statistics have been updated. 

BUG FIX
Number:         490
Date:           Tue Jul 22 12:15:36 MET DST 1997
Report:         Hubert Garavel (INRIA/VASY)
Authors:        Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files:          src/eucalyptus/eucalyptus.tcl

Nature:         A bug was fixed in the Eucalyptus graphical interface: when
                the Aldebaran format or the Graph format were selected for
                LTS generation, this selection remained later when the OPEN/
                CAESAR tools were invoked, causing error messages of the form:
                        #016 error :
                        option ``-open'' is incompatible with graph generation
                        quit

                Also, the "-monitor" option is now unselected automatically
                when the Aldebaran format or Graph format is selected for
                LTS generation.

                Finally, several CAESAR options have been moved from the
                "Generate LTS" panel to the "Options" menu. These options
                are: "Optimization V3", "Optimization V4", "Optimization E7",
                "Optimization Safety", "Optimization Gradual", and "Petri Net
                Printing". 

BUG FIX
Number:         491
Date:           Fri Jul 25 20:14:36 MET DST 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/bcg_io

Nature:         One of the BCG_IO functionalities (translation of LTSs into 
                pseudo-LOTOS code) did not work properly. This minor problem
                was solved.  

IMPROVEMENT
Number:         492
Date:           Fri Jul 25 20:19:56 MET DST 1997        
Authors:        David Jacquemin and Hubert Garavel (INRIA/VASY)
Files:          bcg.*/bcg_io, man/manl/bcg_io.l

Nature:         The BCG_IO tool was extended so as to allow the translation of
                an LTS into the simple SEQUENCE format (see "man exhibitor"
                for a definition of this format). The translation is only
                possible if the LTS has no circuits and if all its states 
                (with the possible exception of the initial state) have at 
                most one outgoing edge.

IMPROVEMENT
Number:         493
Date:           Tue Jul 29 12:21:19 MET DST 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/caesar, bin.*/caesar.adt, incl/X_*.h, demos/*/*.t

Nature:         In the ``.h'' files produced by the new version of CAESAR.ADT,
                there is, for each type T, a macro-definition of the form:
                        #define CAESAR_ADT_SCALAR_T 
                iff variables of type T can be assigned the null value "0".
                
                This macro-definition is used by CAESAR to decide whether a
                variable X of type T can be reset by a simple assignment
                (i.e., X = 0) or by a call to the C function "memset()".

                Currently, this macro is defined by CAESAR.ADT for all the 
                C types generated from LOTOS sorts: integers, enumerations, 
                tuples (i.e., pointers to structs), and discriminated unions 
                (i.e., pointers to unions of structs). 

                On the opposite, this macro is not defined automatically for
                external types: the user should define it selectively for
                all external types T that allow the "0" value. Typical 
                examples of types T for which this macro should not be
                defined are: structures, unions and arrays. 

                Forgetting to define this macro when appropriate is totally
                harmless: the only drawback is that CAESAR will use the
                "memset()" instead of an assignment, which is slightly less
                efficient. 

                Some of the hand-written ``.h'' and ``.t'' files contained in
                the ``incl'' and ``demos'' directories have been updated
                accordingly.

IMPROVEMENT
Number:         494
Date:           Tue Jul 29 15:31:33 MET DST 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          com/upc, com/rfl, com/tst, com/bcg_open, com/bcg_open, 
                com/exp.open

Nature:         The shells scripts listed above have been updated to remove
                some Solaris specific features that would prevent them to
                work under Linux.

BUG FIX
Number:         495
Date:           Tue Aug  5 16:56:03 MET DST 1997
Report:         Ghassan Chehaibar (BULL/DYADE)
Author:         Laurent Mounier (VERIMAG)
Files:          bin.*/exp2c, bin.*/libexpopen.a

Nature:         Several bugs were fixed, which could caused EXP.OPEN to 
                improperly manage the labels of LTS composition expresion.
                Moreover, the number of distinct labels allowed has been 
                extended to 4000.

BUG FIX
Number:         496
Date:           Wed Aug  6 18:56:44 MET DST 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/bcg_io, bin.*/libbcg_io.a, bin.*/libBCG_IO.a

                The BCG_IO tool was modified in order to allow a smoother 
                translation between various formats:

                - When translating a BCG graph into the Aldebaran format,
                double quotes in labels are now replaced by single quotes;
                a warning is emitted in such case.

                - When translating a BCG graph into the Sequence format,
                double quotes in labels are now replaced by single quotes;
                a warning is emitted in such case. 
        
                - When translating a BCG graph into the Viscope format,
                a message is emitted when commas are replaced by semicolons.

                - When translating a BCG graph into the FC2 format, double
                quotes are added around the labels, except for those labels 
                that already have double quotes inside (in such case, it is
                likely that the label comes from an FC2 graph, e.g., has
                the form "a"."b").  

BUG FIX
Number:         497
Date:           Mon Aug 25 19:22:32 MET DST 1997
Authors:        Hubert Garavel and David Jacquemin (INRIA/VASY)
Files:          bin.*/bcg_io, bin.*/libbcg_io.a, bin.*/libBCG_IO.a

Nature:         A minor bug was fixed in the translation into the FC2 format:
                when given the "-verbose" option, the previous version of
                BCG_IO printed ``hook "main"'' instead of ``hook "main">0''. 
 
                Also, in order to allow the FC2 files generated by BCG_IO to
                be used with the Fc2Link tool, the new version of BCG_IO adds
                a declaration of the form ``struct "filename"''.

BUG FIX
Number:         498
Date:           Tue Aug 26 20:31:30 MET DST 1997
Report:         Radu Mateescu (INRIA/VASY)
Author:         Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files:          man/manl/bcg.l, man/windex, man/whatis

Nature:         The BCG manual page has been modified in order to be correctly
                indexed in the "windex" file: this page can now be accessed by
                typing "man bcg" or "man BCG". 

BUG FIX
Number:         499
Date:           Wed Aug 27 16:00:22 MET DST 1997
Report:         Radu Mateescu (INRIA/VASY)
Author:         Laurent Mounier (VERIMAG)
Files:          bin.*/aldebaran

Nature:         Several minor bugs were fixed in ALDEBARAN regarding the
                parsing of the command line (in particular when some options
                were used with incorrect arguments). 

BUG FIX
Number:         500
Date:           Wed Aug 27 16:04:02 MET DST 1997
Report:         Mark Jorgensen (INRIA/VASY)
Author:         Laurent Mounier (VERIMAG)
Files:          bin.*/aldebaran

Nature:         Moreover, the "-live" option did not work properly when 
                applied to ".exp" files. This problem is now solved.

IMPROVEMENT
Number:         501
Date:           Wed Aug 27 17:09:27 MET DST 1997
Report:         Francois Germeau (Univ. de Liege, Belgium)
Author:         Laurent Mounier (VERIMAG)
Files:          bin.*/aldebaran, man/manl/aldebaran.l

Nature:         A new option, "-labels", was added to ALDEBARAN. This option 
                defines the maximum number of distinct labels allowed in an
                LTS (or in a composition of LTSs). The ALDEBARAN man page was
                updated.     

IMPROVEMENT
Number:         502
Date:           Wed Aug 27 11:12:02 MET DST 1997
Authors:        David Jacquemin and Hubert Garavel (INRIA/VASY)
Files:          bcg.*/bcg_io, man/manl/bcg_io.l

Nature:         The BCG_IO tool was extended so as to accept FC2 files as 
                input. The manual page has been updated accordingly.

IMPROVEMENT
Number:         503
Date:           Thu Aug 28 18:04:18 MET DST 1997
Report:         Radu Mateescu (INRIA/VASY)
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*.gcc

Nature:         The two directories $CADP/bin.sun4.gcc and $CADP/bin.sun5.gcc
                containing libraries compiled with the GCC compiler have been
                removed, because they were not used actually. This makes the
                CADP release simpler and lighter (1.5 less Megabytes).

IMPROVEMENT
Number:         504
Date:           Thu Aug 28 21:46:17 MET DST 1997
Report:         Radu Mateescu (INRIA/VASY)
Author:         Hubert Garavel (INRIA/VASY)
Files:          incl/X_NATURAL.h

Nature:         Three #include declarations have been added in X_NATURAL.h
                in order to declare properly the functions kill() and getpid().

IMPROVEMENT
Number:         505
Date:           Wed Sep  3 10:49:59 MET DST 1997        
Author:         Radu Mateescu (INRIA/VASY)
Files:          bin.*/xtl, bin.*/xtl_expand, bin.*/libXTL.a, incl/xtl_*.h, 
                src/xtl/*, man/manl/xtl.l, com/rfl, VERSION

Nature:         The CADP toolbox was enriched with a new tool named XTL
                (an acronym for "eXecutable Temporal Language").

                The XTL tool allows to evaluate temporal logic formulas 
                on graphs encoded in the BCG format. This tool offers the
                following features:

                - XTL supports several temporal logics widely used. Currently,
                  the following temporal logics are supported: HML, CTL, ACTL,
                  LTAC, as well as the modal mu-calculus. All of them can be
                  directly used by end-users to verify properties on BCG 
                  graphs. 

                - Compared to other model-checkers, XTL is more expressive,
                  because it allows to handle the data values contained in 
                  states and transition labels. These values can be used in
                  temporal formulas, assigned to variables, etc.
 
                - Moreover, XTL is extensible. A user can define his/her own
                  temporal logic, as a library of operators written in XTL.
                  This is the way in which the currently available formalisms
                  (HML, CTL, ACTL, LTAC and modal mu-calculus) are implemented.

                - Finally, XTL can also be used for other purpose than
                  evaluation of temporal formulas. Because it is a functional
                  programming language, it allows to perform any computation
                  on BCG graphs: for instance, it can compute the branching
                  factor of a graph, print its list of labels, etc.
 
                For more details, see the manual page (by typing "man xtl")
                and the predefined XTL libraries (in directory $CADP/src/xtl).

IMPROVEMENT
Number:         506
Date:           Wed Sep  3 20:14 MET DST 1997
Author:         Radu Mateescu (INRIA/VASY)
Files:          demos/demo_21, demos/demo_22

Nature:         Two new demo examples have been added to illustrate the use
                of the XTL tool for verifying properties of distributed
                algorithms in the LTAC temporal logic:

                - demo_21 presents Peterson's mutual exclusion algorithm

                - demo_22 presents Dekker's mutual exclusion algorithm 

IMPROVEMENT
Number:         507
Date:           Wed Sep  3 20:44 MET DST 1997
Author:         Radu Mateescu (INRIA/VASY)
Files:          demos/demo_01, demos/demo_02, demos/demo_16     

Nature:         Three existing demos have been improved in order to illustrate
                the use of the XTL tool:

                - In demo_01 and demo_02, a new file "bitalt.xtl" expresses the
                  properties of the alternating bit protocol (written as a 
                  combination of mu-calculus and LTAC temporal logic).

                - In demo_16, a new file "prop.xtl" expresses the properties
                  of the Philips Bounded Retransmission Protocol (written as
                  ACTL temporal logic formulas). 

                  Also, the size of the BRP protocol has been enlarged to 
                  take advantage of the speed increase in CAESAR: the number
                  of retransmissions was set to 3 and the message length was
                  set to 4. 

BUG FIX
Number:         508
Date:           Fri Sep  5 16:16:37 MET DST 1997
Report:         Massimo Zendri (BULL/DYADE)
Author:         Mark Jorgensen (INRIA/VASY)
Files:          bin.*/xsimulator.a

Nature:         Xsimulator did not work properly if the $PATH variable of
                the user did not contain "." (the current directory). This
                problem is now solved.

IMPROVEMENT
Number:         509
Date:           Tue Sep  9 10:29:19 MET DST 1997
Authors:        Hubert GARAVEL (INRIA/VASY) and Laurent MOUNIER (VERIMAG)
Files:          bin.*/exhibitor.a, bin.*/evaluator.a, bin.*/projector.a

Nature:         The Exhibitor, Evaluator, and Projector libraries exported
                objects generated by Lex/Yacc (e.g., yyparse, yytext, etc.)
                which could create conflicts when linking with other code.
                From now on, unique names are used.

BUG FIX
Number:         510
Date:           Wed Sep 10 10:22:58 MET DST 1997
Report:         Ghassan Chehaibar (BULL/DYADE)
Author:         Hubert Garavel (INRIA/VASY) and Laurent Mounier (VERIMAG)
Files:          com/bcg_open, com/exp.open, man/manl/bcg_open.l

Nature:         The previous versions of "bcg_open" and "exp.open" tried to
                optimize CPU time by avoiding recompilations. However, the
                optimization scheme was not precise enough, so that some
                object files were reused incorrectly in some cases (especially
                when using advanced compositional verification techniques).  

                The two tools have been modified so that they no longer try
                to avoid recompilations. We do not expect this change to cause
                any substantial decrease of performance, as "bcg_lib" already
                avoids recompilations (in a safe way), and as most OPEN/CAESAR
                tools are now shipped in archive format ("*.a" files). The
                "bcg_open" manual page was updated to reflect this change.

IMPROVEMENT
Number:         511
Date:           Wed Sep 10 11:02:10 MET DST 1997
Authors:        Patrick Wendel, Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files:          INSTALLATION, com/installator, src/installator, com/rfl, 
                tcl-tk/bin.*/expectk, tcl-tk/COPYRIGHT_EXPECT

Nature:         A new installation procedure was designed for CADP. The main
                changes are the following:

                - A new program, named Installator, has been added to the
                  CADP toolbox. Installator is an computer-aided assistant
                  that will help CADP users to install and upgrade their
                  CADP software. Installator has been designed in the same
                  vein as "setup" programs in PC/Windows software and we
                  hope that CADP users will find it useful and convenient. 

                - The RFL program was adapted: new options have been added,
                  which are used by Installator.  

                - The "expectk" program version 5.24 (developed by Don Libes 
                  at NIST, version 5.24) was added to the CADP release (in
                  binary form).

                - As regards the FTP distribution of CADP, the notion of 
                  "full" distribution was suppressed, because it was not used
                  by Installator. From now on, only the "splitted" distribution
                  will be retained, allowing a more flexible support of
                  multiple architectures/operating systems.

                - The distribution of CADP by magnetic tapes was removed,
                  because everybody seems to prefer the distribution by FTP. 

                - The INSTALLATION file was modified to describe the new
                  installation procedure.

IMPROVEMENT
Number:         512
Date:           Wed Sep 10 12:11:48 MET DST 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/caesar

Nature:         There have been internal changes in CAESAR, in order to prepare
                future evolutions of this tool (especially, state space 
                reduction). These changes are not visible to the users, but
                two of them are worth mentioning:

                - The format of the ".net" file was slightly modified (the 
                  "unites quittees" clauses have been changed into "variables
                  annulees" clauses).  

                - In the C code generated by CAESAR, the preprocessor variable
                  CAESAR_IGNORE_ESCAPE was renamed into CAESAR_NO_CLEARANCE. 

BUG FIX
Number:         513
Date:           Wed Sep 10 14:27:51 MET DST 1997
Report:         Radu Mateescu (INRIA/VASY)
Author:         Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files:          bin.*/libBCG.a

Nature:         A minor bug was fixed in the BCG format: the exponentiation
                operator '**', previously declared as prefix at the source
                language level, is now declared as infix. This bug had no
                effect for any of the existing BCG tools and was revealed by 
                the newly introduced XTL tool.

                When applying the XTL tool on BCG graphs generated with older
                versions of CADP (i.e., version 97a or older), this problem
                will not be noticeable, unless the XTL program invokes the
                exponentation '**' in infix notation. Should this problem
                happen, then generate your BCG file again, or upgrade it
                using the following sequence of commands:
                        bcg_io FILE.bcg FILE.aut
                        bcg_io -aldebaran -parse FILE.aut FILE.bcg
                        rm FILE.aut 

IMPROVEMENT
Number:         514
Date:           Wed Sep 10 15:00:48 MET DST 1997
Authors:        Mihaela Sighireanu and Radu Mateescu (INRIA/VASY)
Files:          demos/demo_23

Nature:         A new demonstration example was added to the CADP release:
                the IEEE 1394 high performance serial bus ("Firewire").

BUG FIX
Number:         515
Date:           Wed Sep 10 15:19:24 MET DST 1997
Author:         Mark Jorgensen (INRIA/VASY)
Files:          src/eucalyptus/eucalyptus.tcl, src/eucalyptus/xeucarc_standard
                com/xeuca_convert

Nature:         Several fixes and major improvements have been done in the
                EUCALYPTUS 2.3 Graphical User-Interface:

                (a) The conversion of .aut, .seq and .bcg files to the 
                    PostScript and encapsulated PostScript formats didn't work.
                    This problem is now solved.

                (b) The reduction of .exp files with ALDEBARAN was stored in
                    a .exp file instead of a .aut file. This problem is now 
                    solved.

                (c) A minor typo caused the interface to stop when calling 
                    the TESTGEN tool two successive times on the same file.

                (d) The Fc2Tools developed by the Meije group at INRIA-Sophia
                    Antipolis have been integrated in the EUCALYPTUS toolset. 
                    Like ALDEBARAN, it is now possible to apply these tools
                    to any automaton file, whatever its format (.bcg, .aut,
                    .fc2, .seq). All the underlying conversions are done
                    implicitly by EUCALYPTUS.

                (e) Reciprocally, it is now possible to use the ALDEBARAN,
                    BCG and OPEN/CAESAR tools on automata encoded in the
                    .fc2 format. All the underlying conversions are done
                    implicitly.

                (f) The file conversions between the various automata formats
                    have been optimised. EUCALYPTUS now maintains a database 
                    to remember if a file has already been converted to a 
                    format, in order to avoid multiple conversions. 
                    Furthermore, the new conversions introduced in BCG_IO
                    (i.e., .fc2 to .bcg converter, and .bcg to .seq converter)
                    have been integrated in the interface. 
                
                (g) The "Compare..." window for automata is now smaller than
                    the previous one, with only one filebox instead of three.

                (h) The "Evaluate mu-calculus formulas..." window is 
                    now called "Verify temporal formulas...", and offers
                    the choice between the OPEN/CAESAR Evaluator tool 
                    and/or the XTL tool (for automata only).

                (i) The "Find deadlocks..." menus have been merged into
                    a unique window proposing the choice between all the
                    tools that can be used for this operation (Exhibitor,
                    Terminator, ALDEBARAN, Fc2Tools).

                (j) The "Find livelocks..." window now proposes the choice
                    between ALDEBARAN and Fc2Tools.

                (k) The menu that appears when clicking on a .lotos file has
                    been simplified. Some of the choices are now proposed in
                    a sub-menu that appears when choosing "More" in the menu.

                (l) Two ALDEBARAN options, "-labels" and "-path", are now
                    supported by the EUCALYPTUS interface. In particular, it
                    is now possible to search for a path leading to a state 
                    identified by its state number.

                (m) The "Web" button now gives access to the CADP Frequently
                    Asked Questions page, to the CADP Patches page, and to
                    the Fc2Tools page.

                (n) The "View" / "Change Presentation" windows was enhanced
                    so as to allow object files (.o) and BCG dynamic libraries
                    (*@1.o, *@2.o, etc.) to be hidden.

                (o) An "Evaluator" entry was created in the "Options" menu.
                    This entry allows to set the verbosity and hash table
                    size values for Evaluator

                (p) Within EUCALYPTUS, it is now possible to mail a file
                    to a specified e-mail address.

                (q) The manual pages for Des2Aut, Projector and the Fc2Tools
                    are now available on-line from the "Help" button of 
                    EUCALYPTUS.

                (r) In "View" / "Change Presentation", the "Other files"
                    options has been fixed: previously it displayed all files
                    in the current directory; currently, it displays only
                    the files that do not belong to the aforementioned
                    file categories (Directories, Extended LOTOS Specs, etc.) 

                (s) It is now possible to save user preferences into the
                    startup file "$HOME/.xeucarc". This is done by clicking
                    the File / Save Preferences menu.

IMPROVEMENT
Number:         516
Date:           Thu Sep 11 12:13:59 MET DST 1997
Report:         Patrick Wendel (INRIA/VASY)
Author:         Hubert Garavel (INRIA/VASY)
Files:          INSTALLATION_1, INSTALLATOR_2, INSTALLATOR_3, INSTALLATOR_4,
                src/installator

Nature:         The INSTALLATION file was too large and not convenient for
                use with INSTALLATOR. It was splitted in four separate files:

                - INSTALLATION_1 describes the assisted installation procedure
                - INSTALLATION_2 describes user customizations
                - INSTALLATION_3 describes the Request for License procedure
                - INSTALLATION_4 describes the manual installation procedure

                Installator was updated to take advantage of these conventions.

                For backward compatibility (especially with the manual pages),
                a symbolic link INSTALLATION pointing to INSTALLATION_2 was 
                created. 

IMPROVEMENT
Number:         517
Date:           Tue Sep 16 13:44:59 MET DST 1997
Report:         Charles Pecheur (INRIA/VASY)
Authors:        Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files:          com/bcg_info

Nature:         The "bcg_info" shell-script was modified so as to avoid the 
                creation of a (sometimes huge) temporary file in /tmp. The
                modified version uses pipes instead.

BUG FIX
Number:         518
Date:           Tue Sep 16 14:22:18 MET DST 1997
Report:         Ghassan Chehaibar (BULL/DYADE)
Author:         Laurent Mounier (VERIMAG)
Files:          man/manl/des2aut.l

Nature:         The manual page for Des2Aut was updated: the new page specifies
                that gate names are case-sensitive, adds a missing rule:
                        <behaviour> ::= '('<behaviour>')'
                and adds a missing comma in the non-terminal <gate-list>. 

BUG FIX
Number:         519
Date:           Tue Sep 16 15:14:12 MET DST 1997
Report:         Ghassan Chehaibar (BULL/DYADE)
Author:         Laurent Mounier (VERIMAG)
Files:          com/exp.open

Nature:         In some cases, the "exp.open" shell-script did not work under 
                Solaris 2.* (due to a non-standard behaviour of the "basename"
                command in Solaris 2.*). This problem has been fixed both for 
                Solaris 1.* and Solaris 2.*.

IMPROVEMENT
Number:         520
Date:           Thu Sep 18 16:29:26 MET DST 1997
Authors:        David Jacquemin, Mark Jorgensen and Hubert Garavel (INRIA/VASY)
Files:          bin.*/exp2fc2, man/manl/exp2fc2.l,
                src/eucalyptus/eucalyptus.tcl, src/eucalyptus/com/xeuca_fc2info

Nature:         A new tool named "exp2fc2" was added to the CADP toolbox.
                This tool translates an ".exp" file into an FC2 file describing
                a set of communicating processes. This allows to apply the 
                FC2 tools to an ".exp" file. A manual page was written for 
                this new tool ("man exp2fc2"). The EUCALYPTUS graphical 
                interface was modified accordingly.

BUG FIX
Number:         521
Date:           Tue Sep 23 18:08:58 MET DST 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          src/open_caesar/generator.c, src/open_caesar/reductor.c

Nature:         The source code of Generator and Reductor was modified to
                avoid the use of the non-POSIX signal SIGSYS, which does not 
                exist in Linux. 

IMPROVEMENT
Number:         522
Date:           Wed Sep 24 17:24:30 MET DST 1997
Authors:        Khalid Laksiouar (INRIA/MEIJE), Mark Jorgensen and 
                Hubert Garavel (INRIA/VASY)
Files:          com/fc2open, man/manl/fc2open.l, man/manl/*or.l
                src/eucalyptus/eucalyptus.tcl,

Nature:         A new tool, named FC2OPEN, was added to the CADP toolbox and 
                to the FC2Tools toolbox developed in the MEIJE project of 
                INRIA Sophia-Antipolis. This new tool allows to apply all
                OPEN/CAESAR tools to FC2 files, either the FC2 files that
                represent sequential automata, or the FC2 files that describe
                networks of parallel processes.

                For technical reasons, the FC2OPEN tool is splitted between 
                the CADP and FC2Tools toolboxes, and requires both toolboxes
                to function. The other part of FC2OPEN is a binary program
                named "fc2open2c", which will be shipped with version 1.2
                and higher of FC2Tools. The environment variable $FC2DIR
                should be set and point to the directory where the FC2Tools
                are installed.

                A manual page was written for this new tool ("man fc2open").
                The manual pages of all OPEN/CAESAR tools (e.g., terminator,
                executor, etc.) were updated to mention the possibility of
                using FC2OPEN.

                The EUCALYPTUS graphical interface was modified accordingly.
                If the $FC2DIR variable is not set, EUCALYPTUS will not use
                the "fc2open" tool, and will try instead to convert the FC2
                file into a BCG file, which will only work if the FC2 file
                represents a sequential automaton.

IMPROVEMENT
Number:         523
Date:           Thu Oct  2 10:50:24 MET 1997
Authors:        Mark Jorgensen (INRIA/VASY), Hubert Garavel (INRIA/VASY),
                Laurent Mounier (VERIMAG)
Files:          bin.*/aldebaran, bin.*/exp2c, bin.*/exp2fc2, 
                bin.*/libexpopen.a, man/manl/aldebaran.l

Nature:         The ".exp" format has been extended. Previously, the LTSs
                composing the network (i.e., the leaves of the composition 
                expression) had to be ".aut" files. The new version also 
                allows these LTSs to be encoded in other formats, e.g. BCG,
                FC2, SEQUENCE, etc. This is done by invoking the BCG_IO tool
                to perform the appropriate conversions. The definition of
                the ".exp" format (type "man aldebaran") was updated. All 
                tools that accept ".exp" files as input (ALDEBARAN, EXP2C, 
                EXP2FC2) have been subsequently modified. 

BUG FIX
Number:         524
Date:           Mon Oct  6 16:37:34 MET DST 1997
Report:         Mark Jorgensen (INRIA/VASY)
Author:         Laurent Mounier (VERIMAG)
Files:          bin.*/aldebaran

Nature:         A bug was fixed, which caused "aldebaran -info" to core dump
                when applied to ".exp" files.

IMPROVEMENT
Number:         525
Date:           Mon Oct  6 18:08:02 MET DST 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          usr

Nature:         Following the results of the technical enquiry conducted in
                the CADP Newsletter #3 (September 1997), the "usr" directory
		was removed from the CADP distribution. Indeed:

                - The "pre" and "post" programs for interfacing the SEDOS
                toolkit with CADP are now useless, because the SEDOS simulator
                HIPPO is no longer maintained nor distributed. 

                - The "deadlock" program for finding deadlocks in ".aut" files
                can now be replaced by a joint use of BCG_OPEN and EXHIBITOR,
                or the "-dead" option of ALDEBARAN. 

                This makes the CADP release 850 kbytes leaner. The contents of
                the "usr" directory can still be obtained by sending a request
                to "caesar@imag.fr". However, the "pre", "post", and "deadlock"
                programs will no longer be maintained, nor ported to other
                architectures / operating systems.

IMPROVEMENT
Number:         526
Date:           Tue Oct  7 12:26:26 MET DST 1997
Author:         Charles Pecheur (INRIA/VASY)
Files:          doc/Pecheur-97.ps, doc/:READ_ME

Nature:         A new publication entitled "Specification and Verification of
                the CO4 Distributed Knowledge System Using LOTOS" was added
                to the CADP release.

BUG FIX
Number:         527
Date:           Thu Oct 23 17:51:39 MET DST 1997
Report:         Ghassan Chehaibar (BULL/DYADE)
Author:         Mark Jorgensen (INRIA/VASY)
Files:          tcl-tk/bin.*/duplex

Nature:         A bug was fixed, which caused the graphical user-interface
                EUCALYPTUS to block when the output of some commands was 
                too long.

BUG FIX
Number:         528
Date:           Fri Oct 24 12:10:19 MET DST 1997
Report:         Charles Pecheur (INRIA/VASY)
Author:         Mark Jorgensen (INRIA/VASY)
Files:          src/installator/*

Nature:         Several bug fixes and improvements have been made in the
                Installator program:

                - Installator would block if $CADP_TMP was set to the current
                  directory ("."). This problem was fixed

                - For a first-time installation, Installator will propose
                  "./cadp" as the default directory for installing CADP

                - Installator now checks the type of Unix to invoke the "df" 
                  command with appropriate options

                - When the untar/uncompress operation is done, a beep is
                  produced to wake up the user

                - When the RFL is done, a beep is also produced

IMPROVEMENT
Number:         529
Date:           Tue Oct 28 16:49:14 MET 1997
Authors:        Bruno Vivien, Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files:          bin.*/caesar.indent, man/manl/caesar.indent.l, src/eucalyptus/*

Nature:         A LOTOS pretty-printer named "caesar.indent" has been added
                to the CADP toolset. This pretty-printer was developed with
                the PARADIS tool of the SYNTAX compiler generator (SYNTAX is
                a registered trademark of INRIA). 

                A manual page is available (type "man caesar.indent"). This 
                pretty-printer is accessible from the EUCALYPTUS graphical 
                interface by clicking on a ".lotos" file and selecting the
                "More" / "Indent" menu.

BUG FIX
Number:         530
Date:           Tue Oct 28 19:23:09 MET 1997
Report:         Charles Pecheur (INRIA/VASY)
Author:         Radu Mateescu (INRIA/VASY)
Files:          bin.sun*/xtl_expand

Nature:         A bug was fixed in the XTL expander, which caused, in certain
                cases, to erroneously detect and signal recursion between macro
                definitions.

BUG FIX
Number:         531
Date:           Tue Oct 28 19:23:09 MET 1997
Author:         Radu Mateescu (INRIA/VASY)
Files:          bin.sun*/xtl

Nature:         Several bugs were corrected in the XTL tool, concerning bad
                code generation for Sun4 machines. Also, a small typing error 
                in the "xtl" manual page has been corrected.

BUG FIX
Number:         532
Date:           Tue Oct 28 19:23:09 MET 1997
Author:         Radu Mateescu (INRIA/VASY)
Files:          src/xtl/ltac.xtl

Nature:         The definition of "FAIR (A, B)" (which is the action-based 
                version of the "FAIR" operator defined by Queille and Sifakis)
                was corrected.

BUG FIX
Number:         533
Date:           Tue Oct 28 20:52:21 MET 1997
Report:         Fabio Paterno (CNUCE-CNR, Pisa, Italy)
Authors:        Radu Mateescu and Hubert Garavel (INRIA/VASY)
Files:          bin.*/xtl

Nature:         The XTL compiler was modified to use always the $CADP/com/arch
                command (instead of the /bin/arch command that exists under
                Solaris). This solves a potential problem occurring when
                CADP users do not configure their $PATH variable properly. 

IMPROVEMENT
Number:         534
Date:           Fri Oct 31 17:48:34 MET 1997
Authors:        Charles Pecheur (INRIA/VASY)
Files:          demos/demo_24

Nature:         A new demonstration example was added to the CADP release:
                the CO4 protocol for distributed knowledge bases.

BUG FIX
Number:         535
Date:           Fri Nov  7 12:42:43 MET 1997
Report:         Fabio Paterno and Carmen Santoro (CNUCE-CNR, Pisa, Italy)
Authors:        Hubert Garavel and Mark Jorgensen (INRIA/VASY)
Files:          installator.shar

Nature:         The self-extracting program "installator.shar" was updated
                to detect if another Installator is already running, or if
                a previous execution of Installator crashed without cleaning 
                up. 

IMPROVEMENT
Number:         536
Date:           Mon Dec  1 18:40:48 MET 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/caesar, man/manl/caesar.l, src/eucalyptus/eucalyptus.tcl

Nature:         CAESAR was modified to avoid unecessary recompilations when
                given either the "-open" option (OPEN/CAESAR mode) or the
                "-exec" option (EXEC/CAESAR mode). Precisely, CAESAR will not 
                regenerate "filename.c" if this file already exists in the 
                current directory and if it has been modified more recently:

                - than the corresponding LOTOS file ("filename.lotos",
                  "filename.lot", or "filename.l"),
                - than any LOTOS library transitively included (using the
                  "library" clause) in this LOTOS file, 
                - and than any C file transitively included (using the 
                  "#include" clause) in "filename.c" itself.

                The CAESAR manual page was updated accordingly. The EUCALYPTUS
                user interface was modified to give access to "-force" option.

IMPROVEMENT
Number:         537
Date:           Mon Dec  1 18:47:44 MET 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/caesar.adt, man/manl/caesar.adt.l, 
                src/eucalyptus/eucalyptus.tcl

Nature:         CAESAR.ADT was modified to avoid unecessary recompilations.
                Precisely, CAESAR.ADT will not regenerate "filename.h" if
                this file already exists in the current directory and if it
                has been modified more recently:

                - than the corresponding LOTOS file ("filename.lotos",
                  "filename.lot", or "filename.l"),
                - than any LOTOS library transitively included (using the
                  "library" clause) in this LOTOS file, 
                - than any C file transitively included (using the 
                  "#include" clause) in "filename.h" itself.
                - than the file named "filename.t" if this file exists in
                  the current directory,
                - and than the file named "filename.f" if this file exists 
                  in the current directory.

                The CAESAR.ADT manual page was updated accordingly. The
                EUCALYPTUS user interface was modified to give access to 
                "-force" option.

IMPROVEMENT
Number:         538
Date:           Tue Dec  2 13:07:32 MET 1997
Author:         Mark Jorgensen (INRIA/VASY)
Files:          com/xeuca, src/eucalyptus/*

Nature:         Following the results of the Technical Enquiry that was 
                enclosed in the CADP Newsletter #3, the TESTGEN and TETRA
                tools are no longer integrated within the EUCALYPTUS graphical
                user interface. 

BUG FIX
Number:         539
Date:           Tue Dec  2 16:29:43 MET 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          com/caesar.open 

Nature:         The "caesar.open" shell-script was entirely rewritten in order
                to take advantage of the recent improvements in CAESAR and 
                CAESAR.ADT (see above items #536 and 537). The new solution
                has several benefits:

                - The previous version of "caesar.open" tried to optimize
                  CPU time by avoiding recompilations. However, the dependency  
                  analysis was approximate, so that object files could be,
                  in some cases, reused incorrectly. From now on, the
                  dependency analysis is accurate. This bug fix is similar
                  to bug fix #510 for "bcg_open" and "exp.open". 

                - "caesar.open" no longer relies upon the generation of a 
                  Makefile. It is faster, more portable, and allows to handle
                  properly the cases where input filenames (".lotos", ".c",
                  ".a", or ".o") contain special characters (e.g., semicolons)
                  not allowed in Makefiles. In the previous version of 
                  "caesar.open", for instance, filenames containing semicolons
                  generated the following error message:

                  make: Fatal error in reader: /tmp/caesar.open.makefile.29719,
                  line 24: Extra `:', `::', or `:=' on dependency line

                - The new version of "caesar.open" is much closer to the
                  other similar shell-scripts ("bcg_open", "exp.open", and
                  "fc2open"), which could enable (in the future) to merge 
                  all these scripts into a single one.

BUG FIX
Number:         540
Date:           Tue Dec  2 17:27:05 MET 1997
Author:         Charles Pecheur (INRIA/VASY)
Files:          src/xtl/actl.xtl

Nature:         The definition in XTL of the "AU_A_B" operator of the ACTL 
                temporal logic was incorrect. It has been fixed.

BUG FIX
Number:         541
Date:           Tue Dec 16 15:41:49 MET 1997
Report:         Marc Herbert (LIP-LHPC, Lyon, France)
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.sun5/*

Nature:         Two problems have been fixed, which would create core dumps
                and/or SIGALRM signals if the duration specified in the LICENSE
                file was less than one month.

BUG FIX
Number:         542
Date:           Thu Dec 18 15:25:37 MET 1997
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/caesar

Nature:         A bug was fixed, which would cause CAESAR 5.2 to core dump
                when the "-graph" option was used.

BUG FIX
Number:         543
Date:           Fri Jan 16 20:54:14 MET 1998
Report:         Mark Jorgensen (INRIA/VASY)
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/caesar

Nature:         A bug was fixed, which caused CAESAR to generate illegal
                C code under Linux, leading to the following error message  
                from the C compiler:
                   /tmp/caesar_xxx.c: In function `CAESAR_STANDARD_LOOP':
                   /tmp/caesar_xxx.c: parse error before character 0204

BUG FIX
Number:         544
Date:           Wed Jan 28 16:17:29 MET 1998
Report:         Ghassan Chehaibar (BULL/DYADE)
Author:         Hubert Garavel (INRIA/VASY)
Files:          src/eucalyptus/eucalyptus.tcl

Nature:         A bug was fixed in the EUCALYPTUS user-interface: by default,
                CAESAR, CAESAR.ADT, and CAESAR.OPEN were always invoked with
                option "-warning" (thus preventing warnings from being
                displayed), even if warnings were selected in the Options menu.

IMPROVEMENT
Number:         545
Date:           Wed Feb  4 18:27:56 MET 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          doc/Garavel-98, doc/:READ_ME, doc/biblio.bib

Nature:         A new publication entitled "OPEN/CAESAR: An Open Software 
                Architecture for Verification, Simulation, and Testing"
                was added to the CADP release. This report provides an
                introduction and overview of the OPEN/CAESAR environment.

BUG FIX
Number:         546
Date:           Fri Feb 13 15:48:14 MET 1998
Report:         Charles Pecheur (INRIA/VASY)
Author:         Laurent Mounier (VERIMAG)
Files:          bin.*/exp2c, bin.*/libexpopen.a

Nature:         A bug was fixed, which caused Exp.Open to behave incorrectly
                on ".exp" files containing several instances of the same 
                ".aut" file, e.g.:
                        cell ||| cell ||| cell

BUG FIX
Number:         547
Date:           Fri Feb 13 15:52:51 MET 1998
Report:         Axel Belinfante (Univ. of Twente, The Netherlands),
                Zoltan Meggyesi (CERN, Geneva, Switzerland)
Author:         Hubert Garavel (INRIA/VASY)
Files:          installator.shar packages

Nature:         The "installator.shar" self-extracting archives were modified
                in order to avoid a problem for users which invoke the GNU
                "gettext" command instead of the Solaris "/bin/gettext" one:
                under these circumstances, the "-beta" option was not taken
                into account by Installator. This problem is now solved.

IMPROVEMENT
Number:         548
Date:           Wed Feb 18 17:11:33 MET 1998
Author:         Marius Bozga (VERIMAG)
Files:          bin.*/evaluator.a

Nature:         Diagnostic sequences are now computed for both evaluation
                strategies (i.e., the "local" one and the "global" one).
                This feature did not exist in the previous version for the 
                global evaluation strategy.

BUG FIX
Number:         549
Date:           Wed Feb 18 17:20:23 MET 1998
Report:         Ghassan Chehaibar (Bull)
Author:         Laurent Mounier (VERIMAG)
Files:          bin.*/aldebaran

Nature:         A bug was fixed in the algorithm used in ALDEBARAN
                for deciding on-the-fly if two LTSs are branching bisimilar 
                (the "-fly -pequ" options were concerned).

BUG FIX
Number:         550
Date:           Wed Feb 18 17:26:14 MET 1998
Report:         Hubert Garavel (INRIA/VASY)
Author:         Laurent Mounier (VERIMAG)
Files:          bin.*/exp2c, bin.*/libexpopen.a

Nature:         The length of the filenames that can be used in a .exp 
                file has been augmented up to 128 characters. The previous
                limitation was not always sufficient for handling the .exp 
                files generated by DES2AUT (for instance in demo_20). 

IMPROVEMENT
Number:         551
Date:           Mon Feb 23 10:29:14 MET 1998
Author:         Charles Pecheur (INRIA/VASY)
Files:          src/xtl/misc.xtl, src/xtl/walk.xtl, src/xtl/walk_actl.xtl,
                src/xtl/walk_print_nice.xtl

Nature:         New XTL libraries have been added, which provide detailed
                diagnostics (annotated execution sequences) justifying the 
                result of the evaluation of CTL and ACTL temporal logic
                formulas. 

IMPROVEMENT
Number:         552
Date:           Mon Feb 23 10:30:14 MET 1998
Author:         Charles Pecheur (INRIA/VASY)
Files:          demos/demo_25

Nature:         A new demo was added: it deals with the verification of
                a CFS (Cluster File System) using CAESAR, ALDEBARAN, 
                EXP.OPEN and XTL.

BUG FIX
Number:         553
Date:           Mon Feb 23 10:14:35 MET 1998
Report:         Mark Jorgensen (INRIA/VASY)
Author:         Laurent Mounier (VERIMAG)
Files:          bin.*/projector.a

Nature:         A minor bug, which prevented projector to generate BCG files,
                has been corrected.

BUG FIX
Number:         554
Date:           Mon Feb 23 16:10:47 MET 1998
Report:         Ghassan Chehaibar (Bull)
Author:         Jean-Pierre Krimm (VERIMAG)
Files:          bin.*/des2aut

Nature:         The preliminary phase of des2aut (i.e., hidden gate
                distribution over parallel compositions) was erroneous
                in some cases. This problem has been corrected.

BUG FIX
Number:         555
Date:           Tue Feb 24 19:04:22 MET 1998
Report:         Hubert Garavel (INRIA/VASY)
Author:         Laurent Mounier (VERIMAG)
Files:          bin.*/aldebaran

Nature:         The diagnostic sequences generated by aldebaran from the 
                two LTSs under comparison were improperly swapped in 
                some cases when using the ``-fly'' options. This problem
                has been corrected.

BUG FIX
Number:         556
Date:           Mon Mar  2 19:37:53 MET 1998
Report:         Charles Pecheur (INRIA/VASY)
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/caesar

Nature:         A bug was fixed in CAESAR, which could cause (in some cases)
                the generation of incorrect LTSs (especially, LTSs with too 
                many transitions). This bug occured because CAESAR tried to 
                optimize a given variable by turning it both into a constant 
                and a register (local variable) at the same time.

IMPROVEMENT
Number:         557
Date:           Tue Mar  3 15:27:59 MET 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          demos/demo_15/:READ_ME, demos/demo_15/verify-all-requirements

Nature:         The demo_15 was improved in order:
                - to use BCG files directly (instead of generating .aut
                  files first and then translating them to .bcg files)
                - to avoid a meaningless error message

IMPROVEMENT
Number:         558
Date:           Mon Mar  9 11:40:31 MET 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          com/bcg_info, bin.sun*/lib_bcg_info.a, man/manl/bcg_info.l,
                src/eucalyptus/eucalyptus.tcl

Nature:         An official "bcg_info" tool was introduced in the CADP 
                release. This new tool replaces the previous undocumented
                versions of "bcg_info". A manual page is provided, which
                is available through the Help button of the EUCALYPTUS
                graphical user-interface. 

BUG FIX
Number:         559
Date:           Wed Mar 11 14:21:47 MET 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/libBCGI_IO.a, bin.*/bcg_io

Nature:         A bug was fixed, which caused "bcg_io" to core dump on
                Solaris 2, when given the "-squiggles" option.

IMPROVEMENT
Number:         560
Date:           Mon Mar 16 12:33:57 MET 1998    
Report:         Judi Romijn (CWI, The Netherlands)
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/libBCG.a, man/manl/bcg_write.l, man/manl/bcg_read.l
                incl/bcg_transition.h, incl/bcg_edges.h, incl/bcg_user.h,

Nature:         An API (programming interface) to read BCG graphs was made
                available and documented (see "man bcg_read" for details).
                Also, the "bcg_write" man page was enhanced with an example.

BUG FIX
Number:         561
Date:           Tue Mar 17 11:28:46 MET 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          com/caesar.aldebaran

Nature:         The "caesar.aldebaran" shell-script was modified in order to 
                invoke "caesar" with option "-more /bin/cat". This avoids a
                deadlock in the EUCALYPTUS user interface.

BUG FIX
Number:         562
Date:           Tue Apr 14 10:50:27 MET DST 1998
Report:         Elie Najm (ENST, Paris)
Author:         Hubert Garavel (INRIA/VASY)
Files:          installator.shar

Nature:         The directory "/usr/openwin/lib" was added to $LD_LIBRARY_PATH
                in order to have proper dynamic libraries under Solaris 2.*

BUG FIX
Number:         563
Date:           Tue Apr 14 11:25:12 MET DST 1998
Report:         Laurence Pierre (Universite de Marseille and TIMA)
Author:         Hubert Garavel
Files:          com/installator, installator.shar

Nature:         A bug was fixed, which would (under some circumstances) cause
                an error message of the form: "error in Tcl script : can't 
                read env(LOGNAME) no such element in array".

BUG FIX
Number:         564
Date:           Tue Apr 14 19:23:28 MET DST 1998
Report:         Bruno Hondelatte and Pierre Kessler (INRIA/VASY)
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/caesar, bin.*/caesar.adt

Nature:         A minor bug was fixed, which could cause CAESAR.ADT and CAESAR
                to emit a "Broken Pipe" message under some circumstances 
                (this message was annoying, but harmless).

BUG FIX
Number:         565
Date:           Tue Apr 14 19:55:25 MET DST 1998
Report:         Jacques Sincennes (University of Ottawa)
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.sun4/caesar, bin.sun4/caesar.adt, bin.*/libcaesar.a

Nature:         A bug was fixed, which could cause CAESAR.ADT and CAESAR
                to emit the following error messages under SunOS 1.* machines:

               /usr/local/gnu/lib/gcc-lib/sparc/2.7.2/include/netinet/in.h:106:
                parse error before `u_char'
               /usr/local/gnu/lib/gcc-lib/sparc/2.7.2/include/netinet/in.h:107:
                parse error before `u_short'

BUG FIX
Number:         566
Date:           Wed Apr 15 22:29:37 MET DST 1998
Report:         Charles Pecheur (INRIA/VASY)
Author:         Radu Mateescu (INRIA/VASY)
Files:          XTL

Nature:         Two minor bugs in XTL 1.1 have been fixed.      

BUG FIX
Number:         567
Date:           Wed Apr 15 23:40:03 MET DST 1998
Authors:        Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files:          BCG

Nature:         A bug was fixed in the low layers of the BCG library, which
                caused some BCG tools and XTL to core dump under Linux. This 
                bug was not visible for Solaris users. 

BUG FIX
Number:         568
Date:           Thu Apr 16 17:47:15 MET DST 1998
Author:         Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files:          BCG

Nature:         Subtle changes have been made in the BCG libraries and 
                include files in order to ensure portability of the BCG files
                across various architectures. This means that BCG files should
                independent from the processor/architecture, so that they can
                be created and read identically under SunOS, Solaris, and 
                Linux environments.

                These changes are upward compatible and should be almost 
                invisible to the user. 

                BCG files generated with any previous version of CADP on 
                Solaris are still valid and can be reused without change.

                However, BCG files generated with beta-versions 97b-* of
                CADP on Linux are invalid: they should be destroyed and
                generated again with the latest version of CADP.

IMPROVEMENT
Number:         569
Date:           Fri Apr 17 12:46:34 MET DST 1998
Report:         Charles Pecheur (INRIA/VASY)
Author:         Hubert Garavel (INRIA/VASY)
Files:          BCG,
                man/manl/bcg_write.l, man/manl/bcg_io.l, man/manl/xtl.l,
                demo_01/:READ_ME, demo_02/:READ_ME, demo_13/*.bcg,
                demo_16/:READ_ME, demo_21/Makefile, demo_22/Makefile, 
                demo_23/Makefile, demo_25/Makefile,
                src/eucalyptus.tcl 

Nature:         The "bcg_write" API (Application Programming Interface) has 
                been improved. The interface itself (see "man bcg_write.l")
                remains unchanged, however, its effects are different. 

                From now on, all the character strings passed to function
                BCG_IO_WRITE_BCG_EDGE() are parsed in order to infer the
                structure and contents of the labels, so that the generated
                BCG files should contain more precise type information.
                The rules for label parsing are described in a section 
                (entitled "Technical Note on Label Parsing") of the 
                "bcg_write.l" manual page.

                As a consequence, the contents of the BCG graphs produced 
                using the "bcg_write" API will be slightly different from 
                those generated with previous versions of CADP. In most
                cases, the difference should not be visible by the user
                (see the "bcg_write.l" manual page for a discussion about
                label normalization).

                Because this change is done in the BCG library, it applies
                to all the CADP tools that generate BCG files, including
                CAESAR, ALDEBARAN, BCG_IO, Generator, Reductor, etc. 

                As regards BCG_IO: the previous version of BCG_IO would
                not perform label parsing unless when reading an ".aut"
                file with the "-parse" option selected. From now on, the
                behaviour is reversed: label parsing will be the default
                behaviour, except when reading an ".aut" file with the
                "-parse" option selected.

                The EUCALYPTUS graphical interface and the demos using
                XTL have been updated not to use the "-parse" option 
                any longer.
        
                Label parsing is especially of interest when using the XTL
                model-checker, which allows to take advantage of the types
                and typed values defined in BCG files. This improvement
                will allow to use consistently the XTL model-checker on
                all the BCG files generated by CADP tools. 

                Note: the BCG files generated with previous versions of CADP
                should be re-generated for a proper use of XTL, except if       
                they were produced from a ".aut" file using the previous 
                version of BCG_IO with the "-parse" selected. An old BCG 
                file, say FILE.bcg, can be upgraded to a new one using the
                following sequence of commands:

                        bcg_io FILE.bcg FILE.aut
                        rm FILE.bcg FILE@1.o
                        bcg_io FILE.aut FILE.bcg

IMPROVEMENT
Number:         570
Date:           Mon Apr 20 20:40:58 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          src/eucalyptus/eucalyptus.tcl

Nature:         The EUCALYPTUS Graphical Interface was improved:
                - by providing the "Indent" command for ".lib" files
                - by setting the "-monitor" option active by default for 
                  the Generator tool.

BUG FIX
Number:         571
Date:           Tue Apr 21 14:25:35 MET DST 1998
Report:         Massimo Zendri (Bull/DYADE)
Authors:        Charles Pecheur and Hubert Garavel (INRIA/VASY)
Files:          bin.*/caesar

Nature:         For very large descriptions (e.g., about 20 processes in
                parallel), CAESAR could signal a deadlock in states from 
                which transitions could actually be fired. This bug was
                caused by the overflow of an integer variable, declared
                as an "unsigned short", although its value could go beyond
                65,536. This bug was fixed.

IMPROVEMENT
Number:         572
Date:           Thu May  7 19:21:37 MET DST 1998
Authors:        Christophe Discours and Hubert Garavel (INRIA/VASY)
Files:          bin.*/libcaesar.a, bin.*/exhibitor.a,
                incl/caesar_regexp.h, incl/caesar_hide_1.h, 
                incl/caesar_rename_1.h.

Nature:         The OPEN/CAESAR library was enriched with three new libraries:
                "caesar_regexp", "caesar_hide_1", and "caesar_rename_1".
                These libraries offer high-level support for handling regular
                expressions, hiding labels and renaming labels.

                The Exhibitor tool was modified to take advantage of these
                new librairies.

IMPROVEMENT
Number:         573
Date:           Fri May 15 10:11:48 MET DST 1998
Authors:        Hubert Garavel, Charles Pecheur, and Mihaela 
		Sighireanu (INRIA/VASY)
Files:          doc/garavel-Sighireanu-98a.ps, doc/Pecheur-98.ps, doc/:READ_ME

Nature:         Two new papers, entitled "Advanced Modelling and Verification 
                Techniques Applied to a Cluster File System" and "Towards a 
                Second Generation of Formal Description Techniques -- Rationale
                for the Design of E-LOTOS", were added to the CADP release. 

BUG FIX
Number:         574
Date:           Sat May 16 14:19:06 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/bcg_io

Nature:         A bug was fixed, which would cause (in a few cases) BCG_IO 
                to stop with an error message of the form: "wrong number of 
                parameters".

IMPROVEMENT
Number:         575
Date:           Sat May 16 16:37:20 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/bcg_io

Nature:         The translation algorithm used by the BCG_IO tool to read
                automata encoded in the FC2 automata and to translate them
                into other formats was extended, so as to accept FC2 files
                in which the initial state is not specified (i.e., when 
                there is no "initial>" directive. Such FC2 files can be
                generated using the Autograph/Atg tool. The previous version 
                of BCG_IO would "core dump" on such incomplete FC2 files. 
                The new version of BCG_IO assumes that, if the initial state
                is not specified, then state 0 is the initial state.

BUG FIX
Number:         576
Date:           Thu May 28 13:03:26 MET DST 1998
Report:         Radu Mateescu (CWI/SEN2)
Author:         Hubert Garavel (INRIA/VASY)
Files:          src/eucalyptus.tcl

Nature:         A bug was fixed in the EUCALYPTUS Graphical User Interface, 
                which caused XTL to be improperly invoked when the $CADP_CC 
                environment variable was set to a complex string such as 
                "gcc -I/usr/include".

IMPROVEMENT
Number:         577
Date:           Thu Jun  4 12:29:19 MET DST 1998
Report:         Axel Belinfante (Univ. of Twente), Elie Najm (ENST, Paris)
Author:         Hubert Garavel (INRIA/VASY)
Files:          com/rfl

Nature:         The old version of RFL would stop as soon as an invalid host
                was detected. The new version will try all hosts, and print
                the list of invalid hosts (if any) before stopping  

IMPROVEMENT
Number:         578
Date:           Thu Jun  4 17:39:45 MET DST 1998
Report:         Axel Belinfante (Univ. of Twente)
Author:         Hubert Garavel (INRIA/VASY)
Files:          src/installator/run_mail, installator.shar

Nature:         From now on, Installator will also send a copy of the LICENSE
                file to the person that is running Installator, so that
                Installator users are aware of the results of the RFL. This
                will also help to detect situations in which the "mail" 
                command does not work properly.

BUG FIX
Number:         579
Date:           Fri Jun  5 10:28:00 MET DST 1998
Report:         Axel Belinfante (Univ. of Twente)
Authors:        Hubert Garavel and Pierre Kessler (INRIA/VASY)
Files:          src/eucalyptus/eucalyptus.tcl, src/eucalyptus/com/xeuca_ps

Nature:         Various problems have been fixed in the "Kill Window" of
                EUCALYPTUS:

                - When resizing the Kill window, the subwindow listing the 
                  processes did not resize as well. This is now the case, 
                  so that the user can display more information about
                  processes to kill.

                - An error message of the form:
                        "ps: no controlling terminal
                             while executing
                         "exec ps | tail +2"
                             invoked from within ...
                  could be printed on Solaris 2.* when clicking on the Kill 
                  button if "/bin" was before "/usr/ucb" in the $PATH variable.
                  This problem is now solved.

                - The Kill window did not display processes without a 
                  controlling terminal. This problem is now solved.

IMPROVEMENT
Number:         580
Date:           Fri Jun 12 09:58:47 MET DST 1998
Authors:        (many)                  
Files:          doc/Mateescu-Garavel-98.ps, doc/Kahlouche-Viho-Zendri-98.ps
                doc/Mateescu-98-b.ps

Nature:         Three new papers have been added, that present the XTL and
                TGV-LOTOS tools.

IMPROVEMENT
Number:         581
Date:           Fri Aug 14 17:48:32 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          man/manl/caesar_hide_1.l, man/manl/caesar_rename_1.l,
                doc/Garavel-92-a.ps, man/manl/aldebaran.l, 
                src/eucalyptus/eucalyptus.tcl, 

Nature:         The manual pages for the new OPEN/CAESAR libraries 
                "caesar_hide_1" and "caesar_rename_1" have been added.

                The OPEN/CAESAR Reference Manual was updated accordingly.

                The ALDEBARAN User Manual was updated to refer the new manual
                pages "caesar_hide_1" and "caesar_rename_1", which give an
                accurate description of the formats for hiding and renaming 
                files.

                The Help window of the EUCALYPTUS graphical interface was
                similarly updated to refer the new manual pages "caesar_hide_1"
                and "caesar_rename_1".

IMPROVEMENT
Number:         582
Date:           Fri Aug 14 17:48:58 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          man/manl/caesar_table_1.l, man/manl/caesar_version.l,
                doc/Garavel-92-a.ps

Nature:         The documentation of the following functions:
                        CAESAR_SEARCH_TABLE_1()
                        CAESAR_SEARCH_AND_PUT_TABLE_1()
                        CAESAR_COMPARE_VERSION()
                        CAESAR_MATCH_VERSION()
                was improved and made more precise. For these functions that
                return a boolean result of type CAESAR_TYPE_BOOLEAN, the text
                fragments "a result different from 0" and "a result equal to 0"
                have been replaced by "CAESAR_TRUE" and "CAESAR_FALSE",
                respectively. 

                Note: this change is totally upward compatible. No modification
                of existing OPEN/CAESAR applications is needed. 

IMPROVEMENT
Number:         583
Date:           Fri Aug 14 19:45:58 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          com/bcg_info, bin.*/libbcg_info.a, man/manl/bcg_info.l

Nature:         A new option ('-size') was added to the BCG_INFO tool, that
                displays the size of a BCG graph (number of states and edges)
                under a single line.

IMPROVEMENT
Number:         584
Date:           Fri Aug 14 19:49:35 MET DST 1998
Authors:        Mihaela Sighireanu (INRIA/VASY) and Ken Turner (Univ. of 
                Stirling, Scotland)
Files:          demos/demo_26

Nature:         A new demo (formal verification of a example of enterprise
                information systems) was added to the CADP distribution.

IMPROVEMENT
Number:         585
Date:           Mon Aug 17 11:58:47 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          com/caesar.aldebaran

Nature:         The "caesar.aldebaran" command was extended so as to handle
                ".bcg" files as well as ".aut" files.

BUG FIX
Number:         586
Date:           Tue Aug 18 15:00:04 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          demo_18/transit_node.exp

Nature:         The ".exp" file contained in demo_18 was syntactically 
                incorrect, which resulted in an error message of the form:
                        exp.open: Generating transit_node.c ...
                        exp2c: syntax error !
                        *** Error code 1
                This ".exp" file (which was indeed a ".des" file, suitable
                for DES2AUT but not EXP.OPEN) was replaced with a correct one.

IMPROVEMENT
Number:         587
Date:           Wed Aug 19 12:05:17 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          demos/* 

Nature:         All the demo exemples have been revisited and improved in
                several respects. The READ_ME files have been updated and
                the commands have been simplified to take advantage of the
                most recent features in CADP.

IMPROVEMENT
Number:         588
Date:           Wed Aug 19 12:18:50 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          */:READ_ME

Nature:         All the files previously named ':READ_ME' have been renamed 
                either into 'READ_ME' or into '=READ_ME.txt', because the
                ':' character cannot be part of file names under Windows.
                This would create problems for people attempting to download
                the demo examples from the VASY FTP server.

BUG FIX
Number:         589
Date:           Tue Aug 25 18:00:05 MET DST 1998
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/libBCG.a, bin.*/libBCG_IO.a

Nature:         A bug was fixed, which caused the BCG library to issue an
                error message of the form:
                        bcg_write_1: wrong natural size in BCG_WRITE_UNSIGNED 
                when attempting to generate a graph with only one label and
                with label parsing activated (which is now the case by default,
                see "man bcg_write" for details). 

BUG FIX
Number:         590
Date:           Wed Aug 26 11:58:16 MET DST 1998
Report:         Christophe Discours (INRIA/VASY)
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/bcg_io

Nature:         A minor bug was fixed, which caused BCG_IO to issue an error 
                message of the form:
                        bcg_file_area: area is missing file in BCG_COPY_AREA
                when invoked with the same BCG file as input and output
                argument, e.g.:
                        bcg_io FILE.bcg FILE.bcg

IMPROVEMENT
Number:         591
Date:           Thu Aug 27 13:04:58 MET DST 1998        
Report:         Charles Pecheur (INRIA/VASY)
Authors:        Christophe Discours and Hubert Garavel (INRIA/VASY)
Files:          bin.*/bcg_labels, man/manl/bcg_labels.l, demo_25

Nature:         A new tool named BCG_LABELS was introduced. This tool allows
                to perform an arbitrary combination of hiding and renaming
                operations on the labels of a BCG graph. See the "bcg_labels"
                manual page for more information.

                The demo_25 was simplified in order to take advantage of this
                new tool. 

                The EUCALYPTUS graphical user-interface was updated to allow
                access to the BCG_LABELS tool: when clicking on an LTS file
                (in BCG or .aut format), two new commands "Hide Labels..."
                and "Rename Labels..." are now available.

BUG FIX
Number:         592
Date:           Mon Aug 31 15:38:15 MET DST 1998
Report:         Guy Tremblay (Universite du Quebec a Montreal, Quebec, Canada)
Author:         Hubert Garavel (INRIA/VASY)
Files:          com/rfl

Nature:         The RFL command was modified to make it independent from
                the value of the LC_TYPE environment variable.

BUG FIX
Number:         593
Date:           Wed Sep 30 13:56:25 MET DST 1998
Author:         Radu Mateescu (INRIA/VASY)
Files:          bin.*/xtl

Nature:         A minor bug was fixed, concerning the printing of messages
                by xtl when called with the -verbose option (when the tool
                was called from the xeuca interface, the results of temporal
                formula evaluation were printed before the informative messages
                issued by the xtl tool).

BUG FIX
Number:         594
Date:           Fri Nov 20 18:35:56 MET 1998
Report:         Ji He (University of Stirling, Dept. of Computing and Maths)
Author:         Radu Mateescu (INRIA/VASY)
Files:          man/manl/xtl.l

Nature:         A minor mistake in the XTL manual was corrected, namely the
                translations of the "forall" and "exists" constructs in terms
                of the "for" expression were permuted.

IMPROVEMENT
Number:         595
Date:           Wed Jan 20 16:12:54 MET 1999
Author:         Mihaela Sighireanu (INRIA/VASY)
Files:          doc/Sighireanu-Turner-98.ps, doc/Kahlouche-Viho-Zendri-99.ps

Nature:         Two new papers have been added in the doc directory. 

BUG FIX
Number:         596
Date:           Mon Jan 25 18:28:13 MET 1999
Report:         Patricia Bournai (IRISA)
Author:         Hubert Garavel (INRIA/VASY)
File:           com/rfl

Nature:         The bug fix #592 (see above) was not sufficient. A different
                fix has been implemented.

IMPROVEMENT
Number:         597
Date:           Mon Jan 25 19:45:01 MET 1999
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/libcaesar.a, man/manl/caesar_hide_1.l, 
                doc/Garavel-92-a.ps, incl/caesar_hide_1.h, incl/caesar_regexp.h

Nature:         The "caesar_hide_1" library has been extended to allow 
                hiding based on "gate matching". This new functionality
                emulates the hiding operator of LOTOS.

                To do so, the last parameter of function CAESAR_CREATE_HIDE_1()
                has been modified. Previously, it was a parameter named 
                CAESAR_PARTIAL_MATCH of type CAESAR_TYPE_BOOLEAN. From now 
                on, it is named CAESAR_KIND and is of type CAESAR_TYPE_NATURAL.

                The "gate matching" facility can be obtained by giving
                the value 2 to the last parameter CAESAR_KIND of function 
                CAESAR_CREATE_HIDE_1 (). 

                This change requires a slight modification of existing code:
                in any call to function CAESAR_CREATE_HIDE_1(), the value of
                the last parameter should be replaced: CAESAR_FALSE should be 
                replaced with 0, CAESAR_TRUE should be replaced with 1.

IMPROVEMENT
Number:         598
Date:           Tue Jan 26 10:12:23 MET 1999
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/libcaesar.a, man/manl/caesar_rename_1.l,
                doc/Garavel-92-a.ps

Nature:         The "caesar_rename_1" library has been extended to allow 
                renaming based on "gate matching". This new functionality
                emulates the renaming operator that exist in modern formal
                description techniques such as E-LOTOS and LOTOS NT.

                The "gate matching" facility can be obtained by giving
                the value 3 to the last parameter CAESAR_KIND of function 
                CAESAR_CREATE_RENAME_1 (). 

                This change is totally upward compatible: existing code does 
                not need to be modified.

IMPROVEMENT
Number:         599     
Date:           Wed Jan 27 10:59:12 MET 1999
Author:         Hubert Garavel (INRIA/VASY)
Files:          bin.*/bcg_labels, man/manl/bcg_labels.l

Nature:         The BCG_LABELS command has been extended to incorporate the
                recently introduced "gate matching" facilities (see #597 and
                #598 above). It is now possible to write:
                        bcg_labels -hide -gate FILE.hid ...
                and/or
                        bcg_labels -rename -gate FILE.ren ...   
                The manual page has been updated. 

VERSION 97b "Liege"


Copyright (C) INRIA 1999 -- Tous droits réservés -- All Rights Reserved.
Back to the CADP Home Page