diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d469da5dd9c163c879d7e7174772a9510a8d2e74..b8d799fc4eb5ba8d1559ad4e12fa956753256d45 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -32,10 +32,12 @@ pages:
image: jahierwan/verimag-sync-tools
stage: deploy
script:
+ - make odoc
- mkdir public
- cd guides/users
- make
- cp README.html ../../public/index.html
+ - cp -rf _html ../../public/
- cp -rf ../styles/ ../../public/
artifacts:
paths:
diff --git a/Makefile b/Makefile
index 8dd44d9a40c73e67e29ce1f966a37b5288dd2d21..2b517a3750ed4dafa12c26e2afaea7b960cf6b4c 100644
--- a/Makefile
+++ b/Makefile
@@ -19,6 +19,9 @@ test:
test-doc:
cd guides/users; make
+odoc:
+ dune build @doc
+
clean:
rm -f *.cmxs sasa *.cmi *.o *.cmx *.pdf
rm -f lib/sasacore/sasaVersion.ml
diff --git a/README.md b/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..e0536e7d239162c61b5421959b68531c8d8a4ced
--- /dev/null
+++ b/README.md
@@ -0,0 +1 @@
+The user guide can be browsed at <https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/>
diff --git a/guides/users/Makefile b/guides/users/Makefile
index e509a160605fde04812b9cd7eb536d0a8520a875..e1947d6184a70d5a9c8ee85691598690d6b62b45 100644
--- a/guides/users/Makefile
+++ b/guides/users/Makefile
@@ -1,5 +1,9 @@
-all:README.html
+all:README.html algo
+
+algo:
+ cd ../../ ; make odoc
+ cp -rf ../../_build/default/_doc/_html .
%.html:%.org
emacs --batch --eval="(add-to-list 'load-path \".\") (add-to-list 'load-path \"./el\")" --eval="(require 'htmlize)" --load=emacs-org.el \
diff --git a/guides/users/README.md b/guides/users/README.md
index 8c2e463327c50c6ff3ae536ad9a289b9067f9697..13bbcefe0907af1ef9397ff544235f62b1074ce0 100644
--- a/guides/users/README.md
+++ b/guides/users/README.md
@@ -1,47 +1,50 @@
# Table of Contents
-1. [TL;DR](#org65d956b)
-2. [Topology](#org777d1ad)
-3. [Algorithms](#org123754b)
-4. [Batch Simulations](#org39d18fd)
- 1. [Running batch simulations with Built-in demons](#orga9e7aba)
- 2. [Running batch simulations with manual demons](#org23a5a25)
- 3. [Running batch simulations with `lurette`](#org12df094)
- 4. [The `sasa` CLI](#org56e87fb)
-5. [Interactive Simulation](#orge4fae0a)
- 1. [Running interactive sessions with `rdbg`](#orgf435d3b)
- 2. [Running batch sessions with `lurette`](#org14962dd)
-6. [Viewing Results](#org65a372b)
-7. [Install](#org93355d3)
- 1. [From source](#org263e905)
- 2. [Via opam (not yet working)](#orgdc7c1f0)
-8. [More](#org86e91bf)
-9. [FAQ](#org5aff55f)
- 1. [Is there a FAQ?](#org0f34393)
-
-
-<a id="org65d956b"></a>
+1. [TL;DR](#org894d8ce)
+2. [Topology](#org4cc393b)
+3. [Algorithms](#orga7945a0)
+4. [Examples](#orgbbf247a)
+5. [Batch mode](#orgf683e52)
+ 1. [Running batch simulations with Built-in demons](#orgc61d0c6)
+ 2. [Running batch simulations with manual demons](#orgbb32fc7)
+ 3. [Running batch simulations with `lurette`](#org0e74651)
+ 4. [Viewing Results](#org81f11cd)
+ 5. [The `sasa` CLI](#org0383e07)
+6. [Interactive mode](#org02765ee)
+ 1. [Running interactive sessions with `rdbg`](#orgefe2347)
+7. [Install](#org52a413e)
+ 1. [Via opam (prefered method)](#orgb7b3818)
+ 2. [From source](#orgf464ad7)
+8. [More](#org9d27083)
+9. [FAQ](#orgebde806)
+ 1. [Is there a FAQ?](#org3dc6690)
+
+
+<a id="org894d8ce"></a>
# TL;DR
-SASA is a **Self-stabilizing Algorithms SimulAtor**, based on the so-called **state model** 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)
+SASA is a **Self-stabilizing Algorithms SimulAtor**, based on the so-called **atomic state model** 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)
Basically, one needs to provide:
-1. a topology, made of nodes and channels (via a dot file)
+1. a topology, made of nodes and transitions (via a dot file)
2. the algorithms attached to nodes (via `ocaml` programs)
-Now, suppose you have a topology defined in `ring.dot`, that refers to an algorithm defined in the ocaml program `p.ml` (cf `test/skeleton/` directory), you can simulate it as follows:
+The fastest way to get started is to copy the files provides in the `test/skeleton` directory, and to modify them:
```sh
-ocamlfind ocamlopt -shared -package sasacore p.ml -o p.cmxs
-sasa g.dot
+cd test
+cp -rf skeleton my_algo
+cd my_algo
+make ring.cmxs
+sasa ring.dot
```
The source code is available at <https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa>
-<a id="org777d1ad"></a>
+<a id="org4cc393b"></a>
# Topology
@@ -66,197 +69,90 @@ graph ring {
Of course the `some_algo.ml` file must exist.
+In order to define initial state values to nodes, one can use `init` node [attribute](http://www.graphviz.org/doc/info/attrs.html).
-<a id="org123754b"></a>
-
-# Algorithms
+```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=1"]
+ p6 [algo="some_algo.ml=1"]
+ p7 [algo="some_algo.ml=1"]
-Those algorithms, implemented in `ocaml`, must provide:
-
-1. a set of variables (registers)
-2. an `enable` fonction that says which actions are enabled (i.e., that can be activated)
-3. a `step` function that executes enabled actions
-
-More precisely, each algorithm should provide 3 functions that must be registred using the string used in dot file algo fields with:
-
-- `reg_vars`
-- `reg_enable`
-- `reg_step`
-
-which profiles is defined in [algo.mli](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli)
-
-```code
-(* Time-stamp: <modified the 25/09/2019 (at 16:03) by Erwan Jahier> *)
-(** The Algorithm programming Interface.
-
- A SASA process is an instance of an algorithm defined via this
- module.
-
- In order to define a SASA algorithm, one need to provide an enable
- and a step function:
- - the enable function states which actions can be triggered;
- - the step function triggers an enable action.
-
- The enable and the step functions should be of the following type:
- *)
-type 's neighbor
-type action = string
-type 's enable_fun = 's -> 's neighbor list -> action list
-type 's step_fun = 's -> 's neighbor list -> action -> 's
-(** The first argument holds the current state of the process. As it is
- polymorphic (='s=), algorithms designers can put anything they need
- into this state (an integer, a structure, etc.). The only constraint
- is that all algorithms should use the same type.
-
- The second argument holds the process neighbors. Note that SASA
- processes, that live in graph nodes, can only access to their
- immediate neighbors. From each neighbor, a process can access to
- various information thanks to the functions below.
-*)
-
-(** When a neighbor information can not be accessed (e.g., the pid
- anonymous networks) the Not_available exception is raised. *)
-exception Not_available
-
-(** Returns the processes local state *)
-val state : 's neighbor -> 's
-
-(** Returns the process id of the current process neighbor. This info
- is not available in all simulation modes. *)
-val pid : 's neighbor -> string
-
-(* Returns the process id of the current process
-
- “To see ourselves as others see us is a most salutary gift. Hardly
- less important is the capacity to see others as they see
- themselves.†― Aldous Huxley, The Doors of Perception.
- *)
-val spid : 's neighbor -> string
-
-(** Returns the channel number that let this neighbor access to the
- content of the process, if it neighbor can access it. Returns -1 if
- the neigbor can not access to the process, which may happen in
- directed graphs only. This info is not available in all simulation
- modes.
- *)
-val reply : 's neighbor -> int
-
-(** Returns the weight decoration the current node and it neighbor
- (which makes sense in directed graphs only) *)
-val weight : 's neighbor -> int
-
-
-(** When writing algorithms, one can also have acces to topological information
- (i.e., information that are relative to the graph) *)
-val card : unit -> int
-val min_degree : unit -> int
-val mean_degree : unit -> float
-val max_degree : unit -> int
-val is_cyclic : unit -> bool
-val is_connected : unit -> bool
-val is_tree : unit -> bool
-val height : unit -> (string (* the node id *) -> int) option
-val links_number : unit -> int
-val diameter : unit -> int
-
-(** It is possible to set some global parameters in the dot file
- using graph attributes. This function allows one the get their
- values. *)
-val get_graph_attribute : string -> string
-
-
-(** Once enable and step functions are defined, they need to be
- registred by calling the register function below.
-
- An alternative to writing this registration code is to let sasa
- generate it with the "--gen-register" (or "-reg") option.
- In this case, one needs to follow some naming conventions (w.r.t file
- and function names):
-
- (1) The internal state (i.e. the 's shared by all algos) should be
- defined in a file named "state.ml" that defines the following 4 entities:
- type t = define_me
- let (to_string: t -> string) = fun _ -> "define_me"
- let (of_string: string -> t option) = fun _ -> None
- let (copy : t -> t) = fun x -> x
-
- If one does not want/need to provide the of_string state parser, returning
- None is fine. This is mandatory only if one wants to define initial values
- in the dot file.
-
- Defining a copy that is not the identity is necessary if the state is not
- functionnal (e.g., if it contains an array or an Hashtbl).
-
- In the file "state.ml" does not exist in the current directory, a skeleton
- is generated.
-
- (2) All the algos mentionned in the dot file should define the
- following functions:
- let (init_state: int -> State.t) = xxx
- let (enable_f: State.t neighbor list -> State.t -> action list) = xxx
- let (step_f : State.t neighbor list -> State.t -> action -> State.t ) = xxx
- let actions = Some ["action1";"action2"];
-*)
-type algo_id = string
-type 's algo_to_register = {
- algo_id : string;
- init_state: int (* holds the process neigbors number *) -> 's;
- enab : 's enable_fun;
- step : 's step_fun;
- actions : action list option (** Mandatory in custom demon mode *)
-}
-type 's to_register = {
- algo : 's algo_to_register list;
- state_to_string: 's -> string; (* [1] *)
- state_of_string: (string -> 's) option; (* To be able to parse state init in the dot *)
- copy_state: 's -> 's;
+ p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
}
-(* [1] for state_to_string, the idea here is to print the raw values
- contained in 's.
-
- If a value is omitted, one won't see it in the simulation outputs.
-
- If one prepend a value with "some_id=", some_id will we used in
- the simulation outputs. Otherwise, an id will be invented *)
-
-
-(** To be called once *)
-val register : 's to_register -> unit
```
-Optionnaly, one can register a function that provides initial values to local variables (`reg_init`). If not such registration is done, local variables will be set according to `init` annotations in the dot file. If no such annotations exists, initial values will be chosen at random.
+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 {
- p1 [algo="some_algo.ml" init="v=1" init="x=3"]
- p2 [algo="some_algo.ml"]
- p3 [algo="some_algo.ml"]
+ 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"]
+ p5 [algo="some_algo.ml=1"]
+ p6 [algo="some_algo.ml=1"]
+ p7 [algo="some_algo.ml=1"]
p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
}
```
-Algorithms must then be compiled with `ocamlopt -shared` to produce the `.cmxs` files corresponding to the `.ml` mentionned in the dot file algo fields.
+Such parameters can be retreived in Algorithms using the `Algo.get_graph_attribute : string -> string` function.
+
+nb: a `Algo.diameter: unit -> int` function is provided, but it can be expensive to use.
-```sh
-ocamlopt -shared -I +sasa some_algo.ml -o some_algo.cmxs
-```
-Actions names (`string`) must be registered if one wants to use `sasa` with custom demons (cf below).
+<a id="orga7945a0"></a>
+
+# Algorithms
-Some examples can be found in the [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test) directory.
+The following has been generated from [algo.mli](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli)
+<div class="html">
+<iframe title="The Algo API" width="700" height="700" src="<_html/algo/Algo/index.html>";></iframe>
-<a id="org39d18fd"></a>
+</div>
-# Batch Simulations
+<a id="orgbbf247a"></a>
-<a id="orga9e7aba"></a>
+# Examples
+
+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.
+
+- `test/skeleton/`: a fake algorithm meant to be used as a skeleton
+- `test/dijkstra-ring/`: Dijkstra token ring
+- `test/unison/`: Synchronous unison
+- `test/async-unison/`: Asynchronous unison
+- `test/coloring/`: a graph coloring algorithm
+- `test/alea-coloring/`: a randomized variant of the previous one
+- `test/bfs-spanning-tree/`: a Breadth First Search spanning tree construction
+- `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))
+- `test/dfs-list/`: a Depth First Search using lists
+
+Each directories contains working exemples, 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` (it it exists).
+
+
+<a id="orgf683e52"></a>
+
+# Batch mode
+
+
+<a id="orgc61d0c6"></a>
## Running batch simulations with Built-in demons
@@ -281,7 +177,7 @@ sasa -h | grep "\-demon"
--custom-demon, -custd
-<a id="org23a5a25"></a>
+<a id="orgbb32fc7"></a>
## Running batch simulations with manual demons
@@ -289,11 +185,10 @@ By using the `--custom-demon` option (or `-custd` for short), you can play the r
```sh
cd ../../test/unison
+make ring.cmxs
sasa ring.dot --custom-demon
```
-At each step, xxx
-
In the custom demon mode, the demon 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-sec-5) 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 demon can thus be played by users that read and enter Boolean values.
@@ -308,10 +203,8 @@ It can also by simulated by [`lutin`](http://www-verimag.imag.fr/DIST-TOOLS/SYNC
Built-in demons can of course be programmed in Lutin. One can generate such demons using the `--gen-lutin-demon` option: `sasa --gen-lutin-demon a_graph.dot`. It can be handy at least to get the demons variables names in the good order if one to write its own demon.
-Moreover, for using the custom mode, it is mandatory to register actions (via `Algo.reg_actions`).
-
-<a id="org12df094"></a>
+<a id="org0e74651"></a>
## Running batch simulations with `lurette`
@@ -321,11 +214,27 @@ If you want to perform simulations with custom demons, you need to use `lurette`
lurette \
-env "sasa ring.dot -custd" \
-sut "lutin ring.lut -n distributed"
+```
+
+For `lurette`, the role of the SUT 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.
+If one wants to use an internal sasa daemon, no environment is needed and sasa can be used with `-sut`. In order to use an oracle defined in Lustre, one can use `lurette` as follows:
+
+```sh
+lurette \
+ -sut "sasa ring.dot" \
+ -oracle "lv6 ring_oracle.lus -n oracle -exec"
```
-<a id="org56e87fb"></a>
+<a id="org81f11cd"></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/lustre-v6/>
+
+
+<a id="org0383e07"></a>
## The `sasa` CLI
@@ -347,9 +256,13 @@ sasa --help
Use a Distributed demon (which select at least one action). This is the default demon.
--custom-demon, -custd
Use a Custom demon (forces --rif)
- --rif, -rif Follows RIF conventions
+ --rif, -rif Display only outputs on stdout (i.e., behave as a rif input file)
+ --no-log, -rif
+ Display only outputs on stdout (i.e., behave as a rif input file)
--seed, -seed
- Set the pseudo-random generator seed of build-in demons
+ Set the pseudo-random generator seed of build-in demons (wins over --replay)
+ --replay, -replay
+ Use the last generated seed to replay the last run
--gen-register, -reg
Generates the registering file and exit.
@@ -387,20 +300,20 @@ sasa --more
Display the version ocaml version sasa was compiled with and exit.
-<a id="orge4fae0a"></a>
+<a id="org02765ee"></a>
-# Interactive Simulation
+# Interactive mode
-If you want to perform interaction
+If you want to perform interactive session, you can launch `sasa` under the control of `rdbg`.
-Lutin, `lurette`, and `rdbg`
+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:
-cf `Makefile` in the [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test) directory.
+- `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).
-In each sub-directory of [../../test/](../../test/), there is a `rdbg-session.ml` file that takes care of the red-tape for using `rdbg` with the corresponding examples.
-
-<a id="orgf435d3b"></a>
+<a id="orgefe2347"></a>
## Running interactive sessions with `rdbg`
@@ -465,43 +378,14 @@ rdbg
Typing '0' will therefore also load the `rdbg_session.ml` file we have just been using.
-<a id="org14962dd"></a>
-
-## Running batch sessions with `lurette`
-
-XXX TODO
-
-
-<a id="org65a372b"></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/lustre-v6/>
-
-
-<a id="org93355d3"></a>
+<a id="org52a413e"></a>
# Install
-<a id="org263e905"></a>
+<a id="orgb7b3818"></a>
-## From source
-
-You will need:
-
-- `make` (gnu)
-- a set of tools installable via [opam](https://opam.ocaml.org/)
- - `dune`
- - `ocamlgraph`
- - `lutin` (not for compiling actually, but for using sasa with custom demons)
-
-One can mimick the content of the `test` job in the project [Gitlab CI script](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/.gitlab-ci.yml).
-
-
-<a id="orgdc7c1f0"></a>
-
-## Via opam (not yet working)
+## Via opam (prefered method)
```sh
opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
@@ -524,7 +408,23 @@ opam install -y rdbg lutin
```
-<a id="org86e91bf"></a>
+<a id="orgf464ad7"></a>
+
+## From source
+
+You will need:
+
+- `make` (gnu)
+- a set of tools installable via [opam](https://opam.ocaml.org/)
+ - `dune`
+ - `ocamlgraph`
+ - `rdbg`
+ - `lutin` (not for compiling actually, but for using sasa with custom demons)
+
+One can mimick the content of the `test` job in the project [Gitlab CI script](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/.gitlab-ci.yml).
+
+
+<a id="org9d27083"></a>
# More
@@ -532,12 +432,12 @@ opam install -y rdbg lutin
- Sources: <https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa>
-<a id="org5aff55f"></a>
+<a id="orgebde806"></a>
# FAQ
-<a id="org0f34393"></a>
+<a id="org3dc6690"></a>
## Is there a FAQ?
diff --git a/guides/users/README.org b/guides/users/README.org
index 06331064cf7445c0b1a1d7d0c43dbfe11669c9e3..56f444d6558a5326a2314048eea47065f8e97eb8 100644
--- a/guides/users/README.org
+++ b/guides/users/README.org
@@ -10,26 +10,28 @@
#+TOC: tables
#+EMAIL: erwan.jahier@univ-grenoble-alpes.fr
#+AUTHOR: Erwan Jahier
-#+TITLE: Self-stabilizing Algorithms SimulAtor: SASA
+#+TITLE: SASA: a SimulAtor of Self-stabilizing Algorithms
* TL;DR
SASA is a *Self-stabilizing Algorithms SimulAtor*, based on the
-so-called *state model* introduced by _Dijkstra_ in its seminal article
+so-called *atomic state model* introduced by _Dijkstra_ in its seminal article
on [[http://www.cs.utexas.edu/~EWD/ewd04xx/EWD426.PDF][Self-stabilizing distributed algorithms]]
Basically, one needs to provide:
-1. a topology, made of nodes and channels (via a dot file)
+1. a topology, made of nodes and transitions (via a dot file)
2. the algorithms attached to nodes (via =ocaml= programs)
-Now, suppose you have a topology defined in =ring.dot=, that refers to
-an algorithm defined in the ocaml program =p.ml= (cf =test/skeleton/=
-directory), you can simulate it as follows:
+The fastest way to get started is to copy the files provides in the
+=test/skeleton= directory, and to modify them:
#+BEGIN_SRC sh
-ocamlfind ocamlopt -shared -package sasacore p.ml -o p.cmxs
-sasa g.dot
+cd test
+cp -rf skeleton my_algo
+cd my_algo
+make ring.cmxs
+sasa ring.dot
#+END_SRC
The source code is available at
@@ -57,58 +59,65 @@ graph ring {
Of course the =some_algo.ml= file must exist.
-* Algorithms
-
-Those algorithms, implemented in =ocaml=, must provide:
-1. a set of variables (registers)
-2. an =enable= fonction that says which actions are enabled (i.e., that can be activated)
-3. a =step= function that executes enabled actions
+In order to define initial state values to nodes, one can use =init=
+node [[http://www.graphviz.org/doc/info/attrs.html][attribute]].
-More precisely, each algorithm should provide 3 functions that must be
-registred using the string used in dot file algo fields with:
-- =reg_vars=
-- =reg_enable=
-- =reg_step=
-
-which profiles is defined in [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli][algo.mli]]
+#+BEGIN_SRC dot :file ring_init.ml :exports code
+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=1"]
+ p6 [algo="some_algo.ml=1"]
+ p7 [algo="some_algo.ml=1"]
-#+INCLUDE: "../../lib/algo/algo.mli" src ocaml :export code
+ p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
+}
+#+END_SRC
-Optionnaly, one can register a function that provides initial values
-to local variables (=reg_init=). If not such registration is done,
-local variables will be set according to =init= annotations in the dot
-file. If no such annotations exists, initial values will be chosen at
-random.
+One can use graph [[http://www.graphviz.org/doc/info/attrs.html][attributes]] to set parameters that can be used by all
+nodes during the simulation.
-#+BEGIN_SRC dot :file ring-init.ml
+#+BEGIN_SRC dot :file ring_init.ml :exports code
graph ring {
- p1 [algo="some_algo.ml" init="v=1" init="x=3"]
- p2 [algo="some_algo.ml"]
- p3 [algo="some_algo.ml"]
+ 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"]
+ p5 [algo="some_algo.ml=1"]
+ p6 [algo="some_algo.ml=1"]
+ p7 [algo="some_algo.ml=1"]
p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1
}
#+END_SRC
-Algorithms must then be compiled with =ocamlopt -shared= to produce
-the =.cmxs= files corresponding to the =.ml= mentionned in the dot
-file algo fields.
-#+BEGIN_SRC sh
-ocamlopt -shared -I +sasa some_algo.ml -o some_algo.cmxs
-#+END_SRC
+Such parameters can be retreived in Algorithms using the
+=Algo.get_graph_attribute : string -> string= function.
-Actions names (=string=) must be registered if one wants to use =sasa=
-with custom demons (cf below).
+nb: a =Algo.diameter: unit -> int= function is provided, but it can
+be expensive to use.
-Some examples can be found in the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test][test]] directory.
-
-* Batch Simulations
+* Algorithms
+
+The following has been generated from [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli][algo.mli]]
+
+#+begin_html
+<iframe title="The Algo API"
+ width="700"
+ height="700"
+ src="file:_html/algo/Algo/index.html";></iframe>
+#+end_html
+
+* Examples
+#+INCLUDE: ../../test/README.org
+
+* Batch mode
+
** Running batch simulations with Built-in demons
@@ -145,12 +154,11 @@ actions.
#+BEGIN_SRC sh :results output :exports both :var input="t t t t t t t"
cd ../../test/unison
+make ring.cmxs
sasa ring.dot --custom-demon
#+END_SRC
#+RESULTS:
-At each step, xxx
-
In the custom demon mode, the demon is executed outside =sasa=, by a
@@ -182,9 +190,6 @@ such demons using the =--gen-lutin-demon= option: =sasa
demons variables names in the good order if one to write its own
demon.
-Moreover, for using the custom mode, it is mandatory to register
-actions (via =Algo.reg_actions=).
-
** Running batch simulations with =lurette=
@@ -197,11 +202,29 @@ in =ring.lut=, you can launch the following command:
lurette \
-env "sasa ring.dot -custd" \
-sut "lutin ring.lut -n distributed"
-
#+END_SRC
+For =lurette=, the role of the SUT 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.
+
+If one wants to use an internal sasa daemon, no environment is needed
+and sasa can be used with =-sut=. In order to use an oracle defined in
+Lustre, one can use =lurette= as follows:
+
+#+BEGIN_SRC sh
+ lurette \
+ -sut "sasa ring.dot" \
+ -oracle "lv6 ring_oracle.lus -n oracle -exec"
+#+END_SRC
+** 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/lustre-v6/
** The =sasa= CLI
#+BEGIN_SRC sh :results output :exports both
@@ -257,18 +280,25 @@ More =sasa= options:
Display the version ocaml version sasa was compiled with and exit.
#+end_example
-* Interactive Simulation
+* Interactive mode
-If you want to perform interaction
+If you want to perform interactive session, you can launch =sasa=
+under the control of =rdbg=.
-Lutin, =lurette=, and =rdbg=
-cf =Makefile= in the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test][test]] directory.
+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:
-In each sub-directory of [[file:../../test/][../../test/]], there is a =rdbg-session.ml=
-file that takes care of the red-tape for using =rdbg= with the
-corresponding examples.
+- =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).
** Running interactive sessions with =rdbg=
@@ -359,31 +389,9 @@ Typing '0' will therefore also load the =rdbg_session.ml= file we have
just been using.
-
-
-** Running batch sessions with =lurette=
-
-XXX TODO
-
-* 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/lustre-v6/
-
* Install
-** From source
-You will need:
-- =make= (gnu)
-- a set of tools installable via [[https://opam.ocaml.org/][opam]]
- - =dune=
- - =ocamlgraph=
- - =lutin= (not for compiling actually, but for using sasa with custom demons)
-
-One can mimick the content of the =test= job in the project [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/.gitlab-ci.yml][Gitlab CI
-script]].
-
-** Via opam (not yet working)
+** Via opam (prefered method)
#+BEGIN_SRC sh :tangle sh/install-opam.sh :noweb yes :tangle-mode (identity #o444)
opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
@@ -407,6 +415,19 @@ opam depext -y rdbg lutin
opam install -y rdbg lutin
#+END_SRC
+** From source
+
+You will need:
+- =make= (gnu)
+- a set of tools installable via [[https://opam.ocaml.org/][opam]]
+ - =dune=
+ - =ocamlgraph=
+ - =rdbg=
+ - =lutin= (not for compiling actually, but for using sasa with custom demons)
+
+One can mimick the content of the =test= job in the project [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/.gitlab-ci.yml][Gitlab CI
+script]].
+
* More
- Releases Notes: https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/releases
diff --git a/lib/algo/algo.mli b/lib/algo/algo.mli
index c1b8053fe6facd98bac653e139eaf8de4b9ac5de..6a84e49923216315702c4deed23c7865076222c4 100644
--- a/lib/algo/algo.mli
+++ b/lib/algo/algo.mli
@@ -1,6 +1,7 @@
-(* Time-stamp: <modified the 17/10/2019 (at 21:08) by Erwan Jahier> *)
-(** The Algorithm programming Interface.
-
+(* Time-stamp: <modified the 22/10/2019 (at 23:58) by Erwan Jahier> *)
+(** {1 The Algorithm programming Interface.} *)
+(**
+ {1 What's need to be provided by users.}
A SASA process is an instance of an algorithm defined via this
module.
@@ -9,14 +10,16 @@
- the enable function states which actions can be triggered;
- the step function triggers an enable action.
- The enable and the step functions should be of the following type:
- *)
+ The enable and the step functions should be of the type
+ [ 's enable_fun ] and [ 's step_fun ] respectively.
+ *)
+
type 's neighbor
type action = string
type 's enable_fun = 's -> 's neighbor list -> action list
type 's step_fun = 's -> 's neighbor list -> action -> 's
(** The first argument holds the current state of the process. As it is
- polymorphic (='s=), algorithms designers can put anything they need
+ polymorphic (['s]), algorithms designers can put anything they need
into this state (an integer, a structure, etc.). The only constraint
is that all algorithms should use the same type.
@@ -37,7 +40,7 @@ val state : 's neighbor -> 's
is not available in all simulation modes. *)
val pid : 's neighbor -> string
-(* Returns the process id of the current process
+(** Returns the process id of the current process
“To see ourselves as others see us is a most salutary gift. Hardly
less important is the capacity to see others as they see
@@ -58,8 +61,11 @@ val reply : 's neighbor -> int
val weight : 's neighbor -> int
-(** When writing algorithms, one can also have acces to topological information
- (i.e., information that are relative to the graph) *)
+(** {1 Access to Topological Information}
+
+ When writing algorithms, one can also have acces to topological
+ information (i.e., information that are relative to the graph) *)
+
val card : unit -> int
val min_degree : unit -> int
val mean_degree : unit -> float
@@ -78,8 +84,43 @@ val diameter : unit -> int
val get_graph_attribute : string -> string
-(** Once enable and step functions are defined, they need to be
- registred by calling the register function below.
+(** {1 Code Registration}
+
+The [register: 's to_register -> unit] function must be called once in
+ the user code. *)
+
+type 's algo_to_register = {
+ algo_id : string;
+ init_state: int -> 's; (** The int holds the process neigbors number *)
+ enab : 's enable_fun;
+ step : 's step_fun;
+ actions : action list option (** Mandatory in custom demon mode *)
+}
+type 's to_register = {
+ algo : 's algo_to_register list;
+ state_to_string: 's -> string;
+ state_of_string: (string -> 's) option;
+ copy_state: 's -> 's;
+ }
+(** - For the [state_to_string] field, the idea is to print the raw
+ values contained in ['s]. If a value is omitted, one won't see it
+ in the simulation outputs. If one prepend a value with "some_id",
+ some_id will we used in the simulation outputs. Otherwise, an id
+ will be invented by sasa.
+
+ - For the [state_of_string] field, if some function is provided,
+ sasa should be able to parse state init values in the dot.
+
+*)
+
+
+(** To be called once *)
+val register : 's to_register -> unit
+
+(** {1 Automatic Generation of Registration Code}
+
+ Once enable and step functions are defined, they need to be
+ registred by calling the register function.
An alternative to writing this registration code is to let sasa
generate it with the "--gen-register" (or "-reg") option.
@@ -88,10 +129,12 @@ val get_graph_attribute : string -> string
(1) The internal state (i.e. the 's shared by all algos) should be
defined in a file named "state.ml" that defines the following 4 entities:
+ {[
type t = define_me
let (to_string: t -> string) = fun _ -> "define_me"
let (of_string: string -> t option) = fun _ -> None
let (copy : t -> t) = fun x -> x
+ ]}
If one does not want/need to provide the of_string state parser, returning
None is fine. This is mandatory only if one wants to define initial values
@@ -105,32 +148,10 @@ val get_graph_attribute : string -> string
(2) All the algos mentionned in the dot file should define the
following functions:
+ {[
let (init_state: int -> State.t) = xxx
let (enable_f: State.t neighbor list -> State.t -> action list) = xxx
let (step_f : State.t neighbor list -> State.t -> action -> State.t ) = xxx
let actions = Some ["action1";"action2"];
+ ]}
*)
-type 's algo_to_register = {
- algo_id : string;
- init_state: int (* holds the process neigbors number *) -> 's;
- enab : 's enable_fun;
- step : 's step_fun;
- actions : action list option (** Mandatory in custom demon mode *)
-}
-type 's to_register = {
- algo : 's algo_to_register list;
- state_to_string: 's -> string; (* [1] *)
- state_of_string: (string -> 's) option; (* To be able to parse state init in the dot *)
- copy_state: 's -> 's;
-}
-(* [1] for state_to_string, the idea here is to print the raw values
- contained in 's.
-
- If a value is omitted, one won't see it in the simulation outputs.
-
- If one prepend a value with "some_id=", some_id will we used in
- the simulation outputs. Otherwise, an id will be invented *)
-
-
-(** To be called once *)
-val register : 's to_register -> unit
diff --git a/lib/sasacore/register.mli b/lib/sasacore/register.mli
index 9c349fe5c901aa3e3631fafdb235eafee30eb4fa..c73dcabbafad903f1aff9811678c46a55bccecce 100644
--- a/lib/sasacore/register.mli
+++ b/lib/sasacore/register.mli
@@ -1,12 +1,12 @@
-(* Time-stamp: <modified the 17/10/2019 (at 20:45) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/10/2019 (at 21:16) by Erwan Jahier> *)
-(** This module duplicates and extends the Algo module with get_*
+(** This module duplicates and extends the Algo module with get_*
functions.
The rationale for defining such a module is to be able to hide the
- get_* functions from the Algo interface. Indeed, they are only
- called bt the sasa engine, and it is useless to show them to
- algorithms designers. *)
+ get_* functions from the Algo interface. Indeed, they are only
+ called by the sasa engine, and it is dangerous and useless to
+ expose them to algorithms designers. *)
type 's neighbor = {
state: 's ;
diff --git a/test/Makefile b/test/Makefile
index a6d7b232c5a1cafc00f7f51328a21bf3889c3f10..3af3c1d28df4ea99e565729fa768386f205ce212 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -21,4 +21,4 @@ clean:
cd dfs/ && make clean
cd dfs-list/ && make clean
-
+-include Makefile.untracked
diff --git a/test/Makefile.inc b/test/Makefile.inc
index 276edfda68fa47cd81c51afde4e5eb01af499138..ed4c5b569225e3831d59de4f56eeb0da35749214 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 16/10/2019 (at 23:27) by Erwan Jahier>
+# Time-stamp: <modified the 17/10/2019 (at 17:11) by Erwan Jahier>
DIR=../../_build/install/default
@@ -26,11 +26,11 @@ LIB=-package algo
$(sasa) $(sasaopt) $*.dot -rif > $*.rif
%.pdf:
- dot -Tpdf $*.dot -o $*.pdf
+ osage -Tpdf $*.dot -o $*.pdf
xpdf $*.pdf
-%.test: %.dot %.cmxs %.lut
- sasa -l 10 $*.dot > $*.rif
+%.log: %.dot %.cmxs %.lut
+ /usr/bin/time -v -o $*.log sasa -l 10000 $*.dot > $*.rif 2> log ; cat log >> $*.log
diff --git a/test/README.md b/test/README.md
index 961f423e71deb69d8bc3590e66f24b30a0568a07..00586e4668442c2c776ede514a5c89070f564ef1 100644
--- a/test/README.md
+++ b/test/README.md
@@ -1,38 +1,22 @@
-- [Algos from the book](#orgec9e12f)
-- [Depth First search](#org9b178aa)
-- [rdbg](#org3ae5b4f)
+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.
+- `test/skeleton/`: a fake algorithm meant to be used as a skeleton
+- `test/dijkstra-ring/`: Dijkstra token ring
+- `test/unison/`: Synchronous unison
+- `test/async-unison/`: Asynchronous unison
+- `test/coloring/`: a graph coloring algorithm
+- `test/alea-coloring/`: a randomized variant of the previous one
+- `test/bfs-spanning-tree/`: a Breadth First Search spanning tree construction
+- `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))
+- `test/dfs-list/`: a Depth First Search using lists
-<a id="orgec9e12f"></a>
+Each directories contains working exemples, 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).
-# Algos from the book
+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).
-This 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` directory also contains sub-directories which gathers programs shared by all examples:
-- <bfs-spanning-tree> : Bread-first-search spanning tree
-- <coloring>: graph coloring
-- <dijkstra-ring>: Dijkstra token ring
-- <unison>:
-
-
-<a id="org9b178aa"></a>
-
-# Depth First search
-
-- <dfs>
-
- contains an \`\`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)
-
-<http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf>
-
-
-<a id="org3ae5b4f"></a>
-
-# rdbg
-
-The following illustrate some possible use of `sasa` with `rdbg` on the examples above
-
-- <my-rdbg-tuning.ml>
-- <rdbg-utils/dot.ml>
+- `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` (it it exists).
diff --git a/test/README.org b/test/README.org
index 888b12e033688354f49e4a0a17d6d7e0f0498303..abd8c1a5d007d91b55b328665f29e730cfa68ab7 100644
--- a/test/README.org
+++ b/test/README.org
@@ -1,30 +1,39 @@
-* Algos from the book
-This directory contains various examples of self-stabilizing
+The [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test][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.
-- file:bfs-spanning-tree : Bread-first-search spanning tree
-- file:coloring: graph coloring
-- file:dijkstra-ring: Dijkstra token ring
-- file:unison:
+- =test/skeleton/=: a fake algorithm meant to be used as a skeleton
+- =test/dijkstra-ring/=: Dijkstra token ring
+- =test/unison/=: Synchronous unison
+- =test/async-unison/=: Asynchronous unison
+- =test/coloring/=: a graph coloring algorithm
+- =test/alea-coloring/=: a randomized variant of the previous one
+- =test/bfs-spanning-tree/=: a Breadth First Search spanning tree construction
+- =test/dfs/=: a Depth First Search using arrays (the ``atomic state
+ model'' version of a [[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf][Depth First Search algorithm proposed by Collin and Dolev in 1994]])
+- =test/dfs-list/=: a Depth First Search using lists
+
+Each directories contains working exemples, 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).
+
+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= (it it exists).
-
-* Depth First search
-
-- file:dfs
-
- contains an ``atomic state model'' version of a
-[[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf][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
-
-* rdbg
-
-The following illustrate some possible use of =sasa= with =rdbg= on
-the examples above
-
-- file:my-rdbg-tuning.ml
-- file:rdbg-utils/dot.ml
diff --git a/test/async-unison/Makefile b/test/async-unison/Makefile
index d9622a8ec91e3d6e54b308aaeeabb732f5b86a59..52da8a2a22ce9d365f685da36e06c2e0c541c716 100644
--- a/test/async-unison/Makefile
+++ b/test/async-unison/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 14/10/2019 (at 20:40) by Erwan Jahier>
+# Time-stamp: <modified the 17/10/2019 (at 17:18) by Erwan Jahier>
test: ring.cmxs ring.lut
@@ -20,6 +20,10 @@ rdbg: ring.ml
rdbg -o ring.rif -l 10000 \
-env "$(sasa) -vl 1 ring.dot -cd"
+rdbg4: grid4.ml
+ rdbg -o ring.rif -l 10000 \
+ -env "sasa grid4.dot -dd"
+
rdbgl: ring.cmxs
rdbg -lurette -o lurette-ring.rif \
-sut "sasa ring.dot -rif -cd "
diff --git a/test/async-unison/grid4.dot b/test/async-unison/grid4.dot
index 17e0751181ff4d340511d27cd0eb8838e98df8af..ef527a6ffce308b4dc4ba87d469634b4bc6665c3 100644
--- a/test/async-unison/grid4.dot
+++ b/test/async-unison/grid4.dot
@@ -1,11 +1,4 @@
-graph grid4 {
-graph [min_deg=2
- mean_deg=3.
- max_deg=4
- is_connected=true
- is_cyclic=true
- is_tree=true
- links_number=24]
+graph g {
p0 [algo="p.ml" init="0"]
p1 [algo="p.ml" init="17"]
p2 [algo="p.ml" init="18"]
@@ -23,29 +16,18 @@ graph [min_deg=2
p14 [algo="p.ml" init="21"]
p15 [algo="p.ml" init="22"]
- p0 -- p1
- p0 -- p4
- p1 -- p2
- p1 -- p5
- p10 -- p11
- p10 -- p14
+ p0 -- p1 -- p2 -- p3 -- p7
+ p0 -- p4 -- p5 -- p6
+ p11-- p15
+ p1 -- p5 -- p9
+ p10 -- p11 -- p7
+ p10 -- p14 -- p15
p10 -- p6
p10 -- p9
- p11 -- p15
- p11 -- p7
- p12 -- p13
- p12 -- p8
- p13 -- p14
+ p12 -- p13 -- p14
+ p12 -- p8 -- p9
p13 -- p9
- p14 -- p15
- p2 -- p3
- p2 -- p6
- p3 -- p7
- p4 -- p5
+ p2 -- p6 -- p7
p4 -- p8
- p5 -- p6
- p5 -- p9
- p6 -- p7
- p8 -- p9
}
-
+
diff --git a/test/async-unison/my-rdbg-tuning.ml b/test/async-unison/my-rdbg-tuning.ml
index 35ea17b36e0d1d1635639f515595333dfb2e90a9..f42644e96dabdd172a901484aeec3fd238f3f5d2 100644
--- a/test/async-unison/my-rdbg-tuning.ml
+++ b/test/async-unison/my-rdbg-tuning.ml
@@ -1,3 +1,8 @@
#use "../my-rdbg-tuning.ml";;
#use "async_unison_oracle.ml";;
+
+let _ =
+ ne ();;
+
+
diff --git a/test/async-unison/state.ml b/test/async-unison/state.ml
index 2c0037d193265e4b72cefe8b07fa491e36c3fe9b..47db884036d1f0d92f855ba68c598a5b93cc3187 100644
--- a/test/async-unison/state.ml
+++ b/test/async-unison/state.ml
@@ -1,5 +1,5 @@
type t = int
-let to_string = (fun s -> Printf.sprintf "i=%i" s)
+let to_string = (fun s -> Printf.sprintf "c=%i" s)
let of_string = Some int_of_string
let copy x = x
diff --git a/test/my-rdbg-tuning.ml b/test/my-rdbg-tuning.ml
index 7ea6d55f0773f856051d2b08ca6e05690f6dbf0a..5d7923d550fe13a55e6807fcc7374b4a47347ba2 100644
--- a/test/my-rdbg-tuning.ml
+++ b/test/my-rdbg-tuning.ml
@@ -37,16 +37,23 @@ let sf () = sfdp p dotfile !e;;
let pa () = patchwork p dotfile !e;;
let os () = osage p dotfile !e;;
-
+let graph_printer =
+ ref (
+ if String.length dotfile > 4 && String.sub dotfile 0 4 = "ring" then ci else
+ if Algo.is_directed () then d else ne)
+(** to change the graph printer
+ graph_printer := ci;;
+ *)
+
(* Convergence is reached when data does not change *)
let rec go () =
let data = !e.data in
- s(); if data = !e.data then ci () else go () ;;
+ s(); if data = !e.data then !graph_printer () else go () ;;
-let sd () = s();ci();;
-let nd () = n();ci();;
-let bd () = b();ci();;
+let sd () = s();!graph_printer();;
+let nd () = n();!graph_printer();;
+let bd () = b();!graph_printer();;
(**********************************************************************)
(* Computing rounds *)
@@ -132,8 +139,9 @@ let prev_match str e =
rev_cond e (fun e -> Str.string_match (Str.regexp_string str) e.name 0)
let rm str = e:=next_match str !e ;;
+
let _ =
- ci ();
+ !graph_printer ();
ignore(Sys.command (Printf.sprintf "zathura sasa-%s.pdf&" dotfile));
round !e
diff --git a/test/skeleton/Makefile b/test/skeleton/Makefile
index 8ddfa28d646eaf3bf9373879d6d6cb4d0e7ccf07..f72dcb9f5d0c495a05d95c5fc2d9f0f5191f59b9 100644
--- a/test/skeleton/Makefile
+++ b/test/skeleton/Makefile
@@ -1,9 +1,8 @@
-# Time-stamp: <modified the 13/09/2019 (at 09:03) by Erwan Jahier>
+# Time-stamp: <modified the 23/10/2019 (at 00:13) by Erwan Jahier>
-test: ring.cmxs ring.lut
- $(sasa) -l 200 ring.dot
-
+test: ring.cmxs
+ sasa -l 200 ring.dot
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
diff --git a/test/unison/Makefile b/test/unison/Makefile
index 42c657db945b33d810344341a18b37cf401d3697..4ebc9768c61a44c0d389bdb59aeae5cee9070d15 100644
--- a/test/unison/Makefile
+++ b/test/unison/Makefile
@@ -1,6 +1,6 @@
-# Time-stamp: <modified the 13/09/2019 (at 10:08) by Erwan Jahier>
+# Time-stamp: <modified the 23/10/2019 (at 09:21) by Erwan Jahier>
-test: test1 test2 lurette0
+test: test1 test2 lurette0 lurette1
test1: fig41.cmxs
$(sasa) -l 5 fig41.dot -sd -rif
@@ -20,7 +20,13 @@ luciole: ring.cmxs
luciole-rif $(sasa) ring.dot -custd -rif -ifi
-lurette0: ring.lut ring_oracle.lus
+lurette0: ring_oracle.lus
+ lurette -o lurette.rif \
+ -sut "$(sasa) ring.dot -sd -rif" \
+ -oracle "lv6 ring_oracle.lus -n oracle"
+
+# Idem with custom daemon
+lurette1: ring.lut ring_oracle.lus
lurette -o lurette.rif \
-env "$(sasa) ring.dot -custd -rif" \
-sut "lutin ring.lut -n synchronous" \