clean-up

LICENSE

@@ -0,0 +1,19 @@
+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.

README.md

@@ -3,6 +3,110 @@
 Reaction Systems Verification Toolkit
 
 The toolkit consists of two separate modules implementing:
-* BDD-based methods
+* Methods implemented using binary decision diagrams (BDD) for storing and manipulating the state space of the verified system.
-* SMT-based methods
+* Methods translating the verification problems into satisfiability modulo theories (SMT).
+
+# Installation
+
+## Installing everything manually
+
+(to be added)
+
+## Virtual Machine
+
+The easiest way to try out ReactICS is to download [the VM where everything is alread installed](http://reactionsystems.org/ReactICS.zip). This a VirtualBox virtual machine. After booting it up, you can log in as `reactics` with the same password. After logging in, ReactICS is available in the `reactics` directory:
+
+```
+$ cd reactics
+```
+
+An update and setup needs to be performed before running any type of verification:
+
+```
+$ ./reactics setup
+```
+
+After performing these steps you should be ready to start using ReactICS.
+
+## Examples
+
+The `examples` directory contains sample input files.
+
+### Multi-agent reaction systems (rsCTLK verification)
+
+To quickly test the BDD module you can perform verification of the TGC controller consiting of three trains:
+
+```
+$ ./reactics bdd -c f1 examples/bdd/tgc.rs
+```
+
+The above command tests the formula labelled `f1` in the input file.
+
+### Reachability
+
+To test the SMT module you can perform reachability verification of the scalable chain system:
+
+Running the benchmark without any arguments tells us what parameters are available:
+
+```
+$ ./reactics smt examples/smt/scalable_chain.py
+
+ ------------------------------------------------
+ -- ReactICS -- Reaction Systems Model Checker --
+ ------------------------------------------------
+
+arguments: <chainLen> <maxConc> <formulaNumber>
+```
+
+We may execute the benchmark for `chainLen=2`, `maxConc=3`, and `formulaNumber=1` using the following command:
+
+```
+$ ./reactics smt examples/smt/chain_reaction.py 2 3 1
+```
+
+### rsLTL verification
+
+To test the SMT module for rsLTL verification the scalable chain system benchmark may be used.
+
+
+
+```
+$ ./reactics smt examples/smt/scalable_chain.py 2 5 1
+```
+
+
+
+### Reaction synthesis
+
+To test the reaction synthesis approach on a mutual exclution protocol modelling three processes, run the following command (three processes, parametric verification, result optimised with OptSMT):
+
+```
+$ ./reactics smt examples/smt/mutex_param.py 3 p -o
+```
+
+To check the available parameters for the benchmark, we run it with `-h`:
+
+```
+$ ./reactics smt examples/smt/mutex_param.py -h
+
+ ------------------------------------------------
+ -- ReactICS -- Reaction Systems Model Checker --
+ ------------------------------------------------
+
+usage: mutex_param.py [-h] [-v] [-o] scaling {p,np-p,np-np}
+
+positional arguments:
+  scaling         scaling parameter value
+  {p,np-p,np-np}  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)
+
+optional arguments:
+  -h, --help      show this help message and exit
+  -v, --verbose   turn verbosity on
+  -o, --optimise  minimise the parametric computation result
+```
+
 

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

@@ -0,0 +1,126 @@
+#!/usr/bin/env python
+
+from sys import argv, exit
+
+OPTIONS_STR = """
+options { use-context-automaton; make-progressive; };
+"""
+
+PROC_STR = """
+    proc{:d} {{
+        {{{{out}}, {{}} -> {{approach}}}};
+        {{{{approach}}, {{req}} -> {{req}}}};
+        {{{{allowed}}, {{}} -> {{in}}}};
+        {{{{in}}, {{}} -> {{out,leave}}}};
+        {{{{req}}, {{in}} -> {{req}}}};
+    }};
+"""
+
+CA_STR = """
+context-automaton {{
+    states {{ init, green, red }};
+    init-state {{ init }};
+    transitions {{
+{:s}
+    }};
+}};
+"""
+
+PROPERTY_STR = """
+rsctlk-property {{ {:s} : {:s} }};
+"""
+
+
+#################################################################
+
+if len(argv) < 1:
+    print("Usage: {:s} <number of processes>".format(argv[0]))
+    exit(100)
+
+n = int(argv[1])
+
+assert n > 1, "number of proc must be > 1"
+
+out = ""
+
+out += OPTIONS_STR
+out += "reactions {\n"
+for i in range(n):
+    out += PROC_STR.format(i)
+out += "};\n"
+
+transitions = ""
+
+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
+        )
+    )
+
+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
+    )
+
+for i in range(n):
+    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
+    )
+
+out += CA_STR.format(transitions)
+
+## f1
+# 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)
+
+# 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)
+
+# 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)
+
+# f4
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+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)
+
+print(out)

examples/bdd/tgc.rs

@@ -0,0 +1,58 @@
+
+options { use-context-automaton; make-progressive; };
+reactions {
+
+    proc0 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+
+    proc1 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+
+    proc2 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+};
+
+context-automaton {
+    states { init, green, red };
+    init-state { init };
+    transitions {
+        { proc0={out} proc1={out} proc2={out} }: init -> green;
+        { proc0={allowed} }: green -> red : proc0.req;
+        { proc1={allowed} }: green -> red : proc1.req;
+        { proc2={allowed} }: green -> red : proc2.req;
+        { proc0={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc1={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc2={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc0={} }: red -> green : proc0.leave;
+        { proc1={} }: red -> green : proc1.leave;
+        { proc2={} }: red -> green : proc2.leave;
+        { proc0={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+        { proc1={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+        { proc2={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+
+    };
+};
+
+rsctlk-property { f1 : EF( E<proc0.allowed>X( proc0.in ) ) AND EF( E<proc1.allowed>X( proc1.in ) ) AND EF( E<proc2.allowed>X( proc2.in ) ) };
+
+rsctlk-property { f2 : EF( proc0.approach AND proc1.approach AND proc2.approach ) };
+
+rsctlk-property { f3 : AG( proc0.in IMPLIES K[proc0](~proc1.in AND ~proc2.in) ) };
+
+rsctlk-property { f4 : AG( proc0.in IMPLIES C[proc0,proc1,proc2](~proc1.in AND ~proc2.in) ) };
+

examples/smt/chain_reaction.py

@@ -0,0 +1,123 @@
+#!/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 *
+import sys
+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()
+        print("* N,M -- integers (scaling parameters)")
+        print("* type:")
+        print("  - 1 - RSC")
+        print("  - 0 - RSC translated into RS")
+        print()
+        exit(1)
+
+    chainLen = int(sys.argv[1])
+    maxConc = int(sys.argv[2])  # depth (max concentration)
+
+    verify_rsc = bool(int(sys.argv[3]))
+
+    if chainLen < 1 or maxConc < 1:
+        print("be reasonable")
+        exit(1)
+
+    r = ReactionSystemWithConcentrations()
+    r.add_bg_set_entity(("inc", 1))
+    r.add_bg_set_entity(("dec", 1))
+
+    for i in range(1, chainLen + 1):
+        r.add_bg_set_entity(("e_" + str(i), maxConc))
+
+    for i in range(1, chainLen + 1):
+        ent = "e_" + str(i)
+        r.add_reaction_inc(ent, "inc", [(ent, 1)], [(ent, maxConc)])
+        r.add_reaction_dec(ent, "dec", [(ent, 1)], [])
+        if i < chainLen:
+            r.add_reaction([(ent, maxConc)], [], [("e_" + str(i + 1), 1)])
+
+    r.add_reaction(
+        [("e_" + str(chainLen), maxConc)],
+        [("dec", 1)],
+        [("e_" + str(chainLen), maxConc)],
+    )
+
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("init")
+    c.add_state("working")
+    c.add_transition("init", [("e_1", 1), ("inc", 1)], "working")
+    c.add_transition("working", [("inc", 1)], "working")
+
+    rc = ReactionSystemWithAutomaton(r, c)
+
+    if print_system:
+        rc.show()
+
+    if verify_rsc:
+        smt_rsc = SmtCheckerRSC(rc)
+        prop = [("e_" + str(chainLen), maxConc)]
+        smt_rsc.check_reachability((prop, []), max_level=maxConc * chainLen + 10)
+
+    else:
+        orc = rc.get_ordinary_reaction_system_with_automaton()
+        if print_system:
+            print("\nTranslated:")
+            orc.show()
+        smt_tr_rs = SmtCheckerRS(orc)
+        smt_tr_rs.check_reachability(["e_" + str(chainLen) + "#" + str(maxConc)])
+
+    time = 0
+    mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+    if verify_rsc:
+        filename_t = "bench_rsc_time.log"
+        filename_m = "bench_rsc_mem.log"
+        time = smt_rsc.get_verification_time()
+    else:
+        filename_t = "bench_tr_rs_time.log"
+        filename_m = "bench_tr_rs_mem.log"
+        time = smt_tr_rs.get_verification_time()
+
+    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.write(log_str)
+    f.close()
+
+
+def main():
+    chain_reaction()
+
+
+if __name__ == "__main__":
+    main()
+
+# EOF

examples/smt/heat_shock_response.py

@@ -0,0 +1,133 @@
+#!/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 *
+import sys
+import resource
+
+
+def heat_shock_response(print_system=True, verify_rsc=True):
+    if len(sys.argv) < 1 + 1:
+        print("{source} <type>".format(source=sys.argv[0]))
+        print("type:")
+        print(" - 1 -- RSC")
+        print(" - 0 -- RSC translated into RS")
+        print()
+        exit(1)
+
+    verify_rsc = bool(int(sys.argv[1]))
+
+    stress_temp = 42
+    max_temp = 50
+
+    r = ReactionSystemWithConcentrations()
+    r.add_bg_set_entity(("hsp", 1))
+    r.add_bg_set_entity(("hsf", 1))
+    r.add_bg_set_entity(("hsf2", 1))
+    r.add_bg_set_entity(("hsf3", 1))
+    r.add_bg_set_entity(("hse", 1))
+    r.add_bg_set_entity(("mfp", 1))
+    r.add_bg_set_entity(("prot", 1))
+    r.add_bg_set_entity(("hsf3:hse", 1))
+    r.add_bg_set_entity(("hsp:mfp", 1))
+    r.add_bg_set_entity(("hsp:hsf", 1))
+    r.add_bg_set_entity(("temp", max_temp))
+    r.add_bg_set_entity(("heat", 1))
+    r.add_bg_set_entity(("cool", 1))
+
+    r.add_reaction([("hsf", 1)], [("hsp", 1)], [("hsf3", 1)])
+    r.add_reaction([("hsf", 1), ("hsp", 1), ("mfp", 1)], [], [("hsf3", 1)])
+    r.add_reaction([("hsf3", 1)], [("hse", 1), ("hsp", 1)], [("hsf", 1)])
+    r.add_reaction([("hsf3", 1), ("hsp", 1), ("mfp", 1)], [("hse", 1)], [("hsf", 1)])
+    r.add_reaction([("hsf3", 1), ("hse", 1)], [("hsp", 1)], [("hsf3:hse", 1)])
+    r.add_reaction(
+        [("hsp", 1), ("hsf3", 1), ("mfp", 1), ("hse", 1)], [], [("hsf3:hse", 1)]
+    )
+    r.add_reaction([("hse", 1)], [("hsf3", 1)], [("hse", 1)])
+    r.add_reaction([("hsp", 1), ("hsf3", 1), ("hse", 1)], [("mfp", 1)], [("hse", 1)])
+    r.add_reaction([("hsf3:hse", 1)], [("hsp", 1)], [("hsp", 1), ("hsf3:hse", 1)])
+    r.add_reaction(
+        [("hsp", 1), ("mfp", 1), ("hsf3:hse", 1)], [], [("hsp", 1), ("hsf3:hse", 1)]
+    )
+    r.add_reaction([("hsf", 1), ("hsp", 1)], [("mfp", 1)], [("hsp:hsf", 1)])
+    r.add_reaction(
+        [("hsp:hsf", 1), ("temp", stress_temp)], [], [("hsf", 1), ("hsp", 1)]
+    )
+    r.add_reaction([("hsp:hsf", 1)], [("temp", stress_temp)], [("hsp:hsf", 1)])
+    r.add_reaction(
+        [("hsp", 1), ("hsf3:hse", 1)], [("mfp", 1)], [("hse", 1), ("hsp:hsf", 1)]
+    )
+    r.add_reaction([("temp", stress_temp), ("prot", 1)], [], [("mfp", 1), ("prot", 1)])
+    r.add_reaction([("prot", 1)], [("temp", stress_temp)], [("prot", 1)])
+    r.add_reaction([("hsp", 1), ("mfp", 1)], [], [("hsp:mfp", 1)])
+    r.add_reaction([("mfp", 1)], [("hsp", 1)], [("mfp", 1)])
+    r.add_reaction([("hsp:mfp", 1)], [], [("hsp", 1), ("prot", 1)])
+
+    r.add_reaction_inc("temp", "heat", [("temp", 1)], [("temp", max_temp)])
+    r.add_reaction_dec("temp", "cool", [("temp", 1)], [])
+
+    r.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("1", [], "1")
+
+    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))
+
+    if verify_rsc:
+        smt_rsc = SmtCheckerRSC(rc)
+        smt_rsc.check_reachability(prop, max_level=40)
+    else:
+        orc = rc.get_ordinary_reaction_system_with_automaton()
+        if print_system:
+            print("\nTranslated:")
+            orc.show()
+        smt_tr_rs = SmtCheckerRS(orc)
+        smt_tr_rs.check_reachability(rs_prop)
+
+
+def state_translate_rsc2rs(p):
+    return [e[0] + "#" + str(e[1]) for e in p]
+
+
+def main():
+    heat_shock_response()
+
+
+if __name__ == "__main__":
+    main()
+
+# EOF

examples/smt/mutex_param.py

@@ -0,0 +1,452 @@
+#
+# Copyright (c) 2015-2019 Artur Meski
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+#
+
+from rs import *
+from smt import *
+from logics import *
+from rsltl_shortcuts import *
+
+from itertools import chain, combinations
+
+import sys
+import resource
+import argparse
+
+
+def powerset(iterable, N=None):
+    if N is None:
+        N = len(s)
+    s = list(iterable)
+    return chain.from_iterable(combinations(s, r) for r in range(N + 1))
+
+
+def mutex_param_bench(cmd_args):
+    """
+    Mutex Benchmark
+
+    Parametric
+    """
+
+    base_entities = ["out", "req", "in", "act"]
+    shared_entities = ["lock", "done", "s"]
+
+    if not cmd_args.scaling:
+        print("Missing scaling parameter")
+        return
+    n_proc = int(cmd_args.scaling)
+
+    r = ReactionSystemWithConcentrationsParam()
+
+    def E(a, b, c=1):
+        return (a + "_" + str(b), c)
+
+    for i in range(n_proc):
+        for ent in base_entities:
+            max_conc = 1
+            if ent == "in":
+                max_conc = 3
+            elif ent == "req":
+                max_conc = 2
+            r.add_bg_set_entity(E(ent, i, max_conc))
+
+    for ent in shared_entities:
+        max_conc = 1
+        r.add_bg_set_entity((ent, max_conc))
+
+    ###################################################
+
+    Inhib = [("s", 1)]
+
+    for i in range(n_proc):
+        r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
+        r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
+
+        for j in range(n_proc):
+            if i != j:
+                r.add_reaction(
+                    [E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
+                )
+
+        r.add_reaction([E("req", i)], [E("act", i)], [E("req", i, 2)])
+
+        enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
+        r.add_reaction(
+            [E("req", i, 2), E("act", i)], enter_inhib, [E("in", i, 3), ("lock", 1)]
+        )
+
+        r.add_reaction([E("in", i, 3), E("act", i)], Inhib, [E("in", i, 2)])
+        r.add_reaction([E("in", i, 2), E("act", i)], Inhib, [E("in", i, 1)])
+
+        r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
+        r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
+
+    r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
+
+    lda1 = r.get_param("lda1")
+    lda2 = r.get_param("lda2")
+    lda3 = r.get_param("lda3")
+
+    r.add_reaction(lda1, lda2, lda3)
+
+    ###################################################
+
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("0")
+    c.add_state("1")
+
+    init_ctx = []
+    for i in range(n_proc):
+        init_ctx.append(E("out", i))
+
+    # the experiments starts with adding x and y:
+    c.add_transition("0", init_ctx, "1")
+
+    all_act = powerset([E("act", i) for i in range(n_proc)], 2)
+
+    for actions in all_act:
+        actions = list(actions)
+
+        c.add_transition("1", actions, "1")
+
+    # for all the remaining steps we have empty context sequences
+    # c.add_transition("1", [], "1")
+    # c.add_transition("1", [("h", 1)], "1")
+
+    ###################################################
+
+    rc = ReactionSystemWithAutomaton(r, c)
+    rc.show()
+
+    f_attack = ltl_F(
+        True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
+    )
+
+    ent_of_Nth_proc = [
+        ent + "_" + str(n_proc - 1) for ent in base_entities
+    ] + shared_entities
+    disallow = ["in_" + str(n_proc - 1)]
+    for ent in r.background_set:
+        if ent not in ent_of_Nth_proc:
+            disallow.append(ent)
+
+    # disallow.append("act_" + str(n_proc-1))
+
+    # disallow = ["in_0", "in_" + str(n_proc)] #, "req_0", "req_1"]
+    lda1_disallow = [param_entity(lda1, ent) == 0 for ent in disallow]
+    lda2_disallow = [param_entity(lda2, ent) == 0 for ent in disallow]
+    lda3_disallow = [param_entity(lda3, ent) == 0 for ent in disallow]
+    lda_disallow = lda1_disallow + lda2_disallow + lda3_disallow
+
+    # for bent in base_entities:
+    #     print(param_entity(lda3, bent + "_0"))
+
+    param_constr = param_And(*lda_disallow)
+
+    smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
+    smt_rsc.check_rsltl(
+        formulae_list=[f_attack], param_constr=param_constr
+    )  # , max_level=4, cont_if_sat=True)
+
+    log_suffix = ""
+    if cmd_args.optimise:
+        log_suffix = "_OPT"
+
+    time = 0
+    mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+    filename_t = "bench_mutex_param" + log_suffix + "_time.dat"
+    filename_m = "bench_mutex_param" + log_suffix + "_mem.dat"
+    time = smt_rsc.get_verification_time()
+
+    with open(filename_t, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, time)
+        f.write(log_str)
+
+    with open(filename_m, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
+        f.write(log_str)
+
+
+def mutex_nonparam_bench(cmd_args):
+    """
+    Mutex Benchmark
+
+    Parametric
+    """
+
+    base_entities = ["out", "req", "in", "act"]
+    shared_entities = ["lock", "done", "s"]
+
+    if not cmd_args.scaling:
+        raise RuntimeError("Missing scaling parameter")
+    n_proc = int(cmd_args.scaling)
+
+    r = ReactionSystemWithConcentrationsParam()
+
+    def E(a, b):
+        return (a + "_" + str(b), 1)
+
+    for i in range(n_proc):
+        for ent in base_entities:
+            r.add_bg_set_entity(E(ent, i))
+
+    for ent in shared_entities:
+        r.add_bg_set_entity((ent, 1))
+
+    ###################################################
+
+    Inhib = [("s", 1)]
+
+    for i in range(n_proc):
+        r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
+        r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
+
+        for j in range(n_proc):
+            if i != j:
+                r.add_reaction(
+                    [E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
+                )
+
+        r.add_reaction([E("req", i)], [E("act", i)], [E("req", i)])
+
+        enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
+        r.add_reaction(
+            [E("req", i), E("act", i)], enter_inhib, [E("in", i), ("lock", 1)]
+        )
+
+        r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
+        r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
+
+    r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
+
+    r.add_reaction(
+        [E("out", n_proc - 1)], [("s", 1)], [("done", 1), E("req", n_proc - 1)]
+    )
+
+    ###################################################
+
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("0")
+    c.add_state("1")
+
+    init_ctx = []
+    for i in range(n_proc):
+        init_ctx.append(E("out", i))
+
+    # the experiments starts with adding x and y:
+    c.add_transition("0", init_ctx, "1")
+
+    all_act = powerset([E("act", i) for i in range(n_proc)], 2)
+
+    for actions in all_act:
+        actions = list(actions)
+
+        c.add_transition("1", actions, "1")
+
+    # for all the remaining steps we have empty context sequences
+    # c.add_transition("1", [], "1")
+    # c.add_transition("1", [("h", 1)], "1")
+
+    ###################################################
+
+    rc = ReactionSystemWithAutomaton(r, c)
+    rc.show()
+
+    f_attack = ltl_F(
+        True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
+    )
+
+    smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
+    smt_rsc.check_rsltl(formulae_list=[f_attack])
+
+    time = 0
+    mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+    filename_t = "bench_mutex_nonparam_time.dat"
+    filename_m = "bench_mutex_nonparam_mem.dat"
+    time = smt_rsc.get_verification_time()
+
+    with open(filename_t, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, time)
+        f.write(log_str)
+
+    with open(filename_m, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
+        f.write(log_str)
+
+
+def mutex_nonparam_bench_oldimpl(cmd_args):
+    """
+    Mutex Benchmark
+
+    Parametric
+    """
+
+    base_entities = ["out", "req", "in", "act"]
+    shared_entities = ["lock", "done", "s"]
+
+    if not cmd_args.scaling:
+        raise RuntimeError("Missing scaling parameter")
+    n_proc = int(cmd_args.scaling)
+
+    r = ReactionSystemWithConcentrations()
+
+    def E(a, b):
+        return (a + "_" + str(b), 1)
+
+    for i in range(n_proc):
+        for ent in base_entities:
+            r.add_bg_set_entity(E(ent, i))
+
+    for ent in shared_entities:
+        r.add_bg_set_entity((ent, 1))
+
+    ###################################################
+
+    Inhib = [("s", 1)]
+
+    for i in range(n_proc):
+        r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
+        r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
+
+        for j in range(n_proc):
+            if i != j:
+                r.add_reaction(
+                    [E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
+                )
+
+        r.add_reaction([E("req", i)], [E("act", i)], [E("req", i)])
+
+        enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
+        r.add_reaction(
+            [E("req", i), E("act", i)], enter_inhib, [E("in", i), ("lock", 1)]
+        )
+
+        r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
+        r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
+
+    r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
+
+    r.add_reaction(
+        [E("out", n_proc - 1)], [("s", 1)], [("done", 1), E("req", n_proc - 1)]
+    )
+
+    ###################################################
+
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("0")
+    c.add_state("1")
+
+    init_ctx = []
+    for i in range(n_proc):
+        init_ctx.append(E("out", i))
+
+    # the experiments starts with adding x and y:
+    c.add_transition("0", init_ctx, "1")
+
+    all_act = powerset([E("act", i) for i in range(n_proc)], 2)
+
+    for actions in all_act:
+        actions = list(actions)
+
+        c.add_transition("1", actions, "1")
+
+    # for all the remaining steps we have empty context sequences
+    # c.add_transition("1", [], "1")
+    # c.add_transition("1", [("h", 1)], "1")
+
+    ###################################################
+
+    rc = ReactionSystemWithAutomaton(r, c)
+    rc.show()
+
+    f_attack = ltl_F(
+        True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
+    )
+
+    smt_rsc = SmtCheckerRSC(rc)
+    smt_rsc.check_rsltl(formula=f_attack)
+
+    time = 0
+    mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+    filename_t = "bench_mutex_nonparam_oldimpl_time.dat"
+    filename_m = "bench_mutex_nonparam_oldimpl_mem.dat"
+    time = smt_rsc.get_verification_time()
+
+    with open(filename_t, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, time)
+        f.write(log_str)
+
+    with open(filename_m, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
+        f.write(log_str)
+
+
+def state_translate_rsc2rs(p):
+    return [e[0] + "#" + str(e[1]) for e in p]
+
+
+def mutex_bench_main(cmd_args):
+    mode = cmd_args.mode
+
+    if mode == "p":
+        mutex_param_bench(cmd_args)
+    elif mode == "np-p":
+        mutex_nonparam_bench(cmd_args)
+    elif mode == "np-np":
+        mutex_nonparam_bench_oldimpl(cmd_args)
+    else:
+        print("Unrecognised mode")
+        return
+
+
+def main():
+    parser = argparse.ArgumentParser()
+
+    parser.add_argument(
+        "scaling",
+        help="scaling parameter value",
+    )
+
+    parser.add_argument(
+        "mode",
+        choices=["p", "np-p", "np-np"],
+        help="Selects the mode: p - parameter synthesis (parametric implementation), np-p - non-parametric with parametric implementation (with the parameters substituted), np-np - non-parametric with non-parametric implementation (parameters substituted)",
+    )
+
+    parser.add_argument(
+        "-v", "--verbose", help="turn verbosity on", action="store_true"
+    )
+    parser.add_argument(
+        "-o",
+        "--optimise",
+        help="minimise the parametric computation result",
+        action="store_true",
+    )
+
+    args = parser.parse_args()
+
+    mutex_bench_main(args)
+
+
+if __name__ == "__main__":
+    main()
+
+# EOF

examples/smt/scalable_chain.py

@@ -0,0 +1,199 @@
+#!/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
+
+
+def generate_system(chainLen, maxConc):
+    """
+    This function generates the reaction system with concentrations
+    for the scalable chain benchmark
+
+    chainLen is the length of the chain
+    maxConc is the maximal concentration
+    """
+
+    r = ReactionSystemWithConcentrations()
+    r.add_bg_set_entity(("inc", 1))
+    r.add_bg_set_entity(("dec", 1))
+
+    for i in range(1, chainLen + 1):
+        r.add_bg_set_entity(("e_" + str(i), maxConc))
+
+    for i in range(1, chainLen + 1):
+        ent = "e_" + str(i)
+        r.add_reaction_inc(ent, "inc", [(ent, 1)], [(ent, maxConc)])
+        r.add_reaction_dec(ent, "dec", [(ent, 1)], [])
+        if i < chainLen:
+            r.add_reaction([(ent, maxConc)], [], [("e_" + str(i + 1), 1)])
+
+    r.add_reaction(
+        [("e_" + str(chainLen), maxConc)],
+        [("dec", 1)],
+        [("e_" + str(chainLen), maxConc)],
+    )
+
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("init")
+    c.add_state("working")
+    c.add_transition("init", [("e_1", 1), ("inc", 1)], "working")
+    c.add_transition("working", [("inc", 1)], "working")
+
+    rc = ReactionSystemWithAutomaton(r, c)
+
+    return rc
+
+
+def generate_formula(formula_number, chainLen, maxConc):
+    """
+    This function generates the rsLTL formula
+    corresponding to the formula_number parameter
+    """
+
+    if formula_number == 1:
+        ret = Formula_rsLTL.f_F(
+            BagDescription.f_entity("inc") > 0,
+            (BagDescription.f_entity("e_" + str(chainLen)) >= maxConc),
+        )
+
+    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),
+            )
+        ret = f_tmp
+
+    elif formula_number == 3:
+        ret = Formula_rsLTL.f_G(
+            BagDescription.f_TRUE(),
+            Formula_rsLTL.f_Implies(
+                (BagDescription.f_entity("e_1") == 1),
+                Formula_rsLTL.f_F(
+                    BagDescription.f_entity("inc") > 0,
+                    (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,
+        )
+
+    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,
+            ),
+        )
+
+    else:
+        ret = None
+
+    assert ret is not None, "Unknown formula"
+
+    return ret
+
+
+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()
+
+    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.write(log_str)
+    f.close()
+
+
+def scalable_chain(print_system=False):
+    """
+    This is the entry point for the benchmark
+    """
+    if len(sys.argv) < 1 + 3:
+        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])
+
+    if chainLen < 1 or maxConc < 1:
+        print("be reasonable")
+        exit(1)
+    if not formula_number in range(1, 5 + 1):
+        print("formulaNumber must be in 1..5")
+        exit(1)
+
+    # Generate the reaction systems with concentrations
+    rc = generate_system(chainLen, maxConc)
+
+    # Generate the formula
+    form = generate_formula(formula_number, chainLen, maxConc)
+
+    # Optional dump/print of the system
+    if print_system:
+        rc.show()
+
+    # Create an instance of the SMT checker for RS with concentrations
+    smt_rsc = SmtCheckerRSC(rc)
+
+    # Start the verification process
+    smt_rsc.check_rsltl(formula=form)
+
+    save_statistics(smt_rsc, formula_number, chainLen, maxConc)
+
+
+def main():
+    scalable_chain(print_system=True)
+
+
+if __name__ == "__main__":
+    main()

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

@@ -0,0 +1,86 @@
+#!/usr/bin/env bash
+
+# 
+# Copyright (c) 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.
+# 
+
+echo
+echo " ------------------------------------------------"
+echo " -- ReactICS -- Reaction Systems Model Checker --"
+echo " ------------------------------------------------"
+echo
+
+mode="$1"
+shift
+
+REACTICS_BDD="$(pwd)/reactics-bdd"
+REACTICS_SMT="$(pwd)/reactics-smt"
+
+if [[ "$mode" == "bdd" ]]
+then
+  
+  if [[ ! -x $REACTICS_BDD/reactics ]]
+  then
+    echo "Make sure to run setup first!"
+  fi
+  
+  reactics-bdd/reactics $*
+  
+elif [[ "$mode" == "smt" ]]
+then
+ 
+  export PYTHONPATH="$PYTHONPATH:$REACTICS_SMT"
+  if [[ "$*" != "" ]]
+  then
+    python3 $* 
+  else
+    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
+
+else
+  
+  echo "Usage: $0 <mode> <module-specific parameters>"
+  echo
+  echo "mode:"
+  echo "  - bdd    -- uses BDD-based module"
+  echo "  - smt    -- used SMT-based module"
+  echo "  - setup  -- builds what is required" 
+  echo
+  
+fi
+
+# EOF

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,11 +75,13 @@ void CtxAut::printAutomaton(void)
 
 void CtxAut::showStates(void)
 {
-  cout << "# Context Automaton States:" << endl;
+  if (states_ids.size() > 0) {
-  cout << " = Init state: " << getStateName(init_state_id) << endl;
+    cout << "# Context Automaton States:" << endl;
+    cout << " = Init state: " << getStateName(init_state_id) << endl;
 
-  for (const auto &s : states_ids) {
+    for (const auto &s : states_ids) {
-    cout << " * " << s << endl;
+      cout << " * " << s << endl;
+    }
   }
 }
 
@@ -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(
+    cout << " * [" << getStateName(t.src_state) << " -> "
-           t.dst_state)
+         << getStateName(t.dst_state) << "]: { "
-         << "]: { " << parent_rctsys->procEntitiesToStr(t.ctx) << "}";
+         << 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(
+      constrs[curr_st] =
-        STC_OR, constrs[curr_st], t.state_constr);
+        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/formrsctlk.cc

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2012, 2013
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #include "formrsctlk.hh"

reactics-bdd/formrsctlk.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2012-2015
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef RS_FORMRSCTLK_HH

reactics-bdd/in/scripts/gen_asm.py

@@ -3,7 +3,7 @@
 from sys import argv,exit
 
 OPTIONS_STR = """
-options { use-context-automaton; make-progressive; }
+options { use-context-automaton; make-progressive; };
 """
 
 PROC_STR = """
@@ -25,16 +25,16 @@ FINAL_PROC = """
 
 CA_STR = """
 context-automaton {{
-    states {{ init, act }}
+    states {{ init, act }};
-    init-state {{ init }}
+    init-state {{ init }};
     transitions {{
 {:s}
-    }}
+    }};
-}}
+}};
 """
 
 PROPERTY_STR = """
-rsctlk-property {{ {:s} : {:s} }}
+rsctlk-property {{ {:s} : {:s} }};
 """
 
 
@@ -56,7 +56,7 @@ for i in range(1, n+1):
     out += PROC_STR.format(i)
 
 out += FINAL_PROC
-out += "}\n"
+out += "};\n"
 
 transitions = ""
 

reactics-bdd/in/scripts/gen_drs_mutex.py

@@ -1,89 +0,0 @@
-#!/usr/bin/env python
-
-from sys import argv,exit
-
-OPTIONS_STR = """
-options { use-context-automaton; }
-"""
-CONTROLLER_STR = """
-    ct {
-        {{lock},{leave} -> {lock}};
-        {{req},{} -> {lock}};
-    };
-"""
-
-PROC_STR = """
-    proc{:d} {{
-        {{{{out}}, {{}} -> {{approach}}}};
-        {{{{approach}}, {{req}} -> {{req}}}};
-        {{{{req}}, {{lock}} -> {{in}}}};
-        {{{{in}}, {{}} -> {{out,leave}}}};
-        {{{{req}}, {{in}} -> {{req}}}};
-    }};
-"""
-
-CA_STR = """
-context-automaton {{
-    states {{ s0, s1 }}
-    init-state {{ s0 }}
-    transitions {{
-{:s}
-    }}
-}}
-"""
-
-PROPERTY_STR = """
-rsctlk-property {{ {:s} : {:s} }}
-"""
-
-
-#################################################################
-
-if len(argv) < 1:
-    print("Usage: {:s} <number of processes>".format(argv[0]))
-    exit(100)
-
-n = int(argv[1])
-
-assert n > 1, "number of proc must be > 1"
-
-out = ""
-
-out += OPTIONS_STR
-out += "reactions {\n"
-out += CONTROLLER_STR
-for i in range(n):
-    out += PROC_STR.format(i)
-out += "}\n"
-
-transitions = ""
-
-init_trans = 8*" " + "{ ct={} "
-for i in range(n):
-    init_trans += "proc{:d}={{out}} ".format(i)
-
-init_trans += "}: s0 -> s1;\n"
-
-transitions += init_trans
-
-for i in range(n):
-    transitions += "{:s}{{ ct={{}} proc{:d}={{}} }}: s1 -> s1;\n".format(8*" ", i)    
-
-out += CA_STR.format(transitions)
-
-# f1
-formula = "EF( proc0.in )"
-for i in range(1, n):
-    formula += " AND EF( proc{:d}.in )".format(i)
-out += PROPERTY_STR.format("f1",formula)
-
-# f2
-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("f2",formula)
-
-print(out)
-

reactics-bdd/in/tgc.rs

@@ -1,48 +0,0 @@
-
-options { use-context-automaton; }
-reactions {
-
-    proc0 {
-        {{out}, {} -> {approach}};
-        {{approach}, {req} -> {req}};
-        {{allowed}, {} -> {in}};
-        {{in}, {} -> {out,leave}};
-        {{req}, {in} -> {req}};
-    };
-
-    proc1 {
-        {{out}, {} -> {approach}};
-        {{approach}, {req} -> {req}};
-        {{allowed}, {} -> {in}};
-        {{in}, {} -> {out,leave}};
-        {{req}, {in} -> {req}};
-    };
-
-    proc2 {
-        {{out}, {} -> {approach}};
-        {{approach}, {req} -> {req}};
-        {{allowed}, {} -> {in}};
-        {{in}, {} -> {out,leave}};
-        {{req}, {in} -> {req}};
-    };
-}
-
-context-automaton {
-    states { init, green, red }
-    init-state { init }
-    transitions {
-        { proc0={out} proc1={out} proc2={out} }: init -> green;
-        { proc0={} proc1={} proc2={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
-        { proc0={allowed} }: green -> red : proc0.req;
-        { proc1={allowed} }: green -> red : proc1.req;
-        { proc2={allowed} }: green -> red : proc2.req;
-        { proc0={} }: red -> green : proc0.leave;
-        { proc1={} }: red -> green : proc1.leave;
-        { proc2={} }: red -> green : proc2.leave;
-        { proc0={} proc1={} proc2={} } : red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
-    }
-}
-
-rsctlk-property { f1 : EF( proc0.in ) AND EF( proc1.in ) AND EF( proc2.in ) }
-
-rsctlk-property { f2 : AG( proc0.in IMPLIES K[proc0](~proc1.in AND ~proc2.in) ) }

reactics-bdd/in/trivial.rs

@@ -0,0 +1,22 @@
+options { use-context-automaton; };
+
+reactions {
+    m {
+        {{e1,e4},{e2} -> {e1,e2}}; 
+        {{e2},{e4} -> {e1,e3,e4}}; 
+	{{e1,e3},{e2} -> {e1,e2}};
+	{{e3},{e2} -> {e1}};
+    };
+
+};
+
+context-automaton {
+	states { s0, s1 };
+    init-state { s0 };
+	transitions {
+		{ m={e1,e4} }: s0 -> s1;
+		{ m={} }: s1 -> s1;
+		{ m={e4} }: s1 -> s1;
+	};
+};
+

reactics-bdd/mc.cc

@@ -198,7 +198,14 @@ void ModelChecker::printReachWithSucc(void)
   while (!unproc.IsZero()) {
     BDD t;
     t = unproc.PickOneMinterm(*pv);
-    cout << "Successors of " << srs->decodedRctSysStateToStr(t) << ":" << endl;
+    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();
 
-  cout << "Formula " << form->toStr() << (result ? " holds" : " does not hold")
+  if (opts->backend_mode) {
-       << endl;
+      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();
 
-  cout << "Formula " << form->toStr() << " " << (result ? "holds" :
+  if (opts->backend_mode) {
-       "does not hold") << endl;
+      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/memtime.hh

@@ -1,18 +1,3 @@
-/**************************************************************************
- *                                                                        *
- *  This file is a part of BMC4LTLK,                                      *
- *  a program for Bounded Model Checking of LTLK.                         *
- *                                                                        *
- *  Copyright (C) 2002-2010 Andrzej Zbrzezny <a.zbrzezny@gmail.com>       *
- *                                                                        *
- *  This program is released under the terms of the license contained     *
- *  in the file LICENSE.                                                  *
- *                                                                        *
- **************************************************************************/
-
-/* WARNING: LICENSE VIOLATION. THIS PROGRAM IS USED FOR TEST PURPOSES ONLY
- *          THIS CODE WILL BE REPLACED BEFORE ANY RELEASE!!!!
- */
 
 /* Based on MiniSat 1.14 */
 

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

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2012-2014
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #include "reactics.hh"
@@ -34,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:
@@ -109,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;
@@ -262,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/rs.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2012-2014
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef RS_RS_HH

reactics-bdd/rsin_parser.yy

@@ -1,7 +1,7 @@
 %skeleton "lalr1.cc" /* -*- C++ -*- */
 %require "2.5"
 %defines
-%define parser_class_name {rsin_parser}
+%define api.parser.class {rsin_parser}
 
 %code requires {
 #include <string>
@@ -28,7 +28,7 @@ class rsin_driver;
 };
 
 %debug
-%error-verbose
+%define parse.error verbose
 
 // Symbols
 %union

reactics-bdd/stateconstr.cc

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #include "stateconstr.hh"

reactics-bdd/stateconstr.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef STATECONSTR_HH
@@ -11,6 +8,8 @@
 
 #include "types.hh"
 
+#include <cassert>
+
 /* For state constraints: */
 #define STC_PV   80
 #define STC_AND  81

reactics-bdd/symrs.cc

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

reactics-bdd/symrs.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2012-2014
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef RS_SYMRSSTATE_HH

reactics-bdd/types.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef RS_TYPES_HH

reactics-smt/colour.py

@@ -1,11 +1,11 @@
-C_HEADER = '\033[95m'
+C_HEADER = "\033[95m"
-C_BLUE = '\033[94m'
+C_BLUE = "\033[94m"
-C_GREEN = '\033[92m'
+C_GREEN = "\033[92m"
-C_SOMEOTHER = '\033[93m'
+C_SOMEOTHER = "\033[93m"
-C_RED = '\033[91m'
+C_RED = "\033[91m"
-C_ENDC = '\033[0m'
+C_ENDC = "\033[0m"
-C_BOLD = '\033[1m'
+C_BOLD = "\033[1m"
-C_UNDERLINE = '\033[4m'
+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,26 +5,26 @@ from smt import *
 from logics import *
 from rsltl_shortcuts import *
 
+
 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([("a", 1)], [("h", 1)], [("b", 2)])
-    prs.add_reaction(lda,[("h",1)],[("c",1)])
+    prs.add_reaction(lda, [("h", 1)], [("c", 1)])
-    
+
     ##
 
     ca = ContextAutomatonWithConcentrations(prs)
     ca.add_init_state("0")
     ca.add_state("1")
-    
+
     ca.add_transition("0", [("a", 3)], "1")
     ca.add_transition("1", [], "1")
     ca.add_transition("1", [("h", 1)], "1")
@@ -37,8 +37,9 @@ def ex():
 
     checker = SmtCheckerRSCParam(crprs, optimise=True)
     checker.check_rsltl(formulae_list=[f], param_constr=pc)
-    
+
+
 if __name__ == "__main__":
-	ex()
+    ex()
 
 # EOF

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(
+                if not (
-                        isinstance(operand, BagDescription)
+                    isinstance(operand, BagDescription) or isinstance(operand, int)
-                        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',
+    "ParamConstraint_oper", "param_entity true l_and l_or l_not lt le eq ge gt"
-    '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(
+                if not (
-                        isinstance(operand, ParamConstraint)
+                    isinstance(operand, ParamConstraint) or isinstance(operand, int)
-                        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,
+        return cls(ParamConstraint_oper.param_entity, param=param, entity=entity_name)
-                   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(
+        return ParamConstraint(ParamConstraint_oper.lt, L_oper=self, R_oper=other)
-            ParamConstraint_oper.lt, L_oper=self, R_oper=other)
 
     def __le__(self, other):
-        return ParamConstraint(
+        return ParamConstraint(ParamConstraint_oper.le, L_oper=self, R_oper=other)
-            ParamConstraint_oper.le, L_oper=self, R_oper=other)
 
     def __eq__(self, other):
-        return ParamConstraint(
+        return ParamConstraint(ParamConstraint_oper.eq, L_oper=self, R_oper=other)
-            ParamConstraint_oper.eq, L_oper=self, R_oper=other)
 
     def __ge__(self, other):
-        return ParamConstraint(
+        return ParamConstraint(ParamConstraint_oper.ge, L_oper=self, R_oper=other)
-            ParamConstraint_oper.ge, L_oper=self, R_oper=other)
 
     def __gt__(self, other):
-        return ParamConstraint(
+        return ParamConstraint(ParamConstraint_oper.gt, L_oper=self, R_oper=other)
-            ParamConstraint_oper.gt, L_oper=self, R_oper=other)
 
     def __and__(self, other):
-        return ParamConstraint(
+        return ParamConstraint(ParamConstraint_oper.l_and, L_oper=self, R_oper=other)
-            ParamConstraint_oper.l_and, L_oper=self, R_oper=other)
 
     def __or__(self, other):
-        return ParamConstraint(
+        return ParamConstraint(ParamConstraint_oper.l_or, L_oper=self, R_oper=other)
-            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),
+            return And(
-                       self.encode(param_constr.right_operand))
+                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),
+            return Or(
-                      self.encode(param_constr.right_operand))
+                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(
+            return self.encode(param_constr.left_operand) < int(
-                param_constr.left_operand) < int(
+                param_constr.right_operand
-                param_constr.right_operand)
+            )
 
         if param_constr.f_type == ParamConstraint_oper.le:
-            return self.encode(
+            return self.encode(param_constr.left_operand) <= int(
-                param_constr.left_operand) <= int(
+                param_constr.right_operand
-                param_constr.right_operand)
+            )
 
         if param_constr.f_type == ParamConstraint_oper.eq:
-            return self.encode(
+            return self.encode(param_constr.left_operand) == int(
-                param_constr.left_operand) == int(
+                param_constr.right_operand
-                param_constr.right_operand)
+            )
 
         if param_constr.f_type == ParamConstraint_oper.ge:
-            return self.encode(
+            return self.encode(param_constr.left_operand) >= int(
-                param_constr.left_operand) >= int(
+                param_constr.right_operand
-                param_constr.right_operand)
+            )
 
         if param_constr.f_type == ParamConstraint_oper.gt:
-            return self.encode(
+            return self.encode(param_constr.left_operand) > int(
-                param_constr.left_operand) > int(
+                param_constr.right_operand
-                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',
+    "rsLTL_form_type",
-    'bag l_and l_or l_not l_implies t_globally t_finally t_next t_until t_release')
+    "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(
+            return (
-                self.left_operand) + " U[" + repr(
+                "("
-                self.sub_operand) + "] " + repr(
+                + repr(self.left_operand)
-                self.right_operand) + ")"
+                + " U["
+                + repr(self.sub_operand)
+                + "] "
+                + repr(self.right_operand)
+                + ")"
+            )
         if self.f_type == rsLTL_form_type.t_release:
-            return "(" + repr(
+            return (
-                self.left_operand) + " R[" + repr(
+                "("
-                self.sub_operand) + "] " + repr(
+                + repr(self.left_operand)
-                self.right_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(
+        return cls(rsLTL_form_type.t_until, L_oper=arg_L, R_oper=arg_R, sub_oper=sub)
-            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(
+        return cls(rsLTL_form_type.t_release, L_oper=arg_L, R_oper=arg_R, sub_oper=sub)
-            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 = [{} for level in range(0, bound + 1)]
-        self.enc_fcache_approx = [{} 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(
+            return Not(self.encode_bag(bag_formula.left_operand, level, context))
-                bag_formula.left_operand, level, context))
 
         if bag_formula.f_type == BagDesc_oper.lt:
-            return self.encode_bag(
+            return self.encode_bag(bag_formula.left_operand, level, context) < int(
-                bag_formula.left_operand, level, context) < int(
+                bag_formula.right_operand
-                bag_formula.right_operand)
+            )
 
         if bag_formula.f_type == BagDesc_oper.le:
-            return self.encode_bag(
+            return self.encode_bag(bag_formula.left_operand, level, context) <= int(
-                bag_formula.left_operand, level, context) <= int(
+                bag_formula.right_operand
-                bag_formula.right_operand)
+            )
 
         if bag_formula.f_type == BagDesc_oper.eq:
-            return self.encode_bag(
+            return self.encode_bag(bag_formula.left_operand, level, context) == int(
-                bag_formula.left_operand, level, context) == int(
+                bag_formula.right_operand
-                bag_formula.right_operand)
+            )
 
         if bag_formula.f_type == BagDesc_oper.ge:
-            return self.encode_bag(
+            return self.encode_bag(bag_formula.left_operand, level, context) >= int(
-                bag_formula.left_operand, level, context) >= int(
+                bag_formula.right_operand
-                bag_formula.right_operand)
+            )
 
         if bag_formula.f_type == BagDesc_oper.gt:
-            return self.encode_bag(
+            return self.encode_bag(bag_formula.left_operand, level, context) > int(
-                bag_formula.left_operand, level, context) > int(
+                bag_formula.right_operand
-                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(
+            raise NotImplementedError("Unsupported formula type: " + str(type(formula)))
-                "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):
+                for loop_level in range(1, bound + 1):
-                    enc = simplify(Or(enc, And(self.loop_position == loop_level, self.encode(
+                    enc = simplify(
-                        formula.left_operand, loop_level, bound))))
+                        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):
+                for loop_level in range(1, bound + 1):
-                    enc_loops = simplify(Or(enc_loops,
+                    enc_loops = simplify(
-                                            And(
+                        Or(
-                                                self.loop_position == loop_level,
+                            enc_loops,
-                                                self.encode_approx(formula, loop_level, bound),
+                            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):
+                for loop_level in range(1, bound + 1):
-                    enc_loops = simplify(Or(enc_loops,
+                    enc_loops = simplify(
-                                            And(
+                        Or(
-                                                self.loop_position == loop_level,
+                            enc_loops,
-                                                self.encode_approx(formula, loop_level, bound),
+                            And(
-                                            )
+                                self.loop_position == loop_level,
-                                            ))
+                                self.encode_approx(formula, loop_level, bound),
+                            ),
+                        )
+                    )
                     # print(enc)
-                enc = Or(self.encode(formula.left_operand, bound, bound),
+                enc = Or(
-                         And(
+                    self.encode(formula.left_operand, bound, bound),
-                    enc_loops,
+                    And(enc_loops, self.encode_bag_ctx(formula.sub_operand, level)),
-                    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):
+                for loop_level in range(1, bound + 1):
-                    inner_enc = simplify(Or(inner_enc,
+                    inner_enc = simplify(
-                                            And(
+                        Or(
-                                                self.loop_position == loop_level,
+                            inner_enc,
-                                                self.encode_approx(formula, loop_level, bound)
+                            And(
-                                            )
+                                self.loop_position == loop_level,
-                                            ))
+                                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):
+                for loop_level in range(1, bound + 1):
-                    inner_enc = simplify(Or(inner_enc,
+                    inner_enc = simplify(
-                                            And(
+                        Or(
-                                                self.loop_position == loop_level,
+                            inner_enc,
-                                                self.encode_approx(formula, loop_level, bound)
+                            And(
-                                            )
+                                self.loop_position == loop_level,
-                                            ))
+                                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(
+                    And(inner_enc, self.encode_bag_ctx(formula.sub_operand, level)),
-                        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(
+            raise NotImplementedError("Unsupported operator in approximation encoding")
-                "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(
+            raise RuntimeError('"' + src + '" is an unknown (undefined) state')
-                "\"" + src + "\" is an unknown (undefined) state")
 
         if not self.is_state(dst):
-            raise RuntimeError(
+            raise RuntimeError('"' + dst + '" is an unknown (undefined) state')
-                "\"" + 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),
+            (self.get_state_id(src), new_context_set, self.get_state_id(dst))
-             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,
+        super(ContextAutomatonWithConcentrations, self).__init__(reaction_system)
-              self).__init__(reaction_system)
 
     def is_valid_context(self, context):
-        if set(
+        if set([e for e, lvl in context]).issubset(
-                [e for e, lvl in context]).issubset(
+            self._reaction_system.background_set
-                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(
+            raise RuntimeError('"' + src + '" is an unknown (undefined) state')
-                "\"" + src + "\" is an unknown (undefined) state")
 
         if not self.is_state(dst):
-            raise RuntimeError(
+            raise RuntimeError('"' + dst + '" is an unknown (undefined) state')
-                "\"" + dst + "\" is an unknown (undefined) state")
 
         new_context_set = set()
         for ent, lvl in set(context_set):
-            new_context_set.add(
+            new_context_set.add((self._reaction_system.get_entity_id(ent), lvl))
-                (self._reaction_system.get_entity_id(ent), lvl))
 
         self._transitions.append(
-            (self.get_state_id(src),
+            (self.get_state_id(src), new_context_set, self.get_state_id(dst))
-             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):
+                for i in range(1, conc + 1):
-                    n = self._reaction_system.get_entity_name(
+                    n = self._reaction_system.get_entity_name(ent) + "#" + str(i)
-                        ent) + "#" + str(i)
                     ca._reaction_system.ensure_bg_set_entity(n)
                     new_ctx.add(n)
 
-            ca.add_transition(
+            ca.add_transition(ca.get_state_name(src), new_ctx, ca.get_state_name(dst))
-                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(
+            raise RuntimeError('"' + src + '" is an unknown (undefined) state')
-                "\"" + src + "\" is an unknown (undefined) state")
 
         if not self.is_state(dst):
-            raise RuntimeError(
+            raise RuntimeError('"' + dst + '" is an unknown (undefined) state')
-                "\"" + 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(
+            str_transition += (
-                reaction[1]) + "," + self.rsset2str(reaction[2]) + " )"
+                "( "
+                + 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: " +
+            print_error("Undefined context automaton action: " + repr(action_name))
-                        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 \"" +
+                    'Mismatching reaction system used in "'
-                    str(automaton.name) + "\"!!!")
+                    + str(automaton.name)
+                    + '"!!!'
+                )
                 exit(1)
 
     def show_prod_entities(self):
-        print(
+        print(C_MARK_INFO + " Possible context-products for the network of automata:")
-            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(
+            raise RuntimeError("The entity " + name + " is already on the list")
-                "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 (" +
+            print(
-                  str(len(self.reactions)) + ")")
+                " -> 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(
-                                                                " { " + self.state_to_str(reaction[1]) + " }",
+                    " "
-                                                                " { " + self.state_to_str(reaction[2]) + " }"))
+                    + "- {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]) + " }",
+                    )
+                )
 
     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(
+                    reactions_by_prod[prod_entity].append([reaction[0], reaction[1]])
-                        [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
@@ -15,7 +16,7 @@ class ReactionSystemWithAutomaton(object):
 
     def is_concentr_and_param_compatible(self):
         """
-        Checks if the underlying RS/CA are compatible 
+        Checks if the underlying RS/CA are compatible
         with parameters and concentrations
         """
         if not isinstance(self.rs, ReactionSystemWithConcentrationsParam):
@@ -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(
+            raise RuntimeError("Bad entity type when adding background set element")
-                "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(
+            raise RuntimeError("Unexpected concentration level in state: " + str(elem))
-                "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(
+            raise RuntimeError("Permanency for {0} already defined.".format(ent))
-                "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(
+                    print(
-                        command) + " ) ] -- ( R={" + self.state_to_str(reactants) + "}, I={" + self.state_to_str(inhibitors) + "} )")
+                        " - [ 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(
+                    raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
-                        "Unknown meta-reaction type: " + repr(r_type))
 
     def show_max_concentrations(self):
         print(
-            C_MARK_INFO +
+            C_MARK_INFO
-            " Maximal allowed concentration levels (for optimized translation to RS):")
+            + " 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) + ": ",
+            print(
-                                            "I={" + self.state_to_str(inhibitors) + "}"))
+                " - {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(
+            producible_entities = producible_entities.union(set(product_entities))
-                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
+                            succ_value = i + l
-                            for j in range(1, succ_value+1):
+                            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
+                            succ_value = i - l
-                            for j in range(1, succ_value+1):
+                            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(
+            raise RuntimeError("Bad entity type when adding background set element")
-                "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:
@@ -98,14 +93,33 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
         return False
 
+    def is_valid_concentration_for_entity(self, entity, level):
+        """Checks the concentration level for entity"""
+        e = self.get_entity_id(entity)
+        try:
+            max_conc = self.max_conc_per_ent[e]
+        except KeyError as _:
+            return True
+
+        if level > max_conc:
+            return False
+
+        return True
+
+    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)
+            )
+            exit(1)
+
     def get_state_ids(self, state):
         """Returns entities of the given state without levels"""
         return [self.get_entity_id(e) for e in state]
 
     def has_non_zero_concentration(self, elem):
         if elem[1] < 1:
-            raise RuntimeError(
+            raise RuntimeError("Unexpected concentration level in state: " + str(elem))
-                "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"""
@@ -124,6 +138,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
                 self.is_valid_entity_with_concentration(r)
                 self.has_non_zero_concentration(r)
                 entity, level = r
+                self.terminate_on_invalid_concentration(entity, level)
                 reactants.append((self.get_entity_id(entity), level))
                 if self.max_concentration < level:
                     self.max_concentration = level
@@ -139,6 +154,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
                 self.is_valid_entity_with_concentration(i)
                 self.has_non_zero_concentration(i)
                 entity, level = i
+                self.terminate_on_invalid_concentration(entity, level)
                 inhibitors.append((self.get_entity_id(entity), level))
                 if self.max_concentration < level:
                     self.max_concentration = level
@@ -154,6 +170,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
                 self.is_valid_entity_with_concentration(p)
                 self.has_non_zero_concentration(p)
                 entity, level = p
+                self.terminate_on_invalid_concentration(entity, level)
                 products.append((self.get_entity_id(entity), level))
 
         return reactants, inhibitors, products
@@ -186,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"""
@@ -208,8 +229,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
         ent_id = self.get_entity_id(ent)
 
         if ent_id in self.permanent_entities:
-            raise RuntimeError(
+            raise RuntimeError("Permanency for {0} already defined.".format(ent))
-                "Permanency for {0} already defined.".format(ent))
 
         inhibitors = self.process_rip([], I, [], ignore_empty_R=True)[1]
         self.permanent_entities[ent_id] = inhibitors
@@ -248,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(
+                    print(
-                        command) + " ) ] -- ( R={" + self.state_to_str(reactants) + "}, I={" + self.state_to_str(inhibitors) + "} )")
+                        " - [ 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(
+                    raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
-                        "Unknown meta-reaction type: " + repr(r_type))
 
     def show_max_concentrations(self):
         print(C_MARK_INFO + " Maximal allowed concentration levels:")
@@ -269,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) + ": ",
+            print(
-                                            "I={" + self.state_to_str(inhibitors) + "}"))
+                " - {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()
@@ -282,7 +320,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
     def get_producible_entities(self):
         """
-        Returns the set of entities that appear as products of 
+        Returns the set of entities that appear as products of
         reactions.
         """
 
@@ -290,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(
+            producible_entities = producible_entities.union(set(product_entities))
-                set(product_entities))
 
         return producible_entities
 
@@ -303,7 +340,6 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
         rs = ReactionSystem()
 
         for reactants, inhibitors, products in self.reactions:
-
             new_reactants = []
             new_inhibitors = []
             new_products = []
@@ -328,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 = []
@@ -350,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
 
@@ -378,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):
@@ -396,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 = []
@@ -436,4 +472,5 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
         return rs
 
+
 # EOF

reactics-smt/rs_examples.py

@@ -1,190 +0,0 @@
-#!/usr/bin/env python
-
-from rs import *
-from smt import *
-import sys
-import resource
-
-def chain_reaction(print_system=False):
-    
-    if len(sys.argv) < 1+3:
-        print("provide N M B")
-        print(" B=1 - RSC")
-        print(" B=0 - Translated RSC into RS")
-        exit(1)
-
-    chainLen=int(sys.argv[1]) # chain length
-    maxConc=int(sys.argv[2]) # depth (max concentration)
-    verify_rsc=bool(int(sys.argv[3]))
-        
-    if chainLen < 1 or maxConc < 1:
-        print("be reasonable")
-        exit(1)
-    
-    r = ReactionSystemWithConcentrations()
-    r.add_bg_set_entity(("inc",1))
-    # r.add_bg_set_entity(("reset",1))
-    r.add_bg_set_entity(("dec",1))
-    # r.add_bg_set_entity(("x",1))
-    
-    for i in range(1,chainLen+1):
-        r.add_bg_set_entity(("e_" + str(i),maxConc))
-    
-    for i in range(1,chainLen+1):
-        ent = "e_" + str(i)
-        # r.add_reaction_inc(ent, "inc", [(ent, 1)],[("reset",1),(ent,maxConc)])
-        r.add_reaction_inc(ent, "inc", [(ent, 1)],[(ent,maxConc)])
-        r.add_reaction_dec(ent, "dec", [(ent, 1)],[])
-        # r.add_reaction([(ent,1),("reset",1)],[],[(ent,1)])
-        if i < chainLen:
-            r.add_reaction([(ent,maxConc)],[],[("e_"+str(i+1),1)])
-
-    r.add_reaction([("e_" + str(chainLen),maxConc)],[("dec",1)],[("e_" + str(chainLen),maxConc)])
-    # r.add_reaction([("e_" + str(chainLen),maxConc)],[],[("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("working", [("reset",1)], "working")
-    # c.add_transition("working",[("x",1)],"working")
-
-    rc = ReactionSystemWithAutomaton(r,c)
-    
-    if print_system:
-        rc.show()
-    
-    if verify_rsc:
-        smt_rsc = SmtCheckerRSC(rc)
-        prop = [('e_'+str(chainLen),maxConc)]
-        smt_rsc.check_reachability((prop,[]),max_level=maxConc*chainLen+10)
-        # smt_rsc.show_encoding(prop,print_time=True,max_level=maxConc*chainLen+10)
-
-    else:
-        orc = rc.get_ordinary_reaction_system_with_automaton()
-        if print_system:
-            print("\nTranslated:")
-            orc.show()
-        smt_tr_rs = SmtCheckerRS(orc)
-        smt_tr_rs.check_reachability(['e_'+str(chainLen)+"#"+str(maxConc)])
-    
-    # print("Reaction System with Concentrations:", smt_rsc.get_verification_time())
-    # print("Reaction System from translating RSC:", smt_tr_rs.get_verification_time())
-    
-    time=0
-    mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)
-    if verify_rsc:
-        filename_t="bench_rsc_time.log"
-        filename_m="bench_rsc_mem.log"
-        time=smt_rsc.get_verification_time()
-    else:
-        filename_t="bench_tr_rs_time.log"
-        filename_m="bench_tr_rs_mem.log"
-        time=smt_tr_rs.get_verification_time()
-
-    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.write(log_str)
-    f.close()
-
-
-def heat_shock_response(print_system=True,verify_rsc=True):
-
-    if len(sys.argv) < 1+1:
-        print("provide B")
-        print(" B=1 - RSC")
-        print(" B=0 - Translated RSC into RS")
-        exit(1)
-
-    verify_rsc=bool(int(sys.argv[1]))
-
-    stress_temp = 42
-    max_temp = 50
-    
-    r = ReactionSystemWithConcentrations()    
-    r.add_bg_set_entity(("hsp",1))
-    r.add_bg_set_entity(("hsf",1))
-    r.add_bg_set_entity(("hsf2",1))
-    r.add_bg_set_entity(("hsf3",1))
-    r.add_bg_set_entity(("hse",1))
-    r.add_bg_set_entity(("mfp",1))
-    r.add_bg_set_entity(("prot",1))
-    r.add_bg_set_entity(("hsf3:hse",1))
-    r.add_bg_set_entity(("hsp:mfp",1))
-    r.add_bg_set_entity(("hsp:hsf",1))
-    r.add_bg_set_entity(("temp",max_temp))
-    r.add_bg_set_entity(("heat",1))
-    r.add_bg_set_entity(("cool",1))
-    
-    r.add_reaction([("hsf",1)],                         [("hsp",1)],        [("hsf3",1)])
-    r.add_reaction([("hsf",1),("hsp",1),("mfp",1)],     [],                 [("hsf3",1)])
-    r.add_reaction([("hsf3",1)],                        [("hse",1),("hsp",1)],[("hsf",1)])
-    r.add_reaction([("hsf3",1),("hsp",1),("mfp",1)],    [("hse",1)],        [("hsf",1)])
-    r.add_reaction([("hsf3",1),("hse",1)],              [("hsp",1)],        [("hsf3:hse",1)])
-    r.add_reaction([("hsp",1),("hsf3",1),("mfp",1),("hse",1)],[],           [("hsf3:hse",1)])
-    r.add_reaction([("hse",1)],                         [("hsf3",1)],       [("hse",1)])
-    r.add_reaction([("hsp",1),("hsf3",1),("hse",1)],    [("mfp",1)],        [("hse",1)])
-    r.add_reaction([("hsf3:hse",1)],                    [("hsp",1)],        [("hsp",1),("hsf3:hse",1)])
-    r.add_reaction([("hsp",1),("mfp",1),("hsf3:hse",1)],[],                 [("hsp",1),("hsf3:hse",1)])
-    r.add_reaction([("hsf",1),("hsp",1)],               [("mfp",1)],        [("hsp:hsf",1)])
-    r.add_reaction([("hsp:hsf",1),("temp",stress_temp)],[],                 [("hsf",1),("hsp",1)])
-    r.add_reaction([("hsp:hsf",1)],                     [("temp",stress_temp)],[("hsp:hsf",1)])
-    r.add_reaction([("hsp",1),("hsf3:hse",1)],          [("mfp",1)],        [("hse",1),("hsp:hsf",1)])
-    r.add_reaction([("temp",stress_temp),("prot",1)],   [],                     [("mfp",1),("prot",1)])
-    r.add_reaction([("prot",1)],                        [("temp",stress_temp)], [("prot",1)])
-    r.add_reaction([("hsp",1),("mfp",1)],               [],                 [("hsp:mfp",1)])
-    r.add_reaction([("mfp",1)],                         [("hsp",1)],        [("mfp",1)])
-    r.add_reaction([("hsp:mfp",1)],                     [],                 [("hsp",1),("prot",1)])
-
-    r.add_reaction_inc("temp", "heat", [("temp",1)],[("temp",max_temp)])
-    r.add_reaction_dec("temp", "cool", [("temp",1)],[])
-
-    r.add_permanency("temp",[("heat",1),("cool",1)])
-    #r.add_permanency("temp",[])
-
-    c = ContextAutomatonWithConcentrations(r)
-    c.add_init_state("0")
-    c.add_state("1")
-    # c.add_transition("0", [("prot",1), ("temp",35)], "1")
-    c.add_transition("0", [("hsf",1),("prot",1),("hse",1),("temp",35)], "1")
-    #-> c.add_transition("0", [("hse",1),("prot",1),("hsp:hsf",1),("temp",stress_temp)], "1")
-    # c.add_transition("0", [("hsp",1),("prot",1),("hsf3:hse",1),("mfp",1),("hsp:mfp",1),("temp",30)], "1")
-    c.add_transition("1", [("cool",1)], "1")
-    c.add_transition("1", [("heat",1)], "1")
-    c.add_transition("1", [], "1")
-    # c.add_transition("1", [("sugar",1)], "1")
-
-    rc = ReactionSystemWithAutomaton(r,c)
-    
-    if print_system:
-        rc.show()
-    
-    # prop_req = [("hsp:hsf",1),("hse",1),("prot",1)]
-    # prop_block = [("temp",stress_temp)]
-    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)
-    else:
-        orc = rc.get_ordinary_reaction_system_with_automaton()
-        if print_system:
-            print("\nTranslated:")
-            orc.show()
-        smt_tr_rs = SmtCheckerRS(orc)
-        smt_tr_rs.check_reachability(rs_prop)
-
-def state_translate_rsc2rs(p):
-    return [e[0] + "#" + str(e[1]) for e in p]
-        
-# EOF

reactics-smt/rs_testing.py

@@ -26,357 +26,11 @@ def run_tests(cmd_args):
     # heat_shock_response_param(cmd_args)
     # simple_param(cmd_args)
 
-    # gene_expression(cmd_args)
+    # param_gene_expression(cmd_args)
 
-    mutex_bench_main(cmd_args)
+def param_gene_expression(cmd_args):
-
-def mutex_bench_main(cmd_args):
-
-    if not cmd_args.special_mode:
-        print("Missing special mode parameter")
-        print("*    1 - parametric")
-        print("*    2 - non-parametric (with parametric implementation)")
-        print("*    3 - non-parametric (with non-parametric implementation)")
-        return
-    
-    smode = int(cmd_args.special_mode)
-
-    if smode == 1:
-        mutex_param_bench(cmd_args)
-    elif smode == 2:
-        mutex_nonparam_bench(cmd_args)
-    elif smode == 3:
-        mutex_nonparam_bench_oldimpl(cmd_args)
-    else:
-        print("Unrecognised mode")
-        return
-
-def mutex_param_bench(cmd_args):
     """
-    Mutex Benchmark
+    Simple gene expression example with parameters
-    
-    Parametric
-    """
-
-    base_entities = ["out","req","in","act"]
-    shared_entities = ["lock","done","s"]
-    
-    if not cmd_args.scaling_parameter:
-        print("Missing scaling parameter")
-        return
-    n_proc = int(cmd_args.scaling_parameter)
-    
-    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)])
-    
-    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 = ["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_parameter:
-        raise RuntimeError("Missing scaling parameter")
-    n_proc = int(cmd_args.scaling_parameter)
-    
-    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_parameter:
-        raise RuntimeError("Missing scaling parameter")
-    n_proc = int(cmd_args.scaling_parameter)
-    
-    r = ReactionSystemWithConcentrations()
-    
-    def E(a,b):
-        return (a + "_" + str(b), 1)
-
-    for i in range(n_proc):
-        for ent in base_entities:
-            r.add_bg_set_entity(E(ent,i))
-
-    for ent in shared_entities:
-        r.add_bg_set_entity((ent, 1))
-    
-    ###################################################
-    
-    Inhib = [("s",1)]
-    
-    for i in range(n_proc):
-        
-        r.add_reaction([E("out",i),E("act",i)],Inhib,[E("req",i)])
-        r.add_reaction([E("out",i)],[E("act",i)],[E("out",i)])
-        
-        for j in range(n_proc):
-            if i != j:
-                r.add_reaction([E("req",i),E("act",i),E("act",j)],Inhib,[E("req",i)])
-        
-        r.add_reaction([E("req",i)],[E("act",i)],[E("req",i)])
-        
-        enter_inhib = [E("act",j) for j in range(n_proc) if i != j] + [("lock",1)]
-        r.add_reaction([E("req",i),E("act",i)],enter_inhib,[E("in",i), ("lock",1)])
-        
-        r.add_reaction([E("in",i),E("act",i)],Inhib,[E("out",i), ("done",1)])
-        r.add_reaction([E("in",i)],[E("act",i)],[E("in",i)])
-    
-    r.add_reaction([("lock",1)],[("done",1)],[("lock",1)])
-    
-    r.add_reaction([E("out",n_proc-1)],[("s",1)],[("done",1),E("req",n_proc-1)])
-    
-    ###################################################
-    
-    c = ContextAutomatonWithConcentrations(r)
-    c.add_init_state("0")
-    c.add_state("1")
-    
-    init_ctx = []
-    for i in range(n_proc):
-        init_ctx.append(E("out", i))
-    
-    # the experiments starts with adding x and y:
-    c.add_transition("0", init_ctx, "1")
-    
-    all_act = powerset([E("act",i) for i in range(n_proc)], 2)
-    
-    for actions in all_act:
-        actions = list(actions)
-
-        c.add_transition("1", actions, "1")
-    
-    # for all the remaining steps we have empty context sequences
-    # c.add_transition("1", [], "1")
-    # c.add_transition("1", [("h", 1)], "1")
-    
-    ###################################################
-    
-    rc = ReactionSystemWithAutomaton(r, c)
-    rc.show()
-    
-    f_attack = ltl_F(True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc-1)) == 1))
-    
-    smt_rsc = SmtCheckerRSC(rc)
-    smt_rsc.check_rsltl(formula=f_attack)
-
-    time=0
-    mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)
-    filename_t="bench_mutex_nonparam_oldimpl_time.dat"
-    filename_m="bench_mutex_nonparam_oldimpl_mem.dat"
-    time=smt_rsc.get_verification_time()
-
-    with open(filename_t, 'a') as f:
-        log_str="{:d} {:f}\n".format(n_proc, time)
-        f.write(log_str)
-    
-    with open(filename_m, 'a') as f:
-        log_str="{:d} {:f}\n".format(n_proc, mem_usage)
-        f.write(log_str)
-
-def gene_expression(cmd_args):
-    """
-    Simple gene expression example
     """
     r = ReactionSystemWithConcentrationsParam()
 
@@ -391,8 +45,14 @@ def gene_expression(cmd_args):
 
     all_entities = set(r.background_set)
 
+    lda0 = r.get_param("lda0")
+    lda1 = r.get_param("lda1")
+    lda2 = r.get_param("lda2")
+    lda3 = r.get_param("lda3")
+
     r.add_reaction([("x",1)],[("h",1)],[("x",1)])
-    r.add_reaction([("x",1)],[("h",1)],[("xp",1)])
+    # r.add_reaction([("x",1)],[("h",1)],[("xp",1)])
+    r.add_reaction(lda0, [("h",1)],[("xp",1)])
     r.add_reaction([("x",1),("xp",1)],[("h",1)],[("X",1)])
 
     r.add_reaction([("X",1),("Y",1)],[("h",1)],[("Q",1)])
@@ -401,9 +61,6 @@ def gene_expression(cmd_args):
     # r.add_reaction([("y",1)],[("h",1)],[("y",1)])
     # r.add_reaction([("y",1)],[("Q",1)],[("yp",1)])
     # r.add_reaction([("y",1),("yp",1)],[("h",1)],[("Y",1)])
-    lda1 = r.get_param("lda1")
-    lda2 = r.get_param("lda2")
-    lda3 = r.get_param("lda3")
 
     r.add_reaction([("y",1)],[("h",1)],lda1)
     r.add_reaction(lda2,[("h",1)],[("yp",1)])
@@ -454,6 +111,12 @@ def gene_expression(cmd_args):
 
     obs_1 = ltl_And(phi_r, phi_c1, phi_c2, delayed_Q)
     
+    # Observation related to A_x:
+    obs_2 = ltl_G(bag_entity("h") == 0, ltl_Implies(
+            bag_entity("x") > 0,
+            ltl_X(True, bag_And(bag_entity("x") > 0, bag_entity("xp") > 0))))
+    
+    
     # obs_2 = ltl_And(f_y2, reach_y, reach_Y, delayed_Y, delayed_Q)
 
     # f_x2 = ltl_G(True, ltl_Implies(
@@ -461,13 +124,33 @@ def gene_expression(cmd_args):
     #     ltl_X(bag_Not("h"), exact_state("X", all_entities))))
     #
     
-    param_constr = param_And(param_entity(lda3, "Y") > 0, param_entity(lda2, "Q") == 0, param_entity(lda1, "yp") == 0, param_entity(lda1, "Y") == 0)
+    related_to_x = ["x", "xp", "X"]
+    related_to_y = ["y", "yp", "Y"]
+    params_for_x = [lda0]
+    params_for_y = [lda1, lda2, lda3]
+    
+    
+    
+    no_x_in_y = param_True()
+    for par in params_for_y:
+        for ent in related_to_x:
+            no_x_in_y = param_And(no_x_in_y, param_entity(par, ent) == 0)
+    
+    no_y_in_x = param_True()
+    for par in params_for_x:
+        for ent in related_to_y:
+            no_y_in_x = param_And(no_y_in_x, param_entity(par, ent) == 0)
+    
+    # param_constr = param_And(param_entity(lda3, "Y") > 0, param_entity(lda3, "X") == 0, param_entity(lda2, "Q") == 0, param_entity(lda1, "yp") == 0, param_entity(lda1, "Y") == 0)
+    param_constr = param_And(no_y_in_x, no_x_in_y)
         
     smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
     #
-    smt_rsc.check_rsltl(formulae_list=[obs_1], param_constr=param_constr) #, max_level=4, cont_if_sat=True)
+    smt_rsc.check_rsltl(
+        formulae_list=[obs_1,obs_2],
+        param_constr=param_constr,
+    ) #, max_level=4, cont_if_sat=True)
 
-    # smt_rsc.check_rsltl(formula=f_x1, print_witness=True)
 
 def gene_expression_full(cmd_args):
     """
@@ -962,236 +645,3 @@ def heat_shock_response(print_system=True):
 def state_translate_rsc2rs(p):
     return [e[0] + "#" + str(e[1]) for e in p]    
 
-
-def scalable_chain(print_system=False):
-    
-    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])
-        
-    if chainLen < 1 or maxConc < 1:
-        print("be reasonable")
-        exit(1)
-    if not formula_number in range(1,5+1):
-        print("formulaNumber must be in 1..5")
-        exit(1)
-    
-    r = ReactionSystemWithConcentrations()
-    r.add_bg_set_entity(("inc",1))
-    r.add_bg_set_entity(("dec",1))
-    
-    for i in range(1,chainLen+1):
-        r.add_bg_set_entity(("e_" + str(i),maxConc))
-    
-    for i in range(1,chainLen+1):
-        ent = "e_" + str(i)
-        r.add_reaction_inc(ent, "inc", [(ent, 1)],[(ent,maxConc)])
-        r.add_reaction_dec(ent, "dec", [(ent, 1)],[])
-        if i < chainLen:
-            r.add_reaction([(ent,maxConc)],[],[("e_"+str(i+1),1)])
-
-    r.add_reaction([("e_" + str(chainLen),maxConc)],[("dec",1)],[("e_" + str(chainLen),maxConc)])
-        
-    c = ContextAutomatonWithConcentrations(r)
-    c.add_init_state("init")
-    c.add_state("working")
-    c.add_transition("init", [("e_1",1),("inc",1)], "working")
-    c.add_transition("working", [("inc",1)], "working")
-    
-    rc = ReactionSystemWithAutomaton(r,c)
-    
-    if print_system:
-        rc.show()
-    
-    smt_rsc = SmtCheckerRSC(rc)
-
-    if formula_number == 1:
-        f_1 = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) >= maxConc) )
-        smt_rsc.check_rsltl(formula=f_1)
-    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_2 = f_tmp
-        smt_rsc.check_rsltl(formula=f_2)
-    elif formula_number == 3:
-        f_3 = Formula_rsLTL.f_G( BagDescription.f_TRUE(),
-            Formula_rsLTL.f_Implies(
-                (BagDescription.f_entity('e_1') == 1),
-                Formula_rsLTL.f_F(
-                    BagDescription.f_entity("inc") > 0,
-                    (BagDescription.f_entity('e_'+str(chainLen)) == maxConc)
-                )
-            )
-        )
-        print(i)
-        smt_rsc.check_rsltl(formula=f_3)
-    elif formula_number == 4:
-        f_4 = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') == maxConc )
-        smt_rsc.check_rsltl(formula=f_4)
-        
-    elif formula_number == 5:
-        f_5 = 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 ) )
-        smt_rsc.check_rsltl(formula=f_5)
-    
-    ###########################################################################
-
-    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.write(log_str)
-    f.close()
-    
-    f=open(filename_m, 'a')
-    log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n"
-    f.write(log_str)
-    f.close()
-
-
-def test_rsLTL():
-
-    r = ReactionSystemWithConcentrations()
-    r.add_bg_set_entity(("inc",2))
-    r.add_bg_set_entity(("ent1",1))
-    r.add_bg_set_entity(("ent2",5))
-    r.add_reaction([("ent2",1),("inc",1)],[],[("ent2",2)])
-    r.add_reaction([("ent2",2)],[],[("ent2",2)])
-
-    c = ContextAutomatonWithConcentrations(r)
-    c.add_init_state("init")
-    c.add_state("working")
-    c.add_transition("init", [("ent2",1),("inc",1)], "working")
-    c.add_transition("working", [("inc",1)], "working")
-
-    # x = ( Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_bag( ~((BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) ) ) ) & Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_bag( ~((BagDescription.f_entity("ent3") == 1) ) ) )
-    x = Formula_rsLTL.f_G((BagDescription.f_entity("inc") > 0), (BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3))
-    
-    #x = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("ent2") == 2) )
-    
-    print(x)
-    
-    rc = ReactionSystemWithAutomaton(r,c)
-    rc.show()
-    
-    checker = SmtCheckerRSC(rc)
-    checker.check_rsltl(formula=x)
-    
-    # checker.dummy_unroll(10)
-    # e = rsLTL_Encoder(checker)
-    # print(checker.get_loop_encodings())
-    # print(e.encode(x, 0, 10))
-
-def test_extended_automaton():
-    
-    r = ReactionSystem()
-    r.add_bg_set_entity("a")
-    r.add_bg_set_entity("b")
-    r.add_bg_set_entity("inc")
-    r.add_bg_set_entity("dec")
-    r.add_bg_set_entity("decx")
-    r.add_bg_set_entity("baam")
-
-    c1 = ExtendedContextAutomaton(r)
-    c1.add_init_state("init")
-    c1.name = "catest"
-    c1.add_state("working")
-    c1.add_action("act1")
-    c1.add_action("act2")
-    c1.add_transition("init", ["act1", "act2"], (["a"],["b"],["inc","dec"]), "working")
-    c1.add_transition("working", ["act2"], ([],[],["inc"]), "working")
-
-    c2 = ExtendedContextAutomaton(r)
-    c2.add_init_state("init")
-    c2.name = "c2"
-    c2.add_state("working")
-    c2.add_action("act1")
-    c2.add_action("act2")
-    c2.add_transition("init", ["act1", "act2"], ([],[],["inc"]), "working")
-    c2.add_transition("working", ["act2"], ([],[],["inc"]), "working")
-    
-    c3 = ExtendedContextAutomaton(r)
-    c3.add_init_state("init")
-    c3.name = "c3"
-    c3.add_state("working")
-    c3.add_action("act1")
-    c3.add_transition("init", ["act1"], ([],[],["inc"]), "working")
-    
-    c4 = ExtendedContextAutomaton(r)
-    c4.add_init_state("init")
-    c4.name = "c4"
-    c4.add_state("w")
-    c4.add_action("action_x")
-    c4.add_transition("init", ["action_x"], ([],[],["baam"]), "w")
-    #
-    # c4 = ExtendedContextAutomaton(r)
-    # c4.add_init_state("init")
-    # c4.name = "c4"
-    # c4.add_state("working")
-    # c4.add_action("act1")
-    # c4.add_action("act42")
-    # c4.add_transition("init", ["act1", "act42"], ([],[],["inc"]), "working")
-    # c4.add_transition("working", ["act42"], ([],[],["inc"]), "working")
-    #
-    # c5 = ExtendedContextAutomaton(r)
-    # c5.add_init_state("init")
-    # c5.name = "c5"
-    # c5.add_state("working")
-    # c5.add_action("act1")
-    # c5.add_action("act2")
-    # c5.add_transition("init", ["act1", "act2"], ([],[],["inc"]), "working")
-    # c5.add_transition("working", ["act2"], ([],[],["inc"]), "working")
-
-    na = NetworkOfContextAutomata(r, [c1,c2,c3,c4])
-
-    rna = ReactionSystemWithNetworkOfAutomata(r,na)
-
-    rna.show()
-    
-    checker = SmtCheckerRSNA(rna)
-    
-    checker.check_reachability([])
-
-def process():
-    
-    # rs_examples.run_counter_exp()
-    rs_examples.chain_reaction(print_system=True)
-    # rs_examples.heat_shock_response()
-    
-    
-
-# RS:
-# rsca = rs_examples.ca_toy_ex1()
-# rsca.show()
-# smt = SmtCheckerRS(rsca)
-# smt.check_reachability(rs_examples.ca_toy_ex1_property1(), print_time=True)
-
-# rsca = rs_examples.ca_bitctr(N)
-# rsca.show(True)
-# smt = SmtCheckerRS(rsca)
-# smt.check_reachability(rs_examples.ca_bitctr_property(N), print_time=True)
-
-# Distributed RS:
-#drs = rs_examples.drs_mutex(N)
-#drs.show()
-
-#smt = SmtCheckerDistribRS(drs,debug_level=0)
-#smt.check_reachability(rs_examples.drs_mutex_property1(N),
-#    exclusive_state=False,
-#    max_level=10,
-#    print_time=True,
-#    print_mem=True)
-
-# drs = rs_examples.drs_toy_ex1()
-# drs.show()
-#
-# smt = SmtCheckerDistribRS(drs,debug_level=3)
-# smt.check_reachability(rs_examples.drs_toy_ex1_property1(),max_level=10,print_time=True)

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 = BagDescription.f_And(last, get_bag_if_str(arg))
-            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)
@@ -106,3 +104,7 @@ def param_And(*args):
     for arg in args[1:]:
         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",
+        "-v", "--verbose", help="turn verbosity on", action="store_true"
-        help="scaling parameter value (used in some benchmarks)")
+    )
-    parser.add_argument("-s", "--special_mode",
+    parser.add_argument(
-                        help="special mode (used in some benchmarks)")
+        "-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(
+        init_state_enc = simplify(
-            level), self.enc_context_controller_init_state(level)))
+            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(
+                enc_reactants = simplify(
-                    self.v[level][reactant], self.v_ctx[level][reactant])))
+                    And(
+                        enc_reactants,
+                        Or(self.v[level][reactant], self.v_ctx[level][reactant]),
+                    )
+                )
             for inhibitor in inhibitors:
-                enc_inhibitors = simplify(And(enc_inhibitors, Not(
+                enc_inhibitors = simplify(
-                    Or(self.v[level][inhibitor], self.v_ctx[level][inhibitor]))))
+                    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),
+            And(Not(enc_enab_cond), Not(self.v[level + 1][prod_entity])),
-                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(
+        return simplify(And(self.enc_rs_trans(level), self.enc_automaton_trans(level)))
-            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(
+            enc_trans = simplify(And(enc_trans, Not(self.v[level + 1][prod_entity])))
-                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: " +
+                "[i] Memory: "
-                repr(
+                + repr(
-                    resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
+                    resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
-                    (1024 * 1024)) + " MB")
+                )
+                + " 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()[
+            rcts_for_prod_entity = self.rs.get_reactions_by_product()[prod_entity]
-                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(
+                enc_reactants = simplify(
-                    self.v[level][reactant] >= concentration, self.v_ctx[level][reactant] >= concentration)))
+                    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(
+                enc_inhibitors = simplify(
-                    self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
+                    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_products = self.v[level + 1][products[0][0]] == products[0][1]
-            enc_rct_prod = simplify(
+            enc_rct_prod = simplify(If(enc_rct_enabled, enc_products, enc_rct_prod))
-                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(
+                enc_reactants = simplify(
-                    self.v[level][reactant] >= concentration, self.v_ctx[level][reactant] >= concentration)))
+                    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(
+            enc_reactants = simplify(
-                self.v[level][command_entity] > 0, self.v_ctx[level][command_entity] > 0)))
+                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(
+                enc_inhibitors = simplify(
-                    self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
+                    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]
+                    self.v[level][prod_entity] > self.v_ctx[level][prod_entity],
-                    [prod_entity],
                     self.v[level][prod_entity],
-                    self.v_ctx[level][prod_entity]) + If(
+                    self.v_ctx[level][prod_entity],
-                    self.v[level][command_entity] > self.
+                ) + If(
-                    v_ctx[level][command_entity],
+                    self.v[level][command_entity] > self.v_ctx[level][command_entity],
                     self.v[level][command_entity],
-                    self.v_ctx[level][command_entity])
+                    self.v_ctx[level][command_entity],
-                enc_products = self.v[level+1][prod_entity] == value_after_inc
+                )
+                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[level][prod_entity] > self.v_ctx[level][prod_entity],
-                        self.v_ctx[level]
-                        [prod_entity],
                         self.v[level][prod_entity],
-                        self.v_ctx[level]
+                        self.v_ctx[level][prod_entity],
-                        [prod_entity]) -
+                    )
-                    If(
+                    - If(
-                        self.v[level]
+                        self.v[level][command_entity]
-                        [command_entity] > self.
+                        > self.v_ctx[level][command_entity],
-                        v_ctx[level][command_entity],
+                        self.v[level][command_entity],
-                        self.v[level]
+                        self.v_ctx[level][command_entity],
-                        [command_entity],
+                    )
-                        self.v_ctx[level]
+                )
-                        [command_entity]))
+                enc_products = self.v[level + 1][prod_entity] == If(
-                enc_products = self.v[level+1][prod_entity] == If(
+                    value_after_dec < 0, 0, value_after_dec
-                    value_after_dec < 0, 0, value_after_dec)
+                )
 
             else:
-                raise RuntimeError(
+                raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
-                    "Unknown meta-reaction type: " + repr(r_type))
 
             enc_meta_reaction_enabledness = And(
-                enc_reactants, enc_inhibitors,
+                enc_reactants, enc_inhibitors, Not(enc_ordinary_reactions_enabledness)
-                Not(enc_ordinary_reactions_enabledness))
+            )
             enc_enabledness = simplify(
-                Or(enc_enabledness, enc_meta_reaction_enabledness))
+                Or(enc_enabledness, enc_meta_reaction_enabledness)
-            enc_rct_prod = simplify(Or(enc_rct_prod, And(
+            )
-                enc_meta_reaction_enabledness, enc_products)))
+            enc_rct_prod = simplify(
+                Or(enc_rct_prod, And(enc_meta_reaction_enabledness, enc_products))
+            )
 
         # -----------------------------------------------------------------------------
 
         if not permanency_inhibition == None:
-
+            enc_reactants = Or(
-            enc_reactants = Or(self.v[level][prod_entity] >= concentration,
+                self.v[level][prod_entity] >= concentration,
-                               self.v_ctx[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(
+                enc_inhibitors = simplify(
-                    self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration)))
+                    And(
+                        enc_inhibitors,
+                        And(
+                            self.v[level][inhibitor] < concentration,
+                            self.v_ctx[level][inhibitor] < concentration,
+                        ),
+                    )
+                )
             enc_products = simplify(
-                self.v[level + 1][prod_entity] ==
+                self.v[level + 1][prod_entity]
-                If(
+                == If(
-                    self.v[level][prod_entity] > self.v_ctx[level]
+                    self.v[level][prod_entity] > self.v_ctx[level][prod_entity],
-                    [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,
+                enc_reactants, enc_inhibitors, Not(enc_ordinary_reactions_enabledness)
-                Not(enc_ordinary_reactions_enabledness))
+            )
-            enc_enabledness = simplify(
+            enc_enabledness = simplify(Or(enc_enabledness, enc_permanency_enabledness))
-                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(
+        return simplify(And(self.enc_rs_trans(level), self.enc_automaton_trans(level)))
-            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(
+            enc_trans = simplify(And(enc_trans, self.v[level + 1][prod_entity] == 0))
-                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(
+                    print(" " + self.rs.get_entity_name(var_id) + "=" + var_rep, end="")
-                        " " + 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,
+        self,
-            max_level=None):
+        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") +
+        print("[" + colour_str(C_BOLD, "i") + "] Running rsLTL bounded model checking")
-              "] 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_rs=self.v, var_ctx=self.v_ctx, var_loop_pos=self.loop_position
-            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.enc_concentration_levels_assertion(self.current_level + 1)
-                    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") +
+            print(
-                  "] Generating the formula encoding...")
+                "[" + 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: " +
+            print(
-                  str(encoder.get_cache_hits()) + ", encode calls: " +
+                "["
-                  str(ncalls[0]) + " (approx: " + str(ncalls[1]) + ")")
+                + colour_str(C_BOLD, "i")
-            print("[" + colour_str(C_BOLD, "i") +
+                + "] Cache hits: "
-                  "] Adding the formula to the solver...")
+                + 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") +
+            print("[" + colour_str(C_BOLD, "i") + "] Adding the loops encoding...")
-                  "] 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(
+                    + colour_str(C_BOLD, "+")
-                        C_GREEN, "SAT at level=" + str(self.current_level)))
+                    + "] "
+                    + 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") +
+            print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation")
-                  "] Unrolling the transition relation")
             self.solver.add(self.enc_transition_relation(self.current_level))
 
-            print(
+            print("{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
-                "{:->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(
+                "\n[i] {: >60}".format(" Time: " + repr(self.verification_time) + " s")
-                    " Time: " + repr(self.verification_time) + " s"))
+            )
 
         if print_mem:
             print(
                 "[i] {: >60}".format(
-                    " Memory: " +
+                    " Memory: "
-                    repr(
+                    + repr(
-                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
+                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss
-                        (1024 * 1024)) + " MB"))
+                        / (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):
+        for i in range(1, k + 1):
-            loop_enc = simplify(And(loop_enc, Implies(
+            loop_enc = simplify(
-                loop_var == i, self.state_equality(i-1, k))))
+                And(loop_enc, Implies(loop_var == i, self.state_equality(i - 1, k)))
+            )
 
         return loop_enc
 
-    def check_reachability(self, state, print_witness=True,
+    def check_reachability(
-                           print_time=True, print_mem=True, max_level=1000):
+        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.enc_concentration_levels_assertion(self.current_level + 1)
-                    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") +
+            print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...")
-                  "] Adding the reachability test...")
             self.solver.push()
 
-            self.solver.add(self.enc_state_with_blocking(
+            self.solver.add(self.enc_state_with_blocking(self.current_level, state))
-                self.current_level, state))
 
             result = self.solver.check()
             if result == sat:
                 print(
-                    "[" + colour_str(C_BOLD, "+") + "] " +
+                    "["
-                    colour_str(
+                    + colour_str(C_BOLD, "+")
-                        C_GREEN, "SAT at level=" + str(self.current_level)))
+                    + "] "
+                    + 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") +
+            print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation")
-                  "] Unrolling the transition relation")
             self.solver.add(self.enc_transition_relation(self.current_level))
 
-            print(
+            print("{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
-                "{:->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(
+                "\n[i] {: >60}".format(" Time: " + repr(self.verification_time) + " s")
-                    " Time: " + repr(self.verification_time) + " s"))
+            )
 
         if print_mem:
             print(
                 "[i] {: >60}".format(
-                    " Memory: " +
+                    " Memory: "
-                    repr(
+                    + repr(
-                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
+                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss
-                        (1024 * 1024)) + " MB"))
+                        / (1024 * 1024)
+                    )
+                    + " MB"
+                )
+            )
 
     def get_verification_time(self):
         return self.verification_time
 
-    def show_encoding(self, state, print_witness=True,
+    def show_encoding(
-                      print_time=False, print_mem=False, max_level=100):
+        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(
+            print("-----[ Working at level=" + str(self.current_level) + " ]-----")
-                "-----[ 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[+] " +
+                    "\n[+] "
-                    colour_str(
+                    + colour_str(C_RED, "SAT at level=" + str(self.current_level))
-                        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(
+        print_info(
-            path_idx, self.next_level_to_encode))
+            "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(
+        self.path_loop_position[path_idx] = Int("p{:d}_loop_pos".format(path_idx))
-            "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(
+                    new_var = Int(
-                        path_idx, level, reaction_id, entity_name))
+                        "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(
+                    new_var = Int(
-                        path_idx, level, reaction_id, entity_name))
+                        "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(
+                    "Pm{:s}_{:s}".format(param_name, self.rs.get_entity_name(entity))
-                        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(
+                enc_param_gz = simplify(And(enc_param_gz, pvar >= 0, pvar < 100))
-                    And(enc_param_gz, pvar >= 0, pvar < 100))
+                enc_param_at_least_one = simplify(Or(enc_param_at_least_one, pvar > 0))
-                enc_param_at_least_one = simplify(
-                    Or(enc_param_at_least_one, pvar > 0))
 
-            enc_non_empty = simplify(
+            enc_non_empty = simplify(And(enc_non_empty, enc_param_at_least_one))
-                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(
+        print_info(
-            path_idx, level))
+            "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 >=
+            enc_gz = simplify(
-                                  0, var <= e_max, var_ctx <= e_max))
+                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][
+            vars_per_reaction = self.path_v_improd_for_entities[path_idx][level + 1]
-                level + 1]
             if e_i in vars_per_reaction:
                 for var_improd in vars_per_reaction[e_i]:
-                    enc_gz = simplify(
+                    enc_gz = simplify(And(enc_gz, var_improd >= 0, var_improd <= e_max))
-                        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),
+            And(
-                self.enc_automaton_trans(level, path_idx)))
+                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(
-                                             Implies(
+                            rct_inh_constr,
-                                                 self.v_param
+                            Implies(
-                                                 [inh_param_name][entity] > 0,
+                                self.v_param[inh_param_name][entity] > 0,
-                                                 self.v_param
+                                self.v_param[rct_param_name][entity]
-                                                 [rct_param_name][entity] <
+                                < self.v_param[inh_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] > 0,
-                            self.v_param[inh_param_name][entity]))
+                            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(
-                    self.v_param[param_name][entity] == 0,
+                    enc_reactants,
-                    self.path_v[path_idx][level][entity] >= self.v_param[param_name][entity],
+                    Or(
-                    self.path_v_ctx[path_idx][level][entity] >= self.v_param[param_name][entity]))
+                        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],
+                    ),
+                )
         else:
             for entity, conc in reactants:
-                enc_reactants = And(enc_reactants, Or(
+                enc_reactants = And(
-                    self.path_v[path_idx][level][entity] >= conc,
+                    enc_reactants,
-                    self.path_v_ctx[path_idx][level][entity] >= conc))
+                    Or(
+                        self.path_v[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(
-                    self.v_param[param_name][entity] == 0,
+                    enc_inhibitors,
-                    And(
+                    Or(
-                        self.path_v[path_idx][level][entity] < self.v_param[param_name][entity],
+                        self.v_param[param_name][entity] == 0,
-                        self.path_v_ctx[path_idx][level][entity] < self.v_param[param_name][entity])))
+                        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],
+                        ),
+                    ),
+                )
         else:
             for entity, conc in inhibitors:
-                enc_inhibitors = And(enc_inhibitors, And(
+                enc_inhibitors = And(
-                    self.path_v[path_idx][level][entity] < conc,
+                    enc_inhibitors,
-                    self.path_v_ctx[path_idx][level][entity] < conc))
+                    And(
+                        self.path_v[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.
+                        enc_products,
-                        path_v_improd[path_idx]
+                        self.path_v_improd[path_idx][level + 1][reaction_id][entity]
-                        [level + 1][reaction_id]
+                        == self.v_param[param_name][entity],
-                        [entity] == self.v_param
+                    )
-                        [param_name][entity]))
+                )
         else:
             for entity, conc in products:
-                enc_products = simplify(And(
+                enc_products = simplify(
-                    enc_products, self.path_v_improd[path_idx][level + 1][reaction_id][entity] == conc))
+                    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 = simplify(
-                    enc_no_prod, self.path_v_improd[path_idx][level + 1][reaction_id][entity] == 0))
+                    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(
+        enc_not_enabled = Not(And(enc_reactants, enc_inhibitors)) == enc_no_prod
-            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 = simplify(
-                enc_max_prod, self.path_v[path_idx][level + 1][entity] == self.enc_max(per_reaction_vars)))
+                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(
+        enc_general_cond = self.enc_general_reaction_enabledness(level, path_idx)
-            level, path_idx)
 
-        enc_trans_with_max = simplify(
+        enc_trans_with_max = simplify(And(enc_general_cond, enc_max_prod, enc_trans))
-            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(
+                    print(" " + self.rs.get_entity_name(var_id) + "=" + var_rep, end="")
-                        " " + 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(
+            print_info(
-                str(formula), path_idx+1, len(formulae_list)))
+                "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(
+            print_info(
-                encoder.get_cache_hits(), ncalls[0], ncalls[1]))
+                "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(self.rs.get_entity_name(entity)) + "=" + str(var_rep),
-                        str(var_rep),
+                        end="",
-                        end="")
+                    )
             print(" }")
 
         print()
 
-    def enc_concentration_levels_assertions_for_paths(
+    def enc_concentration_levels_assertions_for_paths(self, level, num_of_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))
+                self.enc_concentration_levels_assertion(level, path_idx)
-        additional_assertions.append(
+            )
-            self.enc_param_concentration_levels_assertion())
+        additional_assertions.append(self.enc_param_concentration_levels_assertion())
 
         return additional_assertions
 
@@ -750,22 +799,25 @@ class SmtCheckerRSCParam(object):
         return enc_trans
 
     def print_level(self):
-        print(
+        print("{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
-            "{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
 
     def check_rsltl(
-            self, formulae_list,
+        self,
-            print_witness=True,
+        formulae_list,
-            print_time=True, print_mem=True,
+        print_witness=True,
-            max_level=None, cont_if_sat=False,
+        print_time=True,
-            param_constr=None):
+        print_mem=True,
+        max_level=None,
+        cont_if_sat=False,
+        param_constr=None,
+    ):
         """
         Bounded Model Checking for rsLTL properties
 
             * print_witness   -- prints the decoded witness
             * print_time      -- prints the time consumed
             * print_mem       -- prints the memory consumed
-            * max_level       -- if not None, the methods 
+            * max_level       -- if not None, the methods
                                  stops at the specified level
             * cont_if_sat     -- if True, then the method
                                  continues up until max_level is
@@ -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(
+            self.enc_concentration_levels_assertions_for_paths(0, num_of_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(
+                print_positive(
-                    "SAT at level={:d}".format(self.current_level)))
+                    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.solver_add(
-                self.current_level, num_of_paths))
+                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(
+        print_info("{: >60}".format(" Time: " + repr(self.verification_time) + " s"))
-            " Time: " + repr(self.verification_time) + " s"))
 
     def print_mem(self):
         print_info(
             "{: >60}".format(
-                " Memory: " +
+                " Memory: "
-                repr(
+                + repr(
-                    resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
+                    resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
-                    (1024 * 1024)) + " MB"))
+                )
+                + " 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):
+        for i in range(1, k + 1):
-            loop_enc = simplify(And(loop_enc, Implies(
+            loop_enc = simplify(
-                loop_var == i, self.state_equality(i-1, k))))
+                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,
+    def check_reachability(
-                           print_time=True, print_mem=True, max_level=1000):
+        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.enc_concentration_levels_assertion(self.current_level + 1)
-                    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") +
+            print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...")
-                  "] Adding the reachability test...")
             self.solver.push()
 
-            self.solver_add(self.enc_state_with_blocking(
+            self.solver_add(self.enc_state_with_blocking(self.current_level, state))
-                self.current_level, state))
 
             result = self.solver.check()
             if result == sat:
                 print(
-                    "[" + colour_str(C_BOLD, "+") + "] " +
+                    "["
-                    colour_str(
+                    + colour_str(C_BOLD, "+")
-                        C_GREEN, "SAT at level=" + str(self.current_level)))
+                    + "] "
+                    + 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") +
+            print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation")
-                  "] Unrolling the transition relation")
             self.solver_add(self.enc_transition_relation(self.current_level))
 
-            print(
+            print("{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
-                "{:->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(
+                "\n[i] {: >60}".format(" Time: " + repr(self.verification_time) + " s")
-                    " Time: " + repr(self.verification_time) + " s"))
+            )
 
         if print_mem:
             print(
                 "[i] {: >60}".format(
-                    " Memory: " +
+                    " Memory: "
-                    repr(
+                    + repr(
-                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss /
+                        resource.getrusage(resource.RUSAGE_SELF).ru_maxrss
-                        (1024 * 1024)) + " MB"))
+                        / (1024 * 1024)
+                    )
+                    + " MB"
+                )
+            )
 
     def get_verification_time(self):
         return self.verification_time
 
-    def show_encoding(self, state, print_witness=True,
+    def show_encoding(
-                      print_time=False, print_mem=False, max_level=100):
+        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(
+            print("-----[ Working at level=" + str(self.current_level) + " ]-----")
-                "-----[ 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[+] " +
+                    "\n[+] "
-                    colour_str(
+                    + colour_str(C_RED, "SAT at level=" + str(self.current_level))
-                        C_RED, "SAT at level=" + str(self.current_level)))
+                )
                 if print_witness:
                     self.decode_witness(self.current_level)
                 break