diff --git a/guides/users/README.md b/guides/users/README.md
index 45f40201838ee92da0c4666f7528f772737fcd30..fef5b3ff363cc810cbd7054f1fa5dd62880f0f2f 100644
--- a/guides/users/README.md
+++ b/guides/users/README.md
@@ -1,42 +1,42 @@
-- [TL;DR](#orgf91e791)
-- [Topology](#orgb55a700)
-- [Algorithms](#orgbabf1bc)
-- [Examples](#org6caeea0)
-- [Batch mode](#org605c659)
-  - [Running batch simulations](#org66b4e7c)
-  - [Running batch simulations with Built-in daemons](#orga34891c)
-  - [Running batch simulations with manual (a.k.a. custom) daemons](#orgdc4e901)
-  - [Running batch simulations with `lurette`](#org78885ec)
-  - [Viewing Results](#org2753f29)
-  - [The `sasa` CLI](#orge6e4643)
-- [Interactive mode](#org3a02f22)
-  - [Example: use `rdbg` from the `test/alea-coloring/` directory](#org0c64c8e)
-  - [The examples of test directory](#org7332823)
-  - [Running interactive sessions with `rdbg`](#org8c4ba7c)
-  - [Getting `rdbg` on-line help](#orgd2dfbbd)
-  - [A `rdbg`  `sasa` GUI](#org7914fd6)
-  - [Useful Modules](#orgf6b0394)
-- [Install](#orgc3e7487)
-  - [TL;DR](#org70cd209)
-  - [Not strictly mandatory, but useful, third-party software](#org2db11de)
-  - [Install `sasa` via opam (version >= 2.\*)](#org6475b9d)
-  - [Install `sasa` via `git`](#org191f6ee)
-  - [Use `sasa` via docker](#orga9494d0)
-  - [Use `sasa` via a Virtual Machine](#org6282d99)
-- [Screencasts](#orge3d9e56)
-- [More](#org686b3ba)
-- [FAQ](#orgd95151e)
-  - [Is there a FAQ?](#org8853048)
-  - [I have a compilation error that I don't understand](#orgbbdf456)
-  - [I have the error `Invalid_argument("compare: functional value")`](#orga5a86c6)
-
-
-
-<a id="orgf91e791"></a>
+- [TL;DR](#org9c9d503)
+- [Topology](#orgff582ab)
+- [Algorithms](#org5ef8bb4)
+- [Examples](#org2fa119a)
+- [Batch mode](#orga200c38)
+  - [Running batch simulations](#orgbcba3e2)
+  - [Running batch simulations with Built-in daemons](#org6f81e55)
+  - [Running batch simulations with manual (a.k.a. custom) daemons](#org4c63674)
+  - [Running batch simulations with `lurette`](#orgd2bc290)
+  - [Viewing Results](#org2b0799e)
+  - [The `sasa` CLI](#org3b8d4b3)
+- [Interactive mode](#org02bafa4)
+  - [Example: use `rdbg` from the `test/alea-coloring/` directory](#orgd499f7a)
+  - [The examples of test directory](#org75ae70f)
+  - [Running interactive sessions with `rdbg`](#orge4643af)
+  - [Getting `rdbg` on-line help](#org30c51b6)
+  - [A `rdbg`  `sasa` GUI](#org2b4589f)
+  - [Useful Modules](#orgd3bfce6)
+- [Install](#orgead66ac)
+  - [TL;DR](#orgb390429)
+  - [Not strictly mandatory, but useful, third-party software](#orgb4cc09a)
+  - [Install `sasa` via opam (version >= 2.\*)](#org8290be6)
+  - [Install `sasa` via `git`](#orgb63c57e)
+  - [Use `sasa` via docker](#org13c72f7)
+  - [Use `sasa` via a Virtual Machine](#orgaf70033)
+- [Screencasts](#org52c7a2d)
+- [More](#org4d55fa9)
+- [FAQ](#orge446f5a)
+  - [Is there a FAQ?](#org1788b9d)
+  - [I have a compilation error that I don't understand](#org2ea9013)
+  - [I have the error `Invalid_argument("compare: functional value")`](#orga4555a7)
+
+
+
+<a id="org9c9d503"></a>
 
 # TL;DR
 
-<a id="org1c9155f"></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="orgab88045"></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:
 
@@ -61,11 +61,11 @@ sasa ring.dot -l 4      # run a batch simulation for 4 steps
 [![img](poster.png)](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/poster.pdf)
 
 
-<a id="orgb55a700"></a>
+<a id="orgff582ab"></a>
 
 # Topology
 
-<a id="orgb9ac408"></a> <a id="orgc17dcc7"></a> The topology is given via `.dot` files, that should
+<a id="orgbd10083"></a> <a id="orgf20065d"></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,14 +121,14 @@ graph ring {
 
 Such parameters can be retrieved in algorithms using the `Algo.get_graph_attribute : string -> string` function. For example, if you know the graph diameter, you can define it as a graph attribute (a `Algo.diameter: unit -> int` function is provided, but it can be expensive to use for large graphs).
 
-Some tools are provided in the `sasa` [distributions](#org5e646e7) 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](#org6e26471) to generate such kinds of `dot` graphs: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/>
 
 
-<a id="orgbabf1bc"></a>
+<a id="org5ef8bb4"></a>
 
 # Algorithms
 
-<a id="orgf435615"></a>
+<a id="orgd7787ed"></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)
 
@@ -140,7 +140,7 @@ The following has been generated from [algo.mli](https://gricad-gitlab.univ-gren
 </iframe>
 
 
-<a id="org6caeea0"></a>
+<a id="org2fa119a"></a>
 
 # Examples
 
@@ -154,19 +154,19 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t
 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
-6.  `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.
+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).
 
@@ -180,14 +180,14 @@ The `test` directory also contains sub-directories which gathers programs shared
 -   `test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (if it exists).
 
 
-<a id="org605c659"></a>
+<a id="orga200c38"></a>
 
 # Batch mode
 
 ![img](./sasabatch.svg)
 
 
-<a id="org66b4e7c"></a>
+<a id="orgbcba3e2"></a>
 
 ## Running batch simulations
 
@@ -228,31 +228,36 @@ All the CLI commands above can be run automatically using a `make` rule containe
  sasa ring.dot    # launch the simulation
 ```
 
-    sasa -reg ring.dot
-    ocamlfind ocamlopt -bin-annot -package algo -shared state.ml p.ml config.ml ring.ml -o ring.cmxs
-    # Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.9" ("f399592")
-    # on crevetete the 31/3/2022 at 17:12:13
+    make: 'ring.cmxs' is up to date.
+    # Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.5.9" ("c9bee55")
+    # on crevetete the 31/5/2022 at 14:17:11
     #sasa ring.dot
     
-    #seed 330200998
+    #seed 273810591
     #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
     
     
     #step 0
-    #outs 0 1 0 1 1 0 0 t f f t t t t f f f t f f t f 6.
+    #outs 0 1 1 1 1 0 0 t t t t t t t f f f t t t f f 10.
     
     #step 1
-    #outs 0 1 0 2 1 0 1 f f f f f f f f f f t f f t t 0.
+    #outs 0 1 1 0 2 2 0 t t t f t t t t f f f t f f f 6.
+    
+    #step 2
+    #outs 2 1 1 0 1 2 0 f t t f f f f f f t f f f f f 2.
     
-    This algo is silent after 2 moves, 1 step, 1 round.
+    #step 3
+    #outs 2 1 2 0 1 2 0 f f f f f f f f f t f f f f t 0.
+    
+    This algo is silent after 6 moves, 3 steps, 1 round.
     
     #quit
 
 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="orga34891c"></a>
+<a id="org6f81e55"></a>
 
 ## Running batch simulations with Built-in daemons
 
@@ -271,7 +276,7 @@ sasa -h | grep "\-daemon"
     --greedy-daemon, -gd
 
 
-<a id="orgdc4e901"></a>
+<a id="org4c63674"></a>
 
 ## Running batch simulations with manual (a.k.a. custom) daemons
 
@@ -309,7 +314,7 @@ In order to enter such input more easily, one can use (requires [the lustre V4 t
 Daemons can also by simulated by [`lutin`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-4) programs via the use of [`lurette`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-9) (for batch executions) or [`rdbg`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-10) (for interactive sessions).
 
 
-<a id="org78885ec"></a>
+<a id="orgd2bc290"></a>
 
 ## Running batch simulations with `lurette`
 
@@ -334,14 +339,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="org2753f29"></a>
+<a id="org2b0799e"></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="orge6e4643"></a>
+<a id="org3b8d4b3"></a>
 
 ## The `sasa` CLI
 
@@ -352,6 +357,9 @@ For more information on this topic: <https://verimag.gricad-pages.univ-grenoble-
     usage: sasa [<option>]* <topology>.dot 
     use -h to see the available options.
     
+    --length, -l <int>
+                Maximum number of steps to be done (10000 by default).
+    
     --synchronous-daemon, -sd
                 Use a Synchronous daemon
     --central-daemon, -cd
@@ -364,29 +372,36 @@ For more information on this topic: <https://verimag.gricad-pages.univ-grenoble-
                 This is the default daemon.
     --custom-daemon, -custd
                 Use a Custom daemon (forces --rif)
-    --greedy-central-daemon, -gcd
-                Use the central daemon that maximizes the potential function
-                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) 
-    --init-search, -is <int>
+                Use the daemon that maximizes the potential function at each step.
+                Performs 2^|enabled| trials (per step). 
+    --greedy-central-daemon, -gcd
+                Ditto, but restricted to central daemons. Performs |enabled| trials.
+    --exhaustive-daemon, -ed
+                Use the daemon that maximizes the number of steps. 
+                The search is stopped when the maximum number of steps has been reached 
+                (which is controlled by the -l/--length option)
+    --exhaustive-central-daemon, -ecd
+                Ditto, but for central daemons
+    --local-init-search, -is <int>
                 Use local search algorithms to find an initial configuration that pessimize 
                 the step number. The argument is the maximum number of trials to do the search. 
                 Require the state_to_nums Algo.to_register field to be defined.
+    --global-init-search, -gis <int>
+                Use global (i.e., completely random)  search to find an initial configuration 
+                that pessimize the step number. The argument is the maximum number of trials
+                 to do the search. 
     --cores-nb, -cn
-                Number of cores to use during the simulation (default is 1)
+                Number of cores to use during --init-search simulations (default is 1)
+    --outfile, -o
+                Generate simulation data in a file (use stdout otherwise)
     --seed, -seed <int>
                 Set the pseudo-random generator seed of build-in daemons (wins over --replay)
     --replay, -replay
                 Use the last generated seed to replay the last run
-    --gen-register, -reg
-                Generates the registering file and exit. 
-    --length, -l <int>
-                Maximum number of steps to be done (10000 by default).
-    
     --version, -version, -v
                 Display the sasa version and exit.
+    --quiet, -q Set the quiet mode
     --verbose, -vl <int>
                 Set the verbose level
     --help, -help, -h
@@ -399,15 +414,17 @@ More `sasa` options:
   sasa --more
 ```
 
-    --rif, -rif Display only outputs on stdout (i.e., behave as a rif input file)
+    --rif, -rif Print only outputs (i.e., behave as a rif input file)
     --no-data-file, -nd
-                Do not generate any data file
+                Do not print any data
     --gen-lutin-daemon, -gld
-                Generate Lutin daemons and exit
+                Generate Lutin daemons and exit (not finished)
     --gen-lustre-oracle-skeleton, -glos
                 Generate a Lustre oracle skeleton
     --list-algos, -algo
                 Output the algo files used in the dot file and exit. 
+    --gen-register, -reg
+                Generates the registering files and exit. 
     --dummy-input
                 Add a dummy input to sasa so that built-in daemon can be used from rdbg
     --ignore-first-inputs, -ifi
@@ -416,11 +433,11 @@ More `sasa` options:
                 Display the version ocaml version sasa was compiled with and exit.
 
 
-<a id="org3a02f22"></a>
+<a id="org02bafa4"></a>
 
 # Interactive mode
 
-<a id="org13e182c"></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="org4f9a5e3"></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.
 
@@ -429,7 +446,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="org0c64c8e"></a>
+<a id="orgd499f7a"></a>
 
 ## Example: use `rdbg` from the `test/alea-coloring/` directory
 
@@ -472,7 +489,7 @@ rdbg
      [q] quit
 
 
-<a id="org7332823"></a>
+<a id="org75ae70f"></a>
 
 ## The examples of test directory
 
@@ -483,7 +500,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="org8c4ba7c"></a>
+<a id="orge4643af"></a>
 
 ## Running interactive sessions with `rdbg`
 
@@ -500,7 +517,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="orgd2dfbbd"></a>
+<a id="org30c51b6"></a>
 
 ## Getting `rdbg` on-line help
 
@@ -596,7 +613,7 @@ Here are 2 useful entry-points to rdbg on-line help:
     (rdbg) 
 
 
-<a id="org7914fd6"></a>
+<a id="org2b4589f"></a>
 
 ## A `rdbg`  `sasa` GUI
 
@@ -610,7 +627,7 @@ opam install -y rdbgui4ocaml
 To use it: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/>
 
 
-<a id="orgf6b0394"></a>
+<a id="orgd3bfce6"></a>
 
 ## Useful Modules
 
@@ -645,14 +662,14 @@ Some modules, used by the sasa core engine, can be useful from `rdbg`.
 </iframe>
 
 
-<a id="orgc3e7487"></a>
+<a id="orgead66ac"></a>
 
 # Install
 
-<a id="org5e646e7"></a> <a id="org6818f71"></a>
+<a id="org6e26471"></a> <a id="org5302c2f"></a>
 
 
-<a id="org70cd209"></a>
+<a id="orgb390429"></a>
 
 ## TL;DR
 
@@ -706,7 +723,7 @@ git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.gi
 ```
 
 
-<a id="org2db11de"></a>
+<a id="orgb4cc09a"></a>
 
 ## Not strictly mandatory, but useful, third-party software
 
@@ -749,7 +766,7 @@ sudo apt install -y wish
 Otherwise: <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html>
 
 
-<a id="org6475b9d"></a>
+<a id="org8290be6"></a>
 
 ## Install `sasa` via opam (version >= 2.\*)
 
@@ -783,7 +800,7 @@ opam upgrade
 ```
 
 
-<a id="org191f6ee"></a>
+<a id="orgb63c57e"></a>
 
 ## Install `sasa` via `git`
 
@@ -827,24 +844,24 @@ 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="orga9494d0"></a>
+<a id="org13c72f7"></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="org6282d99"></a>
+<a id="orgaf70033"></a>
 
 ## Use `sasa` via a Virtual Machine
 
-<https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/sasaVM.ova>
+<http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/sasaVM.ova>
 
 -   login:sasa
 -   passwd:sasa
 
 
-<a id="orge3d9e56"></a>
+<a id="org52c7a2d"></a>
 
 # Screencasts
 
@@ -860,7 +877,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="org686b3ba"></a>
+<a id="org4d55fa9"></a>
 
 # More
 
@@ -869,12 +886,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="orgd95151e"></a>
+<a id="orge446f5a"></a>
 
 # FAQ
 
 
-<a id="org8853048"></a>
+<a id="org1788b9d"></a>
 
 ## Is there a FAQ?
 
@@ -883,7 +900,7 @@ Yes.
 Beside, some tutorials are also available here: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/>
 
 
-<a id="orgbbdf456"></a>
+<a id="org2ea9013"></a>
 
 ## I have a compilation error that I don't understand
 
@@ -893,7 +910,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="orga5a86c6"></a>
+<a id="orga4555a7"></a>
 
 ## I have the error `Invalid_argument("compare: functional value")`
 
diff --git a/guides/users/README.org b/guides/users/README.org
index c859d7c27e26b7279c398af2dd464245a91b325f..7797f7e806e44c89ed5a048eec669ec57ceb1ab9 100644
--- a/guides/users/README.org
+++ b/guides/users/README.org
@@ -955,7 +955,7 @@ This docker image   contains all the tools mentioned in this section
 
 ** Use =sasa= via a Virtual Machine
 
-https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/sasaVM.ova
+http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/sasaVM.ova
 
 - login:sasa
 - passwd:sasa