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

use std::collections::BTreeSet;
use std::sync::LazyLock;

use log::{trace, warn};
use machine_check_common::iir::description::IMachine;
use machine_check_common::ExecError;

use crate::model_check::property_checker::labelling_updater::LabellingUpdater;
use crate::model_check::property_checker::PropertyChecker;
use crate::space::StateSpace;
use crate::FullMachine;

const INCREMENTAL_DOUBLE_CHECK_ENV_VAR: &str = "MACHINE_CHECK_INCREMENTAL_DOUBLE_CHECK";

static INCREMENTAL_DOUBLE_CHECK: LazyLock<bool> = LazyLock::new(|| {
    let Some(should_double_check) = std::env::var_os(INCREMENTAL_DOUBLE_CHECK_ENV_VAR) else {
        return false;
    };

    let result = should_double_check == "1" || should_double_check.eq_ignore_ascii_case("true");
    if result {
        warn!("Double-checking incremental computation due to environment variable '{}'. This will be slow.", INCREMENTAL_DOUBLE_CHECK_ENV_VAR);
    }
    result
});

impl PropertyChecker {
    pub(super) fn incremental_double_check<M: FullMachine>(
        &mut self,
        machine: &IMachine,
        space: &StateSpace<M>,
    ) -> Result<(), ExecError> {
        if !*INCREMENTAL_DOUBLE_CHECK {
            return Ok(());
        }
        self.double_check(machine, space)
    }

    pub fn double_check<M: FullMachine>(
        &self,
        machine: &IMachine,
        space: &StateSpace<M>,
    ) -> Result<(), ExecError> {
        trace!(
            "Double-checking whether the incremental computation corresponds to non-incremental"
        );

        // retain only states in state space for comparison
        // as it is allowed for incremental model checking to retain states
        // that are no longer in the state space
        let states = BTreeSet::from_iter(space.states());

        let mut fresh_property_checker = self.clone();
        fresh_property_checker.invalidate();
        fresh_property_checker.focus.make_whole_dirty(space);
        LabellingUpdater::new(&mut fresh_property_checker, machine, space)?.compute_inner()?;
        for history in fresh_property_checker.histories.values_mut() {
            history.retain_states(&states);
        }

        let mut incremental_property_checker = self.clone();

        for history in incremental_property_checker.histories.values_mut() {
            history.retain_states(&states);
        }

        // squash both as the slack might be different
        incremental_property_checker.squash()?;
        fresh_property_checker.squash()?;

        let computation_inconsistencies =
            fresh_property_checker.computations != incremental_property_checker.computations;
        let history_inconsistencies =
            fresh_property_checker.histories != incremental_property_checker.histories;

        if !computation_inconsistencies && !history_inconsistencies {
            return Ok(());
        }
        eprintln!("Double-checking found inconsistencies in incremental model-checking, current focus: {:?}", incremental_property_checker.focus);
        if computation_inconsistencies {
            eprintln!(
                "Double-checking found inconsistencies in computations\n\
                    Fresh computations: {:#?}\n\
                    Incremental computations: {:#?}",
                fresh_property_checker.computations, incremental_property_checker.computations,
            );
        } else {
            eprintln!(
                "No inconsistencies in computations:\n{:#?}",
                incremental_property_checker.computations,
            );
        }
        if history_inconsistencies {
            eprintln!(
                "Double-checking found inconsistencies in histories\n\
                    Fresh histories: {:#?}\n\
                    Incremental histories: {:#?}",
                fresh_property_checker.histories, incremental_property_checker.histories,
            );
        } else {
            eprintln!(
                "No inconsistencies in histories:\n{:#?}",
                incremental_property_checker.histories,
            );
        }
        panic!(
            "Found inconsistencies when double-checking incremental model checking for property {:?}",
            self.property
        );
    }
}