Documentation

EventStructures.Family.Rollback

Rollback #

A rollback is a maximal subconfiguration omitting an event. Existence and uniqueness need coherence; maximality is stated for any family.

source
def Rollback.isRollback {L : Type u_1} (F : ConfFamily L) (c : F.Conf) (e : F.Event) (m : F.Conf) :
Prop

A rollback of e on c is a maximal configuration m with m ⊆ c and e ∉ m.

Equations
  • Rollback.isRollback F c e m = (↑m ⊆ ↑c ∧ e ∉ ↑m ∧ ∀ (m' : F.Conf), ↑m' ⊆ ↑c → e ∉ ↑m' → ↑m ⊆ ↑m' → ↑m' ⊆ ↑m)
Instances For
    source
    def Rollback.Rollbacks {L : Type u_1} (F : ConfFamily L) (c : F.Conf) (e : F.Event) :
    Set F.Conf

    The set of all rollbacks of event e on configuration c.

    Equations
    Instances For
      source
      def Rollback.RollbackCandidates {L : Type u_1} (F : ConfFamily L) (c : F.Conf) (e : F.Event) :
      Set F.Conf

      Candidate configurations for rollback.

      Equations
      Instances For
        source
        @[simp]
        theorem Rollback.rollback_subset {L : Type u_1} (F : ConfFamily L) {c : F.Conf} {e : F.Event} {m : F.Conf} (h : isRollback F c e m) :
        ↑m ⊆ ↑c
        source
        @[simp]
        theorem Rollback.rollback_not_mem {L : Type u_1} (F : ConfFamily L) {c : F.Conf} {e : F.Event} {m : F.Conf} (h : isRollback F c e m) :
        e ∉ ↑m
        source
        theorem Rollback.rollback_maximal {L : Type u_1} (F : ConfFamily L) {c : F.Conf} {e : F.Event} {m : F.Conf} (h : isRollback F c e m) (m' : F.Conf) :
        ↑m' ⊆ ↑c → e ∉ ↑m' → ↑m ⊆ ↑m' → ↑m' ⊆ ↑m
        source
        theorem Rollback.isRollback_iff_maximal {L : Type u_1} (F : ConfFamily L) {c : F.Conf} {e : F.Event} {m : F.Conf} :
        isRollback F c e m ↔ m ∈ RollbackCandidates F c e ∧ ∀ m' ∈ RollbackCandidates F c e, ↑m ⊆ ↑m' → ↑m' ⊆ ↑m
        source
        def Rollback.rollbackSet {L : Type u_1} (F : ConfFamily L) (c : F.Conf) (e : F.Event) :
        Set F.Event

        The union of all subconfigurations of c omitting e.

        Equations
        Instances For
          source
          theorem Rollback.rollbackSet_subset {L : Type u_1} (F : ConfFamily L) (c : F.Conf) (e : F.Event) :
          rollbackSet F c e ⊆ ↑c
          source
          theorem Rollback.rollbackSet_not_mem {L : Type u_1} (F : ConfFamily L) (c : F.Conf) (e : F.Event) :
          e ∉ rollbackSet F c e
          source
          theorem Rollback.subset_rollbackSet {L : Type u_1} (F : ConfFamily L) {c m : F.Conf} {e : F.Event} (hmc : ↑m ⊆ ↑c) (hem : e ∉ ↑m) :
          ↑m ⊆ rollbackSet F c e