diff --git a/examples/bdd/generators/gen_drs.py b/examples/bdd/generators/gen_drs.py index c076f7a..2b0ea72 100755 --- a/examples/bdd/generators/gen_drs.py +++ b/examples/bdd/generators/gen_drs.py @@ -135,7 +135,6 @@ class DRSGenerator: rcts.add(SingleReaction(reactants, ["h"], ["TF"])) def generate(self): - print(f"# Generated for: x = {self.x}, y = {self.y}, z = {self.z}") print("options { use-context-automaton; make-progressive; };") @@ -211,7 +210,6 @@ class DRSGenerator: print(aut) def generate_automaton_5(self, n): - aut = self.automaton for i in range(0, (4 * n + 1)): @@ -256,7 +254,6 @@ class DRSGenerator: print(aut) def generate_formula(self): - disjunction = " OR ".join([f"proc{i}.TF" for i in range(1, self.y + 1)]) conjunction = " AND ".join([f"~proc{i}.TF" for i in range(1, self.y + 1)]) diff --git a/examples/bdd/generators/gen_tgc.py b/examples/bdd/generators/gen_tgc.py index d4bfcf0..65a73c4 100755 --- a/examples/bdd/generators/gen_tgc.py +++ b/examples/bdd/generators/gen_tgc.py @@ -1,6 +1,6 @@ #!/usr/bin/env python -from sys import argv,exit +from sys import argv, exit OPTIONS_STR = """ options { use-context-automaton; make-progressive; }; @@ -51,57 +51,67 @@ out += "};\n" transitions = "" -init_trans = 8*" " + "{ " +init_trans = 8 * " " + "{ " for i in range(n): init_trans += "proc{:d}={{out}} ".format(i) init_trans += "}: init -> green;\n" transitions += init_trans for i in range(n): - transitions += "{:s}{{ proc{:d}={{allowed}} }}: green -> red : proc{:d}.req;\n".format(8*" ", i, 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) + 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) + 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) + 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) + 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) + 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) +# formula = "EF( proc0.in )" +# out += PROPERTY_STR.format("f1",formula) # f1 formula = "EF( EX( proc0.in ) )" for i in range(1, n): formula += " AND EF( EX( proc{:d}.in ) )".format(i, i) -out += PROPERTY_STR.format("f1",formula) +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) +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("f3", formula) # f4 subf = "~proc1.in" @@ -110,8 +120,7 @@ for i in range(2, n): 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) +formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents, subf) +out += PROPERTY_STR.format("f4", formula) print(out) -