**SAL** stands for **Symbolic Analysis Laboratory**. A document from SRI International defines it the following way:

The Symbolic Analysis Laboratory (SAL) is a set of tools for the specification, exploration, and verification

of state-transition systems. SAL includes symbolic model-checking tools based on solvers and

decision procedures for linear arithmetic, uninterpreted functions, and propositional logic, among others.

This enables the analysis of a variety of infinite-state systems. In particular, SAL can be used to model

and verify timed systems, which combine real-valued and discrete state variables.

Firstly SAL defines a context. You can define data types and modules in that. Modules encapsulate variables and transitions. Transitions manipulate variables.

The main goal is to define modules that implement the functionality of the model. When you have defined the model in SAL, you have to define theorems to prove them. It is usually implemented in **Linear Temporal Logic (LTL)**. There are four basic LTL expressions:

**Fp**- p will be valid in a future state**Gp**- p globally valid**Xp**- p will be valid in the next state**p U q**- p will be valid in every single state until p becomes valid

**Context**

ContextName : CONTEXT =

BEGIN

...

END

The ContextName and the filename must be the same.

**Module**

*ModuleName* : module =

BEGIN * variables initialization * TRANSITION

*expressions*

...

END;

You can execute modules synchronously by chaining them:

*main* : MODULE =

*module1* || *module2* || ... || *moduleN*;

Decisions in transitions can be defined easily with brackets:

TRANSITION

[

condition1 -->

expression1;

expression2;

[]

condition2 --> expression

[]

ELSE -->

]

If condition is true, branch will be executed and transition processing stops. The final ELSE --> is needed to prevent deadlocks.

An example for a module (it's inside a context):

Phases : type = {p1, p2,p3};

Phase : MODULE =

BEGIN

INPUT tick : BOOLEAN

OUTPUT WorkPhase : Phases

INITIALIZATION tick = false;

INITIALIZATION WorkPhase = p1;

TRANSITION

[

tick = true AND WorkPhase = p1 --> WorkPhase' = p2;

[]

tick = true AND WorkPhase = p2 --> WorkPhase' = p3;

[]

tick = true AND WorkPhase = p3 --> WorkPhase' = p1;

[]

ELSE -->

]

END;

The VariableName' = NewValue is the value setting syntax.

The theorem can be expressed like this:

*TheoremName* : THEOREM *ModuleName* |- *LTLExpressions*

An example for theorem:

Gas : THEOREM main |- G(GasCount > 0 => F(GasPrice =2));