machine-check-common 0.7.1

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58

//! Common structures concerning model-checking.
use std::{collections::VecDeque, fmt::Display};

use serde::{Deserialize, Serialize};

use mck::refin::RefinementValue;

use crate::StateId;

#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub enum KnownConclusion {
    False,
    True,
    Dependent,
}

/// Three-valued model-checking result.
///
/// If the result is unknown, the culprit is given.
#[derive(Debug, Clone, Hash, Serialize, Deserialize)]
pub enum Conclusion {
    Known(KnownConclusion),
    Unknown(Culprit),
    NotCheckable,
}

/// The culprit of an unknown three-valued model-checking result.
///
/// Comprises of a path and an atomic property which is unknown in the last
/// state of the path.
#[derive(Debug, Clone, Hash, Serialize, Deserialize)]
pub struct Culprit {
    pub path: VecDeque<StateId>,
    //pub atomic_property: AtomicProperty,
    pub result: RefinementValue,
    pub panic: RefinementValue,
}

impl KnownConclusion {
    pub fn try_into_bool(self) -> Option<bool> {
        match self {
            KnownConclusion::False => Some(false),
            KnownConclusion::True => Some(true),
            KnownConclusion::Dependent => None,
        }
    }
}

impl Display for KnownConclusion {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        let str = match self {
            KnownConclusion::False => "false",
            KnownConclusion::True => "true",
            KnownConclusion::Dependent => "dependent",
        };
        write!(f, "{}", str)
    }
}