Module mikino_api::check

Types and helpers to check a transition system.

Re-exports

pub use cexs::Cexs;

Modules

cexs

Counterexample extraction.

Structs

Base

Base (init) checker.

BaseRes

Result of a base check, simply wraps a CheckRes.

Bmc

Bounded Model Checker.

BmcRes

Result of a BMC check, simply wraps a CheckRes.

CheckRes

Aggregrates properties that are considered “ok” and properties that have been falsified.

InternalChecker

Internal version of a checker.

NegExpr

Internal mini structure to represent the negation of a borrowed expression.

Step

Step (trans) checker.

StepRes

Result of a step check, simply wraps a CheckRes.