taco_zcs_model_checker/zcs_error_graph/
builder.rs

1//! Factory method to construct a symbolic error graph (ZCS error graph)
2//! for a symbolic 01-CS (ZCS) and a set of error states.
3
4use super::{ZCS, ZCSErrorGraph, ZCSStates};
5
6/// Builder for constructing a symbolic error graph (ZCS error graph)
7///
8/// This builder takes a symnbolic 01-CS (ZCS) and a set of error states
9/// and derives the corresponding symbolic error graph.
10///
11/// The builder performs backwards reachability of all states in the 01-CS starting
12/// from the set of error states.
13#[derive(Debug)]
14pub struct ZCSErrorGraphBuilder<'a> {
15    /// symbolic error graph that is constructed by the builder
16    error_graph: ZCSErrorGraph<'a>,
17}
18impl<'a> ZCSErrorGraphBuilder<'a> {
19    /// creates a new symbolic error graph builder
20    pub fn new(cs: ZCS<'a>, err_states: ZCSStates) -> Self {
21        ZCSErrorGraphBuilder {
22            error_graph: ZCSErrorGraph {
23                error_states: err_states,
24                explored_states: Vec::new(),
25                initial_states: cs.new_empty_sym_state(),
26                cs,
27            },
28        }
29    }
30
31    /// predecessor computation to compute the reachable states
32    ///
33    /// # Pseudocode
34    ///
35    /// ```pseudo
36    ///  unexplored ← error_states
37    ///  visited ← unexplored
38    ///  while (unexplored ≠ ∅) {
39    ///     // 1. add new reachable states
40    ///     explored_states.push(unexplored)
41    ///     
42    ///     // 2. update unexplored
43    ///     unexplored ← Pred(∃ rule_vars: unexplored) ∧ ¬visited
44    ///    
45    ///     // 3. update visited
46    ///     visited ← visited ∨ unexplored
47    ///     abstract_unexplored ← ∃_rule_vars: unexplored
48    ///   
49    ///     for i in 0..|explored_states| {
50    ///         // 4. for each level i, check if a state `s` has already been reached with a different rule
51    ///         already_explored ← explored_states(i) ∧ abstract_unexplored
52    ///
53    ///         if (already_explored ≠ ∅) {
54    ///             abstract_already_explored ← ∃ rule_vars: already_explored
55    ///
56    ///             // 5. add state `s` with new outgoing rule `r` to the set of already explored states
57    ///             error_states(i) ← error_states(i) ∨ (unexplored ∧ abstract_already_explored)
58    ///       
59    ///             // 6. remove `s` from the set of unexplored states
60    ///             abstract_unexplored ← abstract_unexplored ∧ ¬abstract_already_explored
61    ///             unexplored ← unexplored ∧ ¬abstract_already_explored
62    ///         }
63    ///     }
64    ///  }
65    /// ```
66    pub fn compute_explored_states(&mut self) {
67        // unexplored states where the predecessor is computed from next
68        let mut unexplored = self.error_graph.error_states.clone();
69        // all states that are already visited
70        // don't need to compute the predecessor for these states
71        let mut visited = unexplored.clone();
72        while !unexplored.is_empty() {
73            // 1. add new reachable states
74            self.error_graph.explored_states.push(unexplored.clone());
75            // 2. update unexplored (compute predecessor and remove visited states)
76            unexplored = self
77                .error_graph
78                .cs
79                .compute_predecessor(self.error_graph.cs.abstract_rule_vars(unexplored.clone()));
80            unexplored = unexplored.intersection(&visited.complement());
81            // 3. update visited
82            visited = visited.union(&unexplored);
83            let mut abstract_unexplored =
84                self.error_graph.cs.abstract_rule_vars(unexplored.clone());
85            for i in 0..self.error_graph.explored_states.len() {
86                // 4. for each level, check if a state `s` has already been reached with a different rule
87                let already_explored =
88                    self.error_graph.explored_states[i].intersection(&abstract_unexplored);
89                if !already_explored.is_empty() {
90                    let abstract_already_explored =
91                        self.error_graph.cs.abstract_rule_vars(already_explored);
92                    // 5. add state `s` with new outgoing rule `r` to the set of already explored states
93                    self.error_graph.explored_states[i] = self.error_graph.explored_states[i]
94                        .union(&unexplored.intersection(&abstract_already_explored));
95                    // 6. remove `s` from the set of unexplored states
96                    abstract_unexplored =
97                        abstract_unexplored.intersection(&abstract_already_explored.complement());
98                    unexplored = unexplored.intersection(&abstract_already_explored.complement());
99                }
100            }
101        }
102    }
103
104    /// extracts all initial states that are reached in the error graph
105    pub fn compute_reachable_initial_states(&mut self) {
106        let mut initial_states = self.error_graph.cs.new_empty_sym_state();
107        for symbolic_state in self.error_graph.explored_states.iter() {
108            initial_states = initial_states
109                .union(&(symbolic_state.intersection(&self.error_graph.cs.initial_states())))
110        }
111        self.error_graph.initial_states = initial_states
112    }
113
114    /// builds the symbolic error graph
115    pub fn build(mut self) -> ZCSErrorGraph<'a> {
116        self.compute_explored_states();
117        self.compute_reachable_initial_states();
118        self.error_graph
119    }
120}
121
122#[cfg(test)]
123mod tests {
124    use taco_interval_ta::builder::IntervalTABuilder;
125    use taco_threshold_automaton::lia_threshold_automaton::integer_thresholds::Threshold;
126    use taco_threshold_automaton::lia_threshold_automaton::integer_thresholds::WeightedSum;
127
128    use crate::ZCSErrorGraphBuilder;
129    use crate::zcs;
130    use taco_interval_ta::IntervalTAAction;
131    use taco_interval_ta::IntervalTARule;
132    use taco_interval_ta::interval::Interval;
133    use taco_interval_ta::interval::IntervalBoundary;
134    use taco_interval_ta::{IntervalActionEffect, IntervalConstraint};
135    use taco_smt_encoder::SMTSolverBuilder;
136    use taco_threshold_automaton::ParameterConstraint;
137    use taco_threshold_automaton::expressions::fraction::Fraction;
138
139    use std::vec;
140    use taco_interval_ta::IntervalThresholdAutomaton;
141    use taco_threshold_automaton::expressions::{Location, Variable};
142    use taco_threshold_automaton::{
143        BooleanVarConstraint, LocationConstraint,
144        expressions::{ComparisonOp, IntegerExpression, Parameter},
145        general_threshold_automaton::{Action, builder::RuleBuilder},
146    };
147    use zcs::builder::ZCSBuilder;
148
149    /// Used to construct the 01-CS for the following threshold automaton:
150    ///
151    /// # Example
152    ///
153    /// Threshold Automaton:
154    ///     Locations: {l0,l1,l2}
155    ///     Initial location: l0
156    ///     Parameter: {n,t}
157    ///     Shared Variable: x
158    ///     Initial location constraints: l0 = n - t & l1 = 0 & l2
159    ///     Rules:
160    ///         r0: l0 -> l1, guard: true, action: x = x + 1
161    ///         r1: l0 -> l2, guard: x >= n - t, action: none
162    ///         r2: l1 -> l2, guard: x >= n - t, action: none
163    ///
164    /// Abstract Thershold Automaton:
165    /// Intervals for x: I_0 = [0,1), I_1 = [1,n-t), I_2 = [n-t, infty)
166    /// Interval Order: I_0 < I_1 < I_2
167    /// Abstract Rules:
168    ///     r0: l0 -> l1, guard: true, action: x = x + 1
169    ///     r1: l0 -> l1, guard: x = I_2, action: none
170    ///     r2: l1 -> l2, guard: x = I_2, action: none
171    ///
172    /// Structure of the symbolic 01-counter system:
173    ///     [(1,0,0),I_0] --- r0 ---> [(-,1,0),{I_0,I_1}]
174    ///     [(-,1,0),{I_0,I_1}] --- r0 ---> [(-,1,0),{I_0,I_1,I_2}]
175    ///     [(-,1,0),{I_0,I_1,I_2}] --- r0 ---> [(-,1,0),{I_0,I_1,I_2}]
176    ///     [(-,1,0),I_2] --- r1 ---> [(-,1,1),I_2]
177    ///     [(-,1,0),I_2] --- r2 ---> [(-,-,1),I_2]
178    ///
179    /// The backwards reachability analysis for the set of error states {[(0,0,1),-]} looks as follows (already visited states are ignored):
180    ///     level 1: [(0,0,1),-] <---- r1 ---- [(1,0,-),I_2],
181    ///              [(0,0,1),-] <---- r2 ---- [(0,1,-),I_2]
182    ///     level 2: [(1,0,-),I_2] <--- r2 --- [(1,1,-),I_2],
183    ///              [(0,1,-),I_2] <--- r1 --- [(1,1,-),I_2],
184    ///              [(0,1,-),I_1] <--- r0 --- [(1,-,-),{I_1,I_2}],
185    ///     level 3: [(1,-,-),{I_1,I_2}] <--- r0 --- [(1,-,-),{I_0,I_1,I_2}]
186    ///
187    /// The symbol error graph for the set of error    lia_threshold_automaton::WeightedSum,states {[(0,0,1),-]} looks as follows:
188    ///     level 0: {[(0,0,1),-]}
189    ///     level 1: {[(1,0,-),I_2]&r1, [(0,1,-),I_2]&r2} \cup {[(1,0,-),I_2]&r0]} (added in level 3)
190    ///     level 2: {[(1,-,-),I_1]&r0), [(1,1,-),I_2] &(r0 | r1 | r2)} (&r1,r2 added in the next iteration)
191    ///     level 3: {[(1,-,-),I_0]&r0}
192    fn get_test_ata() -> IntervalThresholdAutomaton {
193        let ta_builder =
194            taco_threshold_automaton::general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder::new("test")
195                .with_locations(vec![
196                    Location::new("l0"),
197                    Location::new("l1"),
198                    Location::new("l2"),
199                ])
200                .unwrap()
201                .with_variable(Variable::new("x"))
202                .unwrap()
203                .with_parameters(vec![
204                    Parameter::new("n"),
205                    Parameter::new("t"),
206                    Parameter::new("f"),
207                ])
208                .unwrap()
209                .initialize()
210                .with_initial_location_constraints(vec![
211                    LocationConstraint::ComparisonExpression(
212                        Box::new(IntegerExpression::Atom(Location::new("l0"))),
213                        ComparisonOp::Eq,
214                        Box::new(
215                            IntegerExpression::Param(Parameter::new("n"))
216                                - IntegerExpression::Param(Parameter::new("t")),
217                        ),
218                    ),
219                    LocationConstraint::ComparisonExpression(
220                        Box::new(IntegerExpression::Atom(Location::new("l1"))),
221                        ComparisonOp::Eq,
222                        Box::new(IntegerExpression::Const(0)),
223                    ),
224                    LocationConstraint::ComparisonExpression(
225                        Box::new(IntegerExpression::Atom(Location::new("l2"))),
226                        ComparisonOp::Eq,
227                        Box::new(IntegerExpression::Const(0)),
228                    ),
229                ])
230                .unwrap().with_resilience_conditions([ParameterConstraint::ComparisonExpression(
231                    Box::new(IntegerExpression::Atom(Parameter::new("n")) - IntegerExpression::Atom(Parameter::new("t"))),
232                    ComparisonOp::Gt,
233                    Box::new(IntegerExpression::Const(1)),
234                )]).unwrap().with_initial_variable_constraints([BooleanVarConstraint::ComparisonExpression(Box::new(IntegerExpression::Atom(Variable::new("x"))), ComparisonOp::Eq, Box::new(IntegerExpression::Const(0)))]).unwrap()
235                .with_rules(vec![
236                    RuleBuilder::new(0, Location::new("l0"), Location::new("l1"))
237                        .with_action(
238                            Action::new(
239                                Variable::new("x"),
240                                IntegerExpression::Atom(Variable::new("x"))
241                                    + IntegerExpression::Const(1),
242                            )
243                            .unwrap(),
244                        )
245                        .build(),
246                    RuleBuilder::new(1, Location::new("l0"), Location::new("l2"))
247                        .with_guard(BooleanVarConstraint::ComparisonExpression(
248                            Box::new(IntegerExpression::Atom(Variable::new("x"))),
249                            ComparisonOp::Geq,
250                            Box::new(
251                                IntegerExpression::Param(Parameter::new("n"))
252                                    - IntegerExpression::Param(Parameter::new("t")),
253                            ),
254                        ))
255                        .build(),
256                    RuleBuilder::new(2, Location::new("l1"), Location::new("l2"))
257                        .with_guard(BooleanVarConstraint::ComparisonExpression(
258                            Box::new(IntegerExpression::Atom(Variable::new("x"))),
259                            ComparisonOp::Geq,
260                            Box::new(
261                                IntegerExpression::Param(Parameter::new("n"))
262                                    - IntegerExpression::Param(Parameter::new("t")),
263                            ),
264                        ))
265                        .build(),
266                ])
267                .unwrap();
268        let ta = ta_builder.build();
269        let lia =
270            taco_threshold_automaton::lia_threshold_automaton::LIAThresholdAutomaton::try_from(
271                ta.clone(),
272            )
273            .unwrap();
274
275        let mut interval_tas = IntervalTABuilder::new(lia, SMTSolverBuilder::default(), vec![])
276            .build()
277            .unwrap();
278        let ata = interval_tas.next().unwrap();
279
280        let nxt = interval_tas.next();
281        assert!(nxt.is_none(), "Got additional ta {}", nxt.unwrap());
282
283        ata
284    }
285
286    #[test]
287    fn test_compute_reachable_initial_states() {
288        let ata = get_test_ata();
289        let cs = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata).build();
290
291        let l0 = cs.get_sym_state_for_loc(&Location::new("l0"));
292        let l1 = cs.get_sym_state_for_loc(&Location::new("l1"));
293        let l2 = cs.get_sym_state_for_loc(&Location::new("l2"));
294        let error_states = l0
295            .complement()
296            .intersection(&l1.complement())
297            .intersection(&l2);
298
299        let interval_0 =
300            Interval::new_constant(Fraction::new(0, 1, false), Fraction::new(1, 1, false));
301        let abstract_rule_0 = IntervalTARule::new(
302            0,
303            Location::new("l0"),
304            Location::new("l1"),
305            IntervalConstraint::True,
306            vec![IntervalTAAction::new(
307                Variable::new("x"),
308                IntervalActionEffect::Inc(1),
309            )],
310        );
311        let r0 = cs.get_sym_state_for_rule(&abstract_rule_0);
312        let i0 = cs.get_sym_state_for_shared_interval(&Variable::new("x"), &interval_0);
313        let correct_initial_states = l0
314            .intersection(&l1.complement())
315            .intersection(&l2.complement())
316            .intersection(&i0)
317            .intersection(&r0);
318
319        let builder = ZCSErrorGraphBuilder::new(cs, error_states);
320        let error_graph = builder.build();
321        let initial_states = error_graph.initial_states;
322
323        assert!(correct_initial_states.equal(&initial_states));
324    }
325
326    #[test]
327    fn test_compute_explored_states() {
328        let ata = get_test_ata();
329        let cs = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata).build();
330        let l0 = cs.get_sym_state_for_loc(&Location::new("l0"));
331        let l1 = cs.get_sym_state_for_loc(&Location::new("l1"));
332        let l2 = cs.get_sym_state_for_loc(&Location::new("l2"));
333        let error_states = l0
334            .complement()
335            .intersection(&l1.complement())
336            .intersection(&l2);
337
338        // I_0 = [0,1)
339        let interval_0 =
340            Interval::new_constant(Fraction::new(0, 1, false), Fraction::new(1, 1, false));
341        // I_1 = [1,n-t)
342        let interval_1 = Interval::new(
343            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
344            false,
345            IntervalBoundary::Bound(Threshold::new(
346                [
347                    (Parameter::new("n"), 1.into()),
348                    (Parameter::new("t"), Fraction::new(1, 1, true)),
349                ],
350                0,
351            )),
352            true,
353        );
354        // I_2 = [n-t,infty)
355        let interval_2 = Interval::new(
356            IntervalBoundary::Bound(Threshold::new(
357                [
358                    (Parameter::new("n"), 1.into()),
359                    (Parameter::new("t"), Fraction::new(1, 1, true)),
360                ],
361                0,
362            )),
363            false,
364            IntervalBoundary::new_infty(),
365            true,
366        );
367
368        let i0 = cs.get_sym_state_for_shared_interval(&Variable::new("x"), &interval_0);
369        let i1 = cs.get_sym_state_for_shared_interval(&Variable::new("x"), &interval_1);
370        let i2 = cs.get_sym_state_for_shared_interval(&Variable::new("x"), &interval_2);
371
372        // abstract rules
373        // r0: l0 -> l1, guard: true, action: x = x + 1
374        let abstract_rule_0 = IntervalTARule::new(
375            0,
376            Location::new("l0"),
377            Location::new("l1"),
378            IntervalConstraint::True,
379            vec![IntervalTAAction::new(
380                Variable::new("x"),
381                IntervalActionEffect::Inc(1),
382            )],
383        );
384        // r1: l0 -> l2, guard: x = I_2, action: none
385        let abstract_rule_1 = IntervalTARule::new(
386            1,
387            Location::new("l0"),
388            Location::new("l2"),
389            IntervalConstraint::SingleVarIntervalConstr(
390                Variable::new("x"),
391                [interval_2.clone()].to_vec(),
392            ),
393            Vec::new(),
394        );
395        // r2: l1 -> l2, guard: x = I_2, action: none
396        let abstract_rule_2 = IntervalTARule::new(
397            2,
398            Location::new("l1"),
399            Location::new("l2"),
400            IntervalConstraint::SingleVarIntervalConstr(
401                Variable::new("x"),
402                [interval_2.clone()].to_vec(),
403            ),
404            Vec::new(),
405        );
406
407        let r0 = cs.get_sym_state_for_rule(&abstract_rule_0);
408        let r1 = cs.get_sym_state_for_rule(&abstract_rule_1);
409        let r2 = cs.get_sym_state_for_rule(&abstract_rule_2);
410
411        let builder = ZCSErrorGraphBuilder::new(cs.clone(), error_states.clone());
412
413        let error_graph = builder.build();
414
415        assert_eq!(error_graph.explored_states.len(), 4);
416
417        // level 0: {[(0,0,1),-]} = error_states
418        assert!(error_graph.explored_states[0].equal(&error_states));
419
420        // level 1: {[(1,0,-),I_2]&(r0 | r1), [(0,1,-),I_2]&r2}
421        let mut level1 = l0
422            .intersection(&l1.complement())
423            .intersection(&i2)
424            .intersection(&(r0.union(&r1)));
425        level1 = level1.union(
426            &(l0.complement()
427                .intersection(&l1)
428                .intersection(&i2)
429                .intersection(&r2)),
430        );
431        assert!(error_graph.explored_states[1].equal(&level1));
432
433        // level 2: {[(1,-,-),I_1]&r0), [(1,1,-),I_2] &(r0 | r1 | r2)}
434        let mut level2 = l0.intersection(&i1).intersection(&r0);
435        level2 = level2.union(
436            &(l0.intersection(&l1)
437                .intersection(&i2)
438                .intersection(&(r0.union(&r1).union(&r2)))),
439        );
440        // this constraint needs to be added due to the construction of the symbolic transition
441        // because the guard for r0 is true even though "I_3" does not exist: [(1,-,-), !(I_0 | I_1 | I_2)] &r0
442        level2 = level2.union(
443            &(l0.intersection(&(i0.union(&i1).union(&i2)).complement())
444                .intersection(&r0)),
445        );
446        assert!(error_graph.explored_states[2].equal(&level2));
447
448        // level 3: {[(1,-,-),I_0]&r0}
449        let level3 = l0.intersection(&i0).intersection(&r0);
450        assert!(error_graph.explored_states[3].equal(&level3));
451    }
452}
taco_zcs_model_checker/zcs_error_graph/builder.rs

taco_zcs_model_checker/zcs_error_graph/
builder.rs
