WHAT'S NEW in SAL 3.0

From SRI SAL

Here is a summary of new features introduced in SAL 3.0. Some were already present in the SAL 2.4 pre-releases.

Contents 1 New functionalities 2 New Examples 3 Bug fixes 3.1 SAL 2.3 ChangeLog

New functionalities

• The SALPATH is now called SALCONTEXTPATH.

• Improved performance.

• The user can provide predicates to control BDD variable reordering.

• New configuration scripts are available in the /etc subdirectory.

• New prioritized traversal strategies.

• New option --skolemize in sal-bmc and sal-inf-bmc. This option forces SAL to skolemize quantified variables whenever possible.

• The performance of sal-bmc was improved.

• Yices is the default SAT solver for sal-bmc.

• Yices is the default decision procedure for sal-inf-bmc.

• sal-inf-bmc produces concrete counterexamples.

• The siege SAT solver (http://www.cs.sfu.ca/~loryan/personal) can be used with sal-bmc.

• The BerkMin SAT solver (http://eigold.tripod.com/BerkMin.html) can be used with sal-bmc.

• FORALL definitions are now allowed in guarded commands.

• New type constructors SCALARSET(n) and RINGSET(n) have been defined, where n evaluates to a positive natural number.
  Both type constructors can be viewed as subranges [0..n-1] with a restricted operation set. SCALARSET(n) supports only the operators = and /=. RINGSET(n) supports the operators =, /=, pred, and succ.

• User scripts can be compiled and dynamically linked. This feature is only available on Linux.

• WITH (update expressions) are left associative. So, the following kind of expression is allowed:

   t WITH [i1] := val1 WITH [i2] := val2

• The ';' in qualified names and context parameters is now optional.
  For instance, you can write "bakery{3,5}!mutex" instead of "bakery{;3,5}!mutex".

• It is now possible to mix type and variables parameters in the context declaration.

• The IMPORTING directive can be used in SAL contexts to import other contexts.
  Examples:

  IMPORTING list{NATURAL};
  x : list = cons(1,nil);
  y : NATURAL = car(x);

  IMPORTING list{NATURAL} WITH cons TO mk_cell, car TO hd, cdr TO tl;
  x : list = mk_cell(1,nil);
  y : NATURAL = hd(x);

• Now, the default input syntax in sal-sim and sal-env is the SAL concrete syntax.
  The following command can be used to make LSAL the default:

 (sal/set-make-sal-string-reader-proc! make-lsal-string-reader)

• The keywords in SAL are now case insensitive.

• The ICS, CVC and SVC backends support DIV (integer division) and MOD (modulo) by constants.

• Improved support for integer reasoning in ICS.

• K-induction does not consider acyclic paths by default. The option --acyclic can be used to force acylic paths.

• SAL parser supports hexadecimal (e.g., 0xFF) and binary numbers (e.g., 0b101).

• SAL parser support floating point numbers (e.g., 0.142) as syntactic sugar for rational numbers (e.g., 0.142 is interpreted as 142/1000).

• Added support for ZChaff 2004

• SAL Well-Formedness Checker (type checker light) checks if IMPLEMENTS and OBSERVE-WITH constructors are used correctly.

New Examples

• MCS distributed list-based queuing lock

• Dinning Philosophers

• N-process Peterson Protocol

• Modeling and Verification of an Air Traffic Concept of Operations

• Queue Lock using symmetry reduction

Bug fixes

• Fixed a bug in the parser related to nested ELSIF.

• Fixed a bug related to the invalid use of nested WITH updates.

• Fixed a bug in the quantifier expansion procedure.

• Fixed a bug in the UCLID translator. Some expressions outside of the separation logic fragment were causing the translator to crash.

• Fixed a bug in the boolean circuit generator for subtraction

• Improved garbage collector for huge heaps (> 500Mb)

• Fixed a GC problem during the construction of counterexamples in sal-smc.

• Fixed a bug in sal-inf-bmc and sal-bmc. They were crashing when lemmas contained sliced variables.

• Fixed a bug in sal-inf-bmc and sal-bmc. These tools were not accepting qualified names (using SAL syntax) to reference a lemma.

• Fixed a bug in the AST construction. It crashed when a specification contains an invalid (i.e., type incorrect) nested update expression.

• Fixed a bug in sal-wmc. The bug was in the evaluation of AX and EX operators.

• It is possible to use the same identifier to name a module, type, and constant.

• Fixed the type checker. Now, SAL returns an error when the NEXTOPERATOR is used in a property.

• Fixed a bug in the flat module generator. It was crashing when computing non-trivial implicit assignments.

• Fixed a bug in the generation of counterexamples for the prioritized traversal strategy in sal-smc.

• Reduced the number of processes created when a SAL tool is started.

• Fixed a confusion between n-ary functions and unary functions where the argument is a n-tuple.

• Fixed a bug in the boolean based model checkers. They were crashing in examples that use subtypes in the state variables if the subtype predicate contains quantifiers.

• Fixed a bug related to subtypes. The procedure that computed the union of two subtypes was returning the wrong result in some cases.

• Fixed a segmentation fault that happened when the user provided the wrong number of context parameters in the command line.

• Fixed soundness problems in ICS.

• Removed a nondeterministic behavior in the common subexpression module.

• Fixed a bug in the type inference module.

• Fixed the error message produced when the subrange upper/lower bound is above/below the maximum allowed.

• Fixed a bug in the generation of counterexamples for liveness properties in sal-smc.

• Fixed a bug in the generation of counterexamples in sal-smc and sal-bmc. They were crashing when a multi command was indexed by a DATATYPE.

• Fixed a bug in the partial evaluator that was affecting specs using recursive high-order functions.

• Fixed a bug in the parser. The precedence of WITH (update expression) was wrong, it was using the same precedence of WITH (module expression).

• Fixed a bug in the type checker. It was not checking if a shared input variable in a module composition had the same type in both modules.

SAL 2.3 ChangeLog

• New functionalities

- A new option (--enable-bs-dyn-reorder) is available in sal-smc

 and sal-wmc. It enables BDD variable dynamic reordering during
 the construction of the transition relation.

- A new option (--enable-let-bdd-vars) is available in sal-smc and

 sal-wmc. This option enables the generation of auxiliary BDD
 variable. These variables are used to minimize the size of the
 transition relation. Each new variable corresponds to a new 
 cluster. This option is ingored if a monolithic transition relation
 is required.

- CUDD 2.4.0

- The construction of partitioned transition relations in the

 symbolic model checkers was improved.

- sal-smc supports prioritized traversal. This approach is useful

 for finding bugs. 

- The functions sal-bdd-fsm/pre-image-without-choices and sal-bdd-fsm/pre-image were

 renamed to sal-bdd-fsm/pre-image and sal-bdd-fsm/pre-image-with-choices respectively.

- In sal-sim, the functions pre-image-without-choices and pre-image were

 renamed to pre-image and pre-image-with-choices respectively.

- sal-smc supports the verification of all LTL properties in a context

 in a single call. The CTL properties that can be converted to LTL
 are also verified. It also has a new option --only-invariants, that
 can be used to verify all invariants in a context.

• Bug fixes

- Fixed a bug in make-boolean-state-expression. This bug

 only affects people using the SAL API.

- Fixed a bug in the invocation of external tools. Now pathnames

 and user names may contain spaces.

- Fixed a bug in the ics output parser related to CR/LF (carriage

 return/line feed). This bug happens when the file-system is
 mounted in textmode instead of binmode.

- lsal2xml generates the ELSIF attribute

- Fixed a bug in sal-bmc/extend-path. This bug only affects people

 using the SAL API.

- Removed an invalid optimization in the LTL to Buchi translation.

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