# WHAT'S NEW

From SRI SAL

## Contents |

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