clean-up

examples/bdd/generators/gen_drs.py

@@ -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()

examples/bdd/generators/gen_tgc.py

@@ -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)
-

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} <N> <M> <type>".format(source=sys.argv[0]))
         print()
@@ -115,7 +114,6 @@ def chain_reaction(print_system=False):
 
 
 def main():
-
     chain_reaction()
 
 

examples/smt/heat_shock_response.py

@@ -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()
 

examples/smt/mutex_param.py

@@ -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)",
     )
 

examples/smt/scalable_chain.py

@@ -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()
-

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 <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

experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat

@@ -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

experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat

@@ -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

experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat

@@ -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

experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat

@@ -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

experiments/reaction_mining_mutex/bench_mutex_param_mem.dat

@@ -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

experiments/reaction_mining_mutex/bench_mutex_param_time.dat

@@ -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

experiments/reaction_mining_mutex/pmutex.py

@@ -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

experiments/reaction_mining_mutex/run_mutex_param.sh

@@ -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
+

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" ]]

reactics-smt/rs/reaction_system.py

@@ -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")