Examples and clean-ups #1
287
examples/bdd/generators/gen_drs.py
Executable file
287
examples/bdd/generators/gen_drs.py
Executable file
@@ -0,0 +1,287 @@
|
||||
#!/usr/bin/env python3
|
||||
|
||||
import sys
|
||||
import itertools
|
||||
|
||||
|
||||
class SingleReaction:
|
||||
def __init__(self, reactants=None, inhibitors=None, products=None):
|
||||
self.reactants = set(reactants) if reactants is not None else set()
|
||||
self.inhibitors = set(inhibitors) if inhibitors is not None else set()
|
||||
self.products = set(products) if products is not None else set()
|
||||
|
||||
def get_reactants(self):
|
||||
return "{" + ", ".join(self.reactants) + "}"
|
||||
|
||||
def get_inhibitors(self):
|
||||
return "{" + ", ".join(self.inhibitors) + "}"
|
||||
|
||||
def get_products(self):
|
||||
return "{" + ", ".join(self.products) + "}"
|
||||
|
||||
def __str__(self):
|
||||
return (
|
||||
"{"
|
||||
+ f"{self.get_reactants()}, {self.get_inhibitors()} -> {self.get_products()}"
|
||||
+ "};"
|
||||
)
|
||||
|
||||
|
||||
class Reactions:
|
||||
def __init__(self):
|
||||
self.reactions = []
|
||||
|
||||
def add(self, reaction):
|
||||
self.reactions.append(reaction)
|
||||
|
||||
def __str__(self):
|
||||
ret = ""
|
||||
for r in self.reactions:
|
||||
ret += f"{r}\n"
|
||||
return ret
|
||||
|
||||
|
||||
class Transition:
|
||||
def __init__(self, src, dst, guard, context):
|
||||
self.src = src
|
||||
self.dst = dst
|
||||
self.guard = guard
|
||||
self.context = context
|
||||
|
||||
def get_context_str(self):
|
||||
r = []
|
||||
for proc, entities in self.context:
|
||||
ent_str = ",".join(entities)
|
||||
r.append(f"{proc}={{{ent_str}}}")
|
||||
|
||||
r = " ".join(r)
|
||||
return "{ " + r + " }"
|
||||
|
||||
def __str__(self):
|
||||
if self.guard:
|
||||
return f"{self.get_context_str()}: {self.src} -> {self.dst} : {self.guard};"
|
||||
else:
|
||||
return f"{self.get_context_str()}: {self.src} -> {self.dst};"
|
||||
|
||||
|
||||
class Automaton:
|
||||
def __init__(self):
|
||||
self.transitions = []
|
||||
self.states = []
|
||||
self.init_state = None
|
||||
|
||||
def add_transition(self, transition):
|
||||
self.transitions.append(transition)
|
||||
|
||||
def add_state(self, state):
|
||||
if state not in self.states:
|
||||
self.states.append(state)
|
||||
|
||||
def set_init_state(self, state):
|
||||
assert state in self.states, f"{state} not in states"
|
||||
self.init_state = state
|
||||
|
||||
def __str__(self):
|
||||
r = "context-automaton {\n"
|
||||
r += "\tstates { " + ", ".join(self.states) + " };\n"
|
||||
r += f"\tinit-state {{ {self.init_state} }};\n"
|
||||
r += "\ttransitions {\n"
|
||||
for tr in self.transitions:
|
||||
r += "\t\t" + str(tr) + "\n"
|
||||
r += "\t};\n"
|
||||
r += "};\n"
|
||||
return r
|
||||
|
||||
|
||||
class DRSGenerator:
|
||||
def __init__(self, x, y, z, aut):
|
||||
assert y >= z
|
||||
assert x >= 2 and y >= 2 and z >= 2
|
||||
self.x = x
|
||||
self.y = y
|
||||
self.z = z
|
||||
self.aut_id = aut
|
||||
self.n = self.y
|
||||
self.reactions = {}
|
||||
|
||||
self.automaton = Automaton()
|
||||
|
||||
self.generate()
|
||||
|
||||
def generate_agent_zero(self):
|
||||
rcts = Reactions()
|
||||
for i in range(1, self.y + 1):
|
||||
rcts.add(SingleReaction(["RTK"], ["h"], [f"RTK{i}"]))
|
||||
for j in range(1, self.x + 1):
|
||||
rcts.add(SingleReaction([f"EN:{j}_{i}"], ["h"], [f"ENi:{self.x}_{i}"]))
|
||||
return rcts
|
||||
|
||||
def generate_reactions_for_component(self, i):
|
||||
self.reactions.setdefault(i, Reactions())
|
||||
rcts = self.reactions[i]
|
||||
rcts.add(SingleReaction(["GF"], ["h"], ["GF"]))
|
||||
rcts.add(SingleReaction(["GF"], ["h", f"RTK{i}"], ["RTK"]))
|
||||
rcts.add(SingleReaction(["RTK"], [f"ENi:1_{i}"], [f"EN:1_{i}"]))
|
||||
for j in range(1, self.x):
|
||||
rcts.add(
|
||||
SingleReaction([f"EN:{j}_{i}"], [f"ENi:{j+1}_{i}"], [f"EN:{j+1}_{i}"])
|
||||
)
|
||||
|
||||
indices = list(range(1, self.y + 1))
|
||||
for comb in itertools.combinations(indices, self.z):
|
||||
reactants = []
|
||||
for i in comb:
|
||||
reactants.append(f"EN:{self.x}_{i}")
|
||||
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; };")
|
||||
print("reactions {")
|
||||
|
||||
for i in range(1, self.y + 1):
|
||||
self.generate_reactions_for_component(i)
|
||||
|
||||
rcts_0 = self.generate_agent_zero()
|
||||
|
||||
print("proc0 {")
|
||||
print(rcts_0)
|
||||
print("};")
|
||||
|
||||
for proc, reactions in self.reactions.items():
|
||||
print(f"proc{proc} {{")
|
||||
print(reactions)
|
||||
print("};")
|
||||
|
||||
print("};")
|
||||
|
||||
if self.aut_id == "a":
|
||||
self.generate_automaton_4(self.n)
|
||||
elif self.aut_id == "b":
|
||||
self.generate_automaton_5(self.n)
|
||||
else:
|
||||
raise RuntimeError(f"Unknown automaton identifier: {self.aut_id}")
|
||||
|
||||
self.generate_formula()
|
||||
|
||||
def generate_automaton_4(self, n):
|
||||
aut = self.automaton
|
||||
|
||||
aut.add_state("qI")
|
||||
aut.add_state("qS")
|
||||
for i in range(1, n + 1):
|
||||
aut.add_state(f"q{i}A")
|
||||
aut.add_state(f"q{i}B")
|
||||
aut.add_state(f"q{i}C")
|
||||
aut.add_state(f"q{i}D")
|
||||
|
||||
aut.set_init_state("qI")
|
||||
|
||||
aut.add_transition(
|
||||
Transition("qI", "qS", "", [(f"proc{i}", ["GF"]) for i in range(0, n + 1)])
|
||||
)
|
||||
|
||||
for i in range(1, n + 1):
|
||||
aut.add_transition(Transition("qS", f"q{i}A", "", [(f"proc{i}", [])]))
|
||||
aut.add_transition(
|
||||
Transition(
|
||||
f"q{i}A", f"q{i}B", "", [(f"proc{v}", []) for v in range(0, n + 1)]
|
||||
)
|
||||
)
|
||||
aut.add_transition(Transition(f"q{i}B", f"q{i}C", "", [(f"proc{i}", [])]))
|
||||
aut.add_transition(
|
||||
Transition(
|
||||
f"q{i}C", f"q{i}D", "", [(f"proc{v}", []) for v in range(0, n + 1)]
|
||||
)
|
||||
)
|
||||
|
||||
for i in range(1, n + 1):
|
||||
for j in range(1, n + 1):
|
||||
if i == j:
|
||||
continue
|
||||
aut.add_transition(
|
||||
Transition(f"q{i}B", f"q{j}A", "", [(f"proc{j}", [])])
|
||||
)
|
||||
aut.add_transition(
|
||||
Transition(f"q{i}D", f"q{j}A", "", [(f"proc{j}", [])])
|
||||
)
|
||||
|
||||
print(aut)
|
||||
|
||||
def generate_automaton_5(self, n):
|
||||
aut = self.automaton
|
||||
|
||||
for i in range(0, (4 * n + 1)):
|
||||
aut.add_state(f"q{i}")
|
||||
|
||||
aut.set_init_state("q0")
|
||||
|
||||
aut.add_transition(
|
||||
Transition("q0", "q1", "", [(f"proc{i}", ["GF"]) for i in range(0, n + 1)])
|
||||
)
|
||||
|
||||
for i in range(0, n): # 0, ..., n-1
|
||||
aut.add_transition(
|
||||
Transition(f"q{4*i+1}", f"q{4*i+2}", "", [(f"proc{i+1}", [])])
|
||||
)
|
||||
aut.add_transition(
|
||||
Transition(
|
||||
f"q{4*i+2}",
|
||||
f"q{4*i+3}",
|
||||
"",
|
||||
[(f"proc{v}", []) for v in range(0, n + 1)],
|
||||
)
|
||||
)
|
||||
aut.add_transition(
|
||||
Transition(f"q{4*i+3}", f"q{4*i+4}", "", [(f"proc{i+1}", [])])
|
||||
)
|
||||
|
||||
for i in range(0, n - 1): # 0, ..., n-2
|
||||
aut.add_transition(
|
||||
Transition(
|
||||
f"q{4*i+4}",
|
||||
f"q{4*i+5}",
|
||||
"",
|
||||
[(f"proc{v}", []) for v in range(0, n + 1)],
|
||||
)
|
||||
)
|
||||
|
||||
aut.add_transition(
|
||||
Transition(f"q{4*n}", "q1", "", [(f"proc{i}", []) for i in range(0, n + 1)])
|
||||
)
|
||||
|
||||
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)])
|
||||
|
||||
r = (
|
||||
"rsctlk-property { f0 : AG( K[proc0]( "
|
||||
+ disjunction
|
||||
+ " ) OR K[proc0]( "
|
||||
+ conjunction
|
||||
+ " ) ) };"
|
||||
)
|
||||
|
||||
print(r)
|
||||
|
||||
|
||||
def main():
|
||||
if len(sys.argv) < 1 + 4:
|
||||
print(f"Usage: {sys.argv[0]} <x> <y> <z> <Aut>")
|
||||
print("\twhere x,y,z >= 2 and y >= z")
|
||||
print("\tAut: a, b")
|
||||
sys.exit(1)
|
||||
|
||||
g = DRSGenerator(
|
||||
x=int(sys.argv[1]),
|
||||
y=int(sys.argv[2]),
|
||||
z=int(sys.argv[3]),
|
||||
aut=sys.argv[4],
|
||||
)
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
@@ -58,24 +58,34 @@ 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)
|
||||
|
||||
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)
|
||||
|
||||
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)
|
||||
|
||||
@@ -114,4 +124,3 @@ formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents,subf)
|
||||
out += PROPERTY_STR.format("f4", formula)
|
||||
|
||||
print(out)
|
||||
|
||||
|
||||
2
examples/smt/chain_reaction.py
Normal file → Executable file
2
examples/smt/chain_reaction.py
Normal file → Executable file
@@ -28,7 +28,6 @@ import resource
|
||||
|
||||
|
||||
def chain_reaction(print_system=False):
|
||||
|
||||
if len(sys.argv) < 1 + 3:
|
||||
print("{source} <N> <M> <type>".format(source=sys.argv[0]))
|
||||
print()
|
||||
@@ -115,7 +114,6 @@ def chain_reaction(print_system=False):
|
||||
|
||||
|
||||
def main():
|
||||
|
||||
chain_reaction()
|
||||
|
||||
|
||||
|
||||
19
examples/smt/heat_shock_response.py
Normal file → Executable file
19
examples/smt/heat_shock_response.py
Normal file → Executable file
@@ -28,7 +28,6 @@ import resource
|
||||
|
||||
|
||||
def heat_shock_response(print_system=True, verify_rsc=True):
|
||||
|
||||
if len(sys.argv) < 1 + 1:
|
||||
print("{source} <type>".format(source=sys.argv[0]))
|
||||
print("type:")
|
||||
@@ -62,15 +61,23 @@ def heat_shock_response(print_system=True, verify_rsc=True):
|
||||
r.add_reaction([("hsf3", 1)], [("hse", 1), ("hsp", 1)], [("hsf", 1)])
|
||||
r.add_reaction([("hsf3", 1), ("hsp", 1), ("mfp", 1)], [("hse", 1)], [("hsf", 1)])
|
||||
r.add_reaction([("hsf3", 1), ("hse", 1)], [("hsp", 1)], [("hsf3:hse", 1)])
|
||||
r.add_reaction([("hsp",1),("hsf3",1),("mfp",1),("hse",1)],[], [("hsf3:hse",1)])
|
||||
r.add_reaction(
|
||||
[("hsp", 1), ("hsf3", 1), ("mfp", 1), ("hse", 1)], [], [("hsf3:hse", 1)]
|
||||
)
|
||||
r.add_reaction([("hse", 1)], [("hsf3", 1)], [("hse", 1)])
|
||||
r.add_reaction([("hsp", 1), ("hsf3", 1), ("hse", 1)], [("mfp", 1)], [("hse", 1)])
|
||||
r.add_reaction([("hsf3:hse", 1)], [("hsp", 1)], [("hsp", 1), ("hsf3:hse", 1)])
|
||||
r.add_reaction([("hsp",1),("mfp",1),("hsf3:hse",1)],[], [("hsp",1),("hsf3:hse",1)])
|
||||
r.add_reaction(
|
||||
[("hsp", 1), ("mfp", 1), ("hsf3:hse", 1)], [], [("hsp", 1), ("hsf3:hse", 1)]
|
||||
)
|
||||
r.add_reaction([("hsf", 1), ("hsp", 1)], [("mfp", 1)], [("hsp:hsf", 1)])
|
||||
r.add_reaction([("hsp:hsf",1),("temp",stress_temp)],[], [("hsf",1),("hsp",1)])
|
||||
r.add_reaction(
|
||||
[("hsp:hsf", 1), ("temp", stress_temp)], [], [("hsf", 1), ("hsp", 1)]
|
||||
)
|
||||
r.add_reaction([("hsp:hsf", 1)], [("temp", stress_temp)], [("hsp:hsf", 1)])
|
||||
r.add_reaction([("hsp",1),("hsf3:hse",1)], [("mfp",1)], [("hse",1),("hsp:hsf",1)])
|
||||
r.add_reaction(
|
||||
[("hsp", 1), ("hsf3:hse", 1)], [("mfp", 1)], [("hse", 1), ("hsp:hsf", 1)]
|
||||
)
|
||||
r.add_reaction([("temp", stress_temp), ("prot", 1)], [], [("mfp", 1), ("prot", 1)])
|
||||
r.add_reaction([("prot", 1)], [("temp", stress_temp)], [("prot", 1)])
|
||||
r.add_reaction([("hsp", 1), ("mfp", 1)], [], [("hsp:mfp", 1)])
|
||||
@@ -117,9 +124,9 @@ def state_translate_rsc2rs(p):
|
||||
|
||||
|
||||
def main():
|
||||
|
||||
heat_shock_response()
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
|
||||
|
||||
7
examples/smt/mutex_param.py
Normal file → Executable file
7
examples/smt/mutex_param.py
Normal file → Executable file
@@ -77,7 +77,6 @@ def mutex_param_bench(cmd_args):
|
||||
Inhib = [("s", 1)]
|
||||
|
||||
for i in range(n_proc):
|
||||
|
||||
r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
|
||||
r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
|
||||
|
||||
@@ -217,7 +216,6 @@ def mutex_nonparam_bench(cmd_args):
|
||||
Inhib = [("s", 1)]
|
||||
|
||||
for i in range(n_proc):
|
||||
|
||||
r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
|
||||
r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
|
||||
|
||||
@@ -325,7 +323,6 @@ def mutex_nonparam_bench_oldimpl(cmd_args):
|
||||
Inhib = [("s", 1)]
|
||||
|
||||
for i in range(n_proc):
|
||||
|
||||
r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
|
||||
r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
|
||||
|
||||
@@ -407,7 +404,6 @@ def state_translate_rsc2rs(p):
|
||||
|
||||
|
||||
def mutex_bench_main(cmd_args):
|
||||
|
||||
mode = cmd_args.mode
|
||||
|
||||
if mode == "p":
|
||||
@@ -422,7 +418,6 @@ def mutex_bench_main(cmd_args):
|
||||
|
||||
|
||||
def main():
|
||||
|
||||
parser = argparse.ArgumentParser()
|
||||
|
||||
parser.add_argument(
|
||||
@@ -432,7 +427,7 @@ def main():
|
||||
|
||||
parser.add_argument(
|
||||
"mode",
|
||||
choices=['p', 'np-p', 'np-np'],
|
||||
choices=["p", "np-p", "np-np"],
|
||||
help="Selects the mode: p - parameter synthesis (parametric implementation), np-p - non-parametric with parametric implementation (with the parameters substituted), np-np - non-parametric with non-parametric implementation (parameters substituted)",
|
||||
)
|
||||
|
||||
|
||||
54
examples/smt/scalable_chain.py
Normal file → Executable file
54
examples/smt/scalable_chain.py
Normal file → Executable file
@@ -31,6 +31,7 @@ from itertools import chain, combinations
|
||||
import sys
|
||||
import resource
|
||||
|
||||
|
||||
def generate_system(chainLen, maxConc):
|
||||
"""
|
||||
This function generates the reaction system with concentrations
|
||||
@@ -54,7 +55,11 @@ def generate_system(chainLen, maxConc):
|
||||
if i < chainLen:
|
||||
r.add_reaction([(ent, maxConc)], [], [("e_" + str(i + 1), 1)])
|
||||
|
||||
r.add_reaction([("e_" + str(chainLen),maxConc)],[("dec",1)],[("e_" + str(chainLen),maxConc)])
|
||||
r.add_reaction(
|
||||
[("e_" + str(chainLen), maxConc)],
|
||||
[("dec", 1)],
|
||||
[("e_" + str(chainLen), maxConc)],
|
||||
)
|
||||
|
||||
c = ContextAutomatonWithConcentrations(r)
|
||||
c.add_init_state("init")
|
||||
@@ -66,6 +71,7 @@ def generate_system(chainLen, maxConc):
|
||||
|
||||
return rc
|
||||
|
||||
|
||||
def generate_formula(formula_number, chainLen, maxConc):
|
||||
"""
|
||||
This function generates the rsLTL formula
|
||||
@@ -73,30 +79,50 @@ def generate_formula(formula_number, chainLen, maxConc):
|
||||
"""
|
||||
|
||||
if formula_number == 1:
|
||||
ret = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) >= maxConc) )
|
||||
ret = Formula_rsLTL.f_F(
|
||||
BagDescription.f_entity("inc") > 0,
|
||||
(BagDescription.f_entity("e_" + str(chainLen)) >= maxConc),
|
||||
)
|
||||
|
||||
elif formula_number == 2:
|
||||
f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) )
|
||||
f_tmp = Formula_rsLTL.f_F(
|
||||
BagDescription.f_entity("inc") > 0,
|
||||
(BagDescription.f_entity("e_" + str(chainLen)) == maxConc),
|
||||
)
|
||||
for i in range(chainLen - 1, 0, -1):
|
||||
f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, f_tmp & (BagDescription.f_entity('e_'+str(i)) == maxConc) )
|
||||
f_tmp = Formula_rsLTL.f_F(
|
||||
BagDescription.f_entity("inc") > 0,
|
||||
f_tmp & (BagDescription.f_entity("e_" + str(i)) == maxConc),
|
||||
)
|
||||
ret = f_tmp
|
||||
|
||||
elif formula_number == 3:
|
||||
ret = Formula_rsLTL.f_G( BagDescription.f_TRUE(),
|
||||
ret = Formula_rsLTL.f_G(
|
||||
BagDescription.f_TRUE(),
|
||||
Formula_rsLTL.f_Implies(
|
||||
(BagDescription.f_entity('e_1') == 1),
|
||||
(BagDescription.f_entity("e_1") == 1),
|
||||
Formula_rsLTL.f_F(
|
||||
BagDescription.f_entity("inc") > 0,
|
||||
(BagDescription.f_entity('e_'+str(chainLen)) == maxConc)
|
||||
)
|
||||
)
|
||||
(BagDescription.f_entity("e_" + str(chainLen)) == maxConc),
|
||||
),
|
||||
),
|
||||
)
|
||||
|
||||
elif formula_number == 4:
|
||||
ret = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') == maxConc )
|
||||
ret = Formula_rsLTL.f_F(
|
||||
BagDescription.f_entity("inc") > 0,
|
||||
BagDescription.f_entity("e_1") == maxConc,
|
||||
)
|
||||
|
||||
elif formula_number == 5:
|
||||
ret = Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_U( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') > 0, BagDescription.f_entity('e_2') > 0 ) )
|
||||
ret = Formula_rsLTL.f_X(
|
||||
BagDescription.f_TRUE(),
|
||||
Formula_rsLTL.f_U(
|
||||
BagDescription.f_entity("inc") > 0,
|
||||
BagDescription.f_entity("e_1") > 0,
|
||||
BagDescription.f_entity("e_2") > 0,
|
||||
),
|
||||
)
|
||||
|
||||
else:
|
||||
ret = None
|
||||
@@ -116,12 +142,12 @@ def save_statistics(smt_rsc, formula_number, chainLen, maxConc):
|
||||
filename_m = "bench_rsc_F" + str(formula_number) + "_mem.log"
|
||||
time = smt_rsc.get_verification_time()
|
||||
|
||||
f=open(filename_t, 'a')
|
||||
f = open(filename_t, "a")
|
||||
log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n"
|
||||
f.write(log_str)
|
||||
f.close()
|
||||
|
||||
f=open(filename_m, 'a')
|
||||
f = open(filename_m, "a")
|
||||
log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n"
|
||||
f.write(log_str)
|
||||
f.close()
|
||||
@@ -168,6 +194,6 @@ def scalable_chain(print_system=False):
|
||||
def main():
|
||||
scalable_chain(print_system=True)
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
|
||||
|
||||
97
experiments/drs_cell_signal/run.sh
Executable file
97
experiments/drs_cell_signal/run.sh
Executable file
@@ -0,0 +1,97 @@
|
||||
#!/usr/bin/env bash
|
||||
|
||||
x_values="2 3 4"
|
||||
y_values="`seq 2 20`"
|
||||
z_values="`seq 2 20`"
|
||||
aut_values="a b"
|
||||
|
||||
reactics="$1"
|
||||
reactics_opts="-z -x -vv -B -c"
|
||||
|
||||
input_generator="../../examples/bdd/generators/gen_drs.py"
|
||||
|
||||
benchname="sig"
|
||||
formname="f0"
|
||||
|
||||
outdir="results_${benchname}"
|
||||
|
||||
if [[ -z "$1" ]]
|
||||
then
|
||||
echo "Usage: $0 <path to reactics>"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
if [[ ! -x "$reactics" ]]
|
||||
then
|
||||
echo "Provided path to ReactICS not executable"
|
||||
fi
|
||||
|
||||
if [[ ! -d "$outdir" ]]
|
||||
then
|
||||
echo "Creating output directory: $outdir"
|
||||
mkdir -p $outdir
|
||||
fi
|
||||
|
||||
#ulimit -t 3600
|
||||
#ulimit -v 2097152
|
||||
ulimit -t 3600
|
||||
#ulimit -v 1000000
|
||||
|
||||
for a in $aut_values
|
||||
do
|
||||
for z in $z_values
|
||||
do
|
||||
for y in $y_values
|
||||
do
|
||||
for x in $x_values
|
||||
do
|
||||
|
||||
if [[ $y -lt $z ]]
|
||||
then
|
||||
# Skip undesired values
|
||||
continue
|
||||
fi
|
||||
|
||||
if [[ $y -ne $z ]]
|
||||
then
|
||||
# More aggressive skipping
|
||||
continue
|
||||
fi
|
||||
|
||||
bench_identifier="${benchname}_F${formname}_A${a}"
|
||||
|
||||
filename_base="${outdir}/${benchname}_F${formname}__x${x}_y${y}_z${z}_A${a}"
|
||||
outfile="${filename_base}.out"
|
||||
infile="${filename_base}.drs"
|
||||
|
||||
stopfile="DONE_${bench_identifier}"
|
||||
|
||||
if [[ -e "$stopfile" ]]
|
||||
then
|
||||
echo "Time limit -- SKIPPING"
|
||||
continue
|
||||
fi
|
||||
|
||||
$input_generator $x $y $z $a > ${infile}
|
||||
|
||||
$reactics $reactics_opts $formname $infile |& tee ${outfile}
|
||||
exitcode=$?
|
||||
echo "ReactICS exit code: $exitcode"
|
||||
|
||||
result="$(tail -1 $outfile | grep -E '.*;.*;.*;.*'| sed "s/STAT/$n /")"
|
||||
if [ "$result" = "" ]
|
||||
then
|
||||
echo "TIME LIMIT; marking as finished"
|
||||
#touch $stopfile
|
||||
else
|
||||
echo "$x ; $y ; $z ; $a ; $exitcode $result" >> $outdir/summary_${bench_identifier}.txt
|
||||
echo "$x $y $z $a $(echo $result | sed 's/;/ /g')" >> $outdir/${bench_identifier}.dat
|
||||
echo $result
|
||||
fi
|
||||
|
||||
done
|
||||
done
|
||||
done
|
||||
done
|
||||
|
||||
# EOF
|
||||
@@ -0,0 +1,53 @@
|
||||
2 76.250000
|
||||
3 79.312500
|
||||
4 77.968750
|
||||
5 85.015625
|
||||
6 77.640625
|
||||
7 75.250000
|
||||
8 86.406250
|
||||
9 104.093750
|
||||
10 99.531250
|
||||
11 95.875000
|
||||
12 101.203125
|
||||
13 96.453125
|
||||
14 124.062500
|
||||
15 137.359375
|
||||
16 147.859375
|
||||
17 145.156250
|
||||
18 151.906250
|
||||
19 160.187500
|
||||
20 164.093750
|
||||
21 220.562500
|
||||
22 226.953125
|
||||
23 235.328125
|
||||
24 243.609375
|
||||
25 254.906250
|
||||
26 254.609375
|
||||
27 272.281250
|
||||
28 272.093750
|
||||
29 301.406250
|
||||
30 317.281250
|
||||
31 400.984375
|
||||
32 396.140625
|
||||
33 420.203125
|
||||
34 447.046875
|
||||
35 427.609375
|
||||
36 444.031250
|
||||
37 454.843750
|
||||
38 476.515625
|
||||
39 499.593750
|
||||
40 518.218750
|
||||
41 552.796875
|
||||
42 529.078125
|
||||
43 552.546875
|
||||
44 557.968750
|
||||
45 745.328125
|
||||
46 725.406250
|
||||
47 734.046875
|
||||
48 768.203125
|
||||
49 780.328125
|
||||
50 813.640625
|
||||
51 818.156250
|
||||
52 892.656250
|
||||
53 872.609375
|
||||
54 908.328125
|
||||
@@ -0,0 +1,53 @@
|
||||
2 78.343750
|
||||
3 67.890625
|
||||
4 68.156250
|
||||
5 88.281250
|
||||
6 74.656250
|
||||
7 71.125000
|
||||
8 68.359375
|
||||
9 89.718750
|
||||
10 74.468750
|
||||
11 70.703125
|
||||
12 79.281250
|
||||
13 84.437500
|
||||
14 73.656250
|
||||
15 75.765625
|
||||
16 79.437500
|
||||
17 85.296875
|
||||
18 78.921875
|
||||
19 78.000000
|
||||
20 91.734375
|
||||
21 97.406250
|
||||
22 83.203125
|
||||
23 96.328125
|
||||
24 83.609375
|
||||
25 92.281250
|
||||
26 107.812500
|
||||
27 99.125000
|
||||
28 90.984375
|
||||
29 102.984375
|
||||
30 95.109375
|
||||
31 121.046875
|
||||
32 108.328125
|
||||
33 111.281250
|
||||
34 113.843750
|
||||
35 128.312500
|
||||
36 139.218750
|
||||
37 137.015625
|
||||
38 143.656250
|
||||
39 151.015625
|
||||
40 146.625000
|
||||
41 146.546875
|
||||
42 145.328125
|
||||
43 154.156250
|
||||
44 152.796875
|
||||
45 154.812500
|
||||
46 173.562500
|
||||
47 165.281250
|
||||
48 169.046875
|
||||
49 167.812500
|
||||
50 180.140625
|
||||
51 185.156250
|
||||
52 188.093750
|
||||
53 193.328125
|
||||
54 230.906250
|
||||
@@ -0,0 +1,53 @@
|
||||
2 0.069993
|
||||
3 0.110170
|
||||
4 0.163429
|
||||
5 0.244400
|
||||
6 0.326078
|
||||
7 0.435454
|
||||
8 0.574694
|
||||
9 0.756575
|
||||
10 0.963447
|
||||
11 1.191023
|
||||
12 1.470870
|
||||
13 1.798271
|
||||
14 2.197759
|
||||
15 2.631427
|
||||
16 3.141419
|
||||
17 3.740803
|
||||
18 4.384615
|
||||
19 5.152433
|
||||
20 6.010524
|
||||
21 7.243524
|
||||
22 8.078336
|
||||
23 9.238295
|
||||
24 10.559381
|
||||
25 12.179168
|
||||
26 13.710365
|
||||
27 15.687868
|
||||
28 17.332903
|
||||
29 19.724463
|
||||
30 22.126382
|
||||
31 24.589532
|
||||
32 27.154556
|
||||
33 31.373249
|
||||
34 33.994433
|
||||
35 37.379087
|
||||
36 41.225560
|
||||
37 45.762647
|
||||
38 51.688572
|
||||
39 56.050724
|
||||
40 60.950837
|
||||
41 66.596064
|
||||
42 72.954418
|
||||
43 80.002494
|
||||
44 87.091461
|
||||
45 94.821222
|
||||
46 103.463929
|
||||
47 111.833996
|
||||
48 121.959099
|
||||
49 132.695562
|
||||
50 143.592254
|
||||
51 155.356145
|
||||
52 168.150716
|
||||
53 182.149439
|
||||
54 195.561342
|
||||
@@ -0,0 +1,53 @@
|
||||
2 0.098639
|
||||
3 0.170014
|
||||
4 0.258657
|
||||
5 0.428040
|
||||
6 0.567658
|
||||
7 0.757204
|
||||
8 0.988715
|
||||
9 1.306164
|
||||
10 1.717904
|
||||
11 2.258792
|
||||
12 2.773149
|
||||
13 3.094348
|
||||
14 4.023511
|
||||
15 4.920939
|
||||
16 6.314265
|
||||
17 8.055828
|
||||
18 11.772655
|
||||
19 11.908597
|
||||
20 13.386385
|
||||
21 16.485505
|
||||
22 16.426735
|
||||
23 19.598138
|
||||
24 24.279200
|
||||
25 30.844283
|
||||
26 41.947712
|
||||
27 49.029652
|
||||
28 52.730995
|
||||
29 62.182717
|
||||
30 80.739602
|
||||
31 92.558721
|
||||
32 90.915901
|
||||
33 106.330487
|
||||
34 124.018849
|
||||
35 140.898334
|
||||
36 169.364359
|
||||
37 195.812449
|
||||
38 228.988631
|
||||
39 279.308753
|
||||
40 318.391139
|
||||
41 329.966894
|
||||
42 347.502791
|
||||
43 325.462907
|
||||
44 415.405552
|
||||
45 446.760682
|
||||
46 503.181844
|
||||
47 438.949250
|
||||
48 491.478016
|
||||
49 531.635930
|
||||
50 572.840797
|
||||
51 614.272754
|
||||
52 708.048464
|
||||
53 808.337098
|
||||
54 912.016908
|
||||
53
experiments/reaction_mining_mutex/bench_mutex_param_mem.dat
Normal file
53
experiments/reaction_mining_mutex/bench_mutex_param_mem.dat
Normal file
@@ -0,0 +1,53 @@
|
||||
2 80.750000
|
||||
3 87.406250
|
||||
4 87.500000
|
||||
5 93.109375
|
||||
6 102.687500
|
||||
7 104.265625
|
||||
8 110.406250
|
||||
9 139.343750
|
||||
10 143.343750
|
||||
11 150.859375
|
||||
12 160.140625
|
||||
13 168.031250
|
||||
14 213.890625
|
||||
15 224.937500
|
||||
16 237.750000
|
||||
17 246.421875
|
||||
18 253.718750
|
||||
19 275.343750
|
||||
20 300.734375
|
||||
21 302.687500
|
||||
22 372.859375
|
||||
23 401.906250
|
||||
24 427.656250
|
||||
25 456.406250
|
||||
26 461.843750
|
||||
27 497.953125
|
||||
28 478.796875
|
||||
29 513.015625
|
||||
30 533.640625
|
||||
31 571.406250
|
||||
32 592.890625
|
||||
33 750.218750
|
||||
34 782.078125
|
||||
35 811.390625
|
||||
36 808.765625
|
||||
37 794.375000
|
||||
38 905.328125
|
||||
39 982.078125
|
||||
40 978.343750
|
||||
41 975.796875
|
||||
42 1029.250000
|
||||
43 1009.687500
|
||||
44 1013.093750
|
||||
45 1041.359375
|
||||
46 1093.828125
|
||||
47 1089.546875
|
||||
48 1138.359375
|
||||
49 1451.656250
|
||||
50 1441.484375
|
||||
51 1512.953125
|
||||
52 1538.062500
|
||||
53 1578.609375
|
||||
54 1649.859375
|
||||
53
experiments/reaction_mining_mutex/bench_mutex_param_time.dat
Normal file
53
experiments/reaction_mining_mutex/bench_mutex_param_time.dat
Normal file
@@ -0,0 +1,53 @@
|
||||
2 0.508933
|
||||
3 0.879902
|
||||
4 1.418845
|
||||
5 2.106777
|
||||
6 2.756248
|
||||
7 3.793924
|
||||
8 4.415345
|
||||
9 7.047859
|
||||
10 8.535108
|
||||
11 10.661580
|
||||
12 13.401431
|
||||
13 18.212656
|
||||
14 21.531385
|
||||
15 27.613322
|
||||
16 35.731410
|
||||
17 44.066128
|
||||
18 50.457741
|
||||
19 60.318705
|
||||
20 80.069948
|
||||
21 95.711940
|
||||
22 108.791204
|
||||
23 138.778133
|
||||
24 153.953532
|
||||
25 173.971168
|
||||
26 215.769325
|
||||
27 254.425827
|
||||
28 278.991195
|
||||
29 324.744295
|
||||
30 399.375139
|
||||
31 450.518082
|
||||
32 451.632128
|
||||
33 537.802476
|
||||
34 522.508473
|
||||
35 656.979903
|
||||
36 670.512593
|
||||
37 725.848807
|
||||
38 937.150826
|
||||
39 1092.140628
|
||||
40 1212.583719
|
||||
41 1269.231571
|
||||
42 1480.000170
|
||||
43 1564.529588
|
||||
44 1526.681093
|
||||
45 1617.824403
|
||||
46 2067.677182
|
||||
47 2047.749685
|
||||
48 2030.002665
|
||||
49 2111.684038
|
||||
50 2225.756949
|
||||
51 2843.665940
|
||||
52 3049.816252
|
||||
53 3121.489341
|
||||
54 3430.799971
|
||||
456
experiments/reaction_mining_mutex/pmutex.py
Executable file
456
experiments/reaction_mining_mutex/pmutex.py
Executable file
@@ -0,0 +1,456 @@
|
||||
#!/usr/bin/env python
|
||||
|
||||
#
|
||||
# Copyright (c) 2015-2019 Artur Meski
|
||||
#
|
||||
# Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
# of this software and associated documentation files (the "Software"), to deal
|
||||
# in the Software without restriction, including without limitation the rights
|
||||
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
# copies of the Software, and to permit persons to whom the Software is
|
||||
# furnished to do so, subject to the following conditions:
|
||||
#
|
||||
# The above copyright notice and this permission notice shall be included in all
|
||||
# copies or substantial portions of the Software.
|
||||
#
|
||||
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
|
||||
# SOFTWARE.
|
||||
#
|
||||
|
||||
from rs import *
|
||||
from smt import *
|
||||
from logics import *
|
||||
from rsltl_shortcuts import *
|
||||
|
||||
from itertools import chain, combinations
|
||||
|
||||
import sys
|
||||
import resource
|
||||
import argparse
|
||||
|
||||
|
||||
def powerset(iterable, N=None):
|
||||
if N is None:
|
||||
N = len(s)
|
||||
s = list(iterable)
|
||||
return chain.from_iterable(combinations(s, r) for r in range(N + 1))
|
||||
|
||||
|
||||
def mutex_param_bench(cmd_args):
|
||||
"""
|
||||
Mutex Benchmark
|
||||
|
||||
Parametric
|
||||
"""
|
||||
|
||||
base_entities = ["out", "req", "in", "act"]
|
||||
shared_entities = ["lock", "done", "s"]
|
||||
|
||||
if not cmd_args.scaling:
|
||||
print("Missing scaling parameter")
|
||||
return
|
||||
n_proc = int(cmd_args.scaling)
|
||||
|
||||
r = ReactionSystemWithConcentrationsParam()
|
||||
|
||||
def E(a, b, c=1):
|
||||
return (a + "_" + str(b), c)
|
||||
|
||||
for i in range(n_proc):
|
||||
for ent in base_entities:
|
||||
max_conc = 1
|
||||
if ent == "in":
|
||||
max_conc = 3
|
||||
elif ent == "req":
|
||||
max_conc = 2
|
||||
r.add_bg_set_entity(E(ent, i, max_conc))
|
||||
|
||||
for ent in shared_entities:
|
||||
max_conc = 1
|
||||
r.add_bg_set_entity((ent, max_conc))
|
||||
|
||||
###################################################
|
||||
|
||||
Inhib = [("s", 1)]
|
||||
|
||||
for i in range(n_proc):
|
||||
r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
|
||||
r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
|
||||
|
||||
for j in range(n_proc):
|
||||
if i != j:
|
||||
r.add_reaction(
|
||||
[E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
|
||||
)
|
||||
|
||||
r.add_reaction([E("req", i)], [E("act", i)], [E("req", i, 2)])
|
||||
|
||||
enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
|
||||
r.add_reaction(
|
||||
[E("req", i, 2), E("act", i)], enter_inhib, [E("in", i, 3), ("lock", 1)]
|
||||
)
|
||||
|
||||
r.add_reaction([E("in", i, 3), E("act", i)], Inhib, [E("in", i, 2)])
|
||||
r.add_reaction([E("in", i, 2), E("act", i)], Inhib, [E("in", i, 1)])
|
||||
|
||||
r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
|
||||
r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
|
||||
|
||||
r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
|
||||
|
||||
lda1 = r.get_param("lda1")
|
||||
lda2 = r.get_param("lda2")
|
||||
lda3 = r.get_param("lda3")
|
||||
|
||||
r.add_reaction(lda1, lda2, lda3)
|
||||
|
||||
###################################################
|
||||
|
||||
c = ContextAutomatonWithConcentrations(r)
|
||||
c.add_init_state("0")
|
||||
c.add_state("1")
|
||||
|
||||
init_ctx = []
|
||||
for i in range(n_proc):
|
||||
init_ctx.append(E("out", i))
|
||||
|
||||
# the experiments starts with adding x and y:
|
||||
c.add_transition("0", init_ctx, "1")
|
||||
|
||||
all_act = powerset([E("act", i) for i in range(n_proc)], 2)
|
||||
|
||||
for actions in all_act:
|
||||
actions = list(actions)
|
||||
|
||||
c.add_transition("1", actions, "1")
|
||||
|
||||
# for all the remaining steps we have empty context sequences
|
||||
# c.add_transition("1", [], "1")
|
||||
# c.add_transition("1", [("h", 1)], "1")
|
||||
|
||||
###################################################
|
||||
|
||||
rc = ReactionSystemWithAutomaton(r, c)
|
||||
rc.show()
|
||||
|
||||
f_attack = ltl_F(
|
||||
True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
|
||||
)
|
||||
|
||||
ent_of_Nth_proc = [
|
||||
ent + "_" + str(n_proc - 1) for ent in base_entities
|
||||
] + shared_entities
|
||||
disallow = ["in_" + str(n_proc - 1)]
|
||||
for ent in r.background_set:
|
||||
if ent not in ent_of_Nth_proc:
|
||||
disallow.append(ent)
|
||||
|
||||
# disallow.append("act_" + str(n_proc-1))
|
||||
|
||||
# disallow = ["in_0", "in_" + str(n_proc)] #, "req_0", "req_1"]
|
||||
lda1_disallow = [param_entity(lda1, ent) == 0 for ent in disallow]
|
||||
lda2_disallow = [param_entity(lda2, ent) == 0 for ent in disallow]
|
||||
lda3_disallow = [param_entity(lda3, ent) == 0 for ent in disallow]
|
||||
lda_disallow = lda1_disallow + lda2_disallow + lda3_disallow
|
||||
|
||||
# for bent in base_entities:
|
||||
# print(param_entity(lda3, bent + "_0"))
|
||||
|
||||
param_constr = param_And(*lda_disallow)
|
||||
|
||||
smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
|
||||
smt_rsc.check_rsltl(
|
||||
formulae_list=[f_attack], param_constr=param_constr
|
||||
) # , max_level=4, cont_if_sat=True)
|
||||
|
||||
log_suffix = ""
|
||||
if cmd_args.optimise:
|
||||
log_suffix = "_OPT"
|
||||
|
||||
time = 0
|
||||
mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
|
||||
filename_t = "bench_mutex_param" + log_suffix + "_time.dat"
|
||||
filename_m = "bench_mutex_param" + log_suffix + "_mem.dat"
|
||||
time = smt_rsc.get_verification_time()
|
||||
|
||||
with open(filename_t, "a") as f:
|
||||
log_str = "{:d} {:f}\n".format(n_proc, time)
|
||||
f.write(log_str)
|
||||
|
||||
with open(filename_m, "a") as f:
|
||||
log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
|
||||
f.write(log_str)
|
||||
|
||||
|
||||
def mutex_nonparam_bench(cmd_args):
|
||||
"""
|
||||
Mutex Benchmark
|
||||
|
||||
Parametric
|
||||
"""
|
||||
|
||||
base_entities = ["out", "req", "in", "act"]
|
||||
shared_entities = ["lock", "done", "s"]
|
||||
|
||||
if not cmd_args.scaling:
|
||||
raise RuntimeError("Missing scaling parameter")
|
||||
n_proc = int(cmd_args.scaling)
|
||||
|
||||
r = ReactionSystemWithConcentrationsParam()
|
||||
|
||||
def E(a, b):
|
||||
return (a + "_" + str(b), 1)
|
||||
|
||||
for i in range(n_proc):
|
||||
for ent in base_entities:
|
||||
r.add_bg_set_entity(E(ent, i))
|
||||
|
||||
for ent in shared_entities:
|
||||
r.add_bg_set_entity((ent, 1))
|
||||
|
||||
###################################################
|
||||
|
||||
Inhib = [("s", 1)]
|
||||
|
||||
for i in range(n_proc):
|
||||
r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
|
||||
r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
|
||||
|
||||
for j in range(n_proc):
|
||||
if i != j:
|
||||
r.add_reaction(
|
||||
[E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
|
||||
)
|
||||
|
||||
r.add_reaction([E("req", i)], [E("act", i)], [E("req", i)])
|
||||
|
||||
enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
|
||||
r.add_reaction(
|
||||
[E("req", i), E("act", i)], enter_inhib, [E("in", i), ("lock", 1)]
|
||||
)
|
||||
|
||||
r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
|
||||
r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
|
||||
|
||||
r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
|
||||
|
||||
r.add_reaction(
|
||||
[E("out", n_proc - 1)], [("s", 1)], [("done", 1), E("req", n_proc - 1)]
|
||||
)
|
||||
|
||||
###################################################
|
||||
|
||||
c = ContextAutomatonWithConcentrations(r)
|
||||
c.add_init_state("0")
|
||||
c.add_state("1")
|
||||
|
||||
init_ctx = []
|
||||
for i in range(n_proc):
|
||||
init_ctx.append(E("out", i))
|
||||
|
||||
# the experiments starts with adding x and y:
|
||||
c.add_transition("0", init_ctx, "1")
|
||||
|
||||
all_act = powerset([E("act", i) for i in range(n_proc)], 2)
|
||||
|
||||
for actions in all_act:
|
||||
actions = list(actions)
|
||||
|
||||
c.add_transition("1", actions, "1")
|
||||
|
||||
# for all the remaining steps we have empty context sequences
|
||||
# c.add_transition("1", [], "1")
|
||||
# c.add_transition("1", [("h", 1)], "1")
|
||||
|
||||
###################################################
|
||||
|
||||
rc = ReactionSystemWithAutomaton(r, c)
|
||||
rc.show()
|
||||
|
||||
f_attack = ltl_F(
|
||||
True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
|
||||
)
|
||||
|
||||
smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
|
||||
smt_rsc.check_rsltl(formulae_list=[f_attack])
|
||||
|
||||
time = 0
|
||||
mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
|
||||
filename_t = "bench_mutex_nonparam_time.dat"
|
||||
filename_m = "bench_mutex_nonparam_mem.dat"
|
||||
time = smt_rsc.get_verification_time()
|
||||
|
||||
with open(filename_t, "a") as f:
|
||||
log_str = "{:d} {:f}\n".format(n_proc, time)
|
||||
f.write(log_str)
|
||||
|
||||
with open(filename_m, "a") as f:
|
||||
log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
|
||||
f.write(log_str)
|
||||
|
||||
|
||||
def mutex_nonparam_bench_oldimpl(cmd_args):
|
||||
"""
|
||||
Mutex Benchmark
|
||||
|
||||
Parametric
|
||||
"""
|
||||
|
||||
base_entities = ["out", "req", "in", "act"]
|
||||
shared_entities = ["lock", "done", "s"]
|
||||
|
||||
if not cmd_args.scaling:
|
||||
raise RuntimeError("Missing scaling parameter")
|
||||
n_proc = int(cmd_args.scaling)
|
||||
|
||||
r = ReactionSystemWithConcentrations()
|
||||
|
||||
def E(a, b):
|
||||
return (a + "_" + str(b), 1)
|
||||
|
||||
for i in range(n_proc):
|
||||
for ent in base_entities:
|
||||
r.add_bg_set_entity(E(ent, i))
|
||||
|
||||
for ent in shared_entities:
|
||||
r.add_bg_set_entity((ent, 1))
|
||||
|
||||
###################################################
|
||||
|
||||
Inhib = [("s", 1)]
|
||||
|
||||
for i in range(n_proc):
|
||||
r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
|
||||
r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
|
||||
|
||||
for j in range(n_proc):
|
||||
if i != j:
|
||||
r.add_reaction(
|
||||
[E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
|
||||
)
|
||||
|
||||
r.add_reaction([E("req", i)], [E("act", i)], [E("req", i)])
|
||||
|
||||
enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
|
||||
r.add_reaction(
|
||||
[E("req", i), E("act", i)], enter_inhib, [E("in", i), ("lock", 1)]
|
||||
)
|
||||
|
||||
r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
|
||||
r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
|
||||
|
||||
r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
|
||||
|
||||
r.add_reaction(
|
||||
[E("out", n_proc - 1)], [("s", 1)], [("done", 1), E("req", n_proc - 1)]
|
||||
)
|
||||
|
||||
r.rs_stats()
|
||||
|
||||
###################################################
|
||||
|
||||
c = ContextAutomatonWithConcentrations(r)
|
||||
c.add_init_state("0")
|
||||
c.add_state("1")
|
||||
|
||||
init_ctx = []
|
||||
for i in range(n_proc):
|
||||
init_ctx.append(E("out", i))
|
||||
|
||||
# the experiments starts with adding x and y:
|
||||
c.add_transition("0", init_ctx, "1")
|
||||
|
||||
all_act = powerset([E("act", i) for i in range(n_proc)], 2)
|
||||
|
||||
for actions in all_act:
|
||||
actions = list(actions)
|
||||
|
||||
c.add_transition("1", actions, "1")
|
||||
|
||||
# for all the remaining steps we have empty context sequences
|
||||
# c.add_transition("1", [], "1")
|
||||
# c.add_transition("1", [("h", 1)], "1")
|
||||
|
||||
###################################################
|
||||
|
||||
rc = ReactionSystemWithAutomaton(r, c)
|
||||
rc.show()
|
||||
|
||||
f_attack = ltl_F(
|
||||
True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
|
||||
)
|
||||
|
||||
smt_rsc = SmtCheckerRSC(rc)
|
||||
smt_rsc.check_rsltl(formula=f_attack)
|
||||
|
||||
time = 0
|
||||
mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
|
||||
filename_t = "bench_mutex_nonparam_oldimpl_time.dat"
|
||||
filename_m = "bench_mutex_nonparam_oldimpl_mem.dat"
|
||||
time = smt_rsc.get_verification_time()
|
||||
|
||||
with open(filename_t, "a") as f:
|
||||
log_str = "{:d} {:f}\n".format(n_proc, time)
|
||||
f.write(log_str)
|
||||
|
||||
with open(filename_m, "a") as f:
|
||||
log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
|
||||
f.write(log_str)
|
||||
|
||||
|
||||
def state_translate_rsc2rs(p):
|
||||
return [e[0] + "#" + str(e[1]) for e in p]
|
||||
|
||||
|
||||
def mutex_bench_main(cmd_args):
|
||||
mode = cmd_args.mode
|
||||
|
||||
if mode == "p":
|
||||
mutex_param_bench(cmd_args)
|
||||
elif mode == "np-p":
|
||||
mutex_nonparam_bench(cmd_args)
|
||||
elif mode == "np-np":
|
||||
mutex_nonparam_bench_oldimpl(cmd_args)
|
||||
else:
|
||||
print("Unrecognised mode")
|
||||
return
|
||||
|
||||
|
||||
def main():
|
||||
parser = argparse.ArgumentParser()
|
||||
|
||||
parser.add_argument(
|
||||
"scaling",
|
||||
help="scaling parameter value",
|
||||
)
|
||||
|
||||
parser.add_argument(
|
||||
"mode",
|
||||
choices=["p", "np-p", "np-np"],
|
||||
help="Selects the mode: p - parameter synthesis (parametric implementation), np-p - non-parametric with parametric implementation (with the parameters substituted), np-np - non-parametric with non-parametric implementation (parameters substituted)",
|
||||
)
|
||||
|
||||
parser.add_argument(
|
||||
"-v", "--verbose", help="turn verbosity on", action="store_true"
|
||||
)
|
||||
parser.add_argument(
|
||||
"-o",
|
||||
"--optimise",
|
||||
help="minimise the parametric computation result",
|
||||
action="store_true",
|
||||
)
|
||||
|
||||
args = parser.parse_args()
|
||||
|
||||
mutex_bench_main(args)
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
|
||||
# EOF
|
||||
24
experiments/reaction_mining_mutex/run_mutex_param.sh
Executable file
24
experiments/reaction_mining_mutex/run_mutex_param.sh
Executable file
@@ -0,0 +1,24 @@
|
||||
#!/bin/sh
|
||||
|
||||
# sudo systemsetup -getcomputersleep
|
||||
#sudo systemsetup -setcomputersleep Never
|
||||
# sudo systemsetup -setcomputersleep 1
|
||||
|
||||
REACTICS_SMT="../../reactics-smt"
|
||||
export PYTHONPATH="$PYTHONPATH:$REACTICS_SMT"
|
||||
|
||||
REACTICS_SCRIPT="./pmutex.py"
|
||||
|
||||
for i in `seq 2 50`
|
||||
do
|
||||
for special_mode in "p" "np-p" "np-np"
|
||||
do
|
||||
echo "$i (sm=${special_mode})"
|
||||
if [[ $special_mode == "p" ]]
|
||||
then
|
||||
$REACTICS_SCRIPT -o $i $special_mode
|
||||
fi
|
||||
$REACTICS_SCRIPT $i $special_mode
|
||||
done
|
||||
done
|
||||
|
||||
2
reactics
2
reactics
@@ -52,7 +52,7 @@ then
|
||||
then
|
||||
python3 $*
|
||||
else
|
||||
echo "Nothing to do"
|
||||
echo "Provide path to an example script (typically from ./examples/smt)"
|
||||
fi
|
||||
|
||||
elif [[ "$mode" == "setup" ]]
|
||||
|
||||
@@ -26,6 +26,9 @@ class ReactionSystem(object):
|
||||
def ordered_list_of_bgset_ids(self):
|
||||
return list(range(self.background_set_size))
|
||||
|
||||
def rs_stats(self):
|
||||
print(f"Reactions: {len(self.reactions)}")
|
||||
|
||||
def assume_not_in_bgset(self, name):
|
||||
if self.is_in_background_set(name):
|
||||
raise RuntimeError("The entity " + name + " is already on the list")
|
||||
|
||||
Reference in New Issue
Block a user