Documentation

EventStructures.Prime.Rollback

source
theorem Rollback.rollback_subset_future {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es.toFamily c e m) :
↑m ⊆ ↑c \ es.future e
source
theorem Rollback.rollback_future_isConf {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} :
isConf es (↑c \ es.future e)

Removing the future of e from a configuration keeps it a configuration.

source
def Rollback.rollbackFuture {L : Type u_1} (es : PES L) (c : Conf es) (e : es.Event) :
Conf es

The canonical rollback configuration: remove all events causally after e.

Equations
Instances For
    source
    @[simp]
    theorem Rollback.rollbackFuture_val {L : Type u_1} (es : PES L) (c : Conf es) (e : es.Event) :
    ↑(rollbackFuture es c e) = ↑c \ es.future e
    source
    @[simp]
    theorem Rollback.rollbackFuture_mem {L : Type u_1} (es : PES L) {c : Conf es} {e x : es.Event} :
    x ∈ ↑(rollbackFuture es c e) ↔ x ∈ ↑c ∧ x ∉ es.future e
    source
    theorem Rollback.rollback_redoable {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} (he : e ∈ ↑c) :
    Configuration.enables es (↑(rollbackFuture es c e)) e

    Redoability: e is enabled in rollback(c,e) when e ∈ c.

    source
    theorem Rollback.rollback_causal_safety {L : Type u_1} (es : PES L) {c : Conf es} {e x : es.Event} :
    x ∈ ↑(rollbackFuture es c e) → x ∉ es.future e

    Causal safety: Rollback removes exactly the causal consequences of e.

    source
    theorem Rollback.rollback_future {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} :
    isRollback es.toFamily c e (rollbackFuture es c e)

    The canonical rollback is a rollback for c and e.

    source
    @[simp]
    theorem Rollback.rollback_eq_future {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es.toFamily c e m) :
    ↑m = ↑c \ es.future e

    Any rollback coincides with the canonical rollback.

    source
    theorem Rollback.rollback_unique {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} {m₁ m₂ : Conf es} (h₁ : isRollback es.toFamily c e m₁) (h₂ : isRollback es.toFamily c e m₂) :
    m₁ = m₂

    Rollbacks are unique when they exist.

    source
    theorem Rollback.rollback_maximum {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es.toFamily c e m) (m' : Conf es) :
    m' ∈ RollbackCandidates es.toFamily c e → ↑m' ⊆ ↑m

    The rollback is the maximum element among rollback candidates.

    source
    theorem Rollback.rollback_correctness_finite {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} (cF : Finset es.Event) (hcF : ∀ (x : es.Event), x ∈ cF ↔ x ∈ ↑c) :
    Nonempty (Path es.toFamily (rollbackFuture es c e) c)

    Correctness: c is reachable from rollback(c,e) when c is finite.

    source
    theorem Rollback.rollback_minimality {L : Type u_1} (es : PES L) [DecidableEq es.Event] {c : Conf es} {e : es.Event} {c' : Conf es} (_hredo : Configuration.enables es (↑c') e) (hsafe : ∀ x ∈ ↑c', x ∉ es.future e) (p' : Path es.toFamily c' c) :
    (↑c ∩ es.future e).ncard ≤ Path.length es.toFamily p'

    Any path from a redo candidate c' to c is at least as long as the number of events of c causally after e.