From f284ff2872b46a3f20ea3eedae6533d38cdc2d14 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= <gwenael.delaval@inria.fr>
Date: Thu, 16 Mar 2017 11:59:02 +0100
Subject: [PATCH] Reachability example

Reachability example: use of reax to chech reachability of states.
---
 examples/reachability/build.sh         |  2 ++
 examples/reachability/reachability.ept | 25 +++++++++++++++++++++++++
 2 files changed, 27 insertions(+)
 create mode 100755 examples/reachability/build.sh
 create mode 100644 examples/reachability/reachability.ept

diff --git a/examples/reachability/build.sh b/examples/reachability/build.sh
new file mode 100755
index 0000000..07f1125
--- /dev/null
+++ b/examples/reachability/build.sh
@@ -0,0 +1,2 @@
+heptc -target ctrln reachability.ept
+reax -a 'sB:r' reachability_ctrln/reach_verif.ctrln
diff --git a/examples/reachability/reachability.ept b/examples/reachability/reachability.ept
new file mode 100644
index 0000000..b401761
--- /dev/null
+++ b/examples/reachability/reachability.ept
@@ -0,0 +1,25 @@
+node reach_verif(day_event,night_event,noon_event:bool) = (day_state,evening_state:bool)
+
+  contract
+  reachable evening_state
+
+let
+    automaton
+    state Night do day_state = false; evening_state = false
+    until day_event then Day
+    state Day do
+      day_state = true;
+      automaton
+      state Morning do
+        evening_state = false;
+      until noon_event then Afternoon
+      state Afternoon do
+        evening_state = false;
+      until night_event then Evening
+      state Evening do
+        evening_state = true;
+      until day_event then Morning
+      end
+    until night_event then Night
+    end
+tel