Theory DRA

section ‹Deterministic Rabin Automata›

theory DRA
imports "../Deterministic"
begin

  datatype ('label, 'state) dra = dra
    (alphabet: "'label set")
    (initial: "'state")
    (transition: "'label ⇒ 'state ⇒ 'state")
    (condition: "'state rabin gen")

  global_interpretation dra: automaton dra alphabet initial transition condition
    defines path = dra.path and run = dra.run and reachable = dra.reachable and nodes = dra.nodes
    by unfold_locales auto
  global_interpretation dra: automaton_run dra alphabet initial transition condition "λ P w r p. cogen rabin P (p ## r)"
    defines language = dra.language
    by standard

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

end