Documentation

EventStructures.Stable.Rollback

Rollback for a coherent family #

rollbackSet c e is the union of all subconfigurations of c omitting e. When the family is coherent it is a configuration, hence the greatest such subconfiguration, and rollbacks are unique.

source
theorem Stable.rollbackSet_config {L : Type u_1} {F : ConfFamily L} (hF : Coherent F) (c : F.Conf) (e : F.Event) :
F.Config (Rollback.rollbackSet F c e)

The rollback set is a configuration.

source
def Stable.rollbackConf {L : Type u_1} {F : ConfFamily L} (hF : Coherent F) (c : F.Conf) (e : F.Event) :
F.Conf

The rollback set, as a configuration.

Equations
Instances For
    source
    theorem Stable.rollbackConf_maximum {L : Type u_1} {F : ConfFamily L} (hF : Coherent F) (c : F.Conf) (e : F.Event) (m : F.Conf) (hmc : ↑m ⊆ ↑c) (hem : e ∉ ↑m) :
    ↑m ⊆ ↑(rollbackConf ⋯ c e)

    It is the greatest subconfiguration of c omitting e.

    source
    theorem Stable.isRollback_rollbackConf {L : Type u_1} {F : ConfFamily L} (hF : Coherent F) (c : F.Conf) (e : F.Event) :
    Rollback.isRollback F c e (rollbackConf ⋯ c e)

    Hence it is a rollback.

    source
    theorem Stable.rollback_unique {L : Type u_1} {F : ConfFamily L} (hF : Coherent F) {c : F.Conf} {e : F.Event} {m : F.Conf} (h : Rollback.isRollback F c e m) :
    m = rollbackConf ⋯ c e

    Rollbacks are unique: any rollback is the rollback set.