README.org



SASA: a SimulAtor of Self-stabilizing Algorithms 
#
TL;DR
<<sasa>> SASA  is a Self-stabilizing Algorithms  SimulAtor, based on
  the so-called Atomic  State model (ASM) introduced  by Dijkstra in
  its seminal  article on Self-stabilizing distributed  algorithms. This
  model  is  also sometimes  named  “locally  shared memory  model  with
  composite atomicity”
Basically, one needs to provide:

  a topology,  made of  nodes  and transitions  (via a dot file)
  the algorithms attached to nodes (via =ocaml= programs)

The fastest way to get started is to copy the files provided in the
  test/skeleton directory, and to modify them:
cd test
cp -rf skeleton my_algo # copy a simple example
cd my_algo              # one may want to edit "p.ml" and "ring.dot"
make ring.cmxs          # compile anything that needs to be compiled
sasa ring.dot -l 4      # run a batch simulation for 4 steps

#+RESULTS[6abb8d69a9985c7f167f39a9515f09cdd53bc3e4]:
sasa -reg ring.dot
ocamlfind ocamlopt -package algo -shared state.ml p.ml config.ml ring.ml -o ring.cmxs
# Automatically generated by /home/jahier/.opam/4.10.0/bin/sasa version "4.3.5" ("a6897fa")
# on crevetete the 2/11/2020 at 15:28:50
#sasa ring.dot -l 4

#seed 972333160
#inputs 
#outputs "p1_i":int "p2_i":int "p3_i":int "p4_i":int "p5_i":int "p6_i":int "p7_i":int "Enab_p1_action2":bool "Enab_p1_action1":bool "Enab_p2_action2":bool "Enab_p2_action1":bool "Enab_p3_action2":bool "Enab_p3_action1":bool "Enab_p4_action2":bool "Enab_p4_action1":bool "Enab_p5_action2":bool "Enab_p5_action1":bool "Enab_p6_action2":bool "Enab_p6_action1":bool "Enab_p7_action2":bool "Enab_p7_action1":bool "p1_action2":bool "p1_action1":bool "p2_action2":bool "p2_action1":bool "p3_action2":bool "p3_action1":bool "p4_action2":bool "p4_action1":bool "p5_action2":bool "p5_action1":bool "p6_action2":bool "p6_action1":bool "p7_action2":bool "p7_action1":bool 


#step 0
#outs 4 5 2 1 9 0 4 t f t f f f t f f t t f t f t f t f f f t f f t f f t f 

#step 1
#outs 0 0 2 0 1 0 0 f t t f f t f f f t f t f t f t f f f t f f f t f f f t 

#step 2
#outs 1 0 1 0 1 0 1 f f f f f t f f f t f f f f f f f f f t f f f t f f f f 

#step 3
#outs 1 0 1 0 1 0 1 f f f f f t f f f t f f f f f f f f f t f f f f f f f f 

#step 4
#outs 1 0 1 0 1 0 1 f f f f f t f f f t f f f f f f f f f t f f f f f f f f 
#q

SASA source code: https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa
Some Tutorials: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/
TAP article pre-print : Karine Altisen, Stéphane Devismes, Erwan Jahier. SASA: a SimulAtor of Self-stabilizing Algorithms. 14th International Conference on Tests and Proofs, Jun 2020, Bergen, Norway. hal-02521149

Topology
<<dot>>
  <<topology>>
  The topology is given via .dot files, that  should

  follow the graphviz/dot format

  have  nodes labeled by the algo field

graph ring {
 p1 [algo="some_algo.ml"]
 p2 [algo="some_algo.ml"]
 p3 [algo="some_algo.ml"]
 p4 [algo="some_algo.ml"]
 p5 [algo="some_algo.ml"]
 p6 [algo="some_algo.ml"]
 p7 [algo="some_algo.ml"]

 p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1 
}

#+RESULTS[d65ee51636ffe73dde3eee3488f35b6066c52d98]:
  ring.dot
Of course the some_algo.ml file must exist and contains an algorithm.
In order to  define an initial configuration, one can use the init
  node attribute.
graph ring {
 p1 [algo="some_algo.ml" init="i=1"]
 p2 [algo="some_algo.ml" init="i=2"]
 p3 [algo="some_algo.ml" init="i=42"]
 p4 [algo="some_algo.ml"]
 p5 [algo="some_algo.ml"]
 p6 [algo="some_algo.ml"]
 p7 [algo="some_algo.ml"]

 p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1 
}

#+RESULTS[774c94dfeb9d5c7279e1a267c805461b09ca5c4f]:
  ring_init.dot
One can use graph attributes to set parameters that can be used by all
  nodes during the simulation.
graph ring {
 graph [diameter="4" some_other_global_parameter="42"]
 p1 [algo="some_algo.ml" init="i=1"]
 p2 [algo="some_algo.ml" init="i=2"]
 p3 [algo="some_algo.ml" init="i=42"]
 p4 [algo="some_algo.ml"]
 p5 [algo="some_algo.ml"]
 p6 [algo="some_algo.ml"]
 p7 [algo="some_algo.ml"]

 p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1 
}

#+RESULTS[de8e9d4b7950f4da5976b90639faf6a2d36631ff]:
  ring_init.ml
Such   parameters  can   be   retrieved  in   algorithms  using   the
  Algo.get_graph_attribute : string ->  string function. For example,
  if  you  know the  graph  diameter,  you can  define  it  as a  graph
  attribute (a Algo.diameter:  unit -> int function  is provided, but
  it can be expensive to use for large graphs).
Some tools are provided in the sasa distributions to generate such
  kinds of dot graphs:
  https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/
Algorithms
<<Algorithms>>
The following has been generated from algo.mli


Examples
Batch mode

Running batch simulations with Built-in daemons
To launch batch simulations, one can use the sasa Command Line Interface.
For instance, in order to simulate an algorithm defined in the
  ring.dot (cf test/coloring), you can launch the following
  command (the resulting produced outputs follows in green):