Theory DBTA

section ‹Deterministic Büchi Transition Automata›

theory DBTA
imports "../Deterministic"
begin

  datatype ('label, 'state) dbta = dbta
    (alphabet: "'label set")
    (initial: "'state")
    (transition: "'label ⇒ 'state ⇒ 'state")
    (accepting: "('state × 'label × 'state) pred")

  global_interpretation dbta: automaton dbta alphabet initial transition accepting
    defines path = dbta.path and run = dbta.run and reachable = dbta.reachable and nodes = dbta.nodes
    by unfold_locales auto
  global_interpretation dbta: automaton_run dbta alphabet initial transition accepting
    "λ P w r p. infs P (p ## r ||| w ||| r)"
    defines language = dbta.language
    by standard

  abbreviation target where "target ≡ dbta.target"
  abbreviation states where "states ≡ dbta.states"
  abbreviation trace where "trace ≡ dbta.trace"
  abbreviation successors where "successors ≡ dbta.successors TYPE('label)"

end