Replay

Least and greatest computations compatible with a log. These are defined only on the family of configurations.

def Replay.conf {L : Type u_1} (F : ConfFamily L) (σ : Computations F) : F.Conf

The target configuration of a computation.

Equations

• Replay.conf F σ = σ.fst

def Replay.isMinReplay {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) (l : Set F.Event) (σ : Computations F) : Prop

A least replay of l: compatible, and contained in every compatible computation.

Equations

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

def Replay.isMaxReplay {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) (l : Set F.Event) (σ : Computations F) : Prop

A greatest replay of l.

Equations

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

theorem Replay.minReplay_unique_config {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) {l : Set F.Event} {σ₁ σ₂ : Computations F} (h₁ : isMinReplay F R l σ₁) (h₂ : isMinReplay F R l σ₂) : ↑(conf F σ₁) = ↑(conf F σ₂)

theorem Replay.maxReplay_unique_config {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) {l : Set F.Event} {σ₁ σ₂ : Computations F} (h₁ : isMaxReplay F R l σ₁) (h₂ : isMaxReplay F R l σ₂) : ↑(conf F σ₁) = ↑(conf F σ₂)

theorem Replay.minReplay_unique {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) {l : Set F.Event} {σ₁ σ₂ : Computations F} (h₁ : isMinReplay F R l σ₁) (h₂ : isMinReplay F R l σ₂) : conf F σ₁ = conf F σ₂

theorem Replay.maxReplay_unique {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) {l : Set F.Event} {σ₁ σ₂ : Computations F} (h₁ : isMaxReplay F R l σ₁) (h₂ : isMaxReplay F R l σ₂) : conf F σ₁ = conf F σ₂

def Replay.LabelEquivComputation {L : Type u_1} (F : ConfFamily L) (σ₁ σ₂ : Computations F) : Prop

Two computations are label-equivalent if their configurations have the same labels.

Equations

• Replay.LabelEquivComputation F σ₁ σ₂ = (F.label '' ↑(Replay.conf F σ₁) = F.label '' ↑(Replay.conf F σ₂))

def Replay.isMinLabelReplay {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) (l : Set F.Event) (σ : Computations F) : Prop

A least replay measured by labels rather than events.

Equations

• One or more equations did not get rendered due to their size.

theorem Replay.isMinReplay_imp_isMinLabelReplay {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) {l : Set F.Event} {σ : Computations F} (h : isMinReplay F R l σ) : isMinLabelReplay F R l σ

A least replay is least on labels too.