Theory NGBA

section ‹Nondeterministic Generalized Büchi Automata›

theory NGBA
imports "../Nondeterministic"
begin

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

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

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

end