machine_check_exec/
lib.rs

1#![doc = include_str!("../README.md")]
2
3mod framework;
4mod model_check;
5mod precision;
6mod space;
7
8use machine_check_common::iir::property::IProperty;
9use mck::{concr::FullMachine, misc::MetaWrap};
10
11pub use framework::Framework;
12
13/// Abstraction and refinement strategy.
14pub struct Strategy {
15    /// Whether each input should immediately cover only a single concrete input.
16    pub naive_inputs: bool,
17    /// Whether each step output should decay to fully-unknown by default.
18    pub use_decay: bool,
19}
20
21/// Whether we are verifying the inherent property or a standard property.
22pub enum VerificationType {
23    Inherent,
24    Property(IProperty),
25}
26
27type AbstrInput<M> = <<M as FullMachine>::Abstr as mck::abstr::Machine<M>>::Input;
28type AbstrParam<M> = <<M as FullMachine>::Abstr as mck::abstr::Machine<M>>::Param;
29type AbstrState<M> = <<M as FullMachine>::Abstr as mck::abstr::Machine<M>>::State;
30type AbstrPanicState<M> = mck::abstr::PanicResult<AbstrState<M>>;
31
32type WrappedInput<M> = MetaWrap<AbstrInput<M>>;
33type WrappedParam<M> = MetaWrap<AbstrParam<M>>;
34type WrappedState<M> = MetaWrap<AbstrPanicState<M>>;
machine_check_exec/lib.rs

machine_check_exec/
lib.rs
