machine_check_gui/shared/
snapshot.rs

1use indexmap::IndexMap;
2use serde::{Deserialize, Serialize};
3use std::collections::{BTreeMap, BTreeSet};
4
5use crate::shared::snapshot::log::Log;
6use machine_check_common::{
7    iir::{path::IIdent, property::IProperty, ty::IElementaryType},
8    ExecError, NodeId, ParamValuation, StateId,
9};
10use mck::abstr::AbstractDisplay;
11
12pub mod log;
13
14/// A snapshot of the current state of machine-check.
15///
16/// Provided by the backend to the frontend.
17#[derive(Clone, Debug, Serialize, Deserialize)]
18pub struct Snapshot {
19    pub exec_name: String,
20    pub state_space: StateSpace,
21    pub state_info: StateInfo,
22    pub properties: Vec<PropertySnapshot>,
23    pub log: Log,
24    pub panic_message: Option<String>,
25}
26
27#[derive(Clone, Debug, Serialize, Deserialize)]
28pub struct StateInfo {
29    pub fields: IndexMap<IIdent, IElementaryType>,
30}
31
32#[derive(Clone, Debug, Serialize, Deserialize)]
33pub struct StateSpace {
34    pub nodes: BTreeMap<NodeId, Node>,
35}
36
37#[derive(Clone, Debug, Serialize, Deserialize)]
38pub struct Node {
39    pub incoming: BTreeSet<NodeId>,
40    pub outgoing: BTreeSet<NodeId>,
41    pub panic_state: Option<AbstractDisplay>,
42}
43
44#[derive(Clone, Debug, Serialize, Deserialize)]
45pub struct PropertySnapshot {
46    pub property: IProperty,
47    pub conclusion: Result<ParamValuation, ExecError>,
48    pub labellings: BTreeMap<usize, BTreeMap<StateId, ParamValuation>>,
49}
50
51#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
52pub struct PropertyIndex(pub usize);
53
54impl Snapshot {
55    pub fn new(
56        exec_name: String,
57        state_space: StateSpace,
58        state_info: StateInfo,
59        properties: Vec<PropertySnapshot>,
60        log: Log,
61        panic_message: Option<String>,
62    ) -> Self {
63        Self {
64            exec_name,
65            state_space,
66            state_info,
67            properties,
68            log,
69            panic_message,
70        }
71    }
72
73    pub fn last_property_index(&self) -> Option<PropertyIndex> {
74        if !self.properties.is_empty() {
75            Some(PropertyIndex(self.properties.len() - 1))
76        } else {
77            None
78        }
79    }
80
81    pub fn contains_property(&self, property_index: PropertyIndex) -> bool {
82        property_index.0 < self.properties.len()
83    }
84
85    pub fn contains_subproperty(
86        &self,
87        property_index: PropertyIndex,
88        subproperty_index: usize,
89    ) -> bool {
90        self.properties
91            .get(property_index.0)
92            .is_some_and(|property_snapshot| {
93                subproperty_index < property_snapshot.property.num_subproperties()
94            })
95    }
96
97    pub fn subproperty_labellings(
98        &self,
99        property_index: PropertyIndex,
100        subproperty_index: usize,
101    ) -> Option<&BTreeMap<StateId, ParamValuation>> {
102        self.properties
103            .get(property_index.0)
104            .and_then(|property_snapshot| property_snapshot.labellings.get(&subproperty_index))
105    }
106
107    pub fn property_snapshot(&self, property_index: PropertyIndex) -> &PropertySnapshot {
108        &self.properties[property_index.0]
109    }
110
111    pub fn property_snapshots(&self) -> &Vec<PropertySnapshot> {
112        &self.properties
113    }
114}
machine_check_gui/shared/snapshot.rs

machine_check_gui/shared/
snapshot.rs
