machine_check_common/
lib.rs

1#![doc = include_str!("../README.md")]
2
3use serde::{Deserialize, Serialize};
4use thiserror::Error;
5
6#[derive(Error, Debug, Serialize, Deserialize, Clone)]
7pub enum ExecError {
8    #[error("incomplete verification")]
9    Incomplete,
10    #[error("field '{0}' of bit type not found")]
11    FieldNotFound(String),
12    #[error("property '{0}' part '{1}' could not be lexed")]
13    PropertyNotLexable(String, String),
14    #[error("property '{0}' could not be parsed")]
15    PropertyNotParseable(String),
16    #[error("inherent machine panic")]
17    InherentPanic(String),
18    #[error("{0}")]
19    OtherError(String),
20}
21
22#[derive(Debug, Serialize, Deserialize, Clone)]
23pub struct ExecResult {
24    pub result: Result<bool, ExecError>,
25    pub stats: ExecStats,
26}
27
28#[derive(Debug, Serialize, Deserialize, Clone, Default)]
29pub struct ExecStats {
30    pub num_refinements: usize,
31    pub num_generated_states: usize,
32    pub num_final_states: usize,
33    pub num_generated_transitions: usize,
34    pub num_final_transitions: usize,
35}
machine_check_common/lib.rs

machine_check_common/
lib.rs
