WHAT'S NEW

From SRI SAL
Jump to: navigation, search

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