machine_check_common/
check.rs

1//! Common structures concerning model-checking.
2use std::{collections::VecDeque, fmt::Display};
3
4use serde::{Deserialize, Serialize};
5
6use crate::{
7    property::{AtomicProperty, Property},
8    StateId,
9};
10
11/// A Computation Tree Logic property prepared for model-checking.
12#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash)]
13pub struct PreparedProperty {
14    original: Property,
15    prepared: Property,
16}
17
18impl PreparedProperty {
19    /// Turns the CTL proposition into a form suitable for three-valued checking.
20    ///
21    /// The proposition must be first converted to Positive Normal Form so that
22    /// negations are turned into complementary literals, then converted to
23    /// Existential Normal Form. This way, the complementary literals can be used
24    /// for optimistic/pessimistic labelling while a normal ENF model-checking
25    /// algorithm can be used.
26    pub fn new(original_prop: Property) -> Self {
27        // transform proposition to positive normal form to move negations to literals
28        let prop = original_prop.pnf();
29        // transform proposition to existential normal form to be able to verify
30        let prop = prop.enf();
31        PreparedProperty {
32            original: original_prop,
33            prepared: prop,
34        }
35    }
36
37    pub fn original(&self) -> &Property {
38        &self.original
39    }
40
41    pub fn prepared(&self) -> &Property {
42        &self.prepared
43    }
44}
45
46impl Display for PreparedProperty {
47    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
48        // the prepared property is just a reformulation of the original
49        write!(f, "{}", self.original)
50    }
51}
52
53/// Three-valued model-checking result.
54///
55/// If the result is unknown, the culprit is given.
56#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
57pub enum Conclusion {
58    Known(bool),
59    Unknown(Culprit),
60    NotCheckable,
61}
62
63/// The culprit of an unknown three-valued model-checking result.
64///
65/// Comprises of a path and an atomic property which is unknown in the last
66/// state of the path.
67#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
68pub struct Culprit {
69    pub path: VecDeque<StateId>,
70    pub atomic_property: AtomicProperty,
71}
machine_check_common/check.rs

machine_check_common/
check.rs
