The LTSI of a configuration family

States are configurations, steps add one enabled fresh event, and independence is the derived diamond condition. The forward LPV axioms hold for any family.

def ConfFamily.esStep {L : Type u_1} (F : ConfFamily L) (c₁ : F.Conf) (a : L) (c₂ : F.Conf) : Prop

Forward step: extend by a fresh enabled event.

Equations

• F.esStep c₁ a c₂ = ∃ (e : F.Event), F.enables (↑c₁) e ∧ e ∉ ↑c₁ ∧ F.label e = a ∧ ↑c₂ = ↑c₁ ∪ {e}

def ConfFamily.esIndep {L : Type u_1} (F : ConfFamily L) (c : F.Conf) (a : L) (c₁ : F.Conf) (b : L) (c₂ : F.Conf) : Prop

Coinitial independence of two labelled steps.

Equations

• F.esIndep c a c₁ b c₂ = ∃ (e₁ : F.Event) (e₂ : F.Event), F.Indep (↑c) e₁ e₂ ∧ e₁ ∉ ↑c ∧ e₂ ∉ ↑c ∧ F.label e₁ = a ∧ F.label e₂ = b ∧ ↑c₁ = ↑c ∪ {e₁} ∧ ↑c₂ = ↑c ∪ {e₂}

def ConfFamily.toLTSI {L : Type u_1} (F : ConfFamily L) : LTSI L

The LTSI of a configuration family.

Equations

• F.toLTSI = { State := F.Conf, init := F.empty, step := F.esStep, indep := F.esIndep }

theorem ConfFamily.toLTSI_LPV {L : Type u_1} (F : ConfFamily L) : F.toLTSI.LPV

The forward LPV axioms hold for every configuration family.