def Blaster.StateMachine.bmcStrategy (smInst : Lean.Expr) : Optimize.TranslateEnvT Unit

Given smInst an instance of StateMachine, perform the BMC strategy for counterexample detection up to Depth maxDepth. In particular, considering k = maxDepth, try to incrementally check if one of the following propositional formulae are satisfied: bmcStrategy(smInst) ≡

• cex(k) ≡ st₀ = init in₀ ∧ (∀ i ∈ [0, k-1], assumptions inᵢ stᵢ ∧ stᵢ₊₁ = next inᵢ stᵢ) ∧ assumptions inₖ stₖ ∧ ¬ invariants inₖ stₖ -- counterexample detection
• contradiction(k) = ∀ i ∈ [0, k], assumptions inᵢ stᵢ -- check for contradictory context

where: inᵢ : set of input variables at step ᵢ stᵢ : set of state variables at step ᵢ

Trigger an error when smInst is not an instance of StateMachine.

Equations

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

partial def Blaster.StateMachine.bmcStrategy.visit (smInst : Lean.Expr) (prevState : Option Lean.Expr) : StateMachineEnvT Unit

def Blaster.StateMachine.bmcStrategy.optimizeState (smInst iVar : Lean.Expr) (pState : Option Lean.Expr) : StateMachineEnvT Lean.Expr

Equations

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

def Blaster.StateMachine.bmcStrategy.analysisAtDepth (smInst iVar state : Lean.Expr) : StateMachineEnvT Smt.Result

Equations

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

def Blaster.StateMachine.bmc : Lean.ParserDescr

Equations

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

def Blaster.StateMachine.bmcCommand (sOpts : Options.BlasterOptions) (stx : Lean.Syntax) : Lean.Elab.TermElabM Unit

Equations

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

def Blaster.StateMachine.bmcImp : Lean.Elab.Command.CommandElab

Equations

• Blaster.StateMachine.bmcImp = Blaster.Syntax.commandInvoker Blaster.StateMachine.bmcCommand