machine-check-gui 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

use indexmap::IndexMap;
use serde::{Deserialize, Serialize};
use std::collections::{BTreeMap, BTreeSet};

use crate::shared::snapshot::log::Log;
use machine_check_common::{
    iir::{path::IIdent, property::IProperty, ty::IElementaryType},
    ExecError, NodeId, ParamValuation, StateId,
};
use mck::abstr::AbstractDisplay;

pub mod log;

/// A snapshot of the current state of machine-check.
///
/// Provided by the backend to the frontend.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct Snapshot {
    pub exec_name: String,
    pub state_space: StateSpace,
    pub state_info: StateInfo,
    pub properties: Vec<PropertySnapshot>,
    pub log: Log,
    pub panic_message: Option<String>,
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct StateInfo {
    pub fields: IndexMap<IIdent, IElementaryType>,
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct StateSpace {
    pub nodes: BTreeMap<NodeId, Node>,
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct Node {
    pub incoming: BTreeSet<NodeId>,
    pub outgoing: BTreeSet<NodeId>,
    pub panic_state: Option<AbstractDisplay>,
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct PropertySnapshot {
    pub property: IProperty,
    pub conclusion: Result<ParamValuation, ExecError>,
    pub labellings: BTreeMap<usize, BTreeMap<StateId, ParamValuation>>,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub struct PropertyIndex(pub usize);

impl Snapshot {
    pub fn new(
        exec_name: String,
        state_space: StateSpace,
        state_info: StateInfo,
        properties: Vec<PropertySnapshot>,
        log: Log,
        panic_message: Option<String>,
    ) -> Self {
        Self {
            exec_name,
            state_space,
            state_info,
            properties,
            log,
            panic_message,
        }
    }

    pub fn last_property_index(&self) -> Option<PropertyIndex> {
        if !self.properties.is_empty() {
            Some(PropertyIndex(self.properties.len() - 1))
        } else {
            None
        }
    }

    pub fn contains_property(&self, property_index: PropertyIndex) -> bool {
        property_index.0 < self.properties.len()
    }

    pub fn contains_subproperty(
        &self,
        property_index: PropertyIndex,
        subproperty_index: usize,
    ) -> bool {
        self.properties
            .get(property_index.0)
            .is_some_and(|property_snapshot| {
                subproperty_index < property_snapshot.property.num_subproperties()
            })
    }

    pub fn subproperty_labellings(
        &self,
        property_index: PropertyIndex,
        subproperty_index: usize,
    ) -> Option<&BTreeMap<StateId, ParamValuation>> {
        self.properties
            .get(property_index.0)
            .and_then(|property_snapshot| property_snapshot.labellings.get(&subproperty_index))
    }

    pub fn property_snapshot(&self, property_index: PropertyIndex) -> &PropertySnapshot {
        &self.properties[property_index.0]
    }

    pub fn property_snapshots(&self) -> &Vec<PropertySnapshot> {
        &self.properties
    }
}