From e23b51018e16d1c8dc348ba597975b4ee753cc6e Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Tue, 30 Aug 2022 16:09:29 +0200
Subject: [PATCH] Add some documenation

---
 test/README.org | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test/README.org

diff --git a/test/README.org b/test/README.org
new file mode 100644
index 00000000..528e9ca1
--- /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
+  
-- 
GitLab