Theory NGBTA

section ‹Nondeterministic Generalized Büchi Transition Automata›

theory NGBTA
imports "../Nondeterministic"
begin

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

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

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

end