diff --git a/examples/iterated-majority/README.md b/examples/iterated-majority/README.md new file mode 100644 index 0000000..214abfb --- /dev/null +++ b/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 ) +``` diff --git a/examples/iterated-majority/generate_models.py b/examples/iterated-majority/generate_models.py new file mode 100755 index 0000000..3d6c1f3 --- /dev/null +++ b/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 +Where 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 ") + 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() diff --git a/examples/iterated-majority/nfa-3.png b/examples/iterated-majority/nfa-3.png new file mode 100644 index 0000000..dd5e21a Binary files /dev/null and b/examples/iterated-majority/nfa-3.png differ diff --git a/examples/iterated-majority/run_benchmarks.py b/examples/iterated-majority/run_benchmarks.py new file mode 100755 index 0000000..f2543df --- /dev/null +++ b/examples/iterated-majority/run_benchmarks.py @@ -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()