logicaffeine_verify/
automata.rs

1//! Automata for Reactive Synthesis
2//!
3//! Büchi automaton construction from LTL specifications.
4//! Used as the intermediate representation for game solving.
5
6use crate::ir::VerifyExpr;
7
8/// A state in a Büchi automaton.
9#[derive(Debug, Clone, PartialEq, Eq, Hash)]
10pub struct AutomatonState {
11    pub id: usize,
12    pub label: String,
13}
14
15/// A transition in a Büchi automaton.
16#[derive(Debug, Clone)]
17pub struct AutomatonTransition {
18    pub from: usize,
19    pub guard: VerifyExpr,
20    pub to: usize,
21}
22
23/// A Büchi automaton for LTL specifications.
24#[derive(Debug, Clone)]
25pub struct BuchiAutomaton {
26    pub states: Vec<AutomatonState>,
27    pub initial: usize,
28    pub accepting: Vec<usize>,
29    pub transitions: Vec<AutomatonTransition>,
30}
31
32/// Convert an LTL specification to a Büchi automaton.
33///
34/// Handles common LTL patterns:
35/// - G(p) → single accepting state, self-loop with guard p
36/// - G(F(p)) → two states (waiting, seen), both accepting
37/// - G(p → F(q)) → two states, transitions on p/q
38/// - Simple boolean → single state
39pub fn ltl_to_buchi(spec: &VerifyExpr) -> BuchiAutomaton {
40    match detect_ltl_pattern(spec) {
41        LtlPattern::Safety(prop) => {
42            // G(p) → single accepting state with self-loop guarded by p
43            BuchiAutomaton {
44                states: vec![AutomatonState { id: 0, label: "safe".into() }],
45                initial: 0,
46                accepting: vec![0],
47                transitions: vec![AutomatonTransition {
48                    from: 0,
49                    guard: prop,
50                    to: 0,
51                }],
52            }
53        }
54        LtlPattern::Response(trigger, response) => {
55            // G(p → F(q)) → two states: idle, waiting_for_response
56            BuchiAutomaton {
57                states: vec![
58                    AutomatonState { id: 0, label: "idle".into() },
59                    AutomatonState { id: 1, label: "waiting".into() },
60                ],
61                initial: 0,
62                accepting: vec![0], // Only idle is accepting (response must eventually happen)
63                transitions: vec![
64                    // idle → idle (no trigger)
65                    AutomatonTransition {
66                        from: 0,
67                        guard: VerifyExpr::not(trigger.clone()),
68                        to: 0,
69                    },
70                    // idle → waiting (trigger fires, response not yet)
71                    AutomatonTransition {
72                        from: 0,
73                        guard: VerifyExpr::and(trigger.clone(), VerifyExpr::not(response.clone())),
74                        to: 1,
75                    },
76                    // idle → idle (trigger fires AND response immediate)
77                    AutomatonTransition {
78                        from: 0,
79                        guard: VerifyExpr::and(trigger, response.clone()),
80                        to: 0,
81                    },
82                    // waiting → idle (response arrives)
83                    AutomatonTransition {
84                        from: 1,
85                        guard: response.clone(),
86                        to: 0,
87                    },
88                    // waiting → waiting (still waiting)
89                    AutomatonTransition {
90                        from: 1,
91                        guard: VerifyExpr::not(response),
92                        to: 1,
93                    },
94                ],
95            }
96        }
97        LtlPattern::Liveness(prop) => {
98            // G(F(p)) → two states, loop between them
99            BuchiAutomaton {
100                states: vec![
101                    AutomatonState { id: 0, label: "unseen".into() },
102                    AutomatonState { id: 1, label: "seen".into() },
103                ],
104                initial: 0,
105                accepting: vec![1], // Must visit "seen" infinitely often
106                transitions: vec![
107                    AutomatonTransition { from: 0, guard: VerifyExpr::not(prop.clone()), to: 0 },
108                    AutomatonTransition { from: 0, guard: prop.clone(), to: 1 },
109                    AutomatonTransition { from: 1, guard: VerifyExpr::bool(true), to: 0 },
110                ],
111            }
112        }
113        LtlPattern::Boolean(prop) => {
114            // Simple boolean → single state
115            BuchiAutomaton {
116                states: vec![AutomatonState { id: 0, label: "check".into() }],
117                initial: 0,
118                accepting: vec![0],
119                transitions: vec![AutomatonTransition {
120                    from: 0,
121                    guard: prop,
122                    to: 0,
123                }],
124            }
125        }
126    }
127}
128
129/// Detected LTL pattern.
130enum LtlPattern {
131    Safety(VerifyExpr),                      // G(p)
132    Response(VerifyExpr, VerifyExpr),         // G(p → F(q))
133    Liveness(VerifyExpr),                     // G(F(p))
134    Boolean(VerifyExpr),                      // p
135}
136
137/// Detect the LTL pattern of a specification.
138fn detect_ltl_pattern(spec: &VerifyExpr) -> LtlPattern {
139    // Pattern: NOT(something) at top level → safety (G(NOT(bad)))
140    if let VerifyExpr::Not(_inner) = spec {
141        return LtlPattern::Safety(spec.clone());
142    }
143
144    // Pattern: implies at top → response (G(p → F(q)))
145    if let VerifyExpr::Binary { op: crate::ir::VerifyOp::Implies, left, right } = spec {
146        return LtlPattern::Response(*left.clone(), *right.clone());
147    }
148
149    // Pattern: single variable or boolean → safety
150    if matches!(spec, VerifyExpr::Var(_) | VerifyExpr::Bool(_)) {
151        return LtlPattern::Safety(spec.clone());
152    }
153
154    // Default: treat as safety
155    LtlPattern::Safety(spec.clone())
156}
logicaffeine_verify/automata.rs

logicaffeine_verify/
automata.rs
