Documentation

EventStructures.Prime.Replay

Replay for a prime event structure #

The least/greatest replay sets are built from the causal order and minimal conflict.

source
def Replay.downset {L : Type u_1} (es : PES L) (e : es.Event) :
Set es.Event

The downset (or principal ideal) of an event e: all predecessors including e.

Equations
Instances For
    source
    def Replay.minReplaySet {L : Type u_1} (es : PES L) (l : Set es.Event) :
    Set es.Event

    The minimum replay set of a log l: union of all downsets of events in l.

    Equations
    Instances For
      source
      def Replay.maxReplaySet {L : Type u_1} (es : PES L) (l : Set es.Event) :
      Set es.Event

      The maximum replay set of a log l: the minimum replay set together with the events forced by a minimal conflict in l.

      Equations
      Instances For
        source
        theorem Replay.downset_closed {L : Type u_1} (es : PES L) {e x y : es.Event} (hxy : x ≤ y) (hy : y ∈ downset es e) :
        x ∈ downset es e

        The downset is closed under taking predecessors.

        source
        theorem Replay.minReplaySet_contains_log {L : Type u_1} (es : PES L) {l : Set es.Event} :
        l ⊆ minReplaySet es l

        The minimum replay set contains the log.

        source
        theorem Replay.minReplaySet_closed {L : Type u_1} (es : PES L) {l : Set es.Event} {x y : es.Event} (hy : y ≤ x) (hx : x ∈ minReplaySet es l) :
        y ∈ minReplaySet es l

        The minimum replay set is closed under predecessors.

        source
        theorem Replay.minReplaySet_subset_maxReplaySet {L : Type u_1} (es : PES L) {l : Set es.Event} :
        minReplaySet es l ⊆ maxReplaySet es l

        The maximum replay set contains the minimum replay set.

        source
        theorem Replay.downset_compatible_with_log {L : Type u_1} (es : PES L) {l : Set es.Event} {e x : es.Event} (he : e ∈ l) (hxe : x ≤ e) (hl_conflict_free : ∀ {e₁ e₂ : es.Event}, e₁ ∈ l → e₂ ∈ l → ¬es.conflict e₁ e₂) (e' : es.Event) :
        e' ∈ l → ¬es.conflict x e'

        Below an event of a conflict-free log, every event is compatible with the log.

        source
        theorem Replay.minReplaySet_compatible_with_log {L : Type u_1} (es : PES L) {l : Set es.Event} (hl_conflict_free : ∀ {e₁ e₂ : es.Event}, e₁ ∈ l → e₂ ∈ l → ¬es.conflict e₁ e₂) (x : es.Event) :
        x ∈ minReplaySet es l → ∀ e ∈ l, ¬es.conflict x e

        The minimum replay set is compatible with the log.

        source
        theorem Replay.minReplaySet_is_minimal_replay {L : Type u_1} (es : PES L) {l : Set es.Event} {σ : Computations es.toFamily} (h_conf : ↑(conf es.toFamily σ) = minReplaySet es l) (h_compat : es.compatibleWithLog σ l) :
        isMinReplay es.toFamily es.conflict l σ

        A computation reaching minReplaySet is a minimal replay.

        source
        theorem Replay.maxReplaySet_is_maximal_replay {L : Type u_1} (es : PES L) {l : Set es.Event} {σ : Computations es.toFamily} (h_conf : ↑(conf es.toFamily σ) = maxReplaySet es l) (h_compat : es.compatibleWithLog σ l) :
        isMaxReplay es.toFamily es.conflict l σ

        A computation reaching maxReplaySet is a maximal replay.

        source
        theorem Replay.minReplay_exists {L : Type u_1} (es : PES L) (l : Set es.Event) (hexists : ∃ (σ : Computations es.toFamily), ↑(conf es.toFamily σ) = minReplaySet es l ∧ es.compatibleWithLog σ l) :
        ∃ (σ : Computations es.toFamily), isMinReplay es.toFamily es.conflict l σ

        The least replay exists when some compatible computation reaches minReplaySet.

        source
        theorem Replay.maxReplay_exists {L : Type u_1} (es : PES L) (l : Set es.Event) (hexists : ∃ (σ : Computations es.toFamily), ↑(conf es.toFamily σ) = maxReplaySet es l ∧ es.compatibleWithLog σ l) :
        ∃ (σ : Computations es.toFamily), isMaxReplay es.toFamily es.conflict l σ

        A greatest replay exists once some compatible computation reaches maxReplaySet.

        source
        theorem Replay.downset_isConf {L : Type u_1} (es : PES L) (e : es.Event) :
        isConf es (downset es e)

        The downset is a configuration.

        source
        theorem Replay.hist_eq_downset {L : Type u_1} (es : PES L) {c : Set es.Event} (hc : isConf es c) {x : es.Event} (hx : x ∈ c) :
        Stable.hist es.toFamily c x = downset es x

        Inside a configuration, the history of an event is its downset.

        source
        theorem Replay.replaySet_eq_minReplaySet {L : Type u_1} (es : PES L) {c l : Set es.Event} (hc : isConf es c) (hlc : l ⊆ c) :
        Stable.replaySet es.toFamily c l = minReplaySet es l

        Hence the general least replay set agrees with the prime one.