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

@@ -1,6 +1,6 @@
 #!/usr/bin/env python
 
-from sys import argv,exit
+from sys import argv, exit
 
 OPTIONS_STR = """
 options { use-context-automaton; make-progressive; };
@@ -51,57 +51,67 @@ out += "};\n"
 
 transitions = ""
 
-init_trans = 8*" " + "{ "
+init_trans = 8 * " " + "{ "
 for i in range(n):
     init_trans += "proc{:d}={{out}} ".format(i)
 init_trans += "}: init -> green;\n"
 transitions += init_trans
 
 for i in range(n):
-    transitions += "{:s}{{ proc{:d}={{allowed}} }}: green -> red : proc{:d}.req;\n".format(8*" ", i, i)
+    transitions += (
+        "{:s}{{ proc{:d}={{allowed}} }}: green -> red : proc{:d}.req;\n".format(
+            8 * " ", i, i
+        )
+    )
 
 no_req_cond = "~proc0.req"
 for i in range(1, n):
     no_req_cond += " AND ~proc{:d}.req".format(i)
 
 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)
 
 ## f1
-#formula = "EF( proc0.in )"
-#out += PROPERTY_STR.format("f1",formula)
+# formula = "EF( proc0.in )"
+# out += PROPERTY_STR.format("f1",formula)
 
 # f1
 formula = "EF( E<proc0.allowed>X( proc0.in ) )"
 for i in range(1, n):
     formula += " AND EF( E<proc{:d}.allowed>X( proc{:d}.in ) )".format(i, i)
-out += PROPERTY_STR.format("f1",formula)
+out += PROPERTY_STR.format("f1", formula)
 
 # f2
 formula = "EF( proc0.approach"
 for i in range(1, n):
     formula += " AND proc{:d}.approach".format(i)
 formula += " )"
-out += PROPERTY_STR.format("f2",formula)
+out += PROPERTY_STR.format("f2", formula)
 
 # f3
 subf = "~proc1.in"
 for i in range(2, n):
     subf += " AND ~proc{:d}.in".format(i)
 formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
-out += PROPERTY_STR.format("f3",formula)
+out += PROPERTY_STR.format("f3", formula)
 
 # f4
 subf = "~proc1.in"
@@ -110,8 +120,7 @@ for i in range(2, n):
 all_agents = "proc0"
 for i in range(1, n):
     all_agents += ",proc{:d}".format(i)
-formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents,subf)
-out += PROPERTY_STR.format("f4",formula)
+formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents, subf)
+out += PROPERTY_STR.format("f4", formula)
 
 print(out)
-

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,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} <type>".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_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([("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_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)])
+    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,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
@@ -41,31 +42,36 @@ def generate_system(chainLen, maxConc):
     """
 
     r = ReactionSystemWithConcentrations()
-    r.add_bg_set_entity(("inc",1))
-    r.add_bg_set_entity(("dec",1))
+    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):
+        r.add_bg_set_entity(("e_" + str(i), maxConc))
 
-    for i in range(1,chainLen+1):
+    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)],[])
+        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([(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")
     c.add_state("working")
-    c.add_transition("init", [("e_1",1),("inc",1)], "working")
-    c.add_transition("working", [("inc",1)], "working")
+    c.add_transition("init", [("e_1", 1), ("inc", 1)], "working")
+    c.add_transition("working", [("inc", 1)], "working")
 
-    rc = ReactionSystemWithAutomaton(r,c)
+    rc = ReactionSystemWithAutomaton(r, c)
 
     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) )
-        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
@@ -110,19 +136,19 @@ 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()
 
@@ -131,18 +157,18 @@ 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: <chainLen> <maxConc> <formulaNumber>")
         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)
 
@@ -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

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # 
 # Copyright (c) 2019 Artur Meski
@@ -52,16 +52,24 @@ then
   then
     python3 $* 
   else
-    echo "Nothing to do"
+    echo "Provide path to an example script (typically from ./examples/smt)"
   fi
   
 elif [[ "$mode" == "setup" ]]
 then
 
+  which -s gmake
+  if [[ $? -eq 0 ]]
+  then
+    MAKE="gmake"
+  else
+    MAKE="make"
+  fi
+
   git pull
   cd $REACTICS_BDD
   ./build_cudd.sh
-  make
+  $MAKE
 
 else
   

reactics-bdd/ctx_aut.cc

@@ -1,7 +1,7 @@
 
 #include "ctx_aut.hh"
-#include "rs.hh"
 #include "macro.hh"
+#include "rs.hh"
 #include "stateconstr.hh"
 
 CtxAut::CtxAut(Options *opts, RctSys *parent_rctsys)
@@ -75,12 +75,14 @@ void CtxAut::printAutomaton(void)
 
 void CtxAut::showStates(void)
 {
+  if (states_ids.size() > 0) {
     cout << "# Context Automaton States:" << endl;
     cout << " = Init state: " << getStateName(init_state_id) << endl;
 
     for (const auto &s : states_ids) {
       cout << " * " << s << endl;
     }
+  }
 }
 
 void CtxAut::pushContextEntity(Entity entity_id)
@@ -98,7 +100,8 @@ void CtxAut::saveCurrentContextSet(Process proc_id)
   tmpEntities.clear();
 }
 
-void CtxAut::addTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr)
+void CtxAut::addTransition(std::string srcStateName, std::string dstStateName,
+                           StateConstr *stateConstr)
 {
   VERB_L3("Saving transition");
 
@@ -115,12 +118,17 @@ void CtxAut::addTransition(std::string srcStateName, std::string dstStateName, S
 
 void CtxAut::showTransitions(void)
 {
+  if (transitions.size() == 0) {
+    cout << "Empty context automaton" << endl;
+    return;
+  }
+
   cout << "# Context Automaton Transitions:" << endl;
 
   for (const auto &t : transitions) {
-    cout << " * [" << getStateName(t.src_state) << " -> " << getStateName(
-           t.dst_state)
-         << "]: { " << parent_rctsys->procEntitiesToStr(t.ctx) << "}";
+    cout << " * [" << getStateName(t.src_state) << " -> "
+         << getStateName(t.dst_state) << "]: { "
+         << parent_rctsys->procEntitiesToStr(t.ctx) << "}";
 
     if (t.state_constr != nullptr) {
       cout << " " << t.state_constr->toStr();
@@ -162,8 +170,8 @@ void CtxAut::makeProgressive(void)
     State curr_st = t.src_state;
 
     if (t.state_constr != nullptr) {
-      constrs[curr_st] = new StateConstr(
-        STC_OR, constrs[curr_st], t.state_constr);
+      constrs[curr_st] =
+        new StateConstr(STC_OR, constrs[curr_st], t.state_constr);
     }
   }
 
@@ -174,13 +182,11 @@ void CtxAut::makeProgressive(void)
       state_constr = new StateConstr(STC_NOT, constrs[getStateID(s)]);
       addTransition(s, special_loc, state_constr);
     }
-
   }
 
   addTransition(special_loc, special_loc, nullptr);
 
   made_progressive = true;
-
 }
 
 /** EOF **/

reactics-bdd/mc.cc

@@ -198,7 +198,14 @@ void ModelChecker::printReachWithSucc(void)
   while (!unproc.IsZero()) {
     BDD t;
     t = unproc.PickOneMinterm(*pv);
+    if (opts->backend_mode)
+    {
+        cout << "G " << srs->decodedRctSysStateToStr(t) << endl;
+    }
+    else
+    {
         cout << "Successors of " << srs->decodedRctSysStateToStr(t) << ":" << endl;
+    }
     srs->printDecodedRctSysStates(getSucc(t));
     unproc -= t;
   }
@@ -594,8 +601,12 @@ bool ModelChecker::checkRSCTLKfull(FormRSCTLK *form)
 
   cleanup();
 
+  if (opts->backend_mode) {
+      cout << "Result:" << result << endl;
+  } else {
       cout << "Formula " << form->toStr() << (result ? " holds" : " does not hold")
            << endl;
+  }
 
   if (opts->measure) {
     opts->ver_time = cpuTime() - opts->ver_time;
@@ -658,8 +669,12 @@ bool ModelChecker::checkRSCTLKbmc(FormRSCTLK *form)
 
   cleanup();
 
+  if (opts->backend_mode) {
+      cout << "result:" << result << endl;
+  } else {
       cout << "Formula " << form->toStr() << " " << (result ? "holds" :
            "does not hold") << endl;
+  }
 
   if (opts->measure) {
     opts->ver_time = cpuTime() - opts->ver_time;

reactics-bdd/options.hh

@@ -11,6 +11,7 @@ class Options
     bool part_tr_rel;
     bool reorder_reach;
     bool reorder_trans;
+    bool backend_mode;
 
     double enc_time;
     double enc_mem;
@@ -28,6 +29,8 @@ class Options
       reorder_reach = false;
       reorder_trans = false;
 
+      backend_mode = false;
+
       enc_time = 0;
       enc_mem = 0;
       ver_time = 0;

reactics-bdd/reactics.cc

@@ -31,7 +31,7 @@ int main(int argc, char **argv)
   int c;
   int option_index = 0;
 
-  while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvxzh", long_options,
+  while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvxzXh", long_options,
                           &option_index)) != -1) {
     switch (c) {
       case 0:
@@ -106,6 +106,10 @@ int main(int argc, char **argv)
         opts->reorder_trans = true;
         break;
 
+      case 'X':
+        opts->backend_mode = true;
+        break;
+
       case 'h':
         dump_help_message = true;
         break;
@@ -259,6 +263,8 @@ void print_help(std::string path_str)
        endl
        << "  -p       -- show progress (where possible)" << endl
        << endl
+       << "  -X       -- backend mode (makes output parsing easier)" << endl
+       << endl
        << " Benchmarking options:" << endl
        << "  -m       -- measure and display time and memory usage" << endl
        << "  -B       -- display an easy to parse summary (enables -m)" << endl

reactics-bdd/symrs.cc

@@ -573,7 +573,14 @@ void SymRS::printDecodedRctSysStates(const BDD &states)
 
   while (!unproc.IsZero()) {
     BDD t = unproc.PickOneMinterm(*pv_drs_flat);
+    if (opts->backend_mode)
+    {
+        cout << "s " << decodedRctSysStateToStr(t) << endl;
+    }
+    else
+    {
         cout << decodedRctSysStateToStr(t) << endl;
+    }
 
     if (opts->verbose > 9) {
       BDD_PRINT(t);

reactics-smt/colour.py

@@ -1,11 +1,11 @@
-C_HEADER = '\033[95m'
-C_BLUE = '\033[94m'
-C_GREEN = '\033[92m'
-C_SOMEOTHER = '\033[93m'
-C_RED = '\033[91m'
-C_ENDC = '\033[0m'
-C_BOLD = '\033[1m'
-C_UNDERLINE = '\033[4m'
+C_HEADER = "\033[95m"
+C_BLUE = "\033[94m"
+C_GREEN = "\033[92m"
+C_SOMEOTHER = "\033[93m"
+C_RED = "\033[91m"
+C_ENDC = "\033[0m"
+C_BOLD = "\033[1m"
+C_UNDERLINE = "\033[4m"
 
 C_MARK_INFO = C_BOLD + "[" + C_GREEN + "*" + C_ENDC + C_BOLD + "]" + C_ENDC
 C_MARK_ERROR = C_BOLD + "[" + C_RED + "!" + C_ENDC + C_BOLD + "]" + C_ENDC
@@ -30,4 +30,5 @@ def print_info(s):
 def print_positive(s):
     print("[" + colour_str(C_BOLD, "+") + "] {:s}".format(s))
 
+
 # EOF

reactics-smt/doc/overview.py

@@ -5,19 +5,19 @@ from smt import *
 from logics import *
 from rsltl_shortcuts import *
 
-def ex():
 
+def ex():
     prs = ReactionSystemWithConcentrationsParam()
 
-    ent_with_conc = [("a", 3), ("b",2), ("c",1), ("h",1)]
+    ent_with_conc = [("a", 3), ("b", 2), ("c", 1), ("h", 1)]
 
     for ec in ent_with_conc:
         prs.add_bg_set_entity(ec)
 
     lda = prs.get_param("lda")
 
-    prs.add_reaction([("a",1)],[("h",1)],[("b", 2)])
-    prs.add_reaction(lda,[("h",1)],[("c",1)])
+    prs.add_reaction([("a", 1)], [("h", 1)], [("b", 2)])
+    prs.add_reaction(lda, [("h", 1)], [("c", 1)])
 
     ##
 
@@ -38,6 +38,7 @@ def ex():
     checker = SmtCheckerRSCParam(crprs, optimise=True)
     checker.check_rsltl(formulae_list=[f], param_constr=pc)
 
+
 if __name__ == "__main__":
     ex()
 

reactics-smt/logics/bags.py

@@ -1,10 +1,9 @@
 from enum import Enum
-BagDesc_oper = Enum(
-    'BagDesc_oper', 'entity true l_and l_or l_not lt le eq ge gt')
+
+BagDesc_oper = Enum("BagDesc_oper", "entity true l_and l_or l_not lt le eq ge gt")
 
 
 class BagDescription(object):
-
     def __init__(self, f_type, L_oper=None, R_oper=None, entity=""):
         self.f_type = f_type
         self.left_operand = L_oper
@@ -19,9 +18,13 @@ class BagDescription(object):
         if self.f_type == BagDesc_oper.true:
             return "TRUE"
         if self.f_type == BagDesc_oper.l_and:
-            return "(" + repr(self.left_operand) + " & " + repr(self.right_operand) + ")"
+            return (
+                "(" + repr(self.left_operand) + " & " + repr(self.right_operand) + ")"
+            )
         if self.f_type == BagDesc_oper.l_or:
-            return "(" + repr(self.left_operand) + " | " + repr(self.right_operand) + ")"
+            return (
+                "(" + repr(self.left_operand) + " | " + repr(self.right_operand) + ")"
+            )
         if self.f_type == BagDesc_oper.l_not:
             return "~(" + repr(self.left_operand) + ")"
         if self.f_type == BagDesc_oper.lt:
@@ -39,12 +42,14 @@ class BagDescription(object):
         """Sanity checks"""
         for operand in (self.left_operand, self.right_operand):
             if operand:
-                if not(
-                        isinstance(operand, BagDescription)
-                        or isinstance(operand, int)):
+                if not (
+                    isinstance(operand, BagDescription) or isinstance(operand, int)
+                ):
                     raise RuntimeError(
                         "Unexpected operand type for a bag: {:s} (type: {:s})".format(
-                            str(operand), str(type(operand))))
+                            str(operand), str(type(operand))
+                        )
+                    )
 
     @classmethod
     def f_entity(cls, entity_name):
@@ -86,4 +91,5 @@ class BagDescription(object):
     def __invert__(self):
         return BagDescription(BagDesc_oper.l_not, L_oper=self)
 
+
 # EOF

reactics-smt/logics/param_constr.py

@@ -1,11 +1,11 @@
 from enum import Enum
+
 ParamConstraint_oper = Enum(
-    'ParamConstraint_oper',
-    'param_entity true l_and l_or l_not lt le eq ge gt')
+    "ParamConstraint_oper", "param_entity true l_and l_or l_not lt le eq ge gt"
+)
 
 
 class ParamConstraint(object):
-
     def __init__(self, f_type, L_oper=None, R_oper=None, param=None, entity=""):
         self.f_type = f_type
         self.left_operand = L_oper
@@ -21,9 +21,13 @@ class ParamConstraint(object):
         if self.f_type == ParamConstraint_oper.true:
             return "TRUE"
         if self.f_type == ParamConstraint_oper.l_and:
-            return "(" + repr(self.left_operand) + " & " + repr(self.right_operand) + ")"
+            return (
+                "(" + repr(self.left_operand) + " & " + repr(self.right_operand) + ")"
+            )
         if self.f_type == ParamConstraint_oper.l_or:
-            return "(" + repr(self.left_operand) + " | " + repr(self.right_operand) + ")"
+            return (
+                "(" + repr(self.left_operand) + " | " + repr(self.right_operand) + ")"
+            )
         if self.f_type == ParamConstraint_oper.l_not:
             return "~(" + repr(self.left_operand) + ")"
         if self.f_type == ParamConstraint_oper.lt:
@@ -41,17 +45,18 @@ class ParamConstraint(object):
         """Sanity checks"""
         for operand in (self.left_operand, self.right_operand):
             if operand:
-                if not(
-                        isinstance(operand, ParamConstraint)
-                        or isinstance(operand, int)):
+                if not (
+                    isinstance(operand, ParamConstraint) or isinstance(operand, int)
+                ):
                     raise RuntimeError(
                         "Unexpected operand type for a bag: {:s} (type: {:s})".format(
-                            str(operand), str(type(operand))))
+                            str(operand), str(type(operand))
+                        )
+                    )
 
     @classmethod
     def f_param_ent(cls, param, entity_name):
-        return cls(ParamConstraint_oper.param_entity, param=param,
-                   entity=entity_name)
+        return cls(ParamConstraint_oper.param_entity, param=param, entity=entity_name)
 
     @classmethod
     def f_TRUE(cls):
@@ -66,34 +71,28 @@ class ParamConstraint(object):
         return cls(ParamConstraint_oper.l_not, L_oper=arg)
 
     def __lt__(self, other):
-        return ParamConstraint(
-            ParamConstraint_oper.lt, L_oper=self, R_oper=other)
+        return ParamConstraint(ParamConstraint_oper.lt, L_oper=self, R_oper=other)
 
     def __le__(self, other):
-        return ParamConstraint(
-            ParamConstraint_oper.le, L_oper=self, R_oper=other)
+        return ParamConstraint(ParamConstraint_oper.le, L_oper=self, R_oper=other)
 
     def __eq__(self, other):
-        return ParamConstraint(
-            ParamConstraint_oper.eq, L_oper=self, R_oper=other)
+        return ParamConstraint(ParamConstraint_oper.eq, L_oper=self, R_oper=other)
 
     def __ge__(self, other):
-        return ParamConstraint(
-            ParamConstraint_oper.ge, L_oper=self, R_oper=other)
+        return ParamConstraint(ParamConstraint_oper.ge, L_oper=self, R_oper=other)
 
     def __gt__(self, other):
-        return ParamConstraint(
-            ParamConstraint_oper.gt, L_oper=self, R_oper=other)
+        return ParamConstraint(ParamConstraint_oper.gt, L_oper=self, R_oper=other)
 
     def __and__(self, other):
-        return ParamConstraint(
-            ParamConstraint_oper.l_and, L_oper=self, R_oper=other)
+        return ParamConstraint(ParamConstraint_oper.l_and, L_oper=self, R_oper=other)
 
     def __or__(self, other):
-        return ParamConstraint(
-            ParamConstraint_oper.l_or, L_oper=self, R_oper=other)
+        return ParamConstraint(ParamConstraint_oper.l_or, L_oper=self, R_oper=other)
 
     def __invert__(self):
         return ParamConstraint(ParamConstraint_oper.l_not, L_oper=self)
 
+
 # EOF

reactics-smt/logics/param_constr_encoder.py

@@ -14,57 +14,60 @@ class ParamConstr_Encoder(object):
         # self.loop_position = None
 
     def load_variables(self, var_rs, var_ctx, var_loop_pos):
-
         self.v = var_rs
         self.v_ctx = var_ctx
         self.loop_position = var_loop_pos
 
     def encode(self, param_constr):
-
         if not param_constr:
             raise RuntimeError("param_constr is None")
 
         if param_constr.f_type == ParamConstraint_oper.param_entity:
             return self.smt_checker.get_enc_param(
-                param_constr.param.name, param_constr.entity)
+                param_constr.param.name, param_constr.entity
+            )
 
         if param_constr.f_type == ParamConstraint_oper.true:
             return True
 
         if param_constr.f_type == ParamConstraint_oper.l_and:
-            return And(self.encode(param_constr.left_operand),
-                       self.encode(param_constr.right_operand))
+            return And(
+                self.encode(param_constr.left_operand),
+                self.encode(param_constr.right_operand),
+            )
 
         if param_constr.f_type == ParamConstraint_oper.l_or:
-            return Or(self.encode(param_constr.left_operand),
-                      self.encode(param_constr.right_operand))
+            return Or(
+                self.encode(param_constr.left_operand),
+                self.encode(param_constr.right_operand),
+            )
 
         if param_constr.f_type == ParamConstraint_oper.l_not:
             return Not(self.encode(param_constr.left_operand))
 
         if param_constr.f_type == ParamConstraint_oper.lt:
-            return self.encode(
-                param_constr.left_operand) < int(
-                param_constr.right_operand)
+            return self.encode(param_constr.left_operand) < int(
+                param_constr.right_operand
+            )
 
         if param_constr.f_type == ParamConstraint_oper.le:
-            return self.encode(
-                param_constr.left_operand) <= int(
-                param_constr.right_operand)
+            return self.encode(param_constr.left_operand) <= int(
+                param_constr.right_operand
+            )
 
         if param_constr.f_type == ParamConstraint_oper.eq:
-            return self.encode(
-                param_constr.left_operand) == int(
-                param_constr.right_operand)
+            return self.encode(param_constr.left_operand) == int(
+                param_constr.right_operand
+            )
 
         if param_constr.f_type == ParamConstraint_oper.ge:
-            return self.encode(
-                param_constr.left_operand) >= int(
-                param_constr.right_operand)
+            return self.encode(param_constr.left_operand) >= int(
+                param_constr.right_operand
+            )
 
         if param_constr.f_type == ParamConstraint_oper.gt:
-            return self.encode(
-                param_constr.left_operand) > int(
-                param_constr.right_operand)
+            return self.encode(param_constr.left_operand) > int(
+                param_constr.right_operand
+            )
 
         assert False, "Unsupported case {:s}".format(param_constr.f_type)

reactics-smt/logics/rsltl.py

@@ -4,14 +4,13 @@ from enum import Enum
 from logics.bags import *
 
 rsLTL_form_type = Enum(
-    'rsLTL_form_type',
-    'bag l_and l_or l_not l_implies t_globally t_finally t_next t_until t_release')
+    "rsLTL_form_type",
+    "bag l_and l_or l_not l_implies t_globally t_finally t_next t_until t_release",
+)
 
 
 class Formula_rsLTL(object):
-
-    def __init__(
-            self, f_type, L_oper=None, R_oper=None, sub_oper=None, bag=None):
+    def __init__(self, f_type, L_oper=None, R_oper=None, sub_oper=None, bag=None):
         self.f_type = f_type
         self.left_operand = L_oper
         self.right_operand = R_oper
@@ -21,7 +20,10 @@ class Formula_rsLTL(object):
         # it's silly, but it's a frequent mistake
         if callable(sub_oper):
             raise RuntimeError(
-                "sub_oper should not be a function. Missing () for {0}?".format(sub_oper))
+                "sub_oper should not be a function. Missing () for {0}?".format(
+                    sub_oper
+                )
+            )
 
         if isinstance(self.left_operand, BagDescription):
             self.left_operand = Formula_rsLTL.f_bag(self.left_operand)
@@ -43,21 +45,37 @@ class Formula_rsLTL(object):
         if self.f_type == rsLTL_form_type.t_next:
             return "X[" + repr(self.sub_operand) + "](" + repr(self.left_operand) + ")"
         if self.f_type == rsLTL_form_type.l_and:
-            return "(" + repr(self.left_operand) + " & " + repr(self.right_operand) + ")"
+            return (
+                "(" + repr(self.left_operand) + " & " + repr(self.right_operand) + ")"
+            )
         if self.f_type == rsLTL_form_type.l_or:
-            return "(" + repr(self.left_operand) + " | " + repr(self.right_operand) + ")"
+            return (
+                "(" + repr(self.left_operand) + " | " + repr(self.right_operand) + ")"
+            )
         if self.f_type == rsLTL_form_type.l_implies:
-            return "(" + repr(self.left_operand) + " => " + repr(self.right_operand) + ")"
+            return (
+                "(" + repr(self.left_operand) + " => " + repr(self.right_operand) + ")"
+            )
         if self.f_type == rsLTL_form_type.t_until:
-            return "(" + repr(
-                self.left_operand) + " U[" + repr(
-                self.sub_operand) + "] " + repr(
-                self.right_operand) + ")"
+            return (
+                "("
+                + repr(self.left_operand)
+                + " U["
+                + repr(self.sub_operand)
+                + "] "
+                + repr(self.right_operand)
+                + ")"
+            )
         if self.f_type == rsLTL_form_type.t_release:
-            return "(" + repr(
-                self.left_operand) + " R[" + repr(
-                self.sub_operand) + "] " + repr(
-                self.right_operand) + ")"
+            return (
+                "("
+                + repr(self.left_operand)
+                + " R["
+                + repr(self.sub_operand)
+                + "] "
+                + repr(self.right_operand)
+                + ")"
+            )
 
     @property
     def is_bag(self):
@@ -93,8 +111,7 @@ class Formula_rsLTL(object):
 
     @classmethod
     def f_U(cls, sub, arg_L, arg_R):
-        return cls(
-            rsLTL_form_type.t_until, L_oper=arg_L, R_oper=arg_R, sub_oper=sub)
+        return cls(rsLTL_form_type.t_until, L_oper=arg_L, R_oper=arg_R, sub_oper=sub)
 
     @classmethod
     def f_F(cls, sub, arg_L):
@@ -102,9 +119,7 @@ class Formula_rsLTL(object):
 
     @classmethod
     def f_R(cls, sub, arg_L, arg_R):
-        return cls(
-            rsLTL_form_type.t_release, L_oper=arg_L, R_oper=arg_R,
-            sub_oper=sub)
+        return cls(rsLTL_form_type.t_release, L_oper=arg_L, R_oper=arg_R, sub_oper=sub)
 
     def __and__(self, other):
         return Formula_rsLTL(rsLTL_form_type.l_and, L_oper=self, R_oper=other)

reactics-smt/logics/rsltl_encoder.py

@@ -24,13 +24,11 @@ class rsLTL_Encoder(object):
         self.init_ncalls()
 
     def load_variables(self, var_rs, var_ctx, var_loop_pos):
-
         self.v = var_rs
         self.v_ctx = var_ctx
         self.loop_position = var_loop_pos
 
     def get_encoding(self, formula, bound):
-
         assert self.v is not None
         assert self.v_ctx is not None
         assert self.loop_position is not None
@@ -49,8 +47,8 @@ class rsLTL_Encoder(object):
         Cache for formulae encodings
         """
         self.cache_hits = 0
-        self.enc_fcache = [{} for level in range(0, bound+1)]
-        self.enc_fcache_approx = [{} for level in range(0, bound+1)]
+        self.enc_fcache = [{} for level in range(0, bound + 1)]
+        self.enc_fcache_approx = [{} for level in range(0, bound + 1)]
 
     def cache_save(self, formula, level, formula_encoding):
         self.enc_fcache[level][formula] = formula_encoding
@@ -83,7 +81,6 @@ class rsLTL_Encoder(object):
         return (self.ncalls_encode, self.ncalls_encode_approx)
 
     def encode_bag(self, bag_formula, level, context=False):
-
         if not bag_formula:
             raise RuntimeError("bag_formula is None")
 
@@ -100,41 +97,42 @@ class rsLTL_Encoder(object):
         if bag_formula.f_type == BagDesc_oper.l_and:
             return And(
                 self.encode_bag(bag_formula.left_operand, level, context),
-                self.encode_bag(bag_formula.right_operand, level, context))
+                self.encode_bag(bag_formula.right_operand, level, context),
+            )
 
         if bag_formula.f_type == BagDesc_oper.l_or:
             return Or(
                 self.encode_bag(bag_formula.left_operand, level, context),
-                self.encode_bag(bag_formula.right_operand, level, context))
+                self.encode_bag(bag_formula.right_operand, level, context),
+            )
 
         if bag_formula.f_type == BagDesc_oper.l_not:
-            return Not(self.encode_bag(
-                bag_formula.left_operand, level, context))
+            return Not(self.encode_bag(bag_formula.left_operand, level, context))
 
         if bag_formula.f_type == BagDesc_oper.lt:
-            return self.encode_bag(
-                bag_formula.left_operand, level, context) < int(
-                bag_formula.right_operand)
+            return self.encode_bag(bag_formula.left_operand, level, context) < int(
+                bag_formula.right_operand
+            )
 
         if bag_formula.f_type == BagDesc_oper.le:
-            return self.encode_bag(
-                bag_formula.left_operand, level, context) <= int(
-                bag_formula.right_operand)
+            return self.encode_bag(bag_formula.left_operand, level, context) <= int(
+                bag_formula.right_operand
+            )
 
         if bag_formula.f_type == BagDesc_oper.eq:
-            return self.encode_bag(
-                bag_formula.left_operand, level, context) == int(
-                bag_formula.right_operand)
+            return self.encode_bag(bag_formula.left_operand, level, context) == int(
+                bag_formula.right_operand
+            )
 
         if bag_formula.f_type == BagDesc_oper.ge:
-            return self.encode_bag(
-                bag_formula.left_operand, level, context) >= int(
-                bag_formula.right_operand)
+            return self.encode_bag(bag_formula.left_operand, level, context) >= int(
+                bag_formula.right_operand
+            )
 
         if bag_formula.f_type == BagDesc_oper.gt:
-            return self.encode_bag(
-                bag_formula.left_operand, level, context) > int(
-                bag_formula.right_operand)
+            return self.encode_bag(bag_formula.left_operand, level, context) > int(
+                bag_formula.right_operand
+            )
 
         assert False, "Unsupported case {:s}".format(bag_formula.f_type)
 
@@ -149,7 +147,6 @@ class rsLTL_Encoder(object):
         return res
 
     def encode(self, formula, level, bound):
-
         self.ncalls_encode += 1
 
         from_cache = self.cache_query(formula, level)
@@ -159,12 +156,12 @@ class rsLTL_Encoder(object):
         enc = None
 
         if not isinstance(formula, Formula_rsLTL):
-            raise NotImplementedError(
-                "Unsupported formula type: " + str(type(formula)))
+            raise NotImplementedError("Unsupported formula type: " + str(type(formula)))
 
         if level > bound:
             raise RuntimeError(
-                "level > bound. Unexpected behaviour. The encoding does not support levels higher than a bound.")
+                "level > bound. Unexpected behaviour. The encoding does not support levels higher than a bound."
+            )
 
         if formula.f_type == rsLTL_form_type.bag:
             enc = self.encode_bag_state(formula.bag_descr, level)
@@ -179,33 +176,40 @@ class rsLTL_Encoder(object):
         elif formula.f_type == rsLTL_form_type.l_and:
             enc = And(
                 self.encode(formula.left_operand, level, bound),
-                self.encode(formula.right_operand, level, bound)
+                self.encode(formula.right_operand, level, bound),
             )
 
         elif formula.f_type == rsLTL_form_type.l_or:
             enc = Or(
                 self.encode(formula.left_operand, level, bound),
-                self.encode(formula.right_operand, level, bound)
+                self.encode(formula.right_operand, level, bound),
             )
 
         elif formula.f_type == rsLTL_form_type.l_implies:
             enc = Implies(
                 self.encode(formula.left_operand, level, bound),
-                self.encode(formula.right_operand, level, bound)
+                self.encode(formula.right_operand, level, bound),
             )
 
         elif formula.f_type == rsLTL_form_type.t_next:
             if level < bound:
                 enc = And(
                     self.encode(formula.left_operand, level + 1, bound),
-                    self.encode_bag_ctx(formula.sub_operand, level)
+                    self.encode_bag_ctx(formula.sub_operand, level),
                 )
             else:
                 # level == bound
                 enc = False
-                for loop_level in range(1, bound+1):
-                    enc = simplify(Or(enc, And(self.loop_position == loop_level, self.encode(
-                        formula.left_operand, loop_level, bound))))
+                for loop_level in range(1, bound + 1):
+                    enc = simplify(
+                        Or(
+                            enc,
+                            And(
+                                self.loop_position == loop_level,
+                                self.encode(formula.left_operand, loop_level, bound),
+                            ),
+                        )
+                    )
                 enc = And(enc, self.encode_bag_ctx(formula.sub_operand, level))
                 enc = simplify(enc)
 
@@ -214,22 +218,25 @@ class rsLTL_Encoder(object):
                 enc = And(
                     self.encode(formula.left_operand, level, bound),
                     self.encode_bag_ctx(formula.sub_operand, level),
-                    self.encode(formula, level + 1, bound)
+                    self.encode(formula, level + 1, bound),
                 )
             else:
                 # level == bound
                 enc_loops = False
-                for loop_level in range(1, bound+1):
-                    enc_loops = simplify(Or(enc_loops,
+                for loop_level in range(1, bound + 1):
+                    enc_loops = simplify(
+                        Or(
+                            enc_loops,
                             And(
                                 self.loop_position == loop_level,
                                 self.encode_approx(formula, loop_level, bound),
+                            ),
+                        )
                     )
-                                            ))
                 enc = And(
                     self.encode(formula.left_operand, bound, bound),
                     enc_loops,
-                    self.encode_bag_ctx(formula.sub_operand, level)
+                    self.encode_bag_ctx(formula.sub_operand, level),
                 )
                 enc = simplify(enc)
 
@@ -239,25 +246,26 @@ class rsLTL_Encoder(object):
                     self.encode(formula.left_operand, level, bound),
                     And(
                         self.encode_bag_ctx(formula.sub_operand, level),
-                        self.encode(formula, level + 1, bound)
-                    )
+                        self.encode(formula, level + 1, bound),
+                    ),
                 )
             else:
                 # level == bound
                 enc_loops = False
-                for loop_level in range(1, bound+1):
-                    enc_loops = simplify(Or(enc_loops,
+                for loop_level in range(1, bound + 1):
+                    enc_loops = simplify(
+                        Or(
+                            enc_loops,
                             And(
                                 self.loop_position == loop_level,
                                 self.encode_approx(formula, loop_level, bound),
+                            ),
+                        )
                     )
-                                            ))
                     # print(enc)
-                enc = Or(self.encode(formula.left_operand, bound, bound),
-                         And(
-                    enc_loops,
-                    self.encode_bag_ctx(formula.sub_operand, level)
-                )
+                enc = Or(
+                    self.encode(formula.left_operand, bound, bound),
+                    And(enc_loops, self.encode_bag_ctx(formula.sub_operand, level)),
                 )
 
                 enc = simplify(enc)
@@ -268,21 +276,24 @@ class rsLTL_Encoder(object):
             else:
                 # level == bound
                 inner_enc = False
-                for loop_level in range(1, bound+1):
-                    inner_enc = simplify(Or(inner_enc,
+                for loop_level in range(1, bound + 1):
+                    inner_enc = simplify(
+                        Or(
+                            inner_enc,
                             And(
                                 self.loop_position == loop_level,
-                                                self.encode_approx(formula, loop_level, bound)
+                                self.encode_approx(formula, loop_level, bound),
+                            ),
+                        )
                     )
-                                            ))
 
             enc = Or(
                 self.encode(formula.right_operand, level, bound),
                 And(
                     self.encode(formula.left_operand, level, bound),
                     inner_enc,
-                    self.encode_bag_ctx(formula.sub_operand, level)
-                )
+                    self.encode_bag_ctx(formula.sub_operand, level),
+                ),
             )
 
         elif formula.f_type == rsLTL_form_type.t_release:
@@ -291,23 +302,23 @@ class rsLTL_Encoder(object):
             else:
                 # level == bound
                 inner_enc = False
-                for loop_level in range(1, bound+1):
-                    inner_enc = simplify(Or(inner_enc,
+                for loop_level in range(1, bound + 1):
+                    inner_enc = simplify(
+                        Or(
+                            inner_enc,
                             And(
                                 self.loop_position == loop_level,
-                                                self.encode_approx(formula, loop_level, bound)
+                                self.encode_approx(formula, loop_level, bound),
+                            ),
+                        )
                     )
-                                            ))
 
             enc = And(
                 self.encode(formula.right_operand, level, bound),
                 Or(
                     self.encode(formula.left_operand, level, bound),
-                    And(
-                        inner_enc,
-                        self.encode_bag_ctx(formula.sub_operand, level)
-                    )
-                )
+                    And(inner_enc, self.encode_bag_ctx(formula.sub_operand, level)),
+                ),
             )
 
         else:
@@ -341,8 +352,8 @@ class rsLTL_Encoder(object):
                     And(
                         self.encode(formula.left_operand, level, bound),
                         self.encode_approx(formula, level + 1, bound),
-                        self.encode_bag_ctx(formula.sub_operand, level)
-                    )
+                        self.encode_bag_ctx(formula.sub_operand, level),
+                    ),
                 )
             else:
                 # level == bound
@@ -356,9 +367,9 @@ class rsLTL_Encoder(object):
                         self.encode(formula.left_operand, level, bound),
                         And(
                             self.encode_approx(formula, level + 1, bound),
-                            self.encode_bag_ctx(formula.sub_operand, level)
-                        )
-                    )
+                            self.encode_bag_ctx(formula.sub_operand, level),
+                        ),
+                    ),
                 )
             else:
                 # level == bound
@@ -369,7 +380,7 @@ class rsLTL_Encoder(object):
                 enc = And(
                     self.encode(formula.left_operand, level, bound),
                     self.encode_bag_ctx(formula.sub_operand, level),
-                    self.encode_approx(formula, level + 1, bound)
+                    self.encode_approx(formula, level + 1, bound),
                 )
             else:
                 # level == bound
@@ -381,16 +392,15 @@ class rsLTL_Encoder(object):
                     self.encode(formula.left_operand, level, bound),
                     And(
                         self.encode_bag_ctx(formula.sub_operand, level),
-                        self.encode_approx(formula, level + 1, bound)
-                    )
+                        self.encode_approx(formula, level + 1, bound),
+                    ),
                 )
             else:
                 # level == bound
                 enc = self.encode(formula.left_operand, bound, bound)
 
         else:
-            raise NotImplementedError(
-                "Unsupported operator in approximation encoding")
+            raise NotImplementedError("Unsupported operator in approximation encoding")
 
         if enc is None:
             raise RuntimeError("Encoding is NONE. Should never happen")

reactics-smt/rs/__init__.py

@@ -2,7 +2,11 @@ from rs.reaction_system import ReactionSystem
 from rs.context_automaton import ContextAutomaton
 
 from rs.reaction_system_with_concentrations import ReactionSystemWithConcentrations
-from rs.reaction_system_with_concentrations_param import ReactionSystemWithConcentrationsParam, ParameterObj, is_param
+from rs.reaction_system_with_concentrations_param import (
+    ReactionSystemWithConcentrationsParam,
+    ParameterObj,
+    is_param,
+)
 from rs.context_automaton_with_concentrations import ContextAutomatonWithConcentrations
 
 from rs.extended_context_automaton import ExtendedContextAutomaton

reactics-smt/rs/context_automaton.py

@@ -3,7 +3,6 @@ from colour import *
 
 
 class ContextAutomaton(object):
-
     def __init__(self, reaction_system):
         self._states = []
         self._transitions = []
@@ -40,7 +39,7 @@ class ContextAutomaton(object):
         if name not in self._states:
             self._states.append(name)
         else:
-            print("\'%s\' already added. skipping..." % (name,))
+            print("'%s' already added. skipping..." % (name,))
 
     def add_states(self, states_set):
         for st in states_set:
@@ -101,15 +100,14 @@ class ContextAutomaton(object):
 
         if not self.is_valid_context(context_set):
             raise RuntimeError(
-                "one of the entities in the context set is unknown (undefined)!")
+                "one of the entities in the context set is unknown (undefined)!"
+            )
 
         if not self.is_state(src):
-            raise RuntimeError(
-                "\"" + src + "\" is an unknown (undefined) state")
+            raise RuntimeError('"' + src + '" is an unknown (undefined) state')
 
         if not self.is_state(dst):
-            raise RuntimeError(
-                "\"" + dst + "\" is an unknown (undefined) state")
+            raise RuntimeError('"' + dst + '" is an unknown (undefined) state')
 
         new_context_set = set()
         for e in set(context_set):
@@ -118,8 +116,8 @@ class ContextAutomaton(object):
         self._prod_entities |= new_context_set
 
         self._transitions.append(
-            (self.get_state_id(src),
-             new_context_set, self.get_state_id(dst)))
+            (self.get_state_id(src), new_context_set, self.get_state_id(dst))
+        )
 
     def rsset2str(self, elements):
         """Converts the set of entities ids into the string with their names"""
@@ -168,4 +166,5 @@ class ContextAutomaton(object):
         self.show_transitions()
         self.show_prod_entities()
 
+
 # EOF

reactics-smt/rs/context_automaton_with_concentrations.py

@@ -5,15 +5,13 @@ from rs.context_automaton import ContextAutomaton
 
 
 class ContextAutomatonWithConcentrations(ContextAutomaton):
-
     def __init__(self, reaction_system):
-        super(ContextAutomatonWithConcentrations,
-              self).__init__(reaction_system)
+        super(ContextAutomatonWithConcentrations, self).__init__(reaction_system)
 
     def is_valid_context(self, context):
-        if set(
-                [e for e, lvl in context]).issubset(
-                self._reaction_system.background_set):
+        if set([e for e, lvl in context]).issubset(
+            self._reaction_system.background_set
+        ):
             return True
         else:
             return False
@@ -33,45 +31,38 @@ class ContextAutomatonWithConcentrations(ContextAutomaton):
 
         if not self.is_valid_context(context_set):
             raise RuntimeError(
-                "one of the entities in the context set is unknown (undefined)!")
+                "one of the entities in the context set is unknown (undefined)!"
+            )
 
         if not self.is_state(src):
-            raise RuntimeError(
-                "\"" + src + "\" is an unknown (undefined) state")
+            raise RuntimeError('"' + src + '" is an unknown (undefined) state')
 
         if not self.is_state(dst):
-            raise RuntimeError(
-                "\"" + dst + "\" is an unknown (undefined) state")
+            raise RuntimeError('"' + dst + '" is an unknown (undefined) state')
 
         new_context_set = set()
         for ent, lvl in set(context_set):
-            new_context_set.add(
-                (self._reaction_system.get_entity_id(ent), lvl))
+            new_context_set.add((self._reaction_system.get_entity_id(ent), lvl))
 
         self._transitions.append(
-            (self.get_state_id(src),
-             new_context_set, self.get_state_id(dst)))
+            (self.get_state_id(src), new_context_set, self.get_state_id(dst))
+        )
 
     def get_automaton_with_flat_contexts(self, ordinary_reaction_system):
-
         ca = ContextAutomaton(ordinary_reaction_system)
         ca._states = self._states
         ca._init_state = self._init_state
 
         for src, ctx, dst in self._transitions:
-
             new_ctx = set()
 
             for ent, conc in ctx:
-                for i in range(1, conc+1):
-                    n = self._reaction_system.get_entity_name(
-                        ent) + "#" + str(i)
+                for i in range(1, conc + 1):
+                    n = self._reaction_system.get_entity_name(ent) + "#" + str(i)
                     ca._reaction_system.ensure_bg_set_entity(n)
                     new_ctx.add(n)
 
-            ca.add_transition(
-                ca.get_state_name(src),
-                new_ctx, ca.get_state_name(dst))
+            ca.add_transition(ca.get_state_name(src), new_ctx, ca.get_state_name(dst))
 
         return ca
 
@@ -80,4 +71,5 @@ class ContextAutomatonWithConcentrations(ContextAutomaton):
         self.show_states()
         self.show_transitions()
 
+
 # EOF

reactics-smt/rs/extended_context_automaton.py

@@ -75,23 +75,24 @@ class ExtendedContextAutomaton(ContextAutomaton):
 
         if not self.is_valid_rs_set(ctx_reactants):
             raise RuntimeError(
-                "one of the entities in the reactants set is unknown (undefined)!")
+                "one of the entities in the reactants set is unknown (undefined)!"
+            )
 
         if not self.is_valid_rs_set(ctx_inhibitors):
             raise RuntimeError(
-                "one of the entities in the inhibitors set is unknown (undefined)!")
+                "one of the entities in the inhibitors set is unknown (undefined)!"
+            )
 
         if not self.is_valid_rs_set(ctx_products):
             raise RuntimeError(
-                "one of the entities in the context set is unknown (undefined)!")
+                "one of the entities in the context set is unknown (undefined)!"
+            )
 
         if not self.is_state(src):
-            raise RuntimeError(
-                "\"" + src + "\" is an unknown (undefined) state")
+            raise RuntimeError('"' + src + '" is an unknown (undefined) state')
 
         if not self.is_state(dst):
-            raise RuntimeError(
-                "\"" + dst + "\" is an unknown (undefined) state")
+            raise RuntimeError('"' + dst + '" is an unknown (undefined) state')
 
         src_id = self.get_state_id(src)
         dst_id = self.get_state_id(dst)
@@ -119,8 +120,15 @@ class ExtendedContextAutomaton(ContextAutomaton):
         for src_id, act_id, reaction, dst_id in self._transitions:
             str_transition = self.get_state_name(src_id) + " --( "
             str_transition += "<" + self.get_actions_str(act_id) + "> | "
-            str_transition += "( " + self.rsset2str(reaction[0]) + "," + self.rsset2str(
-                reaction[1]) + "," + self.rsset2str(reaction[2]) + " )"
+            str_transition += (
+                "( "
+                + self.rsset2str(reaction[0])
+                + ","
+                + self.rsset2str(reaction[1])
+                + ","
+                + self.rsset2str(reaction[2])
+                + " )"
+            )
             str_transition += " )--> " + self.get_state_name(dst_id)
             print(" - " + str_transition)
 
@@ -130,7 +138,7 @@ class ExtendedContextAutomaton(ContextAutomaton):
         if action_name not in self._actions:
             self._actions.append(action_name)
         else:
-            print("\'%s\' already added. skipping..." % (action_name,))
+            print("'%s' already added. skipping..." % (action_name,))
 
     def get_action_id(self, action_name):
         """For an action name returns its id"""
@@ -138,8 +146,7 @@ class ExtendedContextAutomaton(ContextAutomaton):
         try:
             return self._actions.index(action_name)
         except ValueError:
-            print_error("Undefined context automaton action: " +
-                        repr(action_name))
+            print_error("Undefined context automaton action: " + repr(action_name))
             exit(1)
 
     def get_action_name(self, action_id):
@@ -173,4 +180,5 @@ class ExtendedContextAutomaton(ContextAutomaton):
         super(ExtendedContextAutomaton, self).show()
         self.show_actions()
 
+
 # EOF

reactics-smt/rs/network_of_context_automata.py

@@ -3,7 +3,6 @@ from colour import *
 
 
 class NetworkOfContextAutomata(object):
-
     def __init__(self, reaction_system, context_automata):
         self.automata = []
         self._reaction_system = reaction_system
@@ -44,14 +43,14 @@ class NetworkOfContextAutomata(object):
         for automaton in self.automata:
             if automaton.reaction_system != self._reaction_system:
                 print_error(
-                    "Mismatching reaction system used in \"" +
-                    str(automaton.name) + "\"!!!")
+                    'Mismatching reaction system used in "'
+                    + str(automaton.name)
+                    + '"!!!'
+                )
                 exit(1)
 
     def show_prod_entities(self):
-        print(
-            C_MARK_INFO +
-            " Possible context-products for the network of automata:")
+        print(C_MARK_INFO + " Possible context-products for the network of automata:")
         for entity in self.prod_entities:
             print(" - " + self._reaction_system.get_entity_name(entity))
 
@@ -96,7 +95,8 @@ class NetworkOfContextAutomata(object):
         for entity in aut.prod_entities:
             self._actions_for_products.setdefault(entity, set())
             self._actions_for_products[entity] |= aut.get_actions_producing_entity(
-                entity)
+                entity
+            )
 
     def show(self):
         print()
@@ -108,4 +108,5 @@ class NetworkOfContextAutomata(object):
         self.show_prod_entities()
         self.show_actions()
 
+
 # EOF

reactics-smt/rs/reaction_system.py

@@ -3,9 +3,7 @@ from colour import *
 
 
 class ReactionSystem(object):
-
     def __init__(self):
-
         self.reactions = []
         self.background_set = []
 
@@ -28,10 +26,12 @@ 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")
+            raise RuntimeError("The entity " + name + " is already on the list")
 
     def add_bg_set_entity(self, name):
         self.assume_not_in_bgset(name)
@@ -106,7 +106,6 @@ class ReactionSystem(object):
         self.init_contexts.append(integers)
 
     def set_context_entities(self, entities):
-
         for entity in entities:
             entity_id = self.get_entity_id(entity)
             self.context_entities.append(entity_id)
@@ -131,20 +130,36 @@ class ReactionSystem(object):
     def show_reactions(self, soft=False):
         print(C_MARK_INFO + " Reactions:")
         if soft and len(self.reactions) > 50:
-            print(" -> there are more than 50 reactions (" +
-                  str(len(self.reactions)) + ")")
+            print(
+                " -> there are more than 50 reactions ("
+                + str(len(self.reactions))
+                + ")"
+            )
         else:
             print(
-                " "*4 + "{0: ^35}{1: ^25}{2: ^15}".format("reactants", " inhibitors", " products"))
+                " " * 4
+                + "{0: ^35}{1: ^25}{2: ^15}".format(
+                    "reactants", " inhibitors", " products"
+                )
+            )
             for reaction in self.reactions:
                 # print("\t( R={" + self.state_to_str(reaction[0]) + "}, I={" + self.state_to_str(reaction[1]) + "}, P={" + self.state_to_str(reaction[2]) + "} )")
-                print(" " + "- {0: ^35}{1: ^25}{2: ^15}".format("{ " + self.state_to_str(reaction[0]) + " }",
+                print(
+                    " "
+                    + "- {0: ^35}{1: ^25}{2: ^15}".format(
+                        "{ " + self.state_to_str(reaction[0]) + " }",
                         " { " + self.state_to_str(reaction[1]) + " }",
-                                                                " { " + self.state_to_str(reaction[2]) + " }"))
+                        " { " + self.state_to_str(reaction[2]) + " }",
+                    )
+                )
 
     def show_background_set(self):
         print(
-            C_MARK_INFO + " Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")
+            C_MARK_INFO
+            + " Background set: {"
+            + self.entities_names_set_to_str(self.background_set)
+            + "}"
+        )
 
     def show_initial_contexts(self):
         if len(self.init_contexts) > 0:
@@ -155,10 +170,12 @@ class ReactionSystem(object):
     def show_context_entities(self):
         if len(self.context_entities) > 0:
             print(
-                C_MARK_INFO + " Context entities: " + self.entities_ids_set_to_str(self.context_entities))
+                C_MARK_INFO
+                + " Context entities: "
+                + self.entities_ids_set_to_str(self.context_entities)
+            )
 
     def show(self, soft=False):
-
         self.show_background_set()
         self.show_initial_contexts()
         self.show_reactions(soft)
@@ -181,8 +198,7 @@ class ReactionSystem(object):
             reactions_by_prod[prod_entity] = []
             for reaction in self.reactions:
                 if prod_entity in reaction[2]:
-                    reactions_by_prod[prod_entity].append(
-                        [reaction[0], reaction[1]])
+                    reactions_by_prod[prod_entity].append([reaction[0], reaction[1]])
 
         # save in cache
         self.reactions_by_prod = reactions_by_prod
@@ -200,4 +216,5 @@ class ReactionSystem(object):
             print("Empty background set")
             exit(1)
 
+
 # EOF

reactics-smt/rs/reaction_system_with_autnet.py

@@ -1,6 +1,4 @@
-
 class ReactionSystemWithNetworkOfAutomata(object):
-
     def __init__(self, reaction_system, context_automata):
         self.rs = reaction_system
         self.cas = context_automata
@@ -9,4 +7,5 @@ class ReactionSystemWithNetworkOfAutomata(object):
         self.rs.show(soft)
         self.cas.show()
 
+
 # EOF

reactics-smt/rs/reaction_system_with_automaton.py

@@ -1,10 +1,11 @@
 from rs.reaction_system_with_concentrations import ReactionSystemWithConcentrations
-from rs.reaction_system_with_concentrations_param import ReactionSystemWithConcentrationsParam
+from rs.reaction_system_with_concentrations_param import (
+    ReactionSystemWithConcentrationsParam,
+)
 from rs.context_automaton_with_concentrations import ContextAutomatonWithConcentrations
 
 
 class ReactionSystemWithAutomaton(object):
-
     def __init__(self, reaction_system, context_automaton):
         self.rs = reaction_system
         self.ca = context_automaton
@@ -35,7 +36,6 @@ class ReactionSystemWithAutomaton(object):
         pass
 
     def get_ordinary_reaction_system_with_automaton(self):
-
         if not self.is_with_concentrations():
             raise RuntimeError("Not RS/CA with concentrations")
 

reactics-smt/rs/reaction_system_with_concentrations.py

@@ -5,9 +5,7 @@ from rs.reaction_system import ReactionSystem
 
 
 class ReactionSystemWithConcentrations(ReactionSystem):
-
     def __init__(self):
-
         self.reactions = []
         self.meta_reactions = dict()
         self.permanent_entities = dict()
@@ -26,8 +24,7 @@ class ReactionSystemWithConcentrations(ReactionSystem):
             name = e
             print("\nWARNING: no maximal concentration level specified for:", e, "\n")
         else:
-            raise RuntimeError(
-                "Bad entity type when adding background set element")
+            raise RuntimeError("Bad entity type when adding background set element")
 
         self.assume_not_in_bgset(name)
         self.background_set.append(name)
@@ -41,7 +38,6 @@ class ReactionSystemWithConcentrations(ReactionSystem):
                 self.max_concentration = def_max_conc
 
     def get_max_concentration_level(self, e):
-
         if e in self.max_conc_per_ent:
             return self.max_conc_per_ent[e]
         else:
@@ -69,8 +65,7 @@ class ReactionSystemWithConcentrations(ReactionSystem):
 
     def has_non_zero_concentration(self, elem):
         if elem[1] < 1:
-            raise RuntimeError(
-                "Unexpected concentration level in state: " + str(elem))
+            raise RuntimeError("Unexpected concentration level in state: " + str(elem))
 
     def process_rip(self, R, I, P, ignore_empty_R=False):
         """Chcecks concentration levels and converts entities names into their ids"""
@@ -123,21 +118,25 @@ class ReactionSystemWithConcentrations(ReactionSystem):
         """Adds a macro/meta reaction for increasing the value of incr_entity"""
 
         reactants, inhibitors, products = self.process_rip(
-            R, I, [], ignore_empty_R=True)
+            R, I, [], ignore_empty_R=True
+        )
         incr_entity_id = self.get_entity_id(incr_entity)
         self.meta_reactions.setdefault(incr_entity_id, [])
         self.meta_reactions[incr_entity_id].append(
-            ("inc", self.get_entity_id(incrementer), reactants, inhibitors))
+            ("inc", self.get_entity_id(incrementer), reactants, inhibitors)
+        )
 
     def add_reaction_dec(self, decr_entity, decrementer, R, I):
         """Adds a macro/meta reaction for decreasing the value of incr_entity"""
 
         reactants, inhibitors, products = self.process_rip(
-            R, I, [], ignore_empty_R=True)
+            R, I, [], ignore_empty_R=True
+        )
         decr_entity_id = self.get_entity_id(decr_entity)
         self.meta_reactions.setdefault(decr_entity_id, [])
         self.meta_reactions[decr_entity_id].append(
-            ("dec", self.get_entity_id(decrementer), reactants, inhibitors))
+            ("dec", self.get_entity_id(decrementer), reactants, inhibitors)
+        )
 
     def add_permanency(self, ent, I):
         """Sets entity to be permanent unless it is inhibited"""
@@ -145,8 +144,7 @@ class ReactionSystemWithConcentrations(ReactionSystem):
         ent_id = self.get_entity_id(ent)
 
         if ent_id in self.permanent_entities:
-            raise RuntimeError(
-                "Permanency for {0} already defined.".format(ent))
+            raise RuntimeError("Permanency for {0} already defined.".format(ent))
 
         inhibitors = self.process_rip([], I, [], ignore_empty_R=True)[1]
         self.permanent_entities[ent_id] = inhibitors
@@ -177,31 +175,50 @@ class ReactionSystemWithConcentrations(ReactionSystem):
 
     def show_background_set(self):
         print(
-            C_MARK_INFO + " Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")
+            C_MARK_INFO
+            + " Background set: {"
+            + self.entities_names_set_to_str(self.background_set)
+            + "}"
+        )
 
     def show_meta_reactions(self):
         print(C_MARK_INFO + " Meta reactions:")
         for param_ent, reactions in self.meta_reactions.items():
             for r_type, command, reactants, inhibitors in reactions:
                 if r_type == "inc" or r_type == "dec":
-                    print(" - [ Type=" + repr(r_type) + " Operand=( " + self.get_entity_name(param_ent) + " ) Command=( " + self.get_entity_name(
-                        command) + " ) ] -- ( R={" + self.state_to_str(reactants) + "}, I={" + self.state_to_str(inhibitors) + "} )")
+                    print(
+                        " - [ Type="
+                        + repr(r_type)
+                        + " Operand=( "
+                        + self.get_entity_name(param_ent)
+                        + " ) Command=( "
+                        + self.get_entity_name(command)
+                        + " ) ] -- ( R={"
+                        + self.state_to_str(reactants)
+                        + "}, I={"
+                        + self.state_to_str(inhibitors)
+                        + "} )"
+                    )
                 else:
-                    raise RuntimeError(
-                        "Unknown meta-reaction type: " + repr(r_type))
+                    raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
 
     def show_max_concentrations(self):
         print(
-            C_MARK_INFO +
-            " Maximal allowed concentration levels (for optimized translation to RS):")
+            C_MARK_INFO
+            + " Maximal allowed concentration levels (for optimized translation to RS):"
+        )
         for e, max_conc in self.max_conc_per_ent.items():
             print(" - {0:^20} = {1:<6}".format(self.get_entity_name(e), max_conc))
 
     def show_permanent_entities(self):
         print(C_MARK_INFO + " Permanent entities:")
         for e, inhibitors in self.permanent_entities.items():
-            print(" - {0:^20}{1:<6}".format(self.get_entity_name(e) + ": ",
-                                            "I={" + self.state_to_str(inhibitors) + "}"))
+            print(
+                " - {0:^20}{1:<6}".format(
+                    self.get_entity_name(e) + ": ",
+                    "I={" + self.state_to_str(inhibitors) + "}",
+                )
+            )
 
     def show(self, soft=False):
         self.show_background_set()
@@ -220,8 +237,7 @@ class ReactionSystemWithConcentrations(ReactionSystem):
 
         for reaction in self.reactions:
             product_entities = [e for e, c in reaction[2]]
-            producible_entities = producible_entities.union(
-                set(product_entities))
+            producible_entities = producible_entities.union(set(product_entities))
 
         reactions_by_prod = {}
 
@@ -242,18 +258,20 @@ class ReactionSystemWithConcentrations(ReactionSystem):
 
                     # we need to order the reactions w.r.t. the concentration levels produced (increasing order)
                     for i in range(0, len(rcts_for_p_e)):
-
                         checked_conc = rcts_for_p_e[i][2][0][1]
                         if prod_conc <= checked_conc:
                             insert_place = i
                             break
 
-                    if insert_place == None:  # empty or the is only one element which is smaller than the element being added
+                    if (
+                        insert_place == None
+                    ):  # empty or the is only one element which is smaller than the element being added
                         # we append (to the end)
                         rcts_for_p_e.append((reactants, inhibitors, products))
                     else:
                         rcts_for_p_e.insert(
-                            insert_place, (reactants, inhibitors, products))
+                            insert_place, (reactants, inhibitors, products)
+                        )
 
         # save in cache
         self.reactions_by_prod = reactions_by_prod
@@ -261,11 +279,9 @@ class ReactionSystemWithConcentrations(ReactionSystem):
         return reactions_by_prod
 
     def get_reaction_system(self):
-
         rs = ReactionSystem()
 
         for reactants, inhibitors, products in self.reactions:
-
             new_reactants = []
             new_inhibitors = []
             new_products = []
@@ -281,7 +297,7 @@ class ReactionSystemWithConcentrations(ReactionSystem):
                 new_inhibitors.append(n)
 
             for ent, conc in products:
-                for i in range(1, conc+1):
+                for i in range(1, conc + 1):
                     n = self.get_entity_name(ent) + "#" + str(i)
                     rs.ensure_bg_set_entity(n)
                     new_products.append(n)
@@ -290,7 +306,6 @@ class ReactionSystemWithConcentrations(ReactionSystem):
 
         for param_ent, reactions in self.meta_reactions.items():
             for r_type, command, reactants, inhibitors in reactions:
-
                 param_ent_name = self.get_entity_name(param_ent)
 
                 new_reactants = []
@@ -312,16 +327,15 @@ class ReactionSystemWithConcentrations(ReactionSystem):
                 else:
                     print(
                         "WARNING:\n\tThere is no maximal concentration level defined for "
-                        + self.get_entity_name(command))
+                        + self.get_entity_name(command)
+                    )
                     print("\tThis is a very bad idea -- expect degraded performance\n")
 
-                for l in range(1, max_cmd_c+1):
-
+                for l in range(1, max_cmd_c + 1):
                     cmd_ent = self.get_entity_name(command) + "#" + str(l)
                     rs.ensure_bg_set_entity(cmd_ent)
 
                     if r_type == "inc":
-
                         # pre_conc  -- predecessor concentration
                         # succ_conc -- successor concentration concentration
 
@@ -329,8 +343,8 @@ class ReactionSystemWithConcentrations(ReactionSystem):
                             pre_conc = param_ent_name + "#" + str(i)
                             rs.ensure_bg_set_entity(pre_conc)
                             new_products = []
-                            succ_value = i+l
-                            for j in range(1, succ_value+1):
+                            succ_value = i + l
+                            for j in range(1, succ_value + 1):
                                 if j > self.max_concentration:
                                     break
                                 new_p = param_ent_name + "#" + str(j)
@@ -340,15 +354,16 @@ class ReactionSystemWithConcentrations(ReactionSystem):
                                 rs.add_reaction(
                                     set(new_reactants + [pre_conc, cmd_ent]),
                                     set(new_inhibitors),
-                                    set(new_products))
+                                    set(new_products),
+                                )
 
                     elif r_type == "dec":
-                        for i in range(1, self.max_concentration+1):
+                        for i in range(1, self.max_concentration + 1):
                             pre_conc = param_ent_name + "#" + str(i)
                             rs.ensure_bg_set_entity(pre_conc)
                             new_products = []
-                            succ_value = i-l
-                            for j in range(1, succ_value+1):
+                            succ_value = i - l
+                            for j in range(1, succ_value + 1):
                                 if j > self.max_concentration:
                                     break
                                 new_p = param_ent_name + "#" + str(j)
@@ -358,28 +373,29 @@ class ReactionSystemWithConcentrations(ReactionSystem):
                                 rs.add_reaction(
                                     set(new_reactants + [pre_conc, cmd_ent]),
                                     set(new_inhibitors),
-                                    set(new_products))
+                                    set(new_products),
+                                )
 
                     else:
                         raise RuntimeError(
-                            "Unknown meta-reaction type: " + repr(r_type))
+                            "Unknown meta-reaction type: " + repr(r_type)
+                        )
 
         for ent, inhibitors in self.permanent_entities.items():
-
             max_c = self.max_concentration
             if ent in self.max_conc_per_ent:
                 max_c = self.max_conc_per_ent[ent]
             else:
                 print(
                     "WARNING:\n\tThere is no maximal concentration level defined for "
-                    + self.get_entity_name(ent))
+                    + self.get_entity_name(ent)
+                )
                 print("\tThis is a very bad idea -- expect degraded performance\n")
 
             def e_value(i):
                 return self.get_entity_name(ent) + "#" + str(i)
 
-            for value in range(1, max_c+1):
-
+            for value in range(1, max_c + 1):
                 new_reactants = []
                 new_inhibitors = []
                 new_products = []
@@ -391,7 +407,7 @@ class ReactionSystemWithConcentrations(ReactionSystem):
                     rs.ensure_bg_set_entity(n)
                     new_inhibitors.append(n)
 
-                for i in range(1, value+1):
+                for i in range(1, value + 1):
                     new_products.append(e_value(i))
 
                 rs.add_reaction(new_reactants, new_inhibitors, new_products)
@@ -400,7 +416,6 @@ class ReactionSystemWithConcentrations(ReactionSystem):
 
 
 class ReactionSystemWithAutomaton(object):
-
     def __init__(self, reaction_system, context_automaton):
         self.rs = reaction_system
         self.ca = context_automaton
@@ -420,7 +435,6 @@ class ReactionSystemWithAutomaton(object):
         pass
 
     def get_ordinary_reaction_system_with_automaton(self):
-
         if not self.is_with_concentrations():
             raise RuntimeError("Not RS/CA with concentrations")
 

reactics-smt/rs/reaction_system_with_concentrations_param.py

@@ -5,7 +5,6 @@ from rs.reaction_system import ReactionSystem
 
 
 class ParameterObj(object):
-
     def __init__(self, name):
         self.name = name
 
@@ -21,9 +20,7 @@ def is_param(some_object):
 
 
 class ReactionSystemWithConcentrationsParam(ReactionSystem):
-
     def __init__(self):
-
         self.reactions = []
         self.parameters = dict()
         self.meta_reactions = dict()
@@ -43,8 +40,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
             name = e
             print("\nWARNING: no maximal concentration level specified for:", e, "\n")
         else:
-            raise RuntimeError(
-                "Bad entity type when adding background set element")
+            raise RuntimeError("Bad entity type when adding background set element")
 
         self.assume_not_in_bgset(name)
         self.background_set.append(name)
@@ -76,7 +72,6 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
         self.parameters[param_key].idx = len(self.parameters)
 
     def get_max_concentration_level(self, e):
-
         if e in self.max_conc_per_ent:
             return self.max_conc_per_ent[e]
         else:
@@ -113,7 +108,9 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
     def terminate_on_invalid_concentration(self, entity, level):
         if not self.is_valid_concentration_for_entity(entity, level):
-            print("FATAL. Invalid entity concentration: {:s}={:d}".format(entity, level))
+            print(
+                "FATAL. Invalid entity concentration: {:s}={:d}".format(entity, level)
+            )
             exit(1)
 
     def get_state_ids(self, state):
@@ -122,8 +119,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
     def has_non_zero_concentration(self, elem):
         if elem[1] < 1:
-            raise RuntimeError(
-                "Unexpected concentration level in state: " + str(elem))
+            raise RuntimeError("Unexpected concentration level in state: " + str(elem))
 
     def process_rip(self, R, I, P, ignore_empty_R=False):
         """Chcecks concentration levels and converts entities names into their ids"""
@@ -207,21 +203,25 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
         """Adds a macro/meta reaction for increasing the value of incr_entity"""
 
         reactants, inhibitors, products = self.process_rip(
-            R, I, [], ignore_empty_R=True)
+            R, I, [], ignore_empty_R=True
+        )
         incr_entity_id = self.get_entity_id(incr_entity)
         self.meta_reactions.setdefault(incr_entity_id, [])
         self.meta_reactions[incr_entity_id].append(
-            ("inc", self.get_entity_id(incrementer), reactants, inhibitors))
+            ("inc", self.get_entity_id(incrementer), reactants, inhibitors)
+        )
 
     def add_reaction_dec(self, decr_entity, decrementer, R, I):
         """Adds a macro/meta reaction for decreasing the value of incr_entity"""
 
         reactants, inhibitors, products = self.process_rip(
-            R, I, [], ignore_empty_R=True)
+            R, I, [], ignore_empty_R=True
+        )
         decr_entity_id = self.get_entity_id(decr_entity)
         self.meta_reactions.setdefault(decr_entity_id, [])
         self.meta_reactions[decr_entity_id].append(
-            ("dec", self.get_entity_id(decrementer), reactants, inhibitors))
+            ("dec", self.get_entity_id(decrementer), reactants, inhibitors)
+        )
 
     def add_permanency(self, ent, I):
         """Sets entity to be permanent unless it is inhibited"""
@@ -229,8 +229,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
         ent_id = self.get_entity_id(ent)
 
         if ent_id in self.permanent_entities:
-            raise RuntimeError(
-                "Permanency for {0} already defined.".format(ent))
+            raise RuntimeError("Permanency for {0} already defined.".format(ent))
 
         inhibitors = self.process_rip([], I, [], ignore_empty_R=True)[1]
         self.permanent_entities[ent_id] = inhibitors
@@ -269,18 +268,32 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
     def show_background_set(self):
         print(
-            C_MARK_INFO + " Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")
+            C_MARK_INFO
+            + " Background set: {"
+            + self.entities_names_set_to_str(self.background_set)
+            + "}"
+        )
 
     def show_meta_reactions(self):
         print(C_MARK_INFO + " Meta reactions:")
         for param_ent, reactions in self.meta_reactions.items():
             for r_type, command, reactants, inhibitors in reactions:
                 if r_type == "inc" or r_type == "dec":
-                    print(" - [ Type=" + repr(r_type) + " Operand=( " + self.get_entity_name(param_ent) + " ) Command=( " + self.get_entity_name(
-                        command) + " ) ] -- ( R={" + self.state_to_str(reactants) + "}, I={" + self.state_to_str(inhibitors) + "} )")
+                    print(
+                        " - [ Type="
+                        + repr(r_type)
+                        + " Operand=( "
+                        + self.get_entity_name(param_ent)
+                        + " ) Command=( "
+                        + self.get_entity_name(command)
+                        + " ) ] -- ( R={"
+                        + self.state_to_str(reactants)
+                        + "}, I={"
+                        + self.state_to_str(inhibitors)
+                        + "} )"
+                    )
                 else:
-                    raise RuntimeError(
-                        "Unknown meta-reaction type: " + repr(r_type))
+                    raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
 
     def show_max_concentrations(self):
         print(C_MARK_INFO + " Maximal allowed concentration levels:")
@@ -290,8 +303,12 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
     def show_permanent_entities(self):
         print(C_MARK_INFO + " Permanent entities:")
         for e, inhibitors in self.permanent_entities.items():
-            print(" - {0:^20}{1:<6}".format(self.get_entity_name(e) + ": ",
-                                            "I={" + self.state_to_str(inhibitors) + "}"))
+            print(
+                " - {0:^20}{1:<6}".format(
+                    self.get_entity_name(e) + ": ",
+                    "I={" + self.state_to_str(inhibitors) + "}",
+                )
+            )
 
     def show(self, soft=False):
         self.show_background_set()
@@ -311,8 +328,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
         for reaction in self.reactions:
             product_entities = [e for e, c in reaction[2] if c > 0]
-            producible_entities = producible_entities.union(
-                set(product_entities))
+            producible_entities = producible_entities.union(set(product_entities))
 
         return producible_entities
 
@@ -324,7 +340,6 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
         rs = ReactionSystem()
 
         for reactants, inhibitors, products in self.reactions:
-
             new_reactants = []
             new_inhibitors = []
             new_products = []
@@ -349,7 +364,6 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
         for param_ent, reactions in self.meta_reactions.items():
             for r_type, command, reactants, inhibitors in reactions:
-
                 param_ent_name = self.get_entity_name(param_ent)
 
                 new_reactants = []
@@ -371,16 +385,15 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
                 else:
                     print(
                         "WARNING:\n\tThere is no maximal concentration level defined for "
-                        + self.get_entity_name(command))
+                        + self.get_entity_name(command)
+                    )
                     print("\tThis is a very bad idea -- expect degraded performance\n")
 
                 for l in range(1, max_cmd_c + 1):
-
                     cmd_ent = self.get_entity_name(command) + "#" + str(l)
                     rs.ensure_bg_set_entity(cmd_ent)
 
                     if r_type == "inc":
-
                         # pre_conc  -- predecessor concentration
                         # succ_conc -- successor concentration concentration
 
@@ -399,7 +412,8 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
                                 rs.add_reaction(
                                     set(new_reactants + [pre_conc, cmd_ent]),
                                     set(new_inhibitors),
-                                    set(new_products))
+                                    set(new_products),
+                                )
 
                     elif r_type == "dec":
                         for i in range(1, self.max_concentration + 1):
@@ -417,28 +431,29 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
                                 rs.add_reaction(
                                     set(new_reactants + [pre_conc, cmd_ent]),
                                     set(new_inhibitors),
-                                    set(new_products))
+                                    set(new_products),
+                                )
 
                     else:
                         raise RuntimeError(
-                            "Unknown meta-reaction type: " + repr(r_type))
+                            "Unknown meta-reaction type: " + repr(r_type)
+                        )
 
         for ent, inhibitors in self.permanent_entities.items():
-
             max_c = self.max_concentration
             if ent in self.max_conc_per_ent:
                 max_c = self.max_conc_per_ent[ent]
             else:
                 print(
                     "WARNING:\n\tThere is no maximal concentration level defined for "
-                    + self.get_entity_name(ent))
+                    + self.get_entity_name(ent)
+                )
                 print("\tThis is a very bad idea -- expect degraded performance\n")
 
             def e_value(i):
                 return self.get_entity_name(ent) + "#" + str(i)
 
             for value in range(1, max_c + 1):
-
                 new_reactants = []
                 new_inhibitors = []
                 new_products = []
@@ -457,4 +472,5 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
         return rs
 
+
 # EOF

reactics-smt/rsltl_shortcuts.py

@@ -27,8 +27,7 @@ def bag_And(*args):
     assert len(args) > 1
     last = get_bag_if_str(args[0])
     for arg in args[1:]:
-        last = BagDescription.f_And(
-            last, get_bag_if_str(arg))
+        last = BagDescription.f_And(last, get_bag_if_str(arg))
     return last
 
 
@@ -46,7 +45,6 @@ def exact_state(contained_entities, all_entities):
             expr.append(ent == 0)
 
     if len(expr) > 0:
-
         last = expr[0]
         for e in expr[1:]:
             last = BagDescription.f_And(last, e)
@@ -107,5 +105,6 @@ def param_And(*args):
         last = ParamConstraint.f_And(last, arg)
     return last
 
+
 def param_True():
     return ParamConstraint.f_TRUE()

reactics-smt/rssmt.py

@@ -24,12 +24,16 @@ if profiling:
 ##################################################################
 
 version = "2.99"
-rsmc_banner = """
+rsmc_banner = (
+    """
 Reaction Systems SMT-Based Model Checking
 
-Version:  """ + version + """
+Version:  """
+    + version
+    + """
 Author:   Artur Meski <artur.meski@gmail.com>
 """
+)
 
 ##################################################################
 
@@ -40,6 +44,7 @@ def print_banner():
         print(colour_str(C_GREEN, " " + 3 * "-" + " "), line)
     print()
 
+
 ##################################################################
 
 
@@ -48,22 +53,30 @@ def main():
 
     parser = argparse.ArgumentParser()
 
-    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")
     parser.add_argument(
-        "-n", "--scaling-parameter",
-        help="scaling parameter value (used in some benchmarks)")
-    parser.add_argument("-s", "--special_mode",
-                        help="special mode (used in some benchmarks)")
+        "-v", "--verbose", help="turn verbosity on", action="store_true"
+    )
+    parser.add_argument(
+        "-o",
+        "--optimise",
+        help="minimise the parametric computation result",
+        action="store_true",
+    )
+    parser.add_argument(
+        "-n",
+        "--scaling-parameter",
+        help="scaling parameter value (used in some benchmarks)",
+    )
+    parser.add_argument(
+        "-s", "--special_mode", help="special mode (used in some benchmarks)"
+    )
 
     args = parser.parse_args()
 
     print_banner()
     rs_testing.run_tests(args)
 
+
 ##################################################################
 
 
@@ -71,7 +84,8 @@ if __name__ == "__main__":
     try:
         if profiling:
             import profile
-            profile.run('main()')
+
+            profile.run("main()")
         else:
             main()
     except KeyboardInterrupt:

reactics-smt/scripts/avg.py

@@ -5,7 +5,6 @@ from os import listdir
 
 
 def proc_files(files):
-
     fs = []
     for f in files:
         try:
@@ -17,7 +16,6 @@ def proc_files(files):
     done = False
     result = []
     while not done:
-
         index = "NONE"
         val_sum = 0
 
@@ -30,7 +28,7 @@ def proc_files(files):
 
             sline = line.split()
 
-            assert(len(sline) == 2)
+            assert len(sline) == 2
 
             index, value = sline
             value = float(value)
@@ -40,7 +38,7 @@ def proc_files(files):
             # print(sline)
 
         else:
-            val_avg = val_sum/len(fs)
+            val_avg = val_sum / len(fs)
             result.append("{:s}\t{:f}".format(index, val_avg))
 
     result.append("")
@@ -48,7 +46,6 @@ def proc_files(files):
 
 
 def proc_dirs(dirs):
-
     first_dir = dirs[0]
 
     for f in listdir(first_dir):
@@ -59,7 +56,6 @@ def proc_dirs(dirs):
 
 
 def main():
-
     proc_dirs(sys.argv[1:])
 
     # proc_files(sys.argv[1:])

reactics-smt/smt/__init__.py

@@ -1,4 +1,4 @@
-#from smt.smt_checker import SmtChecker
+# from smt.smt_checker import SmtChecker
 from smt.smt_checker_rs import SmtCheckerRS
 from smt.smt_checker_rsc import SmtCheckerRSC
 from smt.smt_checker_rsc_param import SmtCheckerRSCParam

reactics-smt/smt/smt_checker_rs.py

@@ -9,9 +9,7 @@ import resource
 
 
 class SmtCheckerRS(object):
-
     def __init__(self, rsca):
-
         rsca.sanity_check()
 
         self.rs = rsca.rs
@@ -40,7 +38,7 @@ class SmtCheckerRS(object):
 
         variables = []
         for entity in self.rs.background_set:
-            variables.append(Bool("C"+str(level)+"_"+entity))
+            variables.append(Bool("C" + str(level) + "_" + entity))
 
         self.v_ctx.append(variables)
 
@@ -51,7 +49,7 @@ class SmtCheckerRS(object):
 
         variables = []
         for entity in self.rs.background_set:
-            variables.append(Bool("L"+str(level)+"_"+entity))
+            variables.append(Bool("L" + str(level) + "_" + entity))
         self.v.append(variables)
 
     def prepare_context_controller_variables(self):
@@ -59,7 +57,7 @@ class SmtCheckerRS(object):
 
         level = self.next_level_to_encode
 
-        self.ca_state.append(Int("CA"+str(level)+"_state"))
+        self.ca_state.append(Int("CA" + str(level) + "_state"))
 
     def prepare_state_variables(self):
         """Encodes all the state variables"""
@@ -84,8 +82,12 @@ class SmtCheckerRS(object):
     def enc_init_state(self, level):
         """Encodes the initial state at the given level"""
 
-        init_state_enc = simplify(And(self.enc_rs_init_state(
-            level), self.enc_context_controller_init_state(level)))
+        init_state_enc = simplify(
+            And(
+                self.enc_rs_init_state(level),
+                self.enc_context_controller_init_state(level),
+            )
+        )
 
         return init_state_enc
 
@@ -102,14 +104,23 @@ class SmtCheckerRS(object):
             enc_reactants = True
             enc_inhibitors = True
             for reactant in reactants:
-                enc_reactants = simplify(And(enc_reactants, Or(
-                    self.v[level][reactant], self.v_ctx[level][reactant])))
+                enc_reactants = simplify(
+                    And(
+                        enc_reactants,
+                        Or(self.v[level][reactant], self.v_ctx[level][reactant]),
+                    )
+                )
             for inhibitor in inhibitors:
-                enc_inhibitors = simplify(And(enc_inhibitors, Not(
-                    Or(self.v[level][inhibitor], self.v_ctx[level][inhibitor]))))
+                enc_inhibitors = simplify(
+                    And(
+                        enc_inhibitors,
+                        Not(Or(self.v[level][inhibitor], self.v_ctx[level][inhibitor])),
+                    )
+                )
 
             enc_rct_prod = simplify(
-                Or(enc_rct_prod, And(enc_reactants, enc_inhibitors)))
+                Or(enc_rct_prod, And(enc_reactants, enc_inhibitors))
+            )
 
         return enc_rct_prod
 
@@ -120,17 +131,15 @@ class SmtCheckerRS(object):
 
         enc_ent_prod = Or(
             And(enc_enab_cond, self.v[level + 1][prod_entity]),
-            And(Not(enc_enab_cond),
-                Not(self.v[level + 1][prod_entity])))
+            And(Not(enc_enab_cond), Not(self.v[level + 1][prod_entity])),
+        )
 
         return simplify(enc_ent_prod)
 
     def enc_transition_relation(self, level):
         """Encodes the combined transition relation"""
 
-        return simplify(
-            And(self.enc_rs_trans(level),
-                self.enc_automaton_trans(level)))
+        return simplify(And(self.enc_rs_trans(level), self.enc_automaton_trans(level)))
 
     def enc_rs_trans(self, level):
         """Encodes the transition relation"""
@@ -143,20 +152,19 @@ class SmtCheckerRS(object):
             unused_entities.remove(prod_entity)
 
             enc_trans = simplify(
-                And(enc_trans, self.enc_entity_production(level, prod_entity)))
+                And(enc_trans, self.enc_entity_production(level, prod_entity))
+            )
 
         for prod_entity in unused_entities:
-            enc_trans = simplify(
-                And(enc_trans, Not(self.v[level+1][prod_entity])))
+            enc_trans = simplify(And(enc_trans, Not(self.v[level + 1][prod_entity])))
 
         return enc_trans
 
     def enc_automaton_single_trans(self, level, transition):
-
         src, ctx, dst = transition
 
         src_enc = self.ca_state[level] == src
-        dst_enc = self.ca_state[level+1] == dst
+        dst_enc = self.ca_state[level + 1] == dst
 
         all_ent = set(range(len(self.rs.background_set)))
         incl_ctx = ctx
@@ -179,7 +187,8 @@ class SmtCheckerRS(object):
         enc_trans = False
         for transition in self.ca.transitions:
             enc_trans = simplify(
-                Or(enc_trans, self.enc_automaton_single_trans(level, transition)))
+                Or(enc_trans, self.enc_automaton_single_trans(level, transition))
+            )
 
         return enc_trans
 
@@ -231,14 +240,12 @@ class SmtCheckerRS(object):
         return simplify(enc)
 
     def decode_witness(self, max_level, print_model=False):
-
         m = self.solver.model()
 
         if print_model:
             print(m)
 
-        for level in range(max_level+1):
-
+        for level in range(max_level + 1):
             print("\n[Level=" + repr(level) + "]")
 
             print("  State: {", end=""),
@@ -256,7 +263,8 @@ class SmtCheckerRS(object):
                 print(" }")
 
     def check_reachability(
-            self, state, print_witness=True, print_time=True, print_mem=True):
+        self, state, print_witness=True, print_time=True, print_mem=True
+    ):
         """Main testing function"""
 
         if not type(state) is tuple:
@@ -299,16 +307,18 @@ class SmtCheckerRS(object):
         if print_time:
             # stop = time()
             stop = resource.getrusage(resource.RUSAGE_SELF).ru_utime
-            self.verification_time = stop-start
+            self.verification_time = stop - start
             print()
             print("[i] Time: " + repr(self.verification_time))
 
         if print_mem:
             print(
-                "[i] Memory: " +
-                repr(
-                    resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
-                    (1024 * 1024)) + " MB")
+                "[i] Memory: "
+                + repr(
+                    resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+                )
+                + " MB"
+            )
 
     def get_verification_time(self):
         return self.verification_time

reactics-smt/smt/smt_checker_rsc.py

@@ -16,9 +16,7 @@ from logics import rsLTL_Encoder
 
 
 class SmtCheckerRSC(object):
-
     def __init__(self, rsca):
-
         rsca.sanity_check()
 
         if not rsca.is_with_concentrations():
@@ -62,7 +60,7 @@ class SmtCheckerRSC(object):
 
         variables = []
         for entity in self.rs.background_set:
-            variables.append(Int("C"+str(level)+"_"+entity))
+            variables.append(Int("C" + str(level) + "_" + entity))
 
         self.v_ctx.append(variables)
 
@@ -73,10 +71,10 @@ class SmtCheckerRSC(object):
 
         variables = []
         for entity in self.rs.background_set:
-            variables.append(Int("L"+str(level)+"_"+entity))
+            variables.append(Int("L" + str(level) + "_" + entity))
         self.v.append(variables)
 
-        self.ca_state.append(Int("CA"+str(level)+"_state"))
+        self.ca_state.append(Int("CA" + str(level) + "_state"))
 
     def enc_concentration_levels_assertion(self, level):
         """Encodes assertions that (some) variables need to be >0
@@ -92,7 +90,8 @@ class SmtCheckerRSC(object):
             v_ctx = self.v_ctx[level][e_i]
             e_max = self.rs.get_max_concentration_level(e_i)
             enc_nz = simplify(
-                And(enc_nz, v >= 0, v_ctx >= 0, v <= e_max, v_ctx <= e_max))
+                And(enc_nz, v >= 0, v_ctx >= 0, v <= e_max, v_ctx <= e_max)
+            )
 
         return enc_nz
 
@@ -116,8 +115,7 @@ class SmtCheckerRSC(object):
 
         rcts_for_prod_entity = []
         if prod_entity in self.rs.get_reactions_by_product():
-            rcts_for_prod_entity = self.rs.get_reactions_by_product()[
-                prod_entity]
+            rcts_for_prod_entity = self.rs.get_reactions_by_product()[prod_entity]
 
         meta_reactions = []
         if prod_entity in self.rs.meta_reactions:
@@ -129,7 +127,7 @@ class SmtCheckerRSC(object):
 
         if rcts_for_prod_entity == [] and meta_reactions == []:
             # this should never happen
-            return simplify(self.v[level+1][prod_entity] == 0)
+            return simplify(self.v[level + 1][prod_entity] == 0)
 
         enc_enabledness = False
 
@@ -140,30 +138,42 @@ class SmtCheckerRSC(object):
         enc_ordinary_reactions_enabledness = False
 
         for reactants, inhibitors, products in rcts_for_prod_entity:
-
             enc_reactants = True
             for reactant, concentration in reactants:
-                enc_reactants = simplify(And(enc_reactants, Or(
-                    self.v[level][reactant] >= concentration, self.v_ctx[level][reactant] >= concentration)))
+                enc_reactants = simplify(
+                    And(
+                        enc_reactants,
+                        Or(
+                            self.v[level][reactant] >= concentration,
+                            self.v_ctx[level][reactant] >= concentration,
+                        ),
+                    )
+                )
 
             enc_inhibitors = True
             for inhibitor, concentration in inhibitors:
-                enc_inhibitors = simplify(And(enc_inhibitors, And(
-                    self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
+                enc_inhibitors = simplify(
+                    And(
+                        enc_inhibitors,
+                        And(
+                            self.v[level][inhibitor] < concentration,
+                            self.v_ctx[level][inhibitor] < concentration,
+                        ),
+                    )
+                )
 
             enc_rct_enabled = And(enc_reactants, enc_inhibitors)
-            enc_products = self.v[level+1][products[0][0]] == products[0][1]
-            enc_rct_prod = simplify(
-                If(enc_rct_enabled, enc_products, enc_rct_prod))
+            enc_products = self.v[level + 1][products[0][0]] == products[0][1]
+            enc_rct_prod = simplify(If(enc_rct_enabled, enc_products, enc_rct_prod))
             enc_enabledness = simplify(Or(enc_enabledness, enc_rct_enabled))
 
             enc_ordinary_reactions_enabledness = simplify(
-                Or(enc_ordinary_reactions_enabledness, enc_rct_enabled))
+                Or(enc_ordinary_reactions_enabledness, enc_rct_enabled)
+            )
 
         # -------- meta reactions ---------------------------------------------------
 
         for r_type, command_entity, reactants, inhibitors in meta_reactions:
-
             # command entity is e.g. 'inc' for incrementation operation
             # (inc,W) gives us the value W by which the given entity's value should be incremented
 
@@ -171,100 +181,127 @@ class SmtCheckerRSC(object):
             enc_inhibitors = True
 
             for reactant, concentration in reactants:
-                enc_reactants = simplify(And(enc_reactants, Or(
-                    self.v[level][reactant] >= concentration, self.v_ctx[level][reactant] >= concentration)))
+                enc_reactants = simplify(
+                    And(
+                        enc_reactants,
+                        Or(
+                            self.v[level][reactant] >= concentration,
+                            self.v_ctx[level][reactant] >= concentration,
+                        ),
+                    )
+                )
 
             # command entity needs to be present (with concentration level > 0) in order to perform the operation
-            enc_reactants = simplify(And(enc_reactants, Or(
-                self.v[level][command_entity] > 0, self.v_ctx[level][command_entity] > 0)))
+            enc_reactants = simplify(
+                And(
+                    enc_reactants,
+                    Or(
+                        self.v[level][command_entity] > 0,
+                        self.v_ctx[level][command_entity] > 0,
+                    ),
+                )
+            )
 
             for inhibitor, concentration in inhibitors:
-                enc_inhibitors = simplify(And(enc_inhibitors, And(
-                    self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
+                enc_inhibitors = simplify(
+                    And(
+                        enc_inhibitors,
+                        And(
+                            self.v[level][inhibitor] < concentration,
+                            self.v_ctx[level][inhibitor] < concentration,
+                        ),
+                    )
+                )
 
             if r_type == "inc":
                 value_after_inc = If(
-                    self.v[level][prod_entity] > self.v_ctx[level]
-                    [prod_entity],
+                    self.v[level][prod_entity] > self.v_ctx[level][prod_entity],
                     self.v[level][prod_entity],
-                    self.v_ctx[level][prod_entity]) + If(
-                    self.v[level][command_entity] > self.
-                    v_ctx[level][command_entity],
+                    self.v_ctx[level][prod_entity],
+                ) + If(
+                    self.v[level][command_entity] > self.v_ctx[level][command_entity],
                     self.v[level][command_entity],
-                    self.v_ctx[level][command_entity])
-                enc_products = self.v[level+1][prod_entity] == value_after_inc
+                    self.v_ctx[level][command_entity],
+                )
+                enc_products = self.v[level + 1][prod_entity] == value_after_inc
 
             elif r_type == "dec":
                 value_after_dec = simplify(
                     If(
-                        self.v[level][prod_entity] >
-                        self.v_ctx[level]
-                        [prod_entity],
+                        self.v[level][prod_entity] > self.v_ctx[level][prod_entity],
                         self.v[level][prod_entity],
-                        self.v_ctx[level]
-                        [prod_entity]) -
-                    If(
-                        self.v[level]
-                        [command_entity] > self.
-                        v_ctx[level][command_entity],
-                        self.v[level]
-                        [command_entity],
-                        self.v_ctx[level]
-                        [command_entity]))
-                enc_products = self.v[level+1][prod_entity] == If(
-                    value_after_dec < 0, 0, value_after_dec)
+                        self.v_ctx[level][prod_entity],
+                    )
+                    - If(
+                        self.v[level][command_entity]
+                        > self.v_ctx[level][command_entity],
+                        self.v[level][command_entity],
+                        self.v_ctx[level][command_entity],
+                    )
+                )
+                enc_products = self.v[level + 1][prod_entity] == If(
+                    value_after_dec < 0, 0, value_after_dec
+                )
 
             else:
-                raise RuntimeError(
-                    "Unknown meta-reaction type: " + repr(r_type))
+                raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
 
             enc_meta_reaction_enabledness = And(
-                enc_reactants, enc_inhibitors,
-                Not(enc_ordinary_reactions_enabledness))
+                enc_reactants, enc_inhibitors, Not(enc_ordinary_reactions_enabledness)
+            )
             enc_enabledness = simplify(
-                Or(enc_enabledness, enc_meta_reaction_enabledness))
-            enc_rct_prod = simplify(Or(enc_rct_prod, And(
-                enc_meta_reaction_enabledness, enc_products)))
+                Or(enc_enabledness, enc_meta_reaction_enabledness)
+            )
+            enc_rct_prod = simplify(
+                Or(enc_rct_prod, And(enc_meta_reaction_enabledness, enc_products))
+            )
 
         # -----------------------------------------------------------------------------
 
         if not permanency_inhibition == None:
-
-            enc_reactants = Or(self.v[level][prod_entity] >= concentration,
-                               self.v_ctx[level][prod_entity] >= concentration)
+            enc_reactants = Or(
+                self.v[level][prod_entity] >= concentration,
+                self.v_ctx[level][prod_entity] >= concentration,
+            )
 
             enc_inhibitors = True
             for inhibitor, concentration in permanency_inhibition:
-                enc_inhibitors = simplify(And(enc_inhibitors, And(
-                    self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
+                enc_inhibitors = simplify(
+                    And(
+                        enc_inhibitors,
+                        And(
+                            self.v[level][inhibitor] < concentration,
+                            self.v_ctx[level][inhibitor] < concentration,
+                        ),
+                    )
+                )
             enc_products = simplify(
-                self.v[level + 1][prod_entity] ==
-                If(
-                    self.v[level][prod_entity] > self.v_ctx[level]
-                    [prod_entity],
+                self.v[level + 1][prod_entity]
+                == If(
+                    self.v[level][prod_entity] > self.v_ctx[level][prod_entity],
                     self.v[level][prod_entity],
-                    self.v_ctx[level][prod_entity]))
+                    self.v_ctx[level][prod_entity],
+                )
+            )
 
             enc_permanency_enabledness = And(
-                enc_reactants, enc_inhibitors,
-                Not(enc_ordinary_reactions_enabledness))
-            enc_enabledness = simplify(
-                Or(enc_enabledness, enc_permanency_enabledness))
+                enc_reactants, enc_inhibitors, Not(enc_ordinary_reactions_enabledness)
+            )
+            enc_enabledness = simplify(Or(enc_enabledness, enc_permanency_enabledness))
             enc_permanency = And(enc_permanency_enabledness, enc_products)
             enc_rct_prod = simplify(Or(enc_rct_prod, enc_permanency))
 
         # -----------------------------------------------------------------------------
 
         enc_when_to_produce_zero_conc = simplify(
-            And(Not(enc_enabledness), self.v[level+1][prod_entity] == 0))
+            And(Not(enc_enabledness), self.v[level + 1][prod_entity] == 0)
+        )
 
         enc_rct_prod = Or(enc_rct_prod, enc_when_to_produce_zero_conc)
         return enc_rct_prod
 
     def enc_transition_relation(self, level):
-        return simplify(
-            And(self.enc_rs_trans(level),
-                self.enc_automaton_trans(level)))
+        return simplify(And(self.enc_rs_trans(level), self.enc_automaton_trans(level)))
 
     def enc_rs_trans(self, level):
         """Encodes the transition relation"""
@@ -279,11 +316,11 @@ class SmtCheckerRSC(object):
         for prod_entity in chain(reactions, meta_reactions):
             unused_entities.discard(prod_entity)
             enc_trans = simplify(
-                And(enc_trans, self.enc_produced_concentration(level, prod_entity)))
+                And(enc_trans, self.enc_produced_concentration(level, prod_entity))
+            )
 
         for prod_entity in unused_entities:
-            enc_trans = simplify(
-                And(enc_trans, self.v[level+1][prod_entity] == 0))
+            enc_trans = simplify(And(enc_trans, self.v[level + 1][prod_entity] == 0))
 
         return enc_trans
 
@@ -294,7 +331,7 @@ class SmtCheckerRSC(object):
 
         for src, ctx, dst in self.ca.transitions:
             src_enc = self.ca_state[level] == src
-            dst_enc = self.ca_state[level+1] == dst
+            dst_enc = self.ca_state[level + 1] == dst
 
             all_ent = set(range(len(self.rs.background_set)))
 
@@ -346,14 +383,12 @@ class SmtCheckerRSC(object):
         return simplify(enc)
 
     def decode_witness(self, max_level, print_model=False):
-
         m = self.solver.model()
 
         if print_model:
             print(m)
 
-        for level in range(max_level+1):
-
+        for level in range(max_level + 1):
             print("\n{: >70}".format("[ level=" + repr(level) + " ]"))
 
             print("  State: {", end=""),
@@ -361,11 +396,10 @@ class SmtCheckerRSC(object):
                 var_rep = repr(m[self.v[level][var_id]])
                 if not var_rep.isdigit():
                     raise RuntimeError(
-                        "unexpected: representation is not a positive integer")
+                        "unexpected: representation is not a positive integer"
+                    )
                 if int(var_rep) > 0:
-                    print(
-                        " " + self.rs.get_entity_name(var_id) + "=" + var_rep,
-                        end="")
+                    print(" " + self.rs.get_entity_name(var_id) + "=" + var_rep, end="")
                 # print(" " + repr(m[self.v[level][var_id]]), end="")
             print(" }")
 
@@ -376,22 +410,28 @@ class SmtCheckerRSC(object):
                     var_rep = repr(m[self.v_ctx[level][var_id]])
                     if not var_rep.isdigit():
                         raise RuntimeError(
-                            "unexpected: representation is not a positive integer")
+                            "unexpected: representation is not a positive integer"
+                        )
                     if int(var_rep) > 0:
                         print(
                             " " + self.rs.get_entity_name(var_id) + "=" + var_rep,
-                            end="")
+                            end="",
+                        )
                 print(" }")
 
     def check_rsltl(
-            self, formula, print_witness=True, print_time=True, print_mem=True,
-            max_level=None):
+        self,
+        formula,
+        print_witness=True,
+        print_time=True,
+        print_mem=True,
+        max_level=None,
+    ):
         """Bounded Model Checking for rsLTL properties"""
 
         self.reset()
 
-        print("[" + colour_str(C_BOLD, "i") +
-              "] Running rsLTL bounded model checking")
+        print("[" + colour_str(C_BOLD, "i") + "] Running rsLTL bounded model checking")
         print("[" + colour_str(C_BOLD, "i") + "] Formula: " + str(formula))
 
         if print_time:
@@ -408,48 +448,61 @@ class SmtCheckerRSC(object):
 
         encoder = rsLTL_Encoder(self)
         encoder.load_variables(
-            var_rs=self.v,
-            var_ctx=self.v_ctx,
-            var_loop_pos=self.loop_position)
+            var_rs=self.v, var_ctx=self.v_ctx, var_loop_pos=self.loop_position
+        )
 
         while True:
             self.prepare_all_variables()
             self.solver.add(
-                self.enc_concentration_levels_assertion(
-                    self.current_level + 1))
+                self.enc_concentration_levels_assertion(self.current_level + 1)
+            )
 
             print(
-                "\n{:-^70}".format("[ Working at level=" + str(self.current_level) + " ]"))
+                "\n{:-^70}".format(
+                    "[ Working at level=" + str(self.current_level) + " ]"
+                )
+            )
             stdout.flush()
 
             # reachability test:
             self.solver.push()
 
-            print("[" + colour_str(C_BOLD, "i") +
-                  "] Generating the formula encoding...")
+            print(
+                "[" + colour_str(C_BOLD, "i") + "] Generating the formula encoding..."
+            )
 
             f = encoder.get_encoding(formula, self.current_level)
             ncalls = encoder.get_ncalls()
 
-            print("[" + colour_str(C_BOLD, "i") + "] Cache hits: " +
-                  str(encoder.get_cache_hits()) + ", encode calls: " +
-                  str(ncalls[0]) + " (approx: " + str(ncalls[1]) + ")")
-            print("[" + colour_str(C_BOLD, "i") +
-                  "] Adding the formula to the solver...")
+            print(
+                "["
+                + colour_str(C_BOLD, "i")
+                + "] Cache hits: "
+                + str(encoder.get_cache_hits())
+                + ", encode calls: "
+                + str(ncalls[0])
+                + " (approx: "
+                + str(ncalls[1])
+                + ")"
+            )
+            print(
+                "[" + colour_str(C_BOLD, "i") + "] Adding the formula to the solver..."
+            )
 
             encoder.flush_cache()
             self.solver.add(f)
 
-            print("[" + colour_str(C_BOLD, "i") +
-                  "] Adding the loops encoding...")
+            print("[" + colour_str(C_BOLD, "i") + "] Adding the loops encoding...")
             self.solver.add(self.get_loop_encodings())
 
             result = self.solver.check()
             if result == sat:
                 print(
-                    "[" + colour_str(C_BOLD, "+") + "] " +
-                    colour_str(
-                        C_GREEN, "SAT at level=" + str(self.current_level)))
+                    "["
+                    + colour_str(C_BOLD, "+")
+                    + "] "
+                    + colour_str(C_GREEN, "SAT at level=" + str(self.current_level))
+                )
                 if print_witness:
                     print("\n{:=^70}".format("[ WITNESS ]"))
                     self.decode_witness(self.current_level)
@@ -457,12 +510,10 @@ class SmtCheckerRSC(object):
             else:
                 self.solver.pop()
 
-            print("[" + colour_str(C_BOLD, "i") +
-                  "] Unrolling the transition relation")
+            print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation")
             self.solver.add(self.enc_transition_relation(self.current_level))
 
-            print(
-                "{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
+            print("{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
             self.current_level += 1
 
             if not max_level is None and self.current_level > max_level:
@@ -472,25 +523,29 @@ class SmtCheckerRSC(object):
         if print_time:
             # stop = time()
             stop = resource.getrusage(resource.RUSAGE_SELF).ru_utime
-            self.verification_time = stop-start
+            self.verification_time = stop - start
             print()
             print(
-                "\n[i] {: >60}".format(
-                    " Time: " + repr(self.verification_time) + " s"))
+                "\n[i] {: >60}".format(" Time: " + repr(self.verification_time) + " s")
+            )
 
         if print_mem:
             print(
                 "[i] {: >60}".format(
-                    " Memory: " +
-                    repr(
-                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
-                        (1024 * 1024)) + " MB"))
+                    " Memory: "
+                    + repr(
+                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss
+                        / (1024 * 1024)
+                    )
+                    + " MB"
+                )
+            )
 
     def dummy_unroll(self, levels):
         """Unrolls the variables for testing purposes"""
 
         self.current_level = -1
-        for i in range(levels+1):
+        for i in range(levels + 1):
             self.prepare_all_variables()
             self.current_level += 1
 
@@ -511,7 +566,6 @@ class SmtCheckerRSC(object):
         return eq_enc
 
     def get_loop_encodings(self):
-
         k = self.current_level
         loop_var = self.loop_position
 
@@ -523,14 +577,16 @@ class SmtCheckerRSC(object):
         Therefore, the encoding starts at 1, not at 0.
         """
 
-        for i in range(1, k+1):
-            loop_enc = simplify(And(loop_enc, Implies(
-                loop_var == i, self.state_equality(i-1, k))))
+        for i in range(1, k + 1):
+            loop_enc = simplify(
+                And(loop_enc, Implies(loop_var == i, self.state_equality(i - 1, k)))
+            )
 
         return loop_enc
 
-    def check_reachability(self, state, print_witness=True,
-                           print_time=True, print_mem=True, max_level=1000):
+    def check_reachability(
+        self, state, print_witness=True, print_time=True, print_mem=True, max_level=1000
+    ):
         """Main testing function"""
 
         self.reset()
@@ -550,27 +606,30 @@ class SmtCheckerRSC(object):
         while True:
             self.prepare_all_variables()
             self.solver.add(
-                self.enc_concentration_levels_assertion(
-                    self.current_level + 1))
+                self.enc_concentration_levels_assertion(self.current_level + 1)
+            )
 
             print(
-                "\n{:-^70}".format("[ Working at level=" + str(self.current_level) + " ]"))
+                "\n{:-^70}".format(
+                    "[ Working at level=" + str(self.current_level) + " ]"
+                )
+            )
             stdout.flush()
 
             # reachability test:
-            print("[" + colour_str(C_BOLD, "i") +
-                  "] Adding the reachability test...")
+            print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...")
             self.solver.push()
 
-            self.solver.add(self.enc_state_with_blocking(
-                self.current_level, state))
+            self.solver.add(self.enc_state_with_blocking(self.current_level, state))
 
             result = self.solver.check()
             if result == sat:
                 print(
-                    "[" + colour_str(C_BOLD, "+") + "] " +
-                    colour_str(
-                        C_GREEN, "SAT at level=" + str(self.current_level)))
+                    "["
+                    + colour_str(C_BOLD, "+")
+                    + "] "
+                    + colour_str(C_GREEN, "SAT at level=" + str(self.current_level))
+                )
                 if print_witness:
                     print("\n{:=^70}".format("[ WITNESS ]"))
                     self.decode_witness(self.current_level)
@@ -578,12 +637,10 @@ class SmtCheckerRSC(object):
             else:
                 self.solver.pop()
 
-            print("[" + colour_str(C_BOLD, "i") +
-                  "] Unrolling the transition relation")
+            print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation")
             self.solver.add(self.enc_transition_relation(self.current_level))
 
-            print(
-                "{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
+            print("{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
             self.current_level += 1
 
             if self.current_level > max_level:
@@ -593,25 +650,35 @@ class SmtCheckerRSC(object):
         if print_time:
             # stop = time()
             stop = resource.getrusage(resource.RUSAGE_SELF).ru_utime
-            self.verification_time = stop-start
+            self.verification_time = stop - start
             print()
             print(
-                "\n[i] {: >60}".format(
-                    " Time: " + repr(self.verification_time) + " s"))
+                "\n[i] {: >60}".format(" Time: " + repr(self.verification_time) + " s")
+            )
 
         if print_mem:
             print(
                 "[i] {: >60}".format(
-                    " Memory: " +
-                    repr(
-                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
-                        (1024 * 1024)) + " MB"))
+                    " Memory: "
+                    + repr(
+                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss
+                        / (1024 * 1024)
+                    )
+                    + " MB"
+                )
+            )
 
     def get_verification_time(self):
         return self.verification_time
 
-    def show_encoding(self, state, print_witness=True,
-                      print_time=False, print_mem=False, max_level=100):
+    def show_encoding(
+        self,
+        state,
+        print_witness=True,
+        print_time=False,
+        print_mem=False,
+        max_level=100,
+    ):
         """Encoding debug function"""
 
         self.reset()
@@ -627,8 +694,7 @@ class SmtCheckerRSC(object):
         while True:
             self.prepare_all_variables()
 
-            print(
-                "-----[ Working at level=" + str(self.current_level) + " ]-----")
+            print("-----[ Working at level=" + str(self.current_level) + " ]-----")
             stdout.flush()
 
             # reachability test:
@@ -643,9 +709,9 @@ class SmtCheckerRSC(object):
             result = self.solver.check()
             if result == sat:
                 print(
-                    "\n[+] " +
-                    colour_str(
-                        C_RED, "SAT at level=" + str(self.current_level)))
+                    "\n[+] "
+                    + colour_str(C_RED, "SAT at level=" + str(self.current_level))
+                )
                 if print_witness:
                     self.decode_witness(self.current_level)
                 break

reactics-smt/smt/smt_checker_rsc_param.py

@@ -23,14 +23,13 @@ def z3_max(a, b):
 
 
 class SmtCheckerRSCParam(object):
-
     def __init__(self, rsca, optimise=False):
-
         rsca.sanity_check()
 
         if not rsca.is_concentr_and_param_compatible():
             raise RuntimeError(
-                "RS and CA with concentrations (and parameters) expected")
+                "RS and CA with concentrations (and parameters) expected"
+            )
 
         self.rs = rsca.rs
         self.ca = rsca.ca
@@ -92,7 +91,6 @@ class SmtCheckerRSCParam(object):
         self.initialise()
 
     def prepare_all_variables(self, num_of_paths):
-
         for path_idx in range(num_of_paths):
             self.prepare_all_path_variables(path_idx)
         self.next_level_to_encode += 1
@@ -100,8 +98,11 @@ class SmtCheckerRSCParam(object):
     def prepare_all_path_variables(self, path_idx):
         """Prepares the variables for a given path index"""
 
-        print_info("Preparing variables for path={:d} (level={:d})".format(
-            path_idx, self.next_level_to_encode))
+        print_info(
+            "Preparing variables for path={:d} (level={:d})".format(
+                path_idx, self.next_level_to_encode
+            )
+        )
 
         self.prepare_state_variables(path_idx)
         self.prepare_context_variables(path_idx)
@@ -111,8 +112,7 @@ class SmtCheckerRSCParam(object):
     def prepare_loop_position_variables(self, path_idx):
         """Prepares the variables for loop positions"""
 
-        self.path_loop_position[path_idx] = Int(
-            "p{:d}_loop_pos".format(path_idx))
+        self.path_loop_position[path_idx] = Int("p{:d}_loop_pos".format(path_idx))
 
     def prepare_context_variables(self, path_idx):
         """Prepares all the context variables"""
@@ -188,22 +188,26 @@ class SmtCheckerRSCParam(object):
             entities_dict = dict()
 
             if is_param(products):
-
                 for entity in self.rs.set_of_bgset_ids:
                     entity_name = self.rs.get_entity_name(entity)
-                    new_var = Int("p{:d}L{:d}_ImProd_r{:d}_{:s}".format(
-                        path_idx, level, reaction_id, entity_name))
+                    new_var = Int(
+                        "p{:d}L{:d}_ImProd_r{:d}_{:s}".format(
+                            path_idx, level, reaction_id, entity_name
+                        )
+                    )
                     entities_dict[entity] = new_var
 
                     all_entities_dict.setdefault(entity, [])
                     all_entities_dict[entity].append(new_var)
 
             else:
-
                 for entity, conc in products:
                     entity_name = self.rs.get_entity_name(entity)
-                    new_var = Int("p{:d}L{:d}_ImProd_r{:d}_{:s}".format(
-                        path_idx, level, reaction_id, entity_name))
+                    new_var = Int(
+                        "p{:d}L{:d}_ImProd_r{:d}_{:s}".format(
+                            path_idx, level, reaction_id, entity_name
+                        )
+                    )
                     entities_dict[entity] = new_var
 
                     all_entities_dict.setdefault(entity, [])
@@ -224,14 +228,13 @@ class SmtCheckerRSCParam(object):
         """
 
         for param_name in self.rs.parameters.keys():
-
             # we start collecting bg-related vars for the given param
             vars_for_param = []
 
             for entity in self.rs.ordered_list_of_bgset_ids:
                 new_var = Int(
-                    "Pm{:s}_{:s}".format(
-                        param_name, self.rs.get_entity_name(entity)))
+                    "Pm{:s}_{:s}".format(param_name, self.rs.get_entity_name(entity))
+                )
                 vars_for_param.append(new_var)
 
             self.v_param[param_name] = vars_for_param
@@ -266,23 +269,17 @@ class SmtCheckerRSCParam(object):
         enc_non_empty = True
 
         for param_vars in self.v_param.values():
-
             enc_param_at_least_one = False
             for pvar in param_vars:
-
                 # TODO: fixed upper limit: 100 (have a per-param setting for that)
-                enc_param_gz = simplify(
-                    And(enc_param_gz, pvar >= 0, pvar < 100))
-                enc_param_at_least_one = simplify(
-                    Or(enc_param_at_least_one, pvar > 0))
+                enc_param_gz = simplify(And(enc_param_gz, pvar >= 0, pvar < 100))
+                enc_param_at_least_one = simplify(Or(enc_param_at_least_one, pvar > 0))
 
-            enc_non_empty = simplify(
-                And(enc_non_empty, enc_param_at_least_one))
+            enc_non_empty = simplify(And(enc_non_empty, enc_param_at_least_one))
 
         return simplify(And(enc_param_gz, enc_non_empty))
 
     def assert_param_optimisation(self):
-
         for param_vars in self.v_param.values():
             for pvar in param_vars:
                 # self.solver.add_soft(pvar == 0)
@@ -296,8 +293,11 @@ class SmtCheckerRSCParam(object):
         only those that can possibly go below 0.
         """
 
-        print_info("Concentration level assertions for path={:d} (level={:d})".format(
-            path_idx, level))
+        print_info(
+            "Concentration level assertions for path={:d} (level={:d})".format(
+                path_idx, level
+            )
+        )
 
         enc_gz = True
 
@@ -305,15 +305,14 @@ class SmtCheckerRSCParam(object):
             var = self.path_v[path_idx][level][e_i]
             var_ctx = self.path_v_ctx[path_idx][level][e_i]
             e_max = self.rs.get_max_concentration_level(e_i)
-            enc_gz = simplify(And(enc_gz, var >= 0, var_ctx >=
-                                  0, var <= e_max, var_ctx <= e_max))
+            enc_gz = simplify(
+                And(enc_gz, var >= 0, var_ctx >= 0, var <= e_max, var_ctx <= e_max)
+            )
 
-            vars_per_reaction = self.path_v_improd_for_entities[path_idx][
-                level + 1]
+            vars_per_reaction = self.path_v_improd_for_entities[path_idx][level + 1]
             if e_i in vars_per_reaction:
                 for var_improd in vars_per_reaction[e_i]:
-                    enc_gz = simplify(
-                        And(enc_gz, var_improd >= 0, var_improd <= e_max))
+                    enc_gz = simplify(And(enc_gz, var_improd >= 0, var_improd <= e_max))
 
         return enc_gz
 
@@ -326,7 +325,8 @@ class SmtCheckerRSCParam(object):
             # the initial concentration levels are zeroed
             rs_init_state_enc = simplify(And(rs_init_state_enc, v == 0))
 
-        ca_init_state_enc = self.path_ca_state[path_idx][level] == self.ca.get_init_state_id(
+        ca_init_state_enc = (
+            self.path_ca_state[path_idx][level] == self.ca.get_init_state_id()
         )
 
         init_state_enc = simplify(And(rs_init_state_enc, ca_init_state_enc))
@@ -335,8 +335,11 @@ class SmtCheckerRSCParam(object):
 
     def enc_transition_relation(self, level, path_idx):
         return simplify(
-            And(self.enc_rs_trans(level, path_idx),
-                self.enc_automaton_trans(level, path_idx)))
+            And(
+                self.enc_rs_trans(level, path_idx),
+                self.enc_automaton_trans(level, path_idx),
+            )
+        )
 
     def enc_param_sanity_for_reactions(self):
         """R < I constraint (R n I = 0)"""
@@ -344,23 +347,21 @@ class SmtCheckerRSCParam(object):
         rct_inh_constr = True
 
         for reactants, inhibitors, products in self.rs.reactions:
-
             if is_param(reactants) or is_param(inhibitors):
-
                 # 1. R and I
                 if is_param(reactants) and is_param(inhibitors):
                     rct_param_name = reactants.name
                     inh_param_name = inhibitors.name
 
                     for entity in self.rs.set_of_bgset_ids:
-                        rct_inh_constr = And(rct_inh_constr,
+                        rct_inh_constr = And(
+                            rct_inh_constr,
                             Implies(
-                                                 self.v_param
-                                                 [inh_param_name][entity] > 0,
-                                                 self.v_param
-                                                 [rct_param_name][entity] <
-                                                 self.v_param
-                                                 [inh_param_name][entity]))
+                                self.v_param[inh_param_name][entity] > 0,
+                                self.v_param[rct_param_name][entity]
+                                < self.v_param[inh_param_name][entity],
+                            ),
+                        )
 
             elif (not is_param(reactants)) and is_param(inhibitors):
                 inh_param_name = inhibitors.name
@@ -370,8 +371,10 @@ class SmtCheckerRSCParam(object):
                     rct_inh_constr = And(
                         rct_inh_constr,
                         Implies(
-                            self.v_param[inh_param_name][entity] > 0, conc <
-                            self.v_param[inh_param_name][entity]))
+                            self.v_param[inh_param_name][entity] > 0,
+                            conc < self.v_param[inh_param_name][entity],
+                        ),
+                    )
 
             elif is_param(reactants) and (not is_param(inhibitors)):
                 rct_param_name = reactants.name
@@ -379,7 +382,8 @@ class SmtCheckerRSCParam(object):
                 for entity, conc in inhibitors:
                     assert conc > 0, "Unexpected concentration level!"
                     rct_inh_constr = And(
-                        rct_inh_constr, self.v_param[rct_param_name][entity] < conc)
+                        rct_inh_constr, self.v_param[rct_param_name][entity] < conc
+                    )
 
         return rct_inh_constr
 
@@ -405,31 +409,52 @@ class SmtCheckerRSCParam(object):
         if is_param(reactants):
             param_name = reactants.name
             for entity in self.rs.set_of_bgset_ids:
-                enc_reactants = And(enc_reactants, Or(
+                enc_reactants = And(
+                    enc_reactants,
+                    Or(
                         self.v_param[param_name][entity] == 0,
-                    self.path_v[path_idx][level][entity] >= self.v_param[param_name][entity],
-                    self.path_v_ctx[path_idx][level][entity] >= self.v_param[param_name][entity]))
+                        self.path_v[path_idx][level][entity]
+                        >= self.v_param[param_name][entity],
+                        self.path_v_ctx[path_idx][level][entity]
+                        >= self.v_param[param_name][entity],
+                    ),
+                )
         else:
             for entity, conc in reactants:
-                enc_reactants = And(enc_reactants, Or(
+                enc_reactants = And(
+                    enc_reactants,
+                    Or(
                         self.path_v[path_idx][level][entity] >= conc,
-                    self.path_v_ctx[path_idx][level][entity] >= conc))
+                        self.path_v_ctx[path_idx][level][entity] >= conc,
+                    ),
+                )
 
         # ** INHIBITORS ******************************************
         enc_inhibitors = True
         if is_param(inhibitors):
             param_name = inhibitors.name
             for entity in self.rs.set_of_bgset_ids:
-                enc_inhibitors = And(enc_inhibitors, Or(
+                enc_inhibitors = And(
+                    enc_inhibitors,
+                    Or(
                         self.v_param[param_name][entity] == 0,
                         And(
-                        self.path_v[path_idx][level][entity] < self.v_param[param_name][entity],
-                        self.path_v_ctx[path_idx][level][entity] < self.v_param[param_name][entity])))
+                            self.path_v[path_idx][level][entity]
+                            < self.v_param[param_name][entity],
+                            self.path_v_ctx[path_idx][level][entity]
+                            < self.v_param[param_name][entity],
+                        ),
+                    ),
+                )
         else:
             for entity, conc in inhibitors:
-                enc_inhibitors = And(enc_inhibitors, And(
+                enc_inhibitors = And(
+                    enc_inhibitors,
+                    And(
                         self.path_v[path_idx][level][entity] < conc,
-                    self.path_v_ctx[path_idx][level][entity] < conc))
+                        self.path_v_ctx[path_idx][level][entity] < conc,
+                    ),
+                )
 
         # ** PRODUCTS *******************************************
         enc_products = True
@@ -438,26 +463,38 @@ class SmtCheckerRSCParam(object):
             for entity in self.rs.set_of_bgset_ids:
                 enc_products = simplify(
                     And(
-                        enc_products, self.
-                        path_v_improd[path_idx]
-                        [level + 1][reaction_id]
-                        [entity] == self.v_param
-                        [param_name][entity]))
+                        enc_products,
+                        self.path_v_improd[path_idx][level + 1][reaction_id][entity]
+                        == self.v_param[param_name][entity],
+                    )
+                )
         else:
             for entity, conc in products:
-                enc_products = simplify(And(
-                    enc_products, self.path_v_improd[path_idx][level + 1][reaction_id][entity] == conc))
+                enc_products = simplify(
+                    And(
+                        enc_products,
+                        self.path_v_improd[path_idx][level + 1][reaction_id][entity]
+                        == conc,
+                    )
+                )
 
         # Nothing is produced (when the reaction is disabled)
         enc_no_prod = True
         if is_param(products):
             for entity in self.rs.set_of_bgset_ids:
                 enc_no_prod = And(
-                    enc_no_prod, self.path_v_improd[path_idx][level + 1][reaction_id][entity] == 0)
+                    enc_no_prod,
+                    self.path_v_improd[path_idx][level + 1][reaction_id][entity] == 0,
+                )
         else:
             for entity, _ in products:
-                enc_no_prod = simplify(And(
-                    enc_no_prod, self.path_v_improd[path_idx][level + 1][reaction_id][entity] == 0))
+                enc_no_prod = simplify(
+                    And(
+                        enc_no_prod,
+                        self.path_v_improd[path_idx][level + 1][reaction_id][entity]
+                        == 0,
+                    )
+                )
 
         #
         # (R and I) iff P
@@ -467,8 +504,7 @@ class SmtCheckerRSCParam(object):
         #
         # ~(R and I) iff P_zero
         #
-        enc_not_enabled = Not(
-            And(enc_reactants, enc_inhibitors)) == enc_no_prod
+        enc_not_enabled = Not(And(enc_reactants, enc_inhibitors)) == enc_no_prod
 
         enc_reaction = And(enc_enabled, enc_not_enabled)
 
@@ -491,7 +527,12 @@ class SmtCheckerRSCParam(object):
         enc_cond = False
         for entity in self.rs.set_of_bgset_ids:
             enc_cond = simplify(
-                Or(enc_cond, self.path_v[path_idx][level][entity] > 0, self.path_v_ctx[path_idx][level][entity] > 0))
+                Or(
+                    enc_cond,
+                    self.path_v[path_idx][level][entity] > 0,
+                    self.path_v_ctx[path_idx][level][entity] > 0,
+                )
+            )
 
         return enc_cond
 
@@ -533,25 +574,29 @@ class SmtCheckerRSCParam(object):
         #       =>
         #   {products}[level+1]
         #
-        current_v_improd_for_entities = self.path_v_improd_for_entities[path_idx][level + 1]
+        current_v_improd_for_entities = self.path_v_improd_for_entities[path_idx][
+            level + 1
+        ]
         for entity in self.rs.set_of_bgset_ids:
             per_reaction_vars = current_v_improd_for_entities.get(entity, [])
-            enc_max_prod = simplify(And(
-                enc_max_prod, self.path_v[path_idx][level + 1][entity] == self.enc_max(per_reaction_vars)))
+            enc_max_prod = simplify(
+                And(
+                    enc_max_prod,
+                    self.path_v[path_idx][level + 1][entity]
+                    == self.enc_max(per_reaction_vars),
+                )
+            )
 
         # make sure at least one entity is >0
-        enc_general_cond = self.enc_general_reaction_enabledness(
-            level, path_idx)
+        enc_general_cond = self.enc_general_reaction_enabledness(level, path_idx)
 
-        enc_trans_with_max = simplify(
-            And(enc_general_cond, enc_max_prod, enc_trans))
+        enc_trans_with_max = simplify(And(enc_general_cond, enc_max_prod, enc_trans))
 
         # print(enc_trans_with_max)
 
         return enc_trans_with_max
 
     def enc_max(self, elements):
-
         enc = None
 
         if elements == []:
@@ -561,7 +606,6 @@ class SmtCheckerRSCParam(object):
             enc = z3_max(0, elements[0])
 
         elif len(elements) > 1:
-
             enc = 0
             for i in range(len(elements) - 1):
                 enc = z3_max(enc, z3_max(elements[i], elements[i + 1]))
@@ -575,7 +619,7 @@ class SmtCheckerRSCParam(object):
 
         for src, ctx, dst in self.ca.transitions:
             src_enc = self.path_ca_state[path_idx][level] == src
-            dst_enc = self.path_ca_state[path_idx][level+1] == dst
+            dst_enc = self.path_ca_state[path_idx][level + 1] == dst
 
             all_ent = set(range(len(self.rs.background_set)))
 
@@ -586,11 +630,13 @@ class SmtCheckerRSCParam(object):
 
             for e, c in ctx:
                 ctx_enc = simplify(
-                    And(ctx_enc, self.path_v_ctx[path_idx][level][e] == c))
+                    And(ctx_enc, self.path_v_ctx[path_idx][level][e] == c)
+                )
 
             for e in excl_ctx:
                 ctx_enc = simplify(
-                    And(ctx_enc, self.path_v_ctx[path_idx][level][e] == 0))
+                    And(ctx_enc, self.path_v_ctx[path_idx][level][e] == 0)
+                )
 
             cur_trans = simplify(And(src_enc, ctx_enc, dst_enc))
             enc_trans = simplify(Or(enc_trans, cur_trans))
@@ -641,7 +687,6 @@ class SmtCheckerRSCParam(object):
             print(m)
 
         for level in range(max_level + 1):
-
             print("\n{: >70}".format("[ level=" + repr(level) + " ]"))
 
             print("  State: {", end=""),
@@ -649,11 +694,10 @@ class SmtCheckerRSCParam(object):
                 var_rep = repr(m[self.path_v[path_idx][level][var_id]])
                 if not var_rep.isdigit():
                     raise RuntimeError(
-                        "unexpected: representation is not a positive integer")
+                        "unexpected: representation is not a positive integer"
+                    )
                 if int(var_rep) > 0:
-                    print(
-                        " " + self.rs.get_entity_name(var_id) + "=" + var_rep,
-                        end="")
+                    print(" " + self.rs.get_entity_name(var_id) + "=" + var_rep, end="")
             print(" }")
 
             if level != max_level:
@@ -663,11 +707,13 @@ class SmtCheckerRSCParam(object):
                     var_rep = repr(m[self.path_v_ctx[path_idx][level][var_id]])
                     if not var_rep.isdigit():
                         raise RuntimeError(
-                            "unexpected: representation is not a positive integer")
+                            "unexpected: representation is not a positive integer"
+                        )
                     if int(var_rep) > 0:
                         print(
                             " " + self.rs.get_entity_name(var_id) + "=" + var_rep,
-                            end="")
+                            end="",
+                        )
                 print(" }")
 
         print()
@@ -675,29 +721,34 @@ class SmtCheckerRSCParam(object):
     def get_enc_formulae(self, encoder, formulae_list):
         enc_form = []
         for formula in formulae_list:
-
             path_idx = formulae_list.index(formula)
 
-            print_info("Generating the encoding for {:s} ({:d} of {:d})".format(
-                str(formula), path_idx+1, len(formulae_list)))
+            print_info(
+                "Generating the encoding for {:s} ({:d} of {:d})".format(
+                    str(formula), path_idx + 1, len(formulae_list)
+                )
+            )
 
             encoder.load_variables(
                 var_rs=self.path_v[path_idx],
                 var_ctx=self.path_v_ctx[path_idx],
-                var_loop_pos=self.path_loop_position[path_idx])
+                var_loop_pos=self.path_loop_position[path_idx],
+            )
 
             enc_form.append(encoder.get_encoding(formula, self.current_level))
             ncalls = encoder.get_ncalls()
 
-            print_info("Cache hits: {:d}, encode calls: {:d} (approx: {:d})".format(
-                encoder.get_cache_hits(), ncalls[0], ncalls[1]))
+            print_info(
+                "Cache hits: {:d}, encode calls: {:d} (approx: {:d})".format(
+                    encoder.get_cache_hits(), ncalls[0], ncalls[1]
+                )
+            )
 
             encoder.flush_cache()
 
         return enc_form
 
     def print_witness(self, formulae_list):
-
         for formula in formulae_list:
             path_idx = formulae_list.index(formula)
             print("\n{:=^70}".format("[ WITNESS ]"))
@@ -707,7 +758,6 @@ class SmtCheckerRSCParam(object):
         self.print_parameter_valuations()
 
     def print_parameter_valuations(self):
-
         m = self.solver.model()
 
         print("\n  Parameters:\n")
@@ -721,25 +771,24 @@ class SmtCheckerRSCParam(object):
                 var_rep = repr(m[params[entity]])
                 if not var_rep.isdigit():
                     raise RuntimeError(
-                        "unexpected: representation is not a positive integer")
+                        "unexpected: representation is not a positive integer"
+                    )
                 if int(var_rep) > 0:
                     print(
-                        " " + str(self.rs.get_entity_name(entity)) + "=" +
-                        str(var_rep),
-                        end="")
+                        " " + str(self.rs.get_entity_name(entity)) + "=" + str(var_rep),
+                        end="",
+                    )
             print(" }")
 
         print()
 
-    def enc_concentration_levels_assertions_for_paths(
-            self, level, num_of_paths):
-
+    def enc_concentration_levels_assertions_for_paths(self, level, num_of_paths):
         additional_assertions = []
         for path_idx in range(num_of_paths):
             additional_assertions.append(
-                self.enc_concentration_levels_assertion(level, path_idx))
-        additional_assertions.append(
-            self.enc_param_concentration_levels_assertion())
+                self.enc_concentration_levels_assertion(level, path_idx)
+            )
+        additional_assertions.append(self.enc_param_concentration_levels_assertion())
 
         return additional_assertions
 
@@ -750,15 +799,18 @@ class SmtCheckerRSCParam(object):
         return enc_trans
 
     def print_level(self):
-        print(
-            "{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
+        print("{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
 
     def check_rsltl(
-            self, formulae_list,
+        self,
+        formulae_list,
         print_witness=True,
-            print_time=True, print_mem=True,
-            max_level=None, cont_if_sat=False,
-            param_constr=None):
+        print_time=True,
+        print_mem=True,
+        max_level=None,
+        cont_if_sat=False,
+        param_constr=None,
+    ):
         """
         Bounded Model Checking for rsLTL properties
 
@@ -783,7 +835,7 @@ class SmtCheckerRSCParam(object):
         print_info("Running rsLTL bounded model checking")
         print_info("Tested formulae:")
         for form in formulae_list:
-            print_info(" "*4 + str(form))
+            print_info(" " * 4 + str(form))
 
         print_info("INITIALISING...")
 
@@ -804,8 +856,8 @@ class SmtCheckerRSCParam(object):
 
         # assertions for all the paths and parameters
         self.solver_add(
-            self.enc_concentration_levels_assertions_for_paths(
-                0, num_of_paths))
+            self.enc_concentration_levels_assertions_for_paths(0, num_of_paths)
+        )
         self.solver_add(self.enc_param_concentration_levels_assertion())
         self.solver_add(self.enc_param_sanity_for_reactions())
 
@@ -822,9 +874,11 @@ class SmtCheckerRSCParam(object):
         print_info("STARTING TO ITERATE...")
 
         while True:
-
             print(
-                "\n{:-^70}".format("[ Working at level=" + str(self.current_level) + " ]"))
+                "\n{:-^70}".format(
+                    "[ Working at level=" + str(self.current_level) + " ]"
+                )
+            )
 
             # reachability test:
             self.solver.push()
@@ -841,8 +895,9 @@ class SmtCheckerRSCParam(object):
             print_info("Testing satisfiability...")
             result = self.solver.check()
             if result == sat:
-                print_positive(green_str(
-                    "SAT at level={:d}".format(self.current_level)))
+                print_positive(
+                    green_str("SAT at level={:d}".format(self.current_level))
+                )
                 # print(self.solver.model())
                 if print_witness:
                     self.print_witness(formulae_list)
@@ -861,11 +916,14 @@ class SmtCheckerRSCParam(object):
             # assertions for all the paths
             self.solver_add(
                 self.enc_concentration_levels_assertions_for_paths(
-                    self.current_level + 1, num_of_paths))
+                    self.current_level + 1, num_of_paths
+                )
+            )
 
             print_info("Unrolling the transition relation")
-            self.solver_add(self.enc_transition_relation_for_paths(
-                self.current_level, num_of_paths))
+            self.solver_add(
+                self.enc_transition_relation_for_paths(self.current_level, num_of_paths)
+            )
 
             self.print_level()
 
@@ -880,22 +938,24 @@ class SmtCheckerRSCParam(object):
         stop = resource.getrusage(resource.RUSAGE_SELF).ru_utime
         self.verification_time = stop - start
         print()
-        print_info("{: >60}".format(
-            " Time: " + repr(self.verification_time) + " s"))
+        print_info("{: >60}".format(" Time: " + repr(self.verification_time) + " s"))
 
     def print_mem(self):
         print_info(
             "{: >60}".format(
-                " Memory: " +
-                repr(
-                    resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
-                    (1024 * 1024)) + " MB"))
+                " Memory: "
+                + repr(
+                    resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+                )
+                + " MB"
+            )
+        )
 
     def dummy_unroll(self, levels):
         """Unrolls the variables for testing purposes"""
 
         self.current_level = -1
-        for i in range(levels+1):
+        for i in range(levels + 1):
             self.prepare_all_variables()
             self.current_level += 1
 
@@ -916,7 +976,6 @@ class SmtCheckerRSCParam(object):
         return eq_enc
 
     def get_loop_encodings(self):
-
         k = self.current_level
         loop_var = self.loop_position
 
@@ -928,9 +987,10 @@ class SmtCheckerRSCParam(object):
         Therefore, the encoding starts at 1, not at 0.
         """
 
-        for i in range(1, k+1):
-            loop_enc = simplify(And(loop_enc, Implies(
-                loop_var == i, self.state_equality(i-1, k))))
+        for i in range(1, k + 1):
+            loop_enc = simplify(
+                And(loop_enc, Implies(loop_var == i, self.state_equality(i - 1, k)))
+            )
 
         return loop_enc
 
@@ -947,8 +1007,9 @@ class SmtCheckerRSCParam(object):
 
         self.solver.add(expression)
 
-    def check_reachability(self, state, print_witness=True,
-                           print_time=True, print_mem=True, max_level=1000):
+    def check_reachability(
+        self, state, print_witness=True, print_time=True, print_mem=True, max_level=1000
+    ):
         """Main testing function"""
 
         self.reset()
@@ -968,27 +1029,30 @@ class SmtCheckerRSCParam(object):
         while True:
             self.prepare_all_variables()
             self.solver_add(
-                self.enc_concentration_levels_assertion(
-                    self.current_level + 1))
+                self.enc_concentration_levels_assertion(self.current_level + 1)
+            )
 
             print(
-                "\n{:-^70}".format("[ Working at level=" + str(self.current_level) + " ]"))
+                "\n{:-^70}".format(
+                    "[ Working at level=" + str(self.current_level) + " ]"
+                )
+            )
             stdout.flush()
 
             # reachability test:
-            print("[" + colour_str(C_BOLD, "i") +
-                  "] Adding the reachability test...")
+            print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...")
             self.solver.push()
 
-            self.solver_add(self.enc_state_with_blocking(
-                self.current_level, state))
+            self.solver_add(self.enc_state_with_blocking(self.current_level, state))
 
             result = self.solver.check()
             if result == sat:
                 print(
-                    "[" + colour_str(C_BOLD, "+") + "] " +
-                    colour_str(
-                        C_GREEN, "SAT at level=" + str(self.current_level)))
+                    "["
+                    + colour_str(C_BOLD, "+")
+                    + "] "
+                    + colour_str(C_GREEN, "SAT at level=" + str(self.current_level))
+                )
                 if print_witness:
                     print("\n{:=^70}".format("[ WITNESS ]"))
                     self.decode_witness(self.current_level)
@@ -996,12 +1060,10 @@ class SmtCheckerRSCParam(object):
             else:
                 self.solver.pop()
 
-            print("[" + colour_str(C_BOLD, "i") +
-                  "] Unrolling the transition relation")
+            print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation")
             self.solver_add(self.enc_transition_relation(self.current_level))
 
-            print(
-                "{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
+            print("{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
             self.current_level += 1
 
             if self.current_level > max_level:
@@ -1011,25 +1073,35 @@ class SmtCheckerRSCParam(object):
         if print_time:
             # stop = time()
             stop = resource.getrusage(resource.RUSAGE_SELF).ru_utime
-            self.verification_time = stop-start
+            self.verification_time = stop - start
             print()
             print(
-                "\n[i] {: >60}".format(
-                    " Time: " + repr(self.verification_time) + " s"))
+                "\n[i] {: >60}".format(" Time: " + repr(self.verification_time) + " s")
+            )
 
         if print_mem:
             print(
                 "[i] {: >60}".format(
-                    " Memory: " +
-                    repr(
-                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
-                        (1024 * 1024)) + " MB"))
+                    " Memory: "
+                    + repr(
+                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss
+                        / (1024 * 1024)
+                    )
+                    + " MB"
+                )
+            )
 
     def get_verification_time(self):
         return self.verification_time
 
-    def show_encoding(self, state, print_witness=True,
-                      print_time=False, print_mem=False, max_level=100):
+    def show_encoding(
+        self,
+        state,
+        print_witness=True,
+        print_time=False,
+        print_mem=False,
+        max_level=100,
+    ):
         """Encoding debug function"""
 
         self.reset()
@@ -1045,8 +1117,7 @@ class SmtCheckerRSCParam(object):
         while True:
             self.prepare_all_variables()
 
-            print(
-                "-----[ Working at level=" + str(self.current_level) + " ]-----")
+            print("-----[ Working at level=" + str(self.current_level) + " ]-----")
             stdout.flush()
 
             # reachability test:
@@ -1061,9 +1132,9 @@ class SmtCheckerRSCParam(object):
             result = self.solver.check()
             if result == sat:
                 print(
-                    "\n[+] " +
-                    colour_str(
-                        C_RED, "SAT at level=" + str(self.current_level)))
+                    "\n[+] "
+                    + colour_str(C_RED, "SAT at level=" + str(self.current_level))
+                )
                 if print_witness:
                     self.decode_witness(self.current_level)
                 break