WHAT'S NEW

From SRI SAL

Contents 1 SAL 3.0 1.1 New functionalities 1.2 New examples 1.3 Bug fixes 2 SAL 2.3 2.1 New functionalities 2.2 Bug fixes 3 SAL 2.2 3.1 New functionalities 3.2 Bug fixes 3.3 Changes 4 SAL 2.1 4.1 New functionalities 4.2 Bug fixes 4.3 Changes 4.4 Documentation

SAL 3.0

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

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 variables. These variables are used to minimize the size of the transition relation. Each new variable corresponds to a new BDD cluster. This option is ignored 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 affects only people who use 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 now accept also file names rather than context names.
  Example:

   sal-smc -v 3 ~/tmp/peterson.sal mutex

When file names are used 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 simplifier related to quantifiers.

• Fixed a bug in the sal-parser: it aborted the program when an undefined module was 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 arithmetic 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 use SAL. The new parser accepts lowercase keywords if the option --enable-parser-ext is used.

• It is now possible to use SAL syntax to specify assertion on 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.

• New sal-smc 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 that produced the wrong transition relation when two modules 'm1' and 'm2' were composed asynchronously and some variable 'x' was global 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.