Stable families

Bounded intersections of configurations are configurations. Hence each event of a configuration has a least history inside it, which makes rollback and least/greatest replay well defined.

def Stable {L : Type u_1} (F : ConfFamily L) : Prop

Configurations bounded by a common configuration are closed under intersection.

Equations

• Stable F = ∀ {S : Set (Set F.Event)} {z : Set F.Event}, S.Nonempty → (∀ x ∈ S, F.Config x) → F.Config z → (∀ x ∈ S, x ⊆ z) → F.Config (⋂₀ S)

def Coherent {L : Type u_1} (F : ConfFamily L) : Prop

Configurations bounded by a common configuration are closed under union.

Equations

• Coherent F = ∀ {S : Set (Set F.Event)} {z : Set F.Event}, (∀ x ∈ S, F.Config x) → F.Config z → (∀ x ∈ S, x ⊆ z) → F.Config (⋃₀ S)

theorem GES.coherent {L : Type u_1} (G : GES L) : Coherent G.toFamily

Every general event structure is coherent.

theorem SES.stable {L : Type u_1} (S : SES L) : Stable S.toFamily

Every stable event structure is stable.

theorem PES.coherent {L : Type u_1} (P : PES L) : Coherent P.toFamily

Every prime event structure is coherent.

theorem PES.stable {L : Type u_1} (P : PES L) : Stable P.toFamily

Every prime event structure is stable.

def Stable.hist {L : Type u_1} (F : ConfFamily L) (c : Set F.Event) (x : F.Event) : Set F.Event

The least subconfiguration of c containing x: its history inside c.

Equations

• Stable.hist F c x = ⋂₀ {m : Set F.Event | F.Config m ∧ m ⊆ c ∧ x ∈ m}

theorem Stable.hist_subset {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {x : F.Event} (hc : F.Config c) (hx : x ∈ c) : hist F c x ⊆ c

theorem Stable.hist_mem {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {x : F.Event} : x ∈ hist F c x

theorem Stable.hist_least {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {x : F.Event} {m : Set F.Event} (hm : F.Config m) (hmc : m ⊆ c) (hxm : x ∈ m) : hist F c x ⊆ m

Any subconfiguration of c containing x contains its history.

theorem Stable.hist_config {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {x : F.Event} (hF : Stable F) (hc : F.Config c) (hx : x ∈ c) : F.Config (hist F c x)

The history is itself a configuration, because of stability.