TGC examples with generator (correct syntax)

examples/bdd/generators/gen_tgc.py

@@ -3,20 +3,14 @@
 from sys import argv,exit
 
 OPTIONS_STR = """
-options { use-context-automaton; }
-"""
-CONTROLLER_STR = """
-    ct {
-        {{lock},{leave} -> {lock}};
-        {{req},{} -> {lock}};
-    };
+options { use-context-automaton; make-progressive; };
 """
 
 PROC_STR = """
     proc{:d} {{
         {{{{out}}, {{}} -> {{approach}}}};
         {{{{approach}}, {{req}} -> {{req}}}};
-        {{{{req}}, {{lock}} -> {{in}}}};
+        {{{{allowed}}, {{}} -> {{in}}}};
         {{{{in}}, {{}} -> {{out,leave}}}};
         {{{{req}}, {{in}} -> {{req}}}};
     }};
@@ -24,16 +18,16 @@ PROC_STR = """
 
 CA_STR = """
 context-automaton {{
-    states {{ s0, s1 }}
-    init-state {{ s0 }}
+    states {{ init, green, red }};
+    init-state {{ init }};
     transitions {{
 {:s}
-    }}
-}}
+    }};
+}};
 """
 
 PROPERTY_STR = """
-rsctlk-property {{ {:s} : {:s} }}
+rsctlk-property {{ {:s} : {:s} }};
 """
 
 
@@ -51,39 +45,73 @@ out = ""
 
 out += OPTIONS_STR
 out += "reactions {\n"
-out += CONTROLLER_STR
 for i in range(n):
     out += PROC_STR.format(i)
-out += "}\n"
+out += "};\n"
 
 transitions = ""
 
-init_trans = 8*" " + "{ ct={} "
+init_trans = 8*" " + "{ "
 for i in range(n):
     init_trans += "proc{:d}={{out}} ".format(i)
-
-init_trans += "}: s0 -> s1;\n"
-
+init_trans += "}: init -> green;\n"
 transitions += init_trans
 
 for i in range(n):
-    transitions += "{:s}{{ ct={{}} proc{:d}={{}} }}: s1 -> s1;\n".format(8*" ", i)    
+    transitions += "{:s}{{ proc{:d}={{allowed}} }}: green -> red : proc{:d}.req;\n".format(8*" ", i, i)
+
+no_req_cond = "~proc0.req"
+for i in range(1, n):
+     no_req_cond += " AND ~proc{:d}.req".format(i)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: green -> green : {:s};\n".format(8*" ", i, no_req_cond)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: red -> green : proc{:d}.leave;\n".format(8*" ", i, i)
+
+no_leave_cond = "~proc0.leave"
+for i in range(1, n):
+     no_leave_cond += " AND ~proc{:d}.leave".format(i)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: red -> red : {:s};\n".format(8*" ", i, no_leave_cond)
 
 out += CA_STR.format(transitions)
 
+## f1
+#formula = "EF( proc0.in )"
+#out += PROPERTY_STR.format("f1",formula)
+
 # f1
-formula = "EF( proc0.in )"
+formula = "EF( E<proc0.allowed>X( proc0.in ) )"
 for i in range(1, n):
-    formula += " AND EF( proc{:d}.in )".format(i)
+    formula += " AND EF( E<proc{:d}.allowed>X( proc{:d}.in ) )".format(i, i)
 out += PROPERTY_STR.format("f1",formula)
 
 # f2
+formula = "EF( proc0.approach"
+for i in range(1, n):
+    formula += " AND proc{:d}.approach".format(i)
+formula += " )"
+out += PROPERTY_STR.format("f2",formula)
+
+# f3
 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("f3",formula)
 
-out += PROPERTY_STR.format("f2",formula)
+# f4
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+all_agents = "proc0"
+for i in range(1, n):
+    all_agents += ",proc{:d}".format(i)
+formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents,subf)
+out += PROPERTY_STR.format("f4",formula)
 
 print(out)
 

reactics

@@ -37,7 +37,6 @@ REACTICS_SMT="$(pwd)/reactics-smt"
 if [[ "$mode" == "bdd" ]]
 then
   
-  echo $*
   if [[ ! -x $REACTICS_BDD/reactics ]]
   then
     echo "Make sure to run setup first!"