SALut - Self-stabilizing Algorithms in LUsTre

SALut is a companion project to Verimag's Synchrone Reactive Toolbox.

It is dedicated to the Simulation and Formal Verification of Self-stabilizing Algorithms in the Lustre Programming Language, relying on Lurette and SASA for testing/simulation and on Kind2 for SMT-powered verification.

salut

Summary

salut compiles a graph described in the DOT format into a Lustre program that executes some Distributed Self-Stabilizing Algorithm over an equivalent network topology.

salut <dotfile> [-o <lusfile>] [--clock] [--help]
  -o Set output file (default is inferred from input file)
  --clock Generate clocked code (default is unclocked)
  --help  Display this list of options

Algorithm API

Following the conventions used in SASA's API, every algorithm currently needs to provide the following definitions, which are shared by all nodes:

(* Represents a node's state. *)
type state;

(* Enumerates the possible atomic actions a node might execute. *)
type action;
const actions_number : int;

(* Maps an integer in [0,actions_number) to an equivalent action. *)
function action_of_int(i : int) returns (a : action);

And each algorithmic node needs enable and step functions prefixed by its name:

(* p.lus *)

(* Computes the set of actions enabled in this configuration. *)
function p_enable<<const degree:int>>(
    this : state;
    neighbors : state^degree
) returns (enabled : bool^actions_number);

(* Executes the given action, returning the updated node state. *)
function p_step<<const degree:int>>(
    this : state;
    neighbors : state^degree;
    action : action
) returns (new : state);

Check out the generated Lustre topology for the graph constants it defines.

Examples

Some example algorithms are provided in this repository. Each folder contains a distributed algorithm defined in both OCaml+SASA and LustreV6+SALUT and with a common network topology.

The shared Makefile has instructions on how to build the Lustre-defined network and use Lurette to test it agains the SASA model.

$ cd salut/test/coloring/
$ make clique3.lurette
$ make er100.lurette

You can also verify it with Kind2. Note that this currently requires converting LustreV6 to LustreV4 and adding Kind2's required annotations (to the generated LV4), which is also handled by the makefile.

$ make clique3.kind2