From af26ca543bb2a947c2a34065fb76e6c607b291b3 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Mon, 6 Nov 2023 21:09:08 +0000 Subject: [PATCH] Examples and clean-ups (#1) - Attempt at implementing an example for DRS - Complete reactions set - New automaton - Formula - Fixed automaton scaling - Proc index in the formula - Benchmark generators - Scripts to reproduce experiments for reaction mining --- examples/bdd/generators/gen_drs.py | 290 +++++++++++ examples/smt/chain_reaction.py | 4 +- examples/smt/heat_shock_response.py | 117 ++--- examples/smt/mutex_param.py | 17 +- examples/smt/scalable_chain.py | 150 +++--- experiments/drs_cell_signal/run.sh | 97 ++++ .../bench_mutex_nonparam_mem.dat | 20 + .../bench_mutex_nonparam_oldimpl_mem.dat | 20 + .../bench_mutex_nonparam_oldimpl_time.dat | 20 + .../bench_mutex_nonparam_time.dat | 20 + .../bench_mutex_param_mem.dat | 20 + .../bench_mutex_param_time.dat | 20 + experiments/reaction_mining_mutex/pmutex.py | 454 ++++++++++++++++++ .../reaction_mining_mutex/run_mutex_param.sh | 26 + reactics | 2 +- rs_testing.py => reactics-smt/rs_testing.py | 0 16 files changed, 1145 insertions(+), 132 deletions(-) create mode 100755 examples/bdd/generators/gen_drs.py mode change 100644 => 100755 examples/smt/chain_reaction.py mode change 100644 => 100755 examples/smt/heat_shock_response.py mode change 100644 => 100755 examples/smt/mutex_param.py mode change 100644 => 100755 examples/smt/scalable_chain.py create mode 100755 experiments/drs_cell_signal/run.sh create mode 100644 experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat create mode 100644 experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat create mode 100644 experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat create mode 100644 experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat create mode 100644 experiments/reaction_mining_mutex/bench_mutex_param_mem.dat create mode 100644 experiments/reaction_mining_mutex/bench_mutex_param_time.dat create mode 100755 experiments/reaction_mining_mutex/pmutex.py create mode 100755 experiments/reaction_mining_mutex/run_mutex_param.sh rename rs_testing.py => reactics-smt/rs_testing.py (100%) diff --git a/examples/bdd/generators/gen_drs.py b/examples/bdd/generators/gen_drs.py new file mode 100755 index 0000000..c076f7a --- /dev/null +++ b/examples/bdd/generators/gen_drs.py @@ -0,0 +1,290 @@ +#!/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]} ") + 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() diff --git a/examples/smt/chain_reaction.py b/examples/smt/chain_reaction.py old mode 100644 new mode 100755 index 9c5205b..b44a67e --- a/examples/smt/chain_reaction.py +++ b/examples/smt/chain_reaction.py @@ -28,7 +28,6 @@ import resource def chain_reaction(print_system=False): - if len(sys.argv) < 1 + 3: print("{source} ".format(source=sys.argv[0])) print() @@ -39,7 +38,7 @@ def chain_reaction(print_system=False): print() exit(1) - chainLen = int(sys.argv[1]) + chainLen = int(sys.argv[1]) maxConc = int(sys.argv[2]) # depth (max concentration) verify_rsc = bool(int(sys.argv[3])) @@ -115,7 +114,6 @@ def chain_reaction(print_system=False): def main(): - chain_reaction() diff --git a/examples/smt/heat_shock_response.py b/examples/smt/heat_shock_response.py old mode 100644 new mode 100755 index 3707236..eb627cd --- a/examples/smt/heat_shock_response.py +++ b/examples/smt/heat_shock_response.py @@ -28,8 +28,7 @@ import resource def heat_shock_response(print_system=True, verify_rsc=True): - - if len(sys.argv) < 1+1: + if len(sys.argv) < 1 + 1: print("{source} ".format(source=sys.argv[0])) print("type:") print(" - 1 -- RSC") @@ -37,72 +36,80 @@ def heat_shock_response(print_system=True, verify_rsc=True): print() exit(1) - verify_rsc=bool(int(sys.argv[1])) + verify_rsc = bool(int(sys.argv[1])) stress_temp = 42 max_temp = 50 - - r = ReactionSystemWithConcentrations() - r.add_bg_set_entity(("hsp",1)) - r.add_bg_set_entity(("hsf",1)) - r.add_bg_set_entity(("hsf2",1)) - r.add_bg_set_entity(("hsf3",1)) - r.add_bg_set_entity(("hse",1)) - r.add_bg_set_entity(("mfp",1)) - r.add_bg_set_entity(("prot",1)) - r.add_bg_set_entity(("hsf3:hse",1)) - r.add_bg_set_entity(("hsp:mfp",1)) - r.add_bg_set_entity(("hsp:hsf",1)) - r.add_bg_set_entity(("temp",max_temp)) - r.add_bg_set_entity(("heat",1)) - r.add_bg_set_entity(("cool",1)) - - r.add_reaction([("hsf",1)], [("hsp",1)], [("hsf3",1)]) - r.add_reaction([("hsf",1),("hsp",1),("mfp",1)], [], [("hsf3",1)]) - 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([("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([("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)],[("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)]) - r.add_reaction([("mfp",1)], [("hsp",1)], [("mfp",1)]) - r.add_reaction([("hsp:mfp",1)], [], [("hsp",1),("prot",1)]) - r.add_reaction_inc("temp", "heat", [("temp",1)],[("temp",max_temp)]) - r.add_reaction_dec("temp", "cool", [("temp",1)],[]) + r = ReactionSystemWithConcentrations() + r.add_bg_set_entity(("hsp", 1)) + r.add_bg_set_entity(("hsf", 1)) + r.add_bg_set_entity(("hsf2", 1)) + r.add_bg_set_entity(("hsf3", 1)) + r.add_bg_set_entity(("hse", 1)) + r.add_bg_set_entity(("mfp", 1)) + r.add_bg_set_entity(("prot", 1)) + r.add_bg_set_entity(("hsf3:hse", 1)) + r.add_bg_set_entity(("hsp:mfp", 1)) + r.add_bg_set_entity(("hsp:hsf", 1)) + r.add_bg_set_entity(("temp", max_temp)) + r.add_bg_set_entity(("heat", 1)) + r.add_bg_set_entity(("cool", 1)) - r.add_permanency("temp",[("heat",1),("cool",1)]) + r.add_reaction([("hsf", 1)], [("hsp", 1)], [("hsf3", 1)]) + r.add_reaction([("hsf", 1), ("hsp", 1), ("mfp", 1)], [], [("hsf3", 1)]) + 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([("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([("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)], [("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)]) + r.add_reaction([("mfp", 1)], [("hsp", 1)], [("mfp", 1)]) + r.add_reaction([("hsp:mfp", 1)], [], [("hsp", 1), ("prot", 1)]) + + r.add_reaction_inc("temp", "heat", [("temp", 1)], [("temp", max_temp)]) + r.add_reaction_dec("temp", "cool", [("temp", 1)], []) + + r.add_permanency("temp", [("heat", 1), ("cool", 1)]) c = ContextAutomatonWithConcentrations(r) c.add_init_state("0") c.add_state("1") - c.add_transition("0", [("hsf",1),("prot",1),("hse",1),("temp",35)], "1") - c.add_transition("1", [("cool",1)], "1") - c.add_transition("1", [("heat",1)], "1") + c.add_transition("0", [("hsf", 1), ("prot", 1), ("hse", 1), ("temp", 35)], "1") + c.add_transition("1", [("cool", 1)], "1") + c.add_transition("1", [("heat", 1)], "1") c.add_transition("1", [], "1") - rc = ReactionSystemWithAutomaton(r,c) - + rc = ReactionSystemWithAutomaton(r, c) + if print_system: rc.show() - - prop_req = [ ("mfp",1) ] - prop_block = [ ] - prop = (prop_req,prop_block) - rs_prop = (state_translate_rsc2rs(prop_req),state_translate_rsc2rs(prop_block)) - + + prop_req = [("mfp", 1)] + prop_block = [] + prop = (prop_req, prop_block) + rs_prop = (state_translate_rsc2rs(prop_req), state_translate_rsc2rs(prop_block)) + if verify_rsc: smt_rsc = SmtCheckerRSC(rc) - smt_rsc.check_reachability(prop,max_level=40) + smt_rsc.check_reachability(prop, max_level=40) else: orc = rc.get_ordinary_reaction_system_with_automaton() if print_system: @@ -117,10 +124,10 @@ def state_translate_rsc2rs(p): def main(): - heat_shock_response() + if __name__ == "__main__": main() - + # EOF diff --git a/examples/smt/mutex_param.py b/examples/smt/mutex_param.py old mode 100644 new mode 100755 index 5a5ff15..ae51160 --- a/examples/smt/mutex_param.py +++ b/examples/smt/mutex_param.py @@ -42,7 +42,7 @@ def powerset(iterable, N=None): def mutex_param_bench(cmd_args): """ Mutex Benchmark - + Parametric """ @@ -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)]) @@ -189,7 +188,7 @@ def mutex_param_bench(cmd_args): def mutex_nonparam_bench(cmd_args): """ Mutex Benchmark - + Parametric """ @@ -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)]) @@ -297,7 +295,7 @@ def mutex_nonparam_bench(cmd_args): def mutex_nonparam_bench_oldimpl(cmd_args): """ Mutex Benchmark - + Parametric """ @@ -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,17 +418,16 @@ def mutex_bench_main(cmd_args): def main(): - parser = argparse.ArgumentParser() parser.add_argument( "scaling", help="scaling parameter value", ) - + 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)", ) @@ -447,7 +442,7 @@ def main(): ) args = parser.parse_args() - + mutex_bench_main(args) diff --git a/examples/smt/scalable_chain.py b/examples/smt/scalable_chain.py old mode 100644 new mode 100755 index d129704..71d11e2 --- a/examples/smt/scalable_chain.py +++ b/examples/smt/scalable_chain.py @@ -31,76 +31,102 @@ from itertools import chain, combinations import sys import resource + def generate_system(chainLen, maxConc): """ This function generates the reaction system with concentrations for the scalable chain benchmark - + chainLen is the length of the chain maxConc is the maximal concentration """ - - r = ReactionSystemWithConcentrations() - r.add_bg_set_entity(("inc",1)) - r.add_bg_set_entity(("dec",1)) - - for i in range(1,chainLen+1): - r.add_bg_set_entity(("e_" + str(i),maxConc)) - - for i in range(1,chainLen+1): - ent = "e_" + str(i) - r.add_reaction_inc(ent, "inc", [(ent, 1)],[(ent,maxConc)]) - r.add_reaction_dec(ent, "dec", [(ent, 1)],[]) - 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 = ReactionSystemWithConcentrations() + r.add_bg_set_entity(("inc", 1)) + r.add_bg_set_entity(("dec", 1)) + + for i in range(1, chainLen + 1): + r.add_bg_set_entity(("e_" + str(i), maxConc)) + + for i in range(1, chainLen + 1): + ent = "e_" + str(i) + r.add_reaction_inc(ent, "inc", [(ent, 1)], [(ent, maxConc)]) + r.add_reaction_dec(ent, "dec", [(ent, 1)], []) + 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)], + ) + c = ContextAutomatonWithConcentrations(r) c.add_init_state("init") c.add_state("working") - c.add_transition("init", [("e_1",1),("inc",1)], "working") - c.add_transition("working", [("inc",1)], "working") - - rc = ReactionSystemWithAutomaton(r,c) + c.add_transition("init", [("e_1", 1), ("inc", 1)], "working") + c.add_transition("working", [("inc", 1)], "working") + + rc = ReactionSystemWithAutomaton(r, c) return rc + def generate_formula(formula_number, chainLen, maxConc): """ - This function generates the rsLTL formula + This function generates the rsLTL formula corresponding to the formula_number parameter """ 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) ) - 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, + (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), + ) 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 - + assert ret is not None, "Unknown formula" return ret @@ -110,64 +136,64 @@ def save_statistics(smt_rsc, formula_number, chainLen, maxConc): """ Saves the statistics fetched from smt_rsc into files """ - time=0 - mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024) - filename_t="bench_rsc_F" + str(formula_number) + "_time.log" - filename_m="bench_rsc_F" + str(formula_number) + "_mem.log" - time=smt_rsc.get_verification_time() + time = 0 + mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024) + filename_t = "bench_rsc_F" + str(formula_number) + "_time.log" + filename_m = "bench_rsc_F" + str(formula_number) + "_mem.log" + time = smt_rsc.get_verification_time() - f=open(filename_t, 'a') - log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n" + 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') - log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n" + + f = open(filename_m, "a") + log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n" f.write(log_str) f.close() - + def scalable_chain(print_system=False): """ This is the entry point for the benchmark """ - if len(sys.argv) < 1+3: + if len(sys.argv) < 1 + 3: print("arguments: ") exit(1) - chainLen=int(sys.argv[1]) # chain length - maxConc=int(sys.argv[2]) # depth (max concentration) - formula_number=int(sys.argv[3]) - + chainLen = int(sys.argv[1]) # chain length + maxConc = int(sys.argv[2]) # depth (max concentration) + formula_number = int(sys.argv[3]) + if chainLen < 1 or maxConc < 1: print("be reasonable") exit(1) - if not formula_number in range(1,5+1): + if not formula_number in range(1, 5 + 1): print("formulaNumber must be in 1..5") exit(1) - + # Generate the reaction systems with concentrations rc = generate_system(chainLen, maxConc) - + # Generate the formula form = generate_formula(formula_number, chainLen, maxConc) - + # Optional dump/print of the system if print_system: rc.show() - + # Create an instance of the SMT checker for RS with concentrations smt_rsc = SmtCheckerRSC(rc) - + # Start the verification process smt_rsc.check_rsltl(formula=form) - + save_statistics(smt_rsc, formula_number, chainLen, maxConc) - - + + def main(): scalable_chain(print_system=True) + if __name__ == "__main__": main() - diff --git a/experiments/drs_cell_signal/run.sh b/experiments/drs_cell_signal/run.sh new file mode 100755 index 0000000..e514361 --- /dev/null +++ b/experiments/drs_cell_signal/run.sh @@ -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 " + 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 diff --git a/experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat b/experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat new file mode 100644 index 0000000..75c8ef6 --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat @@ -0,0 +1,20 @@ +2 69.171875 +3 69.937500 +4 86.109375 +5 76.093750 +6 81.812500 +7 97.078125 +8 88.562500 +9 102.968750 +10 93.546875 +11 98.515625 +12 113.671875 +13 115.656250 +14 132.140625 +15 141.546875 +16 149.890625 +17 155.125000 +18 153.500000 +19 166.953125 +20 169.750000 +21 212.468750 diff --git a/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat b/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat new file mode 100644 index 0000000..ed1a7a8 --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat @@ -0,0 +1,20 @@ +2 68.765625 +3 73.140625 +4 71.625000 +5 73.359375 +6 79.234375 +7 75.578125 +8 79.812500 +9 85.828125 +10 81.718750 +11 79.828125 +12 83.984375 +13 80.406250 +14 75.859375 +15 85.812500 +16 89.093750 +17 84.296875 +18 89.078125 +19 87.609375 +20 88.281250 +21 85.406250 diff --git a/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat b/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat new file mode 100644 index 0000000..a8311e3 --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat @@ -0,0 +1,20 @@ +2 0.068995 +3 0.110615 +4 0.164639 +5 0.234950 +6 0.322793 +7 0.438878 +8 0.578109 +9 0.752163 +10 0.955217 +11 1.190432 +12 1.519409 +13 1.808177 +14 2.200211 +15 2.654874 +16 3.265984 +17 3.824895 +18 4.413004 +19 5.303216 +20 6.310782 +21 7.038971 diff --git a/experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat b/experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat new file mode 100644 index 0000000..4ac4eed --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat @@ -0,0 +1,20 @@ +2 0.095321 +3 0.171177 +4 0.272130 +5 0.417800 +6 0.584877 +7 0.766862 +8 1.009195 +9 1.295766 +10 1.741482 +11 2.354580 +12 2.949242 +13 3.127326 +14 4.074318 +15 4.978959 +16 6.690042 +17 8.114637 +18 12.006410 +19 11.929118 +20 14.044730 +21 15.673520 diff --git a/experiments/reaction_mining_mutex/bench_mutex_param_mem.dat b/experiments/reaction_mining_mutex/bench_mutex_param_mem.dat new file mode 100644 index 0000000..3f84c8e --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_param_mem.dat @@ -0,0 +1,20 @@ +2 80.093750 +3 76.062500 +4 88.312500 +5 97.140625 +6 95.234375 +7 109.843750 +8 111.218750 +9 132.921875 +10 142.546875 +11 151.546875 +12 175.546875 +13 186.109375 +14 206.546875 +15 235.281250 +16 245.515625 +17 249.562500 +18 260.203125 +19 278.796875 +20 292.781250 +21 300.562500 diff --git a/experiments/reaction_mining_mutex/bench_mutex_param_time.dat b/experiments/reaction_mining_mutex/bench_mutex_param_time.dat new file mode 100644 index 0000000..eb244af --- /dev/null +++ b/experiments/reaction_mining_mutex/bench_mutex_param_time.dat @@ -0,0 +1,20 @@ +2 0.487115 +3 0.880007 +4 1.301547 +5 2.172839 +6 2.662308 +7 3.880329 +8 4.491871 +9 6.922392 +10 8.729740 +11 10.901971 +12 13.885037 +13 18.246820 +14 21.987255 +15 28.236579 +16 41.065607 +17 44.456013 +18 50.782835 +19 59.535617 +20 83.400427 +21 96.250559 diff --git a/experiments/reaction_mining_mutex/pmutex.py b/experiments/reaction_mining_mutex/pmutex.py new file mode 100755 index 0000000..3564725 --- /dev/null +++ b/experiments/reaction_mining_mutex/pmutex.py @@ -0,0 +1,454 @@ +#!/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)] + ) + + ################################################### + + 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 diff --git a/experiments/reaction_mining_mutex/run_mutex_param.sh b/experiments/reaction_mining_mutex/run_mutex_param.sh new file mode 100755 index 0000000..ccb2082 --- /dev/null +++ b/experiments/reaction_mining_mutex/run_mutex_param.sh @@ -0,0 +1,26 @@ +#!/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 -eq 1 ]] + then + $REACTICS_SCRIPT $i $special_mode + $REACTICS_SCRIPT -o $i $special_mode + else + $REACTICS_SCRIPT $i $special_mode + fi + done +done + diff --git a/reactics b/reactics index 4cc8de4..b4da96b 100755 --- a/reactics +++ b/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" ]] diff --git a/rs_testing.py b/reactics-smt/rs_testing.py similarity index 100% rename from rs_testing.py rename to reactics-smt/rs_testing.py