Termination of LTS

def Cslib.LTS.MayTerminate {State : Type u} {Label : Type v} (lts : LTS State Label) (Terminated : State → Prop) (s : State) : Prop

A state 'may terminate' if it can reach a terminated state. The definition of Terminated is a parameter.

Equations

• lts.MayTerminate Terminated s = ∃ (s' : State), Terminated s' ∧ lts.CanReach s s'

def Cslib.LTS.Stuck {State : Type u} {Label : Type v} (lts : LTS State Label) (Terminated : State → Prop) (s : State) : Prop

A state 'is stuck' if it is not terminated and cannot go forward. The definition of Terminated is a parameter.

Equations

• lts.Stuck Terminated s = (¬Terminated s ∧ ¬∃ (μ : Label) (s' : State), lts.Tr s μ s')