From 6b6f4c8ba322be79db8b9708567fc8cc89aa175e Mon Sep 17 00:00:00 2001 From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr> Date: Thu, 14 Nov 2019 10:12:34 +0100 Subject: [PATCH] Doc: more work on the user guide --- .gitlab-ci.yml | 3 + guides/users/README.md | 222 ++++++++++++++++++++-------------------- guides/users/README.org | 190 +++++++++++++++------------------- lib/sasacore/sasArg.ml | 4 +- lib/sasacore/sasArg.mli | 3 +- test/my-rdbg-tuning.ml | 151 +++++++++++++++++++++++---- 6 files changed, 334 insertions(+), 239 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d934b343..da771a33 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -39,6 +39,9 @@ pages: - cp README.html ../../public/index.html - cp -rf _html ../../public/ - cp -rf ../styles/ ../../public/ + - cp -rf sasabatch.pdf ../../public/ + - cp -rf sasabatch.png ../../public/ + artifacts: paths: - public diff --git a/guides/users/README.md b/guides/users/README.md index 788339b5..705e47e7 100644 --- a/guides/users/README.md +++ b/guides/users/README.md @@ -1,30 +1,54 @@ +- [TL;DR](#orgb04ef81) +- [Topology](#org625496d) +- [Algorithms](#orgdd85378) +- [Examples](#org27c5f11) +- [Batch mode](#org4911fe9) + - [Running batch simulations with Built-in demons](#org0580268) + - [Running batch simulations with manual demons](#org209a068) + - [Running batch simulations with `lurette`](#orga146cf8) + - [Viewing Results](#org76b8df4) + - [The `sasa` CLI](#org98e3d73) +- [Interactive mode](#org4bf7506) + - [Example: use `rdbg` from the `test/alea-coloring/` directory](#org92a585e) + - [The exemples of test directory](#org5211b7a) + - [Running interactive sessions with `rdbg`](#org80def3d) + - [Getting `rdbg` on-line help](#orgd690b38) +- [Install](#org1943c0a) + - [Via opam 2 (prefered method)](#org89c9e4a) + - [Via docker](#orgfb3abc7) + - [From source](#orgeb5f506) +- [More](#org0602034) +- [FAQ](#org1c5f5bc) + - [Is there a FAQ?](#org643d3a6) + + # Table of Contents -1. [TL;DR](#orgb45de04) -2. [Topology](#org44917a9) -3. [Algorithms](#orgd29bb7c) -4. [Examples](#org64494a4) -5. [Batch mode](#org013085e) - 1. [Running batch simulations with Built-in demons](#org5474a3d) - 2. [Running batch simulations with manual demons](#org28a5404) - 3. [Running batch simulations with `lurette`](#org38bc20c) - 4. [Viewing Results](#org09c40f5) - 5. [The `sasa` CLI](#orga1fe1b8) -6. [Interactive mode](#orga30d18c) - 1. [Running interactive sessions with `rdbg`](#orgfbf8e46) - 2. [Example: use `rdbg` from the `test/alea-coloring/` directory](#orgd02acd8) - 3. [Getting `rdbg` on-line help](#org9abe8a8) - 4. [How `rdbg` interacts with the `ocaml` REPL](#orgbcdd35a) -7. [Install](#orgcf6f501) - 1. [Via opam 2 (prefered method)](#org03438b7) - 2. [Via docker](#org2d2a61a) - 3. [From source](#orgd246fe1) -8. [More](#org8b4cf8e) -9. [FAQ](#orgf7c8932) - 1. [Is there a FAQ?](#org78cc516) - - -<a id="orgb45de04"></a> +1. [TL;DR](#orgb04ef81) +2. [Topology](#org625496d) +3. [Algorithms](#orgdd85378) +4. [Examples](#org27c5f11) +5. [Batch mode](#org4911fe9) + 1. [Running batch simulations with Built-in demons](#org0580268) + 2. [Running batch simulations with manual demons](#org209a068) + 3. [Running batch simulations with `lurette`](#orga146cf8) + 4. [Viewing Results](#org76b8df4) + 5. [The `sasa` CLI](#org98e3d73) +6. [Interactive mode](#org4bf7506) + 1. [Example: use `rdbg` from the `test/alea-coloring/` directory](#org92a585e) + 2. [The exemples of test directory](#org5211b7a) + 3. [Running interactive sessions with `rdbg`](#org80def3d) + 4. [Getting `rdbg` on-line help](#orgd690b38) +7. [Install](#org1943c0a) + 1. [Via opam 2 (prefered method)](#org89c9e4a) + 2. [Via docker](#orgfb3abc7) + 3. [From source](#orgeb5f506) +8. [More](#org0602034) +9. [FAQ](#org1c5f5bc) + 1. [Is there a FAQ?](#org643d3a6) + + +<a id="orgb04ef81"></a> # TL;DR @@ -45,14 +69,12 @@ make ring.cmxs sasa ring.dot ``` - - -<./sasabatch.pdf> + The source code is available at <https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa> -<a id="org44917a9"></a> +<a id="org625496d"></a> # Topology @@ -115,7 +137,7 @@ Such parameters can be retreived in Algorithms using the `Algo.get_graph_attribu nb: a `Algo.diameter: unit -> int` function is provided, but it can be expensive to use. -<a id="orgd29bb7c"></a> +<a id="orgdd85378"></a> # Algorithms @@ -127,7 +149,7 @@ The following has been generated from [algo.mli](https://gricad-gitlab.univ-gren </div> -<a id="org64494a4"></a> +<a id="org27c5f11"></a> # Examples @@ -155,18 +177,18 @@ 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` (it it exists). -<a id="org013085e"></a> +<a id="org4911fe9"></a> # Batch mode -<a id="org5474a3d"></a> +<a id="org0580268"></a> ## Running batch simulations with Built-in demons To launch batch simulations, one can use the `sasa` Command Line Interface. -For instance, in order to simulate an algorithm defined in the `ring.dot` (cf <../../test/coloring>), you can launch the following command: +For instance, in order to simulate an algorithm defined in the `ring.dot` (cf [test/coloring](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/coloring), you can launch the following command: ```sh sasa ring.dot @@ -185,7 +207,7 @@ sasa -h | grep "\-demon" --custom-demon, -custd -<a id="org28a5404"></a> +<a id="org209a068"></a> ## Running batch simulations with manual demons @@ -212,11 +234,11 @@ 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. -<a id="org38bc20c"></a> +<a id="orga146cf8"></a> ## Running batch simulations with `lurette` -If you want to perform simulations with custom demons, you need to use `lurette`. For instance, in order to simulate an algorithm defined in the `ring.dot` (cf <../../test/coloring>) using a Lutin demon defined in `ring.lut`, you can launch the following command: +If you want to perform simulations with custom demons, you need to use `lurette`. For instance, in order to simulate an algorithm defined in the `ring.dot` (cf [test/coloring](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/coloring)) using a Lutin demon defined in `ring.lut`, you can launch the following command: ```sh lurette \ @@ -235,14 +257,14 @@ lurette \ ``` -<a id="org09c40f5"></a> +<a id="org76b8df4"></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="orga1fe1b8"></a> +<a id="org98e3d73"></a> ## The `sasa` CLI @@ -305,43 +327,20 @@ sasa --more Display the version ocaml version sasa was compiled with and exit. -<a id="orga30d18c"></a> +<a id="org4bf7506"></a> # Interactive mode -If you want to perform interactive session, you can launch `sasa` under the control of `rdbg`. +If you want to perform interactive session, you can launch `sasa` under the control of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/). 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#Level0). -The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test) directory contains several files and directories that take advantage of the versatility (programmability) of `rdbg` to perform interactive `sasa` simulations: -- `test/rdbg-utils/`: contains `ocaml` functions that can be used from `rdbg` -- `test/my-rdbg-tuning.ml`: contains useful shortcuts/commands that can be used from `rdbg`. -- `test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (it it exists). - - -<a id="orgfbf8e46"></a> - -## Running interactive sessions with `rdbg` - -1. type `rdbg` -2. press enter to load the defaut session (`rdbg-session.ml`). Then you can type: -3. `d` for displaying a (dynamic) dot graph with `dot` -4. or ALTERNATIVELY `ne` to use the `neato` layout engine (`tw`, `ci`, `fd`, `sf`, `pa`, `os` to use the `twopi`, `circo`, `fdp`, `sfd`, `patchwork`, `osage` layout engines respectively) -5. `s` to move one step forward -6. `sd` to move one step forward and call `d` (to update the graph display []) -7. `nr` to move one round forward -8. `pr` to move one round backward -9. `go` to move forward until convergence - -All those commands are defined in (the common) [../../test/my-rdbg-tuning.ml](../../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="orgd02acd8"></a> +<a id="org92a585e"></a> ## Example: use `rdbg` from the `test/alea-coloring/` directory All the sub-directories of the `test` directory are organized similarly. Let's have a look at the `test/alea-coloring/` directory. It contains the following files: -- `my-rdbg-tuning.ml` that just includes [../../test/my-rdbg-tuning.ml](../../test/my-rdbg-tuning.ml) (some `my-rdbg-tuning.ml` files define more commands, such as the one in [../../test/async-unison](../../test/async-unison/my-rdbg-tuning.ml)). +- `my-rdbg-tuning.ml` that just includes [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml) (some `my-rdbg-tuning.ml` files define more commands, such as the one in [test/async-unison/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/async-unison/my-rdbg-tuning.ml)). - `ring.dot`: a possible topology - `p.ml`: an algorithm used in `ring.dot` - `Makefile`: a Makefile that demonstrates various ways of using `sasa`. In particular, it contains a rule named `rdbg`. @@ -356,85 +355,88 @@ make rdbg This make rule (defined in `Makefile` and `../Makefile.inc`) 1. generates the `ring.ml` file, that contains the registration code (that can indeed be generated by sasa, as explained in `algo.mli`). -2. launches `rdbg` with some arguments. `rdbg` then prompts the user to enter one of the folling commands: `c`, `q`, `s`: +2. launches `rdbg` with some arguments. `rdbg` then prompts the user to enter one of the folling commands: ```sh rdbg -o ring.rif -sut "$(sasa) ring.dot --locally-central-demon" -[c] create a fresh session +[] create a fresh session [q] quit [s] do nothing -[c/q/s]: +[/q/s]: ``` -By default, the first in the list (here `c`) is executed if you press `[Return]` without any command. +By default, the first in the list is executed; hence if you press `[Return]` without any command, a fresh session is created. More precisely it creates a `rdbg_session.ml` file, that loads all the necessary modules to run an interactive session with `rdbg`, where `rdbg` simulates ring.dot with `sasa` using a locally distributed daemon. -Hence, let's create a fresh session by typing `c` and then `[Return]` (or just `[Return]`). This will result in the creation of the `rdbg_session.ml` file, that loads all the necessary modules to run an interactive session with `rdbg`, where `rdbg` simulates ring.dot with `sasa` using a locally distributed daemon. +For instance, you can type `nr[return]`, a `rdbg` command defined in [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml) that steps until the next round is reached. Then, by typing `[return]`; `rdbg` will run the lastly used command, which is `nr`, which allow you to move forward in the execution from rounds to rounds. If you want to go backwards to the previous round, you can use the `br` command=, also defined in [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml). -For instance, you can type `nr [return]`, a `rdbg` command defined in [../../test/my-rdbg-tuning.ml](../../test/my-rdbg-tuning.ml) that steps until the next round is reached. Then, by typing `[return]`; `rdbg` will run the lastly used command, which is `nr`, which allow you to move forward in the execution from rounds to rounds. If you want to go backwards to the previous round, you can use the `br` command=, also defined in [../../test/my-rdbg-tuning.ml](../../test/my-rdbg-tuning.ml). - -nb: the next time rdbg is launched (without argument), you will be prompted with the possibility to reuse this session. +nb: the next time `rdbg` is launched (without argument), you will be prompted with the possibility to reuse this session. ```sh -rdbg +$ rdbg -[0] #use "rdbg-session.ml" +[] #use "rdbg-session.ml" [c] create a fresh session [q] quit [s] do nothing -[0/s/q/c/1/2/...]: +[/c/q/s]: ``` -Typing `0` will therefore also load the `rdbg_session.ml` file we have just been using. +Typing `[Enter]` will therefore also load the `rdbg_session.ml` file we have just been using. -<a id="org9abe8a8"></a> +<a id="org5211b7a"></a> -## Getting `rdbg` on-line help +## The exemples of test directory -Here are 2 useful entry-points to rdbg on-line help: +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: -1. `rdbg --help` and -2. at the `rdbg` prompt, the `help` and the `apropos` commands. +- `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). -Try the following (without leading space!): -```ocaml -help "apropos" -apropos "" -help "back" -``` +<a id="org80def3d"></a> +## Running interactive sessions with `rdbg` -<a id="orgbcdd35a"></a> +1. type `rdbg` +2. press enter to load the defaut session (`rdbg-session.ml`). Then you can type: +3. `d` for displaying a (dynamic) dot graph with `dot` +4. or ALTERNATIVELY `ne` to use the `neato` layout engine (`tw`, `ci`, `fd`, `sf`, `pa`, `os` to use the `twopi`, `circo`, `fdp`, `sfd`, `patchwork`, `osage` layout engines respectively) +5. `s` to move one step forward +6. `sd` to move one step forward and call `d` (to update the graph display []) +7. `nr` to move one round forward +8. `pr` to move one round backward +9. `go` to move forward until convergence -## How `rdbg` interacts with the `ocaml` REPL +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`! -Note that `rdbg` actually sends everything you type to an `ocaml` toplevel REPL, trying to guess when to add boring `()` and `;;` and the end of your `rdbg` phrase (a `rdbg` phrase is any string you type at the `rdbg` prompt until you press the [Return] key). Hence, when you type at the `rdbg` prompt: -- `help "apropos"[Return]` it sends to the ocaml REPL the string `help "apropos";;`, which calls the `help` (pre-loaded) function with the "apropos" string argument. -- `n[Return]` it sends `n();;` to the ocaml REPL (which will do something iff the function `n` is defined and takes `()` (unit) as argument). +<a id="orgd690b38"></a> -If you want to be sure that `rdbg` does not add anything to the phrases you type, or if your want to write a function on several lines, just add a leading blank: +## Getting `rdbg` on-line help -- `​ let my_n () = n ();;` sends `let my_n () = n ();;` +Here are 2 useful entry-points to rdbg on-line help: -but if you type +1. `rdbg --help` and +2. at the `rdbg` prompt, you can use the `l` command: -- `​ n[Return]` it sends `n` and nothing happen as ocaml waits for `;;`; so if then you type -- `;;[Return]` it sends `;;`, which returns the type of `n`, but without actually calling `n` as no `()` has been provided. +```sh +(rdbg) l +``` -In different words `n[Return]` has the same effect as `​ n();;[Return]` + 4c888b8d9782b6e04cba18132c41bb56 -<a id="orgcf6f501"></a> +<a id="org1943c0a"></a> # Install -<a id="org03438b7"></a> +<a id="org89c9e4a"></a> ## Via opam 2 (prefered method) @@ -459,14 +461,14 @@ opam install -y rdbg lutin ``` -<a id="org2d2a61a"></a> +<a id="orgfb3abc7"></a> ## Via docker -cf the Install section of <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/> +cf the Install section of [Synchrone Reactive Tool Box](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6). -<a id="orgd246fe1"></a> +<a id="orgeb5f506"></a> ## From source @@ -479,10 +481,10 @@ You will need: - `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). +One can mimick 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="org8b4cf8e"></a> +<a id="org0602034"></a> # More @@ -490,13 +492,13 @@ One can mimick the content of the `test` job in the project [Gitlab CI script](h - Sources: <https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa> -<a id="orgf7c8932"></a> +<a id="org1c5f5bc"></a> # FAQ -<a id="org78cc516"></a> +<a id="org643d3a6"></a> ## Is there a FAQ? -yes \ No newline at end of file +yes diff --git a/guides/users/README.org b/guides/users/README.org index fdc7fdfa..df9db2ef 100644 --- a/guides/users/README.org +++ b/guides/users/README.org @@ -3,16 +3,18 @@ #+TOC: headlines 2 #+LANGUAGE: en #+OPTIONS: H:3 \n:nil @:t ::t |:t ^:t -:t f:t *:t TeX:t LaTeX:nil skip:nil tags:not-in-toc -#+LINK_UP:http://www-verimag.imag.fr/ -#+LINK_HOME:http://www-verimag.imag.fr/ -#+OPTIONS: toc:nil +#+LINK_UP:https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa +#+LINK_HOME:http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6 +#+HTML_HEAD:https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/ +#+OPTIONS: toc:t #+TOC: listings #+TOC: tables #+EMAIL: erwan.jahier@univ-grenoble-alpes.fr #+AUTHOR: Erwan Jahier #+TITLE: SASA: a SimulAtor of Self-stabilizing Algorithms - +#+LINK: sasa https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/%s + * TL;DR SASA is a *Self-stabilizing Algorithms SimulAtor*, based on the @@ -34,9 +36,8 @@ make ring.cmxs sasa ring.dot #+END_SRC -[[file:sasabatch.png]] - -[[./sasabatch.pdf]] +#+attr_html: :width 700px +[[./sasabatch.svg]] The source code is available at https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa @@ -130,7 +131,8 @@ The following has been generated from [[https://gricad-gitlab.univ-grenoble-alpe To launch batch simulations, one can use the =sasa= Command Line Interface. For instance, in order to simulate an algorithm defined in the -=ring.dot= (cf [[file:../../test/coloring]]), you can launch the following +=ring.dot= + (cf [[sasa:test/coloring][test/coloring]], you can launch the following command: #+BEGIN_SRC sh @@ -201,7 +203,7 @@ demon. If you want to perform simulations with custom demons, you need to use =lurette=. For instance, in order to simulate an algorithm defined -in the =ring.dot= (cf [[file:../../test/coloring]]) using a Lutin demon defined +in the =ring.dot= (cf [[sasa:test/coloring][test/coloring]]) using a Lutin demon defined in =ring.lut=, you can launch the following command: #+BEGIN_SRC sh @@ -288,48 +290,10 @@ More =sasa= options: * Interactive mode -If you want to perform interactive session, you can launch =sasa= -under the control of =rdbg=. - - -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: - - -- =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= - -1. type =rdbg= -2. press enter to load the defaut session (=rdbg-session.ml=). - Then you can type: -3. =d= for displaying a (dynamic) dot graph with =dot= -4. or ALTERNATIVELY =ne= to use the =neato= layout engine (=tw=, =ci=, - =fd=, =sf=, =pa=, =os= to use the =twopi=, =circo=, =fdp=, =sfd=, - =patchwork=, =osage= layout engines respectively) -5. =s= to move one step forward -6. =sd= to move one step forward and call =d= (to update the graph - display []) -7. =nr= to move one round forward -8. =pr= to move one round backward -9. =go= to move forward until convergence +If you want to perform interactive session, you can launch =sasa= +under the control of [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/][rdbg]]. Before reading this section, please read +at least the [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/README.html#Level0][Basic usage Section if the rdbg documentation]]. -All those commands are defined in (the common) -[[file:../../test/my-rdbg-tuning.ml][../../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=! ** Example: use =rdbg= from the =test/alea-coloring/= directory @@ -337,8 +301,8 @@ All the sub-directories of the =test= directory are organized similarly. Let's have a look at the =test/alea-coloring/= directory. It contains the following files: - =my-rdbg-tuning.ml= that just includes - [[file:../../test/my-rdbg-tuning.ml][../../test/my-rdbg-tuning.ml]] (some =my-rdbg-tuning.ml= files define more - commands, such as the one in [[file:../../test/async-unison/my-rdbg-tuning.ml][../../test/async-unison]]). + [[sasa:test/my-rdbg-tuning.ml][test/my-rdbg-tuning.ml]] (some =my-rdbg-tuning.ml= files define more + commands, such as the one in [[sasa:test/async-unison/my-rdbg-tuning.ml][test/async-unison/my-rdbg-tuning.ml]]). - =ring.dot=: a possible topology - =p.ml=: an algorithm used in =ring.dot= - =Makefile=: a Makefile that demonstrates various ways of using @@ -354,95 +318,108 @@ This make rule (defined in =Makefile= and =../Makefile.inc=) 1. generates the =ring.ml= file, that contains the registration code (that can indeed be generated by sasa, as explained in =algo.mli=). 2. launches =rdbg= with some arguments. =rdbg= then prompts the user to - enter one of the folling commands: =c=, =q=, =s=: + enter one of the folling commands: #+BEGIN_SRC sh rdbg -o ring.rif -sut "$(sasa) ring.dot --locally-central-demon" -[c] create a fresh session +[] create a fresh session [q] quit [s] do nothing -[c/q/s]: +[/q/s]: #+END_SRC -By default, the first in the list (here =c=) is executed if you press -=[Return]= without any command. +By default, the first in the list is executed; hence if you press +=[Return]= without any command, a fresh session is created. More precisely +it creates a =rdbg_session.ml= file, that loads all +the necessary modules to run an interactive session with =rdbg=, +where =rdbg= simulates ring.dot with =sasa= using a locally +distributed daemon. -Hence, let's create a fresh session by typing =c= and then =[Return]= -(or just =[Return]=). This will result in the creation of the -=rdbg_session.ml= file, that loads all the necessary modules to run an -interactive session with =rdbg=, where =rdbg= simulates ring.dot with -=sasa= using a locally distributed daemon. - -For instance, you can type =nr [return]=, a =rdbg= command defined in - [[file:../../test/my-rdbg-tuning.ml][../../test/my-rdbg-tuning.ml]] that steps until the next round is +For instance, you can type =nr[return]=, a =rdbg= command defined in + [[sasa:test/my-rdbg-tuning.ml][test/my-rdbg-tuning.ml]] that steps until the next round is reached. Then, by typing =[return]=; =rdbg= will run the lastly used command, which is =nr=, which allow you to move forward in the execution from rounds to rounds. If you want to go backwards to the previous round, you can use the =br= command=, also defined in - [[file:../../test/my-rdbg-tuning.ml][../../test/my-rdbg-tuning.ml]]. + [[sasa:test/my-rdbg-tuning.ml][test/my-rdbg-tuning.ml]]. -nb: the next time rdbg is launched (without argument), you will +nb: the next time =rdbg= is launched (without argument), you will be prompted with the possibility to reuse this session. #+BEGIN_SRC sh -rdbg +$ rdbg -[0] #use "rdbg-session.ml" +[] #use "rdbg-session.ml" [c] create a fresh session [q] quit [s] do nothing -[0/s/q/c/1/2/...]: +[/c/q/s]: #+END_SRC -Typing =0= will therefore also load the =rdbg_session.ml= file we have +Typing =[Enter]= will therefore also load the =rdbg_session.ml= file we have just been using. -** Getting =rdbg= on-line help +** The exemples of test directory -Here are 2 useful entry-points to rdbg on-line help: -1. =rdbg --help= and -2. at the =rdbg= prompt, the =help= and the =apropos= commands. +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: + + +- =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). -Try the following (without leading space!): -#+BEGIN_SRC ocaml -help "apropos" -apropos "" -help "back" -#+END_SRC +** Running interactive sessions with =rdbg= + +1. type =rdbg= +2. press enter to load the defaut session (=rdbg-session.ml=). + Then you can type: +3. =d= for displaying a (dynamic) dot graph with =dot= +4. or ALTERNATIVELY =ne= to use the =neato= layout engine (=tw=, =ci=, + =fd=, =sf=, =pa=, =os= to use the =twopi=, =circo=, =fdp=, =sfd=, + =patchwork=, =osage= layout engines respectively) +5. =s= to move one step forward +6. =sd= to move one step forward and call =d= (to update the graph + display []) +7. =nr= to move one round forward +8. =pr= to move one round backward +9. =go= to move forward until convergence -** How =rdbg= interacts with the =ocaml= REPL +All those commands are defined in (the common) +[[sasa:test/my-rdbg-tuning.ml][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=! +** Getting =rdbg= on-line help -Note that =rdbg= actually sends everything you type to an =ocaml= -toplevel REPL, trying to guess when to add boring =()= and =;;= and -the end of your =rdbg= phrase (a =rdbg= phrase is any string you type -at the =rdbg= prompt until you press the [Return] key). Hence, when -you type at the =rdbg= prompt: +Here are 2 useful entry-points to rdbg on-line help: +1. =rdbg --help= and +2. at the =rdbg= prompt, you can use the =l= command: -- =help "apropos"[Return]= it sends to the ocaml REPL the string =help - "apropos";;=, which calls the =help= (pre-loaded) function with the - "apropos" string argument. -- =n[Return]= it sends =n();;= to the ocaml REPL (which will do - something iff the function =n= is defined and takes =()= (unit) as - argument). +#+BEGIN_SRC sh +(rdbg) l +#+END_SRC -If you want to be sure that =rdbg= does not add anything to the phrases -you type, or if your want to write a function on several lines, just -add a leading blank: +#+BEGIN_SRC sh :results output :session :exports results :async +echo "\nl\nq\n" | rdbg | tail -n +21 +#+END_SRC +#+RESULTS: -- =​ let my_n () = n ();;= sends =let my_n () = n ();;= -but if you type -- =​ n[Return]= it sends =n= and nothing happen as ocaml waits for - =;;=; so if then you type -- =;;[Return]= it sends =;;=, which returns the type of =n=, but - without actually calling =n= as no =()= has been provided. -In different words =n[Return]= has the same effect as =​ n();;[Return]= * Install @@ -474,8 +451,7 @@ opam install -y rdbg lutin ** Via docker -cf the Install section of -http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/ +cf the Install section of [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6][Synchrone Reactive Tool Box]]. ** From source @@ -488,8 +464,8 @@ You will need: - =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]]. +One can mimick the content of the =test= job in the project + [[sasa:.gitlab-ci.yml][.gitlab-ci.yml Gitlab CI script]]. * More diff --git a/lib/sasacore/sasArg.ml b/lib/sasacore/sasArg.ml index 635e9def..5e46ed29 100644 --- a/lib/sasacore/sasArg.ml +++ b/lib/sasacore/sasArg.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 23/10/2019 (at 09:51) by Erwan Jahier> *) +(* Time-stamp: <modified the 04/11/2019 (at 10:47) by Erwan Jahier> *) type t = { @@ -8,6 +8,7 @@ type t = { mutable demon: Demon.t; mutable rif: bool; mutable no_data_file: bool; + mutable quiet: bool; mutable seed: int option; mutable replay_seed: bool; mutable ifi: bool; @@ -40,6 +41,7 @@ let (make_args : unit -> t) = demon = Demon.Distributed; rif = false; no_data_file = false; + quiet = false; seed = None; replay_seed = false; ifi = false; diff --git a/lib/sasacore/sasArg.mli b/lib/sasacore/sasArg.mli index f096ef34..eeb560e4 100644 --- a/lib/sasacore/sasArg.mli +++ b/lib/sasacore/sasArg.mli @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 23/10/2019 (at 08:55) by Erwan Jahier> *) +(* Time-stamp: <modified the 06/11/2019 (at 16:24) by Erwan Jahier> *) type t = { mutable topo: string; @@ -7,6 +7,7 @@ type t = { mutable demon: Demon.t; mutable rif: bool; mutable no_data_file: bool; + mutable quiet: bool; mutable seed: int option; mutable replay_seed: bool; mutable ifi: bool; diff --git a/test/my-rdbg-tuning.ml b/test/my-rdbg-tuning.ml index f0c6fea1..fa7e9df8 100644 --- a/test/my-rdbg-tuning.ml +++ b/test/my-rdbg-tuning.ml @@ -1,24 +1,119 @@ (* Some useful short-cuts for rdbg interactive sessions *) + (* you need to install the emacs highligth package available in melpa *) +let hl hook (file, line, charb, chare) = + let cmd = Printf.sprintf "emacsclient -e '(save-selected-window (find-file-other-window \"%s\") %s (goto-char (point-min)) (forward-line %i) (forward-char %i) (set-mark-command nil) (forward-char %i) (hlt-highlight-region) )' " + file hook (line-1) charb (max 1 (chare-charb)) + in + ignore(Sys.command cmd) + +let hl_atoms = function + | []-> () + | x::t -> hl "(hlt-unhighlight-region)" x; List.iter (hl "") t +(*| x::t -> hl "(hlt-unhighlight-all-prop t)" x; List.iter (hl "") t *) + +let _ = + let cmd = "emacsclient -e ' (hlt-choose-default-face \"org-checkbox\") '" in + ignore(Sys.command cmd) -let _ = time_travel true;; +let emacs = ref false -(* Shortcuts for moving around *) +let emacs_udate e = + if !emacs then + try + match e.sinfo with + | None -> () + | Some si -> + let si_list = + List.map + (fun si -> (si.file, fst si.line, fst si.char, snd si.char)) + (si()).atoms + in + hl_atoms si_list + with + Match_failure _ -> () + +let _ = time_travel true;; let e = ref (RdbgStdLib.run());; -let s () = e:=step !e;; -let si i = e:=stepi !e i;; -let n () = e:=next !e ;; -let ni i = e:= nexti !e i;; -let g i = e:= goto !e i;; -let b () = e:= back !e ;; -let bi i = e:= backi !e i;; -let r () = !e.Event.reset(); e:= RdbgStdLib.run();; -let c () = e:= continue !e;; +let s () = e:=step !e; ignore(emacs_udate !e);; +let si i = e:=stepi !e i; ignore(emacs_udate !e);; +let n () = e:=next !e; ignore(emacs_udate !e);; +let ni i = e:= nexti !e i;emacs_udate !e;; +let g i = e:= goto !e i;emacs_udate !e;; +let b () = e:= back !e ;emacs_udate !e;; +let bi i = e:= backi !e i;emacs_udate !e;; +let r () = !e.Event.reset(); e:=RdbgStdLib.run();emacs_udate !e;; +let c () = e:= continue !e;emacs_udate !e;; +let cb () = e:= rev !e;emacs_udate !e;; +(**********************************************************************) +open Callgraph;; +let cgf () = gen_call_graph_full !e;; +let cg () = (gen_call_graph !e);; +let dcg ()= ignore(display_call_graph ());; let bt () = print_src !e;; let finish () = loopforever !e;; +let where () = print_call_stack !e;; + +(**********************************************************************) +(* breakpoints *) + +let blist () = !breakpoints;; (**********************************************************************) +(* Goto to the next event which name contains a string (useful for + navigating inside lustre or lutin programs) *) +let nm str = e:= next_match !e str ;; +let pm str = e:=previous_match !e str ;; + +(**********************************************************************) +(* Online Level 0 doc *) + +let l () = print_string " +Here is the list of rdbg Level 0 commands: +- forward moves: + n: move forward of one event + ni i: move forward of i events + s: move forward of one step + si i: move forward of n steps + nm <string>: move forward until a function which name matches a <string> + +- backward moves: + b: move backward of one event + bi i: move backward of i events + pm <string>: move backward until a function which name matches a <string> + g i: go to event number i + +- Call graphs (requires GraphViz dot, and works from Lustre node only) + cg: generate the call graph (one level) + cgf: generate the full call graph (i.e., node are clickable) + dcg: display the generated call graph + +- Breakpoints: + break <brpt>: add a breakpoint + where <brpt> is a string of the form: + \"node\" + \"node@line\" + \"file\" + \"file@line\" + c: continue forward until the next breakpoint + cb: ditto backwards + blist: list of the current breakpoints + delete: empty the list of the current breakpoints + +- misc: + where: print the call stack with source information + +- main: + l: print this list of L0 commands + i: print information relative to the current session parameters + r: restart + q: quit rdbg +";; + +(**********************************************************************) +(**********************************************************************) + #mod_use "../../lib/algo/algo.ml";; #mod_use "../../lib/sasacore/register.ml";; #mod_use "../../lib/sasacore/topology.ml";; @@ -119,7 +214,7 @@ let pr () = e:=goto_last_ckpt !e.nb; !dot_view ();; (* Goto to the next oracle violation *) let goto_next_false_oracle e = next_cond e (fun e -> e.kind = Exit && e.lang = "lustre" && - e.outputs = [("ok", Bool)] && + List.mem ("ok", Bool) e.outputs && not (vb "ok" e)) let viol () = e:=goto_next_false_oracle !e @@ -129,15 +224,31 @@ let viol () = e:=goto_next_false_oracle !e let _ = check_ref := round;; (**********************************************************************) -(* Goto to the next event which name contains a string (useful for - navigating inside lustre or lutin programs) *) -let next_match str e = - next_cond e (fun e -> Str.string_match (Str.regexp_string str) e.name 0) -let nm str = e:= next_match str !e ;; -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 l () = + l(); + print_string " +- sasa commands + + Display network with GraphViz tools + d: display the current network with dot + ne: display the current network with neato + tw: display the current network with twopi + ci: display the current network with circo + fd: display the current network with fdp + sf: display the current network with sfdp + pa: display the current network with patchwork + os: display the current network with osage + + Moving commands + sd: go to the next step and display the network with one of the GraphViz tools (*) + nd: go to the next event and display the network + bd: go to the previous event and display the network + rd: go to the next round and display the network + pd: go to the previous round and display the network +(*) In order to change the current graph drawing engine, you can use +the dot_view command as follows: + dot_view := ci + +" (**********************************************************************) (* ok, let's start the debugging session! *) -- GitLab