example: iterative majority

Author: pazz

examples/iterated-majority/README.md

@@ -0,0 +1,58 @@
+
+# A family of uncontrollable NFAs
+
+Each automaton in this family is a chain of diamonds where after a split, controller can move a majority of the population into the target and moves the rest to the next round. The last round is a bad sink.
+
+![nfa for N=3](nfa-3.png)
+
+All of these models are **not** congrollable for arbitrary number of processes, but in the size-$n$ chain one can control $\le 2^n$ tokens.
+
+## Generate model files
+
+Starting in shepherd's main directory, run the python script to generate 10 models.
+
+```console
+./generate_models.py 10
+nfa-10.dot  nfa-2.dot  nfa-4.dot  nfa-6.dot  nfa-8.dot  generate_models.py
+nfa-1.dot   nfa-3.dot  nfa-5.dot  nfa-7.dot  nfa-9.dot
+```
+
+## Solve them using prism
+
+This assumes the `schaeppert` binary is in your PATH, which can be done by running `cargo install --path .`
+
+```console
+schaeppert -f dot nfa-3.dot iterate tmp/ 
+n=1 -> 1.000
+n=2 -> 1.000
+n=3 -> 1.000
+n=4 -> 1.000
+n=5 -> 1.000
+n=6 -> 1.000
+n=7 -> 1.000
+n=8 -> 0.949
+The value is less than 1.0, stopping the search.
+The 8-fold power of this NFA is not controllable.
+```
+
+
+## Solve them using shepherd
+
+
+```console
+shepherd -f dot nfa-2.dot 
+
+Maximal winning strategy;
+Answer:
+	NO (uncontrollable)
+
+States: ( 1a , 0a , T , 1 , 0b , 2 , 1b , 0 )
+ Play action 'a' in the downward-closure of
+	( ω , ω , ω , 1 , 1 , _ , _ , 1 )
+	( ω , ω , ω , _ , 1 , _ , _ , 3 )
+
+
+Play action 'b' in the downward-closure of
+	( _ , 1 , ω , 1 , ω , _ , ω , 1 )
+	( _ , 1 , ω , _ , ω , _ , ω , 3 )
+```

examples/iterated-majority/generate_models.py

@@ -0,0 +1,75 @@
+#!/usr/bin/env python3
+"""
+generate_models.py
+
+This script generates DOT files representing a family of NFA (nondeterministic finite automaton) models.
+For each integer i from 1 to n (inclusive), it creates a file named 'nfa-i.dot' describing an NFA with a specific structure:
+- States 0 through i, plus a target state T.
+- Initial transitions from state 0 to each state 1..i+1 labeled 'a'.
+- For each state j in 1..i+1, transitions from j to T labeled 'a{k}' for every k in 1..i+1 where k != j.
+
+Usage:
+    python generate_models.py <n>
+Where <n> is a positive integer.
+
+
+Note: All of these models are not congrollable for arbitrary number of processes, but the n-fold product of the size-m model is controllable by playing action "a", then "aj" if node "j" if none of the n processes reside in node j.
+"""
+import sys
+def generate_model_file(n):
+    filename = f"nfa-{n}.dot"
+    with open(filename, "w") as f:
+        f.write('digraph NFA {\n')
+        f.write('    init [label=" ",shape=none,height=0,width=0];\n')
+        # States 0..N
+        for i in range(n):
+            f.write(
+                f'    s{i} [label="{i}",   shape=circle];\n'
+                f'    s{i}a [label="{i}a", shape=circle];\n'
+                f'    s{i}b [label="{i}b", shape=circle];\n'
+                    )
+        # Sink
+        f.write(f'    s{n} [label="{n}", shape=circle];\n')
+        # Target state T
+        f.write('    T [label="T", shape=doublecircle];\n\n')
+        # Initial arrow
+        f.write('    init -> s0;\n')
+        # Transitions from 0 to 1..N
+        for i in range(n):
+            f.write(
+                f'    s{i} -> s{i}a [label="a"];\n'
+                f'    s{i} -> s{i}b [label="a"];\n'
+                f'    s{i} -> s{i}a [label="b"];\n'
+                f'    s{i} -> s{i}b [label="b"];\n'
+
+                f'    s{i}a -> T [label="a"];\n'
+                f'    s{i}a -> s{i+1} [label="b"];\n'
+                f'    s{i}b -> T [label="b"];\n'
+                f'    s{i}b -> s{i+1} [label="a"];\n'
+            )
+        
+        # Good and bad sink
+        f.write(
+            '    T -> T [label="a"];\n'
+            '    T -> T [label="b"];\n'
+            f'    s{n} -> s{n} [label="a"];\n'
+            f'    s{n} -> s{n} [label="b"];\n'
+        )
+        f.write('}\n')
+
+def main():
+    if len(sys.argv) != 2:
+        print("Usage: python generate_models.py <n>")
+        sys.exit(1)
+    try:
+        n = int(sys.argv[1])
+        if n < 1:
+            raise ValueError
+    except ValueError:
+        print("n must be a positive integer")
+        sys.exit(1)
+    for i in range(1, n + 1):
+        generate_model_file(i)
+
+if __name__ == "__main__":
+    main()

examples/iterated-majority/nfa-3.png

@@ -0,0 +1,101 @@
+#!/usr/bin/env python3
+import os
+import shutil
+import subprocess
+import sys
+import time
+import csv
+import matplotlib.pyplot as plt
+
+# Constants
+COMMANDS = [
+    "schaeppert -vv -f dot nfa-{n}.dot iterate tmp/",
+    # "schaeppert -f dot nfa-{n}.dot iterate tmp/",
+    #"shepherd -vv -f dot nfa-{n}.dot",
+    "shepherd -f dot nfa-{n}.dot",
+]
+TIMEOUT = 60  # seconds
+TMP_DIR = "tmp"
+LOGFILE_TEMPLATE = "log_{cmd_idx}_n{n}.txt"
+
+def ensure_empty_tmp():
+    if os.path.exists(TMP_DIR):
+        shutil.rmtree(TMP_DIR)
+    os.makedirs(TMP_DIR)
+
+def run_command(cmd, logfile, timeout):
+    start = time.time()
+    try:
+        proc = subprocess.run(
+            cmd,
+            shell=True,
+            stdout=subprocess.PIPE,
+            stderr=subprocess.PIPE,
+            timeout=timeout
+        )
+        elapsed = time.time() - start
+        with open(logfile, 'wb') as f:
+            f.write(b'=== STDOUT ===\n')
+            f.write(proc.stdout)
+            f.write(b'\n=== STDERR ===\n')
+            f.write(proc.stderr)
+        return elapsed
+    except subprocess.TimeoutExpired as e:
+        with open(logfile, 'wb') as f:
+            f.write(b'=== STDOUT ===\n')
+            f.write((e.stdout or b''))
+            f.write(b'\n=== STDERR ===\n')
+            f.write((e.stderr or b''))
+            f.write(b'\n=== TIMEOUT ===\n')
+        return None
+
+def main():
+    if len(sys.argv) != 2:
+        print(f"Usage: {sys.argv[0]} N", file=sys.stderr)
+        sys.exit(1)
+    try:
+        N = int(sys.argv[1])
+    except ValueError:
+        print("N must be an integer", file=sys.stderr)
+        sys.exit(1)
+
+    ensure_empty_tmp()
+    results = []
+    for n in range(1, N + 1):
+        row = {'n': n}
+        for cmd_idx, cmd_template in enumerate(COMMANDS):
+            cmd = cmd_template.format(n=n)
+            logfile = LOGFILE_TEMPLATE.format(cmd_idx=cmd_idx, n=n)
+            print(f"Running command {cmd_idx+1} for n={n}: {cmd_template}")
+            t = run_command(cmd, logfile, TIMEOUT)
+            if t is None:
+                break
+            row[f'cmd{cmd_idx+1}_time'] = t
+        else:
+            results.append(row)
+            continue
+        break
+
+    # Write CSV to stdout
+    fieldnames = ['n'] + [f'cmd{i+1}_time' for i in range(len(COMMANDS))]
+    writer = csv.DictWriter(sys.stdout, fieldnames=fieldnames)
+    writer.writeheader()
+    for row in results:
+        writer.writerow(row)
+
+    # Plotting
+    ns = [row['n'] for row in results]
+    for cmd_idx, cmd_template in enumerate(COMMANDS):
+        times = [row.get(f'cmd{cmd_idx+1}_time') for row in results]
+        plt.plot(ns, times, label=cmd_template)
+    plt.xlabel('n')
+    plt.ylabel('Wallclock time (s)')
+    plt.legend()
+    plt.title('Command Running Times')
+    plt.grid(True)
+    plt.tight_layout()
+    plt.savefig("benchmark_results.png")
+    plt.show()
+
+if __name__ == '__main__':
+    main()