SASA: a SimulAtor of Self-stabilizing Algorithms

In order to run an algorithm, e.g., the coloring algorithm, on a 5x5 grid topology, do:

cd test/coloring
make grid5.dot  # actually optional; the command below would generate it
make grid5.cmxs
sasa grid5.dot

Once you have defined your algorithm and your topology, you can launch batch simulations with the sasa CLI (Command Line Interface). To do that, one needs to:

1. write or generate some registration (Ocaml) code
2. compile the Ocaml programs.

The easiest way to get registration code is to let sasa generate it.

cd test/coloring
sasa -reg ring.dot

This command will generate the ring.ml file, that contains the registration code. It will also generate, if they do not already exist, 2 other (skeleton) files:

• state.ml which contains types and functions definition related to algorithm states, and
• config.ml which contains optional function definitions, such as the legitimate function that allows one to define what a legitimate configuration is (but we'll come to that later).

The ring.ml file refers to state.ml, config.ml, and p.ml; p.ml needs the definitions in state.ml; moreover, definitions in p.ml can be used useful in config.ml. We need to take those dependencies into account to compile those files and generate the .cmxs file (that should be named according to the topology file name).

ocamlfind ocamlopt -shared -package algo state.ml p.ml config.ml ring.ml -o ring.cmxs

Now we are ready to launch our first batch simulation:

sasa ring.dot

But all of these commands can actually be automated with make and dune:

make ring.cxms

If you have created a fresh directory from scratch, do not forget to copy (or sym-sink) the Makefile* and the dune* files that are in one of the test/*/* directories.

Hence, to sum-up, to simulate the coloring algorithm on 5x5 grid:

 cd test/coloring # from the sasa git repository
 make grid5.cmxs   # generate and compile all necessary files
 sasa grid5.dot    # launch a simulation

nb: the simulation output (in the green frame) follows the RIF conventions.

By default, the distributed daemon is used to activate enabled actions. Several other daemons can be used, via one of the following options:

sasa -h | grep "\-daemon"

--synchronous-daemon, -sd
--central-daemon, -cd
--locally-central-daemon, -lcd
--distributed-daemon, -dd
--custom-daemon, -custd
--greedy-central-daemon, -gcd
--greedy-daemon, -gd

By using the --custom-daemon option (or -custd for short), you can play the role of the daemon. More precisely, you will be prompted for stating which actions should be activated, among the set of enabled actions.

cd test/unison
make ring.cmxs
echo " # here we provide input in batch via echo, but it can be done interactively
t t t t t t t # Active all the processes for the first step
f f f f f f t # Active only p7 at the second step
q             # and then quit
" | sasa ring.dot --custom-daemon

In the custom daemon mode, the daemon is executed outside sasa, by a process that communicates via the standard input/output using RIF conventions. More precisely, sasa writes on stdout a Boolean for each action and each process, that states if the corresponding action is enabled for the current step. Then it reads on stdin a Boolean for each action and each process that tells which actions (among the enabled ones) should be activated.

The daemon can thus be played by users that read and enter Boolean values. In the example above, the user has played t t t t t t t, i.e., it has asked to trigger all the processes (which were all activated at the first step). At the second step, only the process p2 is not activated. In the session above we have chosen to activate only p7.

If one wants to use a test oracle to check at runtime some algorithms properties, one can use lurette as follows:

 cd test/coloring
 make ring.cmxs
 lurette -sut "sasa ring.dot" -oracle "lv6 ring_oracle.lus -n oracle -exec"

Here the oracle is specified in Lustre V6. For more information on this topic: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-oracles/

lurette can also be used to perform simulations with programmed daemons. For instance, in order to simulate an algorithm defined in ring.dot (cf test/coloring) using a Lutin daemon defined in ring.lut, you can launch the following:

 lurette -env "sasa ring.dot -custd" -sut "lutin ring.lut -n distributed"

Note that for lurette, the role of the SUT (System Under Test) and the one of the environment is dual: the outputs of the SUT are the inputs of the environment, and vice-versa. The only difference is that the environment plays first. But sasa needs to play first, to be able to state which actions are enabled at the very first step. Hence sasa is used as a lurette environment, and the daemon program is used a lurette SUT.

For more information on this topic: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-daemons/

sasa -rif and lurette generates .rif files that can be viewed with gnuplot-rif or sim2chro; cf http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/

  sasa --help

usage: sasa [<option>]* <topology>.dot
use -h to see the available options.

--length, -l <int>
            Maximum number of steps to be done (4611686018427387903 by default).

--synchronous-daemon, -sd
            Use a Synchronous daemon
--central-daemon, -cd
            Use a Central daemon (selects exactly one action)
--locally-central-daemon, -lcd
            Use a Locally Central daemon
            (i.e., never activates two neighbors actions in the same step)
--distributed-daemon, -dd
            Use a Distributed daemon (which select at least one action).
            This is the default daemon.
--custom-daemon, -custd
            Use a Custom daemon (forces --rif)
--greedy-daemon, -gd
            Use the daemon that maximizes the potential function at each step.
            Performs 2^|enabled| trials (per step). 
--greedy-central-daemon, -gcd
            Ditto, but restricted to central daemons.
--greedy-deterministic-central-daemon, -gdcd
            Ditto, but always return the same solution.
--exhaustive-daemon, -ed
            Use the daemon that maximizes the number of steps. 
            The search is stopped when the maximum number of steps has been reached 
            (which is controlled by the -l/--length option)
--exhaustive-central-daemon, -ecd
            Ditto, but for central daemons
--es-abort-if-not-progressing <int>
            Abort the exhaustive search if not progressing (i.e., when #step>step(last sol)x<int>).
--es-dfs    Use a depth first search to perform the exploration.
--es-no-tabu
            Do not use Tabu list during the exhaustive search.
--is-no-tabu
            Do not use Tabu list during the initial configuration search.
--local-init-search, -is <int>
            Use local search algorithms to find an initial configuration that pessimize 
            the step number. The argument is the maximum number of trials to do the search. 
            Require the state_to_nums Algo.to_register field to be defined.
--global-init-search, -gis <int>
            Use global (i.e., completely random)  search to find an initial configuration 
            that pessimize the step number. The argument is the maximum number of trials
             to do the search. 
--cores-nb, -cn
            Number of cores to use during --init-search simulations (default is 1)
--outfile, -o
            Generate simulation data in a file (use stdout otherwise)
--seed, -seed <int>
            Set the pseudo-random generator seed of build-in daemons (wins over --replay)
--replay, -replay
            Use the last generated seed to replay the last run
--restart, -restart
            If a fault function has been provided, use it to restart when a legitimate configuration is reached
--version, -version, -v
            Display the sasa version and exit.
--quiet, -q Set the quiet mode (for batch)
--verbose, -vl <int>
            Set the verbose level
--help, -help, -h
            Display main options
--more, -m  Display more options

More sasa options:

  sasa --more

--es-bfs    Use a breadth first search to perform the exploration.
--es-continue-when-best-sol-found
            Do not stop when |path(sol)|=pot(init): this is necessary when E.x phi'(c)>0 (pseudo pot)
--es-dont-cut
            Do not cut path when n.cost < prev_sol.cost : this is useful when E.x phi'(c)>0 (pseudo pot)
--rif, -rif Print only outputs (i.e., behave as a rif input file)
--no-data-file, -nd
            Do not print any data
--gen-dot-at-legit, -gdal
            Generate a dot file initialised with the reached legitimate config
--gen-lutin-daemon, -gld
            Generate Lutin daemons and exit (not finished)
--gen-lustre-oracle-skeleton, -glos
            Generate a Lustre oracle skeleton
--list-algos, -algo
            Output the algo files used in the dot file and exit. 
--gen-register, -reg
            Generates the registering files and exit. 
--dummy-input
            Add a dummy input
--ignore-first-inputs, -ifi
            [Deprecated] make sasa ignore its first input vector
--ocaml-version
            Display the version ocaml version sasa was compiled with and exit.

On debian-based distributions, open a terminal and copy/paste (on other Linux (or mac) distributions, the packages names should be more or less the same):

## Fisrt you need to install opam
sudo apt install -y  opam
opam init -y
eval $(opam env)
echo "test -r ~/.opam/opam-init/init.sh && . ~/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true" >> ~/.bashrc
opam switch create 4.14.1
eval $(opam env)
opam install -y merlin tuareg
opam user-setup install

Once opam is installed:

opam repo add -a verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
opam update -y
opam install -y sasa rdbgui4sasa

# optionally (to perform automated tests):
opam depext  -y lutin || echo "useless with opam >= 2.1"
opam install -y lutin lustre-v6

For running examples in the sasa/test/ directory of the git repo to check the installation has worked:

git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
cd sasa/test/
make test

Follows more or less the same instructions as above, but described into more details in case you want to understand the rationale for each command and adapt it to your distribution.

As using sasa requires to write Ocaml programs, you definitely need to install the Ocaml package manager =opam=. opam works out of the box with most Linux distributions and OSX (mac). opam ought to work on windows too.

sudo apt install -y opam
opam init -y
eval $(opam env)

The opam init ought to have populated your shell resource file with the necessary configurations commands, but it case it didn't you can run something like:

echo "eval $(opam env)" >> ~/.bashrc

Once opam is installed and configured, you may want to install (or not) the last version of the compiler.

opam switch create 4.14.1
eval $(opam env)
echo "eval $(opam env)" >> ~/.bashrc

Then, you need to add the verimag-sync-repo into your set of opam's repository:

opam repo add -a verimag-sync-repo \
  "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
opam update -y

Now you should be able to install sasa:

opam install -y sasa

as well as the rdbgui4sasa Graphical User Interface:

(opam depext -y rdbgui4sasa || echo "useless since opam 2.1") && opam install -y rdbgui4sasa

If you want to be able to use the automated test framework, you can also install the following packages:

opam install -y lustre-v6
(opam depext -y lutin  || echo "useless since opam 2.1") && opam install -y lutin

Then, if one day you want to upgrade your sasa version:

opam update
opam upgrade

You will need:

• make (gnu)
• git
• graphviz
• lablgtk3
• opam

For instance, on ubuntu,

apt install graphviz git make lablgtk3 opam

And of course you need ocaml. And a set of tools installable via opam

• dune
• ocamlgraph
• rdbg
• lutin (not for compiling actually, but for using sasa with custom daemons)

Hence, once opam is installed, one just need to:

opam install --deps-only ./sasa.opam

And then:

git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
cd sasa
make
make install
make test

One can also mimic the content of the test job in the project .gitlab-ci.yml Gitlab CI script.

cf the Docker Install section of the Synchrone Reactive Tool Box. This docker image contains all the tools mentioned in this section (sasa, lustre, opam, ocaml, emacs, graphviz, etc.).

http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/sasaVM.ova

• login:sasa
• passwd:sasa

Yes.

Beside, some tutorials are also available here: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/

• Look at recent .log files (e.g., rdbg.log); they sometimes contain more information than what is printed onto the screen.
• Do a make clean
• Read carefully the error message. Sometimes it helps.
• If the message is totally useless, please feel free to add an issue here https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/issues

Most probably you a try to compare 2 's Algo.neighbor. It's an abstract type, hence you cannot compare them, i.e., you cannot use Stdlib.compare, nor its twins (<>, >, <, etc.), nor functions that use them (min, max, List.sort, etc.). You should compare their pid instead (if the network is not anonymous).