Documentation

LeanPool.EventStructures.Replay

Replay #

This module defines minimal and maximal replays of a log, the minimum and maximum replay sets, and proves that the minimum (resp. maximum) replay set is the smallest (resp. largest) configuration compatible with a log, together with uniqueness of minimal and maximal replays and conditional existence lemmas: existence is established relative to a computation compatible with the log that reaches the corresponding replay set, not unconditionally.

source
def EventStructures.Replay.conf (es : EventStructure) (σ : Computations es) :
Conf es

Extract the configuration from a computation.

Equations
Instances For
    source
    def EventStructures.Replay.isMinReplay (es : EventStructure) (l : Set es.Event) (σ : Computations es) :
    Prop

    A computation is a minimal replay of a log if it's compatible (σ ⊨ l) and its configuration is a subset of all other compatible computations.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def EventStructures.Replay.isMaxReplay (es : EventStructure) (l : Set es.Event) (σ : Computations es) :
      Prop

      A computation is a maximal replay of a log if it's compatible (σ ⊨ l) and all other compatible computations' configurations are subsets of it.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def EventStructures.Replay.downset (es : EventStructure) (e : es.Event) :
        Set es.Event

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

        Equations
        Instances For
          source
          def EventStructures.Replay.minReplaySet (es : EventStructure) (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 EventStructures.Replay.maxReplaySet (es : EventStructure) (l : Set es.Event) :
            Set es.Event

            The maximum replay set of a log l: the minimum replay set plus all events that are causally forced if any of their minimal conflicts (e₁ ## e₂) are in the log.

            Equations
            Instances For
              source
              theorem EventStructures.Replay.downset_closed (es : EventStructure) {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 EventStructures.Replay.minReplaySet_contains_log (es : EventStructure) {l : Set es.Event} :
              l ⊆ minReplaySet es l

              The minimum replay set contains the log.

              source
              theorem EventStructures.Replay.minReplaySet_closed (es : EventStructure) {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 EventStructures.Replay.minReplaySet_subset_maxReplaySet (es : EventStructure) {l : Set es.Event} :
              minReplaySet es l ⊆ maxReplaySet es l

              The maximum replay set contains the minimum replay set.

              source
              theorem EventStructures.Replay.downset_compatible_with_log (es : EventStructure) {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'

              If e is in l and x ≤ e, and l is conflict-free, then x is compatible with all events in l.

              source
              theorem EventStructures.Replay.minReplaySet_compatible_with_log (es : EventStructure) {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 EventStructures.Replay.minReplaySet_is_minimal_replay (es : EventStructure) {l : Set es.Event} {σ : Computations es} (h_conf : ↑(conf es σ) = minReplaySet es l) (h_compat : Log.compatibleWithLog es σ l) :
              isMinReplay es l σ

              The minimum replay set is the smallest configuration compatible with a log. Any computation with configuration equal to minReplaySet is a minimal replay.

              source
              theorem EventStructures.Replay.maxReplaySet_is_maximal_replay (es : EventStructure) {l : Set es.Event} {σ : Computations es} (h_conf : ↑(conf es σ) = maxReplaySet es l) (h_compat : Log.compatibleWithLog es σ l) :
              isMaxReplay es l σ

              The maximum replay set is the largest configuration compatible with a log. Any computation with configuration equal to maxReplaySet is a maximal replay.

              source
              theorem EventStructures.Replay.minReplay_unique_config (es : EventStructure) {l : Set es.Event} {σ₁ σ₂ : Computations es} (h₁ : isMinReplay es l σ₁) (h₂ : isMinReplay es l σ₂) :
              ↑(conf es σ₁) = ↑(conf es σ₂)

              Any two minimal replays of a log have equal configurations. Since both are minimal, each configuration is a subset of the other by definition.

              source
              theorem EventStructures.Replay.maxReplay_unique_config (es : EventStructure) {l : Set es.Event} {σ₁ σ₂ : Computations es} (h₁ : isMaxReplay es l σ₁) (h₂ : isMaxReplay es l σ₂) :
              ↑(conf es σ₁) = ↑(conf es σ₂)

              Any two maximal replays of a log have equal configurations. Since both are maximal, each configuration is a superset of the other by definition.

              source
              theorem EventStructures.Replay.minReplay_exists (es : EventStructure) (l : Set es.Event) (hexists : ∃ (σ : Computations es), ↑(conf es σ) = minReplaySet es l ∧ Log.compatibleWithLog es σ l) :
              ∃ (σ : Computations es), isMinReplay es l σ

              Conditional existence of the minimal replay: if some computation compatible with the log reaches the minimum replay set, then a minimal replay exists. This is a characterization lemma, not an unconditional existence theorem; minimality follows from minReplaySet_is_minimal_replay.

              source
              theorem EventStructures.Replay.maxReplay_exists (es : EventStructure) (l : Set es.Event) (hexists : ∃ (σ : Computations es), ↑(conf es σ) = maxReplaySet es l ∧ Log.compatibleWithLog es σ l) :
              ∃ (σ : Computations es), isMaxReplay es l σ

              Conditional existence of the maximal replay: if some computation compatible with the log reaches the maximum replay set, then a maximal replay exists. This is a characterization lemma, not an unconditional existence theorem; maximality follows from maxReplaySet_is_maximal_replay.

              source
              theorem EventStructures.Replay.minReplay_unique (es : EventStructure) {l : Set es.Event} {σ₁ σ₂ : Computations es} (h₁ : isMinReplay es l σ₁) (h₂ : isMinReplay es l σ₂) :
              conf es σ₁ = conf es σ₂

              Uniqueness of the minimal replay: any two minimal replays of a log reach the same configuration.

              source
              theorem EventStructures.Replay.maxReplay_unique (es : EventStructure) {l : Set es.Event} {σ₁ σ₂ : Computations es} (h₁ : isMaxReplay es l σ₁) (h₂ : isMaxReplay es l σ₂) :
              conf es σ₁ = conf es σ₂

              Uniqueness of the maximal replay: any two maximal replays of a log reach the same configuration.