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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
use std::collections::BTreeSet;
use std::collections::VecDeque;
use machine_check_common::NodeId;
use machine_check_common::StateId;
use mck::abstr::Abstr;
use mck::abstr::Machine as AbstrMachine;
use mck::concr::FullMachine;
use mck::misc::Meta;
use crate::AbstrState;
impl<M: FullMachine> super::Framework<M> {
/// Regenerates the state space from a given node, keeping its other parts. Returns whether the state space changed.
pub(super) fn regenerate(&mut self, from_node_id: NodeId) -> bool {
let mut queue = VecDeque::new();
// clear the step from the initial node so it is processed
self.work_state.space.clear_step(from_node_id);
queue.push_back(from_node_id);
let mut something_changed = false;
let mut new_states = BTreeSet::new();
let mut changed_successors = BTreeSet::new();
let param_start_tracker = self.machine.state().fields.len() as u32;
// construct state space by breadth-first search
while let Some(node_id) = queue.pop_front() {
// if it has already been processed, continue
let current_has_direct_successor = self
.work_state
.space
.direct_successor_iter(node_id)
.next()
.is_some();
if current_has_direct_successor {
continue;
}
self.work_state.num_generated_states += 1;
// remove outgoing edges
let (removed_direct_successors, removed_tail_partition) =
self.work_state.space.clear_step(node_id);
// prepare precision
let input_precision = self.work_state.input_precision.get(
&self.work_state.space,
node_id,
&self.default_input_precision,
);
let param_precision = self.work_state.param_precision.get(
&self.work_state.space,
node_id,
&self.default_param_precision,
);
let step_precision = self.work_state.step_precision.get(
&self.work_state.space,
node_id,
&self.default_step_precision,
);
// get current state, none if we are at start node
let current_state = if let Ok(state_id) = StateId::try_from(node_id) {
Some(self.work_state.space.state_data(state_id).clone())
} else {
None
};
// generate direct successors
for mut param in param_precision.into_proto_iter() {
let mut param_id = None;
let input_start_tracker = param.assign_trackers(param_start_tracker);
let param = <M::Abstr as AbstrMachine<M>>::Param::from_runtime(¶m);
for mut input in input_precision.clone().into_proto_iter() {
input.assign_trackers(input_start_tracker);
let input = <M::Abstr as AbstrMachine<M>>::Input::from_runtime(&input);
// compute the next state
let mut next_state = {
if let Some(current_state) = ¤t_state {
M::Abstr::next(
&self.abstract_system,
¤t_state.result,
&input,
¶m,
)
} else {
M::Abstr::init(&self.abstract_system, &input, ¶m)
}
};
/*log::trace!(
"Next state from {:?} with param {:?} and input {:?} is {:?}",
current_state,
param,
input,
next_state
);*/
// TODO: apply decay and trackers canonisation without conversion to/from runtime
let mut next_result = next_state.result.to_runtime();
// apply decay
step_precision.force_decay(&mut next_result);
// make trackers canonical
next_result.canonicise_trackers();
next_state.result = AbstrState::<M>::from_runtime(&next_result);
// add the step to the state space
self.work_state.num_generated_transitions += 1;
let (next_state_index, inserted, added_param_id) = self
.work_state
.space
.add_step(node_id, next_state, &input, ¶m, param_id);
param_id = Some(added_param_id);
if inserted {
new_states.insert(next_state_index);
}
// add the tail to the queue if it has no direct successors yet
let next_has_direct_successor = self
.work_state
.space
.direct_successor_iter(next_state_index.into())
.next()
.is_some();
if !next_has_direct_successor {
// add to queue
queue.push_back(next_state_index.into());
}
}
}
// compare sets of node ids
let direct_successors: BTreeSet<StateId> = self
.work_state
.space
.direct_successor_iter(node_id)
.collect();
let node_changed = direct_successors != removed_direct_successors
|| removed_tail_partition.as_ref()
!= self
.work_state
.space
.direct_successor_param_partition(node_id);
if node_changed {
if let Ok(state_id) = StateId::try_from(node_id) {
changed_successors.insert(state_id);
}
}
// make sure changed is true if the target nodes are different from the removed ones
// ignore the edges changing, currently only used for representative inputs
// which has no impact on verification
if !something_changed {
something_changed = node_changed;
}
}
self.work_state.checker.declare_regeneration(
&self.work_state.space,
&new_states,
&changed_successors,
);
// Each node now should have at least one direct successor.
// Assert it to be sure.
self.space().assert_left_total();
something_changed
}
}