Mon 31 Jul NuSMV team <nusmv@irst.itc.it> 
	* === Released version 2.4.0 ===
	

Thu 27 Jul 2006 16:04:01 Roberto Cavada <cavada@irst.itc.it>
	* configure.ac 
	Removed unused dependency with bsd library (was not used, but
	requested)

Wed 26 Jul 2006 Roberto Cavada <cavada@irst.itc.it>
	* doc/user-man/syntax.tex 
	Added some text to document where IVAR are not allowed to occur. 

Wed 26 Jul 2006 Roberto Cavada <cavada@irst.itc.it>
	* src/enc/be/BeEnc.c src/bmc/bmcSatTrace.c
	BUG FIX
	Due to a bug in BMC counter-example construction, be vars indices
	were still assumed to be > 0
	
	* src/compile/compileFlatten.c
	BUG FIX
	Array indices are checked to be atomic constants

	* src/bmc/sbmc/sbmcBmcInc.c 
	BUG FIX
	This bug fix makes the command check_ltlspec_sbmc_inc re-entrant wrt ctrl+c
	(A similar bug fix for non incremental command has been already
	committed)

	* doc/user-man/{inter.tex,main.bib}
	* doc/user-man/cmd/{check_ltlspec_sbmc.tex,check_ltlspec_sbmc_inc.tex,gen_ltlspec_sbmc.tex}
	Added docs of new commands and options for SBMC

	* src/bmc/sbmc/sbmcTableauLTLformula.c
	BUG FIX
	Added a fallback behaviour to the il-opt algorithm for the case
	k=0

	* src/bmc/sbmc/sbmcUtils.c 
	BUG FIX
	Fixed creation/destruction of the loop var layer.
	The bug occurred if the user interrupted the execution (ctrl+c) of
	sbmc commands. 

Tue 25 Jul 2006	Roberto Cavada <cavada@irst.itc.it>
	* src/enc/be/BeEnc.c 
	BUG FIX
	Physical indices for BE vars were created starting from 1 instead
	of 0

	* src/bmc/{bmcDump.c,bmcSatTrace.c}
		* src/bmc/sbmc/sbmcUtils.c
	* src/be/{be.h,beRbcManager.c}
	* src/rbc/rbcCnf.c 
	BUG FIX
	Having BE variables with index 0 occurring in CNF was not allowed. 
	Fixed by hiding the way BE indices are associated to BE literals. 
	Thanks to [MB] for double checking the fix. 

	* src/compile/type_checking/TypeChecker.c 
	PERFORMANCE 
	Changed complexity of type checking of enumerations from O(N*N) to 
	at most	O(N*lgN). This *makes* the difference when relatively big
	number of constants are used (see for example the test for
	bug_155)

	* src/utils/NodeList.c
	BUG FIX
	When the underlying list is shared, it is no longer destroyed by 
	the class destroyer. 

Fri 21 Jul 2006	Charles Arthur Jochim <jochim@irst.itc.it>
	* configure.ac 
	Add flag to enable/disable readline at configuration time.
	
Wed 19 Jul 2006	Roberto Cavada <cavada@irst.itc.it>
	* src/utils/{error.c,error.h}
	* src/parser/grammar.y
	* src/enc/utils/AddArray.c
	* src/fsm/sexp/SexpFsm.c 
	* src/enc/operators.c 
	* src/compile/{compile.h,compileBEval.c,compileWrite.c}
	* src/bmc/sbmc/sbmcBmc.c,sbmcUtils.c}
	* src/nmb{bmcBmcInc.c,bmcBmcNonInc.c,bmcConv.c,bmcTest.c}
	* src/node/printers/PrinterWffCore.c 
	* src/node/{node.h,nodePrint.c}
	BUG FIX
	Partially fixed the inconsisten behaviour when compiling 
	(possibly) not exhaustive CASEs expression into either BDD or BE:
	With BDDs it is possible to detect correctly bad CASEs and report them 
	to the user, whereas with BEs only a syntactical analysis is performed 
	at the moment, so it is not always possible (for release 2.4.0) 
	to distinguish between right cases and not-exhaustive cases. 

	When BEs (BMC) are used, a warning is printed in ambiguous cases. 
	
	* src/enc/bdd/{BddEnc.c,BddEnc.h,BddEnc_private.h}
	NEW FEATURE
	Added public methods 'add_to_expr' and 'bdd_to_expr' to the class BddEnc
	(Thanks to <thiagocarvalho@yahoo.com> for requesting it. 

Mon 17 Jul 2006	Roberto Cavada <cavada@irst.itc.it>
	* src/parser{grammar.y,input.l,symbols.h}
	* node/printers/PrinterWffCore.c 
	* src/node/nodePrint.c 
	* src/fsm/sexp/{SexpFsm.c,SexpFsm.h}
	* compile/type_checking/checkers/{CheckerCore.c,CheckerPsl.c,CheckerStatement.c}
	* src/compile/{compileCmd.c,compileFlatten.c,compileWrite.c}
	NEW GRAMMAR STATEMENT
	Added a new statement at SMV grammar level: CONSTANTS
	The new statement allows a user (or a generator) to make NuSMV 
	declar  e a set of symbolic constants when flattening a SMV file. 
	This makes it posssible to parse a file that contains DEFINEs whose 
	body refer to symbolic constants values that do not occur into VARS
	ranges. This is the case of SMV files generated by the command 
	write_boolean_model that dumps boolean variables as VARS, and 
	each scalar variable as a DEFINEs whose body is the boolean encoding
	of the scalar variable (to help reading counter-examples, simulation, 
	etc. as the user can still reason with scalar values even when
	working with a purely booleanized model)
	Dumping of CONSTANTS is conditioned to the value of the system variable
	backward_compatibility.
	
	* src/opt/{opt.h,optCmd.c,optInt.h}
	OPTION RENAMING
	Renamed system variable 'type_checking_backward_compatibility' to 
	'backward_compatibility'

	* src/sm/smMain.c
	NEW CMDLINE OPTION
	Added new command line option '-old' to control the variable 
	'backward_compatibility' in batch mode

	* src/compile/compileBEval.c
	BUG FIX
	Determinization variables are now declared as STATE variables
	instead of INPUT vars, as determinization happens at state level, 
	and not at transition level. This allows determinization vars to 
	stay into INITs and INVARs as it may happen when booleanized 
	models are written and then need to be re-parsed. 

	* src/compile/{compile.h,compileUtil.c}
	* src/ltl/ltl2smv/ltl2smvMain.c 
	* src/prop/propProp.c
	NEW FEATURE
	Added function:
	 node_ptr Compile_pop_distrib_ops(node_ptr prop) 
	 ... that simplifies the given property by exploiting the
	 distributivity of G, AG and H over AND, and distributivity of F, AF
	 and O over OR:
	    1) <OP> <OP> a           :-> <OP> a
	    2) (<OP> a) * (<OP> b)   :-> <OP> (a * b);
	    3) (<OP> (a * <OP> b))   :-> <OP> (a * b);
	    4) (<OP> (<OP> a * b))   :-> <OP> (a * b);
	    5) (<OP> (<OP> a * <OP> b)) :-> <OP> (a * b); 
	   Where <OP> can be either:
	        G|AG|H for * := &
		F|AF|O for * := |

Tue 11 Jul 2006	Roberto Cavada <cavada@irst.itc.it>
	* src/parser/psl/psl_grammar.y 
	* src/node/printers/PrinterPsl.c 
	BUG FIXES
	1. "G Sequence" is no longer a parsable PSL property 
	   (accordingly to the grammar provided by IBM)
        2. always, never and eventually! are now printed correctly when
	   printing a following PSL Sequence
        3. Removed nested {} when printing SEREs
	
Mon 10 Jul 2006 Roberto Cavada <cavada@irst.itc.it>
	* src/compile/{compile.h,compileCmd.c,compileStruct.c}
	BUG FIX
	Changed the behaviour of the command flatten_hierarchy when it fails:
	now it resets also the result of the command read_model to allow the
	user to fix the model and then re-read when working in interactive
	mode.

Fri 7 Jul 2006 Roberto Cavada <cavada@irst.itc.it>
	* src/parser/psl/pslConv.c 
	BUG FIX
	Conversion of PSL -> LTL was not handling the operator 'until!'
	(until bang) 

Mon 3 Jul 2006 Roberto Cavada <cavada@irst.itc.it>
	* src/sm/smMain.c
	FEATURE
	Reachable states are now computed by default (i.e. command line option 
	-f is set by default)
	+ New command line option -df is provided to prevent the computation
	+ Docs have been changed accordingly

Mon 12 Jun Marco Roveri <roveri@irst.itc.it>
	* src/bmc/sbmc/...
	First porting of the Incremental SBMC by Tommi Juntilla, Timo
	Latval. Helianko published in CAV 05.

Thu 1 Jun 2006 Marco Roveri <roveri@irst.itc.it>
	* src/dd/{dd.h,dd.c}
	Added a function bdd_get_one_sparse_sat that returns one satidfying
	assignment for a BDD (i.e. a path from the root to the leaf 1).

	* src/compile/compileWrite.c
	BUG FIX #397
	Now fairness conditions FAIRNESS a & b are printed by the 
	write flat model as FAIRNESS a & b instead of the wrong:
	 FAIRNESS a 
         FAIRNESS b

	* src/ompile/compileCheck.c
	BUG FIX #314
	We cover also the hierarchy. Before only next of input variables
	in the rhs of next assign where detected only if they where
	occurring in the top level module (main).

Mon 29 May 2006 Roberto Cavada <cavada@irst.itc.it>
	* src/sm/smInit.c
	* src/ltl/ltl.c 
	BUG FIX
	Fixed a couple of memory leaks. Thanks to [AT] for profiling and
	finding these bugs.

Fri 26 May 2006	Roberto Cavada <cavada@irst.itc.it>
	* src/compile/compileFlatten.c 
	BUG FIX #393
	When there is name clashing between a variable and a formal
	parameter, this error message is printed (and the execution
	prevented from continuing): file <FILE>: line <N>: variable
	"<NAME>" shadows formal parameter
	
Fri 19 May 2006 Roberto Cavada <cavada@irst.itc.it>
	* src/compile/compileCmd.c 
	NEW COMMAND
	+ Added command print_fsm_stats
	+ Old command print_clusterinfo is still supported, but documented as 
	  deprecated in 2.4
	+ Added docs for the new command 

	* src/mc/mcMc.c 
	* src/prop/{prop.h,propProp.c}
	* doc/user-man/syntax.tex
	* doc/user-man/cmd/compute.tex 
	BUG FIX #315
	+ Fixed MAX behaviour when any of initial or final states is empty. 
	+ Added value undefined to COMPUTE specifications
	+ Fixed docs
	+ Added warning during MAX computation for: 
	  - initial states empty
	  - final states empty
	  - empty fair states
	
	* src/compile/compileCmd.c
	* src/opt/optCmd.c 
	* src/sm/smInit.c 
	* doc/user-man/cmd/process_model.tex
	BUG FIX #394
	+ Fixed re-enabling of dd dynamic reordering after reset when
	  previously enabled.
	+ removed system variable 'enable_reorder' at user level
	+ added option -r to the command 'process_model' to force 
	  reordering and dumping of vars order. 
	+ fixed docs accordingly
	
Thu 18 May 2006 Roberto Cavada <cavada@irst.itc.it>
	* src/prop/propCmd.c 
	BUG FIX #313
	Added PSL support to commands {check,add}_property (added option -s)

Mon 15 May 2006	Roberto Cavada <cavada@irst.itc.it>
	* src/node/node.{c,h}
	BUG FIX #311
	Fixed lineno overflow

	* src/parser/parserUtil.c 
	BUG FIX #318
	Fixed reentrancy of parsing function. Exception is catched and 
	parser status is reset. 

Fri 12 May 2006	Roberto Cavada <cavada@irst.itc.it>
	* src/sim/{simClause.c,simInt.h}
	BUG FIX #175
	Fixed integer overflow. Still to be tested.

Tue 9 May 2006 Marco Roveri <roveri@irst.itc.it>
	* src/parser/grammar.y 
	FEATURE
	Allowed the declaration of array of modules.

Tue 11 Apr 2006	Roberto Cavada <cavada@irst.itc.it>
	* src/fsm/sexp/SexpFsm.{h,c}
	FEATURE
	Changed class SexpFsm in order to provide a better mechanism to 
	build FSMs on the fly. 
	It is now possbile to derive a SexpFsm f2 from a SexpFsm f1, by 
	changing parts of f2 and keeping f1 unchanged. 

	Method create_from_members has been removed, and constructor
	makes use of the FlatHierarchy structure to pass FSM data. 

	FlatHierarchy has been exptended to allow developers to copy, modify 
	and derive an existing instance into another instance that will 
	eventually be used to create a new FSM chain. 

Tue 4 Apr 2006 Roberto Cavada <cavada@irst.itc.it>
	NEW FEATURES
	+ Plugged in support for PSL at system level 
	  - type checker supports now psl through a checker for PSL nodes
	  - psl formulae are still converted to a core-compliant parse tree for 
	    model checking and dependency finding
	+ Provided a generic architecture to support grammar extensions

Mon 13 Feb 2006	Andrei Tchaltsev <tchaltsev@irst.itc.it>
	* /src/sm/smMisc.c
	CODE REWRITING
	The batch mode was implemented as a list of functions which performed
	the required actions.
	Now the batch mode is a list of commands.


Mon 13 Feb 2006 Roberto Cavada <cavada@irst.itc.it>
	* src/sm/smMain.c
	DOC FIX
	Fixed references to the zchaff home page. 
	Thankt to Roopsha <roopsha@ece.utexas.edu> for reporting it. 

Thu 12 Jan 2006 Andrei Tchaltsev <tchaltsev@irst.itc.it>
	* src/ltl/ltl.c 
	BUG FIX
	Ltl_CheckLtlSpec function did not re-throw a caught exception but just 
	returned.

Fri 7 Oct 2005 Andrei Tchaltsev <tchaltsev@irst.itc.it>
	* src/compile/type_checking/PredicateNormaliser.{h,c}
	NEW FEATURE
	A new class PredicateNormaliser is created (in src/compile).
	This class can take an symbolic expression (Sexp_ptr) and normalise
	predicates in it. A predicate-normalised expression is an expression
	whose not-boolean subexpression (predicate) cannot have boolean operands.
	Also a symbolic FSM class (src/fsm/sexp) was updated: now it has 
	a new constructor which takes a symbolic FSM and a predicate-normaliser
	and returns a new symbolic FSM with all constrains (INIT, TRANS and INVAR)
	already normalised.

Fri 9 Sep 2005 Andrei Tchaltsev <tchaltsev@irst.itc.it>
	* src/sm/smMain.c 
	NEW COMMAND LINE OPTION
	A new command line option "-old_div_op" is enabled.
	This option switches from the "new" ANSI C semantics of division and remainder
	operators to the old one used in NuSMV 2.3.1 and earlier.

Tue 24 May 2005	Andrei Tchaltsev <tchaltsev@irst.itc.it>
	* src/enc/utils/AddArray.{h,c}
	NEW CLASS
	A new class AddArray is created in enc/utils module.
	This class is used during BDD evaluation to deal with arrays of ADD.
	Except ADD arrays primitives, this class also has functions to perform
	Word operations on arrays of boolean values. 

	* src/sm/smMain.c
	NEW COMMAND LINE OPTION
	Added a new option "-word_mono". With this flag Words are encoded as
	a signle ADD. Without this flag Words are encoded as 
	arrays of boolean values.

	* src/opt/{opt.h,optCmd.c,optInt.h}
	NEW VARIABLE
	A new variable encode_word_monolithic is added.  Its true value means that
	one ADD is used to encode a Word expression, whereas false value means
	that an array of ADD will be used (one for every bit).
	
Thu 21 Apr 2005 Andrei Tchaltsev <tchaltsev@irst.itc.it>
	* src/opt/{opt.h,optCmd.c,optInt.h}
	NEW VARIABLE
	A new system variable "output_word_format" is added.
	Possible values are 2, 8, 10, 16.
	This variable specifies how (in what base) Word numbers are printed out
	during traces outputting, counterexamples, etc.

Mon 4 Apr 2005 Andrei Tchaltsev <tchaltsev@irst.itc.it>
	* src/enc/bdd/BddEnc.c
	NEW FEATURE
	Word type is added to evaluation and some other parts of NuSMV.
	Further changes are expected soon.


Tue 15 Feb 2005 Andrei Tchaltsev <tchaltsev@irst.itc.it> 
	* src/compile/type_checking
	Here is the first full version of the type checking package.

Wed 9 Feb 2005 Andrei Tchaltsev <tchaltsev@irst.itc.it> 
	* src/opt/{opt.h,optCmd.c,optInt.h}
	NEW FEATURE
	There are two new environment variables:
	+ "backward_compatibility" 
	+ "type_checking_warning_on"

Fri 14 Jan 2005 Roberto Cavada <cavada@irst.itc.it>
	* src/be/{be.h,beRbcManager.c}
	* src/rbc/{rbc.h,rbcSubst.c}
	* src/enc/be/BeEnc.c
	NEW FEATURE
	Added logical level to BEs at BeEnc level

Tue 11 Jan 2005 Andrei Tchaltsev <tchaltsev@irst.itc.it> 
	* src/parser/{grammar.y,input.l,symbols.h}
	NEW FEATURE
	Modified parser and lexer to deal with new type "word" and its associated 
	operators (<<, >>, <<<, >>>, ::, [:]).

Mon 10 Jan 2005	Roberto Cavada <cavada@irst.itc.it>
	* src/enc/be
	First shot of class BeEnc.

Wed 24 Nov 2004	Roberto Cavada <cavada@irst.itc.it>
	* src/enc/base/{BaseEnc.c,BaseEnc.h,BaseEnc_private.h}
	* src/enc/base/{BoolEncClient.c,BoolEncClient.h,BoolEncClient_private.h}
	* src/enc/bool/{BoolEnc.c BoolEnc.h BoolEnc_private.h}
	NEW CLASSES
	+ BaseEnc is the abstract pure base class for all the encodings
	+ BoolEncClient is the abstract purebase class for all the encodings 
	  that need an instance of BoolEnc to operate. 
        + BoolEnc handles the booleanization of variables, and keeps track 
	  of the var <-> bool encoding relation.

	
Tue 28 Sep 2004 Roberto Cavada <cavada@irst.itc.it>
	NEW CLASS
	* src/compile/symb_table/{SymbLayer.c SymbLayer.h SymbTable.c SymbTable.h}
	Added class SymbTable, as a collection of Layers.

	

Mon 21 Nov NuSMV team <nusmv@irst.itc.it> 
	* === Released version 2.3.1 ===
	
Fri 18 Nov 2005 12:37:51 Roberto Cavada <cavada@irst.itc.it>
	* Makefile.am configure.ac
	Integrated new zchaff helper directory
	Default used zchaff version is now 2004.11.15

Fri 18 Nov 2005 10:38:06 Roberto Cavada <cavada@irst.itc.it>
	* ../zchaff
	Improved integration with zchaff.
	Like Minisat, zchaff is now compiled into a dedicated directory. 
	scripts are provided to help the user to unpack, patch and compile
	zchaff. 

Wed 16 Nov 2005 11:44:40 Simone Semprini <semprini@irst.itc.it>
	* src/parser/psl/{pslConv.c,pslInt.h,pslNode.c,pslNode.h}
	BUG FIX
	Fixed forall expansion of PSL formulae, moving it earlier in the
	PSL compilation process.

Wed 16 Nov 2005 14:38:52 Roberto Cavada <cavada@irst.itc.it>
	* src/utils/portability.{h,c} src/ltl/ltl2smv/main.c
	PORTABILITY 
	Added 
	- portability module to package utils
	- some code into ltl2smv/main.c for the sake of portability
	Now nusmv can be cross-compiled (at least for mingw...)
	
Wed 16 Nov 2005 09:40:32 Roberto Cavada <cavada@irst.itc.it>
	* src/dd/dd.h
	BUG FIX
	Fixing a few wrong declations (param type add_ptr used instead 
	of bdd_ptr).
	Thanks to Ittai Balaban <ittaibalaban@gmail.com> for reporting the
	bug. 
	
Tue 15 Nov 2005 17:31:44 Roberto Cavada <cavada@irst.itc.it>
	* configure.ac 
	BUG FIX
	Fixed a few configuration tests about zchaff and minisat.

Tue 15 Nov 2005 15:02:02 Roberto Cavada <cavada@irst.itc.it>
	* src/opt/opt.h
	FEATURE
	Minisat is the default sat solver when available (ported from 2.4)

Tue 15 Nov 2005 14:40:28 Roberto Cavada <cavada@irst.itc.it>	
	* Makefile.am
	BUG FIX
	'make dist' failed on automake >= 1.7, as generated files were 
	expected to be distributed. (ported from 2.4)

Tue 15 Nov 2005 14:34:26 Roberto Cavada <cavada@irst.itc.it>
	* src/sm/smInit.c 
	BUG FIX
	The command 'reset' reset also ordering file variable to a 
	default value. 'reset' does not modify input_order and 
	output_order variables anymore. (ported from 2.4)

Tue 15 Nov 2005 13:48:57 Roberto Cavada <cavada@irst.itc.it>
	* src/trace/plugins/{TraceXmlDumper.c,TraceXml_private.h}
	FEATURE
	The Xml dumper plugin dumps loops information now. (ported from
	2.4)

Tue 15 Nov 2005 13:48:12 Roberto Cavada <cavada@irst.itc.it>
	* README.MiniSat Makefile.am configure.ac src/sm/smMain.c 
	FEATURE 
	NuSMV now uses Minisat-1.14. 

Tue 15 Nov 2005 09:15:01 Roberto Cavada <cavada@irst.itc.it>
	* src/cmd/cmdMisc.c src/sm/smMain.c
	BUG FIX
	When an error occurs during command execution (in interactive
	mode) and the flag on_failure_script_quit is set, nusmv exists now
	with the value 1. (ported from 2.4)

	
Mon 14 Nov 2005 15.30 Roberto Cavada <cavada@irst.itc.it>
	* src/sm/smMain.c
	Added command line option "sat_solver" that allows to specify 
	the SAT solver to be used in batch mode. 
	Many thanks to Guido Wimmel <wimmel@in.tum.de> for providing 
	the code to handle the option. 
	
Thu 10 Nov 2005 09:08:31 Marco Roveri <roveri@irst.itc.it>
	* src/ltl/ltl.c
	BUG FIX
	Fixed problem with COI when only LTL properties are present in the
	SMV file. The COI structure were wrongly initialized due to the
	push/pop mechanism to implement LTL BDD based model checking.
	The problem does not occur in the version 2.4.
	Thanks to Kevin Xuke <xk02@mails.tsinghua.edu.cn> for reporting
	this bug.

Tue, 13 Sep 2005 14:37:10  Roberto Cavada <cavada@irst.itc.it>
	* src/parser/input.l src/parser/psl/psl_input.l 
	PORTABILITY FIX
	Upcased yy_current_buffer for the sake of portability with
	different flex versions.

Fri 2 Sep 2005 10:21:25	Roberto Cavada <cavada@irst.itc.it> SimoneSemprini <semprini@irst.itc.it>
	* src/parser/psl/pslNode.c 
	BUG FIX
	Fixed a bug that made expressions like LTL * SERE not correctly
	converted to LTL, as the tree was not travesed correctly by 
	is_ltl and is_obe predicates. 

Tue 30 Aug 2005 12:01:09 Roberto Cavada <cavada@irst.itc.it>
	* src/enc/symb/Encoding.c src/utils/error.{c,h}
	BUG FIX
	The actual existance of vars ordering input file is now checked. 
	Previously, when the file was not found stdin was used instead. 

Mon 22 Aug 2005 08:29:07 Andrei Tchaltsev <tchaltsev@irst.itc.it>
	* src/fsm/bdd/{BddFsm.c,BddFsmCache.c,bddInt.h}
	BUG FIX
	Fixed bug in BddFsm_get_strong_backward_image: the function
	bdd_fsm_get_backward_si_projection computed legal states/input
	without caring for invariants.
	In BddFsm_get_strong_backward_image I also removed unnecessary
	conjunctions with invariants since they are performed in
	BddFsm_get_weak_backward_image.
	Function bdd_fsm_get_backward_si_projection was fixed and renamed to
	bdd_fsm_get_legal_state_input (more understandable name). Also a
	variable backward_projection (which hold the result of
	bdd_fsm_get_backward_si_projection) was renamed to
	legal_state_input.



Fri 15 Jul 2005 17:00:00 NuSMV team <nusmv@irst.itc.it> 
	* === Released version 2.3.0 ===

	
Fri 15 Jul 2005 08:49:52 Roberto Cavada <cavada@irst.itc.it>
	* src/fsm/bdd/BddFsm.c 
	Bug fix: the command check_fsm did not consider already computed
	reachable states when computation of reachable was not requested
	by specifying the option -f or by executing the interactive
	command compute_reachable.

Thu 14 Jul 2005 15:58:26 Roberto Cavada <cavada@irst.itc.it>
	* src/parser/psl/pslConv.c
	Bug fix, feature
	- Extended subtitution in replicator
	- Nested replicators with same IDs are no longer allowed. 
	
Fri 8 Jul 2005 10:48:38 Simone Semprini <semprini@itc.it>
	* src/parser/psl/{pslConv.c,pslInt.h,pslNode.c}
	- Integration of last functionalities regarding [*] and [+]
	  standalone not top level into new architecture
	- Varius extension to already existing functions
	- Some bug fixes
	- Some old functions removed
	- Some new functions added (renamed extension of old ones)	
	
Thu 7 Jul 2005 16:45:28 Roberto Cavada <cavada@irst.itc.it>
	* src/parser/psl/
	Package refactoring.
	- splitted psl_expr int a few separate modules:
	  - pslExpr: interface for the parser (PslExpr)
	  - pslNode: low level functions over PslNode
	  - pslConv: high level functions over PslNode (convertions)
	  - pslPrint: printing feature over PslNode

	Files psl_expr.{h,c} have been removed. 
	Since the interfaces are changed, other packages have been adjusted 
	accordingly: prop, compile	
	
Thu 7 Jul 2005 09:37:47 Roberto Cavada <cavada@irst.itc.it>
	* src/parser/psl/psl_expr.c
	Feature: nested suffix implications are now supported.
	
Wed 6 Jul 2005 11:14:07 Simone Semprini <semprini@itc.it>
	* src/parser/psl/psl_expr.c
	Bug fixes, refactoring
	- Extension of is_handled family of functions to deal with
          [*count] stand-alone and with [*] and [+] that are stand-alone but
          not top level (e.g. a;[*];b)
	- Treatment of stand-alone [+] complete
	- Treatment of [*] and [+] that are stand-alone but not top level
	  to be implemented
	
Tue 5 Jul 2005 16:55:02 Roberto Cavada <cavada@irst.itc.it> Simone Semprini <semprini@itc.it>
	* src/parser/psl/psl_expr.c
	Bug fixes, new feature
	- completed handling of * on propositionals
	- several bug fixes
	
Mon 4 Jul 2005 14:45:19 Roberto Cavada <cavada@irst.itc.it> Simone Semprini <semprini@itc.it>
	* src/parser/psl/psl_expr.{h,c}
	Bug fixes, new feature
	- In function PslNode_is_handled_sere: case TKCOMPOUND merged
	  conjuctions and disjunction.
        - Renamed PslNode_has_handled_sere to PslNode_is_handled_psl
	- Extended PslNode_is_handled_psl to deal with whilenot and other sere-based 
	  ops there were not dealt with. 
	
Mon 4 Jul 2005 09:35:56 Simone Semprini <semprini@itc.it>
	* doc/user-man/{syntax.tex,app_grammar.tex}
	- PSL part of user-man uptodate with grammar in PSL parser.
	- app_grammar.tex extended witl PSL grammar
	
Mon 4 Jul 2005 08:53:47 Fabio Barbon <barbonfab@itc.it>
	* src/parser/psl/psl_expr.c
	Fixed star handling according to [*] versus [*0] difference.
	
Thu 30 Jun 2005 15:44:59 Simone Semprini <semprini@itc.it>
	* src/parser/psl/psl_expr.c
	1. Completed translation of star-free sere.
	2. Extended recognition of handled subset for sere with star count and
	   star on propositionals (to be tested)
	3. Implemented translation of star count sere (to be tested)
	4. Partially implemented translation of star on propositionals
	
Wed 29 Jun 2005 09:52:35 Roberto Cavada <cavada@itc.it>
	* src/sm/sm{Main,Misc}
	Added command-line option -ips.

Wed 29 Jun 2005 09:18:09 Marco Roveri <roveri@itc.it>
	* examples/psl-samples
	Porting to PSL of some SMV files from the previous distribution.

Tue 28 Jun 2005 09:48:01 Simone Semprini <semprini@itc.it> 
	* doc/user-man/cmd
	Extensions to the user manual for PSL

Tue 28 Jun 2005 08:39:03 Roberto Cavada <cavada@itc.it>
	* src/parser/psl/spl_grammar.y
	A first cleanup of the psl grammar for the version being
	delivered. 

Mon 27 Jun 2005 14:46:39 Roberto Cavada <cavada@itc.it>
	* src/parser
	Integrated the PSL parser from branch 2.4

Fri 24 Jun 2005 15:12:07 Fabio Barbon <barbonfab@itc.it>
	* src/parser/psl
	Added code to translate SERE int LTL

Fri 24 Jun 2005 09:46:46 Marco Roveri Roberto Cavada <roveri,cavada}@itc.it>
	* src/parser/psl/psl_grammar.y
	* src/parser/grammar.y
	Bug fix: Fixed the handling of the IN context while interactive mode.
	
Wed 22 Jun 2005 15:03:46 Roberto Cavada <cavada@itc.it>
	* nusmv/src/bmc/{bmcBmc.h,bmcCmd.c,bmcCmd.h}
	Added psl model checking to batch mode. 

Wed 22 Jun 2005 14:03:52 Roberto Cavada <cavada@itc.it>	
	* src/prop/propDb.c
	Those psl properties that cannot be converted to ltl nor ctl, are now 
	allowed to be added to the prop db. 
	No model checking is allowed on them, though. 
	A warning will be issued when a property gets added under these
	conditions.

Wed 22 Jun 2005 13:34:26 Roberto Cavada <cavada@itc.it>	
	* src/prop/{propInt.h,propProp.c}
	Added lazy evaluation to property conversion psl->{ctl,ltl}

Mon 20 Jun 2005 15:16:36 Roberto Cavada <cavada@itc.it>	
	* src/mc/mcCmd.c
	Implemented a new command 'check_pslspec'

Fri 17 Jun 2005 12:23:26 Roberto Cavada <cavada@itc.it>	
	* src/prop/{propDb.c,propProp.c}
	PSLSPECs are now pushed within the PropDB like all other specs.

Tue 14 Jun 2005 16:57:28 Marco Roveri <roveri@itc.it>
	* src/parser/psl/psl_expr.c
	Expanded pslltl2ltl to expand forall cases.

Mon 6 Jun 2005 13:34:52	Marco Roveri <roveri@itc.it>
	* src/parser/psl/psl_expr.c
	Fixed a problem in the expansion of next_event_a|e

Wed 4 May 2005 07:52:10	Roberto Cavada <cavada@itc.it>	
	* src/parser/psl
	Added a  parser for PSL.

	

Thu May 05 2005 18:00:00  NuSMV team <nusmv@irst.itc.it> 
	* === Released version 2.2.5 ===

Wed May 5 15:20:43 2005 Roberto Cavada <cavada@itc.it>
	* src/trace/TraceManager.{h,c} 
	Added method is_plugin_internal to deal with a request by the 
	group sa-nusmv.
	
Wed May 4 16:56:52 2005 Roberto Cavada <cavada@itc.it>, Andrei Tchaltsev <tchaltsev@itc.it>
	* src/sm/smMain.c: NEW FEATURE (BUG FIX #183)
	Option -load now sets the interactive mode. 
	
Wed May 4 16:16:20 2005 Roberto Cavada <cavada@itc.it>,	Andrei Tchaltsev <tchaltsev@itc.it>
	* doc/tutorial/Makefile.am, doc/user-man/Makefile.am: BUG FIX #300
	Fixed incorrect indexing in the documentation.
	
Wed May 4 15:33:51 2005 Andrei Tchaltsev <tchaltsev@itc.it>
	* src/parser/parserUtil.c: BUG FIX
	Fixed a bug in generation of temporary files.
	
Tue May 3 14:38:37 2005 Roberto Cavada <cavada@itc.it>,	Andrei Tchaltsev <tchaltsev@itc.it>
	* src/simulate/simulateTransSet.c: BUG FIX
	A 'double' type was erroneously used instead of integer.
	
Tue May 3 14:35:43 2005 Andrei Tchaltsev <tchaltsev@itc.it>, Roberto Cavada <cavada@itc.it>
Tue Apr 19 17:55:49 2005 Marco Roveri <roveri@itc.it>
	* src/opt/optCmd.c, src/parser/parserUtil.c,
	* src/sm/smInit.c, src/sm/smMain.c, src/utils/utils.c: BUG FIX
	Fixed dealing with preprocessors, in particular, memory leaks,
	incorrect string copying, removal of temporary files.
	
Mon Apr 18 11:40:12 2005 Marco Roveri <roveri@itc.it>
	* src/opt/optCmd.c, src/sm/smMain.c: BUG FIX
	Fixed the setting of system variables for reachable states
	computation in interactive mode.
	
Tue Apr 12 10:16:27 2005 Marco Roveri <roveri@itc.it>
	* src/ltl/ltl2smv/lex.l: BUG FIX
	Fixed parsing of end-of-line under windows.
	Thanks to H. Peter Gumm for the bug report.
	
Thu Apr 7 11:16:48 2005 Roberto Cavada <cavada@itc.it>
	* src/simulate/{simulate.c, simulateTransSet.c,	simulateTransSet.h}:
	BUG FIX. Fixed wrong cast of double to int.
	Thanks to Alessandro Saiani for this bug report.
	
Tue Mar 22 17:28:25 2005 Marco Roveri <roveri@itc.it>
	* src/compile/compileCmd.c: BUG FIX #297
	This critical bug caused input constraints to be not included into a FSM 
	during model construction.
	

Thu 17 Mar 2005 18:00:00  NuSMV team <nusmv@irst.itc.it> 
	* === Released version 2.2.4 ===

Thu 17 Mar 2005 14:46:00 Roberto Cavada <cavada@itc.it>
        * src/simulate/simulateCmd.c: BUG FIX
	In commands pick_state and simulate, the option -a had an inverted
	semantics.
	
Tue 15 Mar 2005 17:35:32 Roberto Cavada <cavada@itc.it>
	* doc/user-man/{inter.tex,nusmv.sty}: Added description of new
	variables and options.
	* doc/user-man/{echo,write_order,source}.tex: Added description of new
	variables and options.

Mon 14 Mar 2005 13:42:48 Roberto Cavada <cavada@itc.it>
	* src/enc/symb/Encoding.c: Ported a bug fix back from 
	version 2.2.99.
	* src/enc/{enc.c,encInt.h}: Ported a bug fix back from 
	version 2.2.99.

Mon 14 Mar 2005 13:26:24 Roberto Cavada <cavada@itc.it>
	* src/bmc/{bmcInt.h,bmcUtils.h}: INTERFACE CHANGE 
	Moved function Bmc_Utils_generate_and_print_cntexample from
	internal interface bmcInt to the bmc.utils module interface
	bmcUtils.h as required by SA porting.

Mon 14 Mar 2005 13:20:46 Roberto Cavada <cavada@itc.it>
	* configure.ac: Changed version number to 2.2.4

Mon 14 Mar 2005 13:20:06 Roberto Cavada <cavada@itc.it>
	* src/simulate/{simulate.c,simulateTransSet.c}: BUG FIX #295 
	This fixes bug 295 *only* for 2.2.4, and must be ported to 2.2.99

Fri 11 Mar 2005 16:24:46 Roberto Cavada <cavada@itc.it>
	* src/sm/{smMain.c,smMisc.c}:
	* src/opt/{opt.h,optCmd.c,optInt.h}:
	* src/compile/compileCmd.c:
	* src/cmd/{cmdCmd.c,cmdMisc.c}:
	NEW FEATURES
	- New system variables:
	  - write_order_dumps_bits
          - on_failure_script_quits
	- New command options:
	   - Command write_order has options '-b'
	   - Command echo has options '-a' and '-o filename'

Fri 11 Mar 2005 16:17:17 Roberto Cavada <cavada@itc.it>
	* src/node/nodeWffPrint.c: BUG FIX
	Fixed a missing return statement. This bug has been back ported
	from 2.2.99

Tue 1 Mar 2005 12:29:51	Roberto Cavada <cavada@itc.it>
	* cudd-2.3.0.1/mtr/mtrGroup.c: BUG FIX CANDIDATE
	This is a bug fix candidate to allow groups to dissolve (required
	by 2.2.99) This has no effect on the 2.2.x series.

Tue 18 Jan 2005 14:56:13 Marco Roveri <roveri@itc.it>
	* src/fsm/bdd/BddFsm.c: BUG FIX
	Fixed problem in BddFsm_check_machine that wrongly printed out
	also inputs instead of only state variables while printing
	deadlock states.	

Thu 30 Dec 2004 09:47:51 Gavin Keighren <keighren@irst.itc.it> 
	* src/rbc/rbcFormula.c: BUG FIX
	Fxed ordering of sons during generation of RBC's IIF nodes. This
	fix slightly reduces the number of RBC nodes and corresponding CNF
	indexes.
	
Wed 29 Dec 2004 12:00:00  NuSMV team <nusmv@irst.itc.it> 
	* === Released version 2.2.3 ===

Tue 21 Dec 2004 15:49:44 Andrei Tchaltsev <tchaltsev@itc.it>
	* src/ltl/ltl.c: Fixed memory corruption due to uninitialized
	string.
	
15.12.2004 11:00 Andrei Tchaltsev <tchaltsev@itc.it>
	* examples/tcas/*.smv, examples/deadlock/*.smv
	* examples/ctl-ltl/*.smv, examples/abp/*.smv, examples/brp/*.smv: 
	Fixed some old smv files from examples. They can be now parsed by
	the current version of NuSMV.
	
19.11.2004 15:53 Marco Roveri <roveri@itc.it>
        * src/ltl/ltl.c, src/ltl/ltl2smv/ltl2smv.c: Fixed memory leaks
	
19.11.2004 12:12 Roberto Cavada <cavada@itc.it>
	* src/bmc/bmcTableauPLTLformula.c: bug #289 the usage of past
	operators with input variables caused segfault to occur. 
		
11.11.2004 13:51 Marco Roveri <roveri@itc.it>, Roberto Cavada <cavada@itc.it>
	* src/trace/Trace.c: Bug fix (access to freed memory was carried
	out).

10.11.2004 09:18 Marco Roveri <roveri@itc.it>
	* src/bmc/bmcDump.c: Fixed dumping of DIMACS.

09.11.2004 15:19 Andrei Tchaltsev <tchaltsev@itc.it>
	* src/be/beRbcManager.c: Removed redundant function
	Be_Cnf_RemoveDuplicateLiterals.
	
29.10.2004 16:02 Roberto Cavada <cavada@itc.it>
	* src/enc/bdd/BddEnc.c: Removed a too strong assertion.
	
29.10.2004 12:10 Andrei Tchaltsev <tchaltsev@itc.it>
	* src/prop/prop.h: Bug fix (wrong prototype of the function
	PropDb_print_all_status_type).
	
28.10.2004 18:18 Marco Roveri <roveri@itc.it>
	* src/sm/smInt.h: Bug fix (not conditioned include).
	
28.10.2004 17:43 Marco Roveri <roveri@itc.it>
	* src/dag/dag.h: Bug fix (wrong inot conditioned include).

27.10.2004 19:05 Roberto Cavada <cavada@itc.it>
	* src/compile/compileFlatten.c: Variables with a range 0..1
	are now coded as boolean, not as normal scalar variables with bits. 
        Now ranges 0..1 are upcasted to "boolean" automatically. 

06.10.2004 13:43 Andrei Tchaltsev <tchaltsev@itc.it>
	* src/rbc/rbcFormula.c, src/rbc/rbcCnf.c: Fixed memory leaks.

04.10.2004 17:00 Marco Roveri <roveri@itc.it>
	* src/compile/compileBEval.c: Fixed a bug in memoizing of
	formula while converting SEXP to BEXP.


14.09.2004 18:14 Andrei Tchaltsev <tchaltsev@itc.it> 
	* src/ltl/*, src/ltl/ltl2smv: ltl2smv is changed to enable its 
	invocation as a function, not as an external program.
	

02.09.2004 12:38 Andrei Tchaltsev <tchaltsev@itc.it>
	* src/bmc/bmcDump.c: Fixed bug in the DIMACS dumping of constant
	(true of false) formulas.
	
	
Wed 25 Aug 2004 11:02:00 Roberto Cavada <cavada@irst.itc.it>
	* src/compile/compile.h, src/compile/compileBEval.c: Added
	memoizing to expr2bexpr conversion.
	* src/bmc/bmcInt.h, src/bmc/bmcPkg.c, src/bmc/bmcWff.c: Added
	memoizing to wff2nnf conversion.
	* src/sm/smInit.c: fixed de-initialization of package bmc.

Tue 17 Aug 2004 12:00:00 Marco Roveri <roveri@irst.itc.it>
	* compile/compileFlatten.c: Fixed wrong flattening of defined
	  symbols within the Compile_FlattenSexpExpandDefine.



	
Thu 6 Aug 2004 12:00:00  NuSMV team <nusmv@irst.itc.it> 
	* === Released version 2.2.2 ===
	
Thu 5 Aug 2004 09:46:34  Roberto Cavada <cavada@irst.itc.it> 
	* node/nodePrint.c: Added cases XOR and XNOR to print_sexp. 

Wed 4 Aug 2004 14:06:11   Andrey Tchaltsev <tchaltsev@irst.itc.it> Gavin Keighren <keighren@irst.itc.it> 
	* docs/user-man/*: Added and fixed documentation.

Wed 4 Aug 2004 13:28:35  Roberto Cavada <cavada@irst.itc.it>
        * options -k and -l, if specified more than once, make nusmv emit an error 
          message and go back to the shell. 
        * checked the use of mutually exclusive options -v and -p in bmc_simulate.
        * Filename patterns like @@@@k are now correcly expanded as @@k. 
          Ahead of this fix, @k was expanded at first. 
        * When unknown options are used with bmc_simulate, the command execution 
          is now stopped.
        * Fixed unregistered traces in check_invar_bmc_inc and check_invar_bmc.
        * Other minor fixes.

Wed 4 Aug 2004 10:10:40  Roberto Cavada <cavada@irst.itc.it>
	* Factorized counterexample printing code in bmc
	* In bmc, during checking commands current bounds and the
	specification were printed out if neither counter-example nor
	proof was found. Now only bounds are printed out to provide feedback
	to users, and the specification text is printed only when the
	verbosity level is greater than two. 

Tue 3 Aug 2004 17:24:37  Roberto Cavada <cavada@irst.itc.it>
	* Fixed memory leaks in bmc.
	* Fixed a bug in BMC commands options handling. 

Tue 3 Aug 2004 14:23:51  Andrey Tchaltsev <tchaltsev@irst.itc.it>
	* New function in module 'be'. For a given be index the function
	returns an associated cnf index, and viceversa. 

Mon 2 Aug 2004 14:34:24  Roberto Cavada <cavada@irst.itc.it>  Gavin Keighren <keighren@irst.itc.it>
        * The tutorial contains now a section about complete invariant 
	checking.  
	* Fixed description of system variable 'ag_only_search' in the
	user manual.

Thu 29 Jul 2004 14:43:41  Roberto Cavada <cavada@irst.itc.it>
	* enc/symb/Encoding.c: Fixed a problem that occurred in bmc when
	determinization variables were introduced, and variable ordering
	file was used. 

Thu 29 Jul 2004 13:30:58  Roberto Cavada <cavada@irst.itc.it>
	* enc/symb/Encoding.{h,c}: Added method is_symbol_determ_var to
	class Encoding. 
	
Wed 28 Jul 2004 15:33:04  Roberto Cavada <cavada@irst.itc.it> 
	* bmc/*: Bug fix #275. Arrays variables are now allowed to occur in
	formulae, but only if they are boolean arrays. 

Wed 28 Jul 2004 11:31:53  Roberto Cavada <cavada@irst.itc.it> 
	* enc/symb/Encoding.c: Bug fix #273. When grouping variables,
	variables for determinization were missing. This made the encoding
	with ordering file possibly buggy. 
	
Tue 27 Jul 2004 12:12:11  Andrey Tchaltsev <tchaltsev@irst.itc.it> 
	* sat/* : Added support for incremental sat solvers.
	* bmc/* : Added algorithms for incremental bmc. 

Tue 27 Jul 2004 12:12:11  Roberto Cavada <cavada@irst.itc.it> 
	* bmc/*: Adapted non incremental bmc to the new sat interface.
	* bmc/*: Added een/sorensson algorithm for non incremental invar
 	checking.

Mon 19 Jul 2004 12:05:52  Marco Roveri <roveri@irst.itc.it>
	* mc/mcMc.c, ltl/ltl.c: fixed missing intersection with fair
	states before invoking counter-example extraction.

Mon 19 Jul 2004 11:54:09  Roberto Cavada <cavada@irst.itc.it>
	* compile/compileFlatten.c: Fixed a bug that occurred when
	instantiating more than once a variable whose range contained one
	value only.
	
Thu 15 Jul 2004 15:52:54  Roveri <roveri@irst.itc.it> Cavada <cavada@irst.itc.it>
	* bmc/bmcConv.c: bexpr -> be conversion caches results. This makes
	convertion more efficient. 	

	
Wed 14 Jul 2004 14:11:47 Marco Roveri  <roveri@irst.itc.it>
	* bmc/bmcSat.c: Fixed wrong allocation when sat solvers but SIM
	were called 
	

Tue 13 Jul 2004 14:02:14 Roberto Cavada  <cavada@irst.itc.it>
	* sm/smMist.c: Fixed behaviour of option -r in batch mode
	

Wed 23 Jun 2004 12:00:00 Roberto Cavada  <cavada@irst.itc.it>
	* Released minor version 2.2.1

	
Mon 21 Jun 2004 16:16:51  Andrey TChaltsev <tchaltsev@irs.itc.it>  Cavada <cavada@irs.itc.it>
	* Added platform-dependant suffix when searching for executable
	files

	
Thu 17 Jun 2004 12:00:00 Roberto Cavada  <cavada@irst.itc.it>	
	* compile/compileFlatten.c: Fixed ordering of insertion of vars.
	
	* enc/bdd/BddEnc: Changed initial variables index: one instead of
	zero. This makes dynamic reordering fully working.

	* compile/compileFlatten.c: Fixed one-value range management.

	* examples/m4: Added m4 examples provided by Villemaire.

	* sm/smMisc.c: Realigned -o option behaviour wrt what version 2.1
	did. 


Tue 15 Jun 2004 09:59:53  Roberto Cavada  <cavada@irst.itc.it>
	* compile/compileCheck.c: Fixed missing type ARRAY when checking
	for input vars in assignements.
	
