machine_check_common/
check.rs

1//! Common structures concerning model-checking.
2use std::{collections::VecDeque, fmt::Display};
3
4use serde::{Deserialize, Serialize};
5
6pub use crate::property::Property;
7
8use crate::{property::AtomicProperty, 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, PartialEq, Eq, 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, PartialEq, Eq, Hash, Serialize, Deserialize)]
32pub struct Culprit {
33    pub path: VecDeque<StateId>,
34    pub atomic_property: AtomicProperty,
35}
36
37impl KnownConclusion {
38    pub fn try_into_bool(self) -> Option<bool> {
39        match self {
40            KnownConclusion::False => Some(false),
41            KnownConclusion::True => Some(true),
42            KnownConclusion::Dependent => None,
43        }
44    }
45}
46
47impl Display for KnownConclusion {
48    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
49        let str = match self {
50            KnownConclusion::False => "false",
51            KnownConclusion::True => "true",
52            KnownConclusion::Dependent => "dependent",
53        };
54        write!(f, "{}", str)
55    }
56}
machine_check_common/check.rs

machine_check_common/
check.rs
