.github/workflows/tests.yml

@@ -0,0 +1,99 @@
+name: Tests
+
+on:
+  push:
+    branches: [master, refactor]
+  pull_request:
+    branches: [master]
+
+jobs:
+  bdd:
+    name: BDD tests
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install system dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y g++ make bison flex
+
+      - name: Build CUDD
+        working-directory: reactics-bdd
+        run: ./build_cudd.sh
+
+      - name: Build ReactICS BDD module
+        working-directory: reactics-bdd
+        run: make
+
+      - name: Run BDD tests
+        run: bash tests/run_tests.sh
+
+  smt:
+    name: SMT tests
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+
+      - name: Install Python dependencies
+        run: pip install z3-solver pytest
+
+      - name: Run SMT tests
+        run: python3 -m pytest tests/test_smt.py -v
+
+  generators:
+    name: Generator tests
+    runs-on: ubuntu-latest
+    needs: bdd
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install system dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y g++ make bison flex
+
+      - name: Build CUDD
+        working-directory: reactics-bdd
+        run: ./build_cudd.sh
+
+      - name: Build ReactICS BDD module
+        working-directory: reactics-bdd
+        run: make
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+
+      - name: Run generator tests
+        run: |
+          REACTICS="$PWD/reactics-bdd/reactics"
+          GENERATORS="$PWD/examples/bdd/generators"
+          failed=0
+          check_gen() {
+            local name="$1" gen_cmd="$2" property="$3" expected="$4"
+            local tmpfile=$(mktemp /tmp/reactics_gen_XXXXXX.drs)
+            eval "$gen_cmd" > "$tmpfile" 2>&1
+            local result=$("$REACTICS" -c "$property" "$tmpfile" 2>&1 | grep -oE "(holds|does not hold)" || true)
+            rm -f "$tmpfile"
+            if [ "$result" = "$expected" ]; then
+              echo "  PASS: $name"
+            else
+              echo "  FAIL: $name (expected '$expected', got '$result')"
+              failed=1
+            fi
+          }
+          check_gen "tgc(3) f1"        "python3 $GENERATORS/gen_tgc.py 3"        f1 "holds"
+          check_gen "tgc(3) f3"        "python3 $GENERATORS/gen_tgc.py 3"        f3 "holds"
+          check_gen "tgc(4) f2"        "python3 $GENERATORS/gen_tgc.py 4"        f2 "holds"
+          check_gen "asm(3) f1"        "python3 $GENERATORS/gen_asm.py 3"        f1 "holds"
+          check_gen "asm(3) f2"        "python3 $GENERATORS/gen_asm.py 3"        f2 "holds"
+          check_gen "drs(2,2,2,a) f0"  "python3 $GENERATORS/gen_drs.py 2 2 2 a"  f0 "does not hold"
+          check_gen "drs(2,2,2,b) f0"  "python3 $GENERATORS/gen_drs.py 2 2 2 b"  f0 "holds"
+          exit $failed

TESTING.md

@@ -0,0 +1,65 @@
+# Testing ReactICS
+
+## Prerequisites
+
+- **BDD module**: compiled (`./reactics setup` or `make` in `reactics-bdd/`)
+- **SMT module**: Python 3 with `z3-solver` and `pytest` installed
+
+```
+pip install z3-solver pytest
+```
+
+## Running all tests
+
+```
+./run_tests.sh
+```
+
+This runs the BDD, SMT, and generator test suites in sequence.
+
+## BDD tests
+
+```
+bash tests/run_tests.sh
+```
+
+10 regression tests that run the compiled `reactics-bdd/reactics` binary
+against example `.drs` files and compare output to saved baselines in
+`tests/expected/`. Covers:
+
+- Parsed system printing (`-P`)
+- Reaction listing (`-r`)
+- Reachable state enumeration (`-s`)
+- RSCTLK model checking (`-c`) for properties f1--f4
+
+Input files: `examples/bdd/tgc.drs`, `examples/bdd/tgc4.drs`,
+`reactics-bdd/in/trivial.drs`.
+
+To update baselines after an intentional output change, delete the
+relevant file in `tests/expected/` and re-run; the test will regenerate it.
+
+## SMT tests
+
+```
+python3 -m pytest tests/test_smt.py -v
+```
+
+23 pytest tests exercising the Python API directly. Organised by layer:
+
+- **Data model** -- ReactionSystem, concentrations, context automata,
+  formula construction (BagDescription, rsLTL)
+- **SmtCheckerRS** -- basic reachability (no concentrations)
+- **SmtCheckerRSC** -- reachability and rsLTL model checking with
+  concentrations (chain reaction, heat shock response)
+- **SmtCheckerRSCParam** -- parametric verification
+- **RSC-to-RS translation** -- verifying the translated system
+
+## Generator tests
+
+7 tests that run each generator (from `examples/bdd/generators/`),
+feed the output into the BDD model checker, and verify the expected
+verification result (holds / does not hold).
+
+Generators using old syntax (`examples/bdd/generators/old_syntax/`)
+are not tested this way as they are not compatible with the current
+parser.

examples/bdd/generators/gen_asm.py

@@ -0,0 +1,103 @@
+#!/usr/bin/env python3
+"""
+Generator for the Assembly-line (ASM) benchmark.
+
+Produces a distributed reaction system modelling an assembly line
+where N sequential processes pass activation tokens. Each process
+cycles through entities a -> y,b -> c -> d, and the final process
+signals 'done'. Uses a context automaton for scheduling.
+"""
+
+import argparse
+
+
+OPTIONS = "options { use-context-automaton; make-progressive; };\n"
+
+PROC_TEMPLATE = """
+    proc{i} {{
+        {{{{a}}, {{s}} -> {{y}}}};
+        {{{{y}}, {{s}} -> {{y}}}};
+        {{{{a}}, {{s}} -> {{b}}}};
+        {{{{b}}, {{s}} -> {{c}}}};
+        {{{{c}}, {{s}} -> {{d}}}};
+        {{{{d,y}}, {{s}} -> {{dy}}}};
+    }};
+"""
+
+FINAL_PROC = """
+    procFinal {
+        {{done}, {s} -> {done}};
+    };
+"""
+
+CA_TEMPLATE = """
+context-automaton {{
+    states {{ init, act }};
+    init-state {{ init }};
+    transitions {{
+{transitions}
+    }};
+}};
+"""
+
+PROPERTY_TEMPLATE = '\nrsctlk-property {{ {name} : {formula} }};\n'
+
+
+def generate(n):
+    out = OPTIONS
+    out += "\nreactions {\n"
+    for i in range(1, n + 1):
+        out += PROC_TEMPLATE.format(i=i)
+    out += FINAL_PROC
+    out += "};\n"
+
+    indent = 8 * " "
+    transitions = ""
+
+    # init -> act: first process gets activated
+    transitions += "{indent}{{ proc1={{a}} }}: init -> act;\n".format(indent=indent)
+
+    # act -> act: process stays idle (dy not produced)
+    for i in range(1, n + 1):
+        transitions += "{indent}{{ proc{i}={{}} }}: act -> act : ~proc{i}.dy;\n".format(
+            indent=indent, i=i)
+
+    # act -> act: next process gets activated when previous produces 'dy'
+    for i in range(2, n + 1):
+        transitions += "{indent}{{ proc{i}={{a}} }}: act -> act : proc{prev}.dy;\n".format(
+            indent=indent, i=i, prev=i - 1)
+
+    # act -> act: final process signals done when all have produced 'dy'
+    all_dy = " AND ".join("proc{}.dy".format(i) for i in range(1, n + 1))
+    transitions += "{indent}{{ procFinal={{done}} }}: act -> act : {guard};\n".format(
+        indent=indent, guard=all_dy)
+
+    out += CA_TEMPLATE.format(transitions=transitions)
+
+    # f1: the assembly line eventually completes
+    out += PROPERTY_TEMPLATE.format(name="f1", formula="EF( procFinal.done )")
+
+    # f2: last process knows its predecessor has produced 'y'
+    f2 = "AG( proc{n}.d IMPLIES K[proc{n}]( proc{prev}.y ) )".format(n=n, prev=n - 1)
+    out += PROPERTY_TEMPLATE.format(name="f2", formula=f2)
+
+    # x1: negation of f1 (sanity check -- should also hold)
+    out += PROPERTY_TEMPLATE.format(name="x1", formula="EF( ~procFinal.done )")
+
+    return out
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__,
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    parser.add_argument("n", type=int, help="number of processes (must be > 1)")
+    args = parser.parse_args()
+
+    if args.n < 2:
+        parser.error("number of processes must be > 1")
+
+    print(generate(args.n))
+
+
+if __name__ == "__main__":
+    main()

examples/bdd/generators/gen_drs.py

@@ -1,6 +1,15 @@
 #!/usr/bin/env python3
+"""
+Generator for the DRS (Distributed Reaction Systems) epistemic benchmark.
+
+Produces a distributed reaction system with epistemic properties
+(knowledge operators). The system models signal transduction cascades
+with configurable depth (x), number of components (y), threshold (z),
+and context automaton variant (a or b).
+"""
 
 import sys
+import argparse
 import itertools
 
 
@@ -272,18 +281,20 @@ class DRSGenerator:
 
 
 def main():
-    if len(sys.argv) < 1 + 4:
+    parser = argparse.ArgumentParser(description=__doc__,
-        print(f"Usage: {sys.argv[0]} <x> <y> <z> <Aut>")
+        formatter_class=argparse.RawDescriptionHelpFormatter)
-        print("\twhere x,y,z >= 2 and y >= z")
+    parser.add_argument("x", type=int, help="cascade depth (>= 2)")
-        print("\tAut: a, b")
+    parser.add_argument("y", type=int, help="number of components (>= 2, >= z)")
-        sys.exit(1)
+    parser.add_argument("z", type=int, help="threshold (>= 2, <= y)")
+    parser.add_argument("aut", choices=["a", "b"], help="automaton variant")
+    args = parser.parse_args()
 
-    g = DRSGenerator(
+    if args.x < 2 or args.y < 2 or args.z < 2:
-        x=int(sys.argv[1]),
+        parser.error("x, y, z must all be >= 2")
-        y=int(sys.argv[2]),
+    if args.y < args.z:
-        z=int(sys.argv[3]),
+        parser.error("y must be >= z")
-        aut=sys.argv[4],
+
-    )
+    DRSGenerator(x=args.x, y=args.y, z=args.z, aut=args.aut)
 
 
 if __name__ == "__main__":

examples/bdd/generators/gen_tgc.py

@@ -1,13 +1,20 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
+"""
+Generator for the Traffic Guard Controller (TGC) benchmark.
 
-from sys import argv,exit
+Produces a distributed reaction system where N processes compete
-
+for access to a shared resource, governed by a context automaton
-OPTIONS_STR = """
+with green/red states. Generates RSCTLK properties for liveness,
-options { use-context-automaton; make-progressive; };
+reachability, and mutual exclusion (epistemic).
 """
 
-PROC_STR = """
+import argparse
-    proc{:d} {{
+
+
+OPTIONS = "options { use-context-automaton; make-progressive; };\n"
+
+PROC_TEMPLATE = """
+    proc{i} {{
         {{{{out}}, {{}} -> {{approach}}}};
         {{{{approach}}, {{req}} -> {{req}}}};
         {{{{allowed}}, {{}} -> {{in}}}};
@@ -16,102 +23,94 @@ PROC_STR = """
     }};
 """
 
-CA_STR = """
+CA_TEMPLATE = """
 context-automaton {{
     states {{ init, green, red }};
     init-state {{ init }};
     transitions {{
-{:s}
+{transitions}
     }};
 }};
 """
 
-PROPERTY_STR = """
+PROPERTY_TEMPLATE = '\nrsctlk-property {{ {name} : {formula} }};\n'
-rsctlk-property {{ {:s} : {:s} }};
-"""
 
 
-#################################################################
+def conj(fmt, indices, sep=" AND "):
+    return sep.join(fmt.format(i=i) for i in indices)
 
-if len(argv) < 1:
-    print("Usage: {:s} <number of processes>".format(argv[0]))
-    exit(100)
 
-n = int(argv[1])
+def generate(n):
+    out = OPTIONS
+    out += "\nreactions {\n"
+    for i in range(n):
+        out += PROC_TEMPLATE.format(i=i)
+    out += "};\n"
 
-assert n > 1, "number of proc must be > 1"
+    indent = 8 * " "
+    transitions = ""
 
-out = ""
+    # init -> green: all processes start with 'out'
+    transitions += indent + "{ "
+    transitions += " ".join("proc{:d}={{out}}".format(i) for i in range(n))
+    transitions += " }: init -> green;\n"
 
-out += OPTIONS_STR
+    # green -> red: a process requests
-out += "reactions {\n"
+    for i in range(n):
-for i in range(n):
+        transitions += "{indent}{{ proc{i}={{allowed}} }}: green -> red : proc{i}.req;\n".format(
-    out += PROC_STR.format(i)
+            indent=indent, i=i)
-out += "};\n"
 
-transitions = ""
+    # green -> green: no requests pending
+    no_req = conj("~proc{i}.req", range(n))
+    for i in range(n):
+        transitions += "{indent}{{ proc{i}={{}} }}: green -> green : {guard};\n".format(
+            indent=indent, i=i, guard=no_req)
 
-init_trans = 8*" " + "{ "
+    # red -> green: a process leaves
-for i in range(n):
+    for i in range(n):
-    init_trans += "proc{:d}={{out}} ".format(i)
+        transitions += "{indent}{{ proc{i}={{}} }}: red -> green : proc{i}.leave;\n".format(
-init_trans += "}: init -> green;\n"
+            indent=indent, i=i)
-transitions += init_trans
 
-for i in range(n):
+    # red -> red: no process leaves
-    transitions += "{:s}{{ proc{:d}={{allowed}} }}: green -> red : proc{:d}.req;\n".format(8*" ", i, i)
+    no_leave = conj("~proc{i}.leave", range(n))
+    for i in range(n):
+        transitions += "{indent}{{ proc{i}={{}} }}: red -> red : {guard};\n".format(
+            indent=indent, i=i, guard=no_leave)
 
-no_req_cond = "~proc0.req"
+    out += CA_TEMPLATE.format(transitions=transitions)
-for i in range(1, n):
-     no_req_cond += " AND ~proc{:d}.req".format(i)
 
-for i in range(n):
+    # f1: each process can eventually enter
-    transitions += "{:s}{{ proc{:d}={{}} }}: green -> green : {:s};\n".format(8*" ", i, no_req_cond)
+    f1 = conj("EF( E<proc{i}.allowed>X( proc{i}.in ) )", range(n))
+    out += PROPERTY_TEMPLATE.format(name="f1", formula=f1)
 
-for i in range(n):
+    # f2: all processes can simultaneously approach
-    transitions += "{:s}{{ proc{:d}={{}} }}: red -> green : proc{:d}.leave;\n".format(8*" ", i, i)
+    f2 = "EF( " + conj("proc{i}.approach", range(n)) + " )"
+    out += PROPERTY_TEMPLATE.format(name="f2", formula=f2)
 
-no_leave_cond = "~proc0.leave"
+    # f3: mutual exclusion (knowledge)
-for i in range(1, n):
+    others_not_in = conj("~proc{i}.in", range(1, n))
-     no_leave_cond += " AND ~proc{:d}.leave".format(i)
+    f3 = "AG( proc0.in IMPLIES K[proc0]({}) )".format(others_not_in)
+    out += PROPERTY_TEMPLATE.format(name="f3", formula=f3)
 
-for i in range(n):
+    # f4: mutual exclusion (common knowledge)
-    transitions += "{:s}{{ proc{:d}={{}} }}: red -> red : {:s};\n".format(8*" ", i, no_leave_cond)
+    all_agents = conj("proc{i}", range(n), sep=",")
+    f4 = "AG( proc0.in IMPLIES C[{}]({}) )".format(all_agents, others_not_in)
+    out += PROPERTY_TEMPLATE.format(name="f4", formula=f4)
 
-out += CA_STR.format(transitions)
+    return out
 
-## f1
-#formula = "EF( proc0.in )"
-#out += PROPERTY_STR.format("f1",formula)
 
-# f1
+def main():
-formula = "EF( E<proc0.allowed>X( proc0.in ) )"
+    parser = argparse.ArgumentParser(description=__doc__,
-for i in range(1, n):
+        formatter_class=argparse.RawDescriptionHelpFormatter)
-    formula += " AND EF( E<proc{:d}.allowed>X( proc{:d}.in ) )".format(i, i)
+    parser.add_argument("n", type=int, help="number of processes (must be > 1)")
-out += PROPERTY_STR.format("f1",formula)
+    args = parser.parse_args()
 
-# f2
+    if args.n < 2:
-formula = "EF( proc0.approach"
+        parser.error("number of processes must be > 1")
-for i in range(1, n):
-    formula += " AND proc{:d}.approach".format(i)
-formula += " )"
-out += PROPERTY_STR.format("f2",formula)
 
-# f3
+    print(generate(args.n))
-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)
 
+if __name__ == "__main__":
+    main()

examples/bdd/generators/old_syntax/gen_abstract.py

@@ -0,0 +1,62 @@
+#!/usr/bin/env python3
+"""
+Generator for the Abstract Pipeline benchmark.
+
+Produces a reaction system modelling a pipeline of N modules,
+each cycling through entities a -> y,b -> c -> d before passing
+activation to the next module. The final reaction requires all
+modules to have completed (all y_i present).
+
+NOTE: generates old-syntax input (context-entities, initial-contexts,
+rsctl-property) which is not compatible with the current parser.
+"""
+
+import argparse
+
+
+def generate(n, variant):
+    out = "reactions {\n"
+    out += "\t{ {x},{s} -> {a1} };\n"
+
+    for i in range(1, n + 1):
+        out += "\t{{ {{a{i}}},{{s}} -> {{y{i}}} }};\n".format(i=i)
+        out += "\t{{ {{a{i}}},{{s}} -> {{b{i}}} }};\n".format(i=i)
+        out += "\t{{ {{b{i}}},{{s}} -> {{c{i}}} }};\n".format(i=i)
+        out += "\t{{ {{c{i}}},{{s}} -> {{d{i}}} }};\n".format(i=i)
+        out += "\t{{ {{d{i},y{i}}},{{s}} -> {{a{j}}} }};\n".format(i=i, j=i + 1)
+        out += "\t{{ {{y{i}}},{{s}} -> {{y{i}}} }};\n".format(i=i)
+
+    final_reactants = "a" + str(n + 1)
+    for i in range(1, n + 1):
+        final_reactants += ",y" + str(i)
+    out += "\t{{ {{{r}}},{{s}} -> {{r}} }};\n".format(r=final_reactants)
+    out += "}\n"
+
+    if variant == 1:
+        out += "context-entities { s }\n"
+    elif variant == 2:
+        ctx = "s"
+        for i in range(1, n + 1):
+            if i % 2 == 0:
+                ctx += ",a" + str(i)
+        out += "context-entities {{ {} }}\n".format(ctx)
+
+    out += "initial-contexts { {x} }\n"
+    out += "rsctl-property { E[{}]F(r) }\n"
+
+    return out
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__,
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    parser.add_argument("n", type=int, help="number of pipeline modules")
+    parser.add_argument("variant", type=int, choices=[1, 2],
+        help="context variant (1: minimal, 2: extended)")
+    args = parser.parse_args()
+
+    print(generate(args.n, args.variant))
+
+
+if __name__ == "__main__":
+    main()

examples/bdd/generators/old_syntax/gen_bc.py

@@ -0,0 +1,88 @@
+#!/usr/bin/env python3
+"""
+Generator for the Binary Counter (BC) benchmark.
+
+Produces a reaction system modelling an N-bit binary counter
+with increment and decrement operations controlled via context
+entities. Generates one of four RSCTL properties.
+
+NOTE: generates old-syntax input (context-entities, initial-contexts,
+rsctl-property) which is not compatible with the current parser.
+"""
+
+import argparse
+
+K = 8  # constant used by property 3
+
+
+def generate(n, prop):
+    out = "reactions {\n"
+
+    # (1) no dec, no inc: bits persist
+    out += "\t# (1) no decrement, no increment\n"
+    for j in range(n):
+        out += "\t{{{{p{j}}},{{dec,inc}} -> {{p{j}}}}};\n".format(j=j)
+
+    # (2) increment operation
+    out += "\n\t# (2) increment operation\n"
+    out += "\t{{inc},{dec,p0} -> {p0}};\n"
+    for j in range(1, n):
+        bits = ",".join("p" + str(k) for k in range(j))
+        out += "\t{{{{inc,{bits}}},{{dec,p{j}}} -> {{p{j}}}}};\n".format(bits=bits, j=j)
+
+    out += "\n\t# the more significant bits remain (inc)\n"
+    for j in range(n):
+        for k in range(j + 1, n):
+            out += "\t{{{{inc,p{k}}},{{dec,p{j}}} -> {{p{k}}}}};\n".format(j=j, k=k)
+
+    # (3) decrement operation
+    out += "\n\t# (3) decrement operation\n"
+    for j in range(n):
+        bits = ",".join("p" + str(k) for k in range(j + 1))
+        out += "\t{{{{dec}},{{inc,{bits}}} -> {{p{j}}}}};\n".format(bits=bits, j=j)
+
+    out += "\n\t# the more significant bits remain (dec)\n"
+    for j in range(n):
+        for k in range(j + 1, n):
+            out += "\t{{{{dec,p{j},p{k}}},{{inc}} -> {{p{k}}}}};\n".format(j=j, k=k)
+
+    out += "}\n\n"
+    out += "context-entities { inc,dec }\n"
+    out += "initial-contexts { {} }\n"
+
+    if prop == 1:
+        all_neg = " AND ".join("~p" + str(i) for i in range(n))
+        all_pos = " AND ".join("p" + str(i) for i in range(n))
+        out += "rsctl-property {{ AG(({}) IMPLIES E[{{inc}},{{dec}}]F({})) }}\n".format(
+            all_neg, all_pos)
+    elif prop == 2:
+        all_pos = " AND ".join("p" + str(i) for i in range(n))
+        all_neg = " AND ".join("~p" + str(i) for i in range(n))
+        out += "rsctl-property {{ AG(({}) IMPLIES A[{{inc}}]X({})) }}\n".format(
+            all_pos, all_neg)
+    elif prop == 3:
+        parts = ["p" + str(i) for i in range(n - K)]
+        parts += ["~p" + str(i) for i in range(n - K, n)]
+        out += "rsctl-property {{ E[{{inc}}]F({}) }}\n".format(" AND ".join(parts))
+    elif prop == 4:
+        out += "rsctl-property {{ AG( p{} IMPLIES EF ~p{} ) }}\n".format(n - 1, n - 1)
+
+    return out
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__,
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    parser.add_argument("n", type=int, help="number of bits")
+    parser.add_argument("property", type=int, choices=[1, 2, 3, 4],
+        help="property to generate (1-4)")
+    args = parser.parse_args()
+
+    if args.property == 3 and args.n < K + 1:
+        parser.error("n must be >= {} for property 3".format(K + 1))
+
+    print(generate(args.n, args.property))
+
+
+if __name__ == "__main__":
+    main()

examples/bdd/generators/old_syntax/gen_mutex.py

@@ -0,0 +1,71 @@
+#!/usr/bin/env python3
+"""
+Generator for the Mutual Exclusion (Mutex) benchmark.
+
+Produces a reaction system modelling N processes competing for
+exclusive access to a critical section, using activation signals,
+request tokens, and a lock. Generates one of three RSCTL properties.
+
+NOTE: generates old-syntax input (context-entities, initial-contexts,
+rsctl-property) which is not compatible with the current parser.
+"""
+
+import argparse
+
+
+def generate(n, formula):
+    out = "reactions {\n"
+    for i in range(n):
+        out += "\t{{{{out{i},act{i}}},{{}} -> {{request{i}}}}};\n".format(i=i)
+        out += "\t{{{{out{i}}},{{act{i}}} -> {{out{i}}}}};\n".format(i=i)
+
+        for j in range(n):
+            if i != j:
+                out += "\t{{{{request{i},act{i},act{j}}},{{}} -> {{request{i}}}}};\n".format(
+                    i=i, j=j)
+
+        out += "\t{{{{request{i}}},{{act{i}}} -> {{request{i}}}}};\n".format(i=i)
+
+        other_acts = ",".join("act" + str(j) for j in range(n) if i != j)
+        out += "\t{{{{request{i},act{i}}},{{{others},lock}} -> {{in{i},lock}}}};\n".format(
+            i=i, others=other_acts)
+
+        out += "\t{{{{in{i},act{i}}},{{}} -> {{out{i},done}}}};\n".format(i=i)
+        out += "\t{{{{in{i}}},{{act{i}}} -> {{in{i}}}}};\n".format(i=i)
+
+    out += "\t{{lock},{done} -> {lock}};\n"
+    out += "}\n"
+
+    ctx_ents = ",".join("act" + str(i) for i in range(n))
+    out += "context-entities {{ {} }}\n".format(ctx_ents)
+
+    init_ents = ",".join("out" + str(i) for i in range(n))
+    out += "initial-contexts {{ {{{}}} }}\n".format(init_ents)
+
+    if formula == 1:
+        out += "rsctl-property { A[{act1}]F(in1) }\n"
+    elif formula == 2:
+        out += "rsctl-property { E[{act1}]F(in1) }\n"
+    elif formula == 3:
+        pairs = []
+        for i in range(n):
+            for j in range(i + 1, n):
+                pairs.append("~(in{} AND in{})".format(i, j))
+        out += "rsctl-property {{ AG({}) }}\n".format(" AND ".join(pairs))
+
+    return out
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__,
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    parser.add_argument("n", type=int, help="number of processes")
+    parser.add_argument("formula", type=int, choices=[1, 2, 3],
+        help="formula to generate (1: A[]F, 2: E[]F, 3: AG mutex)")
+    args = parser.parse_args()
+
+    print(generate(args.n, args.formula))
+
+
+if __name__ == "__main__":
+    main()

examples/bdd/tgc4.drs

@@ -0,0 +1,70 @@
+
+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}};
+    };
+
+    proc3 {
+        {{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} proc3={out} }: init -> green;
+        { proc0={allowed} }: green -> red : proc0.req;
+        { proc1={allowed} }: green -> red : proc1.req;
+        { proc2={allowed} }: green -> red : proc2.req;
+        { proc3={allowed} }: green -> red : proc3.req;
+        { proc0={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req AND ~proc3.req;
+        { proc1={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req AND ~proc3.req;
+        { proc2={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req AND ~proc3.req;
+        { proc3={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req AND ~proc3.req;
+        { proc0={} }: red -> green : proc0.leave;
+        { proc1={} }: red -> green : proc1.leave;
+        { proc2={} }: red -> green : proc2.leave;
+        { proc3={} }: red -> green : proc3.leave;
+        { proc0={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave AND ~proc3.leave;
+        { proc1={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave AND ~proc3.leave;
+        { proc2={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave AND ~proc3.leave;
+        { proc3={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave AND ~proc3.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 ) ) AND EF( E<proc3.allowed>X( proc3.in ) ) };
+
+rsctlk-property { f2 : EF( proc0.approach AND proc1.approach AND proc2.approach AND proc3.approach ) };
+
+rsctlk-property { f3 : AG( proc0.in IMPLIES K[proc0](~proc1.in AND ~proc2.in AND ~proc3.in) ) };
+
+rsctlk-property { f4 : AG( proc0.in IMPLIES C[proc0,proc1,proc2,proc3](~proc1.in AND ~proc2.in AND ~proc3.in) ) };
+

reactics-bdd/ctx_aut.cc

@@ -13,12 +13,7 @@ CtxAut::CtxAut(Options *opts, RctSys *parent_rctsys)
 
 bool CtxAut::hasState(std::string name)
 {
-  if (states_names.find(name) == states_names.end()) {
+  return states_names.find(name) != states_names.end();
-    return false;
-  }
-  else {
-    return true;
-  }
 }
 
 State CtxAut::getStateID(std::string name)

reactics-bdd/ctx_aut.hh

@@ -12,10 +12,7 @@
 #include <vector>
 #include <string>
 #include <cstdlib>
-// #include "rs.hh"
 #include "types.hh"
-// #include "options.hh"
-// #include "stateconstr.hh"
 
 using std::cout;
 using std::endl;

reactics-bdd/drs_benchmark.sh

@@ -1,6 +1,6 @@
 #!/bin/sh
 
-TMPINPUT="tmp_$RANDOM$RANDOM.rs"
+TMPINPUT="tmp_$RANDOM$RANDOM.drs"
 
 CMD="./reactics -B"
 

reactics-bdd/formrsctlk.cc

@@ -172,39 +172,6 @@ bool FormRSCTLK::isERSCTLK(void) const
 
 std::string FormRSCTLK::getActionsStr(void) const
 {
-  // if (actions != nullptr) {
-  //   std::string r = "[ ";
-  //   bool firstact = true;
-  //
-  //   for (ActionsVec_f::iterator act = actions->begin(); act != actions->end();
-  //        ++act) {
-  //     if (!firstact) {
-  //       r += ",";
-  //     }
-  //     else {
-  //       firstact = false;
-  //     }
-  //
-  //     r += "{";
-  //     bool firstent = true;
-  //
-  //     for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent) {
-  //       if (!firstent) {
-  //         r += ",";
-  //       }
-  //       else {
-  //         firstent = false;
-  //       }
-  //
-  //       r += *ent;
-  //     }
-  //
-  //     r += "}";
-  //   }
-  //
-  //   r += " ]";
-  //   return r;
-  // }
   if (boolCtx != nullptr) {
     return "< " + boolCtx->toStr() + " >";
   }
@@ -222,22 +189,6 @@ void FormRSCTLK::encodeActions(const SymRS *srs)
 
     actions_bdd = new BDD(srs->getBDDfalse());
     assert(boolCtx != nullptr);
-    // assert(actions != nullptr || boolCtx != nullptr);
-    // assert(!(actions != nullptr && boolCtx != nullptr));
-
-    // if (actions != nullptr) {
-    //   for (ActionsVec_f::iterator act = actions->begin(); act != actions->end();
-    //        ++act) {
-    //     BDD single_action = srs->getBDDtrue();
-    //
-    //     for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent) {
-    //       single_action *= srs->encActStrEntity(*ent);
-    //     }
-    //
-    //     single_action = srs->compContext(single_action);
-    //     *actions_bdd += single_action;
-    //   }
-    // }
     if (boolCtx != nullptr) {
       *actions_bdd = boolCtx->getBDDforContext(srs);
     }

reactics-bdd/formrsctlk.hh

@@ -9,7 +9,6 @@
 #include <iostream>
 #include <string>
 #include <cassert>
-// #include "rs.hh"
 #include "symrs.hh"
 #include "cudd.hh"
 #include "types.hh"
@@ -56,9 +55,6 @@
 using std::cout;
 using std::endl;
 
-// typedef std::string Entity_f;
-// typedef std::set<Entity_f> Action_f;
-// typedef vector<Action_f> ActionsVec_f;
 typedef std::set<std::string> Agents_f;
 
 class StateConstr;
@@ -74,7 +70,6 @@ class FormRSCTLK
     std::string proc_name;
     bool tf;
     BDD *bdd;
-    // ActionsVec_f *actions;
     BDD *actions_bdd;
     StateConstr *boolCtx;
     Agents_f agents;
@@ -93,7 +88,6 @@ class FormRSCTLK
       arg[0] = nullptr;
       arg[1] = nullptr;
       bdd = nullptr;
-      // actions = nullptr;
       actions_bdd = nullptr;
       boolCtx = nullptr;
     }
@@ -110,7 +104,6 @@ class FormRSCTLK
       arg[0] = nullptr;
       arg[1] = nullptr;
       bdd = nullptr;
-      // actions = nullptr;
       actions_bdd = nullptr;
       boolCtx = nullptr;
     }
@@ -126,28 +119,10 @@ class FormRSCTLK
       arg[0] = form1;
       arg[1] = form2;
       bdd = nullptr;
-      // actions = nullptr;
       actions_bdd = nullptr;
       boolCtx = nullptr;
     }
 
-    /**
-     * @brief Constructor for two-argument formula with action restrictions.
-     */
-    // FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1, FormRSCTLK *form2)
-    // {
-    //   assert(acts != nullptr);
-    //   assert(RSCTLK_COND_2ARG(op));
-    //   assert(RSCTLK_COND_ACT(op));
-    //   oper = op;
-    //   arg[0] = form1;
-    //   arg[1] = form2;
-    //   bdd = nullptr;
-    //   actions = acts;
-    //   actions_bdd = nullptr;
-    //   boolCtx = nullptr;
-    // }
-
     /**
      * @brief Constructor for two-argument formula with Boolean context restrictions.
      */
@@ -160,7 +135,6 @@ class FormRSCTLK
       arg[0] = form1;
       arg[1] = form2;
       bdd = nullptr;
-      // actions = nullptr;
       actions_bdd = nullptr;
       boolCtx = bctx;
     }
@@ -176,28 +150,10 @@ class FormRSCTLK
       arg[0] = form1;
       arg[1] = nullptr;
       bdd = nullptr;
-      // actions = nullptr;
       actions_bdd = nullptr;
       boolCtx = nullptr;
     }
 
-    /**
-     * @brief Constructor for one-argument formula with action restrictions.
-     */
-    // FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1)
-    // {
-    //   assert(acts != nullptr);
-    //   assert(RSCTLK_COND_1ARG(op));
-    //   assert(RSCTLK_COND_ACT(op));
-    //   oper = op;
-    //   arg[0] = form1;
-    //   arg[1] = nullptr;
-    //   bdd = nullptr;
-    //   // actions = acts;
-    //   actions_bdd = nullptr;
-    //   boolCtx = nullptr;
-    // }
-
     /**
      * @brief Constructor for one-argument formula with Boolean context restrictions.
      */
@@ -210,7 +166,6 @@ class FormRSCTLK
       arg[0] = form1;
       arg[1] = nullptr;
       bdd = nullptr;
-      // actions = nullptr;
       actions_bdd = nullptr;
       boolCtx = bctx;
     }
@@ -234,7 +189,6 @@ class FormRSCTLK
       delete arg[0];
       delete arg[1];
       delete bdd;
-      // delete actions;
       delete actions_bdd;
       delete boolCtx;
     }

reactics-bdd/in/scripts/bench_bc.sh

@@ -42,10 +42,10 @@ for form in $forms; do
 
         echo "$x" > $filename
 
-        ./gen_bc.py $n $form > tmp.rs
+        ./gen_bc.py $n $form > tmp.drs
 
-        echo "EXEC: $tool $options $popt tmp.rs"
+        echo "EXEC: $tool $options $popt tmp.drs"
-        $tool $options $popt tmp.rs >&1  >> $filename 
+        $tool $options $popt tmp.drs >&1  >> $filename 
 
         result="$(tail -1 $filename | grep -E '.*;.*;.*;.*'| sed "s/STAT/$n /")"
         if [ "$result" = "" ];then

reactics-bdd/in/scripts/bench_mutex.sh

@@ -44,11 +44,11 @@ for form in $forms; do
 
         echo "$x" > $filename
 
-        ./gen_mutex.py $n $form > tmp.rs
+        ./gen_mutex.py $n $form > tmp.drs
 
-        echo "EXEC: $tool $options $popt tmp.rs"
+        echo "EXEC: $tool $options $popt tmp.drs"
 
-        $tool $options $popt tmp.rs >&1  >> $filename 
+        $tool $options $popt tmp.drs >&1  >> $filename 
 
         result="$(tail -1 $filename | grep -E '.*;.*;.*;.*'| sed "s/STAT/$n /")" 
         if [ "$result" = "" ];then

reactics-bdd/in/scripts/bench_pipe.sh

@@ -43,11 +43,11 @@ for form in $forms; do
 
         echo "$x" > $filename
 
-        ./gen_abstract1.py $n $form > tmp.rs
+        ./gen_abstract1.py $n $form > tmp.drs
 
-        echo "EXEC: $tool $options $popt tmp.rs"
+        echo "EXEC: $tool $options $popt tmp.drs"
 
-        $tool $options $popt tmp.rs >&1  >> $filename 
+        $tool $options $popt tmp.drs >&1  >> $filename 
 
         result="$(tail -1 $filename | grep -E '.*;.*;.*;.*'| sed "s/STAT/$n /")" 
         if [ "$result" = "" ];then

reactics-bdd/in/scripts/benchmark.sh

@@ -4,8 +4,8 @@ for x in `seq 2 1 24`;do
     echo $y $x
     filename="results/f${y}_n${x}.out"
     echo "$x" > $filename
-    ./gen_bc.py $x $y > tmp.rs
+    ./gen_bc.py $x $y > tmp.drs
-    ../main -c -B tmp.rs  >> $filename
+    ../main -c -B tmp.drs  >> $filename
     result="$(tail -1 $filename | sed "s/STAT/$x /")" 
     echo $result >> results/summary_f${y}.out
     echo $result
@@ -13,4 +13,4 @@ for x in `seq 2 1 24`;do
 done
 done
 
-rm tmp.rs
+rm tmp.drs

reactics-bdd/in/scripts/benchmark_abs1.sh

@@ -4,8 +4,8 @@ for x in `seq 1 60`;do
     echo $x
     filename="results/abs_v${y}_f0_n${x}.out"
     echo "$x" > $filename
-    ./gen_abstract1.py $x $y > tmp.rs
+    ./gen_abstract1.py $x $y > tmp.drs
-    ../main -z -c -p -v -B tmp.rs >&1  >> $filename 
+    ../main -z -c -p -v -B tmp.drs >&1  >> $filename 
     result="$(tail -1 $filename | sed "s/STAT/$x /")" 
     echo $result >> results/summary_v${y}_abs_f0.out
     echo $result
@@ -13,4 +13,4 @@ for x in `seq 1 60`;do
 done
 done
 
-rm tmp.rs
+rm tmp.drs

reactics-bdd/in/scripts/benchmark_abs1_PT.sh

@@ -4,8 +4,8 @@ for x in `seq 1 60`;do
     echo $x
     filename="results/abs_v${y}_f0_n${x}_PT.out"
     echo "$x" > $filename
-    ./gen_abstract1.py $x $y > tmp.rs
+    ./gen_abstract1.py $x $y > tmp.drs
-    ../main -z -x -c -p -v -B tmp.rs >&1  >> $filename 
+    ../main -z -x -c -p -v -B tmp.drs >&1  >> $filename 
     result="$(tail -1 $filename | sed "s/STAT/$x /")" 
     echo $result >> results/summary_v${y}_abs_f0_PT.out
     echo $result
@@ -13,4 +13,4 @@ for x in `seq 1 60`;do
 done
 done
 
-rm tmp.rs
+rm tmp.drs

reactics-bdd/in/scripts/benchmark_bc.sh

@@ -4,8 +4,8 @@ for x in `seq 1 50`;do
     echo $x $y
     filename="results/bc_f${y}_n${x}.out"
     echo "$x" > $filename
-    ./gen_bc.py $x $y > tmp.rs
+    ./gen_bc.py $x $y > tmp.drs
-    ../main -z -c -v -B tmp.rs >&1  >> $filename 
+    ../main -z -c -v -B tmp.drs >&1  >> $filename 
     result="$(tail -1 $filename | sed "s/STAT/$x /")" 
     echo $result >> results/summary_bc_f${y}.out
     echo $result
@@ -13,4 +13,4 @@ for x in `seq 1 50`;do
 done
 done
 
-rm tmp.rs
+rm tmp.drs

reactics-bdd/in/scripts/benchmark_mutex.sh

@@ -4,8 +4,8 @@ for x in `seq 2 40`;do
     echo $x $y
     filename="results/mutex_f${y}_n${x}.out"
     echo "$x" > $filename
-    ./gen_mutex.py $x $y > tmp.rs
+    ./gen_mutex.py $x $y > tmp.drs
-    ../main -z -c -p -v -B tmp.rs >&1  >> $filename 
+    ../main -z -c -p -v -B tmp.drs >&1  >> $filename 
     result="$(tail -1 $filename | sed "s/STAT/$x /")" 
     echo $result >> results/summary_mutex_f${y}.out
     echo $result
@@ -13,4 +13,4 @@ for x in `seq 2 40`;do
 done
 done
 
-rm tmp.rs
+rm tmp.drs

reactics-bdd/in/scripts/benchmark_mutex_PT.sh

@@ -4,8 +4,8 @@ for x in `seq 2 40`;do
     echo $x $y
     filename="results/mutex_f${y}_n${x}_PT.out"
     echo "$x" > $filename
-    ./gen_mutex.py $x $y > tmp.rs
+    ./gen_mutex.py $x $y > tmp.drs
-    ../main -zcpxvB tmp.rs >&1  >> $filename 
+    ../main -zcpxvB tmp.drs >&1  >> $filename 
     result="$(tail -1 $filename | sed "s/STAT/$x /")" 
     echo $result >> results/summary_mutex_f${y}_PT.out
     echo $result
@@ -13,4 +13,4 @@ for x in `seq 2 40`;do
 done
 done
 
-rm tmp.rs
+rm tmp.drs

reactics-bdd/in/scripts/gen_abstract1.py

@@ -1,47 +0,0 @@
-#!/usr/bin/env python
-
-from sys import argv,exit
-
-if len(argv) < 3:
-    print "Usage:", argv[0], "<number of modules> <variant>"
-    exit(100)
-
-n = int(argv[1])
-v = int(argv[2])
-
-if not ( v > 0 and v < 3 ):
-    print "unsupported variant"
-    exit(100)
-
-print "reactions {"
-s = "\t{ {x},{s} -> {a1} };\n"
-print s
-
-for i in range(1,n+1):
-    s = "\t{ {a" + str(i) + "},{s} -> {y" + str(i) + "} };\n"
-    s += "\t{ {a" + str(i) + "},{s} -> {b" + str(i) + "} };\n"
-    s += "\t{ {b" + str(i) + "},{s} -> {c" + str(i) + "} };\n"
-    s += "\t{ {c" + str(i) + "},{s} -> {d" + str(i) + "} };\n"
-    s += "\t{ {d" + str(i) + ",y" + str(i) + "},{s} -> {a" + str(i+1) + "} };\n"
-    s += "\t{ {y" + str(i) + "},{s} -> {y" + str(i) + "} };\n"
-    print s
-
-s = "\t{ {a" + str(n+1) 
-for i in range(1,n+1):
-    s += ",y" + str(i)
-s += "},{s} -> {r} };\n"
-print s
-print "}"
-
-if v == 1:
-    print "context-entities { s }"
-elif v == 2:
-    s = "context-entities { s"
-    for i in range(1,n+1):
-        if i % 2 == 0:
-            s += ",a" + str(i)
-    s += " }"
-    print s
-
-print "initial-contexts { {x} }"
-print "rsctl-property { E[{}]F(r) }"

reactics-bdd/in/scripts/gen_asm.py

@@ -1,93 +0,0 @@
-#!/usr/bin/env python
-
-from sys import argv,exit
-
-OPTIONS_STR = """
-options { use-context-automaton; make-progressive; };
-"""
-
-PROC_STR = """
-    proc{:d} {{
-        {{{{a}}, {{s}} -> {{y}}}};
-        {{{{y}}, {{s}} -> {{y}}}};
-        {{{{a}}, {{s}} -> {{b}}}};
-        {{{{b}}, {{s}} -> {{c}}}};
-        {{{{c}}, {{s}} -> {{d}}}};
-        {{{{d,y}}, {{s}} -> {{dy}}}};
-    }};
-"""
-
-FINAL_PROC = """
-    procFinal {
-        {{done}, {s} -> {done}};
-    };
-"""
-
-CA_STR = """
-context-automaton {{
-    states {{ init, act }};
-    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(1, n+1):
-    out += PROC_STR.format(i)
-
-out += FINAL_PROC
-out += "};\n"
-
-transitions = ""
-
-init_trans = 8*" " + "{ proc1={a} }: init -> act;\n"
-transitions += init_trans
-
-for i in range(1, n+1):
-    transitions += "{:s}{{ proc{:d}={{}} }}: act -> act : ~proc{:d}.dy;\n".format(8*" ", i, i, i)
-
-for i in range(2, n+1):
-    transitions += "{:s}{{ proc{:d}={{a}} }}: act -> act : proc{:d}.dy;\n".format(8*" ", i, i-1)
-
-final_cond = "proc1.dy"
-for i in range(2, n+1):
-     final_cond += " AND proc{:d}.dy".format(i)
-
-transitions += "{:s}{{ procFinal={{done}} }}: act -> act : {:s};\n".format(8*" ", final_cond)
-
-out += CA_STR.format(transitions)
-
-# f1
-formula = "EF( procFinal.done )"
-out += PROPERTY_STR.format("f1",formula)
-
-# f2
-formula = "AG( proc{:d}.d IMPLIES K[proc{:d}]( proc{:d}.y ) )".format(n, n, n-1)
-out += PROPERTY_STR.format("f2",formula)
-
-# x1
-formula = "EF( ~procFinal.done )"
-out += PROPERTY_STR.format("x1",formula)
-
-print(out)
-

reactics-bdd/in/scripts/gen_bc.py

@@ -1,118 +0,0 @@
-#!/usr/bin/env python2.7
-
-from sys import argv,exit
-
-
-if len(argv) < 3:
-    print "Usage:", argv[0], "<number of bits> <property>"
-    exit(100)
-
-n = int(argv[1])
-property = int(argv[2])
-
-K = 8
-if property == 3:
-    if n < K+1:
-        print "too small n"
-        exit(100)
-
-if not ( property >= 1 and property < 5 ):
-    print "property: 1-4"
-    exit(101)
-
-print "reactions {"
-
-# (1) no dec, no inc
-print "\t# (1) no decrement, no increment"
-for j in range(0,n):
-    print "\t{{p" + str(j) + "},{dec,inc} -> {p" + str(j) + "}};"
-
-# (2) increment
-s = "\n\t# (2) increment operation\n"
-s += "\t{{inc},{dec,p0} -> {p0}};\n"
-for j in range(1,n):
-    s += "\t{{inc,"
-    for k in range(0,j):
-        s += "p" + str(k)
-        if k < j-1:
-            s += ","
-    s += "},{dec,p" + str(j) + "} -> {p" + str(j) + "}};\n"
-
-print s
-
-print "\t# the more significant bits remain (inc)"
-s = ""
-for j in range(0,n):
-    for k in range(j+1,n):
-        s += "\t{{inc,p" + str(k) + "},{dec,p" + str(j) + "} -> {p" + str(k) + "}};\n"
-
-print s
-
-print "\t# (3) decrement operation"
-s = ""
-for j in range(0,n):
-    s += "\t{{dec},{inc,"
-    for k in range(0,j+1):
-        s += "p" + str(k)
-        if k < j:
-            s += ","
-    s += "} -> {p" + str(j) + "}};\n"
-print s
-
-print "\t# the more significant bits remain (dec)"
-s = ""
-for j in range(0,n):
-    for k in range(j+1,n):
-        s += "\t{{dec,p" + str(j) + ",p" + str(k) + "},{inc} -> {p" + str(k) + "}};\n"
-
-s += "}\n"
-print s
-
-print "context-entities { inc,dec }"
-print "initial-contexts { {} }"
-
-if property == 4:
-    print "rsctl-property { AG( p" + str(n-1) + " IMPLIES EF ~p" + str(n-1) + " ) }"
-elif property == 1:
-    s = "rsctl-property { AG(("
-    for i in range(0,n):
-        s += "~p" + str(i)
-        if i < n-1:
-            s += " AND "
-    s += ") IMPLIES E[{inc},{dec}]F("
-    for i in range(0,n):
-        s += "p" + str(i)
-        if i < n-1:
-            s += " AND "
- 
-    s += ")) }"
-    print s
-elif property == 2:
-    s = "rsctl-property { AG(("
-    for i in range(0,n):
-        s += "p" + str(i)
-        if i < n-1:
-            s += " AND "
-    s += ") IMPLIES A[{inc}]X("
-    for i in range(0,n):
-        s += "~p" + str(i)
-        if i < n-1:
-            s += " AND "
- 
-    s += ")) }"
-    print s
-
-elif property == 3:
-    s = "rsctl-property { E[{inc}]F("
-    for i in range(0,n-K):
-        s += "p" + str(i)
-        if i < n-1:
-            s += " AND "
-    for i in range(n-K,n):
-        s += "~p" + str(i)
-        if i < n-1:
-            s += " AND "
-    s += ") }"
-    print s
-
-

reactics-bdd/in/scripts/gen_mutex.py

@@ -1,76 +0,0 @@
-#!/usr/bin/env python
-
-from sys import argv,exit
-
-
-if len(argv) < 3:
-    print "Usage:", argv[0], "<number of processes> <formula>"
-    exit(100)
-
-n = int(argv[1])
-f = int(argv[2])
-
-if not ( f>0 and f<4 ):
-    print "unsupported formula"
-    exit(100)
-
-print "reactions {"
-for i in range(0,n):
-    s = "\t{{out" + str(i) + ",act" + str(i) + "},{} -> {request" + str(i) + "}};\n"
-    s += "\t{{out" + str(i) + "},{act" + str(i) + "} -> {out" + str(i) + "}};\n"
-    for j in range(0,n):
-        if i != j:
-            s += "\t{{request" + str(i) + ",act" + str(i) + ",act" + str(j) + "},{} -> {request" + str(i) + "}};\n"
-    #s += "\t{{request" + str(i) + "},{"
-    #for j in range(0,n):
-    #    s += "act" + str(j)
-    #    if j < n-1:
-    #        s += ","
-    #s += "} -> {request" + str(i) + "}};\n"
-    s += "\t{{request" + str(i) + "},{act" + str(i) + "} -> {request" + str(i) + "}};\n"
-    s += "\t{{request" + str(i) + ",act" + str(i) + "},{"
-    for j in range(0,n):
-        if i != j:
-            s += "act" + str(j) + ","
-    s += "lock} -> {in" + str(i) + ",lock}};\n"
-    s += "\t{{in" + str(i) + ",act" + str(i) + "},{} -> {out" + str(i) + ",done}};\n"
-    s += "\t{{in" + str(i) + "},{act" + str(i) + "} -> {in" + str(i) + "}};\n"
-    print s
-
-print "\t{{lock},{done} -> {lock}};"
-
-print "}"
-
-s = "context-entities {"
-for i in range(0,n):
-    s += "act" + str(i)
-    if i < n-1:
-        s += ","
-s += "}\n"
-print s
-
-s = "initial-contexts { {"
-for i in range(0,n):
-    s += "out" + str(i)
-    if i < n-1:
-        s += ","
-s += "} }\n"
-print s
-
-#print "rsctl-property { A[{act1}]G(A[{act1}]F(in1)) }"
-if f == 1:
-    print "rsctl-property { A[{act1}]F(in1) }"
-elif f == 2:
-    print "rsctl-property { E[{act1}]F(in1) }"
-elif f == 3:
-    s = "rsctl-property { AG("
-    for i in range(0,n):
-        for j in range(i+1,n):
-            s += "~(in" + str(i) + " AND in" + str(j) + ")"
-            if i < n-2:
-                s += " AND "
-    s += ") }"
-    print s
-else:
-    exit(111)
-

reactics-bdd/in/scripts/gen_tgc_sc.py

@@ -1,117 +0,0 @@
-#!/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)
-

reactics-bdd/mc.cc

@@ -517,9 +517,9 @@ BDD ModelChecker::getIthOnly(Process proc_id)
   /* nothing has been found in the cache */
   BDD bdd = BDD_TRUE;
 
-  for (auto i = 0; i < pv_drs_E->size(); ++i) {
+  for (size_t i = 0; i < pv_drs_E->size(); ++i) {
 
-    if (i == proc_id) {
+    if (i == static_cast<size_t>(proc_id)) {
       continue;
     }
 
@@ -591,13 +591,7 @@ bool ModelChecker::checkRSCTLKfull(FormRSCTLK *form)
 
   VERB("Checking the formula");
 
-  //if (*initStates * getStatesRSCTLK(form) != cuddMgr->bddZero())
+  result = (*initStates * getStatesRSCTLK(form) == *initStates);
-  if (*initStates * getStatesRSCTLK(form) == *initStates) {
-    result = true;
-  }
-  else {
-    result = false;
-  }
 
   cleanup();
 

reactics-bdd/reactics.cc

@@ -37,13 +37,13 @@ int main(int argc, char **argv)
                           &option_index)) != -1) {
     switch (c) {
       case 0:
-        printf("option %s", long_options[option_index].name);
+        cout << "option " << long_options[option_index].name;
 
         if (optarg) {
-          printf(" with arg %s", optarg);
+          cout << " with arg " << optarg;
         }
 
-        printf("\n");
+        cout << endl;
 
         if (strcmp(long_options[option_index].name, "trace-parsing")) {
           driver.trace_parsing = true;
@@ -236,16 +236,7 @@ int main(int argc, char **argv)
 
   delete opts;
 
-  int ret_val;
+  return result ? 0 : 1;
-
-  if (result) {
-    ret_val = 0;
-  }
-  else {
-    ret_val = 1;
-  }
-
-  return ret_val;
 }
 
 void print_help(std::string path_str)

reactics-bdd/rs.cc

@@ -14,12 +14,7 @@ RctSys::RctSys(void)
 
 bool RctSys::hasEntity(std::string name)
 {
-  if (entities_names.find(name) == entities_names.end()) {
+  return entities_names.find(name) != entities_names.end();
-    return false;
-  }
-  else {
-    return true;
-  }
 }
 
 void RctSys::addEntity(std::string name)
@@ -84,21 +79,12 @@ void RctSys::addProcess(std::string processName)
 
 bool RctSys::hasProcess(std::string processName)
 {
-  if (processes_names.find(processName) == processes_names.end()) {
+  return processes_names.find(processName) != processes_names.end();
-    return false;
-  }
-  else {
-    return true;
-  }
 }
 
 bool RctSys::hasProcess(Process processID)
 {
-  if (processID >= processes_ids.size()) {
+  return processID < processes_ids.size();
-    return false;
-  }
-
-  return true;
 }
 
 Process RctSys::getProcessID(std::string processName)
@@ -120,28 +106,26 @@ std::string RctSys::getProcessName(Process processID)
   }
 }
 
-void RctSys::pushReactant(std::string entityName)
+void RctSys::ensureEntity(std::string entityName)
 {
   if (!hasEntity(entityName)) {
     addEntity(entityName);
   }
+}
 
+void RctSys::pushReactant(std::string entityName)
+{
+  ensureEntity(entityName);
   tmpReactants.insert(getEntityID(entityName));
 }
 void RctSys::pushInhibitor(std::string entityName)
 {
-  if (!hasEntity(entityName)) {
+  ensureEntity(entityName);
-    addEntity(entityName);
-  }
-
   tmpInhibitors.insert(getEntityID(entityName));
 }
 void RctSys::pushProduct(std::string entityName)
 {
-  if (!hasEntity(entityName)) {
+  ensureEntity(entityName);
-    addEntity(entityName);
-  }
-
   tmpProducts.insert(getEntityID(entityName));
 }
 
@@ -232,10 +216,7 @@ void RctSys::commitInitState(void)
 
 void RctSys::addActionEntity(std::string entityName)
 {
-  if (!hasEntity(entityName)) {
+  ensureEntity(entityName);
-    addEntity(entityName);
-  }
-
   actionEntities.insert(getEntityID(entityName));
 }
 
@@ -248,12 +229,7 @@ void RctSys::addActionEntity(Entity entity)
 
 bool RctSys::isActionEntity(Entity entity)
 {
-  if (actionEntities.count(entity) > 0) {
+  return actionEntities.count(entity) > 0;
-    return true;
-  }
-  else {
-    return false;
-  }
 }
 
 void RctSys::showActionEntities(void)

reactics-bdd/rs.hh

@@ -50,6 +50,7 @@ class RctSys
 
     void addReactionForCurrentProcess(Reaction reaction);
 
+    void ensureEntity(std::string entityName);
     void pushReactant(std::string entityName);
     void pushInhibitor(std::string entityName);
     void pushProduct(std::string entityName);

reactics-bdd/symrs.cc

@@ -17,9 +17,6 @@ SymRS::SymRS(RctSys *rs, Options *opts)
 
   totalEntities = rs->getEntitiesSize();
 
-  // TODO: remove
-  totalActions = 0;
-
   totalRctSysStateVars = getTotalProductVariables();
   totalCtxEntities = getTotalCtxEntitiesVariables();
 
@@ -404,39 +401,19 @@ BDD SymRS::encCtxEntity(Process proc_id, Entity entity) const
 
 bool SymRS::productEntityExists(Process proc_id, Entity entity) const
 {
-  if (prod_ent_local_idx.count(proc_id) == 0) {
+  return prod_ent_local_idx.count(proc_id) != 0 &&
-    return false;
+         prod_ent_local_idx.at(proc_id).count(entity) == 1;
-  }
-  else {
-    if (prod_ent_local_idx.at(proc_id).count(entity) == 1) {
-      return true;
-    }
-  }
-
-  return false;
 }
 
 bool SymRS::ctxEntityExists(Process proc_id, Entity entity) const
 {
-  if (ctx_ent_local_idx.count(proc_id) == 0) {
+  return ctx_ent_local_idx.count(proc_id) != 0 &&
-    return false;
+         ctx_ent_local_idx.at(proc_id).count(entity) == 1;
-  }
-  else {
-    if (ctx_ent_local_idx.at(proc_id).count(entity) == 1) {
-      return true;
-    }
-  }
-
-  return false;
 }
 
 bool SymRS::processUsesEntity(Process proc_id, Entity entity_id) const
 {
-  if (productEntityExists(proc_id, entity_id) || ctxEntityExists(proc_id, entity_id)) {
+  return productEntityExists(proc_id, entity_id) || ctxEntityExists(proc_id, entity_id);
-    return true;
-  }
-
-  return false;
 }
 
 BDD SymRS::encEntitiesConj_raw(Process proc_id, const Entities &entities, bool succ)
@@ -511,20 +488,6 @@ BDD SymRS::encContext(const EntitiesForProc &proc_entities)
   return r;
 }
 
-BDD SymRS::compState(const BDD &state) const
-{
-  assert(0);
-  BDD s = state;
-
-  for (unsigned int i = 0; i < totalRctSysStateVars; ++i) {
-    if (!(*pv)[i] * state != cuddMgr->bddZero()) {
-      s *= !(*pv)[i];
-    }
-  }
-
-  return s;
-}
-
 BDD SymRS::compContext(const BDD &context) const
 {
   BDD c = context;
@@ -725,65 +688,6 @@ BDD SymRS::encEnabledness(Process prod_proc_id, Entity entity_id)
   return enab;
 }
 
-// BDD SymRS::encEnabledness(Process prod_proc_id, Entity entity_id)
-// {
-//   assert(prod_conds.size() > prod_proc_id);
-
-//   BDD enab = BDD_FALSE;
-
-//   auto production_conditions = prod_conds[prod_proc_id][entity_id];
-
-//   VERB_LN(5, "| Produce " << rs->getEntityName(entity_id) << " in " << rs->getProcessName(prod_proc_id) << ":");
-
-//   for (const auto &cond : production_conditions) {
-
-//     BDD reactants = BDD_TRUE;
-//     BDD inhibitors = BDD_TRUE;
-
-//     for (const auto &reactant : cond.rctt) {
-//       BDD proc_reactants = BDD_FALSE;
-
-//       for (unsigned int proc_id = 0; proc_id < numberOfProc; ++proc_id) {
-//         if (processUsesEntity(proc_id, reactant)) {
-//           proc_reactants += encProcEnabled(proc_id) * encEntityCondition(proc_id, reactant);
-
-//           VERB_LN(5, "| - if process " << rs->getProcessName(proc_id) << " is enabled and has " << rs->getEntityName(reactant));
-
-//         }
-//       } // END FOR: prod_id
-
-//       reactants *= proc_reactants;
-//     } // END FOR: reactant
-
-//     // For inhibitors, we take all the processes first and then we iterate over the inhibitors
-//     for (unsigned int proc_id = 0; proc_id < numberOfProc; ++proc_id) {
-//       BDD proc_inhibitors = BDD_TRUE;
-
-//       for (const auto &inhibitor : cond.inhib) {
-//         if (processUsesEntity(proc_id, inhibitor)) {
-//           proc_inhibitors *= !encEntityCondition(proc_id, inhibitor);
-//         }
-//       }
-
-//       if (proc_inhibitors != BDD_TRUE) { // just an optimisation
-//         proc_inhibitors += !encProcEnabled(proc_id);
-//         inhibitors *= proc_inhibitors;
-//       }
-//     }
-
-//     enab += reactants * inhibitors;
-
-//   } // END FOR: cond
-
-//   if (opts->reorder_trans) {
-//     VERB_L2("Reordering");
-//     Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
-//   }
-
-//   return enab;
-// }
-
-
 BDD SymRS::encEntitySameSuccessor(Process proc_id, Entity entity_id)
 {
   return BDD_IFF(encEntity(proc_id, entity_id), encEntitySucc(proc_id, entity_id));
@@ -810,7 +714,7 @@ void SymRS::encodeTransitions(void)
 
   prod_conds.resize(numberOfProc);
 
-  for (auto proc_id = 0; proc_id < numberOfProc; ++proc_id) {
+  for (unsigned int proc_id = 0; proc_id < numberOfProc; ++proc_id) {
     prod_conds[proc_id] = getProductionConditions(proc_id);
   }
 

reactics-bdd/symrs.hh

@@ -15,7 +15,6 @@
 #include "types.hh"
 #include "macro.hh"
 #include "bdd_macro.hh"
-// #include "rs.hh"
 #include "options.hh"
 #include "memtime.hh"
 
@@ -240,16 +239,11 @@ class SymRS
     vector<BDDvec> *pv_proc_ctx;
     BDDvec *pv_proc_ctx_E;
 
-    // TODO: remove
-    BDDvec *pv_act;
-    BDD *pv_act_E;
-
     unsigned int totalEntities;
     unsigned int numberOfProc;         /*!< The number of DRS processes */
     unsigned int totalStateVars;
     unsigned int totalRctSysStateVars; /*!< Total number of different entities produced by reactions */
     unsigned int totalCtxEntities;     /*!< Total number of different (process,context) entities used */
-    unsigned int totalActions;
     unsigned int totalCtxAutStateVars;
 
     EntitiesForProc usedProducts;     /*!< Entities used in products (per process) */
@@ -309,13 +303,6 @@ class SymRS
 
     BDD encContext(const EntitiesForProc &proc_entities);
 
-    /**
-     * @brief Complements an encoding of a given state by negating all the variables that are not set to true
-     *
-     * @return Returns the encoded state
-     */
-    BDD compState(const BDD &state) const;
-
     BDD compContext(const BDD &context) const;
 
     std::string decodedRctSysStateToStr(const BDD &state);

reactics-smt/rs/context_automaton.py

@@ -55,10 +55,7 @@ class ContextAutomaton(object):
         return self._states[self._init_state]
 
     def is_state(self, name):
-        if name in self._states:
+        return name in self._states
-            return True
-        else:
-            return False
 
     def get_state_id(self, name):
         try:
@@ -78,10 +75,7 @@ class ContextAutomaton(object):
             print(state)
 
     def is_valid_rs_set(self, elements):
-        if set(elements).issubset(self._reaction_system.background_set):
+        return set(elements).issubset(self._reaction_system.background_set)
-            return True
-        else:
-            return False
 
     def is_valid_context(self, context):
         return self.is_valid_rs_set(context)
@@ -95,7 +89,7 @@ class ContextAutomaton(object):
         return new_set
 
     def add_transition(self, src, context_set, dst):
-        if not type(context_set) is set and not type(context_set) is list:
+        if not isinstance(context_set, (set, list)):
             print("Contexts set must be of type set or list")
 
         if not self.is_valid_context(context_set):

reactics-smt/rs/context_automaton_with_concentrations.py

@@ -9,12 +9,9 @@ class ContextAutomatonWithConcentrations(ContextAutomaton):
         super(ContextAutomatonWithConcentrations, self).__init__(reaction_system)
 
     def is_valid_context(self, context):
-        if set([e for e, lvl in context]).issubset(
+        return set(e for e, lvl in context).issubset(
             self._reaction_system.background_set
-        ):
+        )
-            return True
-        else:
-            return False
 
     def context2str(self, ctx):
         if len(ctx) == 0:
@@ -26,7 +23,7 @@ class ContextAutomatonWithConcentrations(ContextAutomaton):
         return s
 
     def add_transition(self, src, context_set, dst):
-        if not type(context_set) is set and not type(context_set) is list:
+        if not isinstance(context_set, (set, list)):
             print("Contexts set must be of type set or list")
 
         if not self.is_valid_context(context_set):

reactics-smt/rs/extended_context_automaton.py

@@ -70,7 +70,7 @@ class ExtendedContextAutomaton(ContextAutomaton):
 
         ctx_reactants, ctx_inhibitors, ctx_products = ctx_reaction
 
-        if not type(ctx_products) is set and not type(ctx_products) is list:
+        if not isinstance(ctx_products, (set, list)):
             print("Contexts set (context products) must be of type set or list")
 
         if not self.is_valid_rs_set(ctx_reactants):

reactics-smt/rs/reaction_system.py

@@ -43,11 +43,8 @@ class ReactionSystem(object):
             self.add_bg_set_entity(e)
 
     def is_in_background_set(self, entity):
-        """Checks if the given name is valid wrt the background set="""
+        """Checks if the given name is valid wrt the background set"""
-        if entity in self.background_set:
+        return entity in self.background_set
-            return True
-        else:
-            return False
 
     def get_entity_id(self, name):
         try:

reactics-smt/rs/reaction_system_with_concentrations.py

@@ -18,9 +18,9 @@ class ReactionSystemWithConcentrations(ReactionSystem):
     def add_bg_set_entity(self, e):
         name = ""
         def_max_conc = -1
-        if type(e) is tuple and len(e) == 2:
+        if isinstance(e, tuple) and len(e) == 2:
             name, def_max_conc = e
-        elif type(e) is str:
+        elif isinstance(e, str):
             name = e
             print("\nWARNING: no maximal concentration level specified for:", e, "\n")
         else:
@@ -46,18 +46,10 @@ class ReactionSystemWithConcentrations(ReactionSystem):
     def is_valid_entity_with_concentration(self, e):
         """Sanity check for entities with concentration"""
 
-        if type(e) is tuple:
+        if isinstance(e, (tuple, list)) and len(e) == 2 and isinstance(e[1], int):
-            if len(e) == 2 and type(e[1]) is int:
+            return True
-                return True
 
-        if type(e) is list:
+        raise RuntimeError("Invalid entity+concentration: " + repr(e))
-            if len(e) == 2 and type(e[1]) is int:
-                return True
-
-        print("FATAL. Invalid entity+concentration: {:s}".format(e))
-        exit(1)
-
-        return False
 
     def get_state_ids(self, state):
         """Returns entities of the given state without levels"""
@@ -415,33 +407,4 @@ class ReactionSystemWithConcentrations(ReactionSystem):
         return rs
 
 
-class ReactionSystemWithAutomaton(object):
-    def __init__(self, reaction_system, context_automaton):
-        self.rs = reaction_system
-        self.ca = context_automaton
-
-    def show(self, soft=False):
-        self.rs.show(soft)
-        self.ca.show()
-
-    def is_with_concentrations(self):
-        if not isinstance(self.rs, ReactionSystemWithConcentrations):
-            return False
-        if not isinstance(self.ca, ContextAutomatonWithConcentrations):
-            return False
-        return True
-
-    def sanity_check(self):
-        pass
-
-    def get_ordinary_reaction_system_with_automaton(self):
-        if not self.is_with_concentrations():
-            raise RuntimeError("Not RS/CA with concentrations")
-
-        ors = self.rs.get_reaction_system()
-        oca = self.ca.get_automaton_with_flat_contexts(ors)
-
-        return ReactionSystemWithAutomaton(ors, oca)
-
-
 # EOF

reactics-smt/rs/reaction_system_with_concentrations_param.py

@@ -34,9 +34,9 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
     def add_bg_set_entity(self, e):
         name = ""
         def_max_conc = -1
-        if type(e) is tuple and len(e) == 2:
+        if isinstance(e, tuple) and len(e) == 2:
             name, def_max_conc = e
-        elif type(e) is str:
+        elif isinstance(e, str):
             name = e
             print("\nWARNING: no maximal concentration level specified for:", e, "\n")
         else:
@@ -80,18 +80,10 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
     def is_valid_entity_with_concentration(self, e):
         """Sanity check for entities with concentration"""
 
-        if type(e) is tuple:
+        if isinstance(e, (tuple, list)) and len(e) == 2 and isinstance(e[1], int):
-            if len(e) == 2 and type(e[1]) is int:
+            return True
-                return True
 
-        if type(e) is list:
+        raise RuntimeError("Invalid entity+concentration: " + repr(e))
-            if len(e) == 2 and type(e[1]) is int:
-                return True
-
-        print("FATAL. Invalid entity+concentration: {:s}".format(e))
-        exit(1)
-
-        return False
 
     def is_valid_concentration_for_entity(self, entity, level):
         """Checks the concentration level for entity"""

reactics-smt/rs_testing.py

@@ -1,12 +1,10 @@
 from rs import *
 from smt import *
-import rs_examples 
 from logics import *
 from rsltl_shortcuts import *
 
 from itertools import chain, combinations
 
-import sys
 import resource
 
 def powerset(iterable,N=None):

reactics-smt/rssmt.py

@@ -11,7 +11,6 @@ import argparse
 from rs import *
 from smt import *
 import sys
-import rs_examples
 import rs_testing
 
 from colour import *

reactics-smt/smt/__init__.py

@@ -1,4 +1,3 @@
-# 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

@@ -267,7 +267,7 @@ class SmtCheckerRS(object):
     ):
         """Main testing function"""
 
-        if not type(state) is tuple:
+        if not isinstance(state, tuple):
             state = (state, [])
 
         if print_time:

reactics-smt/smt/smt_checker_rsc.py

@@ -11,9 +11,6 @@ from colour import *
 
 from logics import rsLTL_Encoder
 
-# def simplify(x):
-#     return x
-
 
 class SmtCheckerRSC(object):
     def __init__(self, rsca):

reactics-smt/smt/smt_checker_rsc_param.py

@@ -14,9 +14,6 @@ from logics import ParamConstr_Encoder
 
 from rs.reaction_system_with_concentrations_param import ParameterObj, is_param
 
-# def simplify(x):
-#     return x
-
 
 def z3_max(a, b):
     return If(a > b, a, b)

run_tests.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+# Run all ReactICS tests (BDD, SMT, generators)
+exec bash "$(dirname "$0")/tests/run_all_tests.sh" "$@"

tests/expected/tgc4_mc.txt

@@ -0,0 +1,8 @@
+Using BDD-based Bounded Model Checking
+Formula (((EF(E< proc0.allowed >X(proc0.in)) AND EF(E< proc1.allowed >X(proc1.in))) AND EF(E< proc2.allowed >X(proc2.in))) AND EF(E< proc3.allowed >X(proc3.in))) holds
+Using BDD-based Bounded Model Checking
+Formula EF((((proc0.approach AND proc1.approach) AND proc2.approach) AND proc3.approach)) holds
+Using BDD-based Bounded Model Checking
+Formula AG((proc0.in IMPLIES K[proc0](((~proc1.in AND ~proc2.in) AND ~proc3.in)))) holds
+Using BDD-based Bounded Model Checking
+Formula AG((proc0.in IMPLIES C[proc0 proc1 proc2 proc3](((~proc1.in AND ~proc2.in) AND ~proc3.in)))) holds

tests/expected/tgc4_print.txt

@@ -0,0 +1,58 @@
+# Context entities: out allowed
+# Reactions:
+
+  . proc = "proc0":
+     * (R={ out },I={ },P={ approach })
+     * (R={ approach },I={ req },P={ req })
+     * (R={ allowed },I={ },P={ in })
+     * (R={ in },I={ },P={ out leave })
+     * (R={ req },I={ in },P={ req })
+
+  . proc = "proc1":
+     * (R={ out },I={ },P={ approach })
+     * (R={ approach },I={ req },P={ req })
+     * (R={ allowed },I={ },P={ in })
+     * (R={ in },I={ },P={ out leave })
+     * (R={ req },I={ in },P={ req })
+
+  . proc = "proc2":
+     * (R={ out },I={ },P={ approach })
+     * (R={ approach },I={ req },P={ req })
+     * (R={ allowed },I={ },P={ in })
+     * (R={ in },I={ },P={ out leave })
+     * (R={ req },I={ in },P={ req })
+
+  . proc = "proc3":
+     * (R={ out },I={ },P={ approach })
+     * (R={ approach },I={ req },P={ req })
+     * (R={ allowed },I={ },P={ in })
+     * (R={ in },I={ },P={ out leave })
+     * (R={ req },I={ in },P={ req })
+
+# Context Automaton States:
+ = Init state: init
+ * init
+ * green
+ * red
+ * T
+# Context Automaton Transitions:
+ * [init -> green]: { proc0={ out } proc1={ out } proc2={ out } proc3={ out } }
+ * [green -> red]: { proc0={ allowed } } proc0.req
+ * [green -> red]: { proc1={ allowed } } proc1.req
+ * [green -> red]: { proc2={ allowed } } proc2.req
+ * [green -> red]: { proc3={ allowed } } proc3.req
+ * [green -> green]: { proc0={ } } (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)
+ * [green -> green]: { proc1={ } } (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)
+ * [green -> green]: { proc2={ } } (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)
+ * [green -> green]: { proc3={ } } (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)
+ * [red -> green]: { proc0={ } } proc0.leave
+ * [red -> green]: { proc1={ } } proc1.leave
+ * [red -> green]: { proc2={ } } proc2.leave
+ * [red -> green]: { proc3={ } } proc3.leave
+ * [red -> red]: { proc0={ } } (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)
+ * [red -> red]: { proc1={ } } (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)
+ * [red -> red]: { proc2={ } } (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)
+ * [red -> red]: { proc3={ } } (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)
+ * [green -> T]: { } ~((((((((true OR proc0.req) OR proc1.req) OR proc2.req) OR proc3.req) OR (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)) OR (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)) OR (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)) OR (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req))
+ * [red -> T]: { } ~((((((((true OR proc0.leave) OR proc1.leave) OR proc2.leave) OR proc3.leave) OR (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)) OR (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)) OR (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)) OR (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave))
+ * [T -> T]: { }

tests/expected/tgc4_states.txt

@@ -0,0 +1,80 @@
+{ proc0={ req } proc1={ approach } proc2={ req } proc3={ out leave } }
+{ proc0={ req } proc1={ req } proc2={ approach } proc3={ out leave } }
+{ proc0={ req } proc1={ req } proc2={ req } proc3={ out leave } }
+{ proc0={ approach } proc1={ approach } proc2={ req } proc3={ out leave } }
+{ proc0={ approach } proc1={ req } proc2={ req } proc3={ out leave } }
+{ proc0={ approach } proc1={ approach } proc2={ req in } proc3={ approach } }
+{ proc0={ approach } proc1={ req } proc2={ out leave } proc3={ req } }
+{ proc0={ approach } proc1={ req } proc2={ req in } proc3={ approach } }
+{ proc0={ req } proc1={ approach } proc2={ approach } proc3={ out leave } }
+{ proc0={ approach } proc1={ approach } proc2={ approach } proc3={ out leave } }
+{ proc0={ req } proc1={ approach } proc2={ req in } proc3={ req } }
+{ proc0={ approach } proc1={ req } proc2={ approach } proc3={ out leave } }
+{ proc0={ req } proc1={ approach } proc2={ req } proc3={ req in } }
+{ proc0={ approach } proc1={ req } proc2={ req in } proc3={ req } }
+{ proc0={ req } proc1={ approach } proc2={ out leave } proc3={ approach } }
+{ proc0={ req in } proc1={ approach } proc2={ req } proc3={ req } }
+{ proc0={ approach } proc1={ approach } proc2={ approach } proc3={ req in } }
+{ proc0={ req } proc1={ req } proc2={ out leave } proc3={ req } }
+{ proc0={ req } proc1={ approach } proc2={ out leave } proc3={ req } }
+{ proc0={ req } proc1={ req } proc2={ req in } proc3={ approach } }
+{ proc0={ approach } proc1={ approach } proc2={ out leave } proc3={ req } }
+{ proc0={ req } proc1={ req } proc2={ req in } proc3={ req } }
+{ proc0={ req } proc1={ approach } proc2={ req in } proc3={ approach } }
+{ proc0={ approach } proc1={ req } proc2={ out leave } proc3={ approach } }
+{ proc0={ req } proc1={ req } proc2={ out leave } proc3={ approach } }
+{ proc0={ } proc1={ } proc2={ } proc3={ } }
+{ proc0={ approach } proc1={ approach } proc2={ out leave } proc3={ approach } }
+{ proc0={ approach } proc1={ approach } proc2={ req in } proc3={ req } }
+{ proc0={ req } proc1={ approach } proc2={ approach } proc3={ req in } }
+{ proc0={ req in } proc1={ req } proc2={ approach } proc3={ req } }
+{ proc0={ req in } proc1={ approach } proc2={ approach } proc3={ approach } }
+{ proc0={ req } proc1={ req in } proc2={ req } proc3={ req } }
+{ proc0={ req in } proc1={ req } proc2={ approach } proc3={ approach } }
+{ proc0={ req } proc1={ req } proc2={ req } proc3={ req in } }
+{ proc0={ approach } proc1={ req } proc2={ req } proc3={ req in } }
+{ proc0={ approach } proc1={ approach } proc2={ req } proc3={ req in } }
+{ proc0={ out leave } proc1={ req } proc2={ approach } proc3={ approach } }
+{ proc0={ req in } proc1={ req } proc2={ req } proc3={ req } }
+{ proc0={ out leave } proc1={ req } proc2={ req } proc3={ approach } }
+{ proc0={ req } proc1={ req } proc2={ approach } proc3={ req in } }
+{ proc0={ req in } proc1={ approach } proc2={ approach } proc3={ req } }
+{ proc0={ req } proc1={ approach } proc2={ approach } proc3={ req } }
+{ proc0={ req in } proc1={ approach } proc2={ req } proc3={ approach } }
+{ proc0={ out leave } proc1={ approach } proc2={ req } proc3={ req } }
+{ proc0={ approach } proc1={ req } proc2={ approach } proc3={ req in } }
+{ proc0={ out leave } proc1={ req } proc2={ approach } proc3={ req } }
+{ proc0={ req } proc1={ out leave } proc2={ req } proc3={ req } }
+{ proc0={ req } proc1={ approach } proc2={ req } proc3={ req } }
+{ proc0={ out leave } proc1={ req } proc2={ req } proc3={ req } }
+{ proc0={ approach } proc1={ req in } proc2={ approach } proc3={ approach } }
+{ proc0={ out leave } proc1={ approach } proc2={ approach } proc3={ approach } }
+{ proc0={ approach } proc1={ approach } proc2={ approach } proc3={ approach } }
+{ proc0={ approach } proc1={ req } proc2={ req } proc3={ req } }
+{ proc0={ approach } proc1={ out leave } proc2={ approach } proc3={ approach } }
+{ proc0={ approach } proc1={ req } proc2={ approach } proc3={ approach } }
+{ proc0={ approach } proc1={ out leave } proc2={ req } proc3={ req } }
+{ proc0={ req } proc1={ out leave } proc2={ approach } proc3={ req } }
+{ proc0={ approach } proc1={ out leave } proc2={ approach } proc3={ req } }
+{ proc0={ approach } proc1={ req in } proc2={ req } proc3={ req } }
+{ proc0={ out leave } proc1={ approach } proc2={ req } proc3={ approach } }
+{ proc0={ approach } proc1={ approach } proc2={ req } proc3={ req } }
+{ proc0={ out leave } proc1={ approach } proc2={ approach } proc3={ req } }
+{ proc0={ req in } proc1={ req } proc2={ req } proc3={ approach } }
+{ proc0={ approach } proc1={ approach } proc2={ approach } proc3={ req } }
+{ proc0={ req } proc1={ req } proc2={ approach } proc3={ req } }
+{ proc0={ approach } proc1={ req } proc2={ req } proc3={ approach } }
+{ proc0={ req } proc1={ approach } proc2={ approach } proc3={ approach } }
+{ proc0={ approach } proc1={ req in } proc2={ approach } proc3={ req } }
+{ proc0={ approach } proc1={ approach } proc2={ req } proc3={ approach } }
+{ proc0={ approach } proc1={ req in } proc2={ req } proc3={ approach } }
+{ proc0={ req } proc1={ approach } proc2={ req } proc3={ approach } }
+{ proc0={ req } proc1={ req in } proc2={ approach } proc3={ req } }
+{ proc0={ approach } proc1={ req } proc2={ approach } proc3={ req } }
+{ proc0={ req } proc1={ req in } proc2={ approach } proc3={ approach } }
+{ proc0={ req } proc1={ out leave } proc2={ approach } proc3={ approach } }
+{ proc0={ req } proc1={ req } proc2={ approach } proc3={ approach } }
+{ proc0={ approach } proc1={ out leave } proc2={ req } proc3={ approach } }
+{ proc0={ req } proc1={ out leave } proc2={ req } proc3={ approach } }
+{ proc0={ req } proc1={ req in } proc2={ req } proc3={ approach } }
+{ proc0={ req } proc1={ req } proc2={ req } proc3={ approach } }

tests/expected/tgc_mc.txt

@@ -0,0 +1,8 @@
+Using BDD-based Bounded Model Checking
+Formula ((EF(E< proc0.allowed >X(proc0.in)) AND EF(E< proc1.allowed >X(proc1.in))) AND EF(E< proc2.allowed >X(proc2.in))) holds
+Using BDD-based Bounded Model Checking
+Formula EF(((proc0.approach AND proc1.approach) AND proc2.approach)) holds
+Using BDD-based Bounded Model Checking
+Formula AG((proc0.in IMPLIES K[proc0]((~proc1.in AND ~proc2.in)))) holds
+Using BDD-based Bounded Model Checking
+Formula AG((proc0.in IMPLIES C[proc0 proc1 proc2]((~proc1.in AND ~proc2.in)))) holds

tests/expected/tgc_print.txt

@@ -0,0 +1,47 @@
+# Context entities: out allowed
+# Reactions:
+
+  . proc = "proc0":
+     * (R={ out },I={ },P={ approach })
+     * (R={ approach },I={ req },P={ req })
+     * (R={ allowed },I={ },P={ in })
+     * (R={ in },I={ },P={ out leave })
+     * (R={ req },I={ in },P={ req })
+
+  . proc = "proc1":
+     * (R={ out },I={ },P={ approach })
+     * (R={ approach },I={ req },P={ req })
+     * (R={ allowed },I={ },P={ in })
+     * (R={ in },I={ },P={ out leave })
+     * (R={ req },I={ in },P={ req })
+
+  . proc = "proc2":
+     * (R={ out },I={ },P={ approach })
+     * (R={ approach },I={ req },P={ req })
+     * (R={ allowed },I={ },P={ in })
+     * (R={ in },I={ },P={ out leave })
+     * (R={ req },I={ in },P={ req })
+
+# Context Automaton States:
+ = Init state: init
+ * init
+ * green
+ * red
+ * T
+# Context Automaton Transitions:
+ * [init -> green]: { proc0={ out } proc1={ out } proc2={ out } }
+ * [green -> red]: { proc0={ allowed } } proc0.req
+ * [green -> red]: { proc1={ allowed } } proc1.req
+ * [green -> red]: { proc2={ allowed } } proc2.req
+ * [green -> green]: { proc0={ } } ((~proc0.req AND ~proc1.req) AND ~proc2.req)
+ * [green -> green]: { proc1={ } } ((~proc0.req AND ~proc1.req) AND ~proc2.req)
+ * [green -> green]: { proc2={ } } ((~proc0.req AND ~proc1.req) AND ~proc2.req)
+ * [red -> green]: { proc0={ } } proc0.leave
+ * [red -> green]: { proc1={ } } proc1.leave
+ * [red -> green]: { proc2={ } } proc2.leave
+ * [red -> red]: { proc0={ } } ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave)
+ * [red -> red]: { proc1={ } } ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave)
+ * [red -> red]: { proc2={ } } ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave)
+ * [green -> T]: { } ~((((((true OR proc0.req) OR proc1.req) OR proc2.req) OR ((~proc0.req AND ~proc1.req) AND ~proc2.req)) OR ((~proc0.req AND ~proc1.req) AND ~proc2.req)) OR ((~proc0.req AND ~proc1.req) AND ~proc2.req))
+ * [red -> T]: { } ~((((((true OR proc0.leave) OR proc1.leave) OR proc2.leave) OR ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave)) OR ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave)) OR ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave))
+ * [T -> T]: { }

tests/expected/tgc_reactions.txt

@@ -0,0 +1,23 @@
+# Reactions:
+
+  . proc = "proc0":
+     * (R={ out },I={ },P={ approach })
+     * (R={ approach },I={ req },P={ req })
+     * (R={ allowed },I={ },P={ in })
+     * (R={ in },I={ },P={ out leave })
+     * (R={ req },I={ in },P={ req })
+
+  . proc = "proc1":
+     * (R={ out },I={ },P={ approach })
+     * (R={ approach },I={ req },P={ req })
+     * (R={ allowed },I={ },P={ in })
+     * (R={ in },I={ },P={ out leave })
+     * (R={ req },I={ in },P={ req })
+
+  . proc = "proc2":
+     * (R={ out },I={ },P={ approach })
+     * (R={ approach },I={ req },P={ req })
+     * (R={ allowed },I={ },P={ in })
+     * (R={ in },I={ },P={ out leave })
+     * (R={ req },I={ in },P={ req })
+

tests/expected/tgc_states.txt

@@ -0,0 +1,32 @@
+{ proc0={ req in } proc1={ req } proc2={ req } }
+{ proc0={ req in } proc1={ req } proc2={ approach } }
+{ proc0={ req } proc1={ req in } proc2={ approach } }
+{ proc0={ req in } proc1={ approach } proc2={ req } }
+{ proc0={ req in } proc1={ approach } proc2={ approach } }
+{ proc0={ req } proc1={ req in } proc2={ req } }
+{ proc0={ approach } proc1={ req in } proc2={ approach } }
+{ proc0={ approach } proc1={ approach } proc2={ req in } }
+{ proc0={ approach } proc1={ req in } proc2={ req } }
+{ proc0={ approach } proc1={ out leave } proc2={ req } }
+{ proc0={ req } proc1={ approach } proc2={ out leave } }
+{ proc0={ req } proc1={ req } proc2={ req in } }
+{ proc0={ approach } proc1={ req } proc2={ req } }
+{ proc0={ approach } proc1={ req } proc2={ req in } }
+{ proc0={ out leave } proc1={ req } proc2={ req } }
+{ proc0={ req } proc1={ approach } proc2={ req in } }
+{ proc0={ req } proc1={ out leave } proc2={ approach } }
+{ proc0={ approach } proc1={ out leave } proc2={ approach } }
+{ proc0={ req } proc1={ req } proc2={ out leave } }
+{ proc0={ req } proc1={ out leave } proc2={ req } }
+{ proc0={ } proc1={ } proc2={ } }
+{ proc0={ req } proc1={ approach } proc2={ req } }
+{ proc0={ out leave } proc1={ req } proc2={ approach } }
+{ proc0={ approach } proc1={ req } proc2={ out leave } }
+{ proc0={ approach } proc1={ approach } proc2={ req } }
+{ proc0={ req } proc1={ req } proc2={ approach } }
+{ proc0={ out leave } proc1={ approach } proc2={ req } }
+{ proc0={ approach } proc1={ req } proc2={ approach } }
+{ proc0={ approach } proc1={ approach } proc2={ approach } }
+{ proc0={ approach } proc1={ approach } proc2={ out leave } }
+{ proc0={ out leave } proc1={ approach } proc2={ approach } }
+{ proc0={ req } proc1={ approach } proc2={ approach } }

tests/expected/trivial_print.txt

@@ -0,0 +1,17 @@
+# Context entities: e1 e4
+# Reactions:
+
+  . proc = "m":
+     * (R={ e1 e4 },I={ e2 },P={ e1 e2 })
+     * (R={ e2 },I={ e4 },P={ e1 e4 e3 })
+     * (R={ e1 e3 },I={ e2 },P={ e1 e2 })
+     * (R={ e3 },I={ e2 },P={ e1 })
+
+# Context Automaton States:
+ = Init state: s0
+ * s0
+ * s1
+# Context Automaton Transitions:
+ * [s0 -> s1]: { m={ e1 e4 } }
+ * [s1 -> s1]: { m={ } }
+ * [s1 -> s1]: { m={ e4 } }

tests/expected/trivial_reactions.txt

@@ -0,0 +1,8 @@
+# Reactions:
+
+  . proc = "m":
+     * (R={ e1 e4 },I={ e2 },P={ e1 e2 })
+     * (R={ e2 },I={ e4 },P={ e1 e4 e3 })
+     * (R={ e1 e3 },I={ e2 },P={ e1 e2 })
+     * (R={ e3 },I={ e2 },P={ e1 })
+

tests/expected/trivial_states.txt

@@ -0,0 +1,3 @@
+{ m={ e1 e4 e3 } }
+{ m={ e1 e2 } }
+{ m={ } }

tests/run_all_tests.sh

@@ -0,0 +1,85 @@
+#!/usr/bin/env bash
+
+# Runs all ReactICS regression tests (BDD + SMT + generators)
+
+set -uo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+ROOT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)"
+REACTICS="$ROOT_DIR/reactics-bdd/reactics"
+GENERATORS="$ROOT_DIR/examples/bdd/generators"
+
+cd "$ROOT_DIR"
+
+failed=0
+
+# ---------------------------------------------------------------
+echo "========== BDD Tests =========="
+echo
+bash "$SCRIPT_DIR/run_tests.sh" || failed=1
+
+# ---------------------------------------------------------------
+echo
+echo "========== SMT Tests (pytest) =========="
+echo
+python3 -m pytest "$SCRIPT_DIR/test_smt.py" -v || failed=1
+
+# ---------------------------------------------------------------
+echo
+echo "========== Generator Tests =========="
+echo
+
+gen_pass=0
+gen_fail=0
+
+check_gen() {
+    local name="$1"
+    local gen_cmd="$2"
+    local property="$3"
+    local expected="$4"
+
+    local tmpfile
+    tmpfile=$(mktemp /tmp/reactics_gen_XXXXXX.drs)
+
+    eval "$gen_cmd" > "$tmpfile" 2>&1
+    local result
+    result=$("$REACTICS" -c "$property" "$tmpfile" 2>&1 | grep -oE "(holds|does not hold)" || true)
+    rm -f "$tmpfile"
+
+    if [[ "$result" == "$expected" ]]; then
+        echo "  PASS: $name"
+        ((gen_pass++))
+    else
+        echo "  FAIL: $name (expected '$expected', got '$result')"
+        ((gen_fail++))
+        failed=1
+    fi
+}
+
+echo "[gen_tgc]"
+check_gen "tgc(3) f1"  "python3 $GENERATORS/gen_tgc.py 3"  f1  "holds"
+check_gen "tgc(3) f3"  "python3 $GENERATORS/gen_tgc.py 3"  f3  "holds"
+check_gen "tgc(4) f2"  "python3 $GENERATORS/gen_tgc.py 4"  f2  "holds"
+
+echo
+echo "[gen_asm]"
+check_gen "asm(3) f1"   "python3 $GENERATORS/gen_asm.py 3"   f1  "holds"
+check_gen "asm(3) f2"   "python3 $GENERATORS/gen_asm.py 3"   f2  "holds"
+
+echo
+echo "[gen_drs]"
+check_gen "drs(2,2,2,a) f0"  "python3 $GENERATORS/gen_drs.py 2 2 2 a"  f0  "does not hold"
+check_gen "drs(2,2,2,b) f0"  "python3 $GENERATORS/gen_drs.py 2 2 2 b"  f0  "holds"
+
+echo
+echo "Generator results: $gen_pass passed, $gen_fail failed"
+
+# ---------------------------------------------------------------
+echo
+echo "================================"
+if [[ $failed -eq 0 ]]; then
+    echo "All test suites passed."
+else
+    echo "Some tests FAILED."
+    exit 1
+fi

tests/run_tests.sh

@@ -0,0 +1,69 @@
+#!/usr/bin/env bash
+
+# Regression test harness for ReactICS BDD module
+# Compares current output against saved expected output
+
+set -uo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+ROOT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)"
+REACTICS="$ROOT_DIR/reactics-bdd/reactics"
+EXPECTED_DIR="$SCRIPT_DIR/expected"
+
+PASS=0
+FAIL=0
+ERRORS=""
+
+run_test() {
+    local name="$1"
+    local expected_file="$2"
+    shift 2
+    local actual
+    actual=$("$@" 2>&1) || true
+    local expected
+    expected=$(cat "$expected_file")
+
+    if [[ "$actual" == "$expected" ]]; then
+        echo "  PASS: $name"
+        ((PASS++))
+    else
+        echo "  FAIL: $name"
+        diff <(echo "$expected") <(echo "$actual") | head -20
+        ((FAIL++))
+        ERRORS="$ERRORS\n  - $name"
+    fi
+}
+
+echo "Running ReactICS regression tests..."
+echo
+
+# --- tgc.drs tests ---
+echo "[tgc]"
+run_test "tgc print"      "$EXPECTED_DIR/tgc_print.txt"      "$REACTICS" -P examples/bdd/tgc.drs
+run_test "tgc reactions"   "$EXPECTED_DIR/tgc_reactions.txt"   "$REACTICS" -r examples/bdd/tgc.drs
+run_test "tgc states"      "$EXPECTED_DIR/tgc_states.txt"      "$REACTICS" -s examples/bdd/tgc.drs
+run_test "tgc mc (f1-f4)"  "$EXPECTED_DIR/tgc_mc.txt" \
+    bash -c 'for f in f1 f2 f3 f4; do '"$REACTICS"' -c $f examples/bdd/tgc.drs 2>&1; done'
+
+echo
+echo "[trivial]"
+run_test "trivial print"      "$EXPECTED_DIR/trivial_print.txt"      "$REACTICS" -P reactics-bdd/in/trivial.drs
+run_test "trivial reactions"  "$EXPECTED_DIR/trivial_reactions.txt"   "$REACTICS" -r reactics-bdd/in/trivial.drs
+run_test "trivial states"     "$EXPECTED_DIR/trivial_states.txt"      "$REACTICS" -s reactics-bdd/in/trivial.drs
+
+echo
+echo "[tgc4]"
+run_test "tgc4 print"      "$EXPECTED_DIR/tgc4_print.txt"      "$REACTICS" -P examples/bdd/tgc4.drs
+run_test "tgc4 states"     "$EXPECTED_DIR/tgc4_states.txt"      "$REACTICS" -s examples/bdd/tgc4.drs
+run_test "tgc4 mc (f1-f4)" "$EXPECTED_DIR/tgc4_mc.txt" \
+    bash -c 'for f in f1 f2 f3 f4; do '"$REACTICS"' -c $f examples/bdd/tgc4.drs 2>&1; done'
+
+echo
+echo "================================"
+echo "Results: $PASS passed, $FAIL failed"
+if [[ $FAIL -gt 0 ]]; then
+    echo -e "Failures:$ERRORS"
+    exit 1
+else
+    echo "All tests passed."
+fi

tests/test_smt.py

@@ -0,0 +1,501 @@
+"""
+Regression tests for the ReactICS SMT module.
+
+Tests the Python API directly: reaction system construction,
+context automata, and SMT-based verification (reachability + rsLTL).
+"""
+
+import sys
+import os
+import io
+from contextlib import redirect_stdout
+
+# Add reactics-smt to the path
+sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..", "reactics-smt"))
+
+from z3 import sat, unsat
+from rs import (
+    ReactionSystem,
+    ContextAutomaton,
+    ReactionSystemWithConcentrations,
+    ContextAutomatonWithConcentrations,
+    ReactionSystemWithConcentrationsParam,
+    ReactionSystemWithAutomaton,
+)
+from smt import SmtCheckerRS, SmtCheckerRSC, SmtCheckerRSCParam
+from logics import Formula_rsLTL, BagDescription
+from rsltl_shortcuts import ltl_F, bag_entity, param_entity, param_And
+
+
+# ---------------------------------------------------------------------------
+# Helpers
+# ---------------------------------------------------------------------------
+
+def run_silent(fn, *args, **kwargs):
+    """Run a function with stdout suppressed, return its result."""
+    with redirect_stdout(io.StringIO()):
+        return fn(*args, **kwargs)
+
+
+# ---------------------------------------------------------------------------
+# Data model tests
+# ---------------------------------------------------------------------------
+
+class TestReactionSystem:
+    def test_add_entities(self):
+        rs = ReactionSystem()
+        rs.add_bg_set_entity("a")
+        rs.add_bg_set_entity("b")
+        assert rs.background_set == ["a", "b"]
+        assert rs.get_entity_id("a") == 0
+        assert rs.get_entity_id("b") == 1
+        assert rs.get_entity_name(0) == "a"
+
+    def test_add_reaction(self):
+        rs = ReactionSystem()
+        rs.add_bg_set_entity("a")
+        rs.add_bg_set_entity("b")
+        rs.add_bg_set_entity("c")
+        rs.add_reaction(["a"], ["b"], ["c"])
+        assert len(rs.reactions) == 1
+        reactants, inhibitors, products = rs.reactions[0]
+        assert reactants == [0]
+        assert inhibitors == [1]
+        assert products == [2]
+
+    def test_reactions_by_product(self):
+        rs = ReactionSystem()
+        rs.add_bg_set_entity("a")
+        rs.add_bg_set_entity("b")
+        rs.add_reaction(["a"], [], ["b"])
+        rbp = rs.get_reactions_by_product()
+        assert 1 in rbp  # entity id for "b"
+        assert len(rbp[1]) == 1
+
+    def test_duplicate_entity_raises(self):
+        rs = ReactionSystem()
+        rs.add_bg_set_entity("a")
+        try:
+            rs.add_bg_set_entity("a")
+            assert False, "Should have raised"
+        except RuntimeError:
+            pass
+
+
+class TestReactionSystemWithConcentrations:
+    def test_add_entity_with_concentration(self):
+        rs = ReactionSystemWithConcentrations()
+        rs.add_bg_set_entity(("x", 3))
+        rs.add_bg_set_entity(("y", 5))
+        assert rs.background_set == ["x", "y"]
+        assert rs.get_max_concentration_level(0) == 3
+        assert rs.get_max_concentration_level(1) == 5
+
+    def test_add_reaction_with_concentrations(self):
+        rs = ReactionSystemWithConcentrations()
+        rs.add_bg_set_entity(("a", 2))
+        rs.add_bg_set_entity(("b", 1))
+        rs.add_reaction([("a", 1)], [], [("b", 1)])
+        assert len(rs.reactions) == 1
+
+    def test_meta_reactions(self):
+        rs = ReactionSystemWithConcentrations()
+        rs.add_bg_set_entity(("e", 3))
+        rs.add_bg_set_entity(("inc", 1))
+        rs.add_reaction_inc("e", "inc", [("e", 1)], [("e", 3)])
+        e_id = rs.get_entity_id("e")
+        assert e_id in rs.meta_reactions
+        assert rs.meta_reactions[e_id][0][0] == "inc"
+
+
+class TestContextAutomaton:
+    def test_states_and_transitions(self):
+        rs = ReactionSystem()
+        rs.add_bg_set_entity("a")
+        rs.add_bg_set_entity("b")
+        ca = ContextAutomaton(rs)
+        ca.add_init_state("s0")
+        ca.add_state("s1")
+        assert ca.get_init_state_id() == 0
+        assert ca.get_state_id("s1") == 1
+        ca.add_transition("s0", ["a"], "s1")
+        ca.add_transition("s1", [], "s1")
+        assert len(ca.transitions) == 2
+
+    def test_invalid_transition_raises(self):
+        rs = ReactionSystem()
+        rs.add_bg_set_entity("a")
+        ca = ContextAutomaton(rs)
+        ca.add_init_state("s0")
+        try:
+            ca.add_transition("s0", ["a"], "nonexistent")
+            assert False, "Should have raised"
+        except RuntimeError:
+            pass
+
+
+class TestContextAutomatonWithConcentrations:
+    def test_transitions_with_concentrations(self):
+        rs = ReactionSystemWithConcentrations()
+        rs.add_bg_set_entity(("a", 2))
+        rs.add_bg_set_entity(("b", 1))
+        ca = ContextAutomatonWithConcentrations(rs)
+        ca.add_init_state("s0")
+        ca.add_state("s1")
+        ca.add_transition("s0", [("a", 2)], "s1")
+        ca.add_transition("s1", [], "s1")
+        assert len(ca.transitions) == 2
+
+
+# ---------------------------------------------------------------------------
+# Formula construction tests
+# ---------------------------------------------------------------------------
+
+class TestFormulas:
+    def test_bag_description(self):
+        b = BagDescription.f_entity("x")
+        assert str(b) == "x"
+        b_gt = b > 0
+        assert ">" in str(b_gt)
+
+    def test_rsltl_formula(self):
+        f = Formula_rsLTL.f_F(
+            BagDescription.f_TRUE(),
+            BagDescription.f_entity("x") > 0,
+        )
+        assert "F" in str(f)
+
+    def test_combined_formula(self):
+        f = Formula_rsLTL.f_G(
+            BagDescription.f_TRUE(),
+            Formula_rsLTL.f_Implies(
+                BagDescription.f_entity("a") == 1,
+                Formula_rsLTL.f_F(
+                    BagDescription.f_TRUE(),
+                    BagDescription.f_entity("b") > 0,
+                ),
+            ),
+        )
+        assert "G" in str(f)
+        assert "F" in str(f)
+
+
+# ---------------------------------------------------------------------------
+# Verification tests: SmtCheckerRS (basic, no concentrations)
+# ---------------------------------------------------------------------------
+
+def _build_simple_rs():
+    """A minimal RS for testing: a -> b -> c with context automaton."""
+    rs = ReactionSystem()
+    rs.add_bg_set_entity("a")
+    rs.add_bg_set_entity("b")
+    rs.add_bg_set_entity("c")
+    rs.add_reaction(["a"], [], ["b"])
+    rs.add_reaction(["b"], [], ["c"])
+
+    ca = ContextAutomaton(rs)
+    ca.add_init_state("s0")
+    ca.add_state("s1")
+    ca.add_transition("s0", ["a"], "s1")
+    ca.add_transition("s1", [], "s1")
+
+    return ReactionSystemWithAutomaton(rs, ca)
+
+
+class TestSmtCheckerRS:
+    def test_reachability_sat(self):
+        rsa = _build_simple_rs()
+        checker = SmtCheckerRS(rsa)
+        run_silent(
+            checker.check_reachability,
+            ["c"],
+            print_witness=False,
+            print_time=False,
+            print_mem=False,
+        )
+        # After finding SAT, solver state should be satisfiable
+        assert checker.solver.check() == sat
+
+    def test_reachability_unreachable(self):
+        """Entity 'a' is never produced, so it shouldn't be reachable as a final state."""
+        rs = ReactionSystem()
+        rs.add_bg_set_entity("a")
+        rs.add_bg_set_entity("b")
+        rs.add_reaction(["a"], [], ["b"])
+
+        ca = ContextAutomaton(rs)
+        ca.add_init_state("s0")
+        ca.add_state("s1")
+        # Context provides 'a' initially, then nothing
+        ca.add_transition("s0", ["a"], "s1")
+        ca.add_transition("s1", [], "s1")
+
+        rsa = ReactionSystemWithAutomaton(rs, ca)
+        checker = SmtCheckerRS(rsa)
+
+        # 'b' is reachable (produced from 'a')
+        run_silent(
+            checker.check_reachability,
+            ["b"],
+            print_witness=False,
+            print_time=False,
+            print_mem=False,
+        )
+        assert checker.solver.check() == sat
+
+
+# ---------------------------------------------------------------------------
+# Verification tests: SmtCheckerRSC (with concentrations)
+# ---------------------------------------------------------------------------
+
+def _build_chain_rsc(chain_len=2, max_conc=2):
+    """Build a chain reaction system with concentrations."""
+    r = ReactionSystemWithConcentrations()
+    r.add_bg_set_entity(("inc", 1))
+    r.add_bg_set_entity(("dec", 1))
+
+    for i in range(1, chain_len + 1):
+        r.add_bg_set_entity(("e_" + str(i), max_conc))
+
+    for i in range(1, chain_len + 1):
+        ent = "e_" + str(i)
+        r.add_reaction_inc(ent, "inc", [(ent, 1)], [(ent, max_conc)])
+        r.add_reaction_dec(ent, "dec", [(ent, 1)], [])
+        if i < chain_len:
+            r.add_reaction([(ent, max_conc)], [], [("e_" + str(i + 1), 1)])
+
+    r.add_reaction(
+        [("e_" + str(chain_len), max_conc)],
+        [("dec", 1)],
+        [("e_" + str(chain_len), max_conc)],
+    )
+
+    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")
+
+    return ReactionSystemWithAutomaton(r, c)
+
+
+class TestSmtCheckerRSC:
+    def test_chain_reachability_sat(self):
+        """Chain(2,2): e_2=2 should be reachable at level 3."""
+        rc = _build_chain_rsc(2, 2)
+        checker = SmtCheckerRSC(rc)
+        prop = ([("e_2", 2)], [])
+        run_silent(
+            checker.check_reachability,
+            prop,
+            print_witness=False,
+            print_time=False,
+            print_mem=False,
+            max_level=10,
+        )
+        assert checker.solver.check() == sat
+        assert checker.current_level == 3
+
+    def test_chain_reachability_longer(self):
+        """Chain(3,2): e_3=2 should be reachable at level 5."""
+        rc = _build_chain_rsc(3, 2)
+        checker = SmtCheckerRSC(rc)
+        prop = ([("e_3", 2)], [])
+        run_silent(
+            checker.check_reachability,
+            prop,
+            print_witness=False,
+            print_time=False,
+            print_mem=False,
+            max_level=10,
+        )
+        assert checker.solver.check() == sat
+        assert checker.current_level == 5
+
+    def test_rsltl_finally(self):
+        """Check rsLTL F formula on chain(2,2)."""
+        rc = _build_chain_rsc(2, 2)
+        checker = SmtCheckerRSC(rc)
+        form = Formula_rsLTL.f_F(
+            BagDescription.f_entity("inc") > 0,
+            BagDescription.f_entity("e_2") >= 2,
+        )
+        run_silent(
+            checker.check_rsltl,
+            formula=form,
+            print_witness=False,
+            print_time=False,
+            print_mem=False,
+        )
+        assert checker.solver.check() == sat
+        assert checker.current_level == 3
+
+    def test_rsltl_finally_fast(self):
+        """Chain(2,2), F(e_1==2): should be SAT at level 1."""
+        rc = _build_chain_rsc(2, 2)
+        checker = SmtCheckerRSC(rc)
+        form = Formula_rsLTL.f_F(
+            BagDescription.f_entity("inc") > 0,
+            BagDescription.f_entity("e_1") == 2,
+        )
+        run_silent(
+            checker.check_rsltl,
+            formula=form,
+            print_witness=False,
+            print_time=False,
+            print_mem=False,
+        )
+        assert checker.solver.check() == sat
+        assert checker.current_level == 1
+
+    def test_rsltl_next_until(self):
+        """Chain(2,2), X[TRUE](e_1 > 0 U[inc > 0] e_2 > 0): SAT at level 2."""
+        rc = _build_chain_rsc(2, 2)
+        checker = SmtCheckerRSC(rc)
+        form = 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,
+            ),
+        )
+        run_silent(
+            checker.check_rsltl,
+            formula=form,
+            print_witness=False,
+            print_time=False,
+            print_mem=False,
+        )
+        assert checker.solver.check() == sat
+        assert checker.current_level == 2
+
+
+# ---------------------------------------------------------------------------
+# Verification tests: SmtCheckerRSC on heat shock response
+# ---------------------------------------------------------------------------
+
+def _build_heat_shock():
+    """Heat shock response model."""
+    stress_temp = 42
+    max_temp = 50
+
+    r = ReactionSystemWithConcentrations()
+    for e in [("hsp", 1), ("hsf", 1), ("hsf2", 1), ("hsf3", 1), ("hse", 1),
+              ("mfp", 1), ("prot", 1), ("hsf3:hse", 1), ("hsp:mfp", 1),
+              ("hsp:hsf", 1), ("temp", max_temp), ("heat", 1), ("cool", 1)]:
+        r.add_bg_set_entity(e)
+
+    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")
+
+    return ReactionSystemWithAutomaton(r, c)
+
+
+class TestHeatShockResponse:
+    def test_mfp_reachable(self):
+        """mfp should be reachable at level 9."""
+        rc = _build_heat_shock()
+        checker = SmtCheckerRSC(rc)
+        prop = ([("mfp", 1)], [])
+        run_silent(
+            checker.check_reachability,
+            prop,
+            print_witness=False,
+            print_time=False,
+            print_mem=False,
+            max_level=40,
+        )
+        assert checker.solver.check() == sat
+        assert checker.current_level == 9
+
+
+# ---------------------------------------------------------------------------
+# Verification tests: SmtCheckerRSCParam (parametric)
+# ---------------------------------------------------------------------------
+
+def _build_parametric_overview():
+    """Parametric example from doc/overview.py."""
+    prs = ReactionSystemWithConcentrationsParam()
+    for ec in [("a", 3), ("b", 2), ("c", 1), ("h", 1)]:
+        prs.add_bg_set_entity(ec)
+
+    lda = prs.get_param("lda")
+    prs.add_reaction([("a", 1)], [("h", 1)], [("b", 2)])
+    prs.add_reaction(lda, [("h", 1)], [("c", 1)])
+
+    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")
+
+    return ReactionSystemWithAutomaton(prs, ca), lda
+
+
+class TestSmtCheckerRSCParam:
+    def test_parametric_sat(self):
+        """Parametric overview: F[h==0](c>0) should be SAT at level 2."""
+        rc, lda = _build_parametric_overview()
+        pc = param_entity(lda, "a") == 0
+        f = ltl_F(bag_entity("h") == 0, "c")
+
+        checker = SmtCheckerRSCParam(rc, optimise=True)
+        run_silent(
+            checker.check_rsltl,
+            formulae_list=[f],
+            param_constr=pc,
+        )
+        # The parametric checker uses path-based solving;
+        # after SAT the solver should be satisfiable
+        assert checker.solver.check() == sat
+
+
+# ---------------------------------------------------------------------------
+# RS translation tests (RSC -> RS)
+# ---------------------------------------------------------------------------
+
+class TestRSCtoRSTranslation:
+    def test_translated_system_reachability(self):
+        """Chain(2,2) translated to plain RS: e_2#2 should be reachable."""
+        rc = _build_chain_rsc(2, 2)
+        orc = rc.get_ordinary_reaction_system_with_automaton()
+        checker = SmtCheckerRS(orc)
+        run_silent(
+            checker.check_reachability,
+            ["e_2#2"],
+            print_witness=False,
+            print_time=False,
+            print_mem=False,
+        )
+        assert checker.solver.check() == sat