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

THE CADP NEWSLETTER - Nr. 5
July 13, 2001

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


Contents

1. Availability of CADP 2001 "Ottawa"

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:

2. New features

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.

2.a. The new BCG_MIN tool

2.b. The new EVALUATOR 3.0 tool

2.c. The new OCIS tool

2.d. The new SVL tool

2.e. The new TGV tool

2.f. Enhancements to existing tools

Besides introducing new tools, CADP 2001 "Ottawa" also brings significant improvements to existing tools:

3. How to upgrade?

3.a. System requirements

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.

3.b. Potential compatibility issues

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":

If you face unexpected problems, and do not find the solution in the HISTORY file, do not hesitate to contact cadp@inrialpes.fr

4. Credits and acknowledgements

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 advices about the use of CADP:

and all other persons we may forget.

5. Release notes for CADP 2001 "Ottawa"


VERSION 97b "Liege"
IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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. 

BUG FIX
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). 

BUG FIX
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.

IMPROVEMENT
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.

BUG FIX
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. 

BUG FIX
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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 "!="

BUG FIX
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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).

IMPROVEMENT
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).

IMPROVEMENT
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().

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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.

IMPROVEMENT
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. 

IMPROVEMENT
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 "caesar@imag.fr" was replaced with 
                  "cadp@inrialpes.fr" (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. 

IMPROVEMENT
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.

BUG FIX
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 ':'.

IMPROVEMENT
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.

BUG FIX
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).

BUG FIX
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.

IMPROVEMENT
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.

IMPROVEMENT
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). 

IMPROVEMENT
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.

BUG FIX
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).

BUG FIX
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.

IMPROVEMENT
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.

IMPROVEMENT
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"

BUG FIX
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.

IMPROVEMENT
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. 

BUG FIX
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. 

BUG FIX
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.

IMPROVEMENT
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). 

BUG FIX
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.

IMPROVEMENT
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. 

IMPROVEMENT
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.

BUG FIX
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".

BUG FIX
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.

IMPROVEMENT
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

BUG FIX
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).

IMPROVEMENT
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.

BUG FIX
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.

IMPROVEMENT
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.

BUG FIX
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. 

IMPROVEMENT
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

BUG FIX
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

BUG FIX
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".

BUG FIX
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).

BUG FIX
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.

BUG FIX
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.

BUG FIX
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.

IMPROVEMENT
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.

BUG FIX
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.

BUG FIX
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.         

BUG FIX
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

BUG FIX
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.

IMPROVEMENT
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.

BUG FIX
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.

BUG FIX
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.

BUG FIX
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").

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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.

IMPROVEMENT
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.

BUG FIX
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 foo@1.o was left unchanged in the current directory.
                  This could be a problem, because foo@1.o was related to the
                  original file, but not the modified one. The solution is to
                  remove foo@1.o.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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".

IMPROVEMENT
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

IMPROVEMENT
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.

BUG FIX
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. 

BUG FIX
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.

IMPROVEMENT
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)

BUG FIX
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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. 

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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".  

BUG FIX
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 FILE@1.o
                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 FILE@1.o). This would leave the
                user's environment in an inconsistent state.

                The identification string contained in each dynamic library
                FILE@1.o 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 FILE@1.o obsolete, so that FILE@1.o will be regenerated
                as soon as a BCG tool is applied to FILE.bcg.

BUG FIX
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).

BUG FIX
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.

BUG FIX
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).

IMPROVEMENT
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.

IMPROVEMENT
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 FILE@1.o, FILE@2.o...
                (if any) will be removed. This removal will clean the user's
                environment automatically.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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).

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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.

IMPROVEMENT
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).

BUG FIX
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"

BUG FIX
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.

BUG FIX
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.

BUG FIX
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.

BUG FIX
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"

IMPROVEMENT
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.

BUG FIX
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."

BUG FIX
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).

BUG FIX
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".

IMPROVEMENT
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.

BUG FIX
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"

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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

IMPROVEMENT
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). 

IMPROVEMENT
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.

BUG FIX
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.

IMPROVEMENT
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.

BUG FIX
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.

BUG FIX
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. 

IMPROVEMENT
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.

BUG FIX
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.

BUG FIX
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''.

BUG FIX
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.

BUG FIX
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.

IMPROVEMENT
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").

BUG FIX
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.

IMPROVEMENT
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.

BUG FIX
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. 

BUG FIX
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.

IMPROVEMENT
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.

BUG FIX
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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.

BUG FIX
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.

BUG FIX
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.

BUG FIX
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.

BUG FIX
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. 

BUG FIX
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.

IMPROVEMENT
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.

BUG FIX
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.

BUG FIX
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.

BUG FIX
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.

BUG FIX
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.

BUG FIX
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.

BUG FIX
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.

BUG FIX
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.

IMPROVEMENT
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.

BUG FIX
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.

IMPROVEMENT
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). 

IMPROVEMENT
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.

IMPROVEMENT
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.

IMPROVEMENT
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.

BUG FIX
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.

IMPROVEMENT
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.

VERSION 2001 "Ottawa"
Copyright (C) INRIA 2001 -- Tous droits réservés -- All Rights Reserved.

Back to the CADP Home Page