diff --git a/salut/README.md b/salut/README.md index 3e153030b154ea7486347a9707b8674f72a3aacf..e3759b4044a90d926409d99605809bf5a7c70e75 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