@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.FiniteLTS.StateSet (State : Type v) : Type v

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.StateSet State = EqCheckingAbstractInterpretation.FiniteEvaluator.FSet State

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.FiniteLTS.ReadyConfig (State : Type v) : Type v

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.ReadyConfig State = EqCheckingAbstractInterpretation.FiniteEvaluator.StateConfig State

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.FiniteLTS.CapabilityConfig (State : Type v) : Type v

Equations

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

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.FiniteLTS.CapabilityTable (State : Type v) : Type v

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.CapabilityTable State = List (EqCheckingAbstractInterpretation.Ready.FiniteLTS.CapabilityConfig State)

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.FiniteLTS.shift {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (competitors : StateSet State) (action : Action) : StateSet State

Shift a finite competitor set through one action.

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.shift lts competitors action = EqCheckingAbstractInterpretation.FiniteEvaluator.shift lts competitors action

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.FiniteLTS.configMem {State : Type v} [DecidableEq State] (config : ReadyConfig State) (configs : List (ReadyConfig State)) : Bool

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.configMem config configs = EqCheckingAbstractInterpretation.FiniteEvaluator.configMem config configs

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.configInsert {State : Type v} [DecidableEq State] (config : ReadyConfig State) (configs : List (ReadyConfig State)) : List (ReadyConfig State)

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.configUnion {State : Type v} [DecidableEq State] (left right : List (ReadyConfig State)) : List (ReadyConfig State)

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.capLeBool : Capability → Capability → Bool

Boolean capability order, aligned with capLe.

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.capLeBool EqCheckingAbstractInterpretation.Ready.Capability.T x✝ = true
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.capLeBool EqCheckingAbstractInterpretation.Ready.Capability.S EqCheckingAbstractInterpretation.Ready.Capability.S = true
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.capLeBool EqCheckingAbstractInterpretation.Ready.Capability.S EqCheckingAbstractInterpretation.Ready.Capability.RS = true
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.capLeBool EqCheckingAbstractInterpretation.Ready.Capability.F EqCheckingAbstractInterpretation.Ready.Capability.F = true
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.capLeBool EqCheckingAbstractInterpretation.Ready.Capability.F EqCheckingAbstractInterpretation.Ready.Capability.RS = true
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.capLeBool EqCheckingAbstractInterpretation.Ready.Capability.RS EqCheckingAbstractInterpretation.Ready.Capability.RS = true
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.capLeBool x✝¹ x✝ = false

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilities : List Capability

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityConfigMem {State : Type v} [DecidableEq State] (config : CapabilityConfig State) : CapabilityTable State → Bool

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityConfigMem config [] = false

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.markedAt {State : Type v} [DecidableEq State] (marked : CapabilityTable State) (config : ReadyConfig State) (threshold : Capability) : Bool

A capability holds at a configuration when some derived requirement is below it.

Equations

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

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.FiniteLTS.Assignment (Action : Type u) : Type u

All ways to assign each competitor either to the negative set or a positive branch.

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.Assignment Action = List (Option (ℕ × Action × EqCheckingAbstractInterpretation.Ready.Capability))

structure EqCheckingAbstractInterpretation.Ready.FiniteLTS.Branch (Action : Type u) (State : Type v) : Type (max u v)

• slot : ℕ
• action : Action
• capability : Capability
• competitors : StateSet State

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentChoices {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (slots : List ℕ) : List (Option (ℕ × Action × Capability))

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentsWithSlots {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (slots : List ℕ) : List State → List (Assignment Action)

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentsWithSlots lts slots [] = [[]]

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.competitorsOf {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (competitors : StateSet State) : List State

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.competitorsOf lts competitors = List.filter (fun (state : State) => decide (state ∈ competitors)) lts.states

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignments {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (competitors : StateSet State) : List (Assignment Action)

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentsAny {Action : Type u} {State : Type v} (choices : List (Option (ℕ × Action × Capability))) : List State → (Assignment Action → Bool) → Bool

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentsAny choices [] x✝ = x✝ []

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentWellFormed {Action : Type u} [DecidableEq Action] : Assignment Action → Bool

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentWellFormed [] = true
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentWellFormed (none :: assignments) = EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentWellFormed assignments

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.wellFormedAssignmentsAny {Action : Type u} {State : Type v} [DecidableEq Action] (choices : List (Option (ℕ × Action × Capability))) : List State → (Assignment Action → Bool) → Bool

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.wellFormedAssignmentsAny choices [] x✝ = x✝ []

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchInsert {Action : Type u} {State : Type v} [DecidableEq State] (slot : ℕ) (action : Action) (capability : Capability) (competitor : State) : List (Branch Action State) → List (Branch Action State)

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchInsert slot action capability competitor [] = [{ slot := slot, action := action, capability := capability, competitors := {competitor} }]

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentBranches {Action : Type u} {State : Type v} [DecidableEq State] : List State → Assignment Action → List (Branch Action State)

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentBranches [] [] = []
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentBranches x✝¹ x✝ = []

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.negativeCompetitors {Action : Type u} {State : Type v} : List State → Assignment Action → List State

Competitors assigned to the negative side of a Ready partition.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.negativeCompetitors x✝¹ x✝ = []

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchCapabilities {Action : Type u} {State : Type v} : List (Branch Action State) → Capability

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchCapabilities [] = EqCheckingAbstractInterpretation.Ready.Capability.T

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchesRequirement {Action : Type u} {State : Type v} (negative : List Action) (branches : List (Branch Action State)) : Capability

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.negativeAssignmentValid {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (competitors : List State) (negative : List Action) : Assignment Action → Bool

Verify the negative-group obligation of a finite Ready partition.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.negativeAssignmentValid lts competitors negative [] = competitors.isEmpty
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.negativeAssignmentValid lts [] negative (none :: assignments) = false
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.negativeAssignmentValid lts [] negative (some val :: assignments) = false

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchesValid {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (marked : CapabilityTable State) (state : State) : List (Branch Action State) → Bool

Verify all positive-branch obligations of a finite Ready partition.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchesValid lts marked state [] = true

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.marks {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (marked : CapabilityTable State) (config : ReadyConfig State) (capability : Capability) : Bool

Does one symbolic Ready step derive precisely the requested capability?

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.marks.refuses {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (negative : List Action) : Bool

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.marks.refuses lts state negative = negative.all fun (action : Action) => (lts.next state action).isEmpty

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.refusalChoices {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) : List (List Action)

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.refusalChoices lts state = [[], List.filter (fun (action : Action) => (lts.next state action).isEmpty) lts.actions]

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.marksWithRefusals {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (marked : CapabilityTable State) (config : ReadyConfig State) (capability : Capability) : Bool

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.configSuccessors {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (config : ReadyConfig State) : List (ReadyConfig State)

Direct successors needed by all finite partitions at a Ready configuration.

Equations

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

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.FiniteLTS.configUniverse {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) : List (ReadyConfig State)

All state-and-competitor configurations expressible by the finite LTS.

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.configUniverse lts = EqCheckingAbstractInterpretation.FiniteEvaluator.configUniverse lts

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.expandConfigs {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (configs : List (ReadyConfig State)) : List (ReadyConfig State)

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigsN {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : ℕ → List (ReadyConfig State)

Repeatedly close a query configuration under one Ready successor-expansion round.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigsN lts state competitors 0 = [(state, competitors)]

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigsUntil {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) : ℕ → List (ReadyConfig State) → List (ReadyConfig State)

Stop expanding the query domain when one round discovers no new configurations.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigsUntil lts 0 x✝ = x✝

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigs {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : List (ReadyConfig State)

Derivative-closed finite domain needed to evaluate one process-versus-set query.

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityConfigs {State : Type v} [DecidableEq State] (configs : List (ReadyConfig State)) : List (CapabilityConfig State)

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityTableUntil {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (configs : List (CapabilityConfig State)) : ℕ → CapabilityTable State → CapabilityTable State

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityTableUntil lts configs 0 x✝ = x✝

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityTable {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : CapabilityTable State

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.minimalCapabilities {State : Type v} [DecidableEq State] (marked : CapabilityTable State) (config : ReadyConfig State) : List Capability

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.prunedCapabilityStep {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (domain : List (CapabilityConfig State)) (marked : CapabilityTable State) : CapabilityTable State

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.minimalCapabilitiesUntil {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (domain : List (CapabilityConfig State)) (config : ReadyConfig State) : ℕ → CapabilityTable State → List Capability

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.FiniteLTS.minimalCapabilitiesUntil lts domain config 0 x✝ = EqCheckingAbstractInterpretation.Ready.FiniteLTS.minimalCapabilities x✝ config

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.readyCapabilities {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : List Capability

Finite exact-capability query for the symbolic Ready transformer. The result is the minimal antichain of capability requirements derived at the query.

Equations

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

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.failsAt {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (threshold : Capability) (state : State) (competitors : StateSet State) : Bool

Does the finite capability result refute the given threshold preorder?

Equations

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