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

Add some documenation

parent 9bad9c8b
No related branches found
No related tags found
No related merge requests found
This directory contains Lustre versions of the ASM algorithms available
in Ocaml in file:../../test/
More precisely, each directory contains :
- a lustre implementation of an ASM algorithm
- some symbolic links to their Ocaml implementation
- a lustre oracle that checks (with lurette) that both implementations behaves the same
- a =verify.lus= that models some properties to be model-checked (with lesar or kinds2)
- a Makefile to run simulations or model-checking
To simulate or to model-check such Lustre programs, one can use
- =gg= and =gg-deco= to generate topologies via =.dot= files
- =salut= to generate a lustre versions of the =.dot= files
- the various =Makefiles= for examples of uses
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