machine_check_gui/shared/
snapshot.rs

1use serde::{Deserialize, Serialize};
2use std::collections::{BTreeMap, BTreeSet};
3
4use crate::shared::snapshot::log::Log;
5use machine_check_common::{
6    check::Conclusion, property::Subproperty, ExecError, NodeId, ParamValuation, StateId,
7    ThreeValued,
8};
9use mck::abstr::Field;
10
11pub mod log;
12
13/// A snapshot of the current state of machine-check.
14///
15/// Provided by the backend to the frontend.
16#[derive(Clone, Debug, Serialize, Deserialize)]
17pub struct Snapshot {
18    pub exec_name: String,
19    pub state_space: StateSpace,
20    pub state_info: StateInfo,
21    subproperties: Vec<SubpropertySnapshot>,
22    pub log: Log,
23    pub panic_message: Option<String>,
24}
25
26#[derive(Clone, Debug, Serialize, Deserialize)]
27pub struct StateInfo {
28    pub field_names: Vec<String>,
29}
30
31#[derive(Clone, Debug, Serialize, Deserialize)]
32pub struct StateSpace {
33    pub nodes: BTreeMap<NodeId, Node>,
34}
35
36#[derive(Clone, Debug, Serialize, Deserialize)]
37pub struct Node {
38    pub incoming: BTreeSet<NodeId>,
39    pub outgoing: BTreeSet<NodeId>,
40    pub panic: Option<ThreeValued>,
41    pub fields: BTreeMap<String, Field>,
42}
43
44#[derive(Clone, Debug, Serialize, Deserialize)]
45pub struct SubpropertySnapshot {
46    pub subproperty: Subproperty,
47    pub conclusion: Result<Conclusion, ExecError>,
48    pub labellings: BTreeMap<StateId, ParamValuation>,
49    pub children: Vec<SubpropertySnapshot>,
50}
51
52#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
53pub struct RootPropertyIndex(pub usize);
54#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
55pub struct SubpropertyIndex(pub usize);
56
57impl Snapshot {
58    pub fn new(
59        exec_name: String,
60        state_space: StateSpace,
61        state_info: StateInfo,
62        properties: Vec<SubpropertySnapshot>,
63        log: Log,
64        panic_message: Option<String>,
65    ) -> Self {
66        Self {
67            exec_name,
68            state_space,
69            state_info,
70            subproperties: properties,
71            log,
72            panic_message,
73        }
74    }
75
76    pub fn root_properties_iter(&self) -> impl Iterator<Item = &SubpropertySnapshot> {
77        self.subproperties.iter()
78    }
79
80    fn num_subproperties(&self) -> usize {
81        fn recurse(property: &SubpropertySnapshot, count: &mut usize) {
82            *count += 1;
83            for child in &property.children {
84                recurse(child, count);
85            }
86        }
87        let mut result = 0;
88        for property in &self.subproperties {
89            recurse(property, &mut result);
90        }
91        result
92    }
93
94    pub fn contains_subindex(&self, index: SubpropertyIndex) -> bool {
95        index.0 < self.num_subproperties()
96    }
97
98    pub fn select_root_property(&self, index: RootPropertyIndex) -> &SubpropertySnapshot {
99        let Some(property) = self.subproperties.get(index.0) else {
100            panic!(
101                "Property index out of bounds: the len is {} but the index is {}",
102                self.subproperties.len(),
103                index.0
104            );
105        };
106        property
107    }
108
109    pub fn select_subproperty(&self, subindex: SubpropertyIndex) -> &SubpropertySnapshot {
110        fn recurse<'a>(
111            property: &'a SubpropertySnapshot,
112            subindex: usize,
113            count: &mut usize,
114        ) -> Option<&'a SubpropertySnapshot> {
115            if *count == subindex {
116                return Some(property);
117            }
118            *count += 1;
119            for child in &property.children {
120                if let Some(property) = recurse(child, subindex, count) {
121                    return Some(property);
122                }
123            }
124            None
125        }
126        let mut current_subindex = 0;
127        for property in &self.subproperties {
128            if let Some(property) = recurse(property, subindex.0, &mut current_subindex) {
129                return property;
130            }
131        }
132        panic!(
133            "Property subindex out of bounds: the sublen is {} but the subindex is {}",
134            current_subindex, subindex.0
135        );
136    }
137
138    pub fn subindex_to_root_index(&self, subindex: SubpropertyIndex) -> RootPropertyIndex {
139        fn recurse(property: &SubpropertySnapshot, subindex: usize, count: &mut usize) -> bool {
140            if *count == subindex {
141                return true;
142            }
143            *count += 1;
144            for child in &property.children {
145                if recurse(child, subindex, count) {
146                    return true;
147                }
148            }
149            false
150        }
151        let mut count = 0;
152        for (property_index, property) in self.subproperties.iter().enumerate() {
153            if recurse(property, subindex.0, &mut count) {
154                return RootPropertyIndex(property_index);
155            }
156        }
157        panic!(
158            "Property subindex out of bounds: the sublen is {} but the subindex is {}",
159            count, subindex.0
160        );
161    }
162
163    pub fn root_index_to_subindex(&self, index: RootPropertyIndex) -> SubpropertyIndex {
164        fn recurse(property: &SubpropertySnapshot, count: &mut usize) {
165            *count += 1;
166            for child in &property.children {
167                recurse(child, count);
168            }
169        }
170        let mut current_subindex = 0;
171        let mut current_index = 0;
172        for property in &self.subproperties {
173            if current_index == index.0 {
174                return SubpropertyIndex(current_subindex);
175            }
176            recurse(property, &mut current_subindex);
177            current_index += 1;
178        }
179        panic!(
180            "Property index out of bounds: the len is {} but the index is {}",
181            self.subproperties.len(),
182            current_index
183        );
184    }
185
186    pub fn last_property_subindex(&self) -> Option<SubpropertyIndex> {
187        let len = self.subproperties.len();
188        if len > 0 {
189            Some(self.root_index_to_subindex(RootPropertyIndex(len - 1)))
190        } else {
191            None
192        }
193    }
194}
machine_check_gui/shared/snapshot.rs

machine_check_gui/shared/
snapshot.rs
