diff --git a/guides/users/README.md b/guides/users/README.md
index 312cef9a4cb2e86f9f697e8ab180188b42473724..68b88a36a88bf00c4d2a5ee349404914e216a9bd 100644
--- a/guides/users/README.md
+++ b/guides/users/README.md
@@ -1,42 +1,42 @@
-- [TL;DR](#org7d8f7c0)
-- [Topology](#orgb740b40)
-- [Algorithms](#org8dcf853)
-- [Examples](#org4a3e28a)
-- [Batch mode](#org45900d7)
- - [Running batch simulations](#org5e6aabd)
- - [Running batch simulations with Built-in daemons](#org688c49a)
- - [Running batch simulations with manual (a.k.a. custom) daemons](#orge126295)
- - [Running batch simulations with `lurette`](#org5e351b7)
- - [Viewing Results](#org5a16c11)
- - [The `sasa` CLI](#org787969e)
-- [Interactive mode](#org578208a)
- - [Example: use `rdbg` from the `test/alea-coloring/` directory](#org7d9fb4e)
- - [The examples of test directory](#org646483c)
- - [Running interactive sessions with `rdbg`](#org4538175)
- - [Getting `rdbg` on-line help](#org8bb16ba)
- - [A `rdbg` `sasa` GUI](#org69bf58c)
- - [Useful Modules](#org5781218)
-- [Install](#orgccc7e98)
- - [TL;DR](#orgf88e099)
- - [Not strictly mandatory, but useful, third-party software](#orge18cbad)
- - [Install `sasa` via opam (version >= 2.\*)](#orgb522bdb)
- - [Install `sasa` via `git`](#orgb3bb93b)
- - [Use `sasa` via docker](#orgbdfd166)
- - [Use `sasa` via a Virtual Machine](#org8a3c22b)
-- [Screencasts](#orgcb02048)
-- [More](#org020d69e)
-- [FAQ](#org4be25b7)
- - [Is there a FAQ?](#orgb84f441)
- - [I have a compilation error that I don't understand](#orgc8ed449)
- - [I have the error `Invalid_argument("compare: functional value")`](#org0f6d260)
-
-
-
-<a id="org7d8f7c0"></a>
+- [TL;DR](#org39183ef)
+- [Topology](#org6e25882)
+- [Algorithms](#org8d92aaa)
+- [Examples](#org69e266f)
+- [Batch mode](#org7ccea27)
+ - [Running batch simulations](#org179a988)
+ - [Running batch simulations with Built-in daemons](#org824da33)
+ - [Running batch simulations with manual (a.k.a. custom) daemons](#org9d25e8a)
+ - [Running batch simulations with `lurette`](#org519078c)
+ - [Viewing Results](#org2cce9d1)
+ - [The `sasa` CLI](#org03c25f2)
+- [Interactive mode](#org9240f09)
+ - [Example: use `rdbg` from the `test/alea-coloring/` directory](#org8c861b9)
+ - [The examples of test directory](#org7b1ddfd)
+ - [Running interactive sessions with `rdbg`](#org217b3a7)
+ - [Getting `rdbg` on-line help](#orge9d7f0c)
+ - [A `rdbg` `sasa` GUI](#orgb314d64)
+ - [Useful Modules](#orga76b44c)
+- [Install](#orgb39525c)
+ - [TL;DR](#orgd7c4a67)
+ - [Not strictly mandatory, but useful, third-party software](#org2fc3700)
+ - [Install `sasa` via opam (version >= 2.\*)](#orgf9f69ad)
+ - [Install `sasa` via `git`](#org48f2912)
+ - [Use `sasa` via docker](#org587fcce)
+ - [Use `sasa` via a Virtual Machine](#org2137ab7)
+- [Screencasts](#org194016f)
+- [More](#orgc6ef0db)
+- [FAQ](#org4b684da)
+ - [Is there a FAQ?](#org0900013)
+ - [I have a compilation error that I don't understand](#org25122e8)
+ - [I have the error `Invalid_argument("compare: functional value")`](#orgebdea9f)
+
+
+
+<a id="org39183ef"></a>
# TL;DR
-<a id="org7c817e9"></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="org33ef0b5"></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:
@@ -49,8 +49,8 @@ The fastest way to get started is to copy the files provided in the `test/skelet
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 ring7.cmxs # compile anything that needs to be compiled
-sasa ring7.dot -l 4 # run a batch simulation for 4 steps
+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)
@@ -61,11 +61,11 @@ sasa ring7.dot -l 4 # run a batch simulation for 4 steps
[](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/poster.pdf)
-<a id="orgb740b40"></a>
+<a id="org6e25882"></a>
# Topology
-<a id="orgf00d97c"></a> <a id="org5857dc1"></a> The topology is given via `.dot` files, that should
+<a id="org6ac5cf5"></a> <a id="orga382cab"></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
@@ -121,24 +121,26 @@ graph ring {
Such parameters can be retrieved in algorithms using the `Algo.get_graph_attribute : string -> string` function. For example, if you know the graph diameter, you can define it as a graph attribute (a `Algo.diameter: unit -> int` function is provided, but it can be expensive to use for large graphs).
-Some tools are provided in the `sasa` [distributions](#org366a559) 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](#org960f5a3) to generate such kinds of `dot` graphs: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/>
-<a id="org8dcf853"></a>
+<a id="org8d92aaa"></a>
# Algorithms
-<a id="orga43fd68"></a>
+<a id="org01365c1"></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)
-<div class="html">
-<iframe title="The Algo API" name="algo-api" width="700" height="700" src="<https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/algo/Algo/index.html>" alt="<sub>html</sub>/algo/Algo/index.html";> </iframe>
+<iframe title="The Algo API" name="algo-api"
+ width="700"
+ height="700"
+ src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/algo/Algo/index.html"
+ alt="_html/algo/Algo/index.html";>
+</iframe>
-</div>
-
-<a id="org4a3e28a"></a>
+<a id="org69e266f"></a>
# Examples
@@ -178,14 +180,14 @@ The `test` directory also contains sub-directories which gathers programs shared
- `test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (if it exists).
-<a id="org45900d7"></a>
+<a id="org7ccea27"></a>
# Batch mode
-<a id="org5e6aabd"></a>
+<a id="org179a988"></a>
## Running batch simulations
@@ -252,7 +254,7 @@ sasa ring.dot # launch the 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.
-<a id="org688c49a"></a>
+<a id="org824da33"></a>
## Running batch simulations with Built-in daemons
@@ -271,7 +273,7 @@ sasa -h | grep "\-daemon"
--greedy-daemon, -gd
-<a id="orge126295"></a>
+<a id="org9d25e8a"></a>
## Running batch simulations with manual (a.k.a. custom) daemons
@@ -309,7 +311,7 @@ luciole-rif sasa ring.dot --custom-daemon
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).
-<a id="org5e351b7"></a>
+<a id="org519078c"></a>
## Running batch simulations with `lurette`
@@ -334,14 +336,14 @@ Note that for `lurette`, the role of the SUT (System Under Test) and the one of
For more information on this topic: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-daemons/>
-<a id="org5a16c11"></a>
+<a id="org2cce9d1"></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/>
-<a id="org787969e"></a>
+<a id="org03c25f2"></a>
## The `sasa` CLI
@@ -411,11 +413,11 @@ sasa --more
Display the version ocaml version sasa was compiled with and exit.
-<a id="org578208a"></a>
+<a id="org9240f09"></a>
# Interactive mode
-<a id="org1e0f245"></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/).
+<a id="orgddd934b"></a> If you want to perform step-by-step simulations, you can use the `-custd` option. But if you want to perform step-by-step simulations without the burden of playing the role of the daemon, you can launch `sasa` under the control of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/).
Another advantage of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/) is its ability to display a graphical view of the current configuration during the simulation, to move step by step, or round by round, forward or backwards.
@@ -424,7 +426,7 @@ cf <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbg-sasa/>
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).
-<a id="org7d9fb4e"></a>
+<a id="org8c861b9"></a>
## Example: use `rdbg` from the `test/alea-coloring/` directory
@@ -467,7 +469,7 @@ rdbg
[q] quit
-<a id="org646483c"></a>
+<a id="org7b1ddfd"></a>
## The examples of test directory
@@ -478,7 +480,7 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t
- `test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (it it exists).
-<a id="org4538175"></a>
+<a id="org217b3a7"></a>
## Running interactive sessions with `rdbg`
@@ -495,7 +497,7 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t
All those commands are defined in (the common) [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml) that is included in (locals) `test/*/my-rdbg-tuning.ml` that are included in (generated) `test/*/rdbg-session.ml` files. `my-rdbg-tuning.ml` contains straigthforward `ocaml` code that defines various `rdbg` shortcuts to ease the simulation of `sasa` systems. Feel free to tailor those command to yours needs by modyfying the local `my-rdbg-tuning.ml`!
-<a id="org8bb16ba"></a>
+<a id="orge9d7f0c"></a>
## Getting `rdbg` on-line help
@@ -591,7 +593,7 @@ Here are 2 useful entry-points to rdbg on-line help:
(rdbg)
-<a id="org69bf58c"></a>
+<a id="orgb314d64"></a>
## A `rdbg` `sasa` GUI
@@ -605,41 +607,49 @@ opam install -y rdbgui4ocaml
To use it: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/>
-<a id="org5781218"></a>
+<a id="orga76b44c"></a>
## Useful Modules
Some modules, used by the sasa core engine, can be useful from `rdbg`.
-<div class="html">
-<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="<./_html/sasacore/Sasacore/Topology/index.html>";> </iframe>
-
-</div>
-
-<div class="html">
-<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="<./_html/sasacore/Sasacore/Diameter/index.html>";> </iframe>
-
-</div>
-
-<div class="html">
-<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="<./_html/sasacore/Sasacore/Process/index.html>";> </iframe>
-
-</div>
-
-<div class="html">
-<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="<./_html/sasacore/Sasacore/StringOf/index.html>";> </iframe>
-
-</div>
-
-
-<a id="orgccc7e98"></a>
+<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="orgb39525c"></a>
# Install
-<a id="org366a559"></a> <a id="org4c1c8c8"></a>
+<a id="org960f5a3"></a> <a id="orgd4bae36"></a>
-<a id="orgf88e099"></a>
+<a id="orgd7c4a67"></a>
## TL;DR
@@ -693,7 +703,7 @@ git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.gi
```
-<a id="orge18cbad"></a>
+<a id="org2fc3700"></a>
## Not strictly mandatory, but useful, third-party software
@@ -736,7 +746,7 @@ sudo apt install -y wish
Otherwise: <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html>
-<a id="orgb522bdb"></a>
+<a id="orgf9f69ad"></a>
## Install `sasa` via opam (version >= 2.\*)
@@ -770,7 +780,7 @@ opam upgrade
```
-<a id="orgb3bb93b"></a>
+<a id="org48f2912"></a>
## Install `sasa` via `git`
@@ -814,14 +824,14 @@ 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).
-<a id="orgbdfd166"></a>
+<a id="org587fcce"></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.).
-<a id="org8a3c22b"></a>
+<a id="org2137ab7"></a>
## Use `sasa` via a Virtual Machine
@@ -831,7 +841,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve
- passwd:sasa
-<a id="orgcb02048"></a>
+<a id="org194016f"></a>
# Screencasts
@@ -847,7 +857,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve
cf <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/>
-<a id="org020d69e"></a>
+<a id="orgc6ef0db"></a>
# More
@@ -856,12 +866,12 @@ cf <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/>
- Tutorials: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt//tags/sasa/>
-<a id="org4be25b7"></a>
+<a id="org4b684da"></a>
# FAQ
-<a id="orgb84f441"></a>
+<a id="org0900013"></a>
## Is there a FAQ?
@@ -870,7 +880,7 @@ Yes.
Beside, some tutorials are also available here: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/>
-<a id="orgc8ed449"></a>
+<a id="org25122e8"></a>
## I have a compilation error that I don't understand
@@ -880,7 +890,7 @@ Beside, some tutorials are also available here: <https://verimag.gricad-pages.un
- If the message is totally useless, please feel free to add an issue here <https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/issues>
-<a id="org0f6d260"></a>
+<a id="orgebdea9f"></a>
## I have the error `Invalid_argument("compare: functional value")`
diff --git a/guides/users/README.org b/guides/users/README.org
index 8af41139d44e7008ef52ded132fcddd2c1ad40cf..b0600652771dd2f34a8abf10954915cc53c98ef8 100644
--- a/guides/users/README.org
+++ b/guides/users/README.org
@@ -51,40 +51,10 @@ make clean
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 ring7.cmxs # compile anything that needs to be compiled
-sasa ring7.dot -l 4 # run a batch simulation for 4 steps
+make ring.cmxs # compile anything that needs to be compiled
+sasa ring.dot -l 4 # run a batch simulation for 4 steps
#+END_SRC
-#+RESULTS[13cc60a20b534115483ffd7ae0f22f6bcc52a8dd]:
-#+begin_example
-sasa -reg ring7.dot
-ocamlfind ocamlopt -package algo -shared state.ml p.ml config.ml ring7.ml -o ring7.cmxs
-# Automatically generated by /home/jahier/.opam/4.10.0/bin/sasa version "4.3.5" ("a6897fa")
-# on crevetete the 4/11/2020 at 8:28:38
-#sasa ring7.dot -l 4
-
-#seed 194528744
-#inputs
-#outputs "p1_i":int "p2_i":int "p3_i":int "p4_i":int "p5_i":int "p6_i":int "p7_i":int "Enab_p1_action2":bool "Enab_p1_action1":bool "Enab_p2_action2":bool "Enab_p2_action1":bool "Enab_p3_action2":bool "Enab_p3_action1":bool "Enab_p4_action2":bool "Enab_p4_action1":bool "Enab_p5_action2":bool "Enab_p5_action1":bool "Enab_p6_action2":bool "Enab_p6_action1":bool "Enab_p7_action2":bool "Enab_p7_action1":bool "p1_action2":bool "p1_action1":bool "p2_action2":bool "p2_action1":bool "p3_action2":bool "p3_action1":bool "p4_action2":bool "p4_action1":bool "p5_action2":bool "p5_action1":bool "p6_action2":bool "p6_action1":bool "p7_action2":bool "p7_action1":bool
-
-
-#step 0
-#outs 4 5 2 1 9 0 4 t f t f f f t f f t t f t f f f f f f f t f f t t f f f
-
-#step 1
-#outs 4 5 2 0 1 0 4 t f t f f t f f f t t f t f f f t f f t f f f f t f t f
-
-#step 2
-#outs 4 0 1 0 1 0 0 f t f f f t f f f t f t t f f f f f f t f f f f f f t f
-
-#step 3
-#outs 4 0 1 0 1 0 0 f t f f f t f f f t f t t f f t f f f f f f f f f f f f
-
-#step 4
-#outs 1 0 1 0 1 0 0 f t f f f t f f f t f t f f f f f f f t f f f t f t f f
-#q
-#+end_example
-
+ [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa][SASA source code]]
+ [[https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/][Some Online Tutorials]]
+ [[https://hal.archives-ouvertes.fr/hal-02521149][TAP 2020 article pre-print]]
@@ -175,14 +145,14 @@ https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/
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
+#+BEGIN_EXPORT html
<iframe title="The Algo API" name="algo-api"
width="700"
height="700"
src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/algo/Algo/index.html"
alt="_html/algo/Algo/index.html";>
</iframe>
-#+end_html
+#+END_EXPORT
* Examples
@@ -738,38 +708,38 @@ To use it: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdb
Some modules, used by the sasa core engine, can be useful from =rdbg=.
-#+begin_html
+#+BEGIN_EXPORT html
<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>
-#+end_html
-#+begin_html
+#+END_EXPORT
+#+BEGIN_EXPORT html
<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>
-#+end_html
-#+begin_html
+#+END_EXPORT
+#+BEGIN_EXPORT html
<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>
-#+end_html
-#+begin_html
+#+END_EXPORT
+#+BEGIN_EXPORT html
<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>
-#+end_html
+#+END_EXPORT
* Install
<<distributions>>
diff --git a/lib/sasa/sasaRun.ml b/lib/sasa/sasaRun.ml
index 6b1b1b45dd950d950d274bdf11042256783f5549..5e06fd21e52434eedd8535cb977fe79b3f851e61 100644
--- a/lib/sasa/sasaRun.ml
+++ b/lib/sasa/sasaRun.ml
@@ -15,22 +15,29 @@ let (get_action_value : (string * Data.v) list -> string -> string -> bool) =
open Sasacore
open Process
-let (from_sasa_env : 'v SimuState.t -> RdbgPlugin.sl) =
- fun st ->
+
+let (from_conf : 'v Process.t list -> 'v Conf.t -> RdbgPlugin.sl) =
+ fun pl conf ->
List.fold_left
(fun acc p ->
- let state = Conf.get st.config p.pid in
+ let state = Conf.get conf p.pid in
let sl = SasaState.to_rdbg_subst p.pid state in
acc@sl
)
[]
- st.network
+ pl
+
+let (from_sasa_env : 'v SimuState.t -> RdbgPlugin.sl) =
+ fun st ->
+ from_conf st.network st.config
let (get_sl_out: bool -> 'v Process.t list -> bool list list -> RdbgPlugin.sl) =
fun enab pl ll ->
let str = if enab then "Enab_" else "" in
List.flatten (
+ (* assert (List.length pl = List.length ll); *)
List.map2 (fun p enab_l ->
+ (* assert (List.length p.actions = List.length enab_l); *)
List.map2 (fun a enab ->
Printf.sprintf "%s%s_%s" str p.pid (StringOf.action a), Data.B enab)
p.actions enab_l)
@@ -93,7 +100,7 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
pre_enable_processes_opt := Some(pnall, enab_ll);
("silent", Data.B silent)::("legitimate", Data.B legit)::pot_sl
@ sasa_nenv @ (get_sl_out true pl enab_ll)
- )
+ )
| Some (pre_pnall, pre_enab_ll) ->
(* let was_silent = List.for_all (fun b -> not b) (List.flatten pre_enab_ll) in *)
(* if was_silent then failwith "Silent"; *)
@@ -149,11 +156,55 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
(from_sasa_env st) @ (get_sl_out true pl enab_ll) @
(get_sl_out false pl activate_val)
in
+ let exaustive_search_res = ref None in
+ let rec (step_exhaustive_search : RdbgPlugin.sl -> RdbgPlugin.sl) =
+ fun x ->
+ match !exaustive_search_res with
+ | None ->
+ let log = open_out (st.sasarg.topo ^ ".log") in
+ let path = ExhaustSearch.f log (st.sasarg.daemon=ExhaustCentralSearch) st in
+ exaustive_search_res := Some path;
+ step_exhaustive_search x
+ | Some [] -> []
+ | Some ((enab_ll, trig_ll, legit, pot, conf)::path) ->
+ exaustive_search_res := Some path;
+ let trig_ll = if List.flatten trig_ll = [] then enab_ll else trig_ll in
+ let silent = List.for_all (fun b -> not b) (List.flatten enab_ll) in
+ let conf_sl = from_conf st.network conf in
+ let enab = get_sl_out true pl enab_ll in
+ let trig = get_sl_out false pl trig_ll in
+ ("silent", Data.B silent)::("legitimate", Data.B legit)::
+ ("potential", Data.F pot):: conf_sl @ enab @ trig
+ in
+ let es_ss_table = Hashtbl.create 10 in
+ let exhaustive_search_save_state i =
+ Hashtbl.replace es_ss_table i !exaustive_search_res
+ in
+ let exhaustive_search_restore_state i =
+ match Hashtbl.find_opt es_ss_table i with
+ | Some esr -> exaustive_search_res := esr
+ | None ->
+ Printf.eprintf "Cannot restore state %i from sasa\n" i;
+ flush stderr
+ in
+ let exhaustive_search_reset () =
+ match !exaustive_search_res with
+ | None -> ()
+ | Some _ ->
+ let log = open_out (st.sasarg.topo ^ ".log") in
+ ExhaustSearch.reset ();
+ let path = ExhaustSearch.f log (st.sasarg.daemon=ExhaustCentralSearch) st in
+ exaustive_search_res := Some path
+ in
+ let _exhaustive_search_reset () =
+ ()
+ in
let step =
- if st.sasarg.daemon = DaemonType.Custom then
- step_custom
- else
- step_internal_daemon
+ match st.sasarg.daemon with
+ | DaemonType.Custom -> step_custom
+ | ExhaustCentralSearch
+ | ExhaustSearch -> step_exhaustive_search
+ | _ -> step_internal_daemon
in
let ss_table = Hashtbl.create 10 in
let step_dbg sl_in ctx cont =
@@ -178,32 +229,43 @@ let (make_do: string array -> 'v SimuState.t -> RdbgPlugin.t) =
in
let (mems_in : Data.subst list) = [] in
let (mems_out : Data.subst list) = [] in
+ let sasa_save_state i =
+ let prgs = Random.get_state () in
+ (* Printf.eprintf "Save state %i from sasa\n%!" i; *)
+ Hashtbl.replace ss_table i
+ (prgs, !sasa_config, !pre_enable_processes_opt)
+ in
+ let sasa_restore_state i =
+ match Hashtbl.find_opt ss_table i with
+ | Some (prgs, e, pepo) ->
+ Random.set_state prgs;
+ (* Printf.eprintf "Restore state %i from sasa\n%!" i; *)
+ sasa_config := e; pre_enable_processes_opt := pepo
+ | None ->
+ Printf.eprintf "Cannot restore state %i from sasa\n" i;
+ flush stderr
+ in
{
id = prog_id;
inputs = vntl_i;
outputs= vntl_o;
- reset=(fun () -> reset());
+ reset= (match st.sasarg.daemon with
+ | ExhaustCentralSearch | ExhaustSearch -> exhaustive_search_reset
+ | _ -> reset
+ );
kill=(fun _ -> flush stdout; flush stderr);
init_inputs=mems_in;
init_outputs=mems_out;
step=step;
step_dbg = step_dbg;
- save_state = (fun i ->
- let prgs = Random.get_state () in
- (* Printf.eprintf "Save state %i from sasa\n%!" i; *)
- Hashtbl.replace ss_table i
- (prgs, !sasa_config, !pre_enable_processes_opt)
- );
- restore_state = (fun i ->
- match Hashtbl.find_opt ss_table i with
- | Some (prgs, e, pepo) ->
- Random.set_state prgs;
- (* Printf.eprintf "Restore state %i from sasa\n%!" i; *)
- sasa_config := e; pre_enable_processes_opt := pepo
- | None ->
- Printf.eprintf "Cannot restore state %i from sasa\n" i;
- flush stderr
- );
+ save_state = (match st.sasarg.daemon with
+ | ExhaustCentralSearch | ExhaustSearch -> exhaustive_search_save_state
+ | _ -> sasa_save_state
+ );
+ restore_state = (match st.sasarg.daemon with
+ | ExhaustCentralSearch | ExhaustSearch -> exhaustive_search_restore_state
+ | _ -> sasa_restore_state
+ );
}
diff --git a/lib/sasacore/daemon.ml b/lib/sasacore/daemon.ml
index 58b61ff7e5c1bf84834963f8488d6ab8d66bd5c2..24781ad2ca8823fe83b88d11a651499f5b620fe8 100644
--- a/lib/sasacore/daemon.ml
+++ b/lib/sasacore/daemon.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/10/2021 (at 23:20) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/10/2021 (at 14:17) by Erwan Jahier> *)
(* Enabled processes (with its enabling action + neighbors) *)
type 'v pna = 'v Process.t * 'v Register.neighbor list * Register.action
diff --git a/src/exhaustSearch.ml b/lib/sasacore/exhaustSearch.ml
similarity index 93%
rename from src/exhaustSearch.ml
rename to lib/sasacore/exhaustSearch.ml
index 54b7ed023532f03d109ef43f1b8db189d5e9f466..a6e92a64ca9321371319405cb57c2694a17b94f6 100644
--- a/src/exhaustSearch.ml
+++ b/lib/sasacore/exhaustSearch.ml
@@ -1,5 +1,4 @@
-open Sasacore
open LocalSearch
type 'v ss = 'v SimuState.t
@@ -19,7 +18,7 @@ let delta = 1.0 (* the potential decreases of at least delta at each step *)
(* This priority is given to the highest (depth, potential) couple at
the beginning, which induces a greedy depth first search. Then,
once a first solution has been found, the priority goes to the most
- promising node *)
+ promising node *)
let best = ref None
let pot_init = ref max_float
@@ -29,7 +28,7 @@ let priority n =
| None -> if n.pot <= 0.0 then d else d -. (1.0 /. (n.pot/.delta))
| Some b -> d +. n.pot *. (b /. !pot_init)
-let priority n =
+let _priority n =
let d = float_of_int n.d in
if n.pot <= 0.0 then d else d -. (1.0 /. (n.pot/.delta))
@@ -45,7 +44,8 @@ end
module Q = Psq.Make (Int) (M)
let cumulated_Q_time = ref 0.0
-let update_Q_now = ref false
+let update_Q_now = ref false
+
let update_Q q =
(* when the priority changes, we need to recompute the queue from
scratch (actually, it does not work too bad if we don't, but
@@ -73,9 +73,11 @@ let all_false ll = List.for_all (fun b -> not b) (List.flatten ll)
let sob = fun b -> if b then "t" else "f"
-let (bnb : out_channel -> bool -> int -> 'v ss ->
+open SimuState
+let (bnb : out_channel -> bool -> 'v ss ->
(bool list list * bool list list * bool * float * 'v Conf.t) list) =
- fun log central max_step st0 ->
+ fun log central st0 ->
+ let max_step = st0.sasarg.length in
let cpt = ref 0 in
let qsize = ref 0 in
let args = st0.sasarg in
@@ -83,9 +85,9 @@ let (bnb : out_channel -> bool -> int -> 'v ss ->
let successors n =
let st = get_ss n.st in
let pot_st = n.cost -. (float_of_int n.d) in
- let all, enab_ll = Sasacore.SimuState.get_enable_processes st in
+ let all, enab_ll = SimuState.get_enable_processes st in
let enable_val = String.concat " " (List.map sob (List.flatten enab_ll)) in
- if Sasacore.SimuState.legitimate st then [] else (
+ if SimuState.legitimate st then [] else (
let all = if central then Enumerate.central_list all else Enumerate.all_list all in
List.map
(fun al ->
@@ -118,7 +120,7 @@ let (bnb : out_channel -> bool -> int -> 'v ss ->
{
init = { st=marshall_ss st0; d=0; pot=pot0 ; cpt=0; path=[]; cost=pot0 }, Q.empty, ();
succ = successors;
- stop = (fun _ node ->
+ stop = (fun _ _node ->
if !cpt >= max_step then (
pf log "Max number of step reached (%d). Queue size=%d\n%!" !cpt !qsize;
pf stdout "Max number of step reached (%d). Queue size=%d\n%!" !cpt !qsize;
@@ -157,7 +159,7 @@ let (bnb : out_channel -> bool -> int -> 'v ss ->
let path =
let st = get_ss sol.st in
let pot_st = sol.cost -. (float_of_int sol.d) in
- let _all, enab_ll = Sasacore.SimuState.get_enable_processes st in
+ let _all, enab_ll = SimuState.get_enable_processes st in
(enab_ll,[], true, pot_st, sol.st)::sol.path
in
List.map
@@ -207,3 +209,9 @@ let (bnb : out_channel -> bool -> int -> 'v ss ->
let f = bnb
+
+let reset () =
+ best := None;
+ pot_init := max_float;
+ cumulated_Q_time := 0.0;
+ update_Q_now := false
diff --git a/lib/sasacore/worstInit.ml b/lib/sasacore/worstInit.ml
index 728ce99d92cc3a9b4deef439e3d7f1daac6af4d1..fd6ba9171fdf155e984563a57d1984e7f5e44bad 100644
--- a/lib/sasacore/worstInit.ml
+++ b/lib/sasacore/worstInit.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/10/2021 (at 13:53) by Erwan Jahier> *)
+(* Time-stamp: <modified the 22/10/2021 (at 10:48) by Erwan Jahier> *)
open Register
@@ -7,15 +7,6 @@ type point = value Array.t
let debug = false
- (* type succ_heuristic = (* Various heuristic to choose the neighbor *) *)
- (* | OneDim (* only move one value at a time *) *)
- (* | RanDim (* move a value or not at random *) *)
-(* | AllDim (* move all values *) *)
-
-(* let succ_heuristic_nb = 3 *)
-(* let int_of_succ_heuristic = function OneDim -> 0 | RanDim -> 1 | AllDim -> 2 *)
- (* let succ_heuristic_of_int = function 0 -> OneDim | 1 -> RanDim | 2 -> AllDim *)
-(* | _ -> assert false *)
let deltaf=1.0 (* something else ?? *)
let mutate_value = function
diff --git a/src/sasaMain.ml b/src/sasaMain.ml
index 1f0178777df53ff52c37570d84afe3b2dd82959d..0b96c75c856becb84da49a9dda747c4a3706fb3d 100644
--- a/src/sasaMain.ml
+++ b/src/sasaMain.ml
@@ -192,7 +192,7 @@ let () =
match st.sasarg.init_search_max_trials, st.sasarg.daemon with
| None, (ExhaustSearch|ExhaustCentralSearch) ->
let log = open_out (st.sasarg.topo ^ ".log") in
- let path = ExhaustSearch.f log (st.sasarg.daemon=ExhaustCentralSearch) n st in
+ let path = ExhaustSearch.f log (st.sasarg.daemon=ExhaustCentralSearch) st in
List.iteri
(fun i (enab, trig, leg, pot, conf) ->
if trig <> [] then
@@ -228,9 +228,9 @@ let () =
let res =
try if st.sasarg.daemon = ExhaustSearch ||
st.sasarg.daemon = ExhaustCentralSearch
- then
- List.length (ExhaustSearch.f log (st.sasarg.daemon=ExhaustCentralSearch) n st)
- else
+ then
+ List.length (ExhaustSearch.f log (st.sasarg.daemon=ExhaustCentralSearch) st)
+ else
simuloop log n n "" s
with error ->
(* We consider that error here mean that a meaningless configuration
@@ -248,8 +248,9 @@ let () =
close_out newdot;
close_out log;
failwith(Printf.sprintf
- "Maximum simulation length reached. Something went wrong or %d is not long enough (use sasa -l to try longer simulation" n
- )
+ "Maximum simulation length reached. Something went wrong or %d %s"
+ n "is not long enough (use sasa -l to try longer simulation)"
+ )
)
else
res
diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml
index 3ecd327f7aa1e6fed366885c9d2ad51c01e48e42..50d7ccbb757c74e68be8adfda989dad824ac7feb 100644
--- a/tools/rdbg4sasa/gtkgui.ml
+++ b/tools/rdbg4sasa/gtkgui.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 27/08/2021 (at 16:36) by Erwan Jahier> *)
+(* Time-stamp: <modified the 22/10/2021 (at 10:43) by Erwan Jahier> *)
#thread
#require "lablgtk3"
@@ -565,6 +565,7 @@ let main () =
in
let p str = black text_out#buffer str in
(* It should be better to rely on the gtk event handler *)
+
restart p ();
let bbox = GPack.hbox ~packing: box#add () in
diff --git a/tools/rdbgui4sasa/rdbgui.ml b/tools/rdbgui4sasa/rdbgui.ml
index edaa729a9f70df56f20d9b93a5b6333d922383d9..246fcaf2a0ec34e43f509dd2fc1beaa8a1c4e9d5 100644
--- a/tools/rdbgui4sasa/rdbgui.ml
+++ b/tools/rdbgui4sasa/rdbgui.ml
@@ -7,6 +7,10 @@ let rdbg_cmd =
let salut_mode = not (Str.string_match (Str.regexp ".*sasa .*\\.dot") str 0) in
let str = if salut_mode then str else
Str.replace_first (Str.regexp "sasa ") "sasa -custd -replay " str
+ (* I add -custd here, but it ought to be overridden by user option.
+ The idea is that I don't want the default daemon to be -dd from the gui
+ (as it is the case from the cli)
+ *)
in
let sasa_opt = if salut_mode then "--salut" else "--sasa" in
String.concat " " ("rdbg"::sasa_opt::str::[])