clean-up
This commit is contained in:
@@ -135,7 +135,6 @@ class DRSGenerator:
|
|||||||
rcts.add(SingleReaction(reactants, ["h"], ["TF"]))
|
rcts.add(SingleReaction(reactants, ["h"], ["TF"]))
|
||||||
|
|
||||||
def generate(self):
|
def generate(self):
|
||||||
|
|
||||||
print(f"# Generated for: x = {self.x}, y = {self.y}, z = {self.z}")
|
print(f"# Generated for: x = {self.x}, y = {self.y}, z = {self.z}")
|
||||||
|
|
||||||
print("options { use-context-automaton; make-progressive; };")
|
print("options { use-context-automaton; make-progressive; };")
|
||||||
@@ -211,7 +210,6 @@ class DRSGenerator:
|
|||||||
print(aut)
|
print(aut)
|
||||||
|
|
||||||
def generate_automaton_5(self, n):
|
def generate_automaton_5(self, n):
|
||||||
|
|
||||||
aut = self.automaton
|
aut = self.automaton
|
||||||
|
|
||||||
for i in range(0, (4 * n + 1)):
|
for i in range(0, (4 * n + 1)):
|
||||||
@@ -256,7 +254,6 @@ class DRSGenerator:
|
|||||||
print(aut)
|
print(aut)
|
||||||
|
|
||||||
def generate_formula(self):
|
def generate_formula(self):
|
||||||
|
|
||||||
disjunction = " OR ".join([f"proc{i}.TF" for i in range(1, self.y + 1)])
|
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)])
|
conjunction = " AND ".join([f"~proc{i}.TF" for i in range(1, self.y + 1)])
|
||||||
|
|
||||||
|
|||||||
@@ -1,6 +1,6 @@
|
|||||||
#!/usr/bin/env python
|
#!/usr/bin/env python
|
||||||
|
|
||||||
from sys import argv,exit
|
from sys import argv, exit
|
||||||
|
|
||||||
OPTIONS_STR = """
|
OPTIONS_STR = """
|
||||||
options { use-context-automaton; make-progressive; };
|
options { use-context-automaton; make-progressive; };
|
||||||
@@ -51,57 +51,67 @@ out += "};\n"
|
|||||||
|
|
||||||
transitions = ""
|
transitions = ""
|
||||||
|
|
||||||
init_trans = 8*" " + "{ "
|
init_trans = 8 * " " + "{ "
|
||||||
for i in range(n):
|
for i in range(n):
|
||||||
init_trans += "proc{:d}={{out}} ".format(i)
|
init_trans += "proc{:d}={{out}} ".format(i)
|
||||||
init_trans += "}: init -> green;\n"
|
init_trans += "}: init -> green;\n"
|
||||||
transitions += init_trans
|
transitions += init_trans
|
||||||
|
|
||||||
for i in range(n):
|
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"
|
no_req_cond = "~proc0.req"
|
||||||
for i in range(1, n):
|
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):
|
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):
|
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"
|
no_leave_cond = "~proc0.leave"
|
||||||
for i in range(1, n):
|
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):
|
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)
|
out += CA_STR.format(transitions)
|
||||||
|
|
||||||
## f1
|
## f1
|
||||||
#formula = "EF( proc0.in )"
|
# formula = "EF( proc0.in )"
|
||||||
#out += PROPERTY_STR.format("f1",formula)
|
# out += PROPERTY_STR.format("f1",formula)
|
||||||
|
|
||||||
# f1
|
# f1
|
||||||
formula = "EF( E<proc0.allowed>X( proc0.in ) )"
|
formula = "EF( E<proc0.allowed>X( proc0.in ) )"
|
||||||
for i in range(1, n):
|
for i in range(1, n):
|
||||||
formula += " AND EF( E<proc{:d}.allowed>X( proc{:d}.in ) )".format(i, i)
|
formula += " AND EF( E<proc{:d}.allowed>X( proc{:d}.in ) )".format(i, i)
|
||||||
out += PROPERTY_STR.format("f1",formula)
|
out += PROPERTY_STR.format("f1", formula)
|
||||||
|
|
||||||
# f2
|
# f2
|
||||||
formula = "EF( proc0.approach"
|
formula = "EF( proc0.approach"
|
||||||
for i in range(1, n):
|
for i in range(1, n):
|
||||||
formula += " AND proc{:d}.approach".format(i)
|
formula += " AND proc{:d}.approach".format(i)
|
||||||
formula += " )"
|
formula += " )"
|
||||||
out += PROPERTY_STR.format("f2",formula)
|
out += PROPERTY_STR.format("f2", formula)
|
||||||
|
|
||||||
# f3
|
# f3
|
||||||
subf = "~proc1.in"
|
subf = "~proc1.in"
|
||||||
for i in range(2, n):
|
for i in range(2, n):
|
||||||
subf += " AND ~proc{:d}.in".format(i)
|
subf += " AND ~proc{:d}.in".format(i)
|
||||||
formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
|
formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
|
||||||
out += PROPERTY_STR.format("f3",formula)
|
out += PROPERTY_STR.format("f3", formula)
|
||||||
|
|
||||||
# f4
|
# f4
|
||||||
subf = "~proc1.in"
|
subf = "~proc1.in"
|
||||||
@@ -110,8 +120,7 @@ for i in range(2, n):
|
|||||||
all_agents = "proc0"
|
all_agents = "proc0"
|
||||||
for i in range(1, n):
|
for i in range(1, n):
|
||||||
all_agents += ",proc{:d}".format(i)
|
all_agents += ",proc{:d}".format(i)
|
||||||
formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents,subf)
|
formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents, subf)
|
||||||
out += PROPERTY_STR.format("f4",formula)
|
out += PROPERTY_STR.format("f4", formula)
|
||||||
|
|
||||||
print(out)
|
print(out)
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user