Model checking with SAL

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