@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Trace.FiniteLTS.Config (State : Type v) : Type v

Equations

• EqCheckingAbstractInterpretation.Trace.FiniteLTS.Config State = EqCheckingAbstractInterpretation.FiniteEvaluator.StateConfig State

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Trace.FiniteLTS.MarkerTable (State : Type v) : Type v

Equations

• EqCheckingAbstractInterpretation.Trace.FiniteLTS.MarkerTable State = List (EqCheckingAbstractInterpretation.Trace.FiniteLTS.Config State)

def EqCheckingAbstractInterpretation.Trace.FiniteLTS.marks {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (marked : MarkerTable State) (state : State) (competitors : StateSet State) : Bool

Boolean form of the two DTrSharp clauses at one configuration.

Equations

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

def EqCheckingAbstractInterpretation.Trace.FiniteLTS.successors {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) : Config State → MarkerTable State

Equations

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

def EqCheckingAbstractInterpretation.Trace.FiniteLTS.reachUntil {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) : ℕ → MarkerTable State → MarkerTable State

Equations

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

def EqCheckingAbstractInterpretation.Trace.FiniteLTS.reachableConfigs {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (initial : Config State) : MarkerTable State

Equations

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

def EqCheckingAbstractInterpretation.Trace.FiniteLTS.markerTable {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) : MarkerTable State

Saturated Boolean form of DTrSharp over a finite transition system.

Equations

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

def EqCheckingAbstractInterpretation.Trace.FiniteLTS.abstractDiff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : Bool

Executable finite-state approximation of AbstractDiff.

Equations

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

def EqCheckingAbstractInterpretation.Trace.FiniteLTS.abstractDiffReachable {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : Bool

Evaluate one abstract-difference query on its reachable configurations.

Equations

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

def EqCheckingAbstractInterpretation.Trace.FiniteLTS.tracePreordered {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (left_state right_state : State) : Bool

Equations

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