This directory contains Lustre versions of the ASM algorithms available in Ocaml in file:../../test/

More precisely, each directory contains:

• symbolic links to the Ocaml implementation
• a lustre implementation of an ASM algorithm
• 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