TGC with generator

examples/bdd/generators/gen_tgc.py

@@ -0,0 +1,89 @@
+#!/usr/bin/env python
+
+from sys import argv,exit
+
+OPTIONS_STR = """
+options { use-context-automaton; }
+"""
+CONTROLLER_STR = """
+    ct {
+        {{lock},{leave} -> {lock}};
+        {{req},{} -> {lock}};
+    };
+"""
+
+PROC_STR = """
+    proc{:d} {{
+        {{{{out}}, {{}} -> {{approach}}}};
+        {{{{approach}}, {{req}} -> {{req}}}};
+        {{{{req}}, {{lock}} -> {{in}}}};
+        {{{{in}}, {{}} -> {{out,leave}}}};
+        {{{{req}}, {{in}} -> {{req}}}};
+    }};
+"""
+
+CA_STR = """
+context-automaton {{
+    states {{ s0, s1 }}
+    init-state {{ s0 }}
+    transitions {{
+{:s}
+    }}
+}}
+"""
+
+PROPERTY_STR = """
+rsctlk-property {{ {:s} : {:s} }}
+"""
+
+
+#################################################################
+
+if len(argv) < 1:
+    print("Usage: {:s} <number of processes>".format(argv[0]))
+    exit(100)
+
+n = int(argv[1])
+
+assert n > 1, "number of proc must be > 1"
+
+out = ""
+
+out += OPTIONS_STR
+out += "reactions {\n"
+out += CONTROLLER_STR
+for i in range(n):
+    out += PROC_STR.format(i)
+out += "}\n"
+
+transitions = ""
+
+init_trans = 8*" " + "{ ct={} "
+for i in range(n):
+    init_trans += "proc{:d}={{out}} ".format(i)
+
+init_trans += "}: s0 -> s1;\n"
+
+transitions += init_trans
+
+for i in range(n):
+    transitions += "{:s}{{ ct={{}} proc{:d}={{}} }}: s1 -> s1;\n".format(8*" ", i)    
+
+out += CA_STR.format(transitions)
+
+# f1
+formula = "EF( proc0.in )"
+for i in range(1, n):
+    formula += " AND EF( proc{:d}.in )".format(i)
+out += PROPERTY_STR.format("f1",formula)
+
+# f2
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
+
+out += PROPERTY_STR.format("f2",formula)
+
+print(out)
+

examples/bdd/tgc.rs

@@ -1,49 +0,0 @@
-
-options { use-context-automaton; }
-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={} proc1={} proc2={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
-        { proc0={allowed} }: green -> red : proc0.req;
-        { proc1={allowed} }: green -> red : proc1.req;
-        { proc2={allowed} }: green -> red : proc2.req;
-        { proc0={} }: red -> green : proc0.leave;
-        { proc1={} }: red -> green : proc1.leave;
-        { proc2={} }: red -> green : proc2.leave;
-        { proc0={} proc1={} proc2={} } : red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
-    }
-}
-
-rsctlk-property { f1 : EF( proc0.in ) AND EF( proc1.in ) AND EF( proc2.in ) }
-
-rsctlk-property { f2 : AG( proc0.in IMPLIES K[proc0](~proc1.in AND ~proc2.in) ) }
-