From 2d00b8311a59af10cc3d70bfb0e0e1c36fc7c8d0 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Mon, 5 Sep 2022 15:55:35 +0200
Subject: [PATCH] doc: add exemples of use of salut

---
 salut/README.md | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/salut/README.md b/salut/README.md
index 3e153030..e3759b40 100644
--- a/salut/README.md
+++ b/salut/README.md
@@ -5,11 +5,11 @@
 It is dedicated to the [Simulation and Formal Verification of Self-stabilizing Algorithms](https://ensiwiki.ensimag.fr/index.php?title=IRL_-_Simulation_and_Formal_Verification_of_Self-stabilizing_Algorithms) in [the Lustre Programming Language](https://www-verimag.imag.fr/The-Lustre-Programming-Language-and), relying on [Lurette][lurette] and [SASA](https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/) for testing/simulation and on [Kind2][kind2] for SMT-powered verification.
 
 
-## [dot2lus](src/dot2lus.ml)
+## [salut](src/dot2lus.ml)
 
 ### Summary
 
-dot2lus    compiles     a    graph    described    in     the    [DOT
+salut    compiles     a    graph    described    in     the    [DOT
 format](https://en.wikipedia.org/wiki/DOT_(graph_description_language))
 into   a    Lustre   program   that   executes    some   [Distributed
 Self-Stabilizing
@@ -17,7 +17,7 @@ Algorithm](https://www-verimag.imag.fr/New-Book-Introduction-to-Distributed.html
 over an equivalent network topology.
 
 ```
-dot2lus <dotfile> [-o <lusfile>] [--clock] [--help]
+salut <dotfile> [-o <lusfile>] [--clock] [--help]
   -o Set output file (default is inferred from input file)
   --clock Generate clocked code (default is unclocked)
   --help  Display this list of options
@@ -68,16 +68,20 @@ function p_step<<const degree:int>>(
 Some [example algorithms](test/) are provided in this repository.
 Each folder contains a distributed algorithm defined in both OCaml+SASA and LustreV6+SALUT and with a common network topology.
 
+
 The [shared Makefile](test/Makefile.inc) has instructions on how to `build` the Lustre-defined network and use [Lurette][lurette] to `test` it agains the SASA model.
 
+```sh
+$ cd salut/test/coloring/
+$ make clique3.lurette
+$ make er100.lurette
+```
+
 You can also `verify` it with [Kind2][kind2].
 Note that this currently requires converting LustreV6 to LustreV4 and adding Kind2's required annotations (to the generated LV4), which is also handled by the makefile.
 
-### Build instructions
-
 ```sh
-$ cd src/
-$ make # => bin/dot2lus
+$ make clique3.kind2
 ```
 
 [lurette]: https://www-verimag.imag.fr/Lurette-107.html
-- 
GitLab