machine-check-exec 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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140

mod deduce;
mod nonincremental;
mod property_checker;

use std::collections::{BTreeMap, BTreeSet, HashMap};

use log::trace;
use machine_check_common::{
    check::{Conclusion, KnownConclusion},
    iir::{description::IMachine, property::IProperty},
    ExecError, ParamValuation, StateId,
};
use mck::concr::FullMachine;

use crate::{model_check::property_checker::PropertyChecker, space::StateSpace};

use std::fmt::Debug;

#[derive(Debug)]
/// Three-valued model checker.
pub struct ThreeValuedChecker {
    property_checkers: HashMap<IProperty, PropertyChecker>,
}

impl ThreeValuedChecker {
    pub fn new() -> Self {
        Self {
            property_checkers: HashMap::new(),
        }
    }

    pub fn get_labellings<M: FullMachine>(
        &mut self,
        machine: &IMachine,
        space: &StateSpace<M>,
        property: &IProperty,
    ) -> Result<BTreeMap<usize, BTreeMap<StateId, ParamValuation>>, ExecError> {
        let property_checker = self
            .property_checkers
            .get_mut(property)
            .expect("Property checker should be inserted after the property was checked");

        // get the labellings as well
        let mut labellings = BTreeMap::<usize, BTreeMap<StateId, ParamValuation>>::new();
        for subproperty_index in 0..property.num_subproperties() {
            let labelling = labellings.entry(subproperty_index).or_default();

            for state_id in space.states() {
                let timed = property_checker
                    .last_getter(machine, space)
                    .compute_latest_timed(subproperty_index, state_id)?;
                labelling.insert(state_id, timed.value.valuation());
            }
        }

        Ok(labellings)
    }

    /// Model-checks a mu-calculus proposition.
    pub fn check_property<M: FullMachine>(
        &mut self,
        space: &StateSpace<M>,
        machine: &IMachine,
        property: &IProperty,
    ) -> Result<Conclusion, ExecError> {
        trace!("Checking property {:#?}", property);

        if !self.property_checkers.contains_key(property) {
            self.property_checkers
                .insert(property.clone(), PropertyChecker::new(property.clone()));
        }

        let property_checker = self
            .property_checkers
            .get_mut(property)
            .expect("Property checker should be just inserted");

        let result = property_checker.compute_interpretation(machine, space)?;

        if !space.is_valid() {
            return Ok(Conclusion::NotCheckable);
        }

        if result.is_known() {
            // double-check known result using the incremental algorithm non-incrementally
            property_checker.double_check(machine, space)?;

            // triple-check known result using the non-incremental algorithm
            let basic_result = nonincremental::check_property(space, machine, property)?;
            if result != basic_result {
                panic!(
                    "Result {:?} does not match the result of basic non-incremental algorithm {:?}",
                    result, basic_result
                );
            }
        }

        // compute optimistic and pessimistic interpretation and get the conclusion from that
        match result {
            ParamValuation::False => Ok(Conclusion::Known(KnownConclusion::False)),
            ParamValuation::True => Ok(Conclusion::Known(KnownConclusion::True)),
            ParamValuation::Dependent => Ok(Conclusion::Known(KnownConclusion::Dependent)),
            ParamValuation::Unknown => Ok(Conclusion::Unknown(deduce::deduce_culprit(
                property_checker,
                space,
                machine,
                property,
            )?)),
        }
    }

    pub fn declare_regeneration<M: FullMachine>(
        &mut self,
        space: &StateSpace<M>,
        new_states: &BTreeSet<StateId>,
        changed_successors: &BTreeSet<StateId>,
    ) {
        let mut open_states = new_states.clone();
        open_states.extend(changed_successors.iter().cloned());

        let purge_states = open_states;

        trace!(
            "Declaring regeneration, new states: {:?}, changed successors: {:?}, purging states: {:?}",
            new_states,
            changed_successors,
            purge_states
        );

        for property_checker in self.property_checkers.values_mut() {
            property_checker.purge_states(space, &purge_states);
        }
    }

    pub fn remove_states(&mut self, removed_states: &BTreeSet<StateId>) {
        for property_checker in self.property_checkers.values_mut() {
            property_checker.remove_states(removed_states);
        }
    }
}