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

THE CADP NEWSLETTER - Nr. 6
April 19, 2007

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


Contents

1. Availability of CADP 2006 "Edinburgh"

The VASY team of INRIA Rhone-Alpes is pleased to announce the availability of a new release of the CADP toolbox.

The new version of CADP is named 2006 "Edinburgh" and dated December 12, 2006. It supersedes all previous versions of CADP.

We are happy to dedicate CADP 2006 "Edinburgh" to Laboratory for Foundations of Computer Science at the University of Edinburgh, as a tribute to their achievements in concurrency theory.

This is a brief chronology of past events:

2. Major enhancements

The new release CADP 2006 "Edinburgh" delivers a total of 150 bug fixes and 245 improvements. In particular, it introduces 15 new tools and libraries: BCG_GRAPH, BCG_MERGE, BCG_STEADY, BCG_TRANSIENT, BISIMULATOR, CAESAR.BDD, CAESAR 7.0, CAESAR_SOLVE, DETERMINATOR, DISTRIBUTOR, EVALUATOR 3.5, EXP.OPEN 2.0, PROJECTOR 2.0, REDUCTOR 5.0, and SEQ.OPEN, which we present hereafter.

2.a. The new BCG_GRAPH tool

2.b. The new BCG_MERGE tool

2.c. The new BCG_STEADY tool

2.d. The new BCG_TRANSIENT tool

2.e. The new BISIMULATOR tool

2.f. The new CAESAR 7.0 tool

2.g. The new CAESAR.BDD tool

2.h. The new CAESAR_SOLVE library

2.i. The new DETERMINATOR tool

2.j. The new DISTRIBUTOR tool

2.k. The new EVALUATOR 3.5 tool

2.l. The new EXP.OPEN 2.0 tool

2.m. The new PROJECTOR 2.0 tool

2.n. The new REDUCTOR 5.0 tool

2.o. The new SEQ.OPEN tool

3. Other enhancements

Besides introducing new tools, CADP 2006 "Edinburgh" also brings significant improvements to existing tools:

4. How to upgrade?

4.a. System requirements

CADP 2006 "Edinburgh" can be used on the following computers/operating systems:

4.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 2006 "Edinburgh":

So far, the rare problems related to changing the version of CADP that have been reported to us were easily fixed by modifying a few lines of code. If you face unexpected problems, and do not find the solution in the HISTORY file or by applying the conversion script "$CADP/com/upc" to your existing C file(s), do not hesitate to contact cadp@inrialpes.fr

5. Credits and acknowledgements

The following scientists contributed to the development of CADP 2006 "Edinburgh":

We are extremely grateful to the following scientists, who provided us with valuable feedback and advice about the use of CADP:

and all other persons we may forget.

6. Release notes for CADP 2006 "Edinburgh"


VERSION 2001 "Ottawa"
IMPROVEMENT
Number:		771
Date: 		Tue Aug 28 16:34:50 MEST 2001
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.sun4, games/bin.sun4, gc/bin.sun4, tcl-tk/bin.sun4,
		INSTALLATION, INSTALLATION_2, INSTALLATION_4.

Nature:		The "sun4" architecture will no longer be supported after
		CADP 2001 "Ottawa": consequently, SunOS 4.1.* binaries have
		been removed from the CADP distribution. The installation
		files have been updated accordingly.

IMPROVEMENT
Number:		772
Date: 		Tue Aug 28 17:59:11 MEST 2001
Authors:	Hubert Garavel, Bruno Ondet, Frederic Perret (INRIA/VASY)
Files:		demos/demo_19/graphics/doc/*.{ps,pdf},
		demos/demo_25/cfs.{ps,pdf}, demos/demo_25/=READ_ME.txt,
		doc/=READ_ME.txt, doc/dvi/*.dvi, doc/ps, doc/pdf,
		man/pdf, man/*/projector.*, man/*/caesar.adt.*, man/*/svl.*,
		src/com/cadp_postscript, src/eucalyptus/eucalyptus.tcl

Nature:		The PostScript documents of the CADP distribution are now
		also available in Adobe's PDF format. This required many
		changes:

		- In the "demos" directory: PDF files have been added for
		  demos 19 and 25 and the existing PostScript files have been 
		  compressed in order to save space.

		- In the "doc" directory: all PostScript documents for which
		  we had the LaTeX source available have been regenerated
		  using vectorial fonts instead of bitmap fonts; the PDF
		  files have been added; the existing documents have been 
		  organized in three sub-directories named doc/dvi, doc/ps, 
		  and doc/pdf; PostScript files have been compressed.

		- In the "man" directory: a new sub-directory named man/pdf
		  has been added; the manual pages referring to PostScript
		  files named doc/*.ps have been updated.
		   
		- The shell-script src/com/cadp_postscript has been extended
		  to display compressed PostScript files (with extension
		  ".ps.Z"), which are uncompressed on the fly.

		- The EUCALYPTUS graphical user-interface has been extended
		  to handle compressed PostScript files.

BUG FIX
Number:		773
Date: 		Fri Aug 31 15:28:31 MEST 2001
Report:		Bert Lisser (CWI, The Netherlands), Benoit Fraikin (Univ. of
		Sherbrooke, Canada)
Author:		Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_hostname, com/tst, com/rfl

Nature:		Three shell-scripts ("cadp_hostname", TST, and RFL) have been
		updated so as to avoid an incorrect warning emitted by "tst":
		   License file ``$CADP/LICENSE'' exists
		   *** No license exists for host ``xxx''
		   ==> Read the INSTALLATION file to apply the RFL procedure

BUG FIX
Number:		774
Date:		Wed Oct  3 17:55:33 MEST 2001
Report:		Holger Hermanns (University of Twente)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel

Nature:		SVL could generate ``.exp'' files containing a "hide all but"
		operator, which is not available for this format. This was not
		accepted by the tools reading the EXP format (ALDEBARAN, 
		EXP.OPEN, etc.). The "all but" feature is at now processed
		correctly using the BCG_LABELS tool.

BUG FIX
Number:		775
Date:		Thu Oct  4 10:00:32 MEST 2001
Authors:	Frederic Lang and Hubert Garavel (INRIA/VASY)
Files:		com/svl, bin.*/svl_kernel, src/svl/standard

Nature:		Option -sh of SVL was not working properly (shell options 
		passed to SVL were ignored). This problem was fixed.

		Also, all warnings and error messages issued by SVL have been
		rewritten in order to be simpler and self-explanative.

BUG FIX
Number:		776
Date: 		Mon Oct 15 18:48:52 MEST 2001
Authors:	Hubert Garavel (INRIA/VASY) and Holger Hermanns (Univ. Twente)
Files:		man/*/bcg_min.*

Nature:		The manual page of BCG_MIN was modified to be compatible with
		the BCG_MIN tool: when option "-rate" is selected, BCG_MIN will
		check for conflicts between "rate" and hidden transitions (and
		remove conflicting "rate" transitions) if the "-branching"
		option is selected (when the "-strong" option is selected,
		no such checking is done).  

BUG FIX
Number:		777
Date: 		Thu Oct 18 15:54:17 MEST 2001
Report:		Thomas Arts (Ericsson, Sweden)
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard, bin.*/svl_kernel

Nature:		When processing an instruction of the form:
			"file.bcg" = rename A -> B in "file.aut"
	 	SVL would generate "file.bcg" and remove it afterwards. SVL
		was designed under the assumption that two files with the
		same prefix would necessarily represent LTSs with the same
		behavior. Hence, if "file.aut" had to be converted to the BCG
		format, then the converted graph was stored in "file.bcg",
		but still considering that "file.bcg" was a temporary file
		that should be removed when SVL terminates.

		Although documented in the SVL manual, this assumption proved
		to be over-constraining, as users may ignore SVL conventions
		or forget about them. To avoid user files from being removed
		or modified accidentally, this assumption has been abandoned
		in the new version of SVL, in which every temporary file is
		given a unique name.

BUG FIX
Number:		778
Date: 		Thu Oct 25 17:58:11 MEST 2001
Report:		Holger Hermanns (University of Twente)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel

Nature:		Strings enclosed in quotes were converted to uppercase. This
		has been changed since it did not satisfy the specification of
		SVL.

IMPROVEMENT
Number:		779
Date:		Mon Nov 19 11:15:18 MET 2001
Report:		Thomas Arts (Ericsson, Sweden)
Authors: 	Frederic Lang and Hubert Garavel (INRIA/VASY)
Files:		com/svl, man/*/svl.*, src/eucalyptus/eucalyptus.tcl

Nature:		SVL scripts can now be parameterized with arguments passed on
		the command line when the SVL compiler is invoked. These 
		parameters are referred to using the classical notations: $#, 
		$*, $@, $1, $2, etc., exactly as in Bourne shell scripts.

		The EUCALYPTUS graphical user-interface was modified: when
		an SVL script is to be executed, a window opens, in which it
		is possible to input the aforementioned parameters.

IMPROVEMENT
Number:		780
Date: 		Mon Nov 19 16:28:20 MET 2001
Author:		Frederic Lang (INRIA/VASY)
Files:		demos/demo_20/=READ_ME.txt, demos/demo_27/=READ_ME.txt

Nature:		The =READ_ME.txt files of demos 20 and 27 have been extended
		with performance tables for compositional verification.

IMPROVEMENT
Number:		781
Date: 		Thu Nov 22 12:06:30 MET 2001
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		bin.*/bcg_io, bin.*/libBCG_IO.a, man/*/bcg_io.*, 
		src/eucalyptus/eucalyptus.tcl

Nature:		A new option ``-graphviz'' was added to BCG_IO in order to
		produce the ``.dot'' format needed by ATT's graph visualization
		package GRAPHVIZ. This offers to CADP users a new mean to
		visualize BCG graphs, in addition to the advanced capabilities
		already provided by BCG_DRAW and BCG_EDIT.

		In the EUCALYPTUS graphical user-interface, this functionality
		is now accessible using the "Convert" item in contextual menus.

IMPROVEMENT
Number:		782
Date: 		Thu Jan 17 18:56:17 MET 2002
Authors:	Hubert Garavel, Frederic Lang, and Radu Mateescu (INRIA/VASY)
Files:		doc/*/Garavel-Mateescu-Smarandache-01.*,
		doc/*/Garavel-Lang-Mateescu-01.*,
		doc/*/Garavel-Lang-Mateescu-02.*,
		doc/*/Lang-02.*, doc/=READ_ME.txt

Nature:		A revised version of the Garavel-Mateescu-Smarandache-01 paper
		has been installed in the "doc" directory. Three new papers 
		(on CADP 2001, SVL, and LOTOS NT respectively) have also been
		added.

IMPROVEMENT
Number:		783
Date: 		Fri Jan 18 18:47:41 MET 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/des2aut, bin.*/READ_ME, man/*/des2aut.*

Nature:		As foreseen (see item #729 above), the Des2Aut tool has been
		removed, since Des2Aut is superseded by SVL entirely. 

BUG FIX
Number:		784
Date: 		Thu Apr  4 10:36:30 MEST 2002
Report:		Solofo Ramangalahy (BULL)
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/caesar.open

Nature:		A bug was fixed in the "caesar.open" shell-script, which
		prevented the "-include" option from working correctly.

BUG FIX
Number:		785
Date:		Thu Apr  4 12:54:09 MEST 2002
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard

Nature:		The string prefixing failure labels in PROJECTOR and EXP.OPEN
		had changed from ":fail:" to ":FAIL:". The change has now been
		passed on to SVL, checking the presence of ":FAIL:" in LTSs
		generated compositionally using abstraction.

IMPROVEMENT
Number:		786
Date: 		Wed Apr 10 10:27:36 MEST 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/libcaesar.a

Nature:		Various enhancements have been brought to OPEN/CAESAR's
		"caesar_table_1" library:

		- Function CAESAR_PRINT_TABLE_1() now displays statistics
		  about the average, minimal, and maximal length of collision
		  lists.

		- When the user specifies a maximal number of elements in 
		  the table (by giving to the parameter CAESAR_LIMIT_SIZE of
		  CAESAR_CREATE_TABLE_1() a value different from zero),
		  changes were made to reduce the number of pages, the size
		  of pages, and the number of hash table entries. For tables
		  with few elements, the gain in memory can be up to 75,000
		  bytes per table, together with a noticeable gain in speed.

IMPROVEMENT
Number:		787
Date: 		Mon Apr 15 17:11:43 MEST 2002
Author:		Radu Mateescu (INRIA/VASY)
Files:		doc/*/mateescu-02.*

Nature:		A new paper on EVALUATOR has been added to the CADP release.

BUG FIX
Number:		788
Date: 		Fri Apr 19 18:34:24 MEST 2002
Report:		Arnaud Gavara (Ecoles des Mines de Nancy, France)
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/rfl

Nature:		In some cases (depending on the environment variable LC_ALL),
		the RFL command could generate an invalid license file, in
		which the dates were not expressed in English. This problem
		was solved.

IMPROVEMENT
Number:		789
Date: 		Mon Apr 22 18:50:09 MEST 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/cadp_memory, com/swapsize, INSTALLATION_2,
		src/com/open_caesar/predictor.c, man/*/predictor.l

Nature:		The "com/swapsize" command has been replaced by an improved
		version named "bin.*/cadp_memory". This new version brings
		support for the Windows operating system; it also gives more
		accurate results for Solaris and Linux; finally, it takes
		into account the new environment variable $CADP_MEMORY
		described in the updated version of file INSTALLATION_2.

		The PREDICTOR tool of OPEN/CAESAR has been modified to use
		"cadp_memory" instead of "swapsize". Its manual page has been
		updated.

IMPROVEMENT
Number:		790
Date: 		Tue Apr 23 09:35:26 MEST 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/cadp_hostinfo, bin.*/hostinfo, com/rfl, com/tst,
		src/eucalyptus/eucalyptus.tcl

Nature:		To avoid conflicts with other software, the program "hostinfo"
		in directory $CADP/bin.* has been renamed into "cadp_hostinfo".
		The RFL, TST, and EUCALYPTUS tools have been updated 
		accordingly.

IMPROVEMENT
Number:		791
Date: 		Tue Apr 30 09:12:56 MEST 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_*.h, bin.*/libcaesar.a, bin.*/libbcg_open.a,
		bin.*/caesar, bin.*/exp2c, bin.*/libseq_open.a,
		man/*/caesar_standard.*, doc/*/Garavel-92-a.*

Nature:		The OPEN/CAESAR include files (contained in $CADP/incl) have
		been enhanced in several respects:

		- The C function prototypes have been activated in order to
		  enable C++ compiling.

		- A bug was fixed in file "caesar_diagnostic_1.h" regarding
		  the type of the first arguments of the two functions 
		  CAESAR_CREATE_DIAGNOSTIC_1() and CAESAR_DELETE_DIAGNOSTIC_1()
		  which are of type (CAESAR_TYPE_DIAGNOSTIC_1 *) instead of
		  CAESAR_TYPE_DIAGNOSTIC_1.

		- The "caesar_graph.h" file was modified to ensure that types
		  CAESAR_TYPE_STATE and CAESAR_TYPE_LABEL are systematically
		  defined, since these types are used in function prototypes
		  (such as CAESAR_COMPARE_STATE()).

		- All OPEN/CAESAR compliant compilers (i.e., BCG_OPEN,
		  CAESAR, EXP.OPEN, and SEQ.OPEN) have been updated so as
		  not to define CAESAR_TYPE_STATE and CAESAR_TYPE_LABEL
		  any longer, but instead to import the definitions present
		  in file "caesar_graph.h" (this requires to set, in the C
		  code generated or used by these compilers, the macro
		  CAESAR_GRAPH_IMPLEMENTATION to an integer number expressing
		  the current OPEN/CAESAR version number).

		- The "caesar_graph" manual page was updated to explain how
		  to define the CAESAR_GRAPH_IMPLEMENTATION macro and the
		  CAESAR_TYPE_STATE and CAESAR_TYPE_LABEL types.

IMPROVEMENT
Number:		792
Date: 		Tue Apr 30 20:37:14 MEST 2002
Report:		Jack Abily and Solofo Ramangalahy (BULL)
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_kernel.h, bin.*/caesar

Nature:		The C function prototypes contained in file "caesar_kernel.h"
		file, which defines the EXEC/CAESAR API, have been activated.
		Also, file "caesar_kernel.h" now defines the CAESAR_TYPE_STATE
		and CAESAR_TYPE_LABEL types, in the same way as for file
		"caesar_graph.h" (see item #791 above). The C code generated
		by CAESAR with option "-exec" has been updated to reflect
		these changes.

IMPROVEMENT
Number:		793
Date:		Tue May 21 15:24:19 MEST 2002
Report:		Hubert Garavel (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard, bin.*/svl_kernel, man/*/svl.l

Nature:		It is now possible to use shell variables in process calls.
		To this aim, process calls can be written between quotes.
		Examples:

		(1) % for PROC in RECEIVER TRANSMITTER MEDIUM1 MEDIUM2
		    % do
		       "$PROC.bcg" = generation of "bitalt.lotos":"$PROC"
		    % done
		generates in turn the graphs of "bitalt.lotos":RECEIVER,
		"bitalt.lotos":TRANSMITTER, "bitalt.lotos":MEDIUM1, and 
		"bitalt.lotos":MEDIUM2.

		(2) % for PROC in P1 P2
		    % do
		    % for GATE in SEND RECV
		    % do
		       "$PROC_$GATE.bcg" =
			   generation of "spec.lotos":"$PROC [$GATE]"
		    % done
		    % done
		generates in turn the graphs of "spec.lotos":P1 [SEND],
		"spec.lotos":P1 [RECV], "spec.lotos":P2 [SEND], and
		"spec.lotos":P2 [RECV].

		Similarly, gates (occurring in parallel composition, semi-
		composition operators, and process calls) and process 
		identifiers can now be specified using shell variables 
		(enclosed between double quotes). In Example (2) above,
		"$PROC [$GATE]" can equivalently be written "$PROC" ["$GATE"].
		In particular, it is now possible to parameterize parallel 
		composition expressions, as in the following SVL script:
		   "result.bcg" = "$1.bcg" |[ "$3" ]| "$2.bcg"
		   (* usage : svl arg1 arg2 arg3
		    * where arg1 and arg2 are two BCG graphs to compose in
		    * parallel, and arg3 denotes the gates on which these
		    * graphs must be synchronized. For instance, 
		    *    svl file1 file2 "G1, G2"
		    * computes "file1.bcg" |[G1, G2]| "file2.bcg"
		    *)

IMPROVEMENT
Number:		794
Date: 		Fri May 31 11:13:44 MEST 2002
Authors:	Hubert Garavel and Bruno Ondet (INRIA/VASY)
Files:		INSTALLATION_0, INSTALLATION_2, cadp_cygwin.com
		com/tst, src/com/cadp_postscript, src/com/cadp_psbox

Nature:		The directives for installation have been updated to take
		into account the recent versions of Cygwin, GhostScript,
		and Gsview, and to mention that ".profile" rather than 
		".bashrc" should be used as the startup file.

		The "tst" command has been updated to report when an existing
		".bashrc" file should be renamed into ".profile", and to
		reflect the fact that recent versions of Cygwin (1.3.10 and
		beyond) come with a "/bin/indent" command.

BUG FIX
Number:		795
Date: 		Thu Jun  6 11:31:57 MEST 2002
Report:		Clara Benac Earle (University of Kent at Canterbury, UK)
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard

Nature:		ALDEBARAN might take a lot of memory when minimizing for the
		safety equivalence minimization ("-smin" option). In the case
		of abstraction interface graphs, when this minimization failed,
		SVL did not try to apply minimization for stronger equivalence
		first, before applying safety minimization. This was fixed:
		the safety minimization of abstraction interfaces now invokes
		the advanced minimization function of SVL, i.e., if ALDEBARAN
		fails, SVL will invoke first BCG_MIN with a stronger equiva-
		lence than safety, and later retry ALDEBARAN on the minimized
		graph.

IMPROVEMENT
Number:		796
Date: 		Fri Jun  7 15:21:12 MEST 2002
Authors:	Hubert Garavel and Bruno Ondet (INRIA/VASY)
Files:		bin.*/caesar

Nature:		The maximal number of states that can be stored by CAESAR was
		increased from 16,777,216 (i.e., 2^24) up to 4,294,967,296
		(i.e., 2^32). On Intel-based machines (architectures "iX86"
		and "win32"), accesses have been made faster by using word
		operations instead of byte operations.

IMPROVEMENT
Number:		797
Date: 		Tue Jun 25 09:19:03 MEST 2002
Report:		Vincent Bories-Azeau (CNES, Toulouse) and Gilles Stragier
		(INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/bcg_*.h

Nature:		C function prototypes have been added to all BCG functions
		declared in the "bcg_*.h" include files. This enables 
		programs written in C++ to invoke the BCG primitives.

BUG FIX
Number:		798
Date: 		Tue Jun 25 18:50:22 MEST 2002
Report:		Salem Derisavi (Univ. of Illinois at Urbana/Champaign, USA)
Authors:	Holger Hermanns (Univ. of Sarrebruck, Germany) and Hubert
		Garavel (INRIA/VASY)
Files:		bin.*/bcg_min

Nature:		A bug in BCG_MIN was discovered: when minimizing certain 
		stochastic systems, the reduced Markov chain produced by 
		BCG_MIN was not always minimal (i.e., in some cases, it did
		not satisfy the strong lumping condition). This problem was
		fixed.

IMPROVEMENT
Number:		799
Date: 		Fri Jun 28 11:10:55 MEST 2002
Authors:	Hubert Garavel and Bruno Ondet (INRIA/VASY)
Files:		bin.*/bcg_io, bin.*/libBCG_IO.a, man/*/bcg_io.*, 
		src/eucalyptus/eucalyptus.tcl

Nature:		Two new options ``-gml'' and ``-vcg'' were added to BCG_IO in
		order to produce the ``.gml'' and ``.vcg'' formats needed by
		the graph drawing tools TULIP and VCG (for more information
		see http://dept-info.labri.u-bordeaux.fr/~auber/projects/tulip
		and http://rw4.cs.uni-sb.de/~sander/html/gsvcg1.html
		respectively). This provides two new ways to visualize BCG 
		graphs, in addition to BCG_DRAW and BCG_EDIT, and to the
		Graphviz connection (see above #781).

		In the EUCALYPTUS graphical user-interface, this functionality
		is now accessible using the "Convert" item in contextual menus.

BUG FIX
Number:		800
Date: 		Sat Jun 29 10:41:33 MEST 2002
Report:		Jack Abily and Solofo Ramangalahy (BULL)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar

Nature:		In the C code generated by CAESAR (using any option such as
		"-aldebaran", "-bcg", "-exec", "-open", "-simulator"), two
		pointers remained uninitialized (one in the table of positions
		and one in the table of successors), which could lead to 
		errors (segmentation fault / core dump) on some examples.
		This problem was fixed.

IMPROVEMENT
Number:		801
Date: 		Thu Jul  4 19:59:46 MEST 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		doc/*/Garavel-Hermanns-02.*, doc/=READ_ME.txt

Nature:		A technical report explaining how to use CADP for 
		compositional verification and performance evaluation of
		probabilistic/stochastic systems was added.

IMPROVEMENT
Number:		802
Date:		Fri Jul 19 14:27:13 MEST 2002
Report: 	Nicolas Stouls (LSR-IMAG, Grenoble, France)
Author:		Hubert Garavel (INRIA/VASY)
Files:		man/*/bcg_read.*, man/*/bcg_write.*

Nature:		The "bcg_read" and "bcg_write" manual pages have been enhanced
		by giving the command-line needed to compile programs making
		use of the "bcg_read" and "bcg_write" APIs.

IMPROVEMENT
Number:		803
Date: 		Fri Jul 19 14:41:51 MEST 2002
Report:		Thierry Heuillard (France Telecom R&D)
Author:		Hubert Garavel (INRIA/VASY)
Files:		INSTALLATION_0

Nature:		The directives for installing Cygwin on Windows have been 
		enhanced in order to use the option "Use IE5 Settings" when
		FTP transfers must be done through a proxy.

IMPROVEMENT
Number:		804
Date: 		Fri Aug  2 20:02:26 MEST 2002
Report:		Mostefa Belarbi (INSA Lyon, France)
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/rfl

Nature:		RFL has been enhanced to check the validity of the arguments
		given with its options "-f", "-d", "-i", "-l", "-n", and "-a"
		and to emit better error messages when such arguments are
		missing or incorrect.

BUG FIX
Number:		805
Date: 		Fri Aug 23 15:27:47 MEST 2002
Report:		Pavel Burget (Czech Technical University) 
Author:		Hubert Garavel (INRIA/VASY)
Files:		gc/bin.*/libgc.a

Nature:		The Boehm-Demers garbage collection library has been upgraded
		from version 5.3 to version 6.0. The version 5.3 used so far
		was not compatible with Linux RedHat 7.3 and would cause a
		segmentation fault when invoking CAESAR with "-gc" option.

BUG FIX
Number:		806
Date:		Wed Sep  4 17:08:11 MEST 2002
Author:		Frederic Lang (INRIA/VASY)
Files:		src/installator/installator.tcl

Nature:		In the case where $CADP and $CADP_TMP would be located in
                the same disk partition (which is unfrequent on Unix, but
		may occur on Windows/Cygwin), INSTALLATOR would not check
		properly that sufficient disk space is available to install
		CADP, and thus could finish abruptly. This problem was fixed. 

BUG FIX
Number:		807
Date: 		Mon Sep 23 20:29:37 MEST 2002
Report:		Pierre-Olivier Ribet (LAAS-CNRS, Toulouse, France)
Authors:	Nicolas Decoubes, Hubert Garavel, and Bruno Ondet (INRIA/VASY)
Files:		com/bcg_info, bin.*/libbcg_info*, man/*/bcg_info.*,
		man/*/aldebaran.*

Nature:		Contrary to what was stated in the ALDEBARAN manual page,
		the "-path" option of ALDEBARAN does not always compute the
		shortest path leading to a given state: for one example
		considered at LAAS-CNRS, ALDEBARAN produced at path with 1232
		transitions whereas the shortest path has 852 transitions only.

		The problem has been addressed in several ways:
		- The manual page for ALDEBARAN was updated to mention that
		  option "-path" does not always produce the shortest path;
		- The BCG_INFO tool was enhanced with a new option "-path"
		  that computes the shortest path; see "man bcg_info" for
		  details.

IMPROVEMENT
Number:		808
Date: 		Tue Sep 24 14:55:28 MEST 2002
Authors:	Hubert Garavel and Bruno Ondet (INRIA/VASY)
Files:		com/bcg_info, bin.*/libbcg_info*, man/*/bcg_info.*

Nature:		Besides the aforementioned "-path" option, BCG_INFO was 
		enhanced with many new options, including "-branching", 
		"-compact", "-deadlock", "-deterministic", "-hidden", "-line",
		"-unreachable", and "-verbose". See "man bcg_info" for a
		description of these new features.

IMPROVEMENT
Number:		809
Date: 		Wed Sep 25 12:03:38 MEST 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/xeuca, src/com/xeuca_man, src/eucalyptus/eucalyptus.tcl,
		src/eucalyptus/xeucarc_standard, man/*/xeuca.*

Nature:		The EUCALYPTUS graphical user interface has been updated in
		several respects:

		- To display general properties of LTSs, EUCALYPTUS now uses
		  "bcg_info" (instead of "aldebaran -info", which is kept
		  but only for ".exp" files). 

		- To display the path leading to a given state (menu "Find
		  Path to State..."), EUCALYPTUS now uses "bcg_info -path"
		  rather than "aldebaran -path".

		- To search for deadlocks in LTSs, EUCALYPTUS now uses 
		  "bcg_info -deadlock" rather than "aldebaran -dead".

		- Two new menu entries for LTSs have been added: "Find
   		  nondeterminism..." and "Find unreachable states", which
		  make use of the new features of BCG_INFO.
		
		- For ".aut", ".bcg", ".exp", ".fc2", and ".seq" files,
		  the menu entry "Information" was renamed into "Properties"
		  and moved at the bottom of the menu list.

		- The Eludo tool was removed from EUCALYPTUS, since the
		  Eludo toolkit can only be used on Sparc machines running
		  SunOS 4.1.3, whereas CADP no longer support SunOS 4.*
		  machines. 

BUG FIX
Number:		810
Date: 		Fri Sep 27 15:49:10 MEST 2002
Report:		Radu Mateescu (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/libcaesar.a

Nature:		In function CAESAR_PRINT_TABLE_1() of OPEN/CAESAR's "table_1"
		library, the statistics displayed for "successes" and 
		"failures" were permuted; the correct order was restored.

BUG FIX
Number:		811
Date: 		Fri Sep 27 16:26:58 MEST 2002
Report:		Radu Mateescu (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/libcaesar.a

Nature:		Function CAESAR_COPY_EDGE_LIST(L1, L2) had a bug: when list
		L2 was empty, the value of *L1 was left uninitialized instead
		of being set to NULL. This problem was fixed. 

BUG FIX
Number:		812
Date: 		Fri Sep 27 17:45:04 MEST 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/libcaesar.a

Nature:		Contrary to the OPEN/CAESAR manual, the formatting function
		CAESAR_FORMAT_EDGE_LIST() had no effect: the ouptut of 
		CAESAR_PRINT_EDGE_LIST() was controlled by CAESAR_FORMAT_EDGE()
		instead of CAESAR_FORMAT_EDGE_LIST(). This problem was solved.

BUG FIX
Number:		813
Date: 		Wed Oct  2 15:21:27 MEST 2002
Report:		Radu Mateescu (INRIA/VASY)
Author:		Laurent Mounier (VERIMAG)
Files:		bin.*/aldebaran

Nature:		A bug was corrected concerning the ``-imin'' option of
		ALDEBARAN (minimization modulo the tau*.a equivalence
		relation). On graphs larger than 65536 states, this option
		produced incorrect minimized graphs (not equivalent to the
		initial graphs modulo the tau*.a relation).

IMPROVEMENT
Number:		814
Date: 		Fri Oct  4 10:27:16 MEST 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_graph.h, man/*/caesar_graph.*, man/*/caesar_edge.*,
		doc/*/Garavel-92-a.*, 
		bin.*/caesar, bin.*/libbcg_open.a, bin.*/libcaesar.a,
		src/open_caesar/declarator.c, src/com/cadp_decl, com/upc

Nature:		The CAESAR_RANK_LABEL() function was removed from OPEN/CAESAR's 
		"caesar_graph" API, for three reasons:
		- This function was difficult to implement when the set of
		  labels was not known in advance, and in absence of any
		  particular information on the form/structure of labels.
		- The computations needed to implement CAESAR_RANK_LABEL(),
		  i.e., a quick sort on the label strings, would slow down
		  BCG_OPEN on graphs with many different labels.
		- Experience taught that this function, originally intended
		  to do a pre-sorting of label lists, was in fact seldom used.

		Two OPEN/CAESAR compliant compilers (CAESAR and BCG_OPEN)
		have been updated to remove the CAESAR_RANK_LABEL() function.
		The EXP.OPEN tool was left unchanged since it is to be replaced
		later by an entirely new version.

		The DECLARATOR tool was updated to detect the OPEN/CAESAR 
		compilers that still produce the CAESAR_RANK_LABEL() function.

		Following the removal of CAESAR_RANK_LABEL(), the function
		CAESAR_CREATE_EDGE_LIST() of the "casar_edge" library was
		modified: from now on, the cases 3 and 4 are identical to the
		cases 5 and 6, respectively. For cases 1 and 2, the documen-
		tation was improved, with explanations being made independent
		from LOTOS.

		The "upc" program was updated so as to detect and report the
		uses of CAESAR_RANK_LABEL() and CAESAR_CREATE_EDGE_LIST().

IMPROVEMENT
Number:		815
Date: 		Fri Oct  4 18:28:33 MEST 2002
Report:		Alain Le Guennec (IRISA, Rennes, France)
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_graph.h, man/*/caesar_graph.*, 
		doc/*/Garavel-92-a.*, bin.*/caesar, bin.*/libbcg_open.a,
		src/com/declarator.c, com/upc 

Nature:		The CAESAR_DUMP_LABEL() function was removed from OPEN/CAESAR's 
		"caesar_graph" API, for two reasons:
		- This function was prone to buffer overrun problems, since
		  it is impossible to predict, in the general case, the length
		  of the character string corresponding to a binary label;
		  thus, it was never possible to guarantee in advance that
		  the character string passed to CAESAR_DUMP_LABEL() would
		  be large enough to contain the character representation of
		  the binary label passed to CAESAR_DUMP_LABEL().
		- This function was not much used, especially in comparison
		  with CAESAR_STRING_LABEL(), which seemed to be preferred. 

		Two OPEN/CAESAR compliant compilers (CAESAR and BCG_OPEN)
		have been updated to remove the CAESAR_DUMP_LABEL() function.
		The EXP.OPEN tool was left unchanged since it is to be replaced
		later by an entirely new version.

		The DECLARATOR tool was updated to detect the OPEN/CAESAR 
		compilers that still produce the CAESAR_RANK_LABEL() function.

		The "upc" program was updated so as to detect and report any
		use of CAESAR_DUMP_LABEL().

IMPROVEMENT
Number:		816
Date: 		Mon Oct  7 12:14:14 MEST 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar

Nature:		The code generated by CAESAR (with option "-open") for the
		CAESAR_STRING_LABEL() function of OPEN/CAESAR's "caesar_graph"
		API was optimized in the particular case of labels that 
		consist of a gate only, without experiment offers (this
		encompasses the case of tau-transitions). For instance,
		on the alternating bit example given in "demos/demo_02" with
		65 different messages, the time needed by GENERATOR to
		produce the corresponding BCG file was reduced from 47.4
		down to 20.6 seconds. 

BUG FIX
Number:		817
Date: 		Thu Oct 17 16:12:33 MEST 2002
Report:		Bruno Ondet (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		src/open_caesar/declarator.c

Nature:		A minor memory leak problem was fixed in the DECLARATOR
		program, which checks if an OPEN/CAESAR compiler is compliant
		wrt the OPEN/CAESAR API.

IMPROVEMENT
Number:		818
Date: 		Fri Oct 18 13:21:58 MEST 2002
Report:		Frederic Tronel (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		com/svl, bin.*/svl_kernel, man/*/svl.*

Nature:		Two improvements have been brought to SVL:
		- The "-expand" command now comes with a "-indent" option that 
		  allows to set the number of blank characters used to indent
		  lines.
		- When the same reduction occurs right before and right after
		  a renaming, SVL eliminates the reduction occurring right
		  before. This optimizes "leaf reduction" in the presence of
		  renaming.

IMPROVEMENT
Number:		819
Date: 		Mon Oct 21 15:55:14 MEST 2002
Report:		Robert de Simone (INRIA/TICK, Sophia-Antipolis, France)
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/fc2open, bin.*/svl_kernel, man/*/fc2open.*, 
		man/*/declarator.*, man/*/executor.*, man/*/evaluator.*,
		man/*/exhibitor.*, man/*/generator.*, man/*/ocis.*,
		man/*/predictor.*, man/*/projector.*, man/*/reductor.*,
		man/*/simulator.*, man/*/terminator.*, man/*/xsimulator.*,
		src/eucalyptus/default/fc2open, 
		src/eucalyptus/default/fc2open2c,
		src/eucalyptus/fc2open.l, src/eucalyptus/eucalyptus.tcl,
		src/svl/standard	

Nature:		The FC2OPEN tool developed at Sophia-Antipolis, which allowed
		to map onto the OPEN/CAESAR "caesar_graph" API networks of
		communicating LTSs expressed in the "parallel" FC2 format,
		is no longer maintained (its source code was lost during the
		team reorganization consecutive to the creation of the Esterel
		Technology company). The documentation of CADP, the EUCALYPTUS
		graphical interface and the SVL language have been updated so
		as to remove any reference to FC2OPEN.

BUG FIX
Number:		820
Date: 		Mon Oct 21 17:08:37 MEST 2002
Report:		Frederic Lang (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/exp2fc2

Nature:		A bug was fixed, which caused EXP2FC2 to loop indefinitely in
		certain cases.

BUG FIX
Number:		821
Date: 		Tue Oct 22 20:00:09 MEST 2002
Report:		Dirk Keck (University of Stuttgart, Germany)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, bin.*/libBCG.a, bin.*/libBCG_IO.a

Nature:		When generating BCG graphs with very long labels (more than
		5,000 characters), CAESAR and BCG would make segmentation
		fault errors due to string buffer overflow. This problem was
		addressed and solved: from now on, the "bcg_write" API accepts
		label strings of unlimited length. Moreover, code has been
		added in the BCG library in order to avoid "memory leak"
		problems detected by Purify (the table of gates and the table
		of labels are now properly disallocated when no longer used). 

IMPROVEMENT
Number:		822
Date: 		Wed Oct 23 18:09:47 MEST 2002
Authors:	Hubert Garavel, Bruno Ondet, and Radu Mateescu (INRIA/VASY)
Files:		com/seq.open, bin.*/libseq_open.a, man/*/seq.open.*,
		man/*/declarator.*, man/*/executor.*, man/*/evaluator.*,
		man/*/exhibitor.*, man/*/generator.*, man/*/ocis.*,
		man/*/predictor.*, man/*/projector.*, man/*/reductor.*,
		man/*/simulator.*, man/*/terminator.*, man/*/xsimulator.*,
		src/eucalyptus/eucalyptus.tcl

Nature:		A new tool named SEQ.OPEN was added to CADP. SEQ.OPEN is an
		OPEN/CAESAR-compliant compiler that maps a ".seq" file (coded
		in CADP's SEQUENCE format) onto OPEN/CAESAR's "caesar_graph"
		API, thus allowing the application of all OPEN/CAESAR tools
		(e.g., OCIS, EVALUATOR...) to this ".seq" file.

		It is worth noticing that the functionality provided by
		SEQ.OPEN could also be obtained by first converting the ".seq"
		file into a ".bcg" file (using BCG_IO) and then applying the
		OPEN/CAESAR tool on the resulting ".bcg" file (by means of
		BCG_OPEN). However, SEQ.OPEN is more efficient (e.g., up to
		50 times faster on large ".seq" files) as it avoids the
		preliminary translation into ".bcg" and does not store the
		entire ".seq" file in main memory.
		
		A first prototype of SEQ.OPEN was developed in December 2000,
		in the framework of the FormalFame collaboration between BULL
		and VASY. This tool served to model-check mu-calculus formulas
		on traces generated by BULL multiprocessor systems. In 2001
		and 2002, SEQ.OPEN was entirely rewritten in order to support
		the complete SEQUENCE format (including comments and multiple
		sequences separated by the "[]" operator) and to implement the
		entire "caesar_graph" API. SEQ.OPEN was also made two times
		faster by removing an internal call to the C compiler, by 
		representing labels using file offsets, and by adding a
		hash-based cache to store labels and transitions. 

		The CADP manual pages have been updated to reflect the
		existence of SEQ.OPEN, and the EUCALYPTUS graphical user-
		interface was modified to handle ".seq" files using SEQ.OPEN
		(for on-the-fly processing) rather than ".bcg" files.

BUG FIX
Number:		823
Date: 		Thu Oct 24 20:32:32 MEST 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		src/eucalyptus/eucalyptus.tcl

Nature:		The EUCALYPTUS graphical user interface was improved:
		- The mechanism for checking the compatibility of ".xeucarc"
		  startup files contained a problem that was fixed.
		- The "Save preferences" feature could generate improper
		  version numbers; this was fixed.
		- All menu entries have been uniformized (single initial
		  capital letter, and "..." notion everywhere needed).

BUG FIX
Number:		824
Date:		Mon Oct 28 16:44:11 MET 2002
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel

Nature:		On Linux, parsing of renaming rules in SVL scripts could have
		side effects on other labels of the SVL script. This problem
		was solved.

IMPROVEMENT
Number:		825
Date: 		Mon Nov 4 15:38:46 MET 2002
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard	

Nature:		The SVL compiler was modified so as to use the new SEQ.OPEN
		tool (see item #822 above). Whenever an OPEN/CAESAR applica-
		tion program is launched on a ".seq" file, SVL will no longer
		invoke BCG_IO/BCG_OPEN, but will use SEQ.OPEN instead. A
		special variable $SEQ_OPEN_OPTIONS was added to SVL in order
		to contain particular options for SEQ.OPEN.

IMPROVEMENT
Number:		826
Date: 		Tue Nov 12 12:32:29 MET 2002
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/caesar.aldebaran, man/*/caesar.aldebaran.*

Nature:		The "caesar.aldebaran" shell-script was removed from CADP,
		since this shell-script was made useless and obsolete by the
		introduction of SVL in January 2001 (see item #729 above).

IMPROVEMENT
Number:		827
Date: 		Wed Nov 13 16:45:24 MET 2002
Report:		Bruno Ondet (INRIA/VASY)
Authors:	Hubert Garavel and Nicolas Descoubes (INRIA/VASY)
Files:		src/com/cadp_cc, src/com/windows/*

Nature:		The Windows version of CADP has been updated to cope with the
		evolution of the Cygwin software, which, in October 2002,
		moved from Gcc 2.95.3-10 to Gcc 3.2. Because of this compiler
		change, the BCG tools did not work with the latest version of
		Cygwin, and would fail with an error message of the form:
		   seek must be permitted for a bcg_file in BCG_OPEN_BINARY
		
		This problem was addressed by enhancing the "cadp_cc" shell
		script and the contents of the "src/com/windows" directory:
		a sub-directory named "bin.win32" was added; the existing file
		gcc-crtdll-specs was renamed into gcc-crtdll-specs-2.95.2-6;
		and a new file named "gcc-crtdll-specs-3.2" was added.

IMPROVEMENT
Number:		828
Date: 		Wed Nov 20 11:31:03 MET 2002
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/bcg_min

Nature:		During October-November 2002, many internal modifications
		have been brought to the BCG_MIN tool, in order to reduce the
		amount of memory required for graph minimization. The results
		can be summarized as follows:
		- Let m and n be the respective numbers of transitions and 
		  states in the graph to be minimized, and
		- Let b be the number of "blocks" in the minimized graph
		  (note that b <= n)

		- For "normal" LTSs and strong bisimulation:
		  the number of bytes needed by BCG_MIN was reduced from
  		  16m + 24n + 32b down to 16m + 16n + 24b

		- For "normal" LTSs and branching bisimulation:
		  the number of bytes needed by BCG_MIN was reduced from
		  16m + 24n + 32b down to max (16m + 16n + 24b, 16m + 20n) 

		- For probabilistic/stochastic LTSs and strong bisimulation:
		  the number of bytes needed by BCG_MIN was reduced from
  		  16m + 32n + 40b down to 16m + 24n + 28b

		- For probabilistic/stochastic LTSs and branching bisimulation:
		  the number of bytes needed by BCG_MIN was reduced from
		  16m + 32n + 40b down to max (16m + 24n + 28b, 16m + 28n) 

		Additional changes have been made to increase speed, which
		make BCG_MIN about 15% faster on some examples.

IMPROVEMENT
Number:		829
Date:		Thu Nov 21 16:21:40 MET 2002
Authors:	Hubert Garavel and Damien Bergamini (INRIA/VASY)
Files:		bin.*/bcg_io, bin.*/libBCG_IO.a, man/*/bcg_io.*,
                src/eucalyptus/eucalyptus.tcl

Nature:		A new option ``-etmcc'' has been added to BCG_IO in order to
		produce the ``.tra'' needed by the Erlangen Twente Markov Chain
		Checker (ETMCC). This enables the model-checking of performance
		properties expressed using the Continuous Stochastic Logic
		(CSL) against a labelled continuous-time Markov chain contained
		in a BCG graph.

                In the EUCALYPTUS graphical user-interface, this functionality
                is now accessible using the "Convert" item in contextual menus.

IMPROVEMENT
Number:		830
Date: 		Fri Dec 13 19:14:53 MET 2002
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		doc/*/Garavel-Lang-02.*

Nature:		A new publication describing a semantical model (NTIF) to be
		used in future versions of CADP was added.

BUG FIX
Number:		831
Date: 		Tue Jan 28 19:47:56 MET 2003
Report:		Ken Turner (Univ. of Stirling, Scotland, UK)
Author:		Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_which

Nature:		A bug (missing '$' before shell variable WHICH) has been 
		fixed.

IMPROVEMENT
Number:		832
Date: 		Tue Jan 28 20:39:46 MET 2003
Report:		Ken Turner (Univ. of Stirling, Scotland, UK)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/*, src/com/*, bin.*/bcg_*, bin/libBCG*.a, bin/libbcg*.a 

Nature:		Changes have been undertaken in order to allow the presence
		of white spaces in file names (mostly needed for Windows, as 
		in "/Program Files", "/Documents and Settings", etc.).
		This is a heavy task, since almost every CADP binary and
		shell scripts have to be patched. A first set of changes has
		been applied, but several tools remain to be patched.

IMPROVEMENT
Number:		833
Date: 		Thu Jan 30 18:42:49 MET 2003
Authors		Holger Hermanns (Univ. Sarrebruck, Germany), Christophe
		Joubert (INRIA/VASY), and Radu Mateescu (INRIA/VASY)
Files:		doc/*/Hermanns-Joubert-03.*, doc/*/Mateescu-03-a.*

Nature:		Two new papers have been added:
		- The first one presents the forthcoming tools BCG_STEADY,
		  BCG_TRANSIENT, and DETERMINATOR for performance evaluation.
		- The second one presents the CAESAR_SOLVE library for
		  efficient resolution of boolean equation systems.

IMPROVEMENT
Number:		834
Date: 		Fri Feb 14 18:20:11 MET 2003
Report:		Volker Braun (Univ. Dortmund, Germany), Lars-Ake Fredlung
		(SICS, Sweden), Jan Friso Groote (Tech. Univ. Eindhoven, The
		Netherlands), and Ken Turner (Univ. of Stirling, Scotland, UK)
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/rfl, INSTALLATION_3

Nature:		The RFL command was enhanced so as to support other remote
		access protocols than rsh/rcp. From now on, ssh/scp and
		Kerberos' krsh/kcp are also supported. Also, the explanations
		given in INSTALLATION_3 have been improved.

BUG FIX
Number:		835
Date: 		Tue Mar 11 11:04:06 MET 2003
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_hash.h, man/*/caesar_hash.*, doc/*/Garavel-92-a.*

Nature:		Hash functions CAESAR_1_HASH(), CAESAR_2_HASH(), and
		CAESAR_3_HASH() were improperly defined. The correct
		definition is
		   CAESAR_i_HASH (CAESAR_S, CAESAR_HASH_SIZE_STATE(),
		   CAESAR_MODULUS)
		instead of:
		   CAESAR_i_HASH (CAESAR_S, CAESAR_SIZE_STATE(),
		   CAESAR_MODULUS)

IMPROVEMENT
Number:		836
Date: 		Wed Mar 12 14:20:54 MET 2003
Authors:	Frederic Lang and Hubert Garavel (INRIA/VASY)
Files:		demos/*

Nature:		Demos 03, 04, 07, 08, 16, and 24 have been equipped with SVL
		scripts. The corresponding =READ_ME.txt files have been
		simplified and most of their contents was transferred to
		the newly created ".svl" files. Also, for most demo examples,
		the existing ".svl" file was renamed into "demo.svl".

IMPROVEMENT
Number:		837
Date: 		Wed Mar 12 16:12:51 MET 2003
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar.adt, incl/X_NATURAL.h

Nature:		The C code generated by CAESAR.ADT was made more portable:
		- on Unix, it now uses the native raise() function, instead
		  of defining raise() as an alias for kill (getpid()). The
		  same modification was made in file incl/X_NATURAL.h.
		- <stdlib.h> is now included to get the declaration of exit().

IMPROVEMENT
Number:		838
Date: 		Wed Mar 12 18:32:11 MET 2003
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		bin.*/caesar

Nature:		The state vector generated by CAESAR is now sorted: fields are
		permuted using a heuristic that tends to minimize unused 
		"padding" bits, which are introduced by the C compiler in
		order to align fields on byte/word boundaries properly. This
		permutation is similar to the one performed by CAESAR.ADT
		on fields of generated structure/union C types. It is 
		transparent to the end-user. On randomly generated state
		vectors, the average reduction in state vector size is 20%.
		However, on the database of real LOTOS examples used for
		regression testing of CAESAR, the gain appears to be more
		limited (1.3%).  

IMPROVEMENT
Number:		839
Date: 		Thu Mar 13 10:20:51 MET 2003
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard, man/*/svl.*, demos/demo_01/*.svl,
		demos/demo_02/*.svl, demos/demo_10/*.svl,
		demos/demo_11/*.svl, demos/demo_24/*.svl
		
Nature:		The choice of the default tool called by SVL to minimize an
		"explicit", "normal" LTS has been simplified:
		- If the reduction relation is strong or branching equivalence,
		  then SVL invokes BCG_MIN;
		- Otherwise, if the reduction relation is observational,
		  safety, or tau*.a, then SVL invokes ALDEBARAN.
		The SVL script files for demos 01, 02, 10, 11, and 24 have
		been simplified accordingly.

BUG FIX
Number:		840
Date: 		Mon Mar 17 13:17:56 MET 2003
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_edit

Nature:		The "cadp_edit" shell-script was modified to avoid a Windows-
		specific problem (files whose name starts with a "/" can not
		be opened using "wordpad.exe" or "write.exe"). Because of this
		problem, the "Help" button of INSTALLATOR would not open the
		help file (on Windows) and the "Edit .rhosts" button of
		INSTALLATOR would open an empty file (still on Windows).

IMPROVEMENT
Number:		841
Date: 		Mon Mar 17 15:53:32 MET 2003
Authors:	Damien Bergamini, Hubert Garavel, and Bruno Ondet (INRIA/VASY)
Files:		bin.*/libcaesar.a, incl/caesar_hash.h,
		man/*/caesar_hash.*, doc/*/Garavel-92-a.*

Nature:		New hash functions named CAESAR_4_HASH(), CAESAR_5_HASH(), 
		and CAESAR_6_HASH() --- together with their corresponding
		functions CAESAR_STATE_4_HASH(), CAESAR_STATE_5_HASH(), and
		CAESAR_STATE_6_HASH() --- have been added to OPEN/CAESAR's
		"caesar_hash" library.

BUG FIX
Number:		842
Date: 		Tue Mar 18 13:14:17 MET 2003
Report:		Frederic Tronel (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard, bin.*/svl_kernel

Nature:		When run with the "-debug" option, an SVL script performing 
		abstractions in a "for" loop could re-use a ".sync" file that 
		was automatically generated in a previous iteration, instead
		of re-generating it. This was incorrect if the interface file 
		changed between successive iterations of the loop. This
		problem was solved.

IMPROVEMENT
Number:		843
Date: 		Wed Apr  2 16:54:06 MEST 2003
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, incl/caesar_kernel.h

Nature:		The "caesar_kernel.h" file containing the EXEC/CAESAR API and
		the C code generated by CAESAR with option "-exec" have been
		modified:

		- From now on, base types (such as CAESAR_TYPE_BOOLEAN, 
		  CAESAR_TYPE_NATURAL, ...) are defined in "caesar_exec.h"
		  rather than in the C code generated by CAESAR with option
		  "-exec". This increases the compatibility between EXEC/
		  and OPEN/CAESAR.

		- The "caesar_kernel.h" API now provides a function (actually,
		  a macro-definition) CAESAR_KERNEL_CURRENT_TRANSITION() that
		  gives the number of the last (visible or tau, but not
		  epsilon) transition fired in the Petri net generated by
		  CAESAR. This new functionality can be useful for measuring
		  the coverage of the Petri net transitions during execution.
		  It is only available when the C code generated by CAESAR 
		  with option "-exec" is compiled with C compiler option 
		  "-DCAESAR_KERNEL_TRANSITION_INFORMATION" (or if a directive
		     #define CAESAR_KERNEL_TRANSITION_INFORMATION
		  occurs before including "caesar_kernel.h" and the C code
		  generated by CAESAR).

IMPROVEMENT
Number:		844
Date: 		Fri Apr  4 13:14:01 MEST 2003
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar

Nature:		The C code generated during the simulation phase of CAESAR
		was improved in two ways:

		- Each sequence of successive assignments of the form
		    P->CAESAR_PASS[I] |= A1;
		    ...
		    P->CAESAR_PASS[I] |= An;
		  was replaced with one unique assignment of the form:
		    P->CAESAR_PASS[I] |= (A1 | ... | An);
		  This reduction in the size of the generated C code applies
		  to all options ("-aldebaran", "-bcg", "-exec", or "-open")

		- For option "-exec", another optimization was added, which
		  avoids recomputing the table of positions and the list of
		  firable transitions when function CAESAR_KERNEL_NEXT() is
		  called twice (or more) on the same current state (for
		  details, see occurrences of variable CAESAR_SAME_STATE in
		  the generated C code). On the "ILU-medium" and "ILU-large"
		  benchmarks given to us by BULL, this optimization improves
		  by 17% the speed of the C code generated by CAESAR.

BUG FIX
Number:		845
Date: 		Tue Apr 15 15:22:56 MEST 2003
Report:		Yehong Xing (BULL)
Authors:	David Champelovier, Frederic Lang, and Hubert Garavel (INRIA/
		VASY)
Files:		bin.*/caesar, bin.*/caesar.adt, bin.*/caesar.indent

Nature:		Some error messages emitted by CAESAR and CAESAR.ADT were
		incorrect: when a syntactic error occurred in a LOTOS file
		included using the "library ... endlib" directive, the
		error message indicated an incorrect filename, e.g.,
		   [PRR:47] Warning : ``)'' is deleted
		instead of
		   [ERR:47] Warning : ``)'' is deleted
		if the syntactic error was at line 47 of file ERR.lib. This
		problem only occurred after the SYNTAX compiler generator
		attempted to repair the syntactic error using its global
		recovery scheme. This was due to a memory allocation error in
		the SYNTAX library, which was fixed.

BUG FIX
Number:		846
Date: 		Wed Apr 16 10:12:24 MEST 2003
Report:		Ghassan Chehaibar (BULL) and Radu Mateescu (INRIA/VASY)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.adt

Nature:		For some syntactically incorrect LOTOS programs, CAESAR and
		CAESAR.ADT could make a core dump. This problem was due to the
		syntax recovery feature of SYNTAX, which can insert "fictive"
		tokens where actual tokens are missing. The problem was solved. 

BUG FIX
Number:		847
Date: 		Thu Apr 17 14:45:47 MEST 2003
Report:		Bruno Vivien (INRIA/VASY)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		bin.*/caesar.adt

Nature:		For some semantically incorrect LOTOS programs containing a
		value expression enclosed between parentheses, e.g.,
            		eqns ofsort Bool
			true = ( 0 );
		CAESAR.ADT could make a core dump (while CAESAR would report
		the error correctly). This problem was solved.		

IMPROVEMENT
Number:		848
Date: 		Fri May  9 15:46:46 MEST 2003
Report:		Yehong Xing (BULL)
Author:		Hubert Garavel (INRIA/VASY)
Files:		lib/NATURAL.lib, lib/X_NATURAL.lib,
		demos/demo_12/maa.lotos, demos/demo_16/BRP.lib

Nature:		The Natural data type library included in CADP was enhanced.
		Previously, this library was a replacement to the standard
		NaturalNumber library provided by the LOTOS definition.
		The compatibility between the Natural and NaturalNumber
		libraries was improved in the sense that Natural is now an
		extension (or enrichment) of NaturalNumber: by importing the
		enhanced version of Natural, one also imports the standard
		NaturalNumber and BasicNaturalNumber libraries in a totally
		standard manner.

		A similar change was brought to the X_Natural library, which
		establishes a missing symmetry between Natural and X_Natural,
		the latter being nothing but the external implementation of
		the former. This is done by splitting the X_Natural library
		into three types (BasicNaturalNumber, NaturalNumber, and
		Natural).

		However, the latter change might create problems in existing
		LOTOS programs. To address this issue, you should first 
		locate all files with either ".lotos" or ".lib" extension
		that import the X_Natural library. This can be done by typing
		the following shell command:

		   find / -name "*.lotos" -o -name "*.lib" -exec \
		   grep -i '\<X_NATURAL\>' \{\} /dev/null \; | tee _xnatural

		Then, for each file F listed in "_xnatural", you should
		try to compile F using CAESAR.ADT (if F is a ".lib" file,
		then you should try to compile a ".lotos" file that imports
		F). If compilation succeeds, no change must be done. If
		compilation fails, then you should replace, in file F (and
		in all LOTOS files dependent on F) lines of the form
			type T is ... NaturalNumber ...
		by
			type T is ... Natural ...
		if type T makes use of the data type operations defined in
		type Natural and not in type NaturalNumber (these operations
		are the following: 1, 2, 3, ..., 9, -, div, mod, ==, <>, <,
		<=, >, >=, gcm, and scm). Given that LOTOS is not case-
		sensitive, the change may consist in replacing
			type T is ... NATURALNUMBER ...
		by
			type T is ... NATURAL ...

		The demos 12 and 16 of CADP have been updated accordingly.

BUG FIX
Number:		849
Date: 		Thu May 15 17:28:14 MEST 2003
Report:		Nicolas Descoubes (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		src/installator/bin.win32/blat.exe

Nature:		For recent versions of Cygwin, INSTALLATOR would fail to send
		the license file by e-mail, because the "x" (eXecute) bit was
		not set on the "blat.exe" file. This was fixed.

BUG FIX
Number:		850
Date: 		Wed May 21 20:05:14 MEST 2003
Report:		Marc Boyer (ENSEEIHT, Toulouse, France),
		Luka Hejtmanek (Masaryk University, Brno, Czech Republic),
		Jean-Christophe Pince (M3 Systems, Lavernose, France), and
		Maciej Szreter (IPIPAN, Warsaw, Poland)
Authors:	Hubert Garavel and Nicolas Descoubes (INRIA/VASY)
Files:		bin.iX86/*

Nature:		On recent versions of Linux (such as RedHat 9.0 and Mandrake
		9.1) the CADP binary tools would not execute properly (they
		would abort with a segmentation fault signal). This problem
		was solved by recompiling all CADP binaries.

IMPROVEMENT
Number:		851
Date: 		Mon May 26 13:13:52 MEST 2003
Author:		Radu Mateescu (INRIA/VASY)
Files:		doc/*/Mateescu-03-c.*, doc/=README.txt

Nature:		A new publication about the CAESAR_SOLVE library was added
		to the "doc" directory.

IMPROVEMENT
Number:		852
Date: 		Mon May 26 16:32:42 MEST 2003
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		demos/demo_12/maa.lotos, demos/demo_12/maa.f

Nature:		The REVERSE function of the MAA protocol is now implemented
		directly in C (in the "maa.f" file). Previously, it was
		specified in LOTOS. This simple change allows significant
		memory savings  (see the "=READ_ME.txt" file).

BUG FIX
Number:		853
Date:		Mon Jun  2 18:18:42 MEST 2003
Author:		Nicolas Descoubes (INRIA/VASY)
Files:		src/monitor/main.tcl

Nature:		A minor problem was fixed in the MONITOR tool: during the
		generation of a large BCG graph, if the MONITOR window was
		hidden by another window and then brought to the front ground,
		the MONITOR window could remain frozen (i.e., grey) during a
		few seconds until the window was refreshed. This problem is
		now solved.

IMPROVEMENT
Number:		854
Date: 		Thu Jun  5 14:48:55 MEST 2003
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar

Nature:		Further changes have been brought to CAESAR so as to generate
		faster C code for firing transition:

		- The CAESAR_PASS data structure becomes an array of 32-bits
		  words instead of an array of bytes. On the ILU-medium
		  example of BULL, this makes EXEC/CAESAR 5.8% faster.

		- When computing successor states, we delay as much as possible
		  the backup of the current state and the computation of the
		  successor marking, until it is certain that the transition
		  will be fireable. This avoids useless computations in the
		  case the transition would not be fireable, either because a
		  "when"-guard evaluates to false, or because the environment
		  refuses the rendezvous (the latter case only applies to
		  EXEC/CAESAR). On the ILU-medium example of BULL, this
		  improves speed by 24% on Linux and 36% on Solaris.

		- By considering, in EXEC/CAESAR mode, whether each variable
		  used as input in a rendezvous is a bit field or not, it
		  becomes possible to delay even more computations until it
		  is certain that the transition will be fireable. 

		All these changes (combined to those mentioned in item #844
		above) lead to significant speed improvement (42% for the 
		ILU-medium example on Solaris).

IMPROVEMENT
Number:		855
Date: 		Mon Jun 16 18:59:42 MEST 2003
Report:		Solofo Ramangalahy (BULL)
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, incl/caesar_kernel.h

Nature:		The EXEC/CAESAR API was enhanced with new primitives that
		provide a finer access to the underlying Petri net model
		(see the "caesar_kernel.h" file).

		A first group of primitives provides statistical information
		about the number of Petri net transitions and the repartition
		of these transitions as epsilon, visible, and tau transitions:
		   CAESAR_KERNEL_NB_TRANSITIONS()
		   CAESAR_KERNEL_NO_TRANSITION()
		   CAESAR_KERNEL_EPSILON_TRANSITION_MIN_NUMBER()
		   CAESAR_KERNEL_EPSILON_TRANSITION_MAX_NUMBER()
		   CAESAR_KERNEL_VISIBLE_TRANSITION_MIN_NUMBER()
		   CAESAR_KERNEL_VISIBLE_TRANSITION_MAX_NUMBER()
		   CAESAR_KERNEL_TAU_TRANSITION_MIN_NUMBER()
		   CAESAR_KERNEL_TAU_TRANSITION_MAX_NUMBER()

		A second group of primitives gives transition properties,
		namely:
		   CAESAR_KERNEL_CURRENT_TRANSITION()   (see item #843 above)
		   CAESAR_KERNEL_TRANSITION_GATE()
 		which return the number and gate, respectively, of the last
		transition fired. In particular, the former function allows,
		in association with primitives of the first group above, to
		measure the coverage by counting the number of visible
		transitions fired.

		A third group of primitives allows to introduce randomness in
		the firing of tau transitions. The user can now provide a 
		CAESAR_KERNEL_TAU() function (presumably based on random
		number generation) that is called every time a tau transition
		T is fireable: T will be fired iff CAESAR_KERNEL_TAU() returns
		true. By default, function CAESAR_KERNEL_TAU() always returns
		true, which expresses the default behaviour of EXEC/CAESAR,
		in which the first fireable tau transition is always selected. 

IMPROVEMENT
Number:		856
Date: 		Tue Jun 17 15:23:56 MEST 2003
Author:		Hubert Garavel (INRIA/VASY)
Files:		games

Nature:		Following a remark from one user, the "games" directory was
		removed from the CADP distribution.

IMPROVEMENT
Number:		857
Date: 		Thu Jun 19 16:55:48 MEST 2003
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar

Nature:		The C code generated by CAESAR (using "-exec" option) for
		function CAESAR_KERNEL_INIT() was improved to discover
		automatically (at run-time) if the user has modified the ".h"
		or ".t" file AFTER generating the ".c" file. This avoids the
		two following situations in which the ".c" file is no longer
		up to date after the modification of the ".h" or ".t" file:

		- Some sort S originally not defined as a bit field is now
		  a bit field; in such case, the ".c" file is incorrect, as
		  it takes the address ("&") of a bit field, and the user will
		  receive an error message while compiling the ".c" file.

		- Some sort S originally defined as a bit field is no longer
		  a bit field; in such case, the ".c" file is no longer
		  optimal and the user will receive a warning when the C code
		  executes; this warning indicates that the ".c" file must
		  be regenerated.

IMPROVEMENT
Number:		858
Date: 		Fri Jun 20 17:42:16 MEST 2003
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.adt

Nature:		Two limitations of CAESAR and CAESAR.ADT have been lifted:

		- The number of ".lib" files that can be included in a LOTOS
		  program was increased from 128 to 255.

		- The number of "significant" characters that are allowed in
		  C identifiers was increased from 32 to 48 (one should keep
		  in mind, however, that the ANSI C standard only permits 6
		  significant characters for external identifiers, because of
		  some obsolete link editors).

IMPROVEMENT
Number:		859
Date: 		Fri Jun 20 19:29:14 MEST 2003
Report:		Jack Abily (BULL)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar.adt

Nature:		The ".h" file produced by CAESAR.ADT has been enhanced so as
		to allow this file to be included in several C files (i.e.,
		for separate compilation purpose). This is done by using a
		new macro CAESAR_ADT_INTERFACE that, if defined, will skip
		variable definitions, function definitions, as well as the
		inclusion of the ".f" file (since the ".f" file is supposed to
		contain user-defined functions, which are not guaranteed to be
		properly bracketed by CAESAR_ADT_INTERFACE). 

		To use the ".h" file as a simple interface, one should either
		compile with the flag -DCAESAR_ADT_INTERFACE, or define the
		CAESAR_ADT_INTERFACE macro before including the ".h" file:
		   #define CAESAR_ADT_INTERFACE
		   #include "xxx.h"

BUG FIX
Number:		860
Date: 		Mon Jun 23 19:23:12 MEST 2003
Report:		Knut Conrad (Humboldt University, Berlin, Germany)
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar

Nature:		A bug was fixed in optimisation E2. This optimization was too
		"aggressive" and could in some rare cases (0.13% of our entire
		non-regression data base) remove some places that were needed
		to preserve the flow of data, leading to an incorrect LTS
		(actually, an LTS smaller than needed, in which some states
		were missing and some transitions were cut). The bug was fixed
		by strengthening the preconditions for application of
		optimization E2.

IMPROVEMENT
Number:		861
Date: 		Wed Jun 25 18:43:36 MEST 2003
Report:		Solofo Ramangalahy (BULL)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar

Nature:		The C code generated by CAESAR no longer declares useless
		variables (those named CAESAR_REGISTER_xxx). On the one hand,
		this avoids compiler warnings (e.g. when compiling with
		"gcc -Wall"). On the other hand, this reduces the stack size
		needed for firing transitions.

BUG FIX
Number:		862
Date: 		Thu Jul 10 15:09:48 MEST 2003
Report:		Nicolas Descoubes (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		man/*/caesar_*.*

Nature:		In the OPEN/CAESAR manuals, whatever their format (".html",
		".l", ".ps", or ".pdf"), there was an error in the text notes
		regarding the various functions named "CAESAR_CREATE_*".
		Instead of:
		   CAESAR_CREATE_TABLE_1 (CAESAR_T, ...)
		the correct text should have been:
		   CAESAR_CREATE_TABLE_1 (&CAESAR_T, ...)
		This error (caused by a mistake in the translator used by
		VASY to generate manual pages automatically) has been fixed.

BUG FIX
Number:		863
Date:		Mon Jul 21 17:48:21 MEST 2003
Report: 	Gregory Lestiennes (Universite Paris Sud, Orsay, France) and
		Ken Turner (Univ. of Stirling, Scotland, UK)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/tst, INSTALLATION_4,
		src/com/install_uncompress, src/com/cadp_postscript

Nature:		On recent Linux and Cygwin distributions, the "compress" and
		"uncompress" commands are no longer available by default. This
		caused a problem for several CADP tools that relied on the
		presence of "uncompress". For instance, INSTALLATOR would stop
		with the following error messages:
		   Extracting files from archive CADP_iX86_...tar.Z
		   Error while decompressing
		   .../install_uncompress: ...: uncompress: command not found
		These tools and the installation directives have been updated
		so as to use "gzip -d" instead of "uncompress" on iX86 and
		win32 architectures.

IMPROVEMENT
Number:		864
Date: 		Fri Sep 12 18:49:17 MEST 2003
Authors:	Hubert Garavel, Frederic Lang, Gordon Pace, and Radu Mateescu
		(INRIA/VASY)
Files:		doc/*/Garavel-03.*, doc/*/Pace-Lang-Mateescu-03.*

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

IMPROVEMENT
Number:		865
Date: 		Thu Sep 18 16:21:26 MEST 2003
Report:		Nicolas Descoubes (INRIA/VASY)
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/libbcg_info.a

Nature:		The BCG_INFO tool was modified in order to improve its 
		performance when handling very large graphs:

		- The algorithm used for option "-nondeterministic" was 
		  improved. From now on, this algorithm opens BCG files in
		  mode 0 instead of mode 1 (see "man bcg_read").

		- When BCG_INFO is called without option, it no longer 
		  displays unreachable states (since this would require to
		  open the BCG file in mode 1).

		As a consequence, BCG_INFO is now much faster. For instance,
		on the cwi_33949_165318 example of the VLTS benchmark suite
		(33 million states and 165 million transitions), BCG_INFO
		now answers in 5 minutes, compared to several hours (or even
		segmentation faults) with the previous version.

BUG FIX
Number:		866
Date: 		Thu Sep 18 17:46:13 MEST 2003
Report:		Ken Turner (University of Stirling, Scotland, UK)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar.adt

Nature:		LOTOS allows to define operation identifiers containing
		special characters such as "+", "-", "/", "--", etc.
		The C code generated by CAESAR.ADT for LOTOS identifiers
		containing the characters "\" and/or "%" was incorrect, as
		these characters have a special meaning in C (they provide an
		escape mechanism in C strings and printf() format strings).
		This bug was fixed.

IMPROVEMENT
Number:		867
Date: 		Tue Sep 23 18:57:40 MEST 2003
Authors:	Hubert Garavel and Damien Bergamini (INRIA/VASY)
Files:		com/bcg_info, bin.*/libbcg_info.a, man/*/bcg_info.*

Nature:		A new option "-order" was added to BCG_INFO. The purpose of
		this option is described in the "bcg_info" manual page.

BUG FIX
Number:		868
Date: 		Wed Oct  1 17:13:49 MEST 2003
Report:		Tomas Barros (INRIA/OASIS, Sophia-Antipolis, France)
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/evaluator.a

Nature:		A bug was fixed in the EVALUATOR model-checker, which generated
		an incorrect error message when the tool was invoked on a BCG
		graph whose initial state number was different from zero.

IMPROVEMENT
Number:		869
Date: 		Fri Oct 3 13:04:09 MEST 2003
Authors		Frederic Tronel, Frederic Lang, Hubert Garavel and David
		Champelovier (INRIA/VASY)
Files:		bin.*/bcg_graph, man/*/bcg_graph.*

Nature:		A new tool, named BCG_GRAPH, was added to the CADP package.
		This tool generates several useful kinds of automata such as
		bugs, FIFO queus, chaos automata.

IMPROVEMENT
Number:		870
Date: 		Mon Oct  6 12:53:33 MEST 2003
Report:		Hubert Garavel (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard, man/*/svl.*

Nature:		The syntax of SVL has been extended in two ways:

		- The "reduction" operator of SVL and the meta-operators
		  related to it have been enhanced with new attributes for
		  dealing with the stochastic and probabilistic bisimulations
		  implemented in BCG_MIN; one can now use the following SVL
		  clauses:
		 	strong stochastic reduction ...
		 	branching stochastic reduction ...
		 	strong probabilistic reduction ...
		 	branching probabilistic reduction ...

		- New SVL behavioural operators ("bag", "chaos", "fifo", ...)
		  have been introduced to take advantage of the facilities
		  provided by the new BCG_GRAPH tool.

IMPROVEMENT
Number:		871
Date: 		Thu Oct 16 16:14:07 MES 2003
Report:		Radu Mateescu (INRIA/VASY)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		bin.*/libbcg_open.a

Nature:		The implementation provided by BCG_OPEN for the two functions
		CAESAR_PRINT_LABEL() and CAESAR_STRING_LABEL() defined in the
		OPEN/CAESAR API has been made faster. For instance, on the
		alternating bit protocol of demo_02 with 50 messages, the
		following command:
		    bcg_open bitalt_protocol.bcg generator result.bcg
		is now 4 times faster.		

IMPROVEMENT
Number:		872
Date: 		Thu Oct 16 17:25:46 MEST 2003
Report:		Nicolas Descoubes (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/libBCG.a, man/*/bcg.*

Nature:		The default values for the compression parameters of the BCG
		format (i.e., the default values for the three BCG general
		options "register", "-short", and "-medium", which are grouped
		altogether by the "-size" option) have been adapted. The
		previous default values (2, 2, 4) defined in 1993 were no
		longer optimal for the larger BCG models that can be generated
		in 2003. The new default values have been set to (4, 1, 3)
		after exhaustive experiments done on the VLTS benchmark suite.

		In practice, for the various BCG graphs that can be generated
		from the CADP demos, one observes an average reduction of 11%
		in the size of BCG files. For large graphs (more than 10^5
		transitions), the average reduction is 11.9%. For small graphs
		(less than 10^5 reduction), the file sizes slightly increases
		(by 3,9%), but this is negligible as the files are small.

IMPROVEMENT
Number:		873
Date: 		Tue Oct 21 14:54:03 MEST 2003
Report:		Hubert Garavel (INRIA/VASY)
Author:		Nicolas Descoubes (INRIA/VASY)
Files:		bin.*/libbcg_draw.a

Nature:		The PostScript files generated by BCG_DRAW have been enhanced
		with a directive:
		   %%Page: 1 1
		so as to avoid the following warning from the Gsview software
		running on Windows:
		   DSC error
		   %%Pages: doesn't match the number of %%Page

IMPROVEMENT
Number:		874
Date: 		Thu Oct 23 18:05:41 MEST 2003
Report:		Marius Minea (Institute e-Austria, Timisoara, Romania)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/tst

Nature:		The "tst" command (self-testing command of CADP) was enhanced
		in several ways:

		- "tst" now displays the version number of the "gcc" compiler,
		  and the version number of the "glibc" library (on Linux).

		- "tst" now detects the case where $CADP is not set to an
		  absolute pathname (i.e., does not start with a "/").

		- "tst" now detects the case where $CADP is set to a Windows
		  pathname (e.g., "C:\...").

		- "tst" now detects the case where $CADP is set to a pathname
		  ending with a trailing "/", which causes "tst" to emit
		  incorrect warning messages of the form:

		     *** The tool ``...'' is not searched in ``$CADP/bin.iX86''
		     but in ``/.../bin.iX86'' instead
		     You might have two versions of CADP installed
		     ==> Reorder your ``$PATH'' variable to have ...
		         and remove all obsolete versions of CADP, if any

		  as the "tst" script is unable to figure out that "//" and 
		  "/" are in fact equivalent.

IMPROVEMENT
Number:		875
Date: 		Fri Oct 24 12:55:34 MEST 2003
Report:		Alban Catry, Radu Mateescu and Nicolas Descoubes (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		doc/*/Garavel-92-a.*, man/*/caesar_*.*

Nature:		The OPEN/CAESAR manual pages (especially the "caesar_graph",
		"caesar_edge", and "caesar_table_1" pages) have been improved.
		In addition to English language corrections, several notes
		have been added. In particular, it is now said explicitly that
		functions CAESAR_COPY_STATE(), CAESAR_COPY_LABEL(), and
		CAESAR_START_STATE() do not allocate memory for their second
		parameter.

IMPROVEMENT
Number:		876
Date: 		Mon Oct 27 17:08:09 MET 2003
Authors:	Hubert Garavel and Damien Bergamini (INRIA/VASY)
Files:		bin.*/caesar

Nature:		The CAESAR compiler was modified so as to minimize the memory
		size used by transition labels under their binary form (this
		size is the result returned by the CAESAR_SIZE_LABEL() function
		of the OPEN/CAESAR API). Three technical approaches have been
		implemented:

		- CAESAR now uses bitfield information when generating the
		  definition of the binary label type.

		- CAESAR now permutes the fields of the binary label type
		  (i.e., the fields corresponding to LOTOS experiment offers)
		  in the same way as it permutes the state vector fields.

		- The field containing the Petri net transition number inside
		  the binary label type was made more compact by introducing a
		  dedicated number type CAESAR_TYPE_PACKED_TRANSITION_NUMBER.

		In practice, on the entire non-regression testing base of
		CADP, these changes reduced the size of binary labels by 45%.

IMPROVEMENT
Number:		877
Date: 		Wed Oct 29 10:59:58 MET 2003
Authors:	Hubert Garavel and Damien Bergamini (INRIA/VASY)
Files:		bin.*/caesar

Nature:		The implementation generated by CAESAR (with option "-open")
		for the CAESAR_HASH_LABEL_SIZE() function of the OPEN/CAESAR
		API was made more accurate. In many cases, this function now
		returns a greater value than previously. This, combined with
		the average label size reduction (see item #876 above),
		improves the quality of hashing on binary labels by increasing
		the relative percentage of binary label representation on
		which user-defined hashing functions can operate.
 
		Reminder: before any LTS processing, one should not forget to
		invoke the CAESAR_INIT_GRAPH() function of the OPEN/CAESAR
		API. The former versions of CAESAR used to generate an empty
		definition for CAESAR_INIT_GRAPH(), so that omitting to invoke
		this function was harmless when using "caesar.open" (but not
		"bcg.open", "seq.open", etc.). At present, the definition
		generated by CAESAR for CAESAR_INIT_GRAPH() is no longer empty
		and cannot be ommitted, otherwise CAESAR_HASH_LABEL_SIZE()
		will return an incorrect value.

IMPROVEMENT
Number:		878
Date: 		Mon Nov 17 15:17:12 MET 2003
Report:		Katsumi Wasaki (Shinshu University, Nagano, Japan), and
		Carlos Eduardo Araujo Vieira (University of Ceara, Brazil)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_cc, src/com/windows/gcc-crtdll-specs-3.3

Nature:		The win32 version of CADP was adapted to support the Gcc 3.3
		compiler included in the latest versions of Cygwin. This
		suppresses various error messages of the form:
		   gcc: installation problem, cannot exec `cpp0': No such
		   file or directory
		   <command line>:20:13: warning: "system" re-asserted
		   <command line>:22:1: warning: "__STDC_HOSTED__" redefined
		   <command line>:1:1: warning: "__STDC__" redefined
		   <command line>:23:9: warning: "cpu" re-asserted
		   <command line>:24:13: warning: "machine" re-asserted
		   /lib/mingw/crt1.o(...):crt1.c: undefined reference to 
		   `__p__fmode'
		   etc.

IMPROVEMENT
Number:		879
Date: 		Mon Nov 17 15:57:10 MET 2003
Report:		Ken Turner (University of Stirling, Scotland, UK)
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/tst, src/com/cadp_which, cadp_cygwin.com

Nature:		The "tst" command was enhanced to compare, on win32, both
		files "/bin/sh.exe" and "/bin/bash.exe", and if different,
		to warn the user that the shell-script "cadp_cygwin.com"
		should be executed.

		The "cadp_which" command was modified on win32 so as to
		function properly even when the "cadp_cygwin.com" shell-
		script has not been applied properly. 

		The "cadp_cygwin.com" shell-script was modified in several
		ways:
		- Obsolete features related to old features of Cygwin have
		  been removed.
		- Version 1.5.5 of Cygwin is now supported.
		- It is now possible to execute "cadp_cygwin.com" several
		  times, e.g., after each upgrade of Cygwin. 

IMPROVEMENT
Number:		880
Date:		Tue Nov 18 10:20:32 MET 2003
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar

Nature:		In the C code generated by CAESAR with "-open" option, the
		array CAESAR_UNIQUE_GATE[] was removed and replaced with a
		new array named CAESAR_UNIQUE_GATE_AND_PROFILE[]. Then,
		the C code generated for functions CAESAR_COMPARE_LABEL()
		and CAESAR_HASH_LABEL() has been revised, with two main
		advantages:

		- The CAESAR_COMPARE_LABEL() function becomes faster.

		- The CAESAR_HASH_LABEL() function becomes faster and gives
		  a better hash dispersion: the previous hash function only
		  considered the gate and the profile of a label, thus giving
		  the same hash value for labels with the same gate and 
		  profile, but different experiment offers; the new hash
		  function reduces the risk of collisions by hashing also on
		  all experiment offers of canonical type (i.e., of any type
		  but a pointer type).

		In the alternating bit protocol of demo_02 with 100 messages,
		the number of hash collisions for all reachable labels was
		reduced from 101 to 0.

		In the bounded retransmission protocol of demo_16 with 10
		messages, the number of hash collisions for all reachable
		labels was reduced from 48 to 10 (only conflicts for non-
		canonical sorts remain).	

		On the entire list of full-LOTOS programs used for regression
		testing of CAESAR, the average number of hash collisions for
		labels was divided by 3.9 on Solaris and divided by 2.5 on
		Linux.

IMPROVEMENT
Number:		881
Date: 		Thu Nov 20 09:35:16 MET 2003
Report:		Katsumi Wasaki (Shinshu University, Nagano, Japan)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/tst

Nature:		The "tst" command was improved in two ways:

		- On Windows, it now detects and report the case where Cygwin
		  is not installed in C:\ but in a sub-directory, such as
		  C:\cygwin.

		- On Linux, it now detects and reports obsolete versions of
		  the Glibc library (i.e., versions strictly older than Glibc
		  2.3) and warns about potential 'undefined symbols' problems.

IMPROVEMENT
Number:		882
Date: 		Thu Nov 20 12:33:53 MET 2003
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.adt

Nature:		In the front-end part of the CAESAR and CAESAR.ADT compilers
		for LOTOS specifications, the static semantics analysis
		phase has changed slightly. From now on, binding of process 
		identifiers is done before binding of gate identifiers. For
		the user, the effect is the same, except for incorrect LOTOS
		specifications that contain both erroneous process and gate
		identifiers; for such specifications, CAESAR and CAESAR.ADT
		will stop just after displaying error messages related to
		processes (previously, error messages related to gates were
		displayed first).

IMPROVEMENT
Number:		883
Date: 		Mon Nov 24 17:09:52 MET 2003
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_windows, com/tst

Nature:		A new shell-script named "cadp_windows" was added. This shell-
		script is used to adapt the Windows distribution of CADP.
		Specifically, "cadp_windows":

		- removes symbolic links in the $CADP directory (symbolic
		  links are a Cygwin-specific extension and are not handled
		  by pure Win32 applications, such as CADP binary programs),

		- modifies text files by expanding tabulations and converts
		  "\n" into "\r\n", so that text files can be read by simple
		  Windows editors such as Notepad. 

		The "tst" command has also been adapted. On Windows, it now
		detects the existence of symbolic links in the $CADP directory
		and, in such case, suggests to execute the "cadp_windows"
		shell-script.

IMPROVEMENT
Number:		884
Date: 		Tue Nov 25 14:38:08 MET 2003
Authors:	Hubert Garavel and Damien Bergamini (INRIA/VASY)
Files:		bin.*/libcaesar.a

Nature:		The CAESAR_PRINT_TABLE_1() function of the OPEN/CAESAR library
		now displays more accurate statistics for hash collision lists.

IMPROVEMENT
Number:		885
Date: 		Tue Nov 25 16:31:47 MET 2003
Author:		Radu Mateescu (INRIA/VASY)
Files:		src/xtl/ctl.mcl

Nature:		A new library file for EVALUATOR (description of the CTL
		logic in modal mu-calculus) was added.

BUG FIX
Number:		886
Date: 		Wed Nov 26 11:27:32 MET 2003
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/bcg_edit

Nature:		The BCG_EDIT tool, when given the "-version" option, would
		fail with the following message:
		    grep: can't open /incl/bcg_version.h
		This problem was solved.

BUG FIX
Number:		887
Date: 		Mon Dec  1 12:11:47 MET 2003
Report:		Frederic Lang (INRIA/VASY)
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		bin.*/libBCG_IO.a

Nature:		The Linux version of the BCG_IO tool would generate incorrect
		Fc2 files. Precisely, the command:
		   bcg_io file.bcg file.fc2
		would generate in the Fc2 file an extra number at the end of
		certain labels, which was then rejected by Fc2 tools such as
		Fc2Link. This bug, which seemed to occur only on Linux, was
		fixed.

IMPROVEMENT
Number:		888
Date: 		Mon Dec  1 17:11:03 MET 2003
Authors:	Frederic Tronel, Frederic Lang and Hubert Garavel (INRIA/VASY)
Files:		doc/*/Tronel-Lang-Garavel-03.*, doc/*/Mateescu-03-b.*

Nature:		Two new papers have been added in the "doc" directory: the
		former deals with the compositional verification using CADP
		of the ScalAgent deployment protocol for software components;
		the latter is about action-based temporal logics for
		asynchronous systems.

BUG FIX
Number:		889
Date: 		Tue Dec  2 13:10:55 MET 2003
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/bcg_edit, src/com/bcg_edit/bcg_edit.tcl

Nature:		In the "Help" menu of the BCG_EDIT tool, the "BCG Postscript
		Format" entry did not work correctly when selected:
		- On Solaris, nothing happened,
		- On Windows, a dialog box would open with the message
		     Error: "/Program: not found"
		These problems were fixed.

BUG FIX
Number:		890
Date: 		Wed Dec  3 15:31:21 MEST 2003
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2fc2

Nature:		A bug was fixed in EXP2FC2, which did not translate the "||"
		operator into the Fc2 format correctly. The reason was that
		EXP2FC2 required synchronization only on labels present on
		both sides of the "||" operator (whereas it should synchronize
		on all labels instead).

BUG FIX
Number:		891
Date: 		Thu Dec 11 13:05:45 MET 2003
Report:		Nicolas Descoubes (INRIA/VASY) and Solofo Ramangalahy (BULL)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.adt, com/cadp_cc

Nature:		On Linux and Windows systems with Gcc version 3.*, the CAESAR
		and CAESAR.ADT compilers performed unecessary recompilations.
		This problem was fixed.

IMPROVEMENT
Number:		892
Date: 		Fri Dec 12 13:51:28 MET 2003
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.adt

Nature:		CAESAR.ADT was enhanced with a sort finiteness analysis 
		(fixpoint computation, 250 lines of C code) that classes
		LOTOS sorts into three categories:
		- sorts whose value domain is finite, 
		- sorts whose value domain is infinite but bounded by a 
		  user-defined iterator, which only enumerates a restricted,
		  finite subset of values,
		- sorts whose value domain is infinite and not bounded by
		  an iterator.
		For each sort of the third category, a comment was added in
		the C code generated by CAESAR.ADT so as to remind the user
		that it is possible to define an iterator manually for this
		sort.

		Then, CAESAR was modified to take advantage of the sort
		finiteness analysis performed by CAESAR.ADT: CAESAR will now
		emit a warning if the generated simulator program contains
		an iteration over the domain of some infinite sort S that
		lacks an iterator in the ".h" file. This warning is emitted
		before compiling and executing the simulator program; it has
		the following form:

		   #185 warning during simulation:
		        foreseeable impossibility to enumerate the domain of
		        some LOTOS sort
		        graph exploration is likely to abort because no
		        iterator exists to enumerate the domain of sort S

		Later, when executing the simulator program after it is
		compiled, if the iteration over the domain of S is actually
		reached, the usual error messages will be displayed:

		   #226 theoretical limitation :
     		        domain of an infinite (or complex) sort cannot be
		        enumerated; no available iterator for sort S
		   #203 system error during simulation:
     		        termination on SOFTWARE_TERMINATION signal (files
		        completed)
		        quit

IMPROVEMENT
Number:		893
Date: 		Tue Dec 16 11:17:27 MET 2003
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_standard.h, bin.*/libcaesar.a, 
		man/*/caesar_standard.*, src/open_caesar/generator.c,
		src/open_caesar/reductor.c, src/open_caesar/executor.c

Nature:		A new function named CAESAR_SIGNALS() was added to the
		"caesar_standard" library of OPEN/CAESAR. This function
		allowed to simplify and shorten the source code of the
		GENERATOR, REDUCTOR, and EXECUTOR tools.

IMPROVEMENT
Number:		894
Date: 		Fri Dec 19 15:57:30 MET 2003
Report:		Matts Kindahl (Uppsala University, Sweden)
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, man/*/caesar_graph.*

Nature:		The C code fragment generated by CAESAR for producing the
		character string corresponding to a label was improved.

		This C code fragment is used by the "-bcg" option of CAESAR
		and by the "-open" option of CAESAR (in order to implement the 
		CAESAR_STRING_LABEL() function of OPEN/CAESAR's "caesar_graph"
		interface). It is not used by the "-aldebaran" and "-exec"
		options of CAESAR. 

		This C code fragment, which could be slow, was made faster by
		implementing a hash-based cache table, which avoids useless
		recomputations.

		In the alternating bit protocol of demo_02 with 100 messages,
		CAESAR with "-bcg" option was made 32% faster after this
		change. In the bounded retransmission protocol of demo_16
		with 10 messages, CAESAR was made 6.5% faster. In the worst
		case where all labels are different, a small penalty (-4.2%)
		can be observed though.

		Similarly, the CAESAR_STRING_LABEL() function, which is used
		intensively in tools such as GENERATOR and EVALUATOR, was
		made faster (26% faster for GENERATOR and 2-4 times faster
		for EVALUATOR). In the worst case, a small penalty (-2%) is
		also observed.

		In the manual page for "caesar_graph", the implementation
		note that warned about the potential inefficiency of function
		CAESAR_PRINT_LABEL() was removed.

IMPROVEMENT
Number:		895
Date: 		Tue Dec 23 17:17:12 MET 2003
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		bin.*/libcaesar.a, man/*/caesar_rename_1.*,
		doc/*/Garavel-92-a.*

Nature:		The documentation of the CAESAR_APPLY_RENAME_1() function of
		the "caesar_rename_1" library was improved: it now specifies
		that it is forbidden to call CAESAR_APPLY_RENAME_1() by giving
		to its second argument the value returned by a former call to
		CAESAR_APPLY_RENAME_1(), as in the following example:
		CAESAR_APPLY_RENAME_1 (..., CAESAR_APPLY_RENAME_1 (..., ...))
		A test was added in the code of CAESAR_APPLY_RENAME_1() so
		as to detect and reject this situation.

IMPROVEMENT
Number:		896
Date: 		Wed Feb 10 16:21:53 MET 2004
Report:		Hubert Garavel (INRIA/VASY)
Author:		David Champelovier (INRIA/VASY)
Files:		bin.*/mcl_expand, demos/demo_02/*.mcl, demos/demo_29/*.mcl

Nature:		The formula language of the EVALUATOR 3 model-checker was
		enhanced with a concatenation operator (noted `#') operating
		on label strings and regular expressions. Precisely, the
		syntax of strings was extended with the following rule:
 
			<string> ::= ...
			          |  <string1> # <string2>

		and the syntax of regular expressions was extended with the
		three following rules:

			<regexp> ::= ...
			          |  <regexp1> # <regexp2>
			          |  <string1> # <regexp2>
				  |  <regexp1> # <string2>

		This syntactic extension, combined with the use of the 
		MCL_EXPAND preprocessor, allows to define parameterized
		action predicates.

		For instance, the "macros.mcl" file of demo_02 now defines
		two parameterized macros GET (N) and PUT (N) instead of
		several macros GET_0, GET_1, ..., PUT_0, PUT_1, etc. 

		Similarly, the "macros.mcl" of demo_29 was simplified; it
		has now only 183 lines instead of 783 lines.

IMPROVEMENT
Number:		897
Date: 		Mon Feb 16 14:58:29 MET 2004
Authors:	Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files:		doc/Garavel-Mateescu-04, doc/=READ_ME.txt, doc/biblio.bib

Nature:		A new publication entitled "SEQ.OPEN: A Tool for Efficient
		Trace-Based Verification" was added to the CADP release.
		This paper describes SEQ.OPEN, an OPEN/CAESAR-compliant
		compiler for the SEQUENCE format.

IMPROVEMENT
Number:		898
Date: 		Mon Feb 16 15:04:24 MET 2004
Authors:	Gregory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel,
		and Radu Mateescu (INRIA)
Files:		doc/Batt-Bergamini-deJong-et-al-04, doc/=READ_ME.txt,
		doc/biblio.bib

Nature:		A new publication entitled "Model Checking Genetic Regulatory
		Networks using GNA and CADP" was added to the CADP release.
		This paper describes a connection between the GNA (Genetic
		Network Analyzer) tool and CADP, which enables the analysis of
		genetic regulatory networks using standard equivalence checking
		and model checking techniques.

BUG FIX
Number:		899
Date: 		Wed Feb 25 15:03:06 MET 2004
Report:		Wendelin Serwe (INRIA/VASY)
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		src/bcg_edit/bcg_edit.tcl

Nature:		Two bugs were fixed in the BCG_EDIT tool:
		- In some cases, refresh would not be done and the BCG_EDIT
		  window could remain grey.
		- Modifying the Postscript Options (e.g., the radius value)
		  would have no effect.

IMPROVEMENT
Number:		900
Date: 		Wed Feb 25 17:50:28 MET 2004
Report:		Jack Abily and Solofo Ramangalahy (BULL)
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_kernel.h, bin.*/caesar

Nature:		The "caesar_kernel.h" file defining the EXEC/CAESAR API was
		enhanced with new functionalities (some of which borrowed
		from the OPEN/CAESAR API).

		Several new primitives have been added: CAESAR_CREATE(),
		CAESAR_DELETE(), CAESAR_CREATE_STATE(), CAESAR_DELETE_STATE(),
		CAESAR_SIZE_STATE(), and CAESAR_ALIGNMENT_STATE().

		Then, two new primitives, CAESAR_KERNEL_SAVE_STATE() and
		CAESAR_KERNEL_RESTORE_STATE() have been added to save and 
		restore the current simulation state to/from memory. These
		functions are useful, e.g., to hardware/software cosimulation.
		The following code fragment shows how these functions can be
		used:

		   main ()
		   {
		   CAESAR_TYPE_STATE CAESAR_S;

		   CAESAR_KERNEL_INIT (NULL);
		   CAESAR_CREATE_STATE (&CAESAR_S);
		   ...
		   /* saving the current simulation state into CAESAR_S */
		   CAESAR_KERNEL_SAVE_STATE (CAESAR_S);
		   ...
		   /* advancing the simulation by one step */
		   CAESAR_KERNEL_NEXT ();
		   ...
		   /* backtracking to saved state CAESAR_S */
		   CAESAR_KERNEL_RESTORE_STATE (CAESAR_S);
		   ...
		   CAESAR_DELETE_STATE (&CAESAR_S);
		   }

		The C code generated by CAESAR with "-exec" option was
		modified so as to implement the new primitives added to
		the EXEC/CAESAR API.

BUG FIX
Number:		901
Date: 		Tue Mar  9 16:47:14 MET 2004
Report:		Andrea Martins Araujo (Univ. Federal do Rio de Janeiro, Brasil)
Author:		Damien Bergamini (INRIA/VASY)
Files:		src/bcg_edit/bcg_edit.tcl

Nature:		If a label of BCG GRAPH would contain braces, e.g., as in the
		following label "GET !1 !true !{}", BCG_EDIT would abort with
		the following error message:
		   Error in startup script: list element in braces 
		   followed by "\))" instead of space
		   ...
		This problem was solved.

BUG FIX
Number:		902
Date: 		Mon Apr 19 21:39:27 MEST 2004
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/libseqopen.a

Nature:		Two bugs have been fixed in the SEQ.OPEN tool:
		- On Windows, ``.seq'' files with lines terminated with CR-LF
		  ("\r\n") instead of LF ("\n") were rejected by SEQ.OPEN,
		  unless the "-seqno" option was selected.
		- The value given to the CAESAR_HINT_HASH_SIZE_LABEL variable
		  is now equal to 0, and not to sizeof (CAESAR_BODY_LABEL).

IMPROVEMENT
Number:		903
Date: 		Fri Apr 23 10:50:16 MEST 2004
Report:		Axel Belinfante (University of Twente, The Netherlands),
		Olivier Bonaventure (Universite de Liege, Belgium),
		Francois Germeau (Universite de Liege, Belgium),
		Michel Jankowski (Universite de Liege, Belgium),
		Charles Pecheur (INRIA/VASY),
		Meurig Sage (University of Glasgow, UK),
		Frederic Tronel (INRIA, VASY), and many others
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar.adt, bin.*/caesar, bin.*/caesar.indent,
		lib/*.lib, incl/X_*.h,
		demos/demo_02/BITALT.t, demos/demo_03/DATALINK.t,
		demos/demo_05/list.lotos, demos/demo_05/user.c,
		demos/demo_07/overtaking.lotos,
		demos/demo_08/REL_REL_FIFO.lib,
		demos/demo_09/INRES_PROTOCOL.lib
		demos/demo_09/INRES_SERVICE.lib, demos/demo_10/BITALT.t
		demos/demo_11/rel_rel.t, demos/demo_11/REL_REL_FIFO.lib,
		demos/demo_16/BRP.t, demos/demo_16/brp_service.t,
		demos/demo_16/brp_protocol.t, demos/demo_18/transit_node.t,
		demos/demo_20/REL_REL_FIFO.lib, demos/demo_20/rel_rel.t,
		demos/demo_23/*.f, demos/demo_26/*.f, demos/demo_31/TYPES.lib,
		demos/demo_31/SCSI_A.f, demos/demo_31/SCSI_A.t, 
		demos/demo_31/SCSI_B.f, demos/demo_31/SCSI_C.f

Nature:		The CAESAR.ADT and CAESAR tools have been modified so as to
		address two issues:

		a) The former versions of CAESAR.ADT could generate iterators
		   only for "simple" LOTOS sorts, namely natural numbers,
		   enumerated types (including singleton types), and tuple
		   types (see $CADP/doc/pdf/Garavel-89-c.pdf for details).
		   However, more "complex" types would not be supported, even
		   if their domain of values was finite, such as the following
		   LOTOS sort T with two constructors:
		      A (*! constructor *) : BOOL -> T
                      B (*! constructor *) : BOOL, BOOL -> T
		   For those types, CAESAR.ADT would generate an error message
		   about infinite or too complex types; this error message
		   would appear as soon as CAESAR would try to enumerate the
		   domains of these types. A workaround was to provide, for
		   these types, hand-written iterators defined in the ".t"
		   and/or ".f" files.

		b) In the particular case of "tuples of tuples" types, the
		   iterators generated by CAESAR.ADT for those types would not
		   work properly: the C compiler would reject them because of
		   name clashes between variables declared in iterators.

		These two issues are now solved by the recent version 5.2 of
		CAESAR.ADT, which can now generate iterators for all LOTOS
		sorts with a finite domain of values. In particular, for the
		previously so-called "complex" sorts, it is no longer needed
		to provide ".t" and/or ".f" files containing hand-written C
		code for enumerating the domain of these sorts.

		However, this improvement requires important changes in the
		definition of the iterators generated by CAESAR.ADT. One must
		now distinguish between two different forms of iterators:

		- "Old-style" iterators are described in the [Garavel-89-c]
		  paper. In a LOTOS specification, an old-style iterator is 
		  specified using a special comment of the form:
		     sort S (*! implementedby S ...
		                enumeratedby ENUM_S ... *)
		  It consists of one single C macro-definition ENUM_S to be
		  used as follows for enumerating all values of sort S:
		     S LOOP_VARIABLE;
		     {
		        ENUM_S (LOOP_VARIABLE) {
		           ... loop body parameterized by LOOP_VARIABLE
		        }
		     }
		  For instance, the old-style iterator for enumerating the
		  integer range 0..15 has the form:
		     #define ENUM(X) for ((X) = 0; X <= 15; ++(X))

		- "New-style" iterators are introduced with CAESAR.ADT 5.2.
		  In a LOTOS specification, a new-style iterator is specified
		  using a special comment of the form:
		     sort S (*! implementedby S ...
		                iteratedby FIRST_S and NEXT_S ... *)
		  It consists of two C macro-definitions FIRST_S and NEXT_S
		  with the following profiles
		     FIRST_S() : returns a constant value of sort S
		     NEXT_S(X) : tries to advance X to the next value of S
			         and returns a non-zero value iff there exists
		                 such a value
		  To enumerate all values of sort S, a new-style iterator 
		  must be used as follows:
		     S LOOP_VARIABLE;
		     LOOP_VARIABLE = FIRST_S();
		     do {
		        ... loop body parameterized by LOOP_VARIABLE
		     } while (NEXT_S (LOOP_VARIABLE));
		  For instance, the new-style iterator for enumerating the
		  integer range 0..15 has the form:
		     #define FIRST() 0
		     #define NEXT(X) ((X)++ < 15)

		Given that there exist two forms of iterators, which one
		should be preferred? The rule is simple: From now on, the
		use of new-style iterators is highly recommended in LOTOS
		files and in their associated hand-written ".t" and ".f"
		files. Specifically, any further use of "enumeratedby"
		clauses in special comments is discouraged; "iteratedby"
		clauses should be used instead. (Backward compatibility
		issues will be discussed later below).

		Consequently, the following changes have been brought to the
		CADP toolbox:

		- The CAESAR.ADT compiler was modified to handle special
		  comments of the form "iteratedby ... and ..." and to
		  generate appropriate C code for new-style iterators. The
		  "-map" and "-external" options of CAESAR.ADT have been
		  extended accordingly.

		- The CAESAR.INDENT pretty-printer was modified to accept
		  special comments of the form "iteratedby ... and ...".

		- The CAESAR compiler was modified to handle special
		  comments of the form "iteratedby ... and ...". In the
		  generated C code, CAESAR can now invoke new-style
		  iterators instead of old-style ones according to rules
		  detailed below. The "-map" option was also updated.

		- In all "*.lib" files contained in directory $CADP/lib,
		  special comments of the form "enumeratedby" have been
		  replaced with "iteratedby" ones.

		- Consequently, in all "X_*.h" files contained in directory
		  $CADP/incl, definitions of old-style iterator macros of
		  the form ADT_ENUM_xxx() have been removed and replaced
		  with corresponding pairs of ADT_ENUM_FIRST_xxx() and
		  ADT_ENUM_NEXT_xxx() macros.

		- In all demo examples containing iterator macros, the
		  "*.lib", "*.h", "*.f", and "*.t" macros have been updated
		  accordingly. The improvement is particularly evident in
		  the case of demo_23, where all the "*.f" containing old-
		  style iterators (a total of 2,464 lines of C code) have
		  been replaced with equivalent, yet shorter ".t" files 
		  (only 111 lines in total) containing new-style iterators.

		Although we recommend to migrate, as much as possible, to
		new-style iterators, we implemented specific policies to
		ensure a maximal backward compatibility for already existing
		LOTOS programs (together with their associated ".t" and ".f"
		files) making use of old-style iterators. In some cases
		however, backward compatibility cannot be ensured, thus
		leaving migration as the only available option.

		First, to avoid migration problems, one should carefully erase
		the ".h" files generated by former versions of CAESAR.ADT
		and the ".c" files generated by former versions of CAESAR.

		The backward compatibility rules implemented in CAESAR.ADT and
		CAESAR are the following:

		(1) If an "iteratedby" comment is present when a LOTOS sort
		    S is declared, then CAESAR.ADT will generate a new-style
		    iterator for S, and CAESAR will invoke this new-style 
		    iterator whenever it is necessary to enumerate all values
		    in the domain of S.

		(2) If an "enumeratedby" comment is present when a LOTOS sort
		    S is declared, then CAESAR.ADT will generate *both* an
		    old-style iterator and a new-style iterator for S, and
		    CAESAR will invoke the old-style iterator whenever it is
		    necessary to enumerate all values in the domain of S.

		(3) If neither "iteratedby" nor "enumeratedby" comment is
		    present when a LOTOS sort S is declared, then CAESAR.ADT
		    and CAESAR will consider, by default, that sort S has a
		    new-style iterator, the name of which is unspecified and
		    provided automatically by CAESAR.ADT and CAESAR. Thus,
		    CAESAR.ADT will generate a new-style iterator for S, and
		    CAESAR will invoke this new-style iterator whenever it is
		    necessary to enumerate all values in the domain of S.

		Note: following rules (1)-(3), a new-style iterator will
		always be generated, independently of whether an "iteratedby"
		or "enumeratedby" comment is present or not.

		Note: in the syntax of special comments attached to LOTOS
		sorts, it is not allowed to specify simultaneously 
		"enumeratedby" and "iteratedby" for the same LOTOS sort.

		Note: rule (3) breaks backward compatibility (but only if
		hand-written old-style iterators are given in the ".t" file
		or if the old-style iterators generated by CAESAR.ADT are
		invoked in some hand-written C program). Previously, any LOTOS
		sort without special comment would be given an old-style
		iterator by default. From now on, it will be given a new-style
		iterator by default. In that case, we decided to give priority
		to new-style iterators instead of old-style ones.

		In addition to the general rules (1)-(3), the following rules
		detail how particular cases are handled:

		(4) In the C code generated by CAESAR.ADT, all iteration
		    macros (either old-style or new-style) are enclosed
		    between #ifdef ... and #endif. This allows users to
		    provide their own iterators by defining their own macros
		    in the ".t" file. Because of #ifdef clauses, the C code
		    generated by CAESAR.ADT will not override the actual
		    macro-definitions provided by the user.

		(5) The new version of CAESAR.ADT will analyze (during its
		    "type survey" phase) the ".t" file (if present) to 
		    determine whether it contains hand-written (old-style or
		    new-style) iterators for the LOTOS sorts. Similarly, the
		    new version of CAESAR does the same with the ".h" file,
		    which can be either generated automatically by CAESAR.ADT
		    or provided by the user.

		    Note: for a new-style operator, the existence test is
		    done by checking the existence of both macros, i.e.,
		       #if defined(FIRST) && defined (NEXT)
		    If only one macro is defined (i.e., if FIRST() exists
		    but not NEXT(), or vice versa), a warning will be emitted.

		(6) Because the tests on iterator existence mentioned in rules
		    (4) and (5) are implemented using #ifdef conditions, the
		    new-style iterators provided by the user must always be
		    defined as C macro-definitions and not as C functions (for
		    old-style iterators, this is always the case). Otherwise, 
		    the #ifdef condition would always be false. Thus, the rule
		    will be to define FIRST() and NEXT() as macros, even if
		    they could be also defined as C functions. Anyway, if
		    the C code for new-style iterators is so complex that it
		    must be enclosed in functions, say FIRST_FUNCTION() and
		    NEXT_FUNCTION(), it is always possible (and required) to
		    define FIRST() and NEXT() as wrappers around these
		    functions, i.e.,
		       #define FIRST() FIRST_FUNCTION()
		       #define NEXT(X) NEXT_FUNCTION(&(X))

		(7) If a LOTOS sort S is specified to be "external" using a
		    special comment of the form "(*! ... external *)", and if
		    CAESAR needs to enumerate the value domain of S, then a
		    ".t" file should be present and should contain an iterator
		    for S. CAESAR.ADT will not generate iterators for external
		    sorts and CAESAR will emit warning/error messages when
		    trying to enumerate the value domain of external sorts
		    without hand-written iterators.

		(8) As regards hand-written old-style iterators given in the
		    ".t" file: it is strongly recommended to rewrite them
		    into new-style iterators. However, to preserve backward
		    compatibility, CAESAR.ADT will generate macro-definitions
		    in which new-style iterators are derived from old-style
		    ones. These new-style operators provided for backward
		    compatibility are functionally correct but slower: when
		    used to enumerate a domain with N values, they take a
		    quadratic amount of time O(N^2) instead of a linear one
		    O(N). Therefore, migrating towards hand-written new-style
		    iterators is advised.

		(9) The new version of CAESAR.ADT analyzes the constructors
		    of each LOTOS sort in order to detect whether the value
		    domain of each sort is finite or infinite (this is done
		    by computing fixed points, since an infinite sort is
		    characterized by the existence of recursive constructor
		    definitions). Even if a sort S has an infinite value
		    domain, the user can always define, in the ".t" file, an
		    iterator for S that enumerates only a finite subset of
		    the value domain of S. If such an iterator is present,
		    CAESAR and CAESAR.ADT will consider that sort S, although
		    infinite in theory, is actually bounded. Otherwise, sort S
		    will be considered as "truly" infinite. In any case,
		    CAESAR.ADT will not generate iterators for infinite sorts
		    and CAESAR will emit warning/error messages when trying
		    to enumerate the value domain of external sorts without
		    hand-written iterators.

		Note: For an external, infinite or "complex" sort S, the
		previous versions of CAESAR.ADT would generate, in the ".h"
		file, a "fake" iterator CAESAR_ADT_NO_ITERATOR_S() that
		would, in turn, invoke a macro CAESAR_ADT_NO_ITERATOR ("S")
		that would itself trigger an exception (using the raise (15)
		signal) as soon as the iterator is invoked. This is no longer
		the case: the new version of CAESAR.ADT generates no iterator
		at all for such sorts and the CAESAR_ADT_NO_ITERATOR_S() and
		CAESAR_ADT_NO_ITERATOR() macros are no longer defined.
		Consequently, the new version of CAESAR no longer tries to
		invoke such macros: instead, during its "type survey" phase,
		it checks for the existence of iterators in the ".h" file;
		if it is required to invoke an interator that does not exist,
		CAESAR will emit first a warning message, followed by an
		error message during the simulation phase when the iterator
		is actually invoked. Note that ".c" files generated by former
		versions of CAESAR should be erased and regenerated, as they
		might contain invocations to the CAESAR_ADT_NO_ITERATOR_S()
		and CAESAR_ADT_NO_ITERATOR() macros.

		(10) Beyond rules (1)-(3), there are two cases in which the
		    new version of CAESAR.ADT tries to generate an old-style
		    iterator for some LOTOS sort S:
		    - when S is declared with an "enumeratedby" comment, as
		      specified by rule (2)
		    - when S is declared with an "iteratedby" comment or
		      without comment, but appears as a field of a tuple
		      sort S' declared with an "enumeratedby" comment (i.e.,
		      S' has a unique constructor with one or several
		      parameters of sort S).
		    The second case intends to provide backward compatibility
		    as much as possible.

		(11) There are situations in which it is not possible to  
		    generate an old-style iterator for some sort S, because
		    of issues a) and b) listed above. This happens when
		    S is finite and S does not have a hand-written iterator
		    given in the ".t" file and
		    - either S is a "complex" sort
		    - or S is a tuple sort, the unique constructor of which
		      has at least one parameter of sort S' such that S' is
		      either a tuple sort, or an external sort declared with
		      an "iteratedby" comment, or a sort declared with an
		      "iteratedby" comment for which a hand-written iterator
		      exists in the ".t" file.
		    In such case, CAESAR.ADT will emit a warning message
		    reporting that the old-style iterator cannot be produced.

		Note: To summarize the benefits of new-style iterators, the
		new version of CAESAR.ADT can generate an iterator for any
		LOTOS sort S that is not declared as external and for which
		no hand-written iterator is given in the ".t" file and that
		has a finite value domain.

BUG FIX
Number:		904
Date: 		Mon Apr 26 13:25:23 MEST 2004
Report:		Bruno Ondet (INRIA/VASY)
Author:		Nicolas Descoubes (INRIA/VASY)
Files:		com/tst, com/installator

Nature:		Two bugs have been fixed in the INSTALLATOR and "tst" tools:
		both tools would fail if the environment variable $CADP_TMP
		was set to a non-existent directory, or to a non-writable
		directory, or to a relative pathname (i.e., not starting
		with a `/'). From now on, both INSTALLATOR and "tst" will
		check that $CADP_TMP is set to the absolute pathname of a
		writable directory and, if not, emit a proper error message. 

IMPROVEMENT
Number:		905
Date: 		Tue Apr 27 13:02:01 MEST 2004
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/installator, src/installator/installator.tcl

Nature:		Many improvements have been made to the INSTALLATOR assistant:

		- INSTALLATOR now handles file and directory name that contain
		  spaces (such as "Program Files", "Documents and Settings",
		  etc.)

		- A "Retry" button was added when the FTP connection needed
		  to search for the most recent (beta-)version of CADP fails.

		- A "Show Prototype License File" was added to display the
		  prototype license file before it is sent to the CADP team.

		- Environment variables $LANG and $LC_ALL are now set to
		  standard values so as to ensure a correct functioning in
		  any country. 

		- The builtin FTP client of INSTALLATOR now opens "passive"
		  connections (instead of "active" ones), which is more
		  compatible with firewall policies that may exist on the
		  side of CADP users. This avoids most "FTP error" messages,
		  but will not bypass strict firewalls (or iptable/ipchains
		  configurations) that disable all FTP downloads.

		- Two new buttons labelled "Look instead for a stable version"
		  and "Look instead for a beta version" have been added. They
		  allow to switch easily from a stable version to a beta-
		  version and vice-versa. These buttons allow to recover
		  easily from the omission of the "-beta" version. 

IMPROVEMENT
Number:		906
Date: 		Tue Apr 27 15:42:26 MEST 2004
Report:		Wendelin Serwe (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		com/svl, bin.*/svl_kernel, man/*/svl.l

Nature:		The semantics of "root leaf reduction" and "node reduction"
		have been modified in order to benefit from the most efficient
		CADP tools available up to date. For instance, certain
		invocations of ALDEBARAN for reducing composition expressions
		have been replaced with invocations of BCG_MIN and GENERATOR.

		Also, to ease the debugging of SVL scripts, the SVL compiler
		has been modified to keep the intermediate files present in
		the current directory when a command called by SVL fails.

BUG FIX
Number:		907
Date:		Tue Apr 27 16:31:48 MEST 2004
Report:		Wendelin Serwe (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard

Nature:		A bug was fixed in SVL. If some label occurring in a hide, 
		rename, or abstraction expression had leading blank characters
		(inside quotes), these blank characters were ignored, since
		SVL would remove quotes while creating the rename, hide, or
		synchronization file.

BUG FIX
Number:		908
Date: 		Fri Apr 30 18:49:46 MEST 2004
Authors:	Nicolas Descoubes, Hubert Garavel, and Frederic Lang
		(INRIA/VASY)
Files:		bin.win32/libBCG.a

Nature:		Two problems have been solved in the BCG library:

		- In some cases, under Windows, the BCG tools could emit a
		  warning message of the form:
		     "bcg_dynamic: stat error on the bcg file"
		  This was due to an error in the system function tmpfile(),
		  which we replaced by a correct function.

		- The value returned by the system function getdtablesize()
		  was increased from 20 to 40, which now allows to open 37
		  BCG files simultaneously (instead of 17 as before).

IMPROVEMENT
Number:		909
Date: 		Tue May  4 14:54:12 MEST 2004
Report:		Jaco van de Pol (CWI, Amsterdam, The Netherlands)
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		bin.*/libcaesar.a, doc/*/Garavel-92-a.*,
		man/*/caesar_hide_1.*, man/*/caesar_rename_1.*

Nature:		The definition of the "gate mode" used in the OPEN/CAESAR
		libraries "hide_1" and "rename_1" was slightly extended.
		Previously, the "gate" extended from the beginning of the
		label up to the first space or tabulation character; now, it
		extends up to the first space, tabulation character, `?', `!',
		or `(' character. This definition is compatible with the
		conventions used in the LOTOS and muCRL languages, but it may
		break compatibility with some (hypothetical) langages that
		would allow the `?', `!', or `(' characters in their gate
		names. The manual pages for the "hide_1" and "rename_1"
		libraries have been made more precise, by defining exactly the
		notion of "the first word of S"  

IMPROVEMENT
Number:		910
Date: 		Tue May  4 15:17:19 MEST 2004
Report:		Nicolas Descoubes (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_standard.h, incl/bcg_standard.h
		doc/*/Garavel-92-a.*, man/*/caesar_standard.*

Nature:		The "caesar_standard.h" include file was modified to ensure
		compatibility with ISO C:

		- It no longer includes <malloc.h> (which does not exist on
		  Mac OS X) but includes <stlib.h> instead. The same change
		  was made also to "bcg_standard.h".

		- Migration from <varargs.h> to <stdargs.h> was achieved.
		  The CAESAR_VARARGS() macro-definition was removed. The
		  prototypes of functions CAESAR_ERROR() and CAESAR_WARNING()
		  was modified to include a first parameter CAESAR_FORMAT
		  (exactly like printf()) in order to be conformant with
		  <stdarg.h>: this change should be totally transparent to the
		  end-users.

BUG FIX
Number:		911
Date: 		Wed May  5 17:58:28 MEST 2004
Report:		Jaco van de Pol (CWI, Amsterdam, The Netherlands)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/ocis.a

Nature:		When launching the OCIS simulator in graphical mode, the
		CAESAR_INIT_GRAPH() primitive was called twice, which was
		inefficient and possibly erroneous, since initialization
		actions that perform side effects should be executed only
		once.

IMPROVEMENT
Number:		912
Date: 		Wed May  5 18:48:13 MEST 2004
Report:		Jaco van de Pol (CWI, Amsterdam, The Netherlands)
Authors:	Radu Mateescu and Hubert Garavel (INRIA/VASY)
Files:		bin.*/evaluator.a

Nature:		The EVALUATOR 3 model-checker is developed using Lex/Yacc.
		When linking the "evaluator.a" library against other binary
		objects (e.g., mcrl.open) also developed using Lex/Yacc,
		name clashes would occur at link edit time. This problem was
		solved by prefixing all Lex/Yacc-related identifiers in
		EVALUATOR 3 with a constant string ("evaluator_yy").

IMPROVEMENT
Number:		913
Date: 		Tue May 25 16:08:34 MEST 2004
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		installator.shar, installator.com, cadp_cygwin.com,
		src/com/install_uncompress

Nature:		The INSTALLATOR assistant was made more portable:

		- An increasing number of operating systems no longer have
		  the "uudecode" command installed by default. From now on,
		  INSTALLATOR will build itself its own version of "uudecode"
		  if the standard "uudecode" is absent from the host machine.
		  Consequently, the "cadp_cygwin.com" shell-script for
		  Windows was simplified, as it no longer needs to install
		  "uudecode": this is now done by INSTALLATOR.

		- Similarly, INSTALLATOR will build itself its own version of
		  "uncompress" if the host machine has neither "uncompress",
		  nor "compress", nor "gunzip", nor "gzip". Also, the 
		  "install_uncompress" shell-script was adapted to perform
		  the installation of CADP using "uncompress", "gzip", etc.
		  depending on what exists. Consequently, the shell-script
		  "cadp_cygwin.com" no longer creates a symbolic link named
		  "uncompress" that points to "gunzip".

IMPROVEMENT
Number:		914
Date: 		Tue Jun  1 15:19:44 MEST 2004
Authors:	Susanne Graf (VERIMAG) and Wendelin Serwe (INRIA/VASY)
Files:		demos/demo_32

Nature:		A new demo (prepared by Susanne Graf in 1994 and slightly
		updated by Wendelin Serwe ten years later) was added to the
		CADP tool set. This demo is about a distributed, lazy cache
		memory preserving sequential consistency.

IMPROVEMENT
Number:		915
Date: 		Wed Jun  2 18:41:59 MEST 2004
Authors:	Frederic Tronel and Frederic Lang (INRIA/VASY)
Files:		demos/demo_33

Nature:		A new demo, dealing with a randomized binary distributed
		consensus protocol proposed by Ben-Or in 1983, was added to
		the CADP tool set.

BUG FIX
Number:		916
Date: 		Tue Jun  8 16:58:07 MEST 2004	
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_cc, src/com/cadp_mail, src/com/cadp_psbox,
		src/com/cadp_tail, src/com/install_version,
		src/com/xeuca_convert, src/com/xeuca_man, src/com/xeuca_ps,
		src/com/xeuca_version, com/tst, com/upc,
		./src/eucalyptus/eucalyptus.tcl,
		./src/installator/installator.tcl

Nature:		Changes were made to the CADP tool set in order to support
		the Linux distribution "gentoo" and, precisely, to avoid
		error messages such as:
		 > tail: `-10' option is obsolete; use `-n 10' since this
		 > will be removed in the future
		To solve this problem, all invocations of the form `head -N',
		`tail -N', and `tail +N' have been replaced, respectively,
		by `head -n N', `"$CADP"/src/com/cadp_tail -n N', and
		`"$CADP"/src/com/cadp_tail -n +N', where "cadp_tail" is a
		new command. 

IMPROVEMENT
Number:		917
Date: 		Tue Jun 15 11:59:34 MEST 2004
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		INSTALLATION_0, INSTALLATION_2

Nature:		The INSTALLATION_0 and INSTALLATION_2 documentation files have
		been simplified and adapted to the latest versions of Linux
		and Cygwin/Windows, and to explain how the $MANPATH variable
		should be set.

IMPROVEMENT
Number:		918
Date: 		Tue Jun 15 15:21:10 MEST 2004
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_web, INSTALLATION_2

Nature:		On Solaris and Linux, when the environment variable $NAVIGATOR
		is not set, it is no longer replaced with "netscape" (since
		most recent Linuxes do not have Netscape installed); instead,
		several browsers are tried, including Mozilla, Firefox, etc.

IMPROVEMENT
Number:		919
Date: 		Wed Jun 16 16:04:29 MEST 2004
Authors:	Nicolas Descoubes, Hubert Garavel, and Damien Bergamini
		(INRIA/VASY)
Files:		tcl-tk/*, bin.*/xsimulator.a, src/ocis/ocis.tcl, 
		src/eucalyptus/eucalyptus.tcl, src/xsimulator/main.tcl, 
		src/bcg_edit/bcg_edit.tcl, src/installator/installator.tcl, 
		src/monitor/main.tcl, src/com/cadp_x11,
		demos/demo_19/graphics/startsimu

Nature:		Several changes were made to port the graphical tools of CADP
		to Mac OS X: 
		- The version of Tcl/Tk shipped with CADP was upgraded to
		  version 8.4.6.
		- The version of Tix shipped with CADP was upgraded to
		  version 8.2. 
		- A new shell-script named cadp_x11 was added.

IMPROVEMENT
Number:		920
Date: 		Thu Jul  1 16:49:43 MEST 2004	
Authors:	Nicolas Descoubes and Wendelin Serwe (INRIA/VASY)
Files:		doc/pdf/Aguilar-Garavel-et-al-01.pdf,
		doc/pdf/Chehaibar-Garavel-et-al-96.pdf,
		doc/pdf/Garavel-98.pdf,
		doc/pdf/Garavel-Lang-01.pdf,
		doc/pdf/Garavel-Mounier-96.pdf,
		doc/pdf/Garavel-Viho-Zendri-00.pdf,
		doc/pdf/Mateescu-00-a.pdf,
		doc/pdf/Mateescu-96.pdf,
		doc/pdf/Mateescu-Sighireanu-00.pdf,
		doc/pdf/Pace-Lang-Mateescu-03.pdf,
		doc/pdf/Sighireanu-Mateescu-97.pdf

Nature:		Several PDF files included in the CADP distribution were
		incorrect (i.e., produced by a bogus PDF document generator).
		These files have been replaced with correct ones. 

IMPROVEMENT
Number:		921
Date: 		Fri Jul  2 17:04:15 MEST 2004
Report:		Stefan Blom (CWI, Amsterdam, The Netherlands)
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/arch, src/com/cadp_cc, src/com/cadp_cpp, src/com/cadp_crlf, 
		src/com/cadp_rm, src/com/install_df, src/com/xeuca_shell, 
		src/com/cadp_which, src/com/xeuca_ps, src/com/xeuca_term 

Nature:		The CADP tool set was ported to AMD's "Opteron" processors
		running in 32-bit mode under Linux.

IMPROVEMENT
Number:		922
Date: 		Mon Jul  5 18:17:49 MEST 2004
Report:		Hubert Garavel (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard

Nature:		The warning messages possibly issued by CAESAR.ADT and CAESAR
		(in the ".err" file) during the compilation of a LOTOS 
		description are now reproduced by the SVL compiler in the SVL
		log file. SVL also reports the occurrence of such message to
		the user, and keeps the ".err" file in the current directory
		until the ``svl -clean'' command is executed.

IMPROVEMENT
Number:		923
Date: 		Thu Jul  8 19:29:23 MEST 2004
Authors:	Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files:		bin.*/libcaesar.a, incl/caesar_standard.h,
		man/*/caesar_standard.*, doc/*/Garavel-92-a.*

Nature:		A new function named CAESAR_TEMPORARY_FILE() was added to
		OPEN/CAESAR's "standard" library.

IMPROVEMENT
Number:		924
Date: 		Tue Jul 13 11:21:45 MEST 2004
Report:		Jack Abily (BULL) and Axel Belinfante (University of Twente)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_cc, src/linux/bin.iX86/libcpatch-2.2.5.a

Nature:		Backward compatibility support was added for the old GNU C
		library "glibc 2.2.5" used in former versions of Linux such
		as Redhat 7.2. This avoids error messages about undefined
		symbols at link edit time, such as:
		   > .../CADP/bin.iX86/libBCG.a(bcg_read_2.o): In function
		   > `BCG_STRING_TO_UPPER': undefined reference to
		   > `__ctype_toupper_loc'
		or:
		   > .../CADP/bin.iX86/libBCG.a(bcg_stream.o): In function
		   > `BCG_PRINT_IN_DOUBLE_QUOTE': undefined reference to
		   > `__ctype_b_loc'

IMPROVEMENT
Number:		925
Date: 		Tue Jul 13 14:47:58 MEST 2004
Author:		Damien Bergamini (INRIA/VASY)
Files:		bin.*/caesar.bdd, man/*/caesar.bdd.*

Nature:		A new tool named CAESAR.BDD was added to the CADP tool set.
		This tool uses Binary Decision Diagrams to compute structural
		properties of Basic Petri Nets. See the "caesar.bdd" manual
		page for details.

IMPROVEMENT
Number:		926
Date: 		Tue Jul 13 17:11:50 MEST 2004
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, man/*/caesar.*

Nature:		The optimization E7 of CAESAR, which removes all network
		transitions that never fire according to Petri net rules,
		was redesigned.

		The former optimization E7 was based on the explicit
		enumeration of all reachable markings ("explicit-state"
		approach); it was optional and only executed if the "-e7"
		option was given on the command-line when invoking CAESAR.

		The new optimization E7 is based on Binary Decision Diagrams
		and relies on the CAESAR.BDD tool (see item #925 above).
		Since this new optimization is much faster, it is no longer
		optional: it is performed by default every time CAESAR is
		invoked.

		Experiments have shown that the new optimization E7 could
		handle large LOTOS examples that could not be processed by
		the old optimization, due to lack of memory. We found no
		counter-example that the old optimization, but not the new
		one, could handle.

		Moreover, on several hundreds of LOTOS examples handled by
		both the old and new optimizations, the new optimization
		proved to be faster than the old optimization by 19%.

		On the same hundreds of examples, it appeared that applying
		the new optimization E7 is as fast as applying no optimization
		E7, either new or old (in fact, it is even slightly faster
		by 0.6%). Thus, the time spent in BDD computations to remove
		dead transitions is totally compensated by the state space
		reductions and time savings arising from a smaller network.
		
		The semantics of CAESAR's command-line options was modified
		as follows:
		- A new option "-e7old" was added for backward compatibility,
		  so as to retain the former behaviour of CAESAR. This option
		  performs the old optimization E7 instead of the new one.
		- Option "-e7" no longer performs the old optimization E7;
		  its new meaning is to disable the new optimization E7.
		- In absence of both "-e7" and "-e7old", the new optimization
		  E7 is peformed by default.

		In summary, there are now three cases:
		- If you do not want optimization E7: use "-e7" option.
		- If you want the old optimization E7: use "-e7old" option.
		- If you want the new optimization E7: use no option.

		The CAESAR manual page was updated accordingly.

IMPROVEMENT
Number:		927
Date: 		Thu Jul 15 12:03:01 MEST 2004
Report:		Nicolas Descoubes (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		src/com/xeuca_info

Nature:		Changes were brought to the "xeuca_info" shell-script in order
		to support recent Linux distributions and, precisely, to avoid
		error messages of the form:
		 > cut: invalid byte, character or field list

IMPROVEMENT
Number:		928
Date: 		Fri Jul 16 14:40:55 MEST 2004
Author:		Damien Bergamini (INRIA/VASY)
Files:		./INSTALLATION_MACOS, ./INSTALLATION_WINDOWS, ./INSTALLATION_0

Nature:		Following the efforts under way to port CADP to Mac OS X,
		the documentation files have been updated:
		- A new file named INSTALLATION_MACOS explains the preliminary
		  steps needed to get CADP working on Mac OS X.
		- The already existing file INSTALLATION_0 was renamed into
		  INSTALLATION_WINDOWS, and a symbolic link INSTALLATION_0
		  pointing to INSTALLATION_WINDOWS was installed for backward
		  compatibility.

IMPROVEMENT
Number:		929
Date: 		Tue Jul 20 11:33:57 MEST 2004
Report:		Humberto Osorio (Universidade Federal do Ceara, Brazil)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.iX86/*

Nature:		The Linux binaries of CADP tools have been made compatible
		with recent Linux distributions based on the Linux 2.6 kernel,
		such as Mandrake version 10.

BUG FIX
Number:		930
Date: 		Wed Jul 21 20:30:43 MEST 2004
Report:		Lars-Ake Fredlund (SICS, Sweden), Marc Herbert (INRIA/VASY),
		and Guy Tremblay (Universite du Quebec a Montreal, Canada)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/*

Nature:		8-bit characters are now allowed in LICENSE files. Previously,
		only 7-bit characters were permitted, and the use of 8-bit
		characters would generate error messages of the form:
		   > *018 protection violation:
		   >      falsified license
		   >      wrong global checksum
		   >      quit

IMPROVEMENT
Number:		931
Date: 		Fri Jul 23 16:54:03 MEST 2004
Report:		Gert Huisman (Vrije Universiteit Amsterdam, The Netherlands),
		and Christophe Joubert (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/*, com/rfl, INSTALLATION_3

Nature:		The CADP licensing mechanism was enhanced to allow multiple
		license files. In addition to the primary license file named
		"$CADP/LICENSE", it is now possible to have a secondary
		license file named "$CADP/LICENSE.1", and even a tertiary
		license file named "$CADP/LICENSE.2". These files will be
		checked in the following order: primary, then secondary, then
		tertiary. This feature is intended to administrators of
		clusters or large networks with hundreds of machines:
		secondary/ tertiary license files allow to obtain licenses
		for machines that were down or otherwise unavailable at the
		time the primary license file was prepared.

BUG FIX
Number:		932
Date: 		Sat Aug  7 11:28 MES 2004
Report:		Katsumi Wasaki (Shinshu University, Nagano, Japan)
Author:		Hubert Garavel (INRIA/VASY)
Files:		demos/demo_04/EXP.t, incl/caesar_kernel.h 

Nature:		The two files "EXP.t" and "caesar_kernel.h" were changed so as
		to remplace the inclusion of <malloc.h> (which does not exist
		on Mac OS X) by the inclusion of <stdlib.h>. This suppresses
		the following error messages emitted by CAESAR and CAESAR.ADT:
		   > .. malloc.h: No such file or directory
		   > #127 error in file ``.h'' during type survey:
		   >      survey program is rejected by the C compiler
		   >      quit

IMPROVEMENT
Number:		933
Date: 		Tue Aug 24 14:57:26 MEST 2004
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c, bin.*/libexpopen.a, bin.*/libexp_open.a,
		com/exp.open, man/*/exp.open.*

Nature:		The EXP.OPEN 1.0 tool, which allows to compile networks of 
		communicating LTSs into the OPEN/CAESAR "caesar_graph" API,
		was replaced by a new version EXP.OPEN 2.0 entirely rewritten
		from scratch.

		The input language of EXP.OPEN 2.0 (i.e., the contents of
		".exp" files) is a superset of the input language of EXP.OPEN
		1.0. That is, the networks of communicating LTSs accepted by
		EXP.OPEN 1.0 (i.e., LTS files combined using LOTOS parallel
		composition and gate hiding operator) are still accepted by
		EXP.OPEN 2.0, which also brings the following extensions:

		- The "hide" operator was generalized so that labels can be
		  defined using regular expressions, possibly in a separate 
		  file, according to the conventions of the "caesar_hide_1" 
		  library.

		- Two new operators, "rename" and "cut", were added to the
		  input language of EXP.OPEN 2.0. Like the generalized "hide"
		  operator, these operators allow labels to be specified using
		  regular expressions, possibly in a separate file.

		- The generalized parallel composition ("par") operator of
		  E-LOTOS was also added; this operator provides advanced
		  features, including "n among m" synchronization.

		- Finally, operators brought from various formalisms were
		  also added to the input language of EXP.OPEN 2.0, namely:
		    - a parallel composition operator based on the notion of
		      synchronization vectors (as in the MEC and FC2 tools),
		    - the parallel composition operators of the CCS, CSP, and
		      mCRL process algebras,
		    - the renaming, cut, and hiding operators of the CCS and
		      CSP process algebras.

		The command-line syntax of EXP.OPEN 2.0 also extends that of
		EXP.OPEN 1.0 with new functionalities:
	
		- New "-branching" and "-ratebranching" options allow to use
		  partial order methods to reduce (at least, partially) state
		  spaces while preserving branching and stochastic branching
		  bisimulations, respectively. By default, strong bisimulation
		  is preserved.

		- A new "-network" option allows to translate the EXP.OPEN 2.0
		  input language into other (lower-level) formats. Currently,
		  two such formats are supported: the Petri net format of the
		  PEP tool (use "-network pep" option) and the parallel FC2
		  format (use "-network fc2").

		- New options ("-ccs", "-csp", "-elotos", "-lotos", "-mcrl")
		  allow to interpret the input language of EXP.OPEN 2.0
		  according to the conventions used in the languages CCS, CSP,
		  E-LOTOS, LOTOS, and muCRL, respectively. These conventions
		  rule, for instance, the case sensitivity in identifiers,
		  the string denoting the silent action ("i", "tau", etc.),
		  the semantics of the "||" operator, etc.

		EXP.OPEN 2.0 corrects all known bugs in EXP.OPEN 1.0. In
		particular:
		- the scope of nested "hide" operators is now correctly
		  handled,
		- there is no more limitation in the number of labels that
		  EXP.OPEN can process, and
		- function CAESAR_HASH_SIZE_STATE() of the OPEN/CAESAR
		  "caesar_graph" API now returns a correct result.

		In the demonstration examples present in the $CADP/demos
		directory, EXP.OPEN 2.0 uses about 2 times less memory than
		EXP.OPEN 1.0, and runs from 1.5 to 45 times faster.

		EXP.OPEN 2.0 provides the user with a better understanding of
		the generated LTS by indicating, for each of its actions, the
		history of successive operations (synchronizations, hidings,
		renamings) that engendered this action.

		Note: EXP.OPEN 2.0 uses a new library named "libexp_open.a",
		which replaces the older "libexpopen.a".

		See the EXP.OPEN manual page for more information.

IMPROVEMENT
Number:		934
Date: 		Tue Aug 24 16:09:39 MEST 2004
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2fc2, com/exp2fc2, man/*/exp2fc2.*

Nature:		The EXP2FC2 program (which contained a few bugs and only
		supported the input language of EXP.OPEN 1.0) was replaced
		by a simple shell-script that invokes EXP.OPEN 2.0 with the
		"-network fc2" option. Indeed, 
		     exp2fc2 FILE.exp FILE.fc2
		is equivalent to:
		     exp.open -case -network fc2 FILE.exp
		The manual page for EXP2FC2 was updated.

IMPROVEMENT
Number:		935
Date: 		Thu Aug 26 14:57:26 MEST 2004
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/rfl

Nature:		The option "-l" of the RFL shell-script was enhanced so as to
		support the secondary and ternary license files, if any (see
		item #931 above).

IMPROVEMENT
Number:		936
Date: 		Fri Aug 27 10:36:35 MEST 2004
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/*, src/com/*, ./INSTALLATION_1, ./INSTALLATION_2,
		./INSTALLATION_3, ./INSTALLATION_4

Nature:		Most CADP shell-scripts were modified in order to support
		spaces in file names. However, this work is not complete yet,
		so the use of spaces in file names is still discouraged.

		Also, the documentation files INSTALLATION_* were updated:
		double quotes were added around every occurrence of $CADP to
		deal with the presence of spaces in directory and file names.

BUG FIX
Number:		937
Date: 		Tue Aug 31 11:38:51 MEST 2004
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/tst, src/com/cadp_adjust, src/com/cadp_windows,
		src/installator/installator.tcl, ./INSTALLATION_4

Nature:		The existing "cadp_windows" shell-script was renamed into
		"cadp_adjust". This shell-script fixes two issues arising on
		Windows:

		- The Cygwin symbolic links are not recognized by standard
		  Win32 applications, among which the CADP binaries; the
		  script "cadp_adjust" solves this problem by replacing all
		  symbolic links by their target.

		- The text files of CADP contain only LF characters and, thus,
		  do not display properly on certain Windows applications
		  such as Notepad; the script "cadp_script" solves this
		  problem by replacing every LF character by a pair CR/LF.

		The INSTALLATOR assistant was modified to invoke "cadp_adjust"
		automatically when installing CADP on a Windows system.

		The "INSTALLATION_4" file (directives for manual installation
		of CADP) was modified to mention that "cadp_adjust" must be
		invoked. 

		Finally, the "tst" shell-script was adapted to detect whether
		"cadp_adjust" has been been correctly applied.

IMPROVEMENT
Number:		938
Date: 		Wed Sep  1 15:13:28 MEST 2004
Report:		Damien Bergamini (INRIA/VASY)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		bin.macOS/xsimulator.a

Nature:		The XSIMULATOR tool was ported to Mac OS X. It will launch
		automatically the X11 server if this server is not already
		running. This is done by invoking the $CADP/src/com/cadp_x11
		shell-script.

BUG FIX
Number:		939
Date: 		Mon Sep  6 10:30:49 MEST 2004
Author:		David Champelovier (INRIA/VASY)
Files:		com/caesar.open

Nature:		The "caesar.open" shell-script no longer sets the environment
		variable $CADP_LANGUAGE to "-english", as this was overriding
		the genuine value of $CADP_LANGUAGE set by the user and the
		"-french" option possibly passed to "caesar.open". 

BUG FIX
Number:		940
Date: 		Tue Sep  7 14:44:02 MEST 2004
Report:		Damien Bergamini (INRIA/VASY)
Author:		Nicolas Descoubes (INRIA/VASY)
Files:		src/bcg_edit/bcg_edit.tcl

Nature:		A bug was fixed in the BCG_EDIT tool. After selecting "Load
		BCG" in the "File" menu, and then making a double click
		(instead of a simple click) on a directory name different
		from the parent directory "..", a warning message would occur:
		   > bad listbox index "": must be active, anchor, end, 
		   > @x,y, or a number

IMPROVEMENT
Number:		941
Date: 		Thu Sep  9 15:05:57 MEST 2004
Report:		Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar.bdd, bin.*/caesar, man/*/caesar.bdd.*

Nature:		The CAESAR.BDD tool was enhanced in several ways:
		- The Basic Petri Net format was extended with, for each
		  unit, the list of its sub-units;
		- CAESAR.BDD now handles properly user interrupts (Ctrl-C);
		- CAESAR.BDD now returns different exit codes for each cause
		  of error;
		- A bug with option "-unit" was fixed.
		The CAESAR compiler was also enhanced to recover from the
		various errors faced by CAESAR.BDD, to display relevant error
		messages, to abort optimization E7 properly, and to continue
		its execution.

BUG FIX
Number:		942
Date: 		Mon Sep 13 10:30:10 MEST 2004
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		demos/demo_26/*

Nature:		The ADT_ENUM_NEXT_NAT() iterators defined in the ".f" files of
		demo_26 have been updated to avoid a "macro redefined" warning
		produced by the C compiler. Also, all the ".f" files have been
		renamed into ".t" files, to follow the CAESAR.ADT conventions.

BUG FIX
Number:		943
Date: 		Mon Sep 13 10:59:08 MEST 2004
Report:		David Champelovier (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/libBCG_IO.a

Nature:		A bug was fixed in the BCG_IO_WRITE_BCG_END() function of
		the "bcg_write" API; in some cases, this bug would cause a 
		segmentation fault / core dump on Linux.

IMPROVEMENT
Number:		944
Date:		Fri Sep 17 11:33:25 MEST 2004
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/rfl, com/installator, src/installator/*, installator.shar

Nature:		The CADP installation procedure was enhanced so that CADP
		users can receive by e-mail a reminder message a fixed number 
		of days (by default, 30 days) before their license expires.
		This new feature required the following changes:

		- LICENSE files now contain the e-mail address of the person
		  to whom the reminder message will be sent;

		- LICENSE files also contain the number of days in advance at
		  which the reminder must be set;

		- The RFL shell-script was extended with two new options
		  ("-e" and "-r") that extract from LICENCE files the e-mail
		  address and the number of days, respectively;

		- INSTALLATOR now always asks for an e-mail address (before,
		  this was optional for Unix and only mandatory on Windows);
		  incidentally, this will solve the problem of LICENSE files
		  sent to the CADP team from the "root" account of Unix,
		  which could be returned only to "root" and not to a real
		  user e-mail address.

BUG FIX
Number:		945
Date: 		Fri Sep 24 10:03:30 MEST 2004
Report:		Marc Herbstritt (Albert-Ludwigs University, Freiburg, Germany),
		Venkatesh P. Ranganath (Kansas State University, USA), and
		Judi Romijn (Technical Univ. of Eindhoven, The Netherlands)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		src/installator/installator.tcl, src/com/install_uncompress

Nature:		On recent Linux systems equipped with GNU tar version 1.14,
		the INSTALLATOR assistant would fail with the following error
		message:
		   > Extracting files from archive CADP_...tar.Z
		   > ./src/linux/bin.iX86/
		   > ./src/linux/bin.iX86/libcpatch-2.2.5.a
		   > ./gc/bin.iX86/
		   > ./gc/bin.iX86/COPYRIGHT_GC
		   > ...
		   > ./bin.iX86/cadp_hostinfo
		   > ./bin.iX86/bcg_graph
		   > ./bin.iX86/caesar.bdd
		   > Error while decompressing

		This problem (which did not occur with the previous version
		1.13.25 of GNU tar) is due to an unexpected change in the
		behaviour of GNU tar, the new version of which writes a
		message (of the form "tar: Read 1536 bytes from -") to the
		stderr stream even if the extraction performed successfully.
		The presence of such messages on the stderr stream confused
		INSTALLATOR, which believed that an error occurred.

		This problem was fixed. Additionally, to prevent similar
		errors arising from further modifications of GNU tar, gzip,
		or uncompress, various buttons were added ("Abort", "Retry",
		"Continue"), so that the user can decide to continue if he/she
		believes that extraction performed correctly.

IMPROVEMENT
Number:		946
Date: 		Fri Sep 24 10:50:51 MEST 2004
Report:		Christophe Lohr (Concordia University, Montreal, Canada), and
		Philippe Marty (Universite de Paris-Sud, Orsay, France)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		src/installator/installator.tcl,
		./INSTALLATION_3, ./INSTALLATION_4

Nature:		The INSTALLATOR assistant was modified to address the case
		of machines that cannot send prototype license files using
		e-mail (and also the case of machines that can send e-mail
		actually, but in an undetectable way, i.e. a way that cannot
		be predicted reliably in advance).

		By default, the new version of INSTALLATOR will send the
		prototype license files using the FTP protocol, i.e., by
		uploading these files onto the VASY FTP server. However,
		INSTALLATOR will still provide the user with 3 possibilities:
		"Send by FTP", "Send by e-mail", and "Save to disk".

BUG FIX
Number:		947
Date: 		Mon Sep 27 09:12:00 MEST 2004
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel

Nature:		A bug was fixed in SVL to handle non-quoted identifiers
		correctly when the "-case" option is set.

BUG FIX
Number:		948
Date: 		Thu Sep 30 17:04:45 MEST 2004
Report:		Greg Eakman (Boston University, Massachussets, USA)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/installator, src/installator/installator.tcl,
		src/com/install_clone, src/com/install_lock,
		src/installator/bin.win32/install_lock.exe

Nature:		A double problem with the Windows version of INSTALLATOR was
		solved. This problem comes from the "locks" that Windows puts
		on files and directories when they are in use. When locked,
		a file or a directory cannot be removed or modified. Thus,
		the Windows version of INSTALLATOR would fail to upgrade
		CADP properly if, for instance, a binary program of CADP was
		already executing (first problem). Also, when INSTALLATOR
		was launched from an existing CADP installation (i.e., by
		running the command "$CADP/com/installator"), rather than
		launched from the "installator.com" file, this would create
		a lock on the existing "$CADP/com" directory (because of the
		existence of a running program in this directory), and thus
		this directory would become unwritable and would prevent CADP
		from being upgraded properly (second problem).

		To solve these two Windows-specific locking problems, the
		following changes were made to INSTALLATOR:

		- When "$CADP/com/installator" is launched to upgrade an
		  existing version of CADP (located in directory "$CADP"),
		  INSTALLATOR will start by "cloning" itself, i.e., copying
		  all its files in "/tmp" and re-launching itself from there.
		  This avoids creating a lock on "$CADP/com" and, thus, solves
		  the second problem.

		- In addition, a test was added to terminate the execution of
		  INSTALLATOR if the "$CADP" directory is locked, i.e., if
		  some CADP program is already executing. This addresses the
		  first problem.

BUG FIX
Number:		949
Date: 		Mon Oct  4 17:01:07 MEST 2004
Report:		Hubert Garavel and Radu Mateescu (INRIA/VASY)
Author:		Nicolas Descoubes (INRIA/VASY)
Files:		com/upc, com/rfl, com/cadp_hostname

Nature:		A minor problem of RFL on Solaris was fixed. This problem
		(upper-case letters instead of lower-case letters in prototype
		license files) only occurred when RFL invoked "/usr/bin/tr"
		instead of "/usr/ucb/tr".

IMPROVEMENT
Number:		950
Date: 		Mon Oct  4 19:14:13 MEST 2004
Report:		Hubert Garavel (INRIA/VASY)
Author:		Nicolas Descoubes (INRIA/VASY)
Files:		com/tst

Nature:		Changes were brought to "tst" in order to allow a better
		detection of the Glibc version number. The modified version
		of "tst" now uses three different methods to ensure that the
		Glibc version number will be properly detected.

BUG FIX
Number:		951
Date: 		Fri Oct  8 14:46:09 MEST 2004
Report:		Frederic Lang (INRIA/VASY)
Authors:	Damien Bergamini and Hubert Garavel (INRIA/VASY)
Files:		bin.*/bcg_min

Nature:		A bug in the implementation of the branching stochastic
		bisimulation was fixed in the BCG_MIN tool. Due to this bug,
		the reduction was not "total" in the sense that one single
		call to "bcg_min -rate -branching" would not always yield the
		minimal stochastic LTS (in some cases, several calls would
		be necessary).

IMPROVEMENT
Number:		952
Date: 		Tue Oct 12 12:17:52 MEST 2004
Report:		Solofo Ramangalahy (BULL) and
		Ken Turner (University of Stirling, Scotland, UK)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		com/rfl, src/com/install_rfl, src/installator/installator.tcl 

Nature:		The RFL and INSTALLATOR tools were modified to provide a
		better support for the SSH protocol. Previously, the RFL
		command tried to estblish remote connections using, first,
		"rsh", then "ssh", then "krsh", and thus could be slow (due
		to timeouts) for machines supporting "ssh" but not "rsh".

		To address this issue, a new "-p" option was added to RFL,
		which specifies the protocol ("rsh", "ssh", or "krsh") to be
		tried first when attempting remote connections. The shell
		"install_rfl" was also modified to support this "-p" option.
		Finally, INSTALLATOR was modified to offer the choice between
		these three protocols.	

BUG FIX
Number:		953
Date: 		Tue Oct 12 15:29:32 MEST 2004
Report:		Tomas Barros (INRIA/OASIS, Sophia-Antipolis, France)
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		installator.shar

Nature:		The Mac OS X version of "installator.shar" was modified to
		solve a problem with the version of "uudecode" present on
		MacOS X 10.3; for security purpose, this particular version
		of "uudecode" requires a "-s" option, otherwise it removes
		the last "/" in the pathnames, leading to error messages of
		the form:
		   > installator.shar: line 807: /tmp/_sh01984/cmp:
		   > No such file or directory
		This problem was solved.

IMPROVEMENT
Number:		954
Date: 		Mon Oct 18 11:20:53 MEST 2004
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c, man/*/exp.open.*

Nature:		A new "-interface" option was added to EXP.OPEN 2.0. This
		option allows to synthesize an "interface" expressing the
		synchronization constraints imposed on one LTS by (a subset
		of) its neighbour LTSs in a parallel composition expression.
		Practically, EXP.OPEN with option "-interface" generates a 
		C file containing an OPEN/CAESAR graph module (implicit LTS)
		and a ".sync" file containing a list of labels. The graph 
		module can be then translated into an interface (explicit LTS)
		using the GENERATOR tool. The resulting LTS can then be given,
		together with the ``.sync'' file, to the PROJECTOR tool. See
		the updated "exp.open" manual page for more details.

IMPROVEMENT
Number:		955
Date: 		Tue Oct 19 16:42:10 MEST 2004
Authors:	Nicolas Descoubes, Hubert Garavel, Christophe Joubert, and
		Radu Mateescu (INRIA/VASY)
Files:		man/*/bcg_info.*, man/*/bcg_labels.*, man/*/bcg_min.*,
		man/*/caesar_*.*, doc/*/Garavel-92-a.*

Nature:		Various mistakes have been fixed in the BCG_INFO, BCG_LABELS,
		and BCG_MIN manual pages, and in the OPEN/CAESAR reference
		manual.

IMPROVEMENT
Number:		956
Date: 		Thu Oct 21 15:03:55 MEST 2004
Authors:	Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_hash.h, bin.*/libcaesar.a,
		man/*/caesar_hash.*, doc/*/Garavel-92-a.*

Nature:		In the "hash" library of OPEN/CAESAR, the existing macro-
		definitions CAESAR_STATE_i_HASH(), where i = 0..6, and
		CAESAR_LABEL_0_HASH() have been turned into functions, so that
		they can be passed as actual parameters to other functions.

		Also, new functions CAESAR_LABEL_i_HASH(), where i= 1..6, and
		CAESAR_STRING_0_HASH() have been added to the "hash" library.

IMPROVEMENT
Number:		957
Date: 		Thu Oct 21 16:55:58 MEST 2004
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_standard.h, bin.*/libcaesar.a,
		man/*/caesar_standard.*, doc/*/Garavel-92-a.*

Nature:		The "standard" library of OPEN/CAESAR was enhanced in three
		ways:

		- Better explanations about CAESAR_ALIGNMENT_POINTER() and the
		  notion of alignment factor have been added.

		- Five new "functional" types have been added, respectively:
		  CAESAR_TYPE_GENERIC_FUNCTION, CAESAR_TYPE_COMPARE_FUNCTION,
		  CAESAR_TYPE_HASH_FUNCTION, CAESAR_TYPE_CONVERT_FUNCTION,
		  and CAESAR_TYPE_PRINT_FUNCTION.

		- A new function CAESAR_FUNCTION_NAME() was added, which
		  allows a better display of the predefined function names
		  of the OPEN/CAESAR library.

IMPROVEMENT
Number:		958
Date: 		Thu Oct 21 18:16:09 MEST 2004
Authors:	Frederic Lang and David Champelovier (INRIA/VASY)
Files:		com/svl, bin.*/svl_kernel, src/svl/standard

Nature:		SVL was improved in order to work correctly when the $CADP 
		environment variable contains spaces or blank characters.

IMPROVEMENT
Number:		959
Date: 		Mon Oct 25 15:21:22 MEST 2004
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_block_1.h, bin.*/libcaesar.a,
		man/*/caesar_block_1.*, doc/*/Garavel-92-a.*

Nature:		A new OPEN/CAESAR library named "block_1" was added to CADP.
		This library provides some form of object-orientation for
		memory blocks of different classes (ordinary, empty, state,
		label, or string).

IMPROVEMENT
Number:		960
Date: 		Wed Nov  3 16:32:35 MET 2004
Authors:	Hubert Garavel and Nicolas Descoubes (INRIA/VASY)
Files:		incl/caesar_mask_1.h, bin.*/libcaesar.a, 
		man/*/caesar_mask_1.*, doc/*/Garavel-92-a.*

Nature:		A new OPEN/CAESAR library named "mask_1" was added to CADP.
		This library allows to perform sequences of hiding and
		renaming operations on memory blocks (labels, strings, ...)
		in the style of BCG_LABELS command-line options. 

IMPROVEMENT
Number:		961
Date: 		Wed Nov  3 17:33:08 MET 2004
Authors:	Hubert Garavel and Nicolas Descoubes (INRIA/VASY)
Files:		src/open_caesar/generator.c, src/open_caesar/generator2.c,
		src/open_caesar/reductor.c, src/open_caesar/reductor2.c,
		src/open_caesar/READ_ME, incl/bcg_options.h

Nature:		The GENERATOR and REDUCTOR tools have been enhanced with
		new command-line options: 

		- Options "-uncompress", "-compress", "-register", "-short",
		  "-medium", "-size", and "-tmp" allow to control the
		  generated BCG graph. For these options, the "bcg_options.h"
		  header file was added in directory $CADP/incl.

		- Options "-hide" and "-rename" (together with the qualifiers
		  "-total", "-partial", "-gate", "-single", and "-multiple")
		  perform on-the-fly hiding and/or renaming of labels. These
		  options are implemented using the recent "mask_1" library
		  (see item #960 above).

		The source C code of GENERATOR and REDUCTOR is available
		in directory $CADP/src/open_caesar. The former versions of
		GENERATOR and REDUCTOR (which are easier to read and to
		understand than the latest versions) are kept in that
		directory for user information (see the READ_ME file for
		information).

IMPROVEMENT
Number:		962
Date: 		Mon Nov 15 12:34:39 MET 2004
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_stack_1.h, bin.*/libcaesar.a, 
		man/*/caesar_stack_1.*, doc/*/Garavel-92-a.*

Nature:		The programming interface of OPEN/CAESAR's "stack_1" library
		was improved:
		- A new function type CAESAR_TYPE_OVERFLOW_FUNCTION_STACK_1
		  was added to caesar_stack_1.h.
		- Consequently, the type of the 3rd argument CAESAR_OVERFLOW
		  of function CAESAR_CREATE_STACK_1() was changed into
		  CAESAR_TYPE_OVERFLOW_FUNCTION_STACK_1. The explanations
		  given in the "stack_1" manual page regarding this argument
		  were simplified.

		This change is fully compatible at the binary level, meaning
		that all OPEN/CAESAR application tools available under binary
		form (".a" or ".o") need not be recompiled with the modified
		"caesar_stack_1.h" file and can be directly linked against the
		modified "libcaesar.a" library.

IMPROVEMENT
Number:		963
Date: 		Wed Nov 17 15:27:24 MET 2004
Authors		Nicolas Descoubes and Hubert Garavel (INRIA/VASY)
Files:		bin.*/bcg_labels

Nature:		The code of the BCG_LABELS tool was greatly simplified by
		taking advantage of the recent "mask_1" library (see item
		#960 above). This simplification should be totally transparent
		to the end-user.

IMPROVEMENT
Number:		964
Date: 		Thu Nov 25 14:28:06 MET 2004
Report:		Damien Bergamini (INRIA/VASY)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		./tst

Nature:		The "tst" shell-script was improved in order to detect, on
		MacOS, situations in which the maximal size allocated to the
		execution stack is unsufficient. For instance, setting a limit
		of 512 kbytes to the execution stack might cause BCG_MIN to
		abort with a core dump. The improved "tst" will warn about
		such situations.

IMPROVEMENT
Number:		965
Date: 		Wed Dec  1 17:59:33 MET 2004
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/libBCG_IO.a, man/*/bcg_write.*

Nature:		In function BCG_IO_WRITE_BCG_BEGIN() of the "bcg_write" API,
		it is now permitted to give a NULL value to the parameter 
		bcg_creation_comment.

IMPROVEMENT
Number:		966
Date: 		Fri Dec  3 15:07:12 MET 2004
Authors:	Holger Hermanns (Saarland University), Christophe Joubert,
		Hubert Garavel, and David Champelovier (INRIA/VASY)
Files:		bin.*/bcg_steady, bin.*/bcg_transient, bin.*/READ_ME
		man/*/bcg_steady.*, man/*/bcg_transient.*

Nature:		Two new tools, BCG_STEADY and BCG_TRANSIENT, for performance
		evaluation have been integrated into the CADP toolbox. The
		BCG_STEADY tool performs steady-state analysis, and the
		BCG_TRANSIENT tool performs transient analysis. For details,
		see the manual pages.

BUG FIX
Number:		967
Date: 		Fri Dec 10 14:44:28 MET 2004
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard, man/man.*/svl.*

Nature:		A semantic bug was fixed in SVL. An ``abstraction'' operator
		with a synchronization set of the form ``all but'' followed
		by an empty list of gates or labels was processed exactly as
		an ``abstraction'' operator without synchronization set. SVL
		was modified to implement the correct semantics, namely:

		- In the former case, synchronization is required on all gates
		  or labels (depending on the matching mode) that occur in the
		  interface graph, except "i".

		- In the latter case, synchronization is required on all gates
		  or labels (depending on the matching mode) that occur in any
		  of the interface and/or specification graphs, except "i".

IMPROVEMENT
Number:		968
Date: 		Mon Dec 13 09:10:15 MET 2004
Author:		Wendelin Serwe (INRIA/VASY)
Files:		incl/caesar_hash.h, bin.*/libcaesar.a,
		man/*/caesar_hash.*, doc/*/Garavel-92-a.*

Nature:		The dispersion of the hash function CAESAR_STRING_0_HASH() was
		improved.

IMPROVEMENT
Number:		969
Date: 		Mon Dec 13 15:34:45 MET 2004
Author:		Hubert Garavel (INRIA/VASY)
Files:		incl/caesar_block_1.h, incl/caesar_area_1.h,
		bin.*/libcaesar.a,
		man/*/caesar_block_1.*, man/*/caesar_area_1.*,
		doc/*/Garavel-92-a.*

Nature:		The recent "block_1" library of OPEN/CAESAR was renamed into
		"area_1" in order to avoid confusion with the notion of block
		used in the "solve_1" library to be added soon to OPEN/CAESAR
		(see item #979 below). Consequently, the include files and
		manual pages named "caesar_block_1.*" have been renamed into
		"caesar_area_1.*".

		Also, the "area_1" library was extended with the notion of
		empty area.

		Finally, a new function CAESAR_HASH_STRING_AREA_1() was added.

BUG FIX
Number:		970
Date: 		Mon Dec 13 19:01:18 MET 2004
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		incl/caesar_table_1.h, bin.*/libcaesar.a,
		man/*/caesar_table_1.*, doc/*/Garavel-92-a.*,
		com/upc

Nature:		The "table_1" library of OPEN/CAESAR, and especially its
		CAESAR_CREATE_TABLE_1() function, have been enhanced in
		subtle ways. The rationale for these changes are threefold:
 
		- Take advantage of the new "area_1" library to improve and
		  simplify the programming interfaces (API) of "table_1":
		  in particular, the use of "area_1" now allows to specify
		  both the memory size and the memory alignment for the base
		  and mark fields (the previous "table_1" API only allowed
		  to specify the memory size).

		- Make the "table_1" more generic (so that it becomes simpler
		  to use the table to store other objects than states) by
		  using the functionnalities of the "area_1" library for
		  automatic selection of hash functions, printing functions,
		  etc. This removes odd dependencies of the "table_1" with
		  respect to the notion of states.

		- Solve an issue that occurred when the base field and the
		  mark field had different memory alignments; the mark field
		  would be improperly aligned, possibly resulting in run-time
		  errors (segmentation faults) unless the programmer took
		  explicit provision to avoid this problem; from now on, the
		  "table_1" library will insert appropriate padding bytes
		  before and after the mark field, so that base and mark
		  fields are always aligned properly.

		Strictly speaking, these changes are not upward compatible
		with the previous versions of the "table_1" library. We
		introduced these changes nevertheless since we believed that
		they were required for a long-term future. However, we took
		great care to ensure backward compatibility as much as
		possible, although we cannot guarantee this in all cases.
		Users facing problems with this migration should contact
		the cadp@inrialpes.fr mailing-list.

		All the changes concern the CAESAR_CREATE_TABLE_1() function,
		which has 10 parameters. Specifically, the changes concern
		the 2nd, 3rd, 7th, 8th, 9th, and 10th parameters.

		* Changes for the 2nd parameter (CAESAR_BASE_SIZE)

		From now on, the parameter CAESAR_BASE_SIZE is declared of
		type CAESAR_TYPE_AREA_1 instead of CAESAR_TYPE_NATURAL. In
		most cases, this change should be upward compatible. However,
		we strongly advise users of the "table_1" library to examine
		every call to CAESAR_CREATE_TABLE_1() and to update the actual
		values supplied for the CAESAR_BASE_SIZE parameter: instead
		of a mere natural number, the actual value should be formed
		using the appropriate primitives provided by the "area_1"
		library. These primitives allow to specify memory alignment
		constraints for the base field and to make special cases of
		base fields (states, labels, strings, etc.) explicit.

		* Changes for the 3rd parameter (CAESAR_MARK_SIZE)

		From now on, the parameter CAESAR_MARK_SIZE is declared of
		type CAESAR_TYPE_AREA_1 instead of CAESAR_TYPE_NATURAL. In
		most cases, this change should be upward compatible. However,
		we strongly advise users of the "table_1" library to examine
		every call to CAESAR_CREATE_TABLE_1() and to update the actual
		values supplied for the CAESAR_MARK_SIZE parameter: instead
		of a mere natural number, the actual value should be formed
		using the appropriate primitives provided by the "area_1"
		library. These primitives allow to specify memory alignment
		constraints for the mark field and to make special cases of
		mark fields (states, labels, strings, etc.) explicit.

		* Changes for the 7th parameter (CAESAR_COMPARE)

		A new type CAESAR_TYPE_COMPARE_FUNCTION_TABLE_1 was added to
		"caesar_table_1.h". This new type is used to declare the 7th
		parameter of CAESAR_CREATE_TABLE_1(), which is now declared as
		   CAESAR_TYPE_COMPARE_FUNCTION_TABLE_1 CAESAR_COMPARE;
		instead of
		   CAESAR_TYPE_BOOLEAN (*CAESAR_COMPARE)(CAESAR_TYPE_POINTER,
		   CAESAR_TYPE_POINTER)
		Both forms are equivalent from a type-checking point of view.
		Additionally, the semantics of CAESAR_CREATE_TABLE_1() was
		modified in the case where CAESAR_COMPARE is NULL. Formerly,
		in such case, a NULL value of CAESAR_COMPARE was replaced by
		CAESAR_COMPARE_STATE() provided that the memory size of the
		base field was equal to CAESAR_SIZE_STATE(), otherwise a
		run-time error would occur. From now on, a NULL value of
		CAESAR_COMPARE() is replaced by a default function determined
		by the CAESAR_USE_COMPARE_FUNCTION_AREA_1() of the "area_1"
		library. The explanations regarding the CAESAR_COMPARE
		parameter in the "table_1" manual page have been simplified
		accordingly.

		* Changes for the 8th parameter (CAESAR_HASH)

		The 8th parameter of CAESAR_CREATE_TABLE_1() is now declared
		as
		   CAESAR_TYPE_HASH_FUNCTION CAESAR_HASH;
		where the type CAESAR_TYPE_HASH_FUNCTION is defined as
		   typedef CAESAR_TYPE_NATURAL (*CAESAR_TYPE_HASH_FUNCTION)
		   (CAESAR_TYPE_POINTER, CAESAR_TYPE_NATURAL);
		instead of
		   CAESAR_TYPE_NATURAL (*CAESAR_HASH) (CAESAR_TYPE_POINTER,
		   CAESAR_TYPE_NATURAL, CAESAR_TYPE_NATURAL);
		Both forms are *not* equivalent from a type-checking point of
		view, since from now on, CAESAR_HASH() has only 2 parameters
		whereas it had 3 parameters previously. This change was needed
		to give a uniform profile to hash functions throughout all
		OPEN/CAESAR APIs. Therefore, from now on, one should no longer
		use for the CAESAR_HASH parameter certain functions of the
		"hash" library, such as CAESAR_0_HASH(), CAESAR_1_HASH(), etc.
		However, the new version of the "table_1" library tries to
		provide some (limited) upward compatibility by detecting when
		certain functions with 3 parameters are used, in which case the
		missing parameter is supplied automatically. However, relying
		on this undocumented feature is not recommended, as it could
		disappear from further versions of CADP.

		Additionally, the semantics of CAESAR_CREATE_TABLE_1() was
		modified in the case where CAESAR_HASH is NULL. Formerly,
		in such case, a NULL value of CAESAR_HASH was replaced by
		CAESAR_HASH_STATE() provided that the memory size of the
		base field was equal to CAESAR_SIZE_STATE(), otherwise a
		run-time error would occur. From now on, a NULL value of
		CAESAR_HASH() is replaced by a default function determined
		by the CAESAR_USE_HASH_FUNCTION_AREA_1() of the "area_1"
		library. The explanations regarding the CAESAR_HASH parameter
		in the "table_1" manual page have been simplified accordingly.

		* Changes for the 9th parameter (CAESAR_PRINT)

		A new type CAESAR_TYPE_PRINT_FUNCTION_TABLE_1 was added to
		"caesar_table_1.h". This new type is used to declare the 9th
		parameter of CAESAR_CREATE_TABLE_1(), which is now declared as
		   CAESAR_TYPE_PRINT_FUNCTION_TABLE_1 CAESAR_PRINT;
		instead of
		   void (*CAESAR_PRINT) (CAESAR_TYPE_FILE,
		   CAESAR_TYPE_POINTER);
		Both forms are equivalent from a type-checking point of view.
		Additionally, the semantics of CAESAR_CREATE_TABLE_1() was
		modified in the case where CAESAR_PRINT is NULL. Formerly,
		in such case, a NULL value of CAESAR_PRINT was replaced by
		CAESAR_PRINT_STATE() provided that the memory size of the
		base field was equal to CAESAR_SIZE_STATE(), otherwise a
		run-time error would occur. From now on, a NULL value of
		CAESAR_PRINT() is replaced by a default function determined
		by the CAESAR_USE_PRINT_FUNCTION_AREA_1() of the "area_1"
		library; this function will print both the base field and
		the mark field (if not empty) whereas the mark field was
		never displayed formerly. The explanations regarding the
		CAESAR_PRINT parameter in the "table_1" manual page have
		been simplified accordingly.

		* Changes for the 10th parameter (CAESAR_OVERFLOW):

		A new type CAESAR_TYPE_OVERFLOW_FUNCTION_TABLE_1 was added to
		"caesar_table_1.h". This new type is used to declare the 10th
		parameter of CAESAR_CREATE_TABLE_1(), which is now declared as
		   CAESAR_TYPE_OVERFLOW_FUNCTION_TABLE_1 CAESAR_OVERFLOW;
		instead of
		   void (*CAESAR_OVERFLOW) ();
		Both forms are equivalent from a type-checking point of view.
		The explanations regarding the CAESAR_OVERFLOW parameter in
		the "table_1" manual page have been simplified.

		* Changes for the memory structure of table_1 items:

		From now on, padding bytes are automatically inserted before
		and after the mark field, so that base fields and mark fields
		are always properly aligned with respect to their alignments
		constraints specified using the 2nd and 3rd parameters of
		CAESAR_CREATE_TABLE_1(). This changes a fundamental invariant
		of the "table_1": the base field and mark field are no longer
		concatenated, meaning that there may be extra bytes between
		the last byte of the base field and the first byte of the mark
		field. The CAESAR_RETRIEVE_B_M_TABLE_1() function can be used
		to access the mark field. Unfortunately, this change is *not*
		upward compatible, so that user programs using the "table_1"
		might need to be modified appropriately.

		* Other changes:

		The manual page for caesar_table_1 (which is part of the
		OPEN/CAESAR reference manual in $CADP/doc/*/Garavel-92-a.*)
		was updated (and simplified) to reflect all these changes.

		The "upc" command was modified to remind the users that calls
		to function CAESAR_CREATE_TABLE_1() might have to be adapted.

		All the CADP tools using the "table_1" library have been
		updated to integrate these evolutions.

BUG FIX
Number:		971
Date: 		Tue Dec 14 14:10:52 MET 2004
Author:		Frederic Lang (INRIA/VASY)
Files:		com/exp2fc2

Nature:		A minor bug in the EXP2FC2 script, which impacted SVL, was
		fixed.

BUG FIX
Number:		972
Date: 		Wed Dec 15 09:41:06 MET 2004
Report:		Tomas Barros (INRIA/OASIS, Sophia Antipolis, France)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c

Nature:		If a label in an LTS of the input composition expression would
		contain special characters, e.g., '"', '%', '\', etc., the C
		program generated by exp2c would contain errors. This problem
		was solved.

IMPROVEMENT
Number:		973
Date: 		Wed Dec 15 11:21:59 MET 2004
Report:		Tomas Barros (INRIA/OASIS, Sophia Antipolis, France)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c

Nature:		The EXP.OPEN tool now issues a warning message when the
		synchronization of a set of LTSs through a respective set of
		gates (or labels, depending on the semantics of the parallel
		composition operator considered) cannot ever happen because 
		one of the LTSs does not contain a transition with the 
		appropriate gate (or label).

IMPROVEMENT
Number:		974
Date: 		Wed Dec 15 16:15:30 MET 2004
Authors:	Hubert Garavel (INRIA/VASY), Holger Hermanns (Saarland Univ.,
		Germany), Christophe Joubert (INRIA/VASY), Frederic Lang
		(INRIA/VASY), Radu Mateescu (INRIA/VASY)
Files:		bin.*/determinator.a, man/*/determinator.*

Nature:		A new tool named DETERMINATOR was added to the CADP toolbox.
		This tool provides determinization features for both ordinary
		LTSs and extended Markovian models containing ordinary,
		probabilistic and/or stochastic transitions.

BUG FIX
Number:		975
Date: 		Thu Dec 16 11:01:51 MET 2004
Report:		Thierry Heuillard (France Telecom R&D)
Author:		Wendelin Serwe (INRIA/VASY)
Files:		bin.win32/tgv.a

Nature:		A bug was fixed in the Windows version of TGV: TGV would stop
		with a segmentation fault after displaying the two lines:
		  > SP initialisation
		  >   - SPEC initialised
		This problem did not occur on Solaris nor Linux.

IMPROVEMENT
Number:		976
Date: 		Thu Dec 16 11:09:04 MET 2004
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		bin.*/tgv.a, man/*/tgv.*

Nature:		Various improvements were brought to the TGV tool:
		- It was ported to MacOS X.
		- It now accepts hiding files with ".hid" suffix (in addition
		  to ".hide").
		- It now accepts renaming files with ".ren" suffix (in addition
		  to ".rename").
		- The manual page was corrected in several places. Especially,
		  it now makes clear that one should use "-bcg -unparse"
		  options instead of "-aldebaran -unparse".

IMPROVEMENT
Number:		977
Date:		Fri Dec 17 16:41:38 MET 2004
Authors:	Nicolas Descoubes, Hubert Garavel, Frederic Lang, Bruno Ondet,
		and Gordon Pace (INRIA/VASY)
Files:		bin.*/projector.a, man/*/projector.*

Nature:		The PROJECTOR 1.0 tool was replaced by a new version 2.0,
		which introduces the following changes and improvements:

		- PROJECTOR 2.0 is more efficient than PROJECTOR 1.0. Speedups
		  of up to 4 times have been observed.

		- Synchronisation sets can now be specified using regular 
		  expressions, and using complementation ("all but" operator).

		- New options ("-gate", "-total", and "-partial") allow to
		  specify whether the regular expressions contained in 
		  synchronisation sets must be interpreted as gates, full 
		  labels, or label substrings.

		- The new "-monitor" option allows to open a graphical window
		  to get real-time monitoring information, such as number of
		  states and transitions generated, labels encountered, etc.

		- PROJECTOR 2.0 is fully compatible with PROJECTOR 1.0, except
		  that interfaces files must now be given in the BCG format,
		  while PROJECTOR 1.0 required the ".aut" format. However,
		  when SVL is used, it will perform such file format
		  conversions automatically whenever necessary.

IMPROVEMENT
Number:		978
Date: 		Fri Dec 17 17:01:54 MET 2004
Report:		Frederic Tronel (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard, man/*/svl.*

Nature:		SVL was enhanced to support the new PROJECTOR 2.0 tool:

		- Following the recent evolution of the PROJECTOR tool, the
		  SVL language was extended to allow abstractions with
		  synchronization on the complement of a set ("sync all but"),
		  and synchronization on labels and gates specified as regular
		  expressions ("gate", "total", and "partial" abstractions).

		- A new notation was introduced to enable the description of
		  label lists and renaming rule lists using shell variables
		  in hide, rename, abstraction, parallel composition, and
		  LOTOS process invocations.

IMPROVEMENT
Number:		979
Date: 		Fri Dec 17 17:13:40 MET 2004
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/libcaesar.a, incl/caesar_solve_1.h,
		man/*/caesar_solve_1.*, doc/*/Garavel-92-a.*

Nature:		The OPEN/CAESAR environment was enhanced with a new generic
		library (named CAESAR_SOLVE_1) for solving boolean equation
		systems on the fly. A manual page for this library (23 pages)
		was written.

IMPROVEMENT
Number:		980
Date: 		Fri Dec 17 18:39:55 MET 2004
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/bisimulator.a, man/*/bisimulator.*

Nature:		A new tool named BISIMULATOR was added to the CADP toolbox.
		This tool allows to check equivalence and preorder relations
		between LTSs on the fly.

IMPROVEMENT
Number:		981
Date: 		Mon Dec 20 15:24:47 MET 2004
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard, man/man.*/svl.*

Nature:		SVL was extended to support the new BISIMULATOR tool. From
		now on, BISIMULATOR becomes the default tool (in place of
		ALDEBARAN) for comparing LTSs and behaviours. As BISIMULATOR
		works on-the-fly, the default comparison method is now "fly"
		instead of "std". 

IMPROVEMENT
Number:		982
Date: 		Tue Dec 21 09:47:41 MET 2004
Authors:	Hubert Garavel (INRIA/VASY), Holger Hermanns (Saarland Univ.,
		Germany), and Christophe Joubert (INRIA/VASY)
Files:		demos/demo_30

Nature:		A new demo (Markovian analysis of the Hubble space telescope)
		was added to the CADP toolbox.

IMPROVEMENT
Number:		983
Date: 		Tue Dec 21 12:09:38 MET 2004
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard

Nature:		SVL now generates extended ".exp" files containing generalized
		hiding and renaming operators (thus allowing "hide all but"
		constructs and different matching semantics to be used inside
		".exp" files). Such ".exp" files are accepted by EXP.OPEN 2.0.
		This modification has the advantage to avoid the generation
		of intermediate BCG graphs.

		At the same time, on-the-fly reduction of ".exp" files using
		ALDEBARAN has been removed from SVL, for the following
		reasons:

		- ALDEBARAN cannot process these extended ".exp" files;

		- On-the-fly reduction is generally slower than standard
		  reduction;

		- On-the-fly reduction does not bring the usual advantages
		  of on-the-fly verification, namely the ability to provide
		  verification verdicts without exploring the entire state
		  space.

		As a consequence, the four shell variables predefined in SVL
		DEFAULT_REDUCTION_TOOL_LTS, DEFAULT_REDUCTION_TOOL_EXP,
		DEFAULT_REDUCTION_METHOD_LTS, and DEFAULT_REDUCTION_METHOD_EXP
		have been replaced by the variables DEFAULT_REDUCTION_TOOL
		and DEFAULT_REDUCTION_METHOD. Warning messages are issued at
		reduction time if one of the former variables is defined.

		Equivalence and preorder checking of ".exp" files using the
		ALDEBARAN tool is still supported in SVL. However, such ".exp"
		files should neither contain hiding nor renaming operators
		(because ALDEBARAN does not handle them properly). Otherwise,
		an error message is emitted. In general, the (more efficient)
		BISIMULATOR tool should be preferred, as it accepts any LTS
		given using the OPEN/CAESAR "graph module" API, including
		enhanced ".exp" files.

IMPROVEMENT
Number:		984
Date: 		Tue Jan  4 18:26:15 MET 2005
Authors:	Christophe Joubert and Radu Mateescu (INRIA/VASY)
Files:		doc/*/Joubert-Mateescu-04.*, doc/*/Joubert-Mateescu-05.*,
		doc/=READ_ME.txt, doc/biblio.bib

Nature:		Two new papers were added in the "doc" directory of the CADP
		toolbox:
		- The paper "Joubert-Mateescu-04" describes a method for
		  distributed on-the-fly equivalence checking.
		- The paper "Joubert-Mateescu-05" presents a distributed
		  on-the-fly resolution algorithm for single block boolean
		  equation systems.

BUG FIX
Number:		985
Date: 		Thu Jan  6 14:04:27 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c

Nature:		A table overflow error was corrected in EXP.OPEN 2.0, which 
		sometimes caused erroneous results when the graph module
		explored by EXP.OPEN 2.0 contained less labels than one of
		the input graphs.

BUG FIX
Number:		986
Date: 		Thu Jan  6 15:19:43 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel

Nature:		A bug was corrected in SVL, which caused erroneous expansion 
		of the "leaf reduction" macro operator.

BUG FIX
Number:		987
Date: 		Mon Jan 10 17:00:53 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, svl/src/standard, man/*/svl.*

Nature:		Three minor bugs were corrected in SVL:

		- Cleaning after macro operator expansion no longer removes
		  "generation" operators when their operand is a "rename"
		  expression (such a "rename" operator may now be part of a
		  ".exp" file).

		- The temporary BCG file containing the LTS generated from
		  a ".exp" file is now given a new file name (previously,
		  its name was the same as the ".exp" file by replacing the
		  ".exp" suffix with a ".bcg" suffix). This new scheme avoids
		  clashes between file names.

		- The SVL_SYNC_TO_HIDE() function defined in "svl/src/standard"
		  was corrected to take into account the fact that ".sync"
		  files may now be begin with either the "Sync" or "sync"
		  keywords.

BUG FIX
Number:		988
Date: 		Mon Jan 10 17:18:54 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c

Nature:		A minor bug was corrected in EXP.OPEN, which caused a warning
		message when compiling the C code generated by EXP2C.

BUG FIX
Number:		989
Date: 		Mon Jan 17 16:50:11 MET 2005
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		com/tst

Nature:		The "tst" shell-script was modified not to emit a spurious
		warning "*** No license exists for host ..." when the current
		host name appears to be suffixed by its domain name (for
		instance, "cadp.inria.fr" instead of "cadp").

IMPROVEMENT
Number:		990
Date: 		Mon Jan 24 16:53:29 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard, man/*/svl.*

Nature:		The SVL tool has been enhanced with a new "refined abstraction"
		operator. This operator allows to restrict a behaviour within
		a parallel composition expression (among other operators) with
		respect to constraints induced by synchronization with some of
		its concurrent neighbours. Compared to normal "abstraction",
		the user does not need to provide a synchronization set, as
		this set will be built automatically using EXP.OPEN. As a
		consequence, the synchronization constraints computed in such
		a way are more precise.

IMPROVEMENT
Number:		991
Date: 		Thu Jan 27 16:33:43 MET 2005
Authors:	Damien Bergamini, Adrian Curic, Nicolas Descoubes,
		Hubert Garavel, Christophe Joubert, Radu Mateescu,
		Irina Smarandache-Sturm, and Gilles Stragier (INRIA/VASY)
Files:		bin.*/distributor.a, bin.*/bcg_merge,
		src/monitor/READ_ME, src/monitor/distributor.tcl,
		man/*/distributor.*, man/*/bcg_merge.*

Nature:		Two new tools named DISTRIBUTOR and BCG_MERGE have been added
		to the CADP toolbox. These tool allow distributed state space
		generation on a network of workstations or a cluster of PCs.

IMPROVEMENT
Number:		992
Date: 		Tue Feb  1 15:11:24 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard, man/*/svl.*

Nature:		The semantics of SVL meta-operations, in particular "leaf" and
		"node reduction", was improved. Expansion of these operations
		now distributes "reduction" across "generation", "abstraction",
		and "refined abstraction". The cleaning function was also
		modified accordingly.

		Additionally, "node reduction" now distributes hiding operators
		as far as possible towards the leaves, in order to allow better
		reductions of intermediate state spaces.

IMPROVEMENT
Number:		993
Date: 		Tue Feb  1 16:16:55 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c, com/exp.open, man/*/exp.open.*

Nature:		A new "-labels" option was added to EXP.OPEN. Given as input
		a network of communicating automata (".exp" file), this option
		displays on the standard output all labels that might occur
		in the LTS generated from this network, assuming that all
		the synchronizations are possible.

IMPROVEMENT
Number:		994
Date: 		Wed Feb  2 08:39:35 MET 2005
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/evaluator.*, man/*/evaluator.*

Nature:		An enhanced version of the EVALUATOR on-the-fly model checker
		was installed in the CADP toolbox. The new version 3.5 of
		EVALUATOR supersedes the former version 3.0 still remaining
		fully compatible with it. The main differences between both
		versions are the following:

		- EVALUATOR 3.5 uses the resolution algorithms provided by
		  the CAESAR_SOLVE library (see item #979 above) whereas
		  EVALUATOR 3.0 contained an ad hoc resolution engine. This
		  improves the modularity by clearly separating the
		  translation of the verification problem (done in EVALUATOR)
		  from the resolution (done in CAESAR_SOLVE).	

		- The analysis of regular alternation-free mu-calculus 
		  formulas is enhanced with the detection of formulas that
		  lead to disjunctive or conjunctive boolean equation systems.
		  These systems can be solved more efficiently using algorithm
		  A4 of CAESAR_SOLVE, which does not keep in memory the
		  dependencies between boolean variables. Since most of the
		  formulas encountered in practice are of this type, this
		  enhancement results in important memory reductions
		  (proportional to the number of transitions in the graph
		  under verification) w.r.t. EVALUATOR 3.0.

		- Another optimization, performed on the system of modal
		  equations used as intermediate representation by EVALUATOR,
		  consists in expanding on-line the propositional variables
		  that occur only once in the right-hand side of an
		  equation. On most practical examples, this reduces by a
		  factor of 3 the number of variables and induces the same
		  reduction on the time and memory necessary for resolution.

		- The generation of diagnostics (examples and counterexamples)
		  is improved in order to reflect more accurately the
		  structure of the temporal formulas. In the diagnostics
		  produced by EVALUATOR 3.0, each state was associated to a
		  state of the graph being checked, which caused the
		  duplication of transitions in the diagnostic. For instance,
		  when evaluating the formula ``<A.A.A> true'' on the graph
		  consisting of a single A-loop ``S --A--> S'', the diagnostic
		  produced by EVALUATOR 3.0 was the graph with a single state
		  S and three A-loop transitions attached to S. To the
		  contrary, the diagnostics produced by EVALUATOR 3.5 is the
		  sequence ``S1 --A--> S2 --A--> S3 --A--> S4'', which is a
		  better explanation that the formula requires to traverse
		  three successive A-transitions.

		- Several new command-line options were added to EVALUATOR 3.5
		  to benefit from all features of CAESAR_SOLVE, namely: use of
		  the breadth-first search based algorithm A2 to produce 
		  small-depth diagnostics ("-bfs" option, with its dual "-dfs"
		  option), use of the memory-efficient algorithm A3 to check
		  properties on acyclic graphs ("-acyclic"), and possibility
		  to display the underlying boolean equation system in a
		  textual form ("-bes").

		Also, the manual page for EVALUATOR was updated. 

IMPROVEMENT
Number:		995
Date: 		Thu Feb 10 11:13:57 MET 2005
Report:		Tomas Barros (INRIA/OASIS, Sophia-Antipolis, France)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		bin.iX86/*

Nature:		The CADP binaries have been ported to Linux Fedora Core 3
		(they no longer make a segmentation fault error when being
		run on this recent version of Linux).

IMPROVEMENT
Number:		996
Date: 		Fri Feb 11 16:44:38 MET 2005
Author:		Frederic Lang and Radu Mateescu (INRIA/VASY)
Files:		bin.*/bisimulator.a, man/*/bisimulator.*, bin.*/svl_kernel,
		src/svl/standard, man/*/svl.*

Nature:		The BISIMULATOR tool was enhanced with comparisons modulo two
		new equivalence relations and their associated preorders:
		trace equivalence (option "-trace") and weak trace equivalence
		(option "-weaktrace"), which considers only visible
		transitions. The generation of counterexamples for these
		equivalences and their preorders was also implemented.

		These equivalence relations have been also added to the SVL
		language. They are implemented as follows:

		- Comparisons modulo these equivalences are done by invoking
		  BISIMULATOR with options "-trace" and "-weaktrace".

		- Reductions modulo these equivalences are done in two steps. 
		  First, DETERMINATOR is invoked to eliminate non-determinism
		  (and, for weak trace reduction only, tau-transitions using
		  the "-tauclosure" option). Second, BCG_MIN is used to merge
		  equivalent states modulo strong bisimulation.

IMPROVEMENT
Number:		997
Date: 		Wed Feb 16 14:24:08 MET 2005
Report:		Samson Bisaro (Universite Henri Poincare, Nancy, France)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		com/tst

Nature:		The "tst" shell-script was enhanced to detect whether the
		GR-security extensions are installed in the Linux kernel
		and, if so, to emit a warning message (as the CADP tools may
		face problems in this case). The "tst" shell-script was also
		enhanced to identify Fedora Core distributions and to display
		their version number.

IMPROVEMENT
Number:		998
Date: 		Fri Feb 18 11:47:45 MET 2005
Authors:	Hubert Garavel (INRIA/VASY), Holger Hermanns (Saarland Univ.),
		Radu Mateescu (INRIA/VASY), Christophe Joubert (INRIA/VASY),
		and David Champelovier (INRIA/VASY)
Files:		demos/demo_31

Nature:		A new demo example (SCSI-2 bus arbitration protocol) was
		added. This demo illustrates major topics, such as formal
		modelling of hardware protocols, compositional state space
		generation, model checking of mu-calculus formulas, and
		performance evaluation combined with functional verification.
		This demo example is presented in an FME'02 paper by Garavel
		and Hermanns (see doc/*/Garavel-Hermanns-02.pdf).

IMPROVEMENT
Number:		999
Date: 		Fri Feb 18 12:04:16 MET 2005
Author:		Radu Mateescu (INRIA/VASY)
Files:		demos/demo_34

Nature:		A new demo (Computer Integrated Manufacturing architecture)
		was added to the CADP toolbox.

BUG FIX
Number:		1000
Date: 		Tue Feb 22 17:26:15 MET 2005
Report:		Christophe Joubert (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/bcg_info

Nature:		A bug was fixed in BCG_INFO. Due to a numerical overflow,
		BCG_INFO could abort with a segmentation fault when invoked
		on large models with its "-nondeterministic" option, as in:
		   bcg_info -nondeterministic - vasy_6020_19353.bcg
		where vasy_6020_19353.bcg is an element of the VLTS benchmark
		suite.

BUG FIX
Number:		1001
Date: 		Wed Feb 23 11:01:23 MET 2005
Authors:	Frederic Perret and David Champelovier (INRIA/VASY)
Files:		bin.*/ocis.a

Nature:		Many issues have been fixed in the OCIS simulator:

		- The new version of OCIS correctly displays deadlock states.

		- The menus of OCIS' main window have been improved.

		- When EXHIBITOR is running, the "OK" button of the OCIS
		  window from which EXHIBITOR was launched is desactivated,
		  so that two instances of EXHIBITOR cannot be launched at
		  the same time.

		- The BCG files containing the scenarios stored by OCIS have
		  been made smaller: they no longer contain so-called
		  "unexplored" transitions; this change is upward compatible
		  in the sense that the new version of OCIS can reload the
		  scenarios stored by both the old and new version of OCIS. 

		- The file selection window was improved in several ways: all
		  clicks on the "Save" button are now ignored until a file
		  name is selected; when a scenario save operation fails
		  (i.e., because the current directory or the BCG file is
		  write-protected), the interface now reacts properly;
		  navigation in directories now works correctly when loading
		  and saving scenarios, sequence files, PostScript files,
		  etc.; when saving a PostScript file, a ".ps" suffix is now
		  added automatically if not already present; when saving a
		  sequence tree, a ".seq" suffix is now added automatically
		  if not already present; when quitting, OCIS no longer
		  proposes to store the current scenario if this one is
		  unmodified.

BUG FIX
Number:		1002
Date: 		Thu Feb 24 13:01:12 MET 2005
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.*/ocis.a

Nature:		More improvements have been brought to the OCIS simulator:

		- A bug was fixed: when launching EXHIBITOR from OCIS on a
		  ".seq" file several times, the first launch would execute
		  properly, but the next launches would face an issue: the
		  pathname of the ".seq" file was an absolute one, which
		  prevented to start a new search; from now on, only the
		  basename of this file is displayed, which solves the
		  problem.

		- OCIS was ported to MacOS X. A bug was fixed in the MacOS X
		  version of OCIS: the communication protocol between C and
		  Tcl would emit error messages of the form "Wrong parameter
		  format".

		- On MacOS X, the "$CADP/src/com/cadp_x11" script is now
		  invoked automatically, so as to start the X11 environment
		  if not already running.

BUG FIX
Number:		1003
Date: 		Thu Feb 24 16:23:25 MET 2005
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		bin.*/libcaesar.a, man/*/caesar_hash.*, doc/*/Garavel-92-a.*

Nature:		The "hash" library of OPEN/CAESAR was enhanced in several
		ways:

		- The CAESAR_1_HASH() function was modified so as to return
		  the same results as the s_hash() function of SPIN when
		  given identical input parameters.

		- The CAESAR_1_HASH() function was corrected so that it no
		  longer reads bytes outside of the memory zone to be hashed.

		- The CAESAR_2_HASH() function was modified so as to return
		  the same results as the d_hash() function of SPIN when
		  given identical input parameters.

		- The CAESAR_2_HASH() function was corrected so that it no
		  longer reads bytes outside of the memory zone to be hashed.

		- The CAESAR_6_HASH() function was entirely rewritten; the
		  previous version could cause a segmentation fault error
		  and could return different results depending on the memory
		  alignment of the memory zone to be hashed.

		- Three new functions CAESAR_7_HASH(), CAESAR_STATE_7_HASH(),
		  and CAESAR_LABEL_7_HASH() have been added. These functions
		  are inspired from those of Bob Jenkins in SPIN 4.2.2.

BUG FIX
Number:		1004
Date: 		Fri Feb 25 14:10:06 MET 2005
Report:		Benjamin Fontan (ENSICA, Toulouse, France)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.iX86/*

Nature:		A license problem with Linux laptops was solved. This problem
		occurred when these laptops were booted on a local area 
		network and then disconnected from the network, or vice-versa.

IMPROVEMENT
Number:		1005
Date: 		Mon Feb 28 19:04:47 MET 2005
Authors:	Frederic Lang, Radu Mateescu, and Hubert Garavel (INRIA/VASY)
Files:		demos/demo_01, demos/demo_02, demos/demo_03, demos/demo_07,
		demos/demo_08, demos/demo_09, demos/demo_10, demos/demo_11,
		demos/demo_14, demos/demo_16, demos/demo_17, demos/demo_20,
		demos/demo_24, demos/demo_25, demos/demo_26, demos/demo_28,
		demos/demo_29, demos/demo_32, demos/demo_33

Nature:		Many CADP demos have been adapted to use the new BISIMULATOR
		tool rather than ALDEBARAN. This was done by modifying the
		"=READ_ME.txt" and "demo.svl" files only.

IMPROVEMENT
Number:		1006
Date: 		Thu Mar  3 12:32:49 MET 2005
Authors:	Damien Bergamini, Hubert Garavel, and Radu Mateescu
		(INRIA/VASY)
Files:		src/eucalyptus

Nature:		The EUCALYPTUS user-interface was updated so as to reflect
		the recent evolutions of CADP:

		- In the  "Options" menu, a "Bisimulator" entry was added,
		  which allows to enable the "-stat" option of BISIMULATOR
		  and to choose the name of the Boolean Equation System
		  file produced by BISIMULATOR.

		- In the "CAESAR and CAESAR.ADT" sub-menu of the "Options"
		  menu, the semantics of "Optimization E7" was modified to
		  take into account the changes in the "-e7" option of
		  CAESAR (see above item #926).

		- In the contextual menu for ".lotos" and ".LOTOS" files, a
		  "Compare" entry was added, which invokes BISIMULATOR.

		- In the contextual menu for ".bcg" files, an "Evaluate
		  performance..." entry was added, which invokes the
		  BCG_STEADY and BCG_TRANSIENT tools.

		- The "Help" menu of EUCALYPTUS was updated with the new
		  tools recently added in CADP. The help page for the
		  obsolete Des2Aut tool was removed.

BUG FIX
Number:		1007
Date: 		Thu Mar  3 16:14:59 MET 2005
Report:		Ken Turner (University of Stirling, Scotland, UK)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar.adt

Nature:		A bug was fixed in the C code generated by CAESAR.ADT for
		constant operations: when a constant operation F1 was defined
		using a non-constructor operation F2, and when the definition
		of F2 contained an occurrence of some other constant operation
		F3, a dependence between F1 and F3 would exist. From now on,
		CAESAR.ADT properly detects the existence of "recursive"
		constants (e.g., when F1 and F3 are identical) and rejects them
		with an explicit error message. Also, the C code generated by
		CAESAR.ADT now properly orders the definitions of constants
		to avoid using a constant before it is assigned.

IMPROVEMENT
Number:		1008
Date: 		Thu Mar  3 17:28:39 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard, man/*/svl.*

Nature:		To compute the graph of a parallel composition expression,
		SVL may now automatically use the partial order reduction
		features of EXP.OPEN ("-branching" and "-ratebranching"
		options). The use of partial order reduction depends on
		the context in which the parallel composition expression
		occurs:

		- If the parallel composition expression occurs in the
		  context of a "stochastic branching reduction", then the 
		  "-ratebranching" option of EXP.OPEN is used .

		- If the parallel composition expression occurs either in
		  the interface part of an "abstraction" operator, or in
		  the context of a "reduction" or "comparison" modulo an
		  equivalence relation that is weaker or equal to branching
		  equivalence (i.e., observational, tau*.a, safety, or weak
		  trace), then the "-branching" option of EXP.OPEN is used.

IMPROVEMENT
Number:		1009
Date: 		Mon Mar 14 11:24:40 MET 2005
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.win32/libm.a, bin.win32/libcaesar.a, incl/bcg_standard.h
		incl/caesar_system.h, incl/caesar_standard.h,

Nature:		A new include file named "caesar_system.h" was added, which
		gathers OS-specific definitions previously contained in file
		"caesar_standard.h" and "bcg_standard.h", such as system(),
		popen(), and pclose(). On Windows, such functions are no
		longer contained in the "bin.win32/libcaesar.a" library
		(since they are useful to both BCG and OPEN/CAESAR tools) but
		in the `fake' "bin.win32/libm.a" library. This change should
		be transparent to most users.

IMPROVEMENT
Number:		1010
Date: 		Mon Mar 14 12:35:39 MET 2005
Authors:	David Champelovier, Hubert Garavel, and Frederic Lang
		(INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.adt, bin.*/caesar.indent,
		exp2c, mcl_expand, svl_kernel, xtl

Nature:		The CAESAR, CAESAR.ADT, CAESAR.INDENT, EXP2C, MCL_EXPAND, SVL,
		and XTL compilers have been enhanced so as to support 8-bit
		characters in source files.

IMPROVEMENT
Number:		1011
Date: 		Fri Mar 18 11:28:59 MET 2005
Authors:	Frederic Perret, David Champelovier, Radu Mateescu, and
		Hubert Garavel (INRIA/VASY)
Files:		bin.*/ocis.a

Nature:		The OCIS interactive simulator was improved: from now on, it
		can re-read a simulation scenario contained in a BCG graph and
		reply this scenario during the current simulation session.
		Typically, the BCG graph can be either a simulation scenario
		previously explored and saved using OCIS, or an execution
		trace produced by EXHIBITOR or EXECUTOR, or a diagnostic
		generated by EVALUATOR for a temporal logic property. To do
		so, OCIS needs to decide whether this BCG graph is a subset
		or not of the graph being explored during the current OCIS
		session. This amounts to checking graph inclusion modulo the
		preorder associated to strong equivalence; if so, a diagnostic
		is generated, which can be subsequently read and replayed by
		OCIS as an ordinary simulation scenario. This is done by
		invoking BISIMULATOR and DETERMINATOR from OCIS automatically. 

BUG FIX
Number:		1012
Date: 		Wed Mar 23 11:22:41 MET 2005
Report:		Judi Romijn (Technical Univ. of Eindhoven, The Netherlands)
Author:		David Champelovier (INRIA/VASY)
Files:		src/monitor/distributor.tcl

Nature:		A bug was fixed in the real-time monitoring window of the
		DISTRIBUTOR tool (this window is created by giving the
		"-monitor" option to DISTRIBUTOR). On large examples,
		DISTRIBUTOR could emit the following error messages:
		> bgerror failed to handle background error.
		> Original error: too many nested evaluations (infinite loop?)
		> ... <snip>
		> fatal error on master node (Exit requested by user)
		> Closing pipe to monitor

BUG FIX
Number:		1013
Date: 		Wed Mar 23 11:55:43 MET 2005
Report:		Christophe Joubert (INRIA/VASY)
Author:		David Champelovier (INRIA/VASY)
Files:		src/monitor/distributor.tcl

Nature:		A bug was fixed in the real-time monitoring window of the
		DISTRIBUTOR tool. When the graph under generation became
		large, the progression bars in the "Progress" tab of the
		monitoring window would block after a certain time. This was
		due to an arithmetic overflow problem, which was solved by
		replacing integer numbers with floating-point numbers.  

IMPROVEMENT
Number:		1014
Date: 		Thu Mar 24 10:36:03 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		com/exp.open, bin.*/exp2c, man/*/exp.open.*

Nature:		A new "-info" option was added to the EXP.OPEN tool. This
		option displays information about the LTSs referenced in the
		input composition expression, using the bcg_info tool.

IMPROVEMENT
Number:		1015
Date: 		Thu Mar 24 10:45:40 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		demos/demo_35, demos/demo_36

Nature:		Two new demo examples have been added to the CADP toolbox:
		- demo_35 features a distributed summation algorithm using
		  the "n among m" synchronization operator proposed by
		  H. Garavel and M. Sighireanu in 1999.
		- demo_36 features a distributed Erathostenes sieve, which
		  is verified using compositional verification and partial
		  order reduction

BUG FIX
Number:		1016
Date: 		Thu Mar 24 15:09:39 MET 2005
Report:		Gregory Batt (INRIA Rhone-Alpes/HELIX),
		Ludovic Apvrille (ENST, Sophia-Antipolis, France), and
		Dave Parker (Univ. of Birmingham, UK)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		src/installator/installator.tcl

Nature:		A bug was fixed in the INSTALLATOR assistant, which would
		sometimes freeze when or after performing FTP transfers. In
		the log file, this bug produced the following error message:
		   > too many nested calls to Tcl_EvalObj (infinite loop?)
		   >    (procedure "Trace" line 9)
		   >    invoked from within
		   > ...
		   > "DisplayMsg "C: 421 Service not available, closing
		   > control connection."
		   > ...

BUG FIX
Number:		1017
Date: 		Fri Mar 25 16:06:22 MET 2005
Report:		Gwen Salaun (INRIA/VASY)
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar

Nature:		A bug was fixed in optimization U2 of CAESAR. Under some rare
		circumstances, this optimization could merge two concurrent
		units into one single sequential unit.

IMPROVEMENT
Number:		1018
Date: 		Fri Mar 25 16:46:15 MET 2005
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		incl/caesar_table_1.h, bin.*/libcaesar.a
		man/*/caesar_table_1.* doc/*/Garavel-92-a.*

Nature:		The "caesar_table_1" library of OPEN/CAESAR was modified so
		as to increase its maximal capacity from (2^24)-1 elements up
		to 2^29 elements. This change increases the memory size of a
		table, but in a reasonable manner.
 
		In particular, the constant CAESAR_NULL_INDEX_TABLE_1 was
		modified: its value changed from 16777215 to -1.

		Consequently, all OPEN/CAESAR applications using the include
		file "caesar_table_1.h" should be recompiled to take into
		account the new value of CAESAR_NULL_INDEX_TABLE_1. This
		does not preserve binary compatibility, since a ".o" or ".a"
		file produced with any version of CADP older or equal to
		CADP 2003-y can not be used with the "libcaesar.a" library
		provided in a version of CADP equal or newer to CADP 2003-z.

IMPROVEMENT
Number:		1019
Date: 		Tue Mar 29 19:02:17 MEST 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c

Nature:		The implementation of the CAESAR_ITERATE_STATE() function 
		provided by EXP.OPEN was modified, which reduces execution
		time with a negligible memory overhead. For instance,
		reachability analysis becomes 1.26 times faster for demo_20
		and 1.36 times faster for demo_35.

IMPROVEMENT
Number:		1020
Date: 		Wed Mar 30 09:45:43 MEST 2005
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		bin.win32/*, src/windows/*, src/com/cadp_cc

Nature:		The Windows binaries of CADP tools have been modernized.
		Previously, these binaries were compiled against Microsoft's 
		CRTDLL library, which is now more or less deprecated. From
		now on, these binaries are compiled against Microsoft's MSVCRT
		library. Precisely:
		- The "cadp_cc" shell-script was modified to compile against
		  MSVCRT instead of CRTDLL.
		- The directory "src/windows" was removed.
		- The Mingwin libraries used to compile the CADP tools have
		  been upgraded to mingw-runtime-3.7 and w32api-3.2.

BUG FIX
Number:		1021
Date: 		Tue Apr  5 12:51:09 MEST 2005
Report:		Frederic Lang (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/bcg_edit

Nature:		A bug was fixed in the BCG_EDIT tool. When the environment
		variable $PRINTER would contain white spaces (for instance,
		"Microsoft Office Document Image Writer"), BCG_EDIT would
		emit an error message "test: too many arguments". A similar
		problem was fixed for environment variable $CADP_PS_VIEWER.

IMPROVEMENT
Number:		1022
Date: 		Thu Apr  7 12:22:41 MEST 2005
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		bin.*/caesar.new, doc/*/Garavel-Serwe-04.*

Nature:		A prototype version of CAESAR (named CAESAR.NEW) was added
		to the CADP toolbox. This prototype version implements the
		state space reductions described in a recent paper by Garavel
		and Serwe (see doc/*/Garavel-Serwe-04.*).
		Eventually, the features provided by CAESAR.NEW will be
		integrated into the "official" version of CAESAR. In the
		meantime, it is possible to use CAESAR.NEW in place of CAESAR
		by typing the following shell commands:
		   $ cd $CADP/bin.`$CADP/com/arch`
		   $ mv caesar caesar#6.2
		   $ mv caesar.new caesar

BUG FIX
Number:		1023
Date: 		Wed Apr 13 18:31:25 MEST 2005
Report:		Howard Bowman (University of Kent at Canterbury, UK)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.adt, bin.*/caesar.new

Nature:		Two minor problems were fixed in the C code generated by
		CAESAR and CAESAR.ADT. This C code was not fully compliant to
		ISO C, so that recent C compilers would emit two warnings:
		  > warning: old-style declaration or incorrect type for: main
		and
		  > warning: implicit function declaration: exit

BUG FIX
Number:		1024
Date: 		Fri Apr 15 10:26:04 MEST 2005
Report:		Frederic Lang (INRIA/VASY)
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		src/monitor/distributor.tcl

Nature:		The real-time monitoring window of DISTRIBUTOR (which is
		created using the "-monitor" option of DISTRIBUTOR) did not
		work on Windows. This problem was solved.

BUG FIX
Number:		1025
Date: 		Thu Apr 21 17:29:48 MEST 2005
Report:		Husain Aljazzar (University of Konstanz, Germany),
		Holger Hermanns (Saarland University, Germany)
Author:		David Champelovier (INRIA/VASY)
Files:		bin.*/bcg_transient

Nature:		When invoked with a list of several "time instants" given on
		the command-line, BCG_TRANSIENT could produce incorrect 
		numerical results (transition throughputs) for one or several
		instants located at the end of the list. This issue was fixed.

IMPROVEMENT
Number:		1026
Date: 		Tue May 17 18:11:59 MEST 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		demos/demo_35

Nature:		The demo_35 (distributed summation algorithm) was entirely
		rewritten. The network topology is now properly isolated in
		the data type part (it is defined using a "neighbourhood"
		function).

IMPROVEMENT
Number:		1027
Date: 		Fri May 20 13:33:39 MEST 2005
Author:		Radu Mateescu (INRIA/VASY)
Files:		doc/*/Bergamini-Descoubes-Joubert-Mateescu-05.*

Nature:		A new paper on BISIMULATOR was added to the CADP toolbox.
		In particular, this paper provides a performance comparison
		between ALDEBARAN and BISIMULATOR.

BUG FIX
Number:		1028
Date: 		Wed Jun 22 11:17:14 MEST 2005
Report:		Hubert Garavel (INRIA/VASY)
Author:		David Champelovier (INRIA/VASY)
Files:		bin.*/src/com/cadp_cc

Nature:		Two minor problems were fixed in the Windows version of CADP:
		CAESAR.ADT and CAESAR would regenerate ".h" and ".c" files
		systematically, even if the source LOTOS file did not change.
		This was not time-effective.

		One problem was caused by the stat() function of Mingwin
		that does not recognize Cygwin's mount points, such as the
		fact that "/usr/lib" is mounted on "/lib", and thus would
		conclude that include files located in "/usr/lib" did not
		exist, thus forcing recompilation. This problem was solved
		by modifying the "-datation" option of the "cadp_cc"
		shell-script.

		Another problem was that some error messages of the GCC
		compiler were unduly understood as file dependencies, thus
		forcing recompilation. Again, the "cadp_cc" shell-script was
		corrected.  

IMPROVEMENT
Number:		1029
Date: 		Fri Jun 24 15:41:32 MEST 2005
Report:		Husain Aljazzar (Univ. of Konstanz, Germany)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.new

Nature:		The C code generated by CAESAR using "-open" option was
		slightly modified (namely, the declaration of the functional
		parameter CAESAR_LOOP of function CAESAR_ITERATE_STATE was
		made more accurate) so that this C code can now be processed
		by the "protoize" tool.

IMPROVEMENT
Number:		1030
Date: 		Fri Jun 24 16:04:23 MEST 2005
Authors:	Frederic Lang and Wendelin Serwe (INRIA/VASY)
Files:		bin.*/projector.a

Nature:		The hash function associated to a hash table in PROJECTOR was
		modified to improve its dispersion. This makes PROJECTOR much
		faster when many labels are identical up to character
		permutations.

IMPROVEMENT
Number:		1031
Date: 		Fri Jun 24 16:57:29 MEST 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard

Nature:		SVL now minimizes the interfaces given to the PROJECTOR 2.0
		tool modulo branching bisimulation before safety equivalence,
		so as to minimize large interfaces in a faster way.

IMPROVEMENT
Number:		1032
Date: 		Fri Jun 24 19:23:16 MEST 2005
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.win32/distributor.a

Nature:		A problem was fixed in the Windows version of DISTRIBUTOR.
		When the SFU (Microsoft's Services for Unix) software was
		installed, DISTRIBUTOR would not work properly because the
		Unix commands contained in C:\SFU would take precedence over
		the Unix commands provided by Cygwin. This would generate an
		error message of the form:
		> This command is not supported. Please type help for further
		and DISTRIBUTOR would stop.

IMPROVEMENT
Number:		1033
Date: 		Mon Jul 18 16:34:05 MEST 2005
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		bin.*/caesar.adt, bin.*/caesar, bin.*/caesar.new

Nature:		From now on, when a ".h" file (resp., a ".f" or a ".t" file)
		does not start with the special macro-definition
			#define CAESAR_ADT_EXPERT_H ...
		(resp. CAESAR_ADT_EXPERT_F or CAESAR_ADT_EXPERT_T), CAESAR 
		and CAESAR.ADT will emit a warning that this macro-definition
		is missing. In such case, the default CAESAR.ADT version
		number will be 5.2 instead of 4.1 (which means that one
		assumes that the ".h", ".f", or ".t" file was written for
		version 5.2 of CAESAR.ADT rather than for version 4.1, which
		lasted from 1993).

IMPROVEMENT
Number:		1034
Date: 		Mon Sep  5 16:12:02 MEST 2005
Authors:	Frederic Lang and Hubert Garavel (INRIA/VASY)
Files:		demo_37

Nature:		A new demo example was added: the ODP (Open Distributed
		Processing) trader.

IMPROVEMENT
Number:		1035
Date: 		Tue Sep  6 18:20:19 MEST 2005
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		src/exec_caesar/main.c, demos/demo_19/main.c, 
		demos/demo_19/driver.c, demos/demo_19/gate_functions.c,
		demos/demo_19/start

Nature:		The "main.c" file containing the entry point of EXEC/CAESAR
		was enhanced. The main() function can now accept an optional
		argument that, if present, will be the file name to which the
		transitions will be logged as they are executed. If this
		argument is absent, no logging will take place. If this
		parameter is equal to "-", then logging will take place on the
		standard output.

		The source files of demo_19 were adapted accordingly. The
		"main.c" program of demo_19 was removed, as it is now subsumed
		by the enhanced file "src/exec_caesar/main.c. The "driver.c"
		program and the "start" shell-script were also simplified.
		Finally, file "driver.c" was renamed into "gate_functions.c".

IMPROVEMENT
Number:		1036
Date: 		Wed Sep  7 14:37:13 MEST 2005
Authors:	Frederic Lang, Gwen Salaun and Wendelin Serwe (INRIA/VASY)
Files:		doc/*/Lang-05.*, doc/*/Salaun-Serwe-05.*, doc/=READ_ME.txt,
		doc/biblio.bib

Nature:		Two new papers were added in the "doc" directory of the CADP
		toolbox:
		- The paper "Lang-05" presents the principles and the main
		  functionalities of the EXP.OPEN 2.0 tool.
		- The paper "Salaun-Serwe-05" discusses translation issues
		  between the hardware process algebra CHP and LOTOS.

IMPROVEMENT
Number:		1037
Date: 		Fri Sep  9 17:56:40 MEST 2005
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		incl/caesar_kernel.h, demos/demo_19/gate_functions.c

Nature:		In the standard EXEC/CAESAR include file "caesar_kernel.h",
		four macro definitions have been added:
		  CAESAR_KERNEL_ASSERT_EOL(), CAESAR_KERNEL_ASSERT_INPUT(), 
		  CAESAR_KERNEL_ASSERT_OUTPUT(), CAESAR_KERNEL_ASSERT_TYPE()
		These macros are useful to check the arguments passed to
		EXEC/CAESAR gate functions. The "gate_functions.c" file of
		demo_19 was modified to take advantage of these new macros.

IMPROVEMENT
Number:		1038
Date: 		Fri Sep  9 18:49:56 MEST 2005
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		demos/demo_38

Nature:		A new demo was added: it features the LOTOS description of an
		asynchronous hardware architecture implementing the DES (Data
		Encryption Standard). The demo illustrates two key points:
		the compositional verification of the control part of this
		architecture, and rapid prototyping by C code generation using
		EXEC/CAESAR.

IMPROVEMENT
Number:		1039
Date: 		Mon Sep 12 15:17:16 MEST 2005
Author:		Radu Mateescu (INRIA/VASY)
Files:		demos/demo_39

Nature:		A new demo was added: it features the LOTOS description of a
		turntable system for drilling products. The demo illustrates
		both functional verification (model checking) and performance
		evaluation.

BUG FIX
Number:		1040
Date: 		Mon Sep 12 19:25:04 MEST 2005
Report:		Alexandre Mota (Univ. Federal de Pernambuco, Recife, Brazil)
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/tst

Nature:		On RedHat Linux version 3WS, the "tst" shell-script would emit
		an incorrect warning:
		> *** The CADP software might not work correctly on RedHat 3WS
		> ==> Please upgrade to RedHat 6.0 or higher
		This erroneous message was removed.

BUG FIX
Number:		1041
Date: 		Mon Sep 19 17:45:37 MEST 2005
Report:		Jaco van de Pol (CWI, Amsterdam, The Netherlands)
Author:		Frederic Lang (INRIA/VASY)
Files:		com/exp.open, bin.*/exp2c

Nature:		Two bugs were fixed in Exp.Open:
		- The -mcrl option was not recognized due to a mistake in the
		  "com/exp.open" command.
		- While generating a synchronization label file for Projector
		  ("-interface" option), Exp.Open assumed erroneously that the
		  hidden action was systematically written "i". Thus, when
		  written differently, the hidden action was considered by 
		  Projector as synchronizable, which led to wrong behaviours.

IMPROVEMENT
Number:		1042
Date: 		Thu Sep 22 11:54:27 MEST 2005
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/libcaesar.a, incl/caesar_solve_1.h,
		man/*/caesar_solve_1.*, doc/*/Garavel-92-a.*

Nature:		The interface of the CAESAR_SOLVE library of OPEN/CAESAR was
		enhanced with several new types and functions, which facilitate
		the creation of boolean equation systems:

		- The enumerated type CAESAR_TYPE_BLOCK_SIGN_SOLVE_1 consists
		  of the two constant values
		    CAESAR_MINIMAL_FIXED_POINT_SOLVE_1()
		  and
		    CAESAR_MAXIMAL_FIXED_POINT_SOLVE_1()
		  denoting the sign of an equation block (minimal or maximal
		  fixed point).

		- The enumerated type CAESAR_TYPE_VARIABLE_KIND_SOLVE_1
		  consists of the two constant values
		    CAESAR_DISJUNCTIVE_VARIABLE_SOLVE_1()
		  and
		    CAESAR_CONJUNCTIVE_VARIABLE_SOLVE_1()
		  denoting the kind of a boolean variable (disjunctive or
		  conjunctive).

		- The following types
		    CAESAR_TYPE_BLOCK_SIGN_FUNCTION_SOLVE_1
		    CAESAR_TYPE_VARIABLE_KIND_FUNCTION_SOLVE_1
		    CAESAR_TYPE_AREA_FUNCTION_SOLVE_1
		    CAESAR_TYPE_BOOLEAN_FUNCTION_SOLVE_1
		    CAESAR_TYPE_NATURAL_FUNCTION_SOLVE_1
		  denote pointers to functions with various profiles, which
		  occur as arguments of the CAESAR_CREATE_SOLVE_1() function.

BUG FIX
Number:		1043
Date: 		Fri Sep 23 16:33:51 MEST 2005
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/libcaesar.a

Nature:		A bug was corrected in the breadth-first resolution algorithm
		of the CAESAR_SOLVE library. In some cases, the error caused
		a loss of information in the diagnostic generated by this
		algorithm.

IMPROVEMENT
Number:		1044
Date: 		Tue Sep 27 15:12:55 MEST 2005
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/libcaesar.a,
		man/*/caesar_solve_1.*, doc/*/Garavel-92-a.*

Nature:		A new on-the-fly resolution algorithm, named A5, was added to
		the CAESAR_SOLVE boolean resolution library of OPEN/CAESAR.
		Similarly to algorithm A0 already present in the library,
		algorithm A5 is based upon a depth-first search of the
		dependency graph between boolean variables and is able to
		solve general equation blocks (containing any combinations of
		disjunctions and conjunctions in the right hand sides of the
		equations).

		Algorithm A5 is optimized to perform a faster detection of
		examples (resp. counterexamples) in maximal (resp. minimal)
		fixed point equation blocks. This detection is based upon a
		generalization of Tarjan's algorithm for computing strongly
		connected components.  Algorithm A5 proves to be much faster
		(between one and two orders of magnitude) than all the other
		algorithms of CAESAR_SOLVE when it is invoked many times on
		the same equation block (e.g., for detecting tau-confluent or
		redundant transitions during the on-the-fly reductions).

IMPROVEMENT
Number:		1045
Date: 		Wed Sep 28 12:31:44 MEST 2005
Report:		Tomas Barros (INRIA/OASIS, Sophia-Antipolis, France)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c, man/*/exp.open.*

Nature:		Exp.Open now allows to write labels containing special
		characters, such as double quotes. To this aim, labels may
		contain escape character sequences such as '"' or '',
		following the definition of character constants of the ANSI
		C specification.

IMPROVEMENT
Number:		1046
Date: 		Thu Sep 29 13:30:25 MEST 2005
Report:		Tomas Barros (INRIA/OASIS, Sophia-Antipolis, France)
Author:		Frederic Lang (INRIA/VASY)
Files:		com/exp.open, bin.*/exp2c, man/*/exp.open.*

Nature:		When some LTS of an Exp.Open composition expression was in
		a format other than BCG (i.e., ALDEBARAN, FC2, or SEQ), 
		Exp.Open did translate this LTS into BCG automatically, by
		calling the bcg_io tool. Doing this, labels were parsed as
		explained in the bcg_write manual page. This prevented using
		labels whose syntax does not fulfill the BCG conventions. To
		palliate this limitation, a new -unparse option was added, 
		which turns label parsing off.

IMPROVEMENT
Number:		1047
Date:		Fri Oct  7 13:27:11 MEST 2005
Author:		Gwen Salaun (INRIA/VASY)
Files:		doc/*/Chirichiello-Salaun-05.*

Nature:		A new paper related to the use of CADP for the verification
		of Web services was added to the CADP toolbox. 

BUG FIX
Number:		1048
Date:		Mon Oct 10 10:18:21 MEST 2005
Report:		Radu Mateescu (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		demos/demo_24/demos.svl, demos/demo_31/demo.svl,
		demos/demo_39/demo.svl

Nature:		Three SVL scripts called the SVL_RECORD_FOR_CLEAN() macro
		(defined in "src/svl/standard") using regular expressions as
		arguments, instead of plain filenames as required. This bug
		was fixed.

IMPROVEMENT
Number:		1049
Date: 		Mon Oct 10 16:28:25 MEST 2005
Authors:	Frederic Lang and Radu Mateescu (INRIA/VASY)
Files:		src/open_caesar/reductor.c, src/open_caesar/reductor3.c, 
		bin.*/reductor.a, man/*/reductor.*

Nature:		The new version 4.0 of Reductor was released. The archive file
		"bin.*/reductor.a" of the CADP toolbox replaces the source file
		"src/open_caesar/reductor.c", which was archived in a new file
		named "src/open_caesar/reductor3.c".

		As before, Reductor 4.0 still allows to eliminate all invisible
		transitions on-the-fly (-taustar option) by merging the source
		and target states of every invisible transition. Reductor 4.0
		also has the following new features:

		- In addition to invisible transitions, Reductor 4.0 allows to
		  eliminate also some nondeterministic transitions that are
		  irrelevant as regards safety equivalence (-safety option).

		- Reductor 4.0 allows to compute the minimal quotient of the
		  graph (-minimal option) modulo either strong bisimulation
		  (-strong option), tau*.a bisimulation (-taustar option), and
		  safety equivalence (-safety option). Reductor 4.0 also allows
		  to display the equivalence classes of the quotient (-class
		  option).

		As in Bisimulator, state equivalence checking is implemented
		using the efficient "caesar_solve_1" library (solving Boolean
		Equation Systems). Moreover, the closure algorithm used to 
		eliminate invisible transitions (tau*.a and safety reductions)
		is faster than in earlier versions. 

		The Reductor manual page was updated.

IMPROVEMENT
Number:		1050
Date:		Thu Oct 13 18:05:22 MEST 2005
Authors:	Hubert Garavel, Bruno Ondet, and Wendelin Serwe (INRIA/VASY)
Files:		bin.*/libcaesar.a,
		man/*/caesar_table_1.*, doc/Garavel-92-a.*

Nature:		The implementation of the "table_1" module of the OPEN/CAESAR
		library was enhanced in three ways so as to reduce its memory
		cost (especially for tables containing a little number of
		items):

		- Depending on the size of base fields, the actual value given
		  to the CAESAR_LIMIT_SIZE parameter of CAESAR_CREATE_TABLE_1()
		  (or the default value given to CAESAR_LIMIT_SIZE when the
		  actual value specified by the user is equal to zero) is now
		  decreased automatically if it exceeds the total number of
		  different base fields.

		- Depending on the (possibly decreased) value given to
		  CAESAR_LIMIT_SIZE, the memory cost of the "table_1" was
		  reduced by representing internal memory cells using a
		  variable number of bytes (1, 2, 3 or 4 bytes) instead of a
		  fixed number (4 bytes) as done previously.

		- Depending on the (possibly decreased) value given to
		  CAESAR_LIMIT_SIZE, the actual value given to the
		  CAESAR_HASH_SIZE parameter of CAESAR_CREATE_TABLE_1()
		  (or the default value given to CAESAR_HASH_SIZE when the
		  actual value specified by the user is equal to zero) is now
		  decreased automatically if it exceeds CAESAR_LIMIT_SIZE,
		  i.e., the maximal number of items that can be stored in the
		  table.

		The "caesar_table_1" manual page was updated accordingly.

IMPROVEMENT
Number:		1051
Date:		Wed Oct 19 17:19:55 MEST 2005
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		./bin.*/caesar, ./bin.*/caesar.adt, ./bin.*/caesar.new,
		./com/tst,
		./src/open_caesar/simulator.c, ./src/open_caesar/simulator.i,
		./src/open_caesar/declarator.c, ./src/open_caesar/executor.c,
		./src/open_caesar/generator.c, ./src/open_caesar/predictor.c,
		./src/open_caesar/terminator.c, ./src/open_caesar/reductor3.c,
		./src/open_caesar/generator2.c, ./src/open_caesar/reductor2.c,
		./man/*/caesar_stack_1.*, ./man/*/caesar_standard.*,
		./man/*/bcg_write.*, ./man/*/bcg_read.*,
		./demos/demo_05/user.c, ./demos/demo_05/=READ_ME.txt,
		./demos/demo_12/main.c, ./demos/demo_12/=READ_ME.txt

Nature:		In order to avoid warnings emitted by recent C compilers,
		such as Sun C compiler 5.7 (SunStudio 10), various changes
		have been brought to the CADP source files written in C, as
		well as to the C code generated by CAESAR, CAESAR.ADT, and
		CAESAR.NEW. We can mention the following enhancements:
		- addition of missing #include directives,
		- addition of missing calls to exit(), and
		- addition of "int" result type when declaring the main()
		  function.

IMPROVEMENT
Number:		1052
Date: 		Thu Oct 20 10:42:31 MEST 2005
Report:		Thomas Arts (Computer Science Lab, Ericsson, Sweden),
		Clara Benac Earle (University of Kent at Canterbury, UK),
		Olivier Bonaventure (University of Liege, Belgium),
		Romaric Charton (LORIA, Nancy),
		Wan Fokkink (CWI, Amsterdam, The Netherlands),
		Hubert Garavel (INRIA/VASY),
		Francois Germeau (University of Liege, Belgium),
		Jean-Charles Henrion (University of Liege, Belgium),
		Marc Herbert (INRIA/VASY),
		Guoping Jia (Verimag, Grenoble),
		Frederic Lang (INRIA/VASY),
		Izak van Langevelde (CWI, Amsterdam, The Netherlands),
		Wayne Liu (University of Waterloo, Ontario, Canada),
		Stephane Martin (INRIA/VASY),
		Radu Mateescu (INRIA/VASY),
		Charles Pecheur (INRIA/VASY),
		Wendelin Serwe (INRIA/VASY), and
		Arno Wouters (CWI, Amsterdam, The Netherlands)
Authors:	Frederic Lang and Hubert Garavel (INRIA/VASY)
Files:		bin.*/aldebaran, bin.*/aldebaran.old, com/aldebaran

Nature:		The Aldebaran binary tool (version 6.6) was replaced by the
		new shell-script "com/aldebaran" (version 7.0), which invokes
		the tools Bcg_Info, Bcg_Io, Bcg_Labels, Bcg_Min, Bcg_Open, 
		Bisimulator, Determinator, Evaluator, Exp.Open, Exhibitor,
		Generator, and Reductor. In the same time, the binary files
		"bin.*/aldebaran" corresponding to version 6.6 were renamed
		into "bin.*/aldebaran.old".

		Aldebaran 7.0 may also invoke Aldebaran 6.6, either when the
		new option -old (which must be the first option on the command
		line) is set, or to perform minimization modulo observational
		equivalence and comparison modulo delay equivalence, which are
		not supported by other CADP tools.

		Aldebaran 7.0 fixes 24 out of the 25 known bugs of Aldebaran
		6.6. In addition, Aldebaran 7.0 relaxes the following
		limitations of Aldebaran 6.6:

		- Aldebaran 7.0 accepts as input the full Exp.Open 2.0 
		  language instead of the subset consisting of LOTOS parallel
		  composition and hiding. In particular, the restriction
		  that forbidded hiding operators whose scope does not contain
		  the whole expression is now relaxed.

		- As regards comparison modulo branching bisimulation, 
		  Aldebaran 7.0 does not require anymore that one of the
		  graphs be free of invisible transitions.

		- Comparisons modulo branching and observational preorders 
		  are now supported.

IMPROVEMENT
Number:		1053
Date: 		Fri Oct 28 19:55:44 MEST 2005
Report:		Hubert Garavel (INRIA/VASY)
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/bisimulator.a, man/*/bisimulator.*

Nature:		The counterexamples produced by BISIMULATOR when the two LTSs
		compared are not equivalent were made more readable. Labels of
		error transitions indicating non equivalent states, which
		previously were of the following form:
			"Absent in LTS1: a"
			and
			"Absent in LTS2: b"
		where a (resp. b) is a transition label belonging to the second
		(resp. the first) LTS given as input to BISIMULATOR, were
		respectively changed into:
			"Present in lts2.bcg: a"
			and
			"Absent in lts2.bcg: b"
		where "lts2.bcg" is the name of the BCG file denoting the
		second LTS given as input to BISIMULATOR.

IMPROVEMENT
Number:		1054
Date: 		Mon Nov 21 16:54:06 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/reductor.a, man/*/reductor.*

Nature:		Two new reduction options preserving branching bisimulation 
		were added in Reductor: the "-tauconfluence" option yields a
		graph in which tau-confluence has been eliminated; the 
		"-taucompression" option yields a graph in which every cycle of 
		tau-transitions has been merged into a single state.

BUG FIX
Number:		1055
Date:		Tue Nov 29 16:48:20 MET 2005
Report:		Gwen Salaun (INRIA/VASY)
Author:		Wendelin Serwe (INRIA/VASY)
Files:		bin.*/caesar.indent

Nature:		Two bug fixes and two enhancements were brought to the
		CAESAR.INDENT pretty-printer for LOTOS:

		- CAESAR.INDENT no longer removes white spaces before or
		  after the keywords "accept", "actualizedby", "any", "par",
		  "renamedby", and "using". For instance, "any Bool" is no
		  longer translated into "anyBool".

		- From now on, CAESAR.INDENT handles ".lib" files containing
		  "library"..."endlib" directives (i.e., nested include
		  files). Previously, such directives would cause syntax
		  errors to be reported.
		  
		- From now on, CAESAR.INDENT no longer inserts extra spaces
		  after the ":", "!" and "?" keywords. For instance,
		     G ! 5 ? B : Bool
		  is now formatted as:
		     G !5 ?B:Bool

		- In type definitions, the formatting of "sortnames" clauses,
		  "opnnames" clauses, and "S1 for S2" lists was improved.

IMPROVEMENT
Number:		1056
Date: 		Fri Dec 16 15:11:44 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		com/exp.open, bin.*/exp2c, bin.*/libexp_open.a, 
		man/*/exp.open.*

Nature:		Two new partial order reductions were added to Exp.Open: the 
		"-deadpreserving" option yields a reduced graph that contains
	 	the same deadlock states as the entire graph, and the
		"-weaktrace" option yields a reduced graph that is equivalent
		to the entire graph modulo weak trace equivalence.

BUG FIX
Number:		1057
Date: 		Fri Dec 16 16:30:39 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		demos/demo_04/EXP.t

Nature:		The PRINT_EXP (F, E) function defined in the "EXP.t" file of
		demo_04 was modified to take into account the case where
		E == NULL. This avoid a segmentation fault when invoking
		"reductor -class" on Solaris.

BUG FIX
Number:		1058
Date: 		Fri Dec 16 18:12:58 MET 2005
Author:		Wendelin Serwe (INRIA/VASY)
Files:		bin.*/caesar.indent, man/*/caesar.indent.*

Nature:		Two problems have been fixed in the CAESAR.INDENT tool:
		- When pretty-printing a ".lib" file, a missing "n" is now
		  added at the end of file;
		- The unsecure mktemp() function is no longer invoked; instead
		  the "secure" mkstemp() is now invoked (except on Windows,
		  where this function does not exist in the Mingwin32 API).

IMPROVEMENT
Number:		1059
Date: 		Mon Dec 19 14:21:19 MET 2005
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		incl/caesar_kernel.h

Nature:		A collection of logging macro-definitions was added to the
		EXEC/CAESAR's interface file "caesar_kernel.h".

IMPROVEMENT
Number:		1060
Date: 		Tue Dec 20 11:48:01 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		com/aldebaran, man/*/aldebaran.*

Nature:		The diagnostics issued by the new ALDEBARAN shell-script are
		now stored in file "aldebaran.bcg". This behaviour is coherent
		with respect to other tools such as BISIMULATOR and EVALUATOR,
		which issue diagnostics in files "bisimulator.bcg" and
		"evaluator.bcg", respectively.

BUG FIX
Number:		1061
Date: 		Tue Dec 20 12:56:17 MET 2005
Report:		Hubert Garavel (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard

Nature:		The BCG files containing the diagnostics issued by ALDEBARAN
		were not removed from the directory when calling SVL with
		the -clean option. This problem was solved.

BUG FIX
Number:		1062
Date: 		Tue Dec 20 14:14:11 MET 2005
Author:		Frederic Lang (INRIA/VASY)
Files:		demos/demo_10/demo.svl, demos/demo_11/demo.svl,
		demos/demo_14/demo.svl, demos/demo_37/demo.svl

Nature:		The diagnostics generated by the ALDEBARAN shell-script for
		a livelock detection is a graph that contains cycles. In four
		demo examples, the SVL script stored these diagnostics into
		".seq" files, thus causing an error as these diagnostics are
		not traces. This bug was solved by replacing ".seq" files by
		".bcg" files.

IMPROVEMENT
Number:		1063
Date: 		Thu Dec 22 12:11:02 MET 2005
Authors:	Frederic Lang and Radu Mateescu (INRIA/VASY)
Files:		bin.*/reductor.a, man/*/reductor.*

Nature:		A new "-divergence" option, to be used with "-taucompression",
		was added to REDUCTOR. Instead of full tau-compression, which
		removes every strongly connected component of tau-transitions,
		the new "-divergence" option allows to keep a self-looping 
		tau-transition in place of every strongly connected component
		of tau-transitions, thus preserving the livelocks of the
		original, entire graph.

BUG FIX
Number:		1064
Date: 		Thu Dec 22 16:37:23 MET 2005
Report:		Hubert Garavel (INRIA/VASY)
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/bisimulator.a

Nature:		A bug was fixed in BISIMULATOR's diagnostic generation for
		branching equivalence. In a few cases, some transitions of
		the diagnostic were labelled by invisible actions instead
		of the visible actions occurring in the LTSs being compared.

BUG FIX
Number:		1065
Date: 		Wed Jan  4 11:14:46 MET 2006
Report:		David Champelovier (INRIA/VASY)
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/bisimulator.a

Nature:		Another bug was fixed in BISIMULATOR's diagnostic generation
		for branching equivalence. Because of the bug, BISIMULATOR
		would in some cases abort with a core dump when writing the
		BCG file containing the diagnostic.

IMPROVEMENT
Number:		1066
Date: 		Fri Jan  6 18:29:04 MET 2006
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/bisimulator.a

Nature:		The comparison modulo branching and observational equivalences
		in BISIMULATOR was improved. 

		The encoding of branching equivalence in terms of boolean
		equation systems was enhanced in order to reduce the number
		of tau-closures (transitive reflexive closures over tau-
		transitions) computed when one of the states being compared
		does not have outgoing tau-transitions. The new encoding
		allows to identify (on the fly) the cases where branching
		equivalence becomes identical to tau*.a equivalence, and
		to simplify the equations accordingly. We observed that this
		can reduce the number of boolean variables by up to 40% and
		the number of boolean operators by up to 60%.

		The encoding of observational equivalence was improved in 
		the case where the explicit LTS (represented as a BCG file)
		is deterministic and does not have invisible transitions.
		In this case, observational equivalence becomes identical
		(modulo the presence of deadlock states) to tau*.a equivalence.
		This allows to simplify the equations and to reduce the number
		of boolean variables and operators by one order of magnitude.

IMPROVEMENT
Number:		1067
Date:		Mon Jan  9 11:48:22 MET 2006
Author:		David Champelovier (INRIA/VASY)
Files:		./INSTALLATION_MACOS,
		./com/installator, ./src/com/install_uncompress

Nature:		We ported INSTALLATOR to MacOS X 10.4 "Tiger": modifications
		were made in order to avoid a problem with the "uncompress"
		command in MacOS X 10.4. Also, the installation directives
		given in file INSTALLATION_MACOS were updated.

BUG FIX
Number:		1068
Date: 		Mon Jan  9 15:07:21 MET 2006
Report:		Mohammad Torabi Dashti (CWI, Amsterdam, The Netherlands)
Author:		Radu Mateescu (INRIA/VASY)
Files:		man/*/evaluator.*

Nature:		In the manual page for EVALUATOR, a syntactic error was
		corrected in an example given to illustrate action predicates
		involving Unix regular expressions.

IMPROVEMENT
Number:		1069
Date:		Wed Jan 11 09:51:24 MET 2006
Authors:	Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files:		doc/*/Mateescu-05.*, doc/*/Garavel-Mateescu-Bergamini-06.*

Nature:		Two new papers were added to CADP, one about state space
		reductions for weak equivalences, and another one about
		the DISTRIBUTOR and BCG_MERGE tools.

BUG FIX
Number:		1070
Date: 		Thu Jan 26 11:42:57 MET 2006
Report:		Wendelin Serwe (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c

Nature:		A table overflow error was corrected in EXP.OPEN 2.0, which
		sometimes caused a segmentation fault when parallel operators
		had synchronization sets containing gates or labels that did
		not occur in any of the parallel behaviours.

IMPROVEMENT
Number:		1071
Date: 		Wed Feb  1 15:04:17 MET 2006
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/bisimulator.a, man/*/bisimulator.l

Nature:		A new option "-tauconfluence" was added to BISIMULATOR. This
		option, which can be used in conjunction with branching and
		observational equivalences, reduces the implicit LTS
		(represented as an OPEN/CAESAR program) on-the-fly by applying
		tau-confluence, a form of partial order reduction preserving
		branching equivalence. In some cases, this option improves the
		speed and memory consumption significantly.

BUG FIX
Number:		1072
Date: 		Thu Feb  2 13:32:10 MET 2006
Report:		Nicolas Descoubes (INRIA/VASY)
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/xtl

Nature:		A bug was fixed in the XTL model checker, which caused it to
		loop forever in certain cases and on some versions of Linux
		and Windows operating systems. The error was apparently in
		the Gcc compiler, some versions of which behave incorrectly
		when they are invoked with the "-O2" option. Replacing the
		"-O2" by "-O3" option solved the problem.

IMPROVEMENT
Number:		1073
Date:		Thu Feb 16 19:16:51 MET 2006
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		demo_19/*, demo_38/gate_functions.c

Nature:		The C files containing the EXEC/CAESAR's gate functions for
		demo_19 and demo_38 have been enhanced to make use of the
		logging macro-definitions recently added to "caesar_kernel.h"
		(see item #1059 above). Also, various issues have been fixed
		in demo_19.

BUG FIX
Number:		1074
Date:		Fri Feb 17 19:13:52 MET 2006
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.new

Nature:		A problem was fixed in the C code generated by CAESAR with
		"-exec" option (i.e., using the EXEC/CAESAR framework). The
		visible gate "delta" expressing the termination of a LOTOS
		program (i.e., the "exit" operator in LOTOS) was translated
		into a C function named exit(), which caused a confusion with
		the predefined C function having the same name. From now on,
		the "delta" gate will be translated into a C gate function
		named CAESAR_EXIT() instead of exit().

IMPROVEMENT
Number:		1075
Date:		Tue Feb 21 10:13:43 MET 2006
Report:		Patrice Moreaux (Universite de Savoie, France)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		src/com/cadp_postscript

Nature:		The BCG_DRAW and EUCALYPTUS tools have been enhanced to use
		automatically, on Solaris and Linux, an alternative PostScript
		viewer ("gv", "ggv", or "kghostview") when the "ghostview"
		PostScript viewer "ghostview" is missing.

IMPROVEMENT
Number:		1076
Date:		Tue Feb 21 12:56:19 MET 2006
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_cc

Nature:		The "cadp_cc" shell-script was enhanced to handle properly,
		on Solaris, the case where the Sun C compiler is installed
		elsewhere than in its standard location /opt/SUNWspro/bin/cc.

IMPROVEMENT
Number:		1077
Date:		Tue Feb 21 17:34:28 MET 2006
Authors:	David Champelovier, Hubert Garavel, and Frederic Lang (INRIA/
		VASY)
Files:		bin.*/caesar, bin.*/caesar.adt, bin.*/caesar.new, 
		bin.*/exp2c, bin.*/libBCG.a, bin.*/bcg_lib,
		demos/demo_12/main.c,
		incl/X_NATURAL.h, incl/bcg_predefined_declarations.h,
		src/open_caesar/simulator.i

Nature:		Many changes have been brought to CADP in order to support
		the Intel C/C++ compiler "icc" version 9.0. These changes
		concerned existing C files as well as C code generated by
		tools such as CAESAR, CAESAR.ADT, CAESAR.NEW, EXP2C, and
		BCG_LIB. They aimed at avoiding warnings emitted by "icc",
		such as:
		- warning #108: implicitly-signed bit field of length 1
		- warning #180: argument is incompatible with formal parameter
		- warning #592: variable "bcg1_return" is used before its
		  value is set
		- warning #1011: missing return statement at end of non-void
		  function "CAESAR_INFORMATION_LABEL"
		- warning #1011: missing return statement at end of non-void
		  function "CAESAR_COMPARE_LABEL"
		- warning #1011: missing return statement at end of non-void
		  function "CAESAR_ADT_ITR_NEXT_FUNCTION_xxx"
		- warning #1011: missing return statement at end of non-void
		  function "EXPOPEN_SELECT_STATE"
		- warning #1011: missing return statement at end of non-void
		  function "Bcg1_GET_VALUE"

IMPROVEMENT
Number:		1078
Date: 		Thu Feb 23 13:39:51 MET 2006
Report:		Hubert Garavel and Jerome Fereyre (INRIA/VASY)
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/libcaesar.a, incl/caesar_solve_1.h,
		bin.*/bisimulator.a, bin.*/evaluator.a,
		man/*/caesar_solve_1.*, doc/*/Garavel-92-a.*

Nature:		The functions CAESAR_READ_SOLVE_1() and CAESAR_WRITE_SOLVE_1()
		belonging to the CAESAR_SOLVE_1 library were improved as
		follows.

		- For each function, the parameter:
		    CAESAR_PATHNAME of type CAESAR_TYPE_STRING
		  previously denoting the pathname of a ".bes" file was
		  replaced by a parameter:
		    CAESAR_FILE of type CAESAR_TYPE_FILE
		  denoting a pointer to an already open file. Consequently,
		  CAESAR_READ_SOLVE_1() and CAESAR_WRITE_SOLVE_1() no longer
		  invoke fopen() and fclose() internally; this should be done
		  outside.

		- Two new parameters were added to CAESAR_READ_SOLVE_1():
		    CAESAR_BLOCK_UNIQUE_RESOLUTION of type
		       CAESAR_TYPE_BOOLEAN_FUNCTION_SOLVE_1
		    CAESAR_BLOCK_SOLVE_MODE of type
		       CAESAR_TYPE_NATURAL_FUNCTION_SOLVE_1
		  These parameters are pointers to functions returning, for
		  each index of an equation block in the system, a boolean
		  value indicating whether that block will be solved one or
		  several times, and the resolution mode used for that block,
		  respectively. If the actual values of these parameters are
		  different from NULL, they will be given to the corresponding
		  parameters in the call to CAESAR_CREATE_SOLVE_1() performed
		  by CAESAR_READ_SOLVE_1(), which creates the boolean equation
		  system read from the file. If these parameters are set to
		  NULL, the corresponding parameters of CAESAR_CREATE_SOLVE_1()
		  are determined by the contents of the input file. These two
		  parameters allow to do last minute changes of the resolution
		  of the boolean equation system contained in the input file.

		- One new parameter was added to CAESAR_WRITE_SOLVE_1():
		    CAESAR_DIAGNOSTIC of type CAESAR_TYPE_BOOLEAN
		  If this parameter is set to CAESAR_FALSE, the portion of the
		  boolean equation system written into the output file will
		  contain all equations defining the variables upon which the
		  variable CAESAR_V depends. Otherwise, the output file will
		  contain only the equations defining the variables contained
		  in the diagnostic of the CAESAR_V variable.

		As these changes are NOT backward-compatible with former
		versions of the CAESAR_SOLVE_1 library, user applications
		invoking CAESAR_READ_SOLVE_1() and/or CAESAR_WRITE_SOLVE_1()
		should be updated accordingly.

BUG FIX
Number:		1079
Date: 		Fri Feb 24 12:12:28 MET 2006
Report:		David Champelovier (INRIA/VASY)
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/xtl

Nature:		A bug was fixed in the XTL tool, which caused a core dump in
		the particular situation when the input BCG file becomes
		unreadable between the moment at which XTL was launched and
		the moment the C code generated by the tool is executed.

BUG FIX
Number:		1080
Date: 		Thu Mar  2 14:29:51 MET 2006
Report:		Frederic Lang (INRIA/VASY)
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/libcaesar.a, bin.*/reductor.a

Nature:		A bug was fixed in the CAESAR_SOLVE library, which caused a
		segmentation fault when invoking the REDUCTOR tool with the
		"-taucompression -divergence" options.

BUG FIX
Number:		1081
Date: 		Fri Mar  3 17:32:17 MET 2006
Report:		Gwen Salaun (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/exp2c

Nature:		A bug was fixed, which caused EXP.OPEN 2.0 to abort with a
		segmentation fault while generating the C code corresponding
		to a composition expression containing the "label par"
		operator.

IMPROVEMENT
Number:		1082
Date: 		Mon Mar  6 19:37:52 MET 2006
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard, man/*/svl.*

Nature:		The SVL language and compiler were extended to integrate 
		several recent functionalities of CADP:

		- Comparison using BISIMULATOR may now use one of the "dfs"
		  or "bfs" methods; this gives access to the "-dfs" and "-bfs"
		  options of BISIMULATOR for selecting depth-first search or
		  breadth-first search algorithms.

		- Temporal logic formula verification (i.e., the "verify"
		  operator in SVL) may now use the "dfs", "bfs", or "acyclic"
		  methods; this triggers the "-dfs", "-bfs", and "-acyclic"
		  options of EVALUATOR, thus allowing to choose among a depth-
		  first search algorithm, a breadth-first search algorithm, or
		  an algorithm dedicated to acyclic graphs.

IMPROVEMENT
Number:		1083
Date: 		Fri Mar 10 08:45:50 MET 2006
Authors:	Frederic Lang and Hubert Garavel (INRIA/VASY)
Files:		bin.*/determinator.a, bin.*/reductor.a,
		man/*/determinator.l, man/*/reductor.l,
		com/aldebaran, man/*/aldebaran.*,
		demo_31/demo.svl, demo_39/demo.svl

Nature:		A new version 5.0 of Reductor was released, together with a
		new version of Determinator. The new version of Reductor
		includes several functionalities previously available in
		Determinator. The main changes wrt version 4.0 of Reductor
		are the following:

		- The "-minimal" option of Reductor was renamed into "-total"
		  (since "-minimal" does not always generate a minimal graph).
		  A new "-partial" option (opposite of "-total") was added
		  for symmetry.

		- New equivalences have been added to Reductor, namely
		  "-trace" (which implements trace reduction, previously
		  available in Determinator as normal determinization),
		  "-weaktrace" (which implements weak trace reduction,
		  previously available in Determinator as determinization
		  with tau-elimination), and "-taudivergence".

		- Consequently, the determinization of ordinary Labelled
		  Transition Systems is no longer supported by Determinator.
		  Option "-rate" of Determinator becomes the default option.
		  The options "-normal" and "-tauclosure" of Determinator are
		  now deprecated. The Reductor tool should be used instead:
		  Precisely, one should use ``reductor -trace'' instead of
		  ``determinator -normal'', and ``reductor -weaktrace''
		  instead of ``determinator -normal -tauclosure''.

		The Aldebaran 7.0 shell-script was modified; it now invokes
		Reductor instead of Determinator to perform determinization,
		trace reduction and weak trace reduction. This change is
		transparent to the end user.

		The demos 31 and 39, which invoked ``determinator -rate''
		have been simplified to drop the "-rate" option.

		The Aldebaran, Determinator, and Reductor manual pages have
		been updated accordingly. The Reductor manual page, in
		particular, was deeply revised.

IMPROVEMENT
Number:		1084
Date: 		Fri Mar 10 18:38:46 MET 2006
Authors:	Frederic Lang and Hubert Garavel (INRIA/VASY)
Files:		bin.*/svl_kernel, src/svl/standard, man/*/svl.*,
		demo_07/demo.svl, demo_32/demo.svl

Nature:		The SVL language and compiler have been modified to reflect
		the changes brought to Reductor 5.0:

		- The "reduction" operator of SVL is now equipped with a new
		  clause "with reductor" and three new equivalence names
		  ("tau-confluence", "tau-compression", and "tau-divergence").

		- A new "partial" or "total" optional attribute was added to
		  the "reduction", "root reduction", "leaf reduction", "root
		  leaf reduction", and "node reduction" operators. Total
		  reduction has the same meaning as reduction alone. Partial
		  reduction denotes an on-the-fly reduction performed using
		  Reductor, which is generally faster but produces a larger
		  graph than total reduction.

		- To compute "tau-confluence", "tau-compression", and
		  "tau-divergence", SVL invokes Reductor by default. To
		  compute "trace" and "weak trace" equivalence, SVL now
		  invokes Reductor instead of Determinator. To compute
		  "tau*.a" and "safety" equivalences, SVL now invokes
		  Reductor by default instead of Aldebaran.

		Demo_07 and demo_32 have been modified so as to remove
		occurrences of "using fly" in SVL scripts.

IMPROVEMENT
Number:		1085
Date: 		Wed Mar 15 11:35:00 MET 2006
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		co,/tst, incl/bcg_standard.h, incl/caesar_standard.h,
		./INSTALLATION_2

Nature:		Many changes have been brought to CADP tools for a smoother
		support of Intel's ICC 9.0 compiler for Linux and Sun's
		SunStudio 11 compiler for Solaris:

		- The "tst" shell-script now recognizes ICC and displays its
		  version number.

		- The "tst" shell-script also displays the version number of
		  Sun's C compiler and, when necessary, emits a warning about
		  the C compilers available on Solaris.

		- "tst" now emits a warning message if the version of ICC
		  is l_cc_c_9.0.030 or older, as these versions of ICC
		  contain a bug (issue Q338282 : "sign extension on cast from
		  unsigned short to int when optimized"), detected by VASY,
		  that prevents BCG tools from working properly when using
		  optimization option "-O1" (which is activated by default
		  in ICC). This issue was fixed by Intel in version
		  l_cc_c_9.0.031.

		- On Linux, "tst" no longer displays any warning message when
		  $CADP_CC is set to a value different from "gcc" (as "icc"
		  is also a valid value). Also, "tst" no longer complains
 		  in the particular case where, under Linux, $CADP_CC is set
		  to "icc" and $LD_LIBRARY_PATH contains the path of ICC's
		  dynamic libraries.

		- "tst" now checks the C compiler contained in $CADP_CC by
		  trying to compile and execute a simple C program.

		- The INSTALLATION_2 file was enhanced to provide better
		  explanations on how to set $CADP_CC (especially for Solaris
		  users) and how to use Parasoft's Insure software.

		- The include files "bcg_standard.h" and "caesar_standard.h"
		  have been adapted to work with ICC.

BUG FIX
Number:		1086
Date: 		Thu Mar 16 12:05:45 MET 2006
Report:		Wendelin Serwe (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard

Nature:		If the diagnostic produced by the SVL's "verify" (respectively,
		"comparison") operator was a trace and if some labels in this
		trace contained the sub-string "TRUE" or "FALSE", these labels
		were displayed after the expected verification (respectively,
		comparison) result, i.e., TRUE or FALSE. This bug was fixed.

BUG FIX
Number:		1087
Date: 		Thu Mar 16 15:32:42 MET 2006
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/reductor.a

Nature:		In some cases, the labelled transition system generated by
		``reductor -total -safety'' was not minimal modulo safety 
		equivalence. This bug was fixed.

IMPROVEMENT
Number:		1088
Date: 		Thu Mar 16 16:23:16 MET 2006
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/bcg_min

Nature:		BCG_MIN now emits a warning message when the "-epsilon" option
		is used for standard labelled transition systems, i.e., when
		neither the "-rate" nor "-prob" option is given on the
		command-line.

IMPROVEMENT
Number:		1089
Date: 		Fri Mar 24 18:14:16 MET 2006
Report:		Sven Johr, Holger Hermanns, and Reza Pulungan (Saarland
		University, Germany)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/bcg_min, bin.*/determinator.a, 
		man/*/bcg_min.*, man/*/determinator.*

Nature:		A new option "-format" was added to BCG_MIN and DETERMINATOR.
		This option allows to control the representation of floating-
		point numbers finely. Previously, the floating-point numbers
		(rate or probabilities) occurring on the transitions of the
		Markov chains generated by BCG_MIN and DETERMINATOR were
		displayed using the "%f" format of sprintf(), i.e. with at
		most 6 digits after the radix character ".", thus causing a
		loss of precision (transitions with slightly different values
		being considered as identical). From now on, the format for
		floating-point numbers can be specified using the "-format"
		option. 

		Also, the following (incompatibble) changes have been brought
		to BCG_MIN and DETERMINATOR:

		- When no "-format" option is given, the default format used
		  by BCG_MIN and DETERMINATOR is now "%g" instead of "%f".
		  For instance, this allows to display a probability value
		  as 1.23e-9 instead of 0.000000.

		- For BCG_MIN, when no "-epsilon" option is given, the default
		  precision is now 1e-6 instead of 1e-3. Thus, the behaviour
		  of BCG_MIN is now aligned on that of DETERMINATOR.

		The manual pages for BCG_MIN and DETERMINATOR have been
		updated accordingly.

IMPROVEMENT
Number:		1090
Date:		Fri Mar 24 19:20:19 MET 2006
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/evaluator.a, man/*/evaluator.*

Nature:		The "-bes" option of EVALUATOR was improved in two ways:

		- When this option is given on the command-line, EVALUATOR no
		  longer stops after producing the text file containing the
		  boolean equation system; from now on, EVALUATOR continues
		  evaluating the formula and generating the diagnostics.

		- If the file name specified after "-bes" has the extension
		  ".bes.gz", it will be compressed using gzip(1), which yields
		  substantial file size reductions for large boolean equation
		  systems.

IMPROVEMENT
Number:		1091
Date: 		Mon Mar 27 19:33:42 MEST 2006
Authors:	Antonella Chirichiello (Univ. La Sapienza, Roma, Italy),
		Gwen Salaun, and Wendelin Serwe (INRIA/VASY)
Files:		demos/demo_40

Nature:		A new demo (Web services for stock management and on-line book
		auction) was added to CADP.

BUG FIX
Number:		1092
Date: 		Tue Mar 28 17:58:42 MEST 2006
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.new

Nature:		In the C code generated by CAESAR (and CAESAR.NEW) using the
		"-exec" option (i.e., the C code produced for the EXEC/CAESAR
		environment), the name of the gate function generated for the
		"delta" gate of LOTOS was renamed into "EXIT()" instead of
		"CAESAR_EXIT()" (see also item #1074 above). This avoids a
		potential name conflict in case the LOTOS specification with
		functionality "exit" would also contain a visible gate named 
		"caesar_exit", or "Caesar_Exit", etc.

BUG FIX
Number:		1093
Date: 		Tue Mar 28 18:55:08 MEST 2006
Report:		Reza Pulungan (Saarland Univ., Germany)
Author:		Frederic Lang (INRIA/VASY)
Files:		bin.*/svl_kernel

Nature:		A bug was fixed in the SVL tool, which generated incorrect
		".exp" files when the gates to synchronize did not start with
		a letter (e.g., when these gates were numbers).

BUG FIX
Number:		1094
Date: 		Thu Mar 30 16:19:48 MEST 2006
Report:		Wendelin Serwe (INRIA/VASY)
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.new

Nature:		In the C code generated by CAESAR (and CAESAR.NEW) using the
		"-exec" option, the gate functions were not declared before
		being used. With recent C compilers, such as SunStudio 11,
		this caused warnings of the form: 
		   warning: implicit declaration of function `G'
		This issue was solved.

BUG FIX
Number:		1095
Date: 		Thu Mar 30 17:45:25 MEST 2006
Report:		Wendelin Serwe (INRIA/VASY)
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.new

Nature:		In the special case of LOTOS specifications not containing
		any visible nor tau transition, the C code generated by CAESAR
		(and CAESAR.NEW) with option "-exec" would not compile 
		properly. This issue was fixed.

IMPROVEMENT
Number:		1096
Date: 		Thu Mar 30 21:48:36 MEST 2006
Report:		Reza Pulungan (Saarland Univ., Germany)
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/bcg_io, man/*/bcg_io.*

Nature:		A new option "-format" (similar to the "-format" option added
		to BCG_MIN and DETERMINATOR recently) was added also to the
		"-etmcc" option of BCG_IO. This option controls the format
		under which floating-point numbers (rates or probabilities)
		are written into the ".tra" file to be read by the ETMCC
		model checker.

		This change is potentially incompatible, as floating-point
		numbers are now displayed, by default, using format "%g"
		instead of "%f". However, the former behaviour can still be
		obtained using option ``-format "%f"''.

BUG FIX
Number:		1097
Date: 		Thu Apr  6 19:24:20 MEST 2006
Report:		Wendelin Serwe (INRIA/VASY)
Authors:	Radu Mateescu and David Champelovier (INRIA/VASY)
Files:		bin.*/ocis.a

Nature:		Recent versions of OCIS could not execute properly. At link
		edit time, an error message of the form:
		  Undefined symbol CAESAR_TAU_CLOSURE_REACH_DEADLOCK_EDGE_LIST
		would be emitted. This issue was fixed. 

IMPROVEMENT
Number:		1098
Date: 		Fri Apr  7 17:02:48 MEST 2006
Authors:	Hubert Garavel and Radu Mateescu (INRIA/VASY)
Files:		doc/=READ_ME.txt

Nature:		The CADP publication list was entirely reorganized. New
		sections were added to reflect the new software architecture
		of CADP. Sections related to obsolete or deprecated CADP tools
		were moved at the end of the list. The corresponding Web page
		   http://vasy.inria.fr/publications/cadp.html
		was updated accordingly.

BUG FIX
Number:		1099
Date: 		Fri Apr  7 18:04:11 MEST 2006
Report:		Frederic Lang (INRIA/VASY)
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		bin.*/libcaesar.a

Nature:		An issue was fixed in function CAESAR_TEST_REGEXP() defined in
		the "caesar_regexp.h" library. In some cases, this function
		would modify the character string pointed by its first
		argument. On Linux, this could cause a segmentation fault
		when running EXP.OPEN.

IMPROVEMENT
Number:		1100
Date:		Mon Apr 10 16:37:41 MEST 2006
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/bisimulator.a, man/*/bisimulator.*

Nature:		The "-bes" option of BISIMULATOR was improved in two ways
		(see also item #1090 above):

		- When this option is given on the command-line, BISIMULATOR
		  no longer stops after producing the text file containing the
		  boolean equation system; from now on, BISIMULATOR continues
		  comparing the graphs and generating the diagnostics.

		- If the file name specified after "-bes" has the extension
		  ".bes.gz", it will be compressed using gzip(1), which yields
		  substantial file size reductions for large boolean equation
		  systems.

IMPROVEMENT
Number:		1101
Date: 		Tue Apr 18 11:25:22 MEST 2006
Authors:	Christophe Joubert and Radu Mateescu (INRIA/VASY)
Files:		doc/*/Joubert-Mateescu-06.*

Nature:		A new paper on distributed verification was added in the
		"doc" directory. 

BUG FIX
Number:		1102
Date:		Wed Apr 26 18:51:34 MEST 2006
Report:		Ken Turner (University of Stirling, Scotland, UK)
Author:		Hubert Garavel (INRIA/VASY)
Files:		tcl-tk/com/wish, tcl-tk/com/tixwish

Nature:		On Windows, if the environment variable $CYGWIN was set and
		if its value contained the substring "tty", all the CADP tools
		based on Tcl/Tk (e.g., Installator, Eucalyptus) would fail
		with the following error message:
		   [main] echo ... tty_list::allocate_tty: No tty allocated
		   while executing ...
		The Wish and Tixwish shell-scripts included in CADP have been
		modified so as to remove the "tty" substring from $CYGWIN
		when present.

BUG FIX
Number:		1103
Date: 		Tue May  2 14:18:30 MEST 2006
Report:		Gwen Salaun and Wendelin Serwe (INRIA/VASY)
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/bisimulator.a

Nature:		A bug was fixed in the counterexample generation feature of
		BISIMULATOR. The bug, which occurred only when checking
		branching equivalence, caused in some cases the insertion in
		the counterexample of certain transition sequences that were
		absent from both LTSs being compared.

BUG FIX
Number:		1104
Date:		Wed May  3 18:57:38 MEST 2006
Report:		Wendelin Serwe (INRIA/VASY)
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		incl/X_STRING.h

Nature:		The two macro-definitions of ADT_CMP_STRING (X1, X2) and 
		ADT_PRINT_STRING (F, X) have been modified to handle the
		cases where string pointers X, X1, and/or X2 are NULL (this
		situation can arise when using CAESAR.NEW, which resets dead
		variables to NULL automatically).

IMPROVEMENT
Number:		1105
Date:		Thu May  4 10:34:21 MEST 2006
Report:		Jacques Abily and Sylvie Lesmanne (Bull)
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.new, man/*/caesar.*

Nature:		CAESAR and CAESAR.NEW have been enhanced with a "-external"
		option that generates automatically a prototype file (with
		suffix ".c.proto") containing skeletons for EXEC/CAESAR's gate
		functions, i.e., functions associated to all visible gates of
		the LOTOS specification. These gate functions are incomplete:
		they must be completed manually (at all places marked "...")
		with input/output operations required to interface the C code
		generated from the LOTOS specification with its real, external
		environment. Option "-external" must be used together with
		"-exec" option. Three new additional options ("-indent", 
		"-oldstyle", and "-newstyle") have been also added to control
		the form of the generated C code.

IMPROVEMENT
Number:		1106
Date: 		May  5 10:37:35 MEST 2006
Report:		Gwen Salaun and Wendelin Serwe (INRIA/VASY)
Authors:	David Champelovier, Hubert Garavel, and Frederic Lang (INRIA/
		VASY)
Files:		src/eucalyptus/eucalyptus.tcl, src/com/xeuca_convert

Nature:		A new version 2.6 of EUCALYPTUS was released, which reflects
		the changes brought to the command-line CADP tools. As regards
		the menu bar, the changes are the following:

		- In the menu "File / Save Preferences", the preferred options
		  for BISIMULATOR, EVALUATOR, and TGV are now stored in file
		  ~/.xeucarc.

		- Following the replacement of ALDEBARAN by a shell-script
		  (see item #1052 above), the menu "Options / ALDEBARAN" was
		  removed. The "-labels" option of ALDEBARAN can now be set
		  in the "Reduce" window of ALDEBARAN.

		- The former menu "Options / EVALUATOR and XTL" was splitted
		  into "Options / EVALUATOR" and "Options / XTL". The new
		  menu "Options / EVALUATOR" gives access to the recent
		  options of EVALUATOR, including "-verbose", "-silent",
		  "Boolean Equation System printing...", etc.

		- A new menu "Options / EXP.OPEN" was added to specify the
		  command-line options of EXP.OPEN 2.0.

		- The "Help" menu was updated. In particular, the manual
		  page for the (now obsolete) EXP2FC2 tool is no longer
		  proposed in the Help window.

		As regards the contextual menus attached to files in the
		left window of EUCALYPTUS, the following changes were made:

		- In the "Compare..." menu, tau-confluence option was added
		  for the BISIMULATOR tool and the ALDEBARAN tool is no
		  longer proposed (since BISIMULATOR is superior to ALDEBARAN
		  in every respect, except that it does not support the
		  delay equivalence, which is never used in practice).
		  Also, a bug that prevented the comparison between a ".aut"
		  and a ".bcg" file was fixed.

		- In the "Convert" menu for ".exp" files, a bug was fixed that
		  prevented ".exp" files from being translated into the FC2
		  format. Also, the translation into the PEP format is now
		  proposed.

		- A new menu "Evaluate performance..." was added to invoke
		  the BCG_STEADY and BCG_TRANSIENT tools.

		- In the "Evaluate temporal formula..." menu, the access to
		  options "-bfs", "-dfs" and "-acyclic" of EVALUATOR was made
		  safer. EUCALYPTUS only proposes three possibilities ("-bfs",
		  "-dfs", and "-dfs -acyclic") thus preventing from selecting
		  "-bfs" and "-acyclic" simultaneously. 

		- In the "Find Deadlock..." menu, the ALDEBARAN tool is no
		  longer proposed.

		- In the "Find Livelock..." menu, the ALDEBARAN tool is no
		  longer proposed.

		- In the "Properties" menu, the ALDEBARAN tool is no longer
		  used to display properties of ".exp" files; EXP.OPEN is used
		  instead, with its "-info" option.

		- In the "Reduce..." menu, many changes have been made. On-
		  the-fly reduction using the REDUCTOR tool is now proposed
		  for several types of files, including ".lotos" files.
		  Generally, the ALDEBARAN tool is still proposed, but for
		  observational equivalence only, as other equivalences are
		  more efficiently implemented by BCG_MIN and REDUCTOR. On
		  ".exp" files however, ALDEBARAN is no longer proposed in
		  the "Reduce..." menu, since ALDEBARAN does not implement
		  observational equivalence for ".exp" files. Finally, the
		  new "-format" option of BCG_MIN and the new default value
		  for the "-epsilon" option of BCG_MIN (see above item #1089)
		  are now reflected by EUCALYPTUS.

IMPROVEMENT
Number:		1107
Date:		Fri May 19 16:39:31 MEST 2006
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		demos/demo_05/user.c, demos/demo_12/main.c, 
		demos/demo_19/gate_functions.c, incl/caesar_standard.h,
		src/exec_caesar/main.c, src/open_caesar/declarator.c,
		src/open_caesar/executor.c, src/open_caesar/generator.c,
		src/open_caesar/generator2.c, src/open_caesar/predictor.c,
		src/open_caesar/reductor2.c, src/open_caesar/reductor3.c,
		src/open_caesar/simulator.c, src/open_caesar/terminator.c

Nature:		Minor changes have been made to source C code files included
		in CADP so as to avoid warnings from the "lint" verifier of
		Sun Studio 11.

IMPROVEMENT
Number:		1108
Date:		Tue May 23 18:38:20 MEST 2006
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar.indent

Nature:		CAESAR.INDENT was modified to produce nicer results when
		pretty-printing LOTOS specifications, and especially data type
		definitions:
		- A newline character is now inserted after keyword "opns"
		- No newline character is any more inserted after keyword "=>"
		- Equations occurring after a "forall" clause are shifted to
		  the right by one tabulation
		- Spaces are no longer inserted around keyword ":" in variable
		  declarations (which have the form X:S or X1, ..., Xn:S)

IMPROVEMENT
Number:		1109
Date:		Tue Jun  6 16:46:50 MEST 2006
Report:		Gert Huisman (Vrije Universiteit Amsterdam, The Netherlands)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		com/rfl

Nature:		Two new options ("-v" and "-t") have been added to the "rfl"
		shell-script. These options will be used when sending e-mail
		messages to warn users about CADP license expiration. They
		will allow to mention the CADP version number and the date at
		which the license was requested. These are useful information
		for users running different versions of CADP on the same
		machine(s).

BUG FIX
Number:		1110
Date:		Tue Jun  6 19:57:26 MEST 2006
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/rfl

Nature:		When installing CADP on certain versions of Windows and
		Cygwin tools, the prototype license files sent by Installator
		would contain extra '^M' (r) characters. This was solved
		by modifying the "rfl" shell-script so as to remove these
		extra-characters.

IMPROVEMENT
Number:		1111
Date:		Wed Jun  7 19:21:08 MEST 2006
Report:		Christophe Joubert (University of Malaga, Spain)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		./INSTALLATION_2, ./INSTALLATION_4,
		./src/com/installator/installator.tcl

Nature:		When installing CADP on a FAT or NTFS partition accessed from
		Linux (using SAMBA), the installation would fail silently as
		symbolic links are not supported by FAT nor NTFS. Two actions
		have been taken to address this issue:

		- This problem is now documented in files INSTALLATION_2 and
		  INSTALLATION_4.

		- Installator now checks whether it is possible to create
		  symbolic links on the partition chosen by the user to
		  install CADP; if not, an error message is displayed.

IMPROVEMENT
Number:		1112
Date: 		Mon Jun 26 14:25:14 MEST 2006
Report:		Nathalie Lepy (INRIA/VASY)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		src/eucalyptus/eucalyptus.tcl, src/com/cadp_web,
		./INSTALLATION_2

Nature:		The EUCALYPTUS graphical user-interface was enhanced in 
		several ways:

		- On Unix systems, the default browser (i.e., the default
		  value of the environment variable $NAVIGATOR) is now
		  "firefox" instead of "netscape".

		- The contents of the "Web" menu have been redesigned. The
		  new "Web" menu gives access to various Web pages providing
		  useful information about CADP: tutorials, manual pages,
		  case studies, FAQ, etc.

		- Two problems have been fixed in the "Compare..." and
		  "Reduce..." menus for files with ".LOTOS" extension
		  (i.e., files to be pre-processed using APERO).

		- The "More" menu for files with a ".lotos" or ".LOTOS"
		  extension has been renamed into "More commands". For
		  ".LOTOS", this menu now contains the "Compile abstract
		  data types" entry. For ".lotos" and ".LOTOS" files, two
		  new entries have been added: "Generate external types/
		  functions" (the corresponding menu entry "Options /
		  Caesar.adt / Generate external prototype files" has been
		  removed) and "Generate gate functions...".

		- In the XTL-related section of the "Verify temporal
		  properties..." menu, the "Expand only" option has been
		  made active.

IMPROVEMENT
Number:		1113
Date: 		Mon Jun 26 17:28:52 MEST 2006
Author:		Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar.adt, man/*/caesar.adt.*

Nature:		From now on, CAESAR.ADT will indent, not only the generated
		".h" file as usual, but also the ".f.proto" and ".t.proto"
		files if the "-external" option is selected. The "-indent"
		option can be use to prevent these files from being indented.

IMPROVEMENT
Number:		1114
Date: 		Mon Jun 26 19:33:52 MEST 2006
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.new, man/*/caesar.*

Nature:		From now on, if the "-external" option is given, CAESAR and
		CAESAR.NEW will no longer stop if the ".c" file already exists
		and is up to date: CAESAR will generate both the ".c" and the
		".c.proto" files.

IMPROVEMENT
Number:		1115
Date: 		Mon Jun 26 19:43:50 MEST 2006
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		bin.*/caesar.adt

Nature:		From now on, if the "-external" option is given, CAESAR.ADT
		will no longer stop if the ".h" file already exists and is up
		to date: CAESAR.ADT will generate the ".h", ".f.proto", and
		".t.proto" files.

BUG FIX
Number:		1116
Date: 		Wed Jun 28 12:42:03 MEST 2006
Report:		Nathalie Lepy (INRIA/VASY)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		src/eucalyptus/eucalyptus.tcl

Nature:		In the EUCALYPTUS interface, when evaluating an XTL formula
		on a BCG file, the "Expand only" option has been made active.

BUG FIX
Number:		1117
Date: 		Mon Jul  3 17:25:10 MEST 2006
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		com/tst

Nature:		When running the "tst" shell-script on Linux, if the process
		stack size was set to unlimited, an error message was issued:
                   tst: line 1055: [: unlimited: integer expression expected
		This problem was fixed.

BUG FIX
Number:		1118
Date: 		Mon Jul  3 18:24:33 MEST 2006
Report:		David Champelovier and Frederic Lang (INRIA/VASY)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		src/com/cadp_tail

Nature:		Under some circumstances, the "cadp_tail" command would emit
		an error message:
		   cadp_tail: line 69:  2548 Broken pipe        tail "$@
		This problem was solved by handling SIGPIPE signals correctly.

IMPROVEMENT
Number:		1119
Date: 		Mon Jul  3 19:12:41 MEST 2006
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_indent

Nature:		The "cadp_indent" command can now detect automatically the
		Sun pretty-printer ("indent") even if it is not located in
		/opt/SUNWspro/bin/indent. It can also use the GNU "indent"
		if present. 

IMPROVEMENT
Number:		1120
Date: 		Tue Jul  4 19:39:32 MEST 2006
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY)
Files:		bin.*/caesar.indent 

Nature:		The LOTOS pretty-printer was enhanced, as regards variable
		declarations. Single variable declarations are formatted
		without spaces ("X:S"), while multiple variable declarations
		are formatted with spaces ("X1, ..., Xn : S"), so as to
		enhance readability.

BUG FIX
Number:		1121
Date: 		Wed Jul  5 17:08:48 MEST 2006
Authors:	Wendelin Serwe and Hubert Garavel (INRIA/VASY) 
Files:		bin.*/caesar.bdd

Nature:		A semantic error was fixed in the "-unit" option of the
		CAESAR.BDD tool. The algorithm implementing this option was
		entirely redesigned so as to be compatible with the definition
		of "concurrent units" given in the [Garavel-Serwe-04] paper.

BUG FIX
Number:		1122
Date: 		Fri Jul  7 11:41:30 MEST 2006
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		src/com/cadp_indent

Nature:		The "cadp_indent" command was modified so as to cope with
		core files on Linux (which are not named "core", but 
		"core.pid", where pid is a process number). 

IMPROVEMENT
Number:		1123
Date:		Fri Jul  7 17:33:12 MEST 2006
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		bin.*/caesar, bin.*/caesar.old, bin.*/caesar.new, com/rfl,
		demo_20/=READ_ME.txt, demo_27/=READ_ME.txt,
		demo_28/=READ_ME.txt

Nature:		The "caesar" binary (version 6.2 of CAESAR) was renamed into
		"caesar.old". The "caesar.new" binary (version 7.0 of CAESAR)
		was renamed into "caesar" and becomes the default.

		The statistics of demos 20, 27 and 28 have been updated
		accordingly, so as to reflect the reduction factor obtained
		using CAESAR 7.0. On all CADP demos, we observed that this
		divides the number of states generated by an average factor
		of 45 (with a maximum factor of 4,400) and the numbers of 
		transitions by an average factor of 38 (with a maximum factor
		of 3,100).

IMPROVEMENT
Number:		1124
Date: 		Mon Jul 10 18:29:19 MEST 2006
Authors:	Frederic Lang and Hubert Garavel (INRIA/VASY)
Files:		com/exp.open, bin.*/exp2c, man/*/exp.open.*,
		src/eucalyptus/eucalyptus.tcl, src/com/xeuca_convert

Nature:		A new "-network tina" option was added to the EXP.OPEN 2.0
		compiler, so as to convert the input language of EXP.OPEN
		into the Petri net format of the TINA toolbox. The EUCALYPTUS
		graphical interface was enhanced to give access to this new
		functionality in the "Convert..." menu associated to ".exp"
		files.

BUG FIX
Number:		1125
Date: 		Wed Jul 12 11:37:40 MEST 2006
Report:		Nathalie Lepy (INRIA/VASY)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		src/eucalyptus/eucalyptus.tcl

Nature:		The Tcl/Tk code of EUCALYPTUS was modified to handle properly
		the situation where a user replaces, in the interface panels,
		an (integer or floating-point) number with the empty string.
		From now on, quotes are added around numbers so that empty
		strings can be detected.

IMPROVEMENT
Number:		1126
Date: 		Wed Jul 19 12:16:21 MEST 2006
Author:		Radu Mateescu (INRIA/VASY)
Files:		doc/*/Mateescu-06-a.*

Nature:		An overview paper on the CAESAR_SOLVE library for on-the-fly
		resolution of alternation-free boolean equation systems was
		added.

BUG FIX
Number:		1127
Date:		Fri Jul 21 11:32:08 MEST 2006
Report:		David Champelovier (INRIA/VASY)
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard

Nature:		On Windows, some ".sync" files produced by SVL automatically
		for Projector were incorrect. This bug was fixed.

BUG FIX
Number:		1128
Date: 		Tue Jul 25 11:46:23 MEST 2006
Report:		David Champelovier (INRIA/VASY)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.macOS/projector.a

Nature:		The Mac OS X version of the PROJECTOR tool was modified so as
		to get rid of the following error message: 

		> /usr/bin/ld: warning -L: directory name ('$CADP'/bin.macOS)
		> does not exist

IMPROVEMENT
Number:		1129
Date: 		Tue Jul 25 12:16:11 MEST 2006
Authors:	Frederic Lang and Hubert Garavel (INRIA/VASY)
Files:		bin.*/reductor.a, bin.*/tgv.a, bin.*/xsimulator.a,
		com/bcg_open, com/caesar.open, com/exp.open, com/seq.open,
		src/open_caesar/generator.c, src/open_caesar/generator2.c,
		src/open_caesar/reductor2.c, src/open_caesar/reductor3.c

Nature:		Many CADP programs and shell-scripts have been modified so as
		to add double quotes around occurrences of $CADP in $LDFLAGS
		and $LD_LIBRARY_PATH. This change is yet another step towards
		the acceptance and proper handling of white spaces in file
		names.

BUG FIX
Number:         1130
Date:           Tue Jul 25 12:24:23 MEST 2006
Report:         Wendelin Serwe (INRIA/VASY)
Author:         Radu Mateescu (INRIA/VASY)
Files:          bin.*/bisimulator.a, man/*/bisimulator.*

Nature:         A bug was fixed in the counterexample generation for branching
		equivalence in BISIMULATOR. In some cases, the counterexamples
		produced contained some transition sequences which were not
		included in the input LTSs. The new counterexamples are correct
		w.r.t. this criterion and illustrate properly the cases where
		the non equivalence of the LTSs is determined by the non
		equivalence of the source states of some transitions (the cases
		erroneously handled before were precisely of this type).
		The description of the -diag option in the manual page of the
		tool was updated accordingly. (The present bug fix completes a
		previous, partial bug fix for the same problem - see item #1103
		above).

BUG FIX
Number:		1131
Date: 		Fri Sep  8 18:35:41 CEST 2006
Author:		Hubert Garavel (INRIA/VASY)
Files:		com/tst

Nature:		The "tst" shell-script was enhanced in several ways to be 
		fully compatible with the Solaris 10 operating system:

		a) When running on Solaris 10, "tst" no longer emits the
		   following warning:

		   > Current operating system is ``SunOS 5.10''
		   > *** The CADP software is intended for SunOS 5.5 (Solaris
		   >     2.5) or higher
		   > ...

		b) When "indent" is missing on the current, "tst" explains
		   how to obtain it from Sun Web site:

		   > *** Can't find command ``indent''
		   > ==> Add directory /opt/SUNWspro/bin to your ``$PATH''
		   >     variable
    		   > If this directory does not exist, we recommend that you
		   > install the Sun Studio 11 (or higher) tool suite, which
		   > you can freely download from www.sun.com (follow
		   > Downloads, then Development Tools)

		c) When the default C compiler (i.e., gcc) is missing, the
		   explanation message was improved.

BUG FIX
Number:		1132
Date:		Mon Sep 18 14:08:55 MEST 2006
Report:		Wendelin Serwe (INRIA/VASY)
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/evaluator.a

Nature:		A minor error was fixed in the way a certain error message was
		printed by EVALUATOR.

BUG FIX
Number:		1133
Date:		Tue Sep 19 11:50:01 MEST 2006
Author:		Radu Mateescu (INRIA/VASY)
Files:		bin.*/evaluator.a

Nature:		A portability issue was fixed in the lexical scanning of .blk
		files containing modal equation systems given as arguments
		to the "-block" option of EVALUATOR. On Windows systems, this
		issue caused an infinite loop of EVALUATOR when parsing .blk
		files containing comments enclosed between "(*" and "*)".

BUG FIX
Number:		1134
Date: 		Wed Sep 20 15:16:37 MEST 2006
Report:		Reza Pulungan (Saarland University, Germany)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		src/com/install_df

Nature:		The "install_df" script used by INSTALLATOR was modified so
		as to avoid a fatal error in INSTALLATOR. This error occurred
		on Windows only for filesystems (mount points) with long names.
		After entering the download password, the following error
		message would be displayed:
		   > syntax error in expression "double(round((double(27%) /
		   >    (1024))*10))/10": unexpected close parenthesis
		   > syntax error in expression "double(round((double(27%) /
		   >    (1024))*10))/10": unexpected close parenthesis
		   >    while executing
		   > "expr double(round((double($TAILLE) / (1024))*10))/10"
		   >    (procedure "Get_Free_Space" line 7)
		   >    invoked from within
		   > "Get_Free_Space $CADP(TMP_ARCHIVE)"
		   >    (procedure "Check_Required_Space" line 28)
		   > ...
		This problem is solved now.

IMPROVEMENT
Number:		1135	
Date: 		Thu Sep 21 11:49:31 MEST 2006
Report:		Jan Rakow (OFFIS, Oldenburg, Germany)
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		com/tst

Nature:		The "tst" shell-script emits a warning when the maximal stack
		size is not large enough (this can cause problems with those
		CADP programs making intensive use of recursion). In such
		case, it emits a warning message:

		> *** The maximal stack size for executing your programs is
		>     currently limited to 2042 kbytes (see the ``ulimit -s''
		>     command'')
		> ...

		Unfortunately, it appears that command "ulimit -s" is not
		fully implemented in Cygwin, so that it is not possible to
		increase the stack size this way. The "tst" warning message
		was improved to explain this situation.

BUG FIX
Number:		1136
Date: 		Fri Sep 22 12:53:34 MEST 2006
Report:		Reza Pulungan (Saarland University, Germany)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		bin.win32/*

Nature:		The CADP licensing mechanism was enhanced to handle the case
		where, on Windows, the CADP tools are invoked from a current
		directory that is not on the same disk as the disk on which
		CADP is installed, for instance, when the user home directory
		is on disk D: while CADP is installed on disk C:.

BUG FIX
Number:		1137
Date: 		Fri Sep 22 17:15:32 MEST 2006
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		src/com/cadp_print, com/tst, INSTALLATION_2

Nature:		The "cadp_print" shell-script was modified to fetch "lpr"
		in "/usr/ucb" on Solaris. This suppresses the need for having
		"/usr/ucb" present in the $PATH on Solaris, thus simplifying
		the installation for Solaris users. The INSTALLATION_2 file
		and the "tst" shell-script have been modified accordingly.

IMPROVEMENT
Number:		1138
Date:		Fri Sep 22 17:22:09 MEST 2006
Report:		Damien Thivolle (INRIA/VASY)
Author:		Radu Mateescu (INRIA/VASY)
Files:		src/xtl/actl.mcl

Nature:		The translation in modal mu-calculus of the inevitability
		operator AU_A_A() of ACTL was improved. When using
		EVALUATOR to verify temporal formulas containing this
		operator, the new translation always leads to gains in time
		and memory, sometimes up to a factor 8.

IMPROVEMENT
Number:		1139
Date: 		Mon Sep 25 16:43:31 MEST 2006
Report:		Claude Jard (ENS Cachan, Bretagne, France)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		bin.macOS/*

Nature:		The CADP licensing mechanism was enhanced to handle the case
		of disconnected Mac OS X machines without DHCP (i.e., using
		fixed IP addresses). Upon disconnection, the names of these
		machines change, e.g., from "xxx.domain.com" into "xxx.local".

BUG FIX
Number:		1140
Date: 		Thu Oct  5 16:43:49 MEST 2006
Report:		Jerome Fereyre (INRIA/VASY)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		bin.*/cadp_hostinfo

Nature:		The "cadp_hostinfo" tool was modified to avoid intermittent
		blockings that occurred on a Linux cluster with biprocessor
		nodes.

BUG FIX
Number:		1141
Date: 		Mon Oct  9 10:43:07 MEST 2006
Author:		David Champelovier (INRIA/VASY)
Files:		com/bcg_open

Nature:		Following the change described in item #1129 above, a residual
		bug (missing backslash) was fixed in the bcg_open script. This
		bug caused warnings of the form 
		   > .../bcg_open: line 1: "/common/Cadp"/com/arch: 
		   > No such file or directory

IMPROVEMENT
Number:		1142
Date: 		Tue Oct 10 11:49:02 MEST 2006
Author:		Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_cc 

Nature:		From now on, CADP will use "cc" (instead of "gcc") as the
		default C compiler on Solaris systems.

IMPROVEMENT
Number:		1143
Date: 		Tue Oct 10 12:15:24 MEST 2006
Author:		Hubert Garavel (INRIA/VASY)
Files:		INSTALLATION_2, INSTALLATION_WINDOWS

Nature:		The installation guidelines have been updated and simplified
		to get rid of obsolete platforms (architectures and operating
		systems). In particular, compared to the previous stable
		version CADP 2001, the following platforms are no longer
		supported:
		- Sparc stations running Solaris 7
		- PC computers running Windows 98 or Windows NT4
		- PC computers running Linux with kernel version <= 2.2 and/or 
		  glibc version < 2.3
		It may happen that recent versions of CADP still work on some
		of these old architectures, but we do not make statements on
		this, as we have discontinued testing CADP on these platforms.

IMPROVEMENT
Number:		1144
Date: 		Wed Oct 11 15:38:10 MEST 2006
Author:		Radu Mateescu (INRIA/VASY)
Files:		doc/=READ_ME.txt, doc/biblio.bib,
		doc/*/Mateescu-Sighireanu-00.*, doc/*/Mateescu-Sighireanu-03.*,
		doc/*/Mateescu-06-b.*

Nature:		The paper Mateescu-Sighireanu-00 (24 pages) was replaced
		with Mateescu-Sighireanu-03 (32 pages), which provides the
		most complete reference on EVALUATOR 3.0 (please note that,
		for EVALUATOR 3.5, the reference paper is Mateescu-06-a).
		Also, a new case-study paper, Mateescu-06-b, was added.

IMPROVEMENT
Number:		1145
Date: 		Wed Oct 11 17:37:23 CEST 2006
Report:		Wendelin Serwe (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_psbox, src/com/cadp_web

Nature:		The "cadp_psbox" and "cadp_web" have been modified so as to
		fetch "gs" and "mozilla" in "/usr/sfw/bin". This is suitable
		on Solaris 10 systems.

IMPROVEMENT
Number:		1146
Date: 		Wed Oct 11 19:13:27 MEST 2006
Authors:	Hubert Garavel, Radu Mateescu, and Wendelin Serwe (INRIA/VASY)
Files:		doc/pdf/*.pdf

Nature:		Many PDF files (those corresponding to INRIA research reports)
		have been reformatted, so as to obtain a well-centered title
		page.

IMPROVEMENT
Number:		1147
Date: 		Tue Oct 17 11:49:48 MEST 2006
Report:		David Champelovier (INRIA/VASY)
Author:		Hubert Garavel (INRIA/VASY)
Files:		INSTALLATION_2

Nature:		The installation guidelines for Windows have been updated to
		specify that the CADP software must be installed on the same
		disk as the Windows operating system itself. Usually, Windows
		is installed on "C:", so should be CADP (installing CADP on
		another disk, such as "E:" will not work).

IMPROVEMENT
Number:		1148
Date: 		Tue Oct 17 18:56:42 MEST 2006
Author:		Frederic Lang (INRIA/VASY)
Files:		doc/*/Lang-06.*, doc/=READ_ME.txt, doc/biblio.bib

Nature:		A new paper on refined interface generation using EXP.OPEN
		and SVL was added in the "doc" directory of the CADP toolbox.

BUG FIX
Number:		1149
Date: 		Fri Oct 20 14:22:24 MEST 2006
Report:		David Champelovier (INRIA/VASY)
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		com/bcg_draw, com/bcg_info, com/bcg_open, com/caesar.open,
		com/exp.open, com/seq.open, com/svl, com/tst, 
		src/com/cadp_basename, src/com/cadp_edit,
		src/com/xeuca_convert, src/svl/standard 

Nature:		Under Solaris, SVL did not detect the presence of ".err" error
		files generated by CAESAR.ADT and CAESAR if the "basename"
		command found in the $PATH was "/usr/bin/basename" instead of
		"/usr/ucb/basename" or "/usr/xpg4/basename". This was caused
		by the fact that "/usr/bin/basename" interprets its second
		argument as a regular expression, not a string. This bug was
		fixed.

		A new shell-script "cadp_basename" was added, which addresses
		this issue by ensuring that "/usr/bin/basename" will not be
		invoked on Solaris. Consequently, all the CADP shell scripts
		have been modified to invoke "cadp_basename" instead of
		"basename" whenever needed.

		The "tst" shell-script has been enhanced to emit a warning
		if neither "/usr/ucb/basename" nor "/usr/xpg4/basename" are
		available on a Solaris machine.

BUG FIX
Number:		1150
Date: 		Mon Oct 23 10:08:10 MEST 2006
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		com/tst

Nature:		The "tst" shell-script was modified to avoid an error on
		Solaris machines working with a non-English language (e.g.,
		French-speaking versions of Solaris).

IMPROVEMENT
Number:		1151
Date: 		Mon Oct 23 11:41:03 MEST 2006
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		INSTALLATION_2, com/tst, com/installator

Nature:		The installation directives have been simplified: it is no
		longer required to set the $LD_LIBRARY_PATH variable on
		Solaris machines (Sun's documentation even discourages using
		$LD_LIBRARY_PATH in production software, as this can result
		in an overall performance degradation).

		The checks performed by the "tst" shell-script regarding the
		setting of $LD_LIBRARY_PATH have been adapted accordingly.
		The "installator" shell-script was also modified.

BUG FIX
Number:		1152
Date: 		Wed Oct 25 15:12:17 MEST 2006
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		com/upc, src/com/cadp_cc, src/com/cadp_indent,
		src/com/cadp_postscript, src/com/cadp_psbox, src/com/cadp_web

Nature:		A minor bug was fixed in several CADP shell-scripts (variable
		$PATH was set but not exported).

BUG FIX
Number:		1153
Date: 		Thu Oct 26 14:46:49 MEST 2006
Report:		Reza Pulungan (Saarland University, Germany),
		Jan Friso Groote (Technical Univ. Eindhoven, The Netherlands)
Authors:	Hubert Garavel and David Champelovier (INRIA/VASY)
Files:		com/tst

Nature:		The "tst" shell script was enhanced in four ways:

		- On Solaris, when $CADP_CC is not set and "/opt/SUNWspro/bin"
		  is not in the $PATH, "tst" no longer emits an error message
		  "cc" not found".

		- When "$CADP/com" and/or "$CADP/bin.*" are missing from the
		  $PATH, "tst" no longer emits a sequence of warnings of the
		  form:
		  > *** The tool ``bcg_draw'' is not searched in ``$CADP/com''
		  >     but in ``'' instead
		  >     You might have two versions of CADP installed
		  > ==> Reorder your ``$PATH'' variable to have ``$CADP/com''
		  >     first and remove all obsolete versions of CADP, if any

		- On Windows, "tst" now detects the case where "$CADP" contains
		  a Cygwin-specific mount point (such as "/cygdrive/c/...")
		  and emits a warning message, as CADP programs will not
		  understand Cygwin conventions because they are pure Win32
		  applications.

		- On Opteron machines running Linux, "tst" now emits a proper
		  warning message if the 32-bit developement library is not
		  installed.

BUG FIX
Number:		1154
Date: 		Thu Oct 26 16:12:22 MEST 2006
Author:		Frederic Lang (INRIA/VASY)
Files:		src/svl/standard

Nature:		The "standard" shell-script for SVL was modified to avoid a
		bug that occurs with the Solaris "test" command, which fails
		when executing the following command:
			A="(" ; if test "$A" = "("; then echo 0; fi
		Note that this problem does not occur on Linux.

BUG FIX
Number:		1155
Date: 		Thu Oct 26 18:57:43 MEST 2006
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		com/rfl

Nature:		The "rfl" shell-script was modified so as to remove all "r"
		characters that remained in license files generated on Windows.

IMPROVEMENT
Number:		1156
Date: 		Fri Oct 27 17:06:23 MEST 2006
Report:		Tomas Barros (Universidad Diego Portales, Santiago, Chile)
Authors:	Hubert Garavel, Frederic Lang, and Marie Vidal (INRIA/VASY)
Files:		bin.*/bcg_labels, man/*/bcg_labels.*, 
		src/eucalyptus/eucalyptus.tcl

Nature:		Two new options "-parse" and "-unparse" have been added to
		BCG_LABELS. See the corresponding man page for details.
		The EUCALYPTUS graphical interface was enhanced so as to
		give access to these options.

		Additionally, a mistake was fixed in EUCALYPTUS: when clicking
		on "Disable parsing of BCG labels", TGV was invoked with
		"-parse" option instead of "-unparse". This issue was fixed.

BUG FIX
Number:		1157
Date: 		Mon Oct 30 10:17:08 MET 2006
Report:		Juan Jose Sanchez Penas (University of Corunha, Spain)
Authors:	Hubert Garavel and Wendelin Serwe (INRIA/VASY)
Files:		src/eucalyptus/eucalyptus.tcl

Nature:		On computer screens with 1024x768 pixels only (such as 14''
		laptops screens), the "Reduce" window of EUCALYPTUS (for
		labelled transitions systems) was too high; thus, the "OK"
		button located at the window bottom could not be accessed.
		the contents of this window have been compacted so as to 
		reduce its height. 

BUG FIX
Number:		1158
Date: 		Mon Oct 30 11:10:03 MET 2006
Report:		Radu Mateescu (INRIA/VASY)
Author:		Marie Vidal (INRIA/VASY)
Files:		./src/bcg_draw/bcg_draw_header.ps

Nature:		Using BCG_EDIT, there was a problem with arrow heads inclined
		at 45 degrees exactly: the arrow heads would disappear in a
		random way, from the screen and/or printed PostScript material.
		This issue (an incorrect test to decide whether two vertices
		overlap or not) was solved.

IMPROVEMENT
Number:		1159
Date: 		Mon Oct 30 12:36:34 MET 2006
Report:		David Champelovier (INRIA/VASY)
Authors:	Hubert Garavel and Frederic Lang (INRIA/VASY)
Files:		com/tst, com/upc, src/com/cadp_echo, src/svl/standard

Nature:		Under Solaris, the command "/bin/echo" has a different
		behaviour than "echo" on all other architectures supported
		by CADP: it does not understand the "-n" option (see items
		#433 and #435 above) and interprets octal characters such
		as '015'. But its exists a Solaris command, "/usr/ucb/echo"
		with the desired behaviour.

		A new shell-script "cadp_echo" was added, which addresses
		this issue by ensuring that "/usr/ucb/echo" will used when
		needed. A few CADP shell scripts have been modified to invoke
		"cadp_echo" instead of "echo".

		The "tst" shell-script has been enhanced to emit a warning
		if "/usr/ucb/echo" is missing from a Solaris machine.

IMPROVEMENT
Number:		1160
Date: 		Thu Nov 16 19:18:00 MET 2006
Report:		Yaroslav Usenko (Technical Univ. of Eindhoven, The Netherlands)
Author:		Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_postscript

Nature:		Support for the Evince PostScript viewer has been added to
		BCG_DRAW and BCG_EDIT.

BUG FIX
Number:		1161
Date: 		Thu Nov 30 12:30:38 MET 2006
Author:		David Champelovier (INRIA/VASY)
Files:		incl/X_ACTION.h, incl/X_BIT.h, incl/X_BOOLEAN.h

Nature:		A minor bug was fixed in the include files that implement
		LOTOS sorts directly in C. The following macro-definitions
		   #define CAESAR_ADT_BITS_ACTION : 1
		   #define CAESAR_ADT_BITS_BIT : 1
		   #define CAESAR_ADT_BITS_BOOL : 1
		have been replaced with
		   #define CAESAR_ADT_BITS_ADT_ACTION : 1
		   #define CAESAR_ADT_BITS_ADT_BIT : 1
		   #define CAESAR_ADT_BITS_ADT_BOOL : 1

BUG FIX
Number:		1162
Date: 		Thu Nov 30 12:41:58 MET 2006
Author:		David Champelovier (INRIA/VASY)
Files:		incl/X_ACTION.h, incl/X_BIT.h, incl/X_BOOLEAN.h

Nature:		The three following C types implementing external LOTOS sorts:
		   ADT_ACTION, ADT_BIT, and ADT_BOOL
		have been implemented as "unsigned char" instead of "char".

BUG FIX
Number:		1163
Date: 		Thu Nov 30 12:52:52 MET 2006
Author:		David Champelovier (INRIA/VASY)
Files:		src/com/cadp_which

Nature:		Due to a bug in the "cadp_which" shell-script (the "macOS"
		architecture was incorrectly handled as "sun5" whereas it
		should be handled as "iX86"), the "tst" command would emit
		strange error messages if Ghostview was not installed:
		   $CADP/src/com/cadp_which: line 1: type: gs: not found

BUG FIX
Number:		1164
Date: 		Thu Nov 30 13:08:31 MET 2006
Report:		Christophe Joubert (University of Malaga, Spain)
Authors:	David Champelovier and Hubert Garavel (INRIA/VASY)
Files:		src/com/cadp_shell, com/tst

Nature:		On Linux systems for which the standard shell "/bin/sh" is a
		link to "dash" instead of "bash" (e.g., Linux Ubuntu Edgy 6.10
		or Linux Kubuntu Edgy 6.10), the Installator assistant would
		freeze on its first screen (the "Next" button not being
		clickable). This problem was solved.

		Additionally, the "tst" shell-script was modified to display
		the system shell (sh, bash, dash, etc.).

BUG FIX
Number:		1165
Date: 		Thu Nov 30 16:20:14 MET 2006
Authors:	Radu Mateescu and Gwen Salaun (INRIA/VASY)
Files:		demos/demo_40/commerce_p2.mcl,
		demos/demo_40/negociation_p2.mcl

Nature:		Two mu-calculus formulas for demo_40 (Web service) have been
		corrected (previously, these formulas always evaluated to
		true). 

BUG FIX
Number:		1166
Date: 		Mon Dec 11 17:40:22 MET 2006
Author:		Radu Mateescu (INRIA/VASY)
Files:		demos/demo_24/co4.lotos

Nature:		A minor bug (extra ".lib" suffix in a "library" ... "endlib"
		directive) was fixed in file "co4.lotos".

VERSION 2006 "Edinburgh"
Copyright (C) INRIA 2007 - Tous droits réservés - All Rights Reserved.

Back to the CADP Home Page