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

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

use log::trace;

use machine_check_common::iir::property::ISubpropertyFunc;
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_func(
        &mut self,
        op: &ISubpropertyFunc,
    ) -> Result<BTreeMap<StateId, TimedCheckValue>, ExecError> {
        trace!("Updating function labelling");

        let mut labellings = BTreeMap::new();
        let mut updated_states = BTreeSet::new();

        for dependency_index in &op.dependencies {
            let labelling =
                self.update_labelling(*dependency_index, op.children.contains(dependency_index))?;
            updated_states.extend(labelling.keys());
            labellings.insert(*dependency_index, labelling);
        }

        let mut result = BTreeMap::new();

        for state_id in updated_states {
            let value = self.getter().apply_func(op, state_id, &mut labellings)?;
            result.insert(state_id, value);
        }

        Ok(result)
    }
}