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

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

use log::trace;
use machine_check_common::iir::property::ISubpropertyNext;
use machine_check_common::{ExecError, StateId};

use crate::model_check::property_checker::labelling_updater::LabellingUpdater;
use crate::model_check::property_checker::value::TimedCheckValue;
use crate::FullMachine;

impl<M: FullMachine> LabellingUpdater<'_, M> {
    pub(super) fn update_next_labelling(
        &mut self,
        op: &ISubpropertyNext,
    ) -> Result<BTreeMap<StateId, TimedCheckValue>, ExecError> {
        let inner_updated = self.update_labelling(op.inner, true)?;

        trace!("Updating next labelling");

        let mut result = BTreeMap::new();

        let states = BTreeSet::from_iter(inner_updated.keys().copied());

        for state_id in states {
            for predecessor_id in self.space.direct_predecessor_iter(state_id.into()) {
                let Ok(predecessor_id) = StateId::try_from(predecessor_id) else {
                    // skip root node
                    continue;
                };

                let predecessor_value =
                    self.getter()
                        .apply_next(op, predecessor_id.into(), &mut BTreeMap::new())?;
                result.insert(predecessor_id, predecessor_value);
            }
        }

        Ok(result)
    }
}