machine_check_common/
check.rs

1//! Common structures concerning model-checking.
2use std::{collections::VecDeque, fmt::Display};
3
4use serde::{Deserialize, Serialize};
5
6use mck::refin::RefinementValue;
7
8use crate::StateId;
9
10#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
11pub enum KnownConclusion {
12    False,
13    True,
14    Dependent,
15}
16
17/// Three-valued model-checking result.
18///
19/// If the result is unknown, the culprit is given.
20#[derive(Debug, Clone, Hash, Serialize, Deserialize)]
21pub enum Conclusion {
22    Known(KnownConclusion),
23    Unknown(Culprit),
24    NotCheckable,
25}
26
27/// The culprit of an unknown three-valued model-checking result.
28///
29/// Comprises of a path and an atomic property which is unknown in the last
30/// state of the path.
31#[derive(Debug, Clone, Hash, Serialize, Deserialize)]
32pub struct Culprit {
33    pub path: VecDeque<StateId>,
34    //pub atomic_property: AtomicProperty,
35    pub result: RefinementValue,
36    pub panic: RefinementValue,
37}
38
39impl KnownConclusion {
40    pub fn try_into_bool(self) -> Option<bool> {
41        match self {
42            KnownConclusion::False => Some(false),
43            KnownConclusion::True => Some(true),
44            KnownConclusion::Dependent => None,
45        }
46    }
47}
48
49impl Display for KnownConclusion {
50    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
51        let str = match self {
52            KnownConclusion::False => "false",
53            KnownConclusion::True => "true",
54            KnownConclusion::Dependent => "dependent",
55        };
56        write!(f, "{}", str)
57    }
58}
machine_check_common/check.rs

machine_check_common/
check.rs
