@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.FiniteEvaluator.FSet (Element : Type u) : Type u

Mathematical finite sets, with extensional equality and library support.

Equations

• EqCheckingAbstractInterpretation.FiniteEvaluator.FSet Element = Finset Element

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.FiniteEvaluator.StateConfig (State : Type v) : Type v

Equations

• EqCheckingAbstractInterpretation.FiniteEvaluator.StateConfig State = (State × EqCheckingAbstractInterpretation.FiniteEvaluator.FSet State)

def EqCheckingAbstractInterpretation.FiniteEvaluator.shift {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (competitors : FSet State) (action : Action) : FSet State

Shift a finite competitor set through one action.

Equations

• EqCheckingAbstractInterpretation.FiniteEvaluator.shift lts competitors action = Finset.biUnion competitors fun (state : State) => (lts.next state action).toFinset

def EqCheckingAbstractInterpretation.FiniteEvaluator.configMem {State : Type v} [DecidableEq State] (config : StateConfig State) : List (StateConfig State) → Bool

Equations

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

def EqCheckingAbstractInterpretation.FiniteEvaluator.powerset {Element : Type u_1} [DecidableEq Element] (elements : List Element) : List (FSet Element)

Enumerate all Finset subsets of an ordered finite source list.

Equations

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

def EqCheckingAbstractInterpretation.FiniteEvaluator.configUniverse {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) : List (StateConfig State)

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

Equations

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

def EqCheckingAbstractInterpretation.FiniteEvaluator.listPowerset {Element : Type u_1} (elements : List Element) : List (List Element)

Enumerate list-valued subsets when their ordering is part of the target syntax.

Equations

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

def EqCheckingAbstractInterpretation.FiniteEvaluator.saturateStep {Config : Type u_1} (configs : List Config) (contains : Config → List Config → Bool) (marks : List Config → Config → Bool) (marked : List Config) : List Config

Run an inflationary Boolean fixed-point computation over a finite configuration space. contains may implement an extensional notion of configuration equality.

Equations

• EqCheckingAbstractInterpretation.FiniteEvaluator.saturateStep configs contains marks marked = marked ++ List.filter (fun (config : Config) => !contains config marked && marks marked config) configs

def EqCheckingAbstractInterpretation.FiniteEvaluator.saturateN {Config : Type u_1} (configs : List Config) (contains : Config → List Config → Bool) (marks : List Config → Config → Bool) : ℕ → List Config

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.FiniteEvaluator.saturateN configs contains marks 0 = []

def EqCheckingAbstractInterpretation.FiniteEvaluator.saturate {Config : Type u_1} (configs : List Config) (contains : Config → List Config → Bool) (marks : List Config → Config → Bool) : List Config

Equations

• EqCheckingAbstractInterpretation.FiniteEvaluator.saturate configs contains marks = EqCheckingAbstractInterpretation.FiniteEvaluator.saturateN configs contains marks configs.length