diff --git a/test/README.org b/test/README.org new file mode 100644 index 0000000000000000000000000000000000000000..528e9ca1ea9ce30c29551778e2cdb34344257cf8 --- /dev/null +++ b/test/README.org @@ -0,0 +1,15 @@ +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 +