Logs

A log records the choice points of a computation. Compatibility is parametric in the incompatibility relation R.

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

A computation is compatible with a log l when l is contained in it, its events are compatible with l, and every incompatible event it performs is in l.

Equations

• Log.compatibleWithLog F R σ l = ((∀ e ∈ l, e ∈ ↑σ.fst) ∧ (∀ e ∈ ↑σ.fst, ∀ e' ∈ l, ¬R e e') ∧ ∀ e ∈ ↑σ.fst, ∀ (e' : F.Event), R e e' → e ∈ l)

theorem Log.compatibleWithLog_log_subset {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) {σ : Computations F} {l : Set F.Event} (h : compatibleWithLog F R σ l) : l ⊆ ↑σ.fst

theorem Log.compatibleWithLog_consistent {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) {σ : Computations F} {l : Set F.Event} (h : compatibleWithLog F R σ l) {e e' : F.Event} (he : e ∈ ↑σ.fst) (he' : e' ∈ l) : ¬R e e'

theorem Log.compatibleWithLog_conflict_in_log {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) {σ : Computations F} {l : Set F.Event} (h : compatibleWithLog F R σ l) {e e' : F.Event} (he : e ∈ ↑σ.fst) (hconf : R e e') : e ∈ l

def Log.CompatibleComputations {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) (l : Set F.Event) : Type u_2

Computations compatible with a given log.

Equations

• Log.CompatibleComputations F R l = { σ : Computations F // Log.compatibleWithLog F R σ l }

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

The underlying computation.

Equations

• Log.CompatibleComputations.val F R σ = ↑σ

theorem Log.CompatibleComputations.compatible {L : Type u_1} (F : ConfFamily L) (R : F.Event → F.Event → Prop) {l : Set F.Event} (σ : CompatibleComputations F R l) : compatibleWithLog F R (val F R σ) l

The compatibility proof.

def Log.labelLog {L : Type u_1} (F : ConfFamily L) (l : Set F.Event) : Set L

The label image of a log.

Equations

• Log.labelLog F l = F.label '' l

theorem Log.label_mem_labelLog {L : Type u_1} (F : ConfFamily L) {l : Set F.Event} {e : F.Event} (h : e ∈ l) : F.label e ∈ labelLog F l