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

Extract the configuration from a computation.

Equations

• Replay.conf es σ = σ.fst

def 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

• Replay.isMinReplay es l σ = (Log.compatibleWithLog es σ l ∧ ∀ (σ' : Computations es), Log.compatibleWithLog es σ' l → ↑(Replay.conf es σ) ⊆ ↑(Replay.conf es σ'))

def 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

• Replay.isMaxReplay es l σ = (Log.compatibleWithLog es σ l ∧ ∀ (σ' : Computations es), Log.compatibleWithLog es σ' l → ↑(Replay.conf es σ') ⊆ ↑(Replay.conf es σ))

def Replay.downset (es : EventStructure) (e : es.Event) : Set es.Event

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

Equations

• Replay.downset es e = {x : es.Event | x ≤ e}

def 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

• Replay.minReplaySet es l = ⋃ e ∈ l, Replay.downset es e

def 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

• Replay.maxReplaySet es l = Replay.minReplaySet es l ∪ {e : es.Event | ∀ (e₁ e₂ : es.Event), es.minimalConflict e₁ e₂ ∧ e₁ ≤ e → e₁ ∈ l}

theorem 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.

theorem Replay.minReplaySet_contains_log (es : EventStructure) {l : Set es.Event} : l ⊆ minReplaySet es l

The minimum replay set contains the log.

theorem 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.

theorem 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.

theorem 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.

theorem 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.

theorem 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.

theorem 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.

theorem 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.

theorem 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.

theorem 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 σ

The minimum replay always exists when there exists a computation reaching the minimum replay set that is compatible with the log. The minimality follows directly from minReplaySet_is_minimal_replay.

theorem 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 σ

The maximum replay always exists when there exists a computation reaching the maximum replay set that is compatible with the log. The maximality follows directly from maxReplaySet_is_maximal_replay.

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

All minimal replays of a log are trace-equivalent. They have the same configuration, so they represent the same point in the quotient of paths by trace equivalence.

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

All maximal replays of a log are trace-equivalent. They have the same configuration, so they represent the same point in the quotient of paths by trace equivalence.