-[Running batch simulations with Built-in daemons](#orgf957f59)
-[Running batch simulations with Built-in daemons](#orgf58fe90)
-[Running batch simulations with manual (a.k.a. custom) daemons](#org2ac3779)
-[Running batch simulations with manual (a.k.a. custom) daemons](#orgf6edca9)
-[Running batch simulations with `lurette`](#org3973e9b)
-[Running batch simulations with `lurette`](#org1e373f4)
-[Viewing Results](#org50909cc)
-[Viewing Results](#orgd0dea06)
-[The `sasa` CLI](#orgdcc2767)
-[The `sasa` CLI](#org60eecdb)
-[Interactive mode](#orgb7d8cc6)
-[Interactive mode](#org7e515d7)
-[Example: use `rdbg` from the `test/alea-coloring/` directory](#org6db5eef)
-[Example: use `rdbg` from the `test/alea-coloring/` directory](#org7be2907)
-[The examples of test directory](#org34cef43)
-[The examples of test directory](#org674a21c)
-[Running interactive sessions with `rdbg`](#org42e0a4c)
-[Running interactive sessions with `rdbg`](#orgf781d43)
-[Getting `rdbg` on-line help](#org9306ae6)
-[Getting `rdbg` on-line help](#org3832092)
-[A `rdbg` `sasa` GUI](#org2b3110e)
-[A `rdbg` `sasa` GUI](#orgc8042a6)
-[Useful Modules](#org6ec961a)
-[Useful Modules](#org4c80d42)
-[Install](#org32bb903)
-[Install](#orgd7160ac)
-[TL;DR](#org53b0731)
-[TL;DR](#org0611b2e)
-[Not strictly mandatory, but useful, third-party software](#org5b78530)
-[Not strictly mandatory, but useful, third-party software](#org449a2c8)
-[Install `sasa` via opam (version >= 2.\*)](#orgd860979)
-[Install `sasa` via opam (version >= 2.\*)](#org5129260)
-[Install `sasa` via `git`](#org435098a)
-[Install `sasa` via `git`](#org3048efb)
-[Use `sasa` via docker](#org0f52d25)
-[Use `sasa` via docker](#org19a7db8)
-[Use `sasa` via a Virtual Machine](#org37d6abb)
-[Use `sasa` via a Virtual Machine](#orgcbbbb16)
-[Screencasts](#org1ace131)
-[Screencasts](#org73741f6)
-[More](#orgce24451)
-[More](#orgbad2570)
-[FAQ](#org75b5edb)
-[FAQ](#org4b28265)
-[Is there a FAQ?](#orgcef3a3f)
-[Is there a FAQ?](#org7243183)
-[I have a compilation error that I don't understand](#org602d497)
-[I have a compilation error that I don't understand](#org2f7cf1b)
-[I have the error `Invalid_argument("compare: functional value")`](#org71301ed)
-[I have the error `Invalid_argument("compare: functional value")`](#orgbeadae9)
<aid="orgf2470e2"></a>
<aid="orgd1705b0"></a>
# TL;DR
# TL;DR
<aid="org8949e4a"></a> SASA is a **Self-stabilizing Algorithms SimulAtor**, based on the so-called **Atomic State model** (ASM) introduced by <spanclass="underline">Dijkstra</span> in its seminal article on [Self-stabilizing distributed algorithms](http://www.cs.utexas.edu/~EWD/ewd04xx/EWD426.PDF). This model is also sometimes named "locally shared memory model with composite atomicity"
<aid="orgc103e09"></a> SASA is a **Self-stabilizing Algorithms SimulAtor**, based on the so-called **Atomic State model** (ASM) introduced by <spanclass="underline">Dijkstra</span> in its seminal article on [Self-stabilizing distributed algorithms](http://www.cs.utexas.edu/~EWD/ewd04xx/EWD426.PDF). This model is also sometimes named "locally shared memory model with composite atomicity"
Basically, one needs to provide:
Basically, one needs to provide:
...
@@ -61,11 +61,11 @@ sasa ring.dot -l 4 # run a batch simulation for 4 steps
...
@@ -61,11 +61,11 @@ sasa ring.dot -l 4 # run a batch simulation for 4 steps
<aid="org3ddd7ad"></a><aid="orga64c3dd"></a> The topology is given via `.dot` files, that should
<aid="org42e1c30"></a><aid="orgad922eb"></a> The topology is given via `.dot` files, that should
1. follow the [graphviz/dot format](https://en.wikipedia.org/wiki/DOT_(graph_description_language))
1. follow the [graphviz/dot format](https://en.wikipedia.org/wiki/DOT_(graph_description_language))
2. have nodes **labeled** by the `algo` field
2. have nodes **labeled** by the `algo` field
...
@@ -121,14 +121,14 @@ graph ring {
...
@@ -121,14 +121,14 @@ graph ring {
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).
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](#orgb220121) to generate such kinds of `dot` graphs: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/>
Some tools are provided in the `sasa`[distributions](#orgc01ca5e) to generate such kinds of `dot` graphs: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/>
<aid="orgce59185"></a>
<aid="orgdba5582"></a>
# Algorithms
# Algorithms
<aid="org9de8fa1"></a>
<aid="org65cdf87"></a>
The following has been generated from [algo.mli](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli)
The following has been generated from [algo.mli](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli)
...
@@ -140,7 +140,7 @@ The following has been generated from [algo.mli](https://gricad-gitlab.univ-gren
...
@@ -140,7 +140,7 @@ The following has been generated from [algo.mli](https://gricad-gitlab.univ-gren
</iframe>
</iframe>
<aid="orgec5f4e7"></a>
<aid="org33bb233"></a>
# Examples
# Examples
...
@@ -180,14 +180,14 @@ The `test` directory also contains sub-directories which gathers programs shared
...
@@ -180,14 +180,14 @@ The `test` directory also contains sub-directories which gathers programs shared
-`test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (if it exists).
-`test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (if it exists).
<aid="org30a5d38"></a>
<aid="org5f5c4f5"></a>
# Batch mode
# Batch mode


<aid="org86a8c98"></a>
<aid="orgc2ed5bc"></a>
## Running batch simulations
## Running batch simulations
...
@@ -228,27 +228,23 @@ All the CLI commands above can be run automatically using a `make` rule containe
...
@@ -228,27 +228,23 @@ All the CLI commands above can be run automatically using a `make` rule containe
#outs 1 1 1 0 0 0 0 t t t t t t t f t t f f t t f 10.
#outs 0 1 0 0 1 0 1 f f t t f f f f f f t f f f f 2.
#step 1
#step 1
#outs 1 0 2 0 0 1 2 f f f t t f f f f f t t f f f 2.
#outs 0 1 0 2 1 0 1 f f f f f f f f f f t f f f t 0.
#step 2
#outs 1 0 2 1 2 1 2 f f f f f f f f f f t t f f t 0.
This algo is silent after 6 moves, 2 steps, 2 rounds.
This algo is silent after 1 move, 1 step, 1 round.
q
q
#quit
#quit
...
@@ -257,7 +253,7 @@ All the CLI commands above can be run automatically using a `make` rule containe
...
@@ -257,7 +253,7 @@ All the CLI commands above can be run automatically using a `make` rule containe
nb: the simulation output (in the green frame) follows the [RIF](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orga43b00b) conventions.
nb: the simulation output (in the green frame) follows the [RIF](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orga43b00b) conventions.
<aid="orgf957f59"></a>
<aid="orgf58fe90"></a>
## Running batch simulations with Built-in daemons
## Running batch simulations with Built-in daemons
...
@@ -276,7 +272,7 @@ sasa -h | grep "\-daemon"
...
@@ -276,7 +272,7 @@ sasa -h | grep "\-daemon"
--greedy-daemon, -gd
--greedy-daemon, -gd
<aid="org2ac3779"></a>
<aid="orgf6edca9"></a>
## Running batch simulations with manual (a.k.a. custom) daemons
## Running batch simulations with manual (a.k.a. custom) daemons
...
@@ -314,7 +310,7 @@ In order to enter such input more easily, one can use (requires [the lustre V4 t
...
@@ -314,7 +310,7 @@ In order to enter such input more easily, one can use (requires [the lustre V4 t
Daemons can also by simulated by [`lutin`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-4) programs via the use of [`lurette`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-9)(for batch executions) or [`rdbg`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-10)(for interactive sessions).
Daemons can also by simulated by [`lutin`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-4) programs via the use of [`lurette`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-9)(for batch executions) or [`rdbg`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-10)(for interactive sessions).
<aid="org3973e9b"></a>
<aid="org1e373f4"></a>
## Running batch simulations with `lurette`
## Running batch simulations with `lurette`
...
@@ -339,14 +335,14 @@ Note that for `lurette`, the role of the SUT (System Under Test) and the one of
...
@@ -339,14 +335,14 @@ Note that for `lurette`, the role of the SUT (System Under Test) and the one of
For more information on this topic: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-daemons/>
For more information on this topic: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-daemons/>
<aid="org50909cc"></a>
<aid="orgd0dea06"></a>
## Viewing Results
## Viewing Results
`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 -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/>
<aid="orgdcc2767"></a>
<aid="org60eecdb"></a>
## The `sasa` CLI
## The `sasa` CLI
...
@@ -415,11 +411,11 @@ More `sasa` options:
...
@@ -415,11 +411,11 @@ More `sasa` options:
Display the version ocaml version sasa was compiled with and exit.
Display the version ocaml version sasa was compiled with and exit.
<aid="orgb7d8cc6"></a>
<aid="org7e515d7"></a>
# Interactive mode
# Interactive mode
<aid="orgd358e1f"></a> If you want to perform step-by-step simulations, you can use the `-custd` option. But if you want to perform step-by-step simulations without the burden of playing the role of the daemon, you can launch `sasa` under the control of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/).
<aid="orgbabc457"></a> If you want to perform step-by-step simulations, you can use the `-custd` option. But if you want to perform step-by-step simulations without the burden of playing the role of the daemon, you can launch `sasa` under the control of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/).
Another advantage of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/) is its ability to display a graphical view of the current configuration during the simulation, to move step by step, or round by round, forward or backwards.
Another advantage of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/) is its ability to display a graphical view of the current configuration during the simulation, to move step by step, or round by round, forward or backwards.
Before reading this section, please read at least the [Basic usage Section if the rdbg documentation](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/README.html#outline-container-sec-3).
Before reading this section, please read at least the [Basic usage Section if the rdbg documentation](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/README.html#outline-container-sec-3).
<aid="org6db5eef"></a>
<aid="org7be2907"></a>
## Example: use `rdbg` from the `test/alea-coloring/` directory
## Example: use `rdbg` from the `test/alea-coloring/` directory
...
@@ -471,7 +467,7 @@ rdbg
...
@@ -471,7 +467,7 @@ rdbg
[q] quit
[q] quit
<aid="org34cef43"></a>
<aid="org674a21c"></a>
## The examples of test directory
## The examples of test directory
...
@@ -482,13 +478,13 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t
...
@@ -482,13 +478,13 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t
-`test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (it it exists).
-`test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (it it exists).
<aid="org42e0a4c"></a>
<aid="orgf781d43"></a>
## Running interactive sessions with `rdbg`
## Running interactive sessions with `rdbg`
1. type `rdbg`
1. type `rdbg`
2. press enter to load the defaut session (`rdbg-session.ml`). Then you can type:
2. press enter to load the defaut session (`rdbg-session.ml`). Then you can type:
3.`d` for displaying a (dynamic) dot graph with `dot`
3.`gv` (graph view) for displaying a (dynamic) dot graph with `dot`
4. or ALTERNATIVELY `ne` to use the `neato` layout engine (`tw`, `ci`, `fd`, `sf`, `pa`, `os` to use the `twopi`, `circo`, `fdp`, `sfd`, `patchwork`, `osage` layout engines respectively)
4. or ALTERNATIVELY `ne` to use the `neato` layout engine (`tw`, `ci`, `fd`, `sf`, `pa`, `os` to use the `twopi`, `circo`, `fdp`, `sfd`, `patchwork`, `osage` layout engines respectively)
5.`s` to move one step forward
5.`s` to move one step forward
6.`sd` to move one step forward and call `d` (to update the graph display [])
6.`sd` to move one step forward and call `d` (to update the graph display [])
...
@@ -499,14 +495,14 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t
...
@@ -499,14 +495,14 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t
All those commands are defined in (the common) [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml) that is included in (locals) `test/*/my-rdbg-tuning.ml` that are included in (generated) `test/*/rdbg-session.ml` files. `my-rdbg-tuning.ml` contains straigthforward `ocaml` code that defines various `rdbg` shortcuts to ease the simulation of `sasa` systems. Feel free to tailor those command to yours needs by modyfying the local `my-rdbg-tuning.ml`!
All those commands are defined in (the common) [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml) that is included in (locals) `test/*/my-rdbg-tuning.ml` that are included in (generated) `test/*/rdbg-session.ml` files. `my-rdbg-tuning.ml` contains straigthforward `ocaml` code that defines various `rdbg` shortcuts to ease the simulation of `sasa` systems. Feel free to tailor those command to yours needs by modyfying the local `my-rdbg-tuning.ml`!
<aid="org9306ae6"></a>
<aid="org3832092"></a>
## Getting `rdbg` on-line help
## Getting `rdbg` on-line help
Here are 2 useful entry-points to rdbg on-line help:
Here are 2 useful entry-points to rdbg on-line help:
1.`rdbg --help` and
1.`rdbg --help` and
2. at the `rdbg --sasa` prompt, you can use the `l` command:
2. at the `rdbg` prompt, you can use the `l` command:
```sh
```sh
(rdbg) l
(rdbg) l
...
@@ -595,21 +591,21 @@ Here are 2 useful entry-points to rdbg on-line help:
...
@@ -595,21 +591,21 @@ Here are 2 useful entry-points to rdbg on-line help:
(rdbg)
(rdbg)
<aid="org2b3110e"></a>
<aid="orgc8042a6"></a>
## A `rdbg` `sasa` GUI
## A `rdbg` `sasa` GUI
To install it:
To install it:
```sh
```sh
opam depext -y rdbgui4ocaml
opam depext -y rdbgui4ocaml-- useless with opam >= 2.1
opam install-y rdbgui4ocaml
opam install-y rdbgui4ocaml
```
```
To use it: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/>
To use it: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/>
<aid="org6ec961a"></a>
<aid="org4c80d42"></a>
## Useful Modules
## Useful Modules
...
@@ -644,14 +640,14 @@ Some modules, used by the sasa core engine, can be useful from `rdbg`.
...
@@ -644,14 +640,14 @@ Some modules, used by the sasa core engine, can be useful from `rdbg`.
</iframe>
</iframe>
<aid="org32bb903"></a>
<aid="orgd7160ac"></a>
# Install
# Install
<aid="orgb220121"></a><aid="orge68345c"></a>
<aid="orgc01ca5e"></a><aid="orge8ea2a3"></a>
<aid="org53b0731"></a>
<aid="org0611b2e"></a>
## TL;DR
## TL;DR
...
@@ -682,7 +678,7 @@ opam install -y sasa
...
@@ -682,7 +678,7 @@ opam install -y sasa
And optionally (to define test oracles in Lustre or daemons in Lutin):
And optionally (to define test oracles in Lustre or daemons in Lutin):
```sh
```sh
opam depext -y rdbgui4sasa lutin
opam depext -y rdbgui4sasa lutin-- useless with opam >= 2.1
One can also mimic the content of the `test` job in the project [.gitlab-ci.yml Gitlab CI script](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml).
One can also mimic the content of the `test` job in the project [.gitlab-ci.yml Gitlab CI script](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml).
<aid="org0f52d25"></a>
<aid="org19a7db8"></a>
## Use `sasa` via docker
## Use `sasa` via docker
cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#docker). This docker image contains all the tools mentioned in this section (`sasa`, `lustre`, `opam`, `ocaml`, emacs, graphviz, etc.).
cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#docker). This docker image contains all the tools mentioned in this section (`sasa`, `lustre`, `opam`, `ocaml`, emacs, graphviz, etc.).
<aid="org37d6abb"></a>
<aid="orgcbbbb16"></a>
## Use `sasa` via a Virtual Machine
## Use `sasa` via a Virtual Machine
...
@@ -843,7 +839,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve
...
@@ -843,7 +839,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve
- passwd:sasa
- passwd:sasa
<aid="org1ace131"></a>
<aid="org73741f6"></a>
# Screencasts
# Screencasts
...
@@ -859,7 +855,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve
...
@@ -859,7 +855,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve
Beside, some tutorials are also available here: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/>
Beside, some tutorials are also available here: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/>
<aid="org602d497"></a>
<aid="org2f7cf1b"></a>
## I have a compilation error that I don't understand
## I have a compilation error that I don't understand
...
@@ -892,7 +888,7 @@ Beside, some tutorials are also available here: <https://verimag.gricad-pages.un
...
@@ -892,7 +888,7 @@ Beside, some tutorials are also available here: <https://verimag.gricad-pages.un
- 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>
- 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>
<aid="org71301ed"></a>
<aid="orgbeadae9"></a>
## I have the error `Invalid_argument("compare: functional value")`
## I have the error `Invalid_argument("compare: functional value")`