Making a nondeterministic automaton total.

def Cslib.Automata.NA.totalize {Symbol : Type u_1} {State : Type u_2} (na : NA State Symbol) : NA (Option State) Symbol

NA.totalize makes the original NA total by replacing its LTS with LTS.totalize and its starting states with their lifted non-sink versions.

Equations

• na.totalize = { toLTS := na.totalize, start := some '' na.start }

theorem Cslib.Automata.NA.totalize_run_mtr {Symbol : Type u_1} {State : Type u_2} {na : NA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence (Option State)} {n : ℕ} (h : na.totalize.Run xs ss) (hl : (ss n).isSome = true) : ∃ (s : State) (t : State), na.MTr s (ωSequence.take n xs) t ∧ s ∈ na.start ∧ ss 0 = some s ∧ ss n = some t

In an infinite execution of NA.totalize, as long as the NA stays in a non-sink state, the execution so far corresponds to a finite execution of the original NA.

theorem Cslib.Automata.NA.totalize_mtr_run {Symbol : Type u_1} {State : Type u_2} {na : NA State Symbol} [Inhabited Symbol] {xl : List Symbol} {s t : State} (hs : s ∈ na.start) (hm : na.MTr s xl t) : ∃ (xs : ωSequence Symbol) (ss : ωSequence (Option State)), na.totalize.Run (xl ++ω xs) ss ∧ ss 0 = some s ∧ ss xl.length = some t

Any finite execution of the original NA can be extended to an infinite execution of NA.totalize, provided that the alphabet is inbabited.

theorem Cslib.Automata.NA.FinAcc.totalize_language_eq {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} : Acceptor.language { toNA := na.totalize, accept := some '' na.accept } = Acceptor.language na

NA.totalize and the original NA accept the same language of finite words, as long as the accepting states are also lifted in the obvious way.