********************** SAL 2.2 **********************

* New functionalities

- ltl2buchi is a new tool that allows the user to visualize the
	Buchi Automata (monitor) used to verify LTL properties.

- The ICS, CVC and SVC backends support division by constants.

- All tools are accepting also file names, instead of context names.
  Example:
    sal-smc -v 3 ~/tmp/peterson.sal mutex

  When file names are used the SALPATH is ignored.

- The call/trace stack is not printed when an error happens in salenv,
  salenv-safe, or sal-sim. The command '(sal/enable-trace-stack! #t)' can
  be used to force SAL to display the call/trace stack when an error
  happens.

- The parser error messages were improved.

* Bug fixes

- Builtin types can be redefined.

- Fixed a bug in the ICS output parser. 

- Fixed a bug in the SVC formula pretty printer. In SVC, the syntax
  for rational numbers is "x|y" instead of "x/y".

- Fixed a bug in the simplier related to quantifiers.

- Fixed a bug in the sal-parser: it aborted the program when an
  undefined module is used in an assertion expression.

- Fixed a bug in the sal-parser: it failed to parse recursive
  datatypes.

- Fixed a bug related to invalid set list expressions. SAL was
  aborting if a set list expression contains elements of incompatible
  types.

- Fixed a bug in sal-inf-bmc related to subtypes of numbers. The user
  defined predicate was not propagated to the decision procedures.

- Fixed a bug in the expression simplifier (equality) of
  tuple and record literals.

- Fixed a bug in the evaluator related to uninterpreted constants.

- Fixed a bug in sal-inf-bmc: it was not propagating the fact that a
  subrange is an integer variable to ICS.

- Fixed a bug related to the use of subtypes as indexes of arrays and
  functions.

- Now, SAL complains when CVC, CVC Lite, UCLID or SVC produces unexpected
	results. 

- Fixed a bug in the generation of arithmetical circuits.

- Now, SAL certificates containing carriage returns (0x0d) are accepted on
  UNIX-like machines.

- Fixed a bug in the LTL to Buchi Automata translator. The translator
  was crashing for trivially true/false properties.

* Changes

- The concrete syntax for StateType and StatePred was modified from
		
    StateType := <module> . STATE
    StatePred := <module> . INIT
               | <module> . TRANS
  to

    StateType := STATE_TYPE ( <module> )
    StatePred := INIT_PRED ( <module> )
               | TRANS_PRED ( <module> )
  


********************** SAL 2.1 **********************

* New functionalities

- A new and more efficient parser. Now, it is not necessary
  to have Java installed to be able to use SAL. The new parser
  accepts lowercase keywords if the option --enable-parser-ext is
  used.

- Now, it is possible to use SAL syntax to specify assertions
  in the command line. Examples:

    sal-smc -v 3 --assertion='peterson!mutex'

    sal-smc -v 3 --assertion='arbiter{;10}!at_most_one_ack'

- New tool: sal-wmc (Witness Counterexample Based Symbolic Model Checker)
  sal-wmc is the main model checker to prove CTL properties. If a LTL
  property is provided, it tries to convert it to CTL.

- Now sal-smc is a model checker to prove LTL properties. If a CTL
  property is provided, it tries to convert it to LTL.

- Implemented the operators "div" and "mod" in the finite
  state model checkers.

- Temporary files generated by SAL are automatically deleted.
  The option --preserve-tmp-files can be used to disable this
  behavior. Remark: XML files are not considered temporary files.

- New path manipulation functions were included in the API.

* Bug fixes

- Fixed a problem in translation of "x - y" to a boolean
  circuit.

- Fixed a problem in the generation of temporary files. 
  Now, it is possible to execute several instances of the
  model checkers at the same time.

- Fixed the path (counterexample) pretty printer. Sliced
  variables were being printed with random values.

- Fixed a nontermination bug in the typepred procedure.

- Now, an error message is produced when sal-inf-bmc (using ICS, CVC,
  CVL-Lite, SVC, or UCLID) finds an occurrence of the operators '/',
  'mod', or 'div'.

- Fixed a bug which produces the wrong transition relation
  when there is an asynchronous composition of two modules
	'm1' and 'm2', where the variable 'x' is a global variable
  in 'm1', and an input variable in 'm2'.

- Fixed a bug in the sal-inf-bmc counterexample pretty printer.
	
* Changes

- GC messages are only printed in verbose mode >= 10.

- The simplification step before the construction of BDD transition
  relation was removed. It was just consuming computer cycles.

- Dynamic variable reordering is active during the construction
  of the BDDs representing the DEFINITION section of a module.
  This modification is useful, since sal-smc does not perform
  any kind of partitioning on a BDD representing a bit of a
  defined variable. The option --disable-def-dyn-reorder can
  be used to disable the dynamic reordering in this step.

* Documentation

- Small modifications in the SALenv tutorial.

