FAQ

From SRI SAL
Revision as of 18:30, 28 November 2011 by Admin (Talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Frequently Asked Questions about SAL

Contents

SAL and Yices

What does SAL need Yices for?

Yices is an SMT solver (i.e.,a solver for Satisfiability Modulo Theories; ordinary SAT solving is a just a special case). For all platforms, there is the option to download the SAL binaries with or without Yices included. ICS, an older SMT solver, is always included with SAL.

  • The SAL slicer uses Yices (it would be better if it used whatever solver was available).
  • The SAL bounded model checker needs a SAT solver.
    Yices is the default, but it can use others, including ICS, which is distributed with SAL.
  • The SAL infinite bounded model checker needs an SMT solver.
    Yices is the default, but it can use others, including ICS, which is distributed with SAL.

Why do you include ICS with the SAL binaries when Yices is so much better?

We do it so that all the SAL model checkers work out of the box (though you will need to add the command line option -s ics). Yices has different license terms and some users may not agree to these. For all platforms, there is the option to download a SAL binary with Yices included (subject to acceptance of its license) and this is what we recommend. If you install SAL without Yices, you can always download and install Yices separately. Note that PVS can use Yices as an endgame prover, and will find it automatically if you downloaded it with SAL.

What SAT solvers can sal-bmc use?

  • sal-bmc supports the following SAT solvers: Yices, ICS, zChaff, siege, GRASP, and BerkMin.
    Yices and ICS are available for all the platforms supported by SAL, but some of the others may not be. The Yices SAT solver is state of the art and other SAT solvers seldom provide any advantage, with the exception of siege, which uses different (undocumented) techniques from other SAT solvers and sometimes outperforms them. The siege_v4 executable for x86-linux can be downloaded here. The ICS SAT solver is from an earlier generation and is not competitive with Yices.

What SMT solvers can sal-inf-bmc use?

  • sal-inf-bmc can use Yices, ICS, SVC, CVC, CVClite, and Uclid
    Yices and ICS are available for all the platforms supported by SAL, but some of the others may not be. SAL may not provide explicit counterexamples from solvers other than Yices (it provides "symbolic" counterexamples with ICS). The Yices SMT solver is state of the art (it won every division at the 2006 SMT competition) and other SMT solvers seldom provide any advantage. The ICS SMT solver is from an earlier generation and is not competitive with Yices.

    The different SMT solvers support different collections of theories, and these theories do not always correspond naturally to SAL types (e.g., difference logic is not a SAL type). Thus, SAL does not always exploit the full capabilities of any given solver (including Yices). For example, it may bit-blast a bounded integer rather than represent it as a true integer plus a constraint.

LTL (Linear Temporal Logic) Topics

LTL (Linear Temporal Logic) is the language used to write SAL properties.

What are the available LTL operators?

SAL provides X (next state), G (always), F (eventually), U and W (strong and weak until), R (release), and B (before). These are written in prefix form (e.g., R(foo, bar)).

In the src directory of the SAL distribution, you will find a file ltllib.lsal that defines numerous additional LTL operators as functions. You can use these in the following way (where responds-to is one of the functions defined in ltllib):

th3: THEOREM main |- ltllib!responds_to(state = busy, request);

Note that ltllib itself is written in lsal, which is the alternative Lisp-like syntax for SAL. You can use the ordinary syntax to define new LTL operators as well. For example, to define a 4-fold iterated X operator, you can define the following function

XXXX(a:boolean): boolean = X(X(X(X(a))));

You can even do the following

posnat: TYPE = {x: natural | x>0};
Xn(a: boolean, n: posnat): boolean = 
   IF n = 1 THEN X(a) ELSE Xn(X(a), n-1) ENDIF;
X24(a: boolean): boolean = Xn(a, 24);

Semantics of the LTL operators

Linear temporal logic (LTL) is used to specify properties of the traces of a system. Define a trace as an infinite sequence of states s = (s_0, s_1, ..., s_i, ...), where s_(i+1) is a successor of s_i, (i.e. there is a transition from s_i to s_(i+1)). Use . to indicate concatenation of trace prefixes and traces.

The semantics of LTL defines whether a trace s of a given system satisfies a formula p (written as s |= p). The base cases are when p is a predicate on states, an X formula, or a U formula.

s |= expr, where expr is a predicate on states, 
           if and only if expr is true on the initial state s_0.
s |= X(p), if and only if s = s_0 . w and w |= p.
s |= U(p, q), if and only if:
  exists n such that s = s_0 . s_1 .  ... . s_n . w, with
    w |= q and for all i in {0, ..., n }, s_i |= p.

The other operators may be seen as macros, and are defined in the following way:

R(p, q) = NOT U(NOT p, NOT q)
G(p) = R(FALSE, p)
F(p) = U(TRUE, p)
B(p, q) = R(p, NOT q)
W(p, q) = G(p) OR U(p, q)

Note that U(p, q) requires that q eventually becomes true; W(p, q) does not require this if p is always true.

Useful LTL Patterns

Note that SAL definitions for many of these patterns are given in the file ltllib.lsal that is included in the SAL distribution (in the src directory).

G(expr) 
expr is always true
init => G(expr)
expr is always true in any trace that begins with a state satisfying init
G(F(expr)) 
expr is true infinitely often
G(F(NOT en OR oc)) 
If en is enabled continuously, then oc will occur infinitely often. This is more easily understood when written as G(F(NOT en) OR F(oc)) or as G(G(en) => F(oc)). This is weak fairness, and is often sufficient for modeling progress in asynchronous systems.
G(F(en)) => G(F(oc)) 
If en is enabled infinitely often, then oc will occur infinitely often. This is strong fairness and is often necessary for modeling synchronous interaction.
G(F(cond-1)) AND G(F(cond-2)) ... AND G(F(cond-n) => expr 
cond-1, cond-2,..., cond-n are (strong) fairness conditions. We say that expr is true assuming these fairness conditions.
G(expr-1 => F(expr-2)) 
Everytime expr-1 is true, eventually expr-2 will also be true. This is a response formula.

Link to LTL specifications for several useful patterns

Does SAL have constructs for fairness?

No. You specify fairness constraints in the properties. See examples above

Visualizing LTL formulas as Buchi automata

You can get SAL to display the Buchi automaton for a formula by

ltl2buchi context-name formula-name -dotty

This requires dotty to be installed on your machine (it is by default in most Linux installations).

How does SAL convert LTL formulas to Buchi Automata?

SAL uses the approach described in "Fast LTL to Buchi Automata Translation" by Paul Gastin and Denis Oddoux, CAV 2001 (LNCS 2102). This is not a direct tableau construction but a chain of translations: LTL --> very weak alternating automata --> generalized Buchi --> Buchi, with simplification rules applied at each step to reduce the size of the automata.

I'd prefer to use CTL

LTL and CTL are incomparable, but SAL does allow use of CTL notation for properties that are common to both. It works by translating to LTL.

This LTL stuff is complicated. Is there an alternative?

For safety properties, you can write a module that observes the state of the system (a synchronous observer) and sets a state variable error to true when its sees something it doesn't like. Then model check for G(NOT error).

General Model Checking Topics

SAL "verifies" obviously false F properties

LTL formulas are defined only for infinite traces. If your module deadlocks (i.e., has reachable states with no successors) then model checking will be unsound (and any F property will be declared true). You can check whether finite state modules deadlock with sal-deadlock-checker (this uses BDDs and is subject to the same performance limitations as any BDD-based checker). There's no tool support in SAL for checking infinite state systems for deadlock.

As a special exception, SAL does interpret G properties over finite traces in the intuitive manner (and, I think, W also).

The [] ELSE --> construction guarantees absence of deadlocks and so does asynchronously composing with an always-enabled module (but neither of these may be suitable in your specification for other reasons).

Counterexamples for livenesss properties are different to those of NuSMV

Counterexamples for liveness properties consist of a prefix and a lasso (loop). In SAL (by user request), the last state of the prefix is repeated at the beginning of the lasso.

Liveness counterexamples in sal-inf-bmc do not identify the beginning of the loop

Yes, we're working on that.

Empty modules behave differently than NuSMV

In SAL, an empty module (one with no transitions) starts in an arbitrary state and then stutters forever; in NuSMV it makes arbitrary transitions. A SAL module that takes arbitrary transitions starting from arbitrary initial states can be introduced by writing x IN {y : T | TRUE} in the DEFINITION section for each variable x, where T is the type corresponding to x. The main use for this kind of module is in deciding satisfiability of temporal logic formulas (by reducing it to model checking).

Bounded model checker fails to find a counterexample to a G property that is obviously falsified within a couple of steps

Bounded model checkers first construct a symbolic representation of all k-step traces of the transition relation, then seek a violation of the property among those traces. In SAL, k defaults to 10, but if your specification deadlocks before that and has no 10-step traces, then the model checker will be unable to construct any traces and will report no errors. If you ask the model checker to look for shorter violations (e.g., with -d 2, or -it), you will get counterexamples.

Bounded model checker fails to find short counterexample

This is a variant of the above: if the bound is, say 10, the model checkers construct all 10-step traces and then look for a violation of the property among those. There's no guarantee the solvers will find one where the violation occurs early in the trace. To get the shortest counterexample, you need to iteratively increment the bound k; the -it option automates this.

The -it option is slow when the maximum depth is large

The bounded model checker treats each iteration as a new problem; it would be better if the SMT or SAT solver retained all the information from depth k when analyzing the increment for depth k+1. The Yices SMT solver supports this kind of incremental solving, but it's nontrivial to modify SAL to exploit this capability.

The SAL model checkers do not work with recursive datatypes

None of the current tools support recursive datatypes. sal-smc, and sal-sim use binary decision diagrams (BDDs) to represent the transition relation. So, the SAL specification must be transformed in boolean formulas, and recursive datatypes are not supported. sal-bmc uses SAT solvers, and has the same limitation. A future release of sal-inf-bmc will support recursive datatypes.

Customization and the SAL API

How do I customize SAL?

SAL programs like sal-smc are actually scripts written in the programming language Scheme that invoke functions from the SAL API. Take a look at the scripts for the SAL test generator to get an idea of how these are written; those scripts are sal-atg-core.scm and sal-atg-front-end.scm in the src directory of the SAL distribution. You can try modifying existing scripts, or writing your own from scratch (see below).

The standard reference for Scheme is http://www.schemers.org/Documents/Standards/R5RS/ and documentation for the Bigloo Scheme implementation used by SAL is available at http://www-sop.inria.fr/mimosa/fp/Bigloo/

How do I create a new SAL tool?

You should create three files (where "tool" is the name of your tool):

  • sal-tool.template

This is the template for a shell script that is going to be created at installation time.

#!/bin/sh
exec __SALENV_DIR__/bin/salenv "$@" __SALENV_DIR__/src/sal-tool-front-end.scm
  • sal-tool-front-end.scm

This is the tool startup script. It is basically responsible for parsing command line arguments, and calling the tool API. Command line arguments are available in the global variable *arguments*.

The macro files front-end.macros and sal-script-util.scm located in the SAL src directory contain useful functions and macros to create a tool front-end.

The macro gen-front-end is particularly useful. The files sal-wmc-front-end.scm (if your tool deals with assertions) or sal-path-finder-front-end.scm (if your tool deals with modules) can be used as templates, and show how to use this macro.

  • sal-tool-core.scm

This contains the tool api. This file is usually compiled and included in the SAL runtime. If it is not compiled, then you should explicitly invoke it in the template file as follows

#!/bin/sh
exec __SALENV_DIR__/bin/salenv __SALENV_DIR__/src/sal-tool-core.scm "$@" __SALENV_DIR__/src/sal-tool-front-end.scm

How do I learn the functions in the SAL API?

This is not documented yet. The best you can do (other than looking at the source) is to start salenv-safe, then type (help "").

SAL Language Topics

What is lsal?

SAL has three syntactic representations. They are all equivalent.

  • The standard SAL concrete syntax, indicated by file extension .sal
  • The lsal concrete syntax, which looks like Lisp or Scheme, indicated by file extension .lsal
  • The SAL XML abstract syntax, which is defined by this DTD

Personal tools