Refactor

.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 @@ def generate_formula(self):
 
 
 def main():
-    if len(sys.argv) < 1 + 4:
-        print(f"Usage: {sys.argv[0]} <x> <y> <z> <Aut>")
-        print("\twhere x,y,z >= 2 and y >= z")
-        print("\tAut: a, b")
-        sys.exit(1)
-
-    g = DRSGenerator(
-        x=int(sys.argv[1]),
-        y=int(sys.argv[2]),
-        z=int(sys.argv[3]),
-        aut=sys.argv[4],
-    )
+    parser = argparse.ArgumentParser(description=__doc__,
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    parser.add_argument("x", type=int, help="cascade depth (>= 2)")
+    parser.add_argument("y", type=int, help="number of components (>= 2, >= z)")
+    parser.add_argument("z", type=int, help="threshold (>= 2, <= y)")
+    parser.add_argument("aut", choices=["a", "b"], help="automaton variant")
+    args = parser.parse_args()
+
+    if args.x < 2 or args.y < 2 or args.z < 2:
+        parser.error("x, y, z must all be >= 2")
+    if args.y < args.z:
+        parser.error("y must be >= z")
+
+    DRSGenerator(x=args.x, y=args.y, z=args.z, aut=args.aut)
 
 
 if __name__ == "__main__":