Nondeterministic automata with ε-transitions.

structure Cslib.Automata.εNA (State : Type u_1) (Symbol : Type u_2) extends Cslib.Automata.NA State (Option Symbol) : Type (max u_1 u_2)

A nondeterministic finite automaton with ε-transitions (εNA) is an NA with an Option symbol type. The special symbol ε is represented by the Option.none case.

Internally, ε (Option.none) is treated as the τ label of the underlying transition system, allowing for reusing the definitions and results on saturated transitions of LTS to deal with ε-closure.

• Tr : State → Option Symbol → State → Prop
• start : Set State

@[reducible, inline]

abbrev Cslib.Automata.εNA.εClosure {State : Type u_1} {Symbol : Type u_2} (a : εNA State Symbol) (S : Set State) : Set State

The ε-closure of a set of states S is the set of states reachable by any state in S by performing only ε-transitions. We use LTS.τClosure since ε (Option.none) is an instance of HasTau.τ.

Equations

• a.εClosure S = a.τClosure S

structure Cslib.Automata.εNA.FinAcc (State : Type u_3) (Symbol : Type u_4) extends Cslib.Automata.εNA State Symbol : Type (max u_3 u_4)

The finite-word acceptance condition of an εNA is a set of accepting states.

• Tr : State → Option Symbol → State → Prop
• start : Set State
• accept : Set State

  The set of accepting states.

instance Cslib.Automata.εNA.FinAcc.instAcceptor {State : Type u_1} {Symbol : Type u_2} : Acceptor (FinAcc State Symbol) Symbol

An εNA.FinAcc accepts a string if there is a saturated multistep accepting derivative with that trace from the start state.

Equations

• One or more equations did not get rendered due to their size.