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

