diff --git a/guides/users/Makefile b/guides/users/Makefile
index 2ff6311b683a54cc16f3b56707d0789b734ed219..5281ccbcf3da713fe87e4aa405f6bce361c1fd8c 100644
--- a/guides/users/Makefile
+++ b/guides/users/Makefile
@@ -1,5 +1,5 @@
-all:README.html README.md algo
+all:README.html algo
# always work via dockver ...
dockver:
@@ -9,21 +9,21 @@ algo:
cd ../..; make odoc
cp -rf ../../_build/default/_doc/_html .
-%.html:%.org
+%.html:%.org
emacs --batch --load=emacs-org.el \
--visit=$*.org --funcall org-html-export-to-html
-%.md:%.org
+%.md:%.org
emacs --batch --eval="(add-to-list 'load-path \".\")" --load=emacs-org.el --visit=$*.org --funcall org-md-export-to-markdown
-%.html3:%.org
+%.html3:%.org
emacs --batch --eval="(add-to-list 'load-path \".\") (add-to-list 'load-path \"./el\")" --eval="(require 'htmlize)" --load=emacs-org.el \
--visit=$*.org --funcall org-html-export-to-html
EMACS=emacs \
--load=htmlize.el \
--load=el/ob-ocaml.el \
- --load=emacs-org.el
+ --load=emacs-org.el
%.html2:
$(EMACS) --visit=$*.org --funcall org-html-export-to-html --eval "(kill-emacs)" -Q
diff --git a/guides/users/README.md b/guides/users/README.md
index acb86af0212aa55042ef82f3850cace30d02eb28..173b5a4b463a559d68c5ae52f5afcb6b1d0d98c3 100644
--- a/guides/users/README.md
+++ b/guides/users/README.md
@@ -1,57 +1,58 @@
-- [TL;DR](#orgbd271a9)
-- [Topology](#org7f566fb)
-- [Algorithms](#org59c1a68)
-- [Examples](#orgf365ef6)
-- [Batch mode](#orgba350a9)
- - [Running batch simulations](#org71360af)
- - [Running batch simulations with Built-in daemons](#org71fc9c6)
- - [Running batch simulations with manual (a.k.a. custom) daemons](#org32785d9)
- - [Running batch simulations with `lurette`](#orge5f0aff)
- - [Viewing Results](#orgf4a3e62)
- - [The `sasa` CLI](#org37b1328)
-- [Interactive mode](#org3ee1c63)
- - [Example: use `rdbg` from the `test/alea-coloring/` directory](#org6223994)
- - [The examples of test directory](#org7361545)
- - [Running interactive sessions with `rdbg`](#org6e733a2)
- - [Getting `rdbg` on-line help](#org4cd47c7)
- - [A `rdbg` `sasa` GUI](#org6831b5f)
- - [Useful Modules](#org9884b00)
-- [Install](#org160a81b)
- - [Install `sasa` via opam: TL;DR](#org7ffb4e0)
- - [Install `sasa` via opam (long version)](#org868c435)
- - [Not strictly mandatory, but useful, third-party software](#org321ff97)
- - [Install `sasa` via `git`](#orgf73d6fa)
- - [Use `sasa` via docker](#org398ecef)
- - [Use `sasa` via a Virtual Machine](#org314e70c)
-- [Screencasts](#orge319dc9)
-- [More](#org34a195d)
-- [FAQ](#orgab249a2)
- - [Is there a FAQ?](#orgf9ef9e9)
- - [I have a compilation error that I don't understand](#orge2003dc)
- - [I have the error `Invalid_argument("compare: functional value")`](#orgccdb4e5)
-
-
-
-<a id="orgbd271a9"></a>
+
+# Table of Contents
+
+1. [TL;DR](#org88ccf0f)
+2. [Topology](#org71c4116)
+3. [Algorithms](#orga8d8246)
+4. [Examples](#org3032033)
+5. [Batch](#orgf72af8e)
+ 1. [TL;DR](#orgbbc6550)
+ 2. [Running batch simulations](#org778d871)
+ 3. [Running batch simulations with Built-in daemons](#orgf216e5a)
+ 4. [Running batch simulations with manual (a.k.a. custom) daemons](#org7d493a4)
+ 5. [Running batch simulations with `lurette`](#orgbd07729)
+ 6. [Viewing Results](#orgef391e1)
+ 7. [The `sasa` CLI](#org0432c0c)
+6. [Interactive simulations](#org1ba91e7)
+7. [Install](#org22e2b0f)
+ 1. [Install `sasa` via opam: TL;DR](#org192cc6c)
+ 2. [Install `sasa` via `opam` (long version)](#org3e48a1e)
+ 1. [Not strictly mandatory, but useful, third-party software](#orgf3e25d3)
+ 3. [Install `sasa` via `git`](#orgcc3ffbf)
+ 4. [Use `sasa` via docker](#orgb26c877)
+ 5. [Use `sasa` via a Virtual Machine](#org5f678fe)
+8. [Screencasts](#org2efcd1b)
+9. [More](#org4645def)
+10. [FAQ](#org4a28da4)
+ 1. [Is there a FAQ?](#orgb7d347f)
+ 2. [I have a compilation error that I don't understand](#org7e0f941)
+ 3. [I have the error `Invalid_argument("compare: functional value")`](#orga50b299)
+
+
+
+<a id="org88ccf0f"></a>
# TL;DR
-<a id="orgf830fc6"></a> SASA is a **Self-stabilizing Algorithms SimulAtor**, based on the so-called **Atomic State model** (ASM) introduced by <span class="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"
+<a id="org1ca248c"></a> SASA is a **Self-stabilizing Algorithms SimulAtor**, based on
+the so-called **Atomic State model** (ASM) introduced by <span class="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:
-1. a topology, made of nodes and transitions (via a [dot](https://en.wikipedia.org/wiki/DOT_(graph_description_language)) file)
+1. a topology, made of nodes and transitions (via a [dot](https://en.wikipedia.org/wiki/DOT_(graph_description_language)) file)
2. the algorithms attached to nodes (via [`ocaml`](https://ocaml.org/) programs)
-The fastest way to get started is to copy the files provided in the `test/skeleton` directory, and to modify them:
+The fastest way to get started is to copy the files provided in the
+`test/skeleton` directory, and to modify them:
-```sh
-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
-```
+ 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
- [SASA source code](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa)
- [Some Online Tutorials](https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/)
@@ -59,79 +60,84 @@ sasa ring.dot -l 4 # run a batch simulation for 4 steps
- [Video of a SASA tutorial given at SSS'2020](https://cloud.univ-grenoble-alpes.fr/index.php/s/yboMr4xbcpWr6d9)
- [Slides](https://cloud.univ-grenoble-alpes.fr/s/dRriW4c2bWinagw)
-[](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/poster.pdf)
-
-<a id="org7f566fb"></a>
+<a id="org71c4116"></a>
# Topology
-<a id="org8f2889a"></a> <a id="org193d09e"></a> The topology is given via `.dot` files, that should
+<a id="orgf9f1890"></a>
+<a id="orgfdd5258"></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))
-2. have nodes **labeled** by the `algo` field
-
-```dot
-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
-}
-```
+2. 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
+ }
Of course the `some_algo.ml` file must exist and contains an algorithm.
-nb : sasa uses ml files, and salut lustre files. Therefore the extension used in this `algo` field is actually ignored by tools. Then sasa will remove the extension, and add an `.ml` one, while salut will add a `.lus` one.
-
-In order to define an initial configuration, one can use the `init` node [attribute](http://www.graphviz.org/doc/info/attrs.html).
-
-```dot
-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
-}
-```
-
-One can use graph [attributes](http://www.graphviz.org/doc/info/attrs.html) to set parameters that can be used by all nodes during the simulation.
-
-```dot
-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
-}
-```
+nb : sasa uses ml files, and salut lustre files. Therefore the extension used
+in this `algo` field is actually ignored by tools. Then sasa will
+remove the extension, and add an `.ml` one, while salut will
+add a `.lus` one.
+
+In order to define an initial configuration, one can use the `init`
+node [attribute](http://www.graphviz.org/doc/info/attrs.html).
+
+ 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
+ }
+
+One can use graph [attributes](http://www.graphviz.org/doc/info/attrs.html) 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
+ }
-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](#org21de61c) 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](#orged6bed8) to generate such
+kinds of `dot` graphs:
+<https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/>
-<a id="org59c1a68"></a>
+<a id="orga8d8246"></a>
# Algorithms
-<a id="org779e381"></a>
+<a id="orgf6378eb"></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)
@@ -143,135 +149,149 @@ The following has been generated from [algo.mli](https://gricad-gitlab.univ-gren
</iframe>
-<a id="orgf365ef6"></a>
+<a id="org3032033"></a>
# Examples
-```sh
-git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
-cd sasa/test
-```
+ git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
+ cd sasa/test
-The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test) directory contains various examples of self-stabilizing distributed programs taken from the book \`\`Introduction to Distributed Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit.
+The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test) directory contains various examples of self-stabilizing
+distributed programs taken from the book \`\`Introduction to Distributed
+Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit.
1. `test/skeleton/`: a fake algorithm meant to be used as a skeleton
2. `test/dijkstra-ring/`: Dijkstra token ring
3. `test/unison/`: Synchronous unison
4. `test/coloring/`: a graph coloring algorithm
5. `test/alea-coloring/`: a randomized variant of the previous one
-6. `test/bfs-spanning-tree/`: a Breadth First Search Spanning tree construction
-
-It also contains implementations of algorithms found in the literature:
+6. `test/bfs-spanning-tree/`: a Breadth First Search Spanning tree
+ construction
+
+It also contains implementations of algorithms found in the
+literature:
+
+1. `test/async-unison/`: Asynchronous unison ("Asynchronous
+ unison" by Couvreur, J., Francez, N., and Gouda, M. G. in 1992)
+2. `test/st-CYH91`: another Spanning tree construction ("A
+ self-stabilizing algorithm for constructing spanning trees" by Chen,
+ Yu, and Huang in 1991)
+3. `test/bfs-st-HC92`: another BFS Spanning tree construction ("A
+ self-stabilizing algorithm for constructing breadth-first trees" by
+ Huang and Chen in 1992)
+4. `test/st-KK06_algo1` and `test/st-KK06_algo2`: another Spanning tree
+ construction ("A Self-stabilizing Algorithm for Finding a Spanning
+ Tree in a Polynomial Number of Moves" by Kosowski and Kuszner, 2006)
+5. `test/dfs/`: a Depth First Search using arrays (the \`\`atomic state
+ model'' version of a [Depth First Search algorithm proposed by Collin and Dolev in 1994](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf))
+6. `test/dfs-list/`: the same Depth First Search, but using lists
+ instead or arrays
+7. `test/rsp-tree/`: The Algorithm 1 of "Self-Stabilizing Disconnected
+ Components Detection and Rooted Shortest-Path Tree Maintenance in
+ Polynomial Steps" by Stéphane Devismes, David Ilcinkas, Colette
+ Johnen.
+
+Each directory contains working examples, which are checked using the
+Continuous Integration facilities of Gitlab (cf the [.gitlab-ci.yml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml)
+script and the [CI pipelines](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/pipelines) results).
+
+If you want to reproduce or understand what those non-regression
+tests do, uo can have a look at the `test/*/Makefile` files, present
+in each directory (which all include the [test/Makefile.inc](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc)and the
+[test/Makefile.dot](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.dot) ones).
+
+The `test` directory also contains sub-directories which gather
+programs shared by all examples:
+
+- `test/lustre/`: contains Lustre programs used as (`test/*/*.lus`) oracles
+- `test/rdbg-utils/`: contains `ocaml` functions that can be used from
+ `rdbg`
+
+
+<a id="orgf72af8e"></a>
+
+# Batch
-1. `test/async-unison/`: Asynchronous unison ("Asynchronous unison" by Couvreur, J., Francez, N., and Gouda, M. G. in 1992)
-2. `test/st-CYH91`: another Spanning tree construction ("A self-stabilizing algorithm for constructing spanning trees" by Chen, Yu, and Huang in 1991)
-3. `test/bfs-st-HC92`: another BFS Spanning tree construction ("A self-stabilizing algorithm for constructing breadth-first trees" by Huang and Chen in 1992)
-4. `test/st-KK06_algo1` and `test/st-KK06_algo2`: another Spanning tree construction ("A Self-stabilizing Algorithm for Finding a Spanning Tree in a Polynomial Number of Moves" by Kosowski and Kuszner, 2006)
-5. `test/dfs/`: a Depth First Search using arrays (the \`\`atomic state model'' version of a [Depth First Search algorithm proposed by Collin and Dolev in 1994](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf))
-6. `test/dfs-list/`: the same Depth First Search, but using lists instead or arrays
-7. `test/rsp-tree/`: The Algorithm 1 of "Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps" by Stéphane Devismes, David Ilcinkas, Colette Johnen.
-
-Each directories contains working examples, which are checked using the Continuous Integration facilities of Gitlab (cf the [.gitlab-ci.yml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml) script and the [CI pipelines](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/pipelines) results).
-
-If you want to reproduce or understand what those non-regression tests do, please look at the `test/*/Makefile`, present in each directory (which all include the [test/Makefile.inc](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc) one).
-
-The `test` directory also contains sub-directories which gathers programs shared by all examples:
+
-- `test/lustre/`: contains Lustre programs used as (`test/*/*.lus`) oracles
-- `test/rdbg-utils/`: contains `ocaml` functions that can be used from `rdbg`
-- `test/my-rdbg-tuning.ml`: contains useful shortcuts/commands that can be used from `rdbg`.
-- `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).
+<a id="orgbbc6550"></a>
-<a id="orgba350a9"></a>
+## TL;DR
-# Batch mode
+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
-<a id="org71360af"></a>
+<a id="org778d871"></a>
## Running batch simulations
-Once you have defined your algorithm and your topology, you can launch batch simulations with the `sasa` Command Line Interface. To do that, one needs to:
+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
+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.
+The easiest way to get registration code is to let `sasa` generate it.
-```:eval
-cd test/coloring
-sasa -reg ring.dot
-```
+ 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:
+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).
+- `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).
+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).
-```:eval
-ocamlfind ocamlopt -shared -package algo state.ml p.ml config.ml ring.ml -o ring.cmxs
-```
+ 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:
+Now we are ready to launch our first batch simulation:
-```:eval
-sasa ring.dot
-```
+ sasa ring.dot
-All the CLI commands above can be run automatically using a `make` rule contained in [test/Makefile.inc](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc). Hence, by including this file the `Makefile` of the current directory (cf [test/coloring/Makefile](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/coloring/Makefile)), one can generate the `ring.cmxs` file straightforwardly:
+But all of these commands can actually be automated with `make` and `dune`:
-```sh
- cd test/coloring # from the sasa git repository
- make ring.cmxs # compile what's need to be compiled
- sasa ring.dot # launch the simulation
-```
+ make ring.cxms
- make: 'ring.cmxs' is up to date.
- # Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.8.0" ("65d9837")
- # on crevetete the 12/12/2022 at 10:53:48
- #sasa ring.dot
-
- #seed 914504953
- #inputs
- #outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool "legitimate":bool potential:real round:bool round_nb:int
-
-
- #step 0
- #outs 0 1 1 0 1 1 1 f t t f t t t f f f f f t f f 6. f 0
-
- #step 1
- #outs 0 1 1 0 1 0 1 f t t f f f f f t t f f f f f 2. f 1
-
- #step 2
- #outs 0 2 2 0 1 0 1 f t t f f f f f t t f f f f f 2. t 2
-
- #step 3
- #outs 0 1 1 0 1 0 1 f t t f f f f f t f f f f f f 2. t 3
-
- #step 4
- #outs 0 2 1 0 1 0 1 f f f f f f f f f f f f f f t 0. t 3
-
- This algo is silent after 6 moves, 4 steps, 3 rounds.
-
- #quit
+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](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/) conventions.
-<a id="org71fc9c6"></a>
+<a id="orgf216e5a"></a>
## Running batch simulations with Built-in daemons
-By default, the distributed daemon is used to activate enabled actions. Several other daemons can be used, via one of the following options:
+By default, the distributed daemon is used to activate enabled actions.
+Several other daemons can be used, via one of the following options:
-```sh
-sasa -h | grep "\-daemon"
-```
+ sasa -h | grep "\-daemon"
--synchronous-daemon, -sd
--central-daemon, -cd
@@ -282,85 +302,85 @@ sasa -h | grep "\-daemon"
--greedy-daemon, -gd
-<a id="org32785d9"></a>
+<a id="org7d493a4"></a>
## Running batch simulations with manual (a.k.a. custom) daemons
-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.
-
-```sh
-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
-```
-
- sasa -reg ring.dot
- ocamlfind ocamlopt -package algo -shared state.ml unison.ml config.ml ring.ml -o ring.cmxs
- #inputs "p1_g":bool "p2_g":bool "p3_g":bool "p4_g":bool "p5_g":bool "p6_g":bool "p7_g":bool
- #outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_g":bool "Enab_p2_g":bool "Enab_p3_g":bool "Enab_p4_g":bool "Enab_p5_g":bool "Enab_p6_g":bool "Enab_p7_g":bool
-
- 2 2 5 1 3 3 4 t t t t t t t
- 3 3 2 2 2 4 3 t f t t t t t
- 3 3 2 2 2 4 4 t f t t t t f
-
-In the custom daemon mode, the daemon is executed outside `sasa`, by a process that communicates via the standard input/output using [RIF](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orga43b00b) 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`.
+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.
-In order to enter such input more easily, one can use (requires [the lustre V4 tool box](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html)): [`luciole-rif`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orgc145c58)
+ 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
-```sh
- luciole-rif 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](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orga43b00b)
+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.
-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).
+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`.
-<a id="orge5f0aff"></a>
+<a id="orgbd07729"></a>
## Running batch simulations with `lurette`
-If one wants to use a test oracle to check at runtime some algorithms properties, one can use `lurette` as follows:
+If one wants to use a test oracle to check at runtime some
+algorithms properties, one can use `lurette` as follows:
-```sh
- cd test/coloring
- make ring.cmxs
- lurette -sut "sasa ring.dot" -oracle "lv6 ring_oracle.lus -n oracle -exec"
-```
+ 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/>
+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](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/coloring)) using a Lutin daemon defined in `ring.lut`, you can launch the following:
+`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](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/coloring)) using a Lutin daemon defined in
+`ring.lut`, you can launch the following:
-```sh
- lurette -env "sasa ring.dot -custd" -sut "lutin ring.lut -n distributed"
-```
+ 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.
+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/>
-<a id="orgf4a3e62"></a>
+<a id="orgef391e1"></a>
## 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/>
-<a id="org37b1328"></a>
+<a id="org0432c0c"></a>
## The `sasa` CLI
-```sh
- sasa --help
-```
+ sasa --help
- usage: sasa [<option>]* <topology>.dot
+ usage: sasa [<option>]* <topology>.dot
use -h to see the available options.
--length, -l <int>
@@ -416,13 +436,13 @@ For more information on this topic: <https://verimag.gricad-pages.univ-grenoble-
More `sasa` options:
-```sh
- sasa --more
-```
+ sasa --more
--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
@@ -439,385 +459,196 @@ More `sasa` options:
Display the version ocaml version sasa was compiled with and exit.
-<a id="org3ee1c63"></a>
+<a id="org1ba91e7"></a>
-# Interactive mode
+# Interactive simulations
-<a id="orga5621e7"></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/).
+In order to run interactive simulations, one can run `sasa` under the control of
+`rdbgui4sasa`. More specifically, instead of running
-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.
+ sasa ring4.dot
-cf <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbg-sasa/>
+you run
-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).
+ rdbgui4sasa -sut "sasa ring4.dot"
+The name `rdbgui4sasa` comes from the fact that is it GUI designed
+for `sasa`, that is built on top of `rdbg`, but you don't need to
+know `rdbg` to use `rdbgui4sasa`. XXX add rdbg link
-<a id="org6223994"></a>
+The `-sut` option stands for "System Under Test". This terminology
+comes from the fact that `rdbg` is an extension of `lurette`, which
+is an automated testing tool.
-## Example: use `rdbg` from the `test/alea-coloring/` directory
+All the CLI options of `sasa` can be used when invoking `rdbgui4sasa`.
-All the sub-directories of the `test` directory are organized similarly. Let's have a look at the `test/alea-coloring/` directory. It contains the following files:
+ rdbgui4sasa -sut "sasa ring4.dot [any valid sasa option]*"
-- `my-rdbg-tuning.ml` that just includes [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml) (some `my-rdbg-tuning.ml` files define more commands, such as the one in [test/async-unison/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/async-unison/my-rdbg-tuning.ml)).
-- `ring.dot`: a possible topology
-- `p.ml`: an algorithm used in `ring.dot`
-- `Makefile`: a Makefile that daemonstrates various ways of using `sasa`. In particular, it contains a rule named `rdbg`.
+Using `rdbgui4sasa` ought to be intuitive. It first asks if you want
+to re-use a previous session, or create a fresh one.
-Try for instance:
+By default, the first in the list is executed; the first time
+`rdbgui4sasa` in invoked, no session is available and thus if you
+press `[Return]`, a fresh session is created. More precisely it
+creates a `.rdbg-session.ml` file, that loads all the necessary
+modules to run an interactive session with `rdbg`, and stores the
+command-line arguments you invoked `rdbgui4sasa` with.
-```sh
-cd test/coloring
-make rdbg
-```
+Then of course, the next time you launch `rdbgui4sasa` (with or
+without arguments), you will be prompted with the possibility to
+reuse this session.
-This make rule (defined in `Makefile` and `../Makefile.inc`)
-
-1. generates the `ring.ml` file, that contains the registration code (that can indeed be generated by sasa, as explained in `algo.mli`).
-2. launches `rdbg` with some arguments (`rdbg --sasa -o ring.rif -sut "sasa ring.dot --locally-central-daemon"`). `rdbg` then prompts the user to enter one of the following commands:
-
- Enter one of the following key (the first is the default one):
- [] create a fresh session
- [q] quit
-
-By default, the first in the list is executed; hence if you press `[Return]` without any command, a fresh session is created. More precisely it creates a `rdbg_session.ml` file, that loads all the necessary modules to run an interactive session with `rdbg`, where `rdbg` simulates ring.dot with `sasa` using a locally distributed daemon.
-
-For instance, you can type `nr[return]`, a `rdbg` command defined in [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml) that steps until the next round is reached. Then, by typing `[return]`; `rdbg` will run the lastly used command, which is `nr`, which allow you to move forward in the execution from rounds to rounds. If you want to go backwards to the previous round, you can use the `br` command=, also defined in [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml).
-
-nb: the next time `rdbg` is launched (without argument), you will be prompted with the possibility to reuse this session.
-
-```sh
-rdbg
-```
+ rdbgui4sasa
Enter one of the following key (the first is the default one):
[] #use "rdbg-session.ml" (2/11/2020: rdbg -o ring.rif -sut sasa ring.d[...])
[c] create a fresh session
[q] quit
+Another convenient way of launching `rdbgui4sasa` is by taking advantage
+of some of the generic Makefile rules available in `test/Makefile.dot` and `test/Makefile.inc`
+that are included in all the `test/*/Makefile` of the git repo:
-<a id="org7361545"></a>
-
-## The examples of test directory
-
-The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test) directory contains several files and directories that take advantage of the versatility (programmability) of `rdbg` to perform interactive `sasa` simulations:
-
-- `test/rdbg-utils/`: contains `ocaml` functions that can be used from `rdbg`
-- `test/my-rdbg-tuning.ml`: contains useful shortcuts/commands that can be used from `rdbg`.
-- `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).
+ make ring10.rdbgui
+is a convenient shortcut for
-<a id="org6e733a2"></a>
+ make ring10.dot
+ make ring10.cmxs
+ rdbgui4sasa -sut "sasa ring10.dot"
-## Running interactive sessions with `rdbg`
+For more information: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbg-sasa/>
-1. type `rdbg`
-2. press enter to load the defaut session (`rdbg-session.ml`). Then you can type:
-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)
-5. `s` to move one step forward
-6. `sd` to move one step forward and call `d` (to update the graph display [])
-7. `nr` to move one round forward
-8. `pr` to move one round backward
-9. `go` to move forward until convergence
-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`!
-
-
-<a id="org4cd47c7"></a>
-
-## Getting `rdbg` on-line help
-
-Here are 2 useful entry-points to rdbg on-line help:
-
-1. `rdbg --help` and
-2. at the `rdbg` prompt, you can use the `l` command:
-
-```sh
-(rdbg) l
-```
-
- Here is the list of rdbg Level 0 commands (i.e., defined in rdbg-cmds.ml) :
- - forward moves:
- n: Moves forward of one event
- ni i: Moves forward of i events
- s: Moves forward of one step
- si i: Moves forward of n steps
- nm <string>: Moves forward until an event which name matches a <string>
- fc pred:Moves forward until a predicate (of type unit -> bool) becomes true
- exit: Goes to the exit of the current event
-
- - backward moves:
- b: Moves backward of one event
- bi i: Moves backward of i events
- g i: Goes to event number i
- pm <string>: Moves backward until a function which name matches a <string>
-
- - Call graphs (requires GraphViz dot)
- cg: Generates the call graph from the current event
- cgf: Generates the full call graph recursively (i.e., nodes are clickable)
- dcg: Displays the generated call graph
-
- - Breakpoints:
- break <brpt>: Adds a breakpoint on a node or a file.
- A breakpoint is a string of the form:
- "node"
- "node@line"
- "file"
- "file@line"
-
- c: Continues forward until the next breakpoint
- cb: Continues backward until the previous breakpoint
- blist: Lists of the current breakpoints
- delete: Removes all breakpoints
-
- - misc:
- where: Prints the call stack with source information
- sinfo: Returns source information attached to the current event (if available)
- vv: Returns the value of a variable attached to the current event (if available)
-
- - main:
- l: Prints this list of L0 commands description
- i: A Shortcut for info
- r: Restarts to the first event
- u: Undo the last move
- q: Quits rdbg
- a: A Shortcut for apropos
- h: A Shortcut for help
-
- - sasa commands
- + Display network with GraphViz tools
- d: update the current network with dot
- ne: update the current network with neato
- tw: update the current network with twopi
- ci: update the current network with circo
- fd: update the current network with fdp
- sf: update the current network with sfdp
- pa: update the current network with patchwork
- os: update the current network with osage
-
- nb: for algorithms that have a field named 'par', you can try
- of the following (which only draw the parent arcs)
-
- d_par: update the current network with dot (parent arcs only)
- ne_par: update the current network with neato (parent arcs only)
- tw_par: update the current network with twopi (parent arcs only)
- ci_par: update the current network with circo (parent arcs only)
- fd_par: update the current network with fdp (parent arcs only)
- sf_par: update the current network with sfdp (parent arcs only)
- pa_par: update the current network with patchwork (parent arcs only)
- os_par: update the current network with osage (parent arcs only)
-
- + Moving commands [*]
- sd: go to the next step and update the network with one of the GraphViz tools
- nd: go to the next event and update the network
- bd: go to the previous event and update the network
- nr: go to the next round and update the network
- pr: go to the previous round and update the network
- [*] in order to change the current graph drawing engine, you can use
- the dot_view command as follows:
- dot_view := ci
- (rdbg)
-
-
-<a id="org6831b5f"></a>
-
-## A `rdbg` `sasa` GUI
-
-To install it:
-
-```sh
-opam depext -y rdbgui4ocaml -- useless with opam >= 2.1
-opam install -y rdbgui4ocaml
-```
-
-To use it: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/>
-
-
-<a id="org9884b00"></a>
-
-## Useful Modules
-
-Some modules, used by the sasa core engine, can be useful from `rdbg`.
-
-<iframe title="The Topology API" name="topology-api"
- width="700"
- height="500"
- src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/sasacore/Sasacore/Topology/index.html"
- alt="file:./_html/sasacore/Sasacore/Topology/index.html";>
-</iframe>
-
-<iframe title="The Diameter API" name="diameter-api"
- width="700"
- height="300"
- src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/sasacore/Sasacore/Diameter/index.html"
- alt="file:./_html/sasacore/Sasacore/Diameter/index.html";>
-</iframe>
-
-<iframe title="The Process API"
- width="700"
- height="300"
- src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/sasacore/Sasacore/Process/index.html"
- alt="file:./_html/sasacore/Sasacore/Process/index.html";>
-</iframe>
-
-<iframe title="The StringOf API"
- width="700"
- height="300"
- src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/sasacore/Sasacore/StringOf/index.html"
- alt="file:./_html/sasacore/Sasacore/StringOf/index.html";>
-</iframe>
-
-
-<a id="org160a81b"></a>
+<a id="org22e2b0f"></a>
# Install
-<a id="org21de61c"></a> <a id="org0706c07"></a>
+<a id="orged6bed8"></a>
+<a id="org98178a8"></a>
-<a id="org7ffb4e0"></a>
+<a id="org192cc6c"></a>
## Install `sasa` via opam: TL;DR
-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):
-
-```sh
-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
-opam repo add -a verimag-sync-repo \
- "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
-opam update -y
-opam install -y sasa
-
-# optionally (to perform automated tests):
-opam depext -y rdbgui4sasa lutin || echo "useless with opam >= 2.1"
-opam install -y rdbgui4sasa lutin lustre-v6
-
-# optionally (Useful during interactive simulations)
-opam install -y graphviz
-
-# optionally (for =luciole=, a gtk-based UI useful to play daemon manually):
-mkdir ~/lv4 # for example
-cd ~/lv4
-wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz
-tar xvzf lustre-v4-III-e-linux64.tgz
-echo "export LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash
-echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc
-sudo apt install -y wish
-```
-
-For running examples in the `sasa/test/` directory to check it has worked:
+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):
+
+ 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
+ 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
-```sh
-git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
-```
+For running examples in the `sasa/test/` directory of the git repo to
+check the installation has worked:
-Hopefully, everything went file. Otherwise, you can try one of methods below :
+ git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
+ cd sasa/test/
+ make test
-<a id="org868c435"></a>
+<a id="org3e48a1e"></a>
-## Install `sasa` via opam (long version)
+## Install `sasa` via `opam` (long version)
-Follows more or less the same instructions as above, but described into more details in case you want to understand the rationale for each commands, and adapt it to your distribution.
+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](http://opam.ocaml.org/doc/Install.html). [opam](http://opam.ocaml.org/doc/Install.html) works out of the box with most Linux distributions and OSX (mac). `opam` ought to work [on windows too](http://protz.github.io/ocaml-installer/).
+As using `sasa` requires to write `Ocaml` programs, you definitely
+need to install the `Ocaml` package manager [=opam](http://opam.ocaml.org/doc/Install.html)=. [`opam`](http://opam.ocaml.org/doc/Install.html) works out
+of the box with most Linux distributions and OSX (mac). `opam` ought
+to work [on windows too](http://protz.github.io/ocaml-installer/).
-```sh
-sudo apt install -y opam
-opam init -y
-eval $(opam env)
-```
+ sudo apt install -y opam
+ opam init -y
+ eval $(opam env)
-The `opam init` ougth to have populated your shell resource file with the necessary configurations commands, but it case it didn't you can run something like:
+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:
-```sh
-echo "eval $(opam env)" >> ~/.bashrc
-```
+ echo "eval $(opam env)" >> ~/.bashrc
-Once opam is installed and configured, you may want to install (or not) the last version of the compiler.
+Once `opam` is installed and configured, you may want to install (or not) the last
+version of the compiler.
-```sh
-opam switch create 4.14.1
-eval $(opam env)
-echo "eval $(opam env)" >> ~/.bashrc
-```
+ 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:
+Then, you need to add the `verimag-sync-repo` into your set of opam's
+repository:
-```sh
-opam repo add -a verimag-sync-repo \
- "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
-opam update -y
-```
+ 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`:
+Now you should be able to install `sasa`:
-```sh
-opam install -y sasa
-```
+ opam install -y sasa
-as well as the `rdbgui4sasa` Graphical User Interface:
+as well as the `rdbgui4sasa` Graphical User Interface:
-```sh
-(opam depext -y rdbgui4sasa || echo "useless since opam 2.1") && opam install -y rdbgui4sasa
-```
+ (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 framawork, you can also install the following packages:
+If you want to be able to use the automated test framework, you can also
+install the following packages:
-```sh
-opam install -y lustre-v6
-(opam depext -y lutin || echo "useless since opam 2.1") && opam install -y lutin
-```
+ 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:
-```sh
-opam update
-opam upgrade
-```
+ opam update
+ opam upgrade
-<a id="org321ff97"></a>
+<a id="orgf3e25d3"></a>
### Not strictly mandatory, but useful, third-party software
-In order to perform interactive simulations, you need to install a pdf viewer that is able to auto-refresh (for instance `zathura`):
+In order to perform interactive simulations, you need to install a
+pdf viewer that is able to auto-refresh (for instance `zathura`):
-```sh
-sudo apt install zathura
-```
+ sudo apt install zathura
-You also need an editor, for instance `emacs` with `merlin` and `tuareg`.
+You also need an editor, for instance `emacs` with `merlin` and `tuareg`.
-```sh
-sudo apt install emacs
-opam install -y merlin tuareg
-opam user-setup install -y
-```
+ sudo apt install emacs
+ opam install -y merlin tuareg
+ opam user-setup install -y
-In order to be able to use `luciole` (a small GUI useful to interactively play the role of the daemon using gtk buttons) you can also install the Lustre V4 distribution. On linux:
+In order to be able to use `luciole` (a small GUI useful to
+interactively play the role of the daemon using gtk buttons) you can
+also install the Lustre V4 distribution. On linux:
-```sh
-mkdir ~/lv4 # for example
-cd ~/lv4
-wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz
-tar xvzf lustre-v4-III-e-linux64.tgz
-echo "export LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash
-echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc
-sudo apt install -y wish
-```
+ mkdir ~/lv4 # for example
+ cd ~/lv4
+ wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz
+ tar xvzf lustre-v4-III-e-linux64.tgz
+ echo "export LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash
+ echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc
+ sudo apt install -y wish
-For more information: <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html>
+For more information:
+<http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html>
-<a id="orgf73d6fa"></a>
+<a id="orgcc3ffbf"></a>
## Install `sasa` via `git`
@@ -831,11 +662,10 @@ You will need:
For instance, on ubuntu,
-```sh
-apt install graphviz git make lablgtk3 opam
-```
+ apt install graphviz git make lablgtk3 opam
-And of course you need `ocaml`. And a set of tools installable via [opam](https://opam.ocaml.org/)
+And of course you need `ocaml`.
+And a set of tools installable via [opam](https://opam.ocaml.org/)
- `dune`
- `ocamlgraph`
@@ -844,31 +674,30 @@ And of course you need `ocaml`. And a set of tools installable via [opam](https:
Hence, once `opam` is installed, one just need to:
-```sh
-opam install --deps-only ./sasa.opam
-```
+ opam install --deps-only ./sasa.opam
And then:
-```sh
-git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
-cd sasa
-make
-make install
-make test
-```
+ 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](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).
-<a id="org398ecef"></a>
+<a id="orgb26c877"></a>
## 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.).
-<a id="org314e70c"></a>
+<a id="org5f678fe"></a>
## Use `sasa` via a Virtual Machine
@@ -878,7 +707,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve
- passwd:sasa
-<a id="orge319dc9"></a>
+<a id="org2efcd1b"></a>
# Screencasts
@@ -886,49 +715,59 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve
- Installing sasa:
- Create a xubuntu 20.4 VM: [2 minutes video (20 min of real time)](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/vbox-x2.avi)
- - Clone that VM and install sasa via opam [2:39 minutes video (37 min of real time)](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/sasa-install-x2.avi)
+ - Clone that VM and install sasa via opam [2:39 minutes video (37 min of real time)](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/sasa-install-x2.avi)
- Sasa demos (done on the VM build above, which is [available here](https://cloud.univ-grenoble-alpes.fr/index.php/s/ekAbtizPFNYPSaf):
- - demo 1: write and execute an algo (Dijkstra ring) [first-demo.avi](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/first-demo.avi)
+ - demo 1: write and execute an algo (Dijkstra ring) [first-demo.avi](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/first-demo.avi)
- demo 2: re-define what a legitimate configuration is (Dijkstra ring) [legitimate-demo.avi](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/legitimate-demo.avi)
cf <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/>
-<a id="org34a195d"></a>
+<a id="org4645def"></a>
# More
- Releases Notes: <https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/releases>
-- Sources: <https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa>
+- Sources:
+ <https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa>
- Tutorials: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt//tags/sasa/>
-<a id="orgab249a2"></a>
+<a id="org4a28da4"></a>
# FAQ
-<a id="orgf9ef9e9"></a>
+<a id="orgb7d347f"></a>
## Is there a FAQ?
Yes.
-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/>
-<a id="orge2003dc"></a>
+<a id="org7e0f941"></a>
## I have a compilation error that I don't understand
-- Look at recent `.log` files (e.g., `rdbg.log`); they sometimes contain more information than what is printed onto the screen.
+- 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>
+- 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>
-<a id="orgccdb4e5"></a>
+<a id="orga50b299"></a>
## I have the error `Invalid_argument("compare: functional value")`
-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).
\ No newline at end of file
+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).
+
diff --git a/guides/users/README.org b/guides/users/README.org
index 2c08d9f21cf88fe261d2273bc3ee63fb77ac84ca..5f08215404c4f8b69788ee8e5a557ab964969ec8 100644
--- a/guides/users/README.org
+++ b/guides/users/README.org
@@ -1,4 +1,4 @@
-# -*- eval: (org-babel-execute-buffer) -*-
+# -*- eval: (org-babel-execute-buffer) -*-
# +SETUPFILE: theme-readtheorg-local.setup
#+SETUPFILE: theme-bigblow-local.setup
#+LANGUAGE: en
@@ -7,14 +7,14 @@
#+LINK_HOME:http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox
#+HTML_HEAD:https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/
-#+HTML_HEAD: <base target="_parent">
+#+HTML_HEAD: <base target="_parent">
#+TOC: listings
-#+TOC: tables
-#+EMAIL: erwan.jahier@univ-grenoble-alpes.fr
-#+AUTHOR: Erwan Jahier
-#+TITLE: SASA: a SimulAtor of Self-stabilizing Algorithms
+#+TOC: tables
+#+EMAIL: erwan.jahier@univ-grenoble-alpes.fr
+#+AUTHOR: Erwan Jahier
+#+TITLE: SASA: a SimulAtor of Self-stabilizing Algorithms
#+LINK: sasa https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/%s
-
+#+STARTUP: nofninline
# - Pour relancer tous les blocks (et maj les sasa -h and co) : org-babel-execute-buffer
# - Pour les lancer 1 par 1 : M-x org-babel-execute-src-block (ctrl-c
@@ -22,11 +22,11 @@
# - pour recalculer le resultat des blocks sh, faire un revert-buffer
# avec "PROPERTY: header-args :cache no" et le remettre à 'yes' apres
# (pour verifier ces sorties via git) QU: Y'a t'il plus simple ?
-#
+#
#+PROPERTY: header-args :cache yes
#
-* TL;DR
+* 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 [[http://www.cs.utexas.edu/~EWD/ewd04xx/EWD426.PDF][Self-stabilizing distributed algorithms]]. This
@@ -39,7 +39,7 @@ Basically, one needs to provide:
2. the algorithms attached to nodes (via [[https://ocaml.org/][=ocaml=]] programs)
The fastest way to get started is to copy the files provided in the
-=test/skeleton= directory, and to modify them:
+=test/skeleton= directory, and to modify them:
#+BEGIN_SRC sh :results none :exports none
rm -rf test/my_algo
@@ -64,24 +64,24 @@ ocamlfind ocamlopt -bin-annot -package algo -shared state.ml p.ml config.ml ring
#sasa ring.dot -l 4
#seed 178073955
-#inputs
-#outputs "p1_v0":int "p2_v0":int "p3_v0":int "p4_v0":int "p5_v0":int "p6_v0":int "p7_v0":int "Enab_p1_action1":bool "Enab_p1_action2":bool "Enab_p2_action1":bool "Enab_p2_action2":bool "Enab_p3_action1":bool "Enab_p3_action2":bool "Enab_p4_action1":bool "Enab_p4_action2":bool "Enab_p5_action1":bool "Enab_p5_action2":bool "Enab_p6_action1":bool "Enab_p6_action2":bool "Enab_p7_action1":bool "Enab_p7_action2":bool "p1_action1":bool "p1_action2":bool "p2_action1":bool "p2_action2":bool "p3_action1":bool "p3_action2":bool "p4_action1":bool "p4_action2":bool "p5_action1":bool "p5_action2":bool "p6_action1":bool "p6_action2":bool "p7_action1":bool "p7_action2":bool "legitimate":bool
+#inputs
+#outputs "p1_v0":int "p2_v0":int "p3_v0":int "p4_v0":int "p5_v0":int "p6_v0":int "p7_v0":int "Enab_p1_action1":bool "Enab_p1_action2":bool "Enab_p2_action1":bool "Enab_p2_action2":bool "Enab_p3_action1":bool "Enab_p3_action2":bool "Enab_p4_action1":bool "Enab_p4_action2":bool "Enab_p5_action1":bool "Enab_p5_action2":bool "Enab_p6_action1":bool "Enab_p6_action2":bool "Enab_p7_action1":bool "Enab_p7_action2":bool "p1_action1":bool "p1_action2":bool "p2_action1":bool "p2_action2":bool "p3_action1":bool "p3_action2":bool "p4_action1":bool "p4_action2":bool "p5_action1":bool "p5_action2":bool "p6_action1":bool "p6_action2":bool "p7_action1":bool "p7_action2":bool "legitimate":bool
#step 0
-#outs 9 2 8 5 5 4 8 t f t f t f t f t f t f t f t f t f t f t f f f t f f f f
+#outs 9 2 8 5 5 4 8 t f t f t f t f t f t f t f t f t f t f t f f f t f f f f
#step 1
-#outs 0 0 0 0 5 0 8 t f f t f t t f f t t f f t f f f f f t t f f f f f f t f
+#outs 0 0 0 0 5 0 8 t f f t f t t f f t t f f t f f f f f t t f f f f f f t f
#step 2
-#outs 0 0 1 0 5 0 1 f f f f f t t f f t f f f t f f f f f f t f f t f f f f f
+#outs 0 0 1 0 5 0 1 f f f f f t t f f t f f f t f f f f f f t f f t f f f f f
#step 3
-#outs 0 0 1 0 1 0 1 f f f f f t f f f t f f f t f f f f f t f f f f f f f f f
+#outs 0 0 1 0 1 0 1 f f f f f t f f f t f f f t f f f f f t f f f f f f f f f
#step 4
-#outs 0 0 1 0 1 0 1 f f f f f t f f f t f f f t f f f f f f f f f f f f f t f
+#outs 0 0 1 0 1 0 1 f f f f f t f f f t f f f t f f f f f f f f f f f f f t f
#q
#+end_example
@@ -91,14 +91,13 @@ ocamlfind ocamlopt -bin-annot -package algo -shared state.ml p.ml config.ml ring
+ [[https://hal.archives-ouvertes.fr/hal-02521149][The computer journal article pre-print]]
+ [[https://cloud.univ-grenoble-alpes.fr/index.php/s/yboMr4xbcpWr6d9][Video of a SASA tutorial given at SSS'2020]]
+ [[https://cloud.univ-grenoble-alpes.fr/s/dRriW4c2bWinagw][Slides]]
-
-#+attr_html: :width 300px
-[[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/poster.pdf][file:poster.png]]
+
+#+attr_html: :://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/poster.pdf][file:poster.png]]
* Topology
<<dot>>
<<topology>>
-The topology is given via =.dot= files, that should
+The topology is given via =.dot= files, that should
1. follow the [[https://en.wikipedia.org/wiki/DOT_(graph_description_language)][graphviz/dot format]]
2. have nodes *labeled* by the =algo= field
@@ -112,22 +111,22 @@ graph ring {
p6 [algo="some_algo.ml"]
p7 [algo="some_algo.ml"]
- p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
+ p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
}
#+END_SRC
-#+RESULTS[d65ee51636ffe73dde3eee3488f35b6066c52d98]:
+#+RESULTS[167d73e80d8e75ef37d800ca0fb6e3a81a7f600c]:
[[file:ring.dot]]
-Of course the =some_algo.ml= file must exist and contains an algorithm.
+Of course the =some_algo.ml= file must exist and contains an algorithm.
nb : sasa uses ml files, and salut lustre files. Therefore the extension used
in this =algo= field is actually ignored by tools. Then sasa will
remove the extension, and add an =.ml= one, while salut will
add a =.lus= one.
-In order to define an initial configuration, one can use the =init=
-node [[http://www.graphviz.org/doc/info/attrs.html][attribute]].
+In order to define an initial configuration, one can use the =init=
+node [[http://www.graphviz.org/doc/info/attrs.html][attribute]].
#+BEGIN_SRC dot :file ring_init.dot :exports code
graph ring {
@@ -139,11 +138,11 @@ graph ring {
p6 [algo="some_algo.ml"]
p7 [algo="some_algo.ml"]
- p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
+ p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
}
#+END_SRC
-#+RESULTS[774c94dfeb9d5c7279e1a267c805461b09ca5c4f]:
+#+RESULTS[35974193fde36ed81f4cf6deda29c2ddd3b1faf7]:
[[file:ring_init.dot]]
One can use graph [[http://www.graphviz.org/doc/info/attrs.html][attributes]] to set parameters that can be used by all
@@ -160,13 +159,13 @@ graph ring {
p6 [algo="some_algo.ml"]
p7 [algo="some_algo.ml"]
- p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
+ p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
}
#+END_SRC
-#+RESULTS[de8e9d4b7950f4da5976b90639faf6a2d36631ff]:
+#+RESULTS[f9255d9ec0e17c302d6c721bcc43fd8f9029502b]:
[[file: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
@@ -174,7 +173,7 @@ 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][distributions]] to generate such
-kinds of =dot= graphs:
+kinds of =dot= graphs:
https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/
* Algorithms
@@ -196,15 +195,29 @@ The following has been generated from [[https://gricad-gitlab.univ-grenoble-alpe
#+INCLUDE: ../../test/README.org
-* Batch mode
+* Batch
#+attr_html: :width 700px
[[./sasabatch.svg]]
-** Running batch simulations
+** TL;DR
+
+In order to run an algorithm, e.g., the coloring algorithm, on a 5x5
+grid topology, do:
+
+#+begin_src sh
+cd test/coloring
+make grid5.dot # actually optional; the command below would generate it
+make grid5.cmxs
+sasa grid5.dot
+#+end_src
+
+#+RESULTS[8631f9b5ae00a59356c155f7d5a2474fade0a67a]:
+
+** Running batch simulations
Once you have defined your algorithm and your topology, you can launch
-batch simulations with the =sasa= Command Line Interface. To
+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.
@@ -233,7 +246,7 @@ dependencies into account to compile those files and generate the
name).
#+BEGIN_SRC :eval no
-ocamlfind ocamlopt -shared -package algo state.ml p.ml config.ml ring.ml -o ring.cmxs
+ocamlfind ocamlopt -shared -package algo state.ml p.ml config.ml ring.ml -o ring.cmxs
#+END_SRC
Now we are ready to launch our first batch simulation:
@@ -242,10 +255,17 @@ Now we are ready to launch our first batch simulation:
sasa ring.dot
#+END_SRC
-All the CLI commands above can be run automatically using a =make= rule
-contained in [[sasa:test/Makefile.inc][test/Makefile.inc]]. Hence, by including this file the
-=Makefile= of the current directory (cf [[sasa:test/coloring/Makefile][test/coloring/Makefile]]), one
-can generate the =ring.cmxs= file straightforwardly:
+
+But all of these commands can actually be automated with =make= and =dune=:
+
+#+begin_src sh
+make ring.cxms
+#+end_src
+
+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.
+
#+BEGIN_SRC sh :results output :exports none
cd test/coloring
@@ -258,10 +278,12 @@ can generate the =ring.cmxs= file straightforwardly:
: rm -f *.exec *.sh grid*.ml read_dot.ml rdbg-history
: rm -f ring.lut ring.ml ring_oracle.ml
+Hence, to sum-up, to simulate the coloring algorithm on 5x5 grid:
+
#+BEGIN_SRC sh :results output :exports both
cd test/coloring # from the sasa git repository
- make ring.cmxs # compile what's need to be compiled
- sasa ring.dot # launch the simulation
+ make grid5.cmxs # generate and compile all necessary files
+ sasa grid5.dot # launch a simulation
#+END_SRC
#+RESULTS[db446f776c56989d6fbc549adb887ebca8b93813]:
@@ -272,7 +294,7 @@ make: 'ring.cmxs' is up to date.
#sasa ring.dot
#seed 852602967
-#inputs
+#inputs
#outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool potential:real
@@ -290,8 +312,7 @@ This algo is silent after 4 moves, 2 steps, 2 rounds.
#quit
#+end_example
-nb: the simulation output (in the green frame) follows the [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orga43b00b][RIF]] conventions.
-
+nb: the simulation output (in the green frame) follows the [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/][RIF]] conventions.
** Running batch simulations with Built-in daemons
@@ -316,7 +337,7 @@ sasa -h | grep "\-daemon"
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.
+actions.
#+BEGIN_SRC sh :results none :exports none
cd test/unison
@@ -324,28 +345,28 @@ actions.
#+END_SRC
#+BEGIN_SRC sh :results output :exports both :var input="t t t t t t t\nq\n"
-cd test/unison
+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
+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
#+END_SRC
#+RESULTS[ef6aa8448ea78c83a132b019b9f7351d3eac2ed7]:
: sasa -reg ring.dot
: ocamlfind ocamlopt -package algo -shared state.ml unison.ml config.ml ring.ml -o ring.cmxs
-: #inputs "p1_g":bool "p2_g":bool "p3_g":bool "p4_g":bool "p5_g":bool "p6_g":bool "p7_g":bool
-: #outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_g":bool "Enab_p2_g":bool "Enab_p3_g":bool "Enab_p4_g":bool "Enab_p5_g":bool "Enab_p6_g":bool "Enab_p7_g":bool
-:
-: 2 2 5 1 3 3 4 t t t t t t t
-: 3 3 2 2 2 4 3 t f t t t t t
-: 3 3 2 2 2 4 4 t f t t t t f
+: #inputs "p1_g":bool "p2_g":bool "p3_g":bool "p4_g":bool "p5_g":bool "p6_g":bool "p7_g":bool
+: #outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_g":bool "Enab_p2_g":bool "Enab_p3_g":bool "Enab_p4_g":bool "Enab_p5_g":bool "Enab_p6_g":bool "Enab_p7_g":bool
+:
+: 2 2 5 1 3 3 4 t t t t t t t
+: 3 3 2 2 2 4 3 t f t t t t t
+: 3 3 2 2 2 4 4 t f t t t t f
In the custom daemon mode, the daemon is executed outside =sasa=, by a
-process that communicates via the standard input/output using [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orga43b00b][RIF]]
+process that communicates via the standard input/output using [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orga43b00b][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
@@ -358,29 +379,11 @@ 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=.
-
-In order to enter such input more easily, one can use (requires [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html][the lustre V4 tool box]]):
- [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orgc145c58][=luciole-rif=]]
-#+BEGIN_SRC sh :eval no
- luciole-rif sasa ring.dot --custom-daemon
-#+END_SRC
-
-Daemons can also by simulated by [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-4][=lutin=]] programs via the use of
-[[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-9][=lurette=]] (for batch executions) or [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-10][=rdbg=]] (for interactive sessions).
-
-
-# Built-in daemons can of course be programmed in Lutin. One can generate
-# such daemons using the =--gen-lutin-daemon= option: =sasa
-# --gen-lutin-daemon a_graph.dot=. It can be handy at least to get the
-# daemons variables names in the good order if one to write its own
-# daemon.
-
-
-** Running batch simulations with =lurette=
+** Running batch simulations with [[https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/][=lurette=]]
If one wants to use a test oracle to check at runtime some
-algorithms properties, one can use =lurette= as follows:
+algorithms properties, one can use [[https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/][=lurette=]] as follows:
#+BEGIN_SRC sh :results none :exports none
cd test/coloring
@@ -395,32 +398,32 @@ algorithms properties, one can use =lurette= as follows:
#+RESULTS[4d083c8e0cc2c5c887b1d58ac3bb45eb4746a144]:
-Here the oracle is specified in Lustre V6.
+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
+[[https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/][=lurette=]] can also be used to perform simulations with programmed
daemons. For instance, in order to simulate an algorithm defined in
=ring.dot= (cf [[sasa:test/coloring][test/coloring]]) using a Lutin daemon defined in
=ring.lut=, you can launch the following:
-#+BEGIN_SRC sh :eval no
+#+BEGIN_SRC sh :eval no
lurette -env "sasa ring.dot -custd" -sut "lutin ring.lut -n distributed"
#+END_SRC
-Note that for =lurette=, the role of the SUT (System Under Test) and
+Note that for [[https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/][=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.
+Hence =sasa= is used as a [[https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/][=lurette=]] environment, and the daemon
+program is used a [[https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/][=lurette=]] SUT.
For more information on this topic: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-daemons/
** Viewing Results
-=sasa -rif= and =lurette= generates =.rif= files that can be viewed
+=sasa -rif= and [[https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/][=lurette=]] generates =.rif= files that can be viewed
with =gnuplot-rif= or =sim2chro=; cf http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/
** The =sasa= CLI
@@ -429,7 +432,7 @@ with =gnuplot-rif= or =sim2chro=; cf http://www-verimag.imag.fr/DIST-TOOLS/SYNCH
#+END_SRC
#+RESULTS[093b3960c8c651b7b53e0cd7bb5d03bd433a567f]:
#+begin_example
-usage: sasa [<option>]* <topology>.dot
+usage: sasa [<option>]* <topology>.dot
use -h to see the available options.
--synchronous-daemon, -sd
@@ -449,13 +452,13 @@ use -h to see the available options.
for the next step (greedy). Performs |enabled| trials)
--greedy-daemon, -gd
Use the daemon that maximizes the potential function
- for the next step (greedy). Performs 2^|enabled| trials)
+ for the next step (greedy). Performs 2^|enabled| trials)
--seed, -seed
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
--gen-register, -reg
- Generates the registering file and exit.
+ Generates the registering file and exit.
--length, -l <int>
Maximum number of steps to be done (10000 by default).
@@ -487,17 +490,121 @@ More =sasa= options:
--gen-lustre-oracle-skeleton, -glos
Generate a Lustre oracle skeleton
--list-algos, -algo
- Output the algo files used in the dot file and exit.
+ Output the algo files used in the dot file and exit.
--dummy-input
Add a dummy input to sasa so that built-in daemon can be used from rdbg
--ignore-first-inputs, -ifi
- Ignore first inputs (necessary to use luciole via
+ Ignore first inputs (necessary to use luciole via
lurette/rdbg/luciole-rif)
--ocaml-version
Display the version ocaml version sasa was compiled with and exit.
#+end_example
-* Interactive mode
+* Interactive simulations
+
+In order to run interactive simulations, one can run =sasa= under the control of
+=rdbgui4sasa=. More specifically, instead of running
+
+#+begin_src sh
+sasa ring4.dot
+#+end_src
+
+you run
+
+#+begin_src sh
+rdbgui4sasa -sut "sasa ring4.dot"
+#+end_src
+
+
+The name =rdbgui4sasa= comes from the fact that is it GUI designed
+for =sasa=, that is built on top of [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/][=rdbg=]], but you don't need to
+know [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/][=rdbg=]] to use =rdbgui4sasa=.
+
+The =-sut= option stands for "System Under Test". This terminology
+comes from the fact that [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/][=rdbg=]] is an extension of [[https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/][=lurette=]], which
+is an automated testing tool.
+
+All the CLI options of =sasa= can be used when invoking =rdbgui4sasa=.
+
+#+begin_src sh
+rdbgui4sasa -sut "sasa ring4.dot [any valid sasa option]*"
+#+end_src
+
+
+Using =rdbgui4sasa= ought to be intuitive. It first asks if you want
+to re-use a previous session, or create a fresh one.
+
+#+BEGIN_SRC sh :results output :exports results :async :cache yes
+cd ~/sasa/test/dijkstra-ring/
+make clean > /dev/null
+make ring.cma > /dev/null
+echo "
+q
+" | make ring.rdbg | head -n +4 | tail -n 3
+#+END_SRC
+#+RESULTS[9f9ae4d607d6162fd92c4873df3429bca405a82c]:
+: Enter one of the following key (the first is the default one):
+: [] create a fresh session
+: [q] quit
+
+
+By default, the first choice in the list (=[]=) is executed if you
+just press =<Return>=. The first time =rdbgui4sasa= in invoked, no
+session is available and thus if you press =<Return>=, a fresh
+session is created -- and of course, if you press =q=, you will quit
+(more precisely it creates a =.rdbg-session.ml= file, that loads all
+the necessary modules to run an interactive session with [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/][=rdbg=]], and
+stores the command-line arguments you invoked =rdbgui4sasa= with).
+
+Then of course, the next time you launch =rdbgui4sasa= (with or
+without arguments), you will be prompted with the possibility to
+reuse this first session:
+
+#+BEGIN_SRC sh :eval no
+rdbgui4sasa
+#+END_SRC
+
+#+BEGIN_SRC sh :results output :exports results :async :cache yes
+cd test/coloring ; echo "
+q
+" | rdbg | head -n +4
+#+END_SRC
+
+#+RESULTS[72530917ef5f40c14bbb2ea3b63197577c03fd51]:
+: Enter one of the following key (the first is the default one):
+: [] #use "rdbg-session.ml" (2/11/2020: rdbg -o ring.rif -sut sasa ring.d[...])
+: [c] create a fresh session
+: [q] quit
+
+
+
+
+Another convenient way of launching =rdbgui4sasa= is by taking
+advantage of some of the generic Makefile rules available in
+=test/Makefile.dot= and =test/Makefile.inc= (that are included in all
+the =test/*/Makefile= of the git repo):
+
+
+#+begin_src sh
+make ring10.rdbgui
+#+end_src
+
+#+RESULTS[0a35b80815a91c17b0a859ae26daa53acbaf63ec]:
+
+which is a shortcut for
+#+begin_src sh
+make ring10.dot
+make ring10.cmxs
+rdbgui4sasa -sut "sasa ring10.dot"
+#+end_src
+
+
+For more information: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/
+
+
+* rdbg :noexport:
+
+
<<rdbg>> 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
@@ -512,17 +619,14 @@ cf https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbg-sasa/
Before reading this section, please read
at least the [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/README.html#outline-container-sec-3][Basic usage Section if the rdbg documentation]].
-** Example: use =rdbg= from the =test/alea-coloring/= directory
+** Example: use =rdbg= from the =test/alea-coloring/= directory
All the sub-directories of the =test= directory are organized similarly.
Let's have a look at the =test/alea-coloring/= directory.
It contains the following files:
-- =my-rdbg-tuning.ml= that just includes
- [[sasa:test/my-rdbg-tuning.ml][test/my-rdbg-tuning.ml]] (some =my-rdbg-tuning.ml= files define more
- commands, such as the one in [[sasa:test/async-unison/my-rdbg-tuning.ml][test/async-unison/my-rdbg-tuning.ml]]).
- =ring.dot=: a possible topology
- =p.ml=: an algorithm used in =ring.dot=
-- =Makefile=: a Makefile that daemonstrates various ways of using
+- =Makefile=: a Makefile that demonstrates various ways of using
=sasa=. In particular, it contains a rule named =rdbg=.
Try for instance:
@@ -533,12 +637,12 @@ make rdbg
#+RESULTS:
-This make rule (defined in =Makefile= and =../Makefile.inc=)
+This make rule (defined in =Makefile= and =../Makefile.inc=)
1. generates the =ring.ml= file, that contains the registration code
(that can indeed be generated by sasa, as explained in =algo.mli=).
2. launches =rdbg= with some arguments (=rdbg --sasa -o ring.rif -sut "sasa ring.dot --locally-central-daemon"=).
=rdbg= then prompts the user to
- enter one of the following commands:
+ enter one of the following commands:
#+BEGIN_SRC sh :results output :exports results :async :cache yes
@@ -567,9 +671,9 @@ For instance, you can type =nr[return]=, a =rdbg= command defined in
command, which is =nr=, which allow you to move forward in the
execution from rounds to rounds. If you want to go backwards to the
previous round, you can use the =br= command=, also defined in
- [[sasa:test/my-rdbg-tuning.ml][test/my-rdbg-tuning.ml]].
+ [[sasa:test/my-rdbg-tuning.ml][test/my-rdbg-tuning.ml]].
-nb: the next time =rdbg= is launched (without argument), you will
+nb: the next time =rdbg= is launched (without argument), you will
be prompted with the possibility to reuse this session.
@@ -592,7 +696,7 @@ q
** The examples of test directory
-The [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test][test]] directory contains several files and directories
+The [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test][test]] directory contains several files and directories
that take advantage of the versatility (programmability) of
=rdbg= to perform interactive =sasa= simulations:
@@ -633,7 +737,7 @@ command to yours needs by modyfying the local =my-rdbg-tuning.ml=!
** Getting =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= prompt, you can use the =l= command:
#+BEGIN_SRC sh :eval no
@@ -666,7 +770,7 @@ Here is the list of rdbg Level 0 commands (i.e., defined in rdbg-cmds
- Call graphs (requires GraphViz dot)
cg: Generates the call graph from the current event
- cgf: Generates the full call graph recursively (i.e., nodes are clickable)
+ cgf: Generates the full call graph recursively (i.e., nodes are clickable)
dcg: Displays the generated call graph
- Breakpoints:
@@ -676,11 +780,11 @@ A breakpoint is a string of the form:
"node@line"
"file"
"file@line"
-
+
c: Continues forward until the next breakpoint
cb: Continues backward until the previous breakpoint
blist: Lists of the current breakpoints
- delete: Removes all breakpoints
+ delete: Removes all breakpoints
- misc:
where: Prints the call stack with source information
@@ -689,27 +793,27 @@ A breakpoint is a string of the form:
- main:
l: Prints this list of L0 commands description
- i: A Shortcut for info
+ i: A Shortcut for info
r: Restarts to the first event
u: Undo the last move
- q: Quits rdbg
- a: A Shortcut for apropos
- h: A Shortcut for help
+ q: Quits rdbg
+ a: A Shortcut for apropos
+ h: A Shortcut for help
- sasa commands
+ Display network with GraphViz tools
d: update the current network with dot
ne: update the current network with neato
- tw: update the current network with twopi
+ tw: update the current network with twopi
ci: update the current network with circo
fd: update the current network with fdp
sf: update the current network with sfdp
pa: update the current network with patchwork
os: update the current network with osage
-
- nb: for algorithms that have a field named 'par', you can try
- of the following (which only draw the parent arcs)
-
+
+ nb: for algorithms that have a field named 'par', you can try
+ of the following (which only draw the parent arcs)
+
d_par: update the current network with dot (parent arcs only)
ne_par: update the current network with neato (parent arcs only)
tw_par: update the current network with twopi (parent arcs only)
@@ -728,7 +832,7 @@ A breakpoint is a string of the form:
[*] in order to change the current graph drawing engine, you can use
the dot_view command as follows:
dot_view := ci
-(rdbg)
+(rdbg)
#+end_example
@@ -742,6 +846,20 @@ opam install -y rdbgui4ocaml
To use it: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/
+** Another way to play the role of the daemon manually
+
+In order to play the role of the daemon via GUI buttons, another
+possibility is to use [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orgc145c58][=luciole-rif=]]:
+#+BEGIN_SRC sh :eval no
+ luciole-rif sasa ring.dot --custom-daemon
+#+END_SRC
+
+# Built-in daemons can of course be programmed in Lutin. One can generate
+# such daemons using the =--gen-lutin-daemon= option: =sasa
+# --gen-lutin-daemon a_graph.dot=. It can be handy at least to get the
+# daemons variables names in the good order if one to write its own
+# daemon.
+
** Useful Modules
Some modules, used by the sasa core engine, can be useful from =rdbg=.
@@ -783,7 +901,7 @@ Some modules, used by the sasa core engine, can be useful from =rdbg=.
<<distributions>>
<<install>>
-** Install =sasa= via opam: TL;DR
+** Install =sasa= via opam: TL;DR
On *debian-based* distributions, open a terminal and copy/paste (on
other Linux (or mac) distributions, the packages names should be more
@@ -791,69 +909,63 @@ or less the same):
#+BEGIN_SRC sh :eval no
+## Fisrt you need to install opam
sudo apt install -y opam
-opam init -y
+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
-opam repo add -a verimag-sync-repo \
- "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
-opam update -y
-opam install -y sasa
+opam user-setup install
+#+END_SRC
-# optionally (to perform automated tests):
-opam depext -y rdbgui4sasa lutin || echo "useless with opam >= 2.1"
-opam install -y rdbgui4sasa lutin lustre-v6
+Once =opam= is installed:
-# optionally (Useful during interactive simulations)
-opam install -y graphviz
+#+BEGIN_SRC sh :eval no
+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 (for =luciole=, a gtk-based UI useful to play daemon manually):
-mkdir ~/lv4 # for example
-cd ~/lv4
-wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz
-tar xvzf lustre-v4-III-e-linux64.tgz
-echo "export LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash
-echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc
-sudo apt install -y wish
+# optionally (to perform automated tests):
+opam depext -y lutin || echo "useless with opam >= 2.1"
+opam install -y lutin lustre-v6
#+END_SRC
-For running examples in the =sasa/test/= directory to check it has worked:
+For running examples in the =sasa/test/= directory of the git repo to
+check the installation has worked:
#+BEGIN_SRC sh :eval no
git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
+cd sasa/test/
+make test
#+END_SRC
-Hopefully, everything went file. Otherwise, you can try one of methods below :
-
-** Install =sasa= via opam (long version)
+** Install =sasa= via =opam= (long version)
Follows more or less the same instructions as above, but described
into more details in case you want to understand the rationale for
-each commands, and adapt it to your distribution.
+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 [[http://opam.ocaml.org/doc/Install.html][opam]]. [[http://opam.ocaml.org/doc/Install.html][opam]] works out
+need to install the =Ocaml= package manager [[http://opam.ocaml.org/doc/Install.html][=opam]]=. [[http://opam.ocaml.org/doc/Install.html][=opam=]] works out
of the box with most Linux distributions and OSX (mac). =opam= ought
to work [[http://protz.github.io/ocaml-installer/][on windows too]].
#+BEGIN_SRC sh :eval no
-sudo apt install -y opam
-opam init -y
+sudo apt install -y opam
+opam init -y
eval $(opam env)
#+END_SRC
-The =opam init= ougth to have populated your shell resource file with
+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:
#+BEGIN_SRC sh :eval no
echo "eval $(opam env)" >> ~/.bashrc
#+END_SRC
-Once opam is installed and configured, you may want to install (or not) the last
+Once =opam= is installed and configured, you may want to install (or not) the last
version of the compiler.
#+BEGIN_SRC sh :eval no
@@ -880,14 +992,14 @@ as well as the =rdbgui4sasa= Graphical User Interface:
#+BEGIN_SRC sh :eval no :tangle sh/install-opam.sh :noweb yes :tangle-mode (identity #o444)
(opam depext -y rdbgui4sasa || echo "useless since opam 2.1") && opam install -y rdbgui4sasa
-#+END_SRC
+#+END_SRC
-If you want to be able to use the automated test framawork, you can also
+If you want to be able to use the automated test framework, you can also
install the following packages:
#+BEGIN_SRC sh :eval no :tangle sh/install-opam.sh :noweb yes :tangle-mode (identity #o444)
-opam install -y lustre-v6
-(opam depext -y lutin || echo "useless since opam 2.1") && opam install -y lutin
-#+END_SRC
+opam install -y lustre-v6
+(opam depext -y lutin || echo "useless since opam 2.1") && opam install -y lutin
+#+END_SRC
Then, if one day you want to upgrade your =sasa= version:
@@ -906,7 +1018,7 @@ sudo apt install zathura
You also need an editor, for instance =emacs= with =merlin= and =tuareg=.
#+BEGIN_SRC sh :eval no
-sudo apt install emacs
+sudo apt install emacs
opam install -y merlin tuareg
opam user-setup install -y
#+END_SRC
@@ -915,38 +1027,38 @@ In order to be able to use =luciole= (a small GUI useful to
interactively play the role of the daemon using gtk buttons) you can
also install the Lustre V4 distribution. On linux:
-#+BEGIN_SRC sh
+#+BEGIN_SRC sh
mkdir ~/lv4 # for example
cd ~/lv4
wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz
tar xvzf lustre-v4-III-e-linux64.tgz
echo "export LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash
-echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc
+echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc
sudo apt install -y wish
#+END_SRC
For more information:
http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html
-** Install =sasa= via =git=
+** Install =sasa= via =git=
You will need:
- =make= (gnu)
- =git=
- =graphviz=
-- =lablgtk3=
+- =lablgtk3=
- =opam=
-For instance, on ubuntu,
+For instance, on ubuntu,
#+BEGIN_SRC sh :eval no
apt install graphviz git make lablgtk3 opam
#+END_SRC
And of course you need =ocaml=.
And a set of tools installable via [[https://opam.ocaml.org/][opam]]
- - =dune=
+ - =dune=
- =ocamlgraph=
- - =rdbg=
+ - [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/][=rdbg=]]
- =lutin= (not for compiling actually, but for using sasa with custom daemons)
Hence, once =opam= is installed, one just need to:
@@ -986,7 +1098,7 @@ http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/sasaVM.ova
- Installing sasa:
- Create a xubuntu 20.4 VM: [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/vbox-x2.avi][2 minutes video (20 min of real time)]]
- - Clone that VM and install sasa via opam [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/sasa-install-x2.avi][2:39 minutes video (37 min of real time)]]
+ - Clone that VM and install sasa via opam [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/sasa-install-x2.avi][2:39 minutes video (37 min of real time)]]
- Sasa demos (done on the VM build above, which is [[https://cloud.univ-grenoble-alpes.fr/index.php/s/ekAbtizPFNYPSaf][available here]]:
- demo 1: write and execute an algo (Dijkstra ring) [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/first-demo.avi][first-demo.avi]]
- demo 2: re-define what a legitimate configuration is (Dijkstra ring) [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/legitimate-demo.avi][legitimate-demo.avi]]
@@ -997,14 +1109,14 @@ http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/sasaVM.ova
cf http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/
-* More
+* More
- Releases Notes: https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/releases
- Sources:
https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa
- Tutorials: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt//tags/sasa/
* FAQ
-
+
** Is there a FAQ?
Yes.
@@ -1012,7 +1124,7 @@ Beside, some tutorials are also available here:
https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/
** I have a compilation error that I don't understand
-
+
- 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=
diff --git a/test/Makefile.inc b/test/Makefile.inc
index 76cc439c0651410f9d4f6a2c19c7eb8113a75594..daabacd260b30bd996e5e0162c86f2e4b6ac5b0f 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 23/01/2023 (at 14:31) by Erwan Jahier>
+# Time-stamp: <modified the 23/01/2023 (at 17:27) by Erwan Jahier>
#
# Define some default rules that ought to work most of the time
#
@@ -9,7 +9,7 @@ LIB=-package algo
ifndef DAEMON
# some rules uses this one
-DAEMON=-dd
+DAEMON=
endif
diff --git a/test/README.md b/test/README.md
index 9d9886481024bc04808b6598cb609356c6d194af..28348c58a9f00d053c505ddaa643213a6afd508e 100644
--- a/test/README.md
+++ b/test/README.md
@@ -1,28 +1,32 @@
+```sh
+git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
+cd sasa/test
+```
+
The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test) directory contains various examples of self-stabilizing distributed programs taken from the book \`\`Introduction to Distributed Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit.
1. `test/skeleton/`: a fake algorithm meant to be used as a skeleton
2. `test/dijkstra-ring/`: Dijkstra token ring
3. `test/unison/`: Synchronous unison
-4. `test/async-unison/`: Asynchronous unison
-5. `test/coloring/`: a graph coloring algorithm
-6. `test/alea-coloring/`: a randomized variant of the previous one
-7. `test/bfs-spanning-tree/`: a Breadth First Search Spanning tree construction
+4. `test/coloring/`: a graph coloring algorithm
+5. `test/alea-coloring/`: a randomized variant of the previous one
+6. `test/bfs-spanning-tree/`: a Breadth First Search Spanning tree construction
It also contains implementations of algorithms found in the literature:
-1. `test/st-CYH91`: another Spanning tree construction ("A self-stabilizing algorithm for constructing spanning trees" by Chen, Yu, and Huang in 1991)
-2. `test/bfs-st-HC92`: another BFS Spanning tree construction ("A self-stabilizing algorithm for constructing breadth-first trees" by Huang and Chen in 1992)
-3. `test/st-KK06_algo1` and `test/st-KK06_algo2`: another Spanning tree construction ("A Self-stabilizing Algorithm for Finding a Spanning Tree in a Polynomial Number of Moves" by Kosowski and Kuszner, 2006)
-4. `test/dfs/`: a Depth First Search using arrays (the \`\`atomic state model'' version of a [Depth First Search algorithm proposed by Collin and Dolev in 1994](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf))
-5. `test/dfs-list/`: the same Depth First Search, but using lists instead or arrays
+1. `test/async-unison/`: Asynchronous unison ("Asynchronous unison" by Couvreur, J., Francez, N., and Gouda, M. G. in 1992)
+2. `test/st-CYH91`: another Spanning tree construction ("A self-stabilizing algorithm for constructing spanning trees" by Chen, Yu, and Huang in 1991)
+3. `test/bfs-st-HC92`: another BFS Spanning tree construction ("A self-stabilizing algorithm for constructing breadth-first trees" by Huang and Chen in 1992)
+4. `test/st-KK06_algo1` and `test/st-KK06_algo2`: another Spanning tree construction ("A Self-stabilizing Algorithm for Finding a Spanning Tree in a Polynomial Number of Moves" by Kosowski and Kuszner, 2006)
+5. `test/dfs/`: a Depth First Search using arrays (the \`\`atomic state model'' version of a [Depth First Search algorithm proposed by Collin and Dolev in 1994](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf))
+6. `test/dfs-list/`: the same Depth First Search, but using lists instead or arrays
+7. `test/rsp-tree/`: The Algorithm 1 of "Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps" by Stéphane Devismes, David Ilcinkas, Colette Johnen.
-Each directories contains working examples, which are checked using the Continuous Integration facilities of Gitlab (cf the [.gitlab-ci.yml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml) script and the [CI pipelines](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/pipelines) results).
+Each directory contains working examples, which are checked using the Continuous Integration facilities of Gitlab (cf the [.gitlab-ci.yml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml) script and the [CI pipelines](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/pipelines) results).
-If you want to reproduce or understand what those non-regression tests do, please look at the `test/*/Makefile`, present in each directory (which all include the [test/Makefile.inc](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc) one).
+If you want to reproduce or understand what those non-regression tests do, uo can have a look at the `test/*/Makefile` files, present in each directory (which all include the [test/Makefile.inc](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc)and the [test/Makefile.dot](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.dot) ones).
-The `test` directory also contains sub-directories which gathers programs shared by all examples:
+The `test` directory also contains sub-directories which gather programs shared by all examples:
- `test/lustre/`: contains Lustre programs used as (`test/*/*.lus`) oracles
-- `test/rdbg-utils/`: contains `ocaml` functions that can be used from `rdbg`
-- `test/my-rdbg-tuning.ml`: contains useful shortcuts/commands that can be used from `rdbg`.
-- `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/rdbg-utils/`: contains `ocaml` functions that can be used from `rdbg`
\ No newline at end of file
diff --git a/test/README.org b/test/README.org
index bdb491fb21439323dc010f89b23c40903d343a85..bec896c6bf483f7800ee07b7badeb34acb8980af 100644
--- a/test/README.org
+++ b/test/README.org
@@ -39,24 +39,18 @@ literature:
Johnen.
-Each directories contains working examples, which are checked using the
-Continuous Integration facilities of Gitlab (cf the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml][.gitlab-ci.yml]]
+Each directory contains working examples, which are checked using the
+Continuous Integration facilities of Gitlab (cf the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml][.gitlab-ci.yml]]
script and the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/pipelines][CI pipelines]] results).
-If you want to reproduce or understand what those non-regression tests
-do, please look at the =test/*/Makefile=, present in each directory
-(which all include the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc][test/Makefile.inc]] one).
+If you want to reproduce or understand what those non-regression
+tests do, uo can have a look at the =test/*/Makefile= files, present
+in each directory (which all include the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.inc][test/Makefile.inc]]and the
+[[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/Makefile.dot][test/Makefile.dot]] ones).
-The =test= directory also contains sub-directories which gathers
+The =test= directory also contains sub-directories which gather
programs shared by all examples:
- =test/lustre/=: contains Lustre programs used as (=test/*/*.lus=) oracles
- =test/rdbg-utils/=: contains =ocaml= functions that can be used from
=rdbg=
-- =test/my-rdbg-tuning.ml=: contains useful shortcuts/commands that
- can be used from =rdbg=.
-- =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).
-
diff --git a/test/alea-coloring-alt/Makefile b/test/alea-coloring-alt/Makefile
index 687b288a78ee3b070f002e0c58eb0f7aed4855a0..ce1b5cf68f9ee2a8f37943f5b0461ce9724c1254 100644
--- a/test/alea-coloring-alt/Makefile
+++ b/test/alea-coloring-alt/Makefile
@@ -1,7 +1,7 @@
-# Time-stamp: <modified the 17/01/2023 (at 14:41) by Erwan Jahier>
+# Time-stamp: <modified the 25/01/2023 (at 10:51) by Erwan Jahier>
DECO_PATTERN="0-:algo_331.ml"
-DAEMON=-sd
+DAEMON=
-include ./Makefile.dot
-include ./Makefile.inc
-include Makefile.untracked
diff --git a/test/alea-coloring/Makefile b/test/alea-coloring/Makefile
index b02297597f20c09544c5f25fd0263a7c235f3c6f..8966becc01290ef514f48951b6eda6cab7c931b4 100644
--- a/test/alea-coloring/Makefile
+++ b/test/alea-coloring/Makefile
@@ -1,7 +1,7 @@
-# Time-stamp: <modified the 21/01/2023 (at 11:44) by Erwan Jahier>
+# Time-stamp: <modified the 25/01/2023 (at 10:51) by Erwan Jahier>
DECO_PATTERN="0-:p.ml"
-DAEMON=-sd
+DAEMON=
-include ./Makefile.dot
-include ./Makefile.inc
-include Makefile.untracked
diff --git a/test/alea-coloring/state.ml b/test/alea-coloring/state.ml
index 730a727f559df16ad86fc112d1c6155a8f5e308b..22781bd43988cdbcd100d48a91b855bce7b0f985 100644
--- a/test/alea-coloring/state.ml
+++ b/test/alea-coloring/state.ml
@@ -1,14 +1,8 @@
-(* Automatically generated by /home/jahier/sasa/_build/default/src/sasaMain.exe version "2.10.4-1-g9a7f112" ("9a7f112")*)
-(* on crevetete the 12/9/2019 at 10:36:45*)
-(*../../_build/install/default/bin/sasa -l 100 -reg ring.dot*)
-
-type t = int (* fixme *)
+type t = int
let to_string = string_of_int
let of_string = Some int_of_string
let copy = fun x -> x
let actions = ["conflict"]
let potential = None
let legitimate = None
-let fault = None
-
-
+let fault = None
diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
index 6f33897481ca1c1decff028720b0b22f9c8d99d3..049641cfe41c6a3992c26ea2811088fa9c25004d 100644
--- a/test/bfs-spanning-tree/Makefile
+++ b/test/bfs-spanning-tree/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 17/01/2023 (at 13:46) by Erwan Jahier>
+# Time-stamp: <modified the 23/01/2023 (at 17:35) by Erwan Jahier>
DECO_PATTERN="0:root.ml 1-:p.ml"
-include ./Makefile.dot
@@ -64,11 +64,11 @@ lurette: lurette0
sim2chrogtk -ecran -in lurette.rif > /dev/null
gnuplot-rif lurette.rif
-rdbgui: fig51_noinit.ml fig51_noinit.lut fig51_noinit_oracle.lus
+rdbgui: fig51_noinit.cma fig51_noinit.lut fig51_noinit_oracle.lus
rdbgui4sasa -sut "sasa -seed 42 fig51_noinit.dot -dd " \
-oracle-nd "lv6 fig51_noinit_oracle.lus -n oracle"
-rdbg2: fig51.ml fig51.lut
+rdbg2: fig51.cma fig51.lut
rdbg --sasa -o lurette.rif \
-env "$(sasa) fig51.dot -custd -rif" \
-sut-nd "lutin fig51.lut -n distributed"
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index e8c8b940d980a4cb4cdbdec2826efa54a891208d..7cb55704703e0ced101b3b787691990ed524cf3e 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 16/01/2023 (at 10:43) by Erwan Jahier>
+# Time-stamp: <modified the 21/01/2023 (at 11:41) by Erwan Jahier>
sasa=$(DIR)/bin/sasa -l 100
@@ -40,44 +40,6 @@ rdbg-lurette: ring.cmxs ring_oracle.lus
-sut "sasa ring.dot -rif -lcd " \
-oracle "lv6 ring_oracle.lus -n oracle -exec"
+
test100:
for i in $$(seq 100); do make lurette && make clean; done
-
-rdbg: grid4.ml
- echo "" > include.ml
- ledit rdbg --sasa -sut "sasa grid4.dot --locally-central-daemon"
-rdbgui: grid4.ml
- echo "" > include.ml
- rdbgui4sasa -sut "sasa grid4.dot --locally-central-daemon"
-
-rdbgui-demo: grid10.ml
- echo "" > include.ml
- rdbgui4sasa -sut "sasa grid10.dot --central-daemon"
-
-rdbg-luciole: grid4.ml
- echo "" > include.ml
- rdbg --sasa --luciole -sut "sasa -rif grid4.dot --custom-daemon"
-
-rdbgui-custd: grid4.ml
- echo "" > include.ml
- rdbgui4sasa -sut "sasa -rif grid4.dot --custom-daemon"
-
-
-rdbg3: ring.ml
- echo "" > include.ml
- ledit rdbg --sasa -sut "sasa ring.dot -wd"
-
-rdbg1: ring.ml ring_oracle.lus
- echo "" > include.ml
- ledit rdbg --sasa -o rdbg-ring.rif \
- -sut "sasa --replay ring.dot -rif -lcd " \
- -oracle "lv6 ring_oracle.lus -n oracle -exec"
-
-rdbg2: ring.cmxs ring.lut
- echo "" > include.ml
- ledit rdbg --sasa -o ring.rif \
- -env "$(sasa) --replay ring.dot -custd -rif" \
- -sut-nd "lutin ring.lut -n distributed"
-
-rdbg4: ring.ml
- ledit rdbg --sasa -o ring.rif -env "sasa ring.dot -custd "