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(p → F(q)) → two states, transitions on p/q
37pub fn ltl_to_buchi(spec: &VerifyExpr) -> BuchiAutomaton {
38    match detect_ltl_pattern(spec) {
39        LtlPattern::Safety(prop) => {
40            // G(p) → single accepting state with self-loop guarded by p
41            BuchiAutomaton {
42                states: vec![AutomatonState {
43                    id: 0,
44                    label: "safe".into(),
45                }],
46                initial: 0,
47                accepting: vec![0],
48                transitions: vec![AutomatonTransition {
49                    from: 0,
50                    guard: prop,
51                    to: 0,
52                }],
53            }
54        }
55        LtlPattern::Response(trigger, response) => {
56            // G(p → F(q)) → two states: idle, waiting_for_response
57            BuchiAutomaton {
58                states: vec![
59                    AutomatonState {
60                        id: 0,
61                        label: "idle".into(),
62                    },
63                    AutomatonState {
64                        id: 1,
65                        label: "waiting".into(),
66                    },
67                ],
68                initial: 0,
69                accepting: vec![0], // Only idle is accepting (response must eventually happen)
70                transitions: vec![
71                    // idle → idle (no trigger)
72                    AutomatonTransition {
73                        from: 0,
74                        guard: VerifyExpr::not(trigger.clone()),
75                        to: 0,
76                    },
77                    // idle → waiting (trigger fires, response not yet)
78                    AutomatonTransition {
79                        from: 0,
80                        guard: VerifyExpr::and(trigger.clone(), VerifyExpr::not(response.clone())),
81                        to: 1,
82                    },
83                    // idle → idle (trigger fires AND response immediate)
84                    AutomatonTransition {
85                        from: 0,
86                        guard: VerifyExpr::and(trigger, response.clone()),
87                        to: 0,
88                    },
89                    // waiting → idle (response arrives)
90                    AutomatonTransition {
91                        from: 1,
92                        guard: response.clone(),
93                        to: 0,
94                    },
95                    // waiting → waiting (still waiting)
96                    AutomatonTransition {
97                        from: 1,
98                        guard: VerifyExpr::not(response),
99                        to: 1,
100                    },
101                ],
102            }
103        }
104    }
105}
106
107/// Detected LTL pattern.
108enum LtlPattern {
109    Safety(VerifyExpr),               // G(p)
110    Response(VerifyExpr, VerifyExpr), // G(p → F(q))
111}
112
113/// Detect the LTL pattern of a specification.
114fn detect_ltl_pattern(spec: &VerifyExpr) -> LtlPattern {
115    // Pattern: NOT(something) at top level → safety (G(NOT(bad)))
116    if let VerifyExpr::Not(_inner) = spec {
117        return LtlPattern::Safety(spec.clone());
118    }
119
120    // Pattern: implies at top → response (G(p → F(q)))
121    if let VerifyExpr::Binary {
122        op: crate::ir::VerifyOp::Implies,
123        left,
124        right,
125    } = spec
126    {
127        return LtlPattern::Response(*left.clone(), *right.clone());
128    }
129
130    // Pattern: single variable or boolean → safety
131    if matches!(spec, VerifyExpr::Var(_) | VerifyExpr::Bool(_)) {
132        return LtlPattern::Safety(spec.clone());
133    }
134
135    // Default: treat as safety
136    LtlPattern::Safety(spec.clone())
137}
logicaffeine_verify/automata.rs

logicaffeine_verify/
automata.rs
