File size: 4,303 Bytes
ba4f7c6 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 | """
Büchi automata for common LTL spec patterns.
Implemented directly — no external tool needed.
Supported patterns:
G(!p) — safety: never visit p
GF(p) — recurrence: visit p infinitely often
F(p) — reachability: eventually visit p
G(p) — invariance: always be in p
Each automaton is a dict-based structure with:
states : list of state names
initial : initial state name
delta : (state, label_frozenset) -> next_state | None (None = sink/stuck)
accepting : set of accepting states
"""
from typing import Callable, FrozenSet, NamedTuple, Optional
class BuchiAut:
def __init__(self, states, initial, delta_fn, accepting, name=""):
self.states = states # list of hashable state ids
self.initial = initial
self._delta = delta_fn # (state, frozenset) -> state | None
self.accepting = set(accepting)
self.name = name
def step(self, state, label: FrozenSet[str]) -> Optional[object]:
return self._delta(state, label)
def is_accepting(self, state) -> bool:
return state in self.accepting
# ── factory functions ─────────────────────────────────────────────────────────
def safety(prop: str, label: str = "") -> BuchiAut:
"""G(!prop) — automaton rejects if prop is ever true."""
# States: q0 (safe), q_sink (violated, non-accepting)
def delta(state, lbl):
if state == "q0":
return "q_sink" if prop in lbl else "q0"
return "q_sink" # once violated, stay violated
return BuchiAut(
states=["q0", "q_sink"],
initial="q0",
delta_fn=delta,
accepting=["q0"], # must stay in q0 infinitely → never violated
name=label or f"G(!{prop})",
)
def recurrence(prop: str, label: str = "") -> BuchiAut:
"""GF(prop) — must visit prop infinitely often."""
# States: q0 (waiting), q1 (just saw prop — accepting)
def delta(state, lbl):
if state == "q0":
return "q1" if prop in lbl else "q0"
# q1: already accepted, loop back to wait for next occurrence
return "q0"
return BuchiAut(
states=["q0", "q1"],
initial="q0",
delta_fn=delta,
accepting=["q1"],
name=label or f"GF({prop})",
)
def reachability(prop: str, label: str = "") -> BuchiAut:
"""F(prop) — eventually reach prop (then stay accepting)."""
# States: q0 (searching), q1 (reached — accepting sink)
def delta(state, lbl):
if state == "q0":
return "q1" if prop in lbl else "q0"
return "q1" # once reached, stay accepting
return BuchiAut(
states=["q0", "q1"],
initial="q0",
delta_fn=delta,
accepting=["q1"],
name=label or f"F({prop})",
)
def invariance(prop: str, label: str = "") -> BuchiAut:
"""G(prop) — always be in prop."""
def delta(state, lbl):
if state == "q0":
return "q0" if prop in lbl else "q_sink"
return "q_sink"
return BuchiAut(
states=["q0", "q_sink"],
initial="q0",
delta_fn=delta,
accepting=["q0"],
name=label or f"G({prop})",
)
# ── simple formula parser ─────────────────────────────────────────────────────
def parse_spec(formula: str, label: str = "") -> BuchiAut:
"""
Parse simple LTL formula string into a BuchiAut.
Supported:
G(!p) → safety
GF(p) → recurrence
F(p) → reachability
G(p) → invariance
"""
f = formula.strip().replace(" ", "")
lbl = label or formula
if f.startswith("GF(") and f.endswith(")"):
return recurrence(f[3:-1], lbl)
if f.startswith("G(!") and f.endswith(")"):
return safety(f[3:-1], lbl)
if f.startswith("G(") and f.endswith(")"):
return invariance(f[2:-1], lbl)
if f.startswith("F(") and f.endswith(")"):
return reachability(f[2:-1], lbl)
raise ValueError(
f"Unsupported formula: '{formula}'. "
"Supported: G(!p), GF(p), G(p), F(p)"
)
|