Skip to main content

ltl_to_buchi

logicaffeine_verify::automata

Function ltl_to_buchi 

Source 
pub fn ltl_to_buchi(spec: &VerifyExpr) -> BuchiAutomaton
Expand description

Convert an LTL specification to a Büchi automaton.

Handles common LTL patterns:

  • G(p) → single accepting state, self-loop with guard p
  • G(F(p)) → two states (waiting, seen), both accepting
  • G(p → F(q)) → two states, transitions on p/q
  • Simple boolean → single state