Configurations

A configuration of an event structure is a conflict-free, downward-closed set of events. This module defines configurations (and their finite variant), the enabling relation between a configuration and an event, and proves that enabling an event extends a configuration.

def EventStructures.isConf (es : EventStructure) (X : Set es.Event) : Prop

A set of events is a configuration if it is conflict-free and downward closed.

Equations

• EventStructures.isConf es X = ((∀ {e₁ e₂ : es.Event}, e₁ ∈ X → e₂ ∈ X → ¬es.conflict e₁ e₂) ∧ ∀ {e e' : es.Event}, e ∈ X → e' ≤ e → e' ∈ X)

def EventStructures.Conf (es : EventStructure) : Type

Type of all configurations of an event structure.

Equations

• EventStructures.Conf es = { X : Set es.Event // EventStructures.isConf es X }

def EventStructures.FinConf (es : EventStructure) : Type

Type of all finite configurations of an event structure.

Equations

• EventStructures.FinConf es = { X : Finset es.Event // EventStructures.isConf es ↑X }

def EventStructures.Configuration.enables (es : EventStructure) (c : Set es.Event) (e : es.Event) : Prop

A configuration c enables an event e if e is fresh (not already in c), e is consistent with all events in c, and the past of e is contained in c. Freshness rules out self-loop edges in the configuration graph.

Equations

• EventStructures.Configuration.enables es c e = (EventStructures.isConf es c ∧ e ∉ c ∧ (∀ e' ∈ c, es.consistent e e') ∧ es.past e ⊆ c)

theorem EventStructures.Configuration.enables_not_mem (es : EventStructure) {c : Set es.Event} {e : es.Event} (h : enables es c e) : e ∉ c

An enabled event is not already in the configuration.

theorem EventStructures.Configuration.enables_extension (es : EventStructure) {c : Set es.Event} {e : es.Event} (h : enables es c e) : isConf es (c ∪ {e})

If a configuration c enables an event e, then c ∪ {e} is also a configuration.