From 6d0057c40f2668cab2ed07fcb0de9cc848f4a15a Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 22 Sep 2019 18:36:47 +0100
Subject: [PATCH] Examples file for TGC

---
 examples/bdd/tgc.rs | 58 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 examples/bdd/tgc.rs

diff --git a/examples/bdd/tgc.rs b/examples/bdd/tgc.rs
new file mode 100644
index 0000000..2498bf8
--- /dev/null
+++ b/examples/bdd/tgc.rs
@@ -0,0 +1,58 @@
+
+options { use-context-automaton; make-progressive; };
+reactions {
+
+    proc0 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+
+    proc1 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+
+    proc2 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+};
+
+context-automaton {
+    states { init, green, red };
+    init-state { init };
+    transitions {
+        { proc0={out} proc1={out} proc2={out} }: init -> green;
+        { proc0={allowed} }: green -> red : proc0.req;
+        { proc1={allowed} }: green -> red : proc1.req;
+        { proc2={allowed} }: green -> red : proc2.req;
+        { proc0={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc1={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc2={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc0={} }: red -> green : proc0.leave;
+        { proc1={} }: red -> green : proc1.leave;
+        { proc2={} }: red -> green : proc2.leave;
+        { proc0={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+        { proc1={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+        { proc2={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+
+    };
+};
+
+rsctlk-property { f1 : EF( E<proc0.allowed>X( proc0.in ) ) AND EF( E<proc1.allowed>X( proc1.in ) ) AND EF( E<proc2.allowed>X( proc2.in ) ) };
+
+rsctlk-property { f2 : EF( proc0.approach AND proc1.approach AND proc2.approach ) };
+
+rsctlk-property { f3 : AG( proc0.in IMPLIES K[proc0](~proc1.in AND ~proc2.in) ) };
+
+rsctlk-property { f4 : AG( proc0.in IMPLIES C[proc0,proc1,proc2](~proc1.in AND ~proc2.in) ) };
+