Skip to content
Snippets Groups Projects
Commit 2d00b831 authored by erwan's avatar erwan
Browse files

doc: add exemples of use of salut

parent 2a18a9bf
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment