taco_zcs_model_checker/
zcs_error_graph.rs

1//! This module contains the symbolic error graph (ZCS error graph)
2//! for a given property and a 01-CS (ZCS).
3
4pub mod builder;
5
6use log::info;
7
8use std::collections::VecDeque;
9
10use taco_interval_ta::IntervalTARule;
11use taco_interval_ta::interval::Interval;
12use taco_threshold_automaton::expressions::{Location, Variable};
13use zcs::*;
14
15use crate::paths::{SteadyErrorPath, SteadyPath, VariableAssignment};
16use crate::smt_encoder_steady::SpuriousResult;
17use crate::{ZCSModelCheckerContext, zcs};
18
19/// Type representing a symbolic error graph (ZCS error graph)
20#[derive(Debug, Clone)]
21pub struct ZCSErrorGraph<'a> {
22    /// set of error states
23    error_states: ZCSStates,
24    /// all iteratively explored states, these states contain bdd variables for transitions
25    /// the first entry is equal to the error states
26    explored_states: Vec<ZCSStates>,
27    /// set of reached initial states of the error graph
28    initial_states: ZCSStates,
29    /// underlying 01-CS (ZCS)
30    cs: ZCS<'a>,
31}
32impl ZCSErrorGraph<'_> {
33    /// checks if an initial state has been reached
34    pub fn is_empty(&self) -> bool {
35        self.initial_states.is_empty()
36    }
37
38    /// reachable initial_states
39    pub fn initial_states(&self) -> ZCSStates {
40        self.initial_states.clone()
41    }
42
43    /// computes the set of successors reachable in the symbolic error graph (ZCS error graph) for a given symbolic transition
44    pub fn compute_successors(&self, from: ZCSStates, with: SymbolicTransition) -> ZCSStates {
45        // TODO: some possible optimization, i.e., check if transition id is contained in `from`
46        let from = self.cs.abstract_rule_vars(from);
47        let mut succ = self.cs.compute_successor(from, with.clone());
48        //remove used transition id
49        succ = self.cs.abstract_rule_vars(succ);
50        //intersect with all states that are in the error graph
51        let mut intersection = self.cs.new_empty_sym_state();
52        for i in 0..self.explored_states.len() {
53            intersection = intersection.union(&(self.explored_states[i].intersection(&succ)));
54        }
55        intersection
56    }
57
58    /// for set of states, it removes the error states
59    /// additionally returns false, if the intersection is empty
60    pub fn get_non_error_intersection(&self, states: ZCSStates) -> (bool, ZCSStates) {
61        let intersection = self.explored_states[0].complement().intersection(&states);
62        if !intersection.is_empty() {
63            (true, intersection)
64        } else {
65            (false, intersection)
66        }
67    }
68
69    /// computes the intersection of a set of states with the set of error states
70    /// additionally returns, if the intersection is empty
71    pub fn get_error_intersection(&self, states: ZCSStates) -> (bool, ZCSStates) {
72        let intersection = self.error_states.intersection(&states);
73        if !intersection.is_empty() {
74            (true, intersection)
75        } else {
76            (false, intersection)
77        }
78    }
79
80    /// returns the set of states where a given location is occupied
81    pub fn get_sym_state_for_loc(&self, loc: &Location) -> ZCSStates {
82        self.cs.get_sym_state_for_loc(loc)
83    }
84
85    /// returns the set of states where the given shared variable is in the given interval
86    pub fn get_sym_state_for_shared_interval(
87        &self,
88        shared: &Variable,
89        interval: &Interval,
90    ) -> ZCSStates {
91        self.cs.get_sym_state_for_shared_interval(shared, interval)
92    }
93
94    /// returns the set of states where the rule_id of a given rule is applied
95    pub fn get_sym_state_for_rule(&self, rule: &IntervalTARule) -> ZCSStates {
96        self.cs.get_sym_state_for_rule(rule)
97    }
98
99    /// returns an iterator over the encoded transition rules in the underlying 01-cs
100    pub fn transitions(&self) -> impl Iterator<Item = &SymbolicTransition> {
101        self.cs.transitions()
102    }
103
104    /// returns a new empty Symbolic State
105    pub fn new_empty_sym_state(&self) -> ZCSStates {
106        self.cs.new_empty_sym_state()
107    }
108
109    /// checks if the error graph contains a non-spurious error path
110    /// `spurious_checker` is used to check if a path is spurious
111    ///
112    /// returns None if every path is spurious
113    ///
114    /// Note that this function is a semi-decision procedure
115    /// if the underlying threshold automaton contains decrements or resets,
116    /// i.e., it might not terminate.
117    ///
118    ///
119    /// ```pseudo
120    ///
121    /// queue ← Queue::new()
122    /// queue.push(SteadyPath::new(initial_states))
123    /// while (queue ≠ ∅) {
124    ///     steady_path ← queue.pop()
125    ///     for rule in transitions {
126    ///         successor_states ← compute_successors(steady_path.last_states, rule)
127    ///         
128    ///         // check if an error state can be reached
129    ///         error_intersection ← get_error_intersection(successor_states)
130    ///         if (error_intersection ≠ ∅) {
131    ///             foreach assignment {
132    ///                 if ((error_intersecion ∧ assignment) ≠ ∅) {
133    ///                     updated_steady_path ← steady_path.add_successor(rule, error_intersection ∧ assignment)
134    ///                     if updated_steady_path.is_non_spurious() {
135    ///                         return "Found non spurious counter example"
136    ///                     }  
137    ///                 }
138    ///             }
139    ///         }
140    ///
141    ///         // check all other reachable steady paths which do not lead to an error state for spuriousness
142    ///         non_error_intersection ← get_non_error_intersection(successor_states)
143    ///         if (non_error_intersection ≠ ∅) {
144    ///             foreach assignment {
145    ///                 if ((non_error_intersection ∧ assignment) ≠ ∅) {
146    ///                     // construct steady path for the given assignment
147    ///                     successor_steady_path ← construct_steady_path(non_error_intersection ∧ assignment, assignment)
148    ///                     updated_steady_path ← steady_path.add_successor(rule, successor_steady_path)
149    ///                     if updated_steady_path.is_non_spurious() {
150    ///                         queue.push(updated_steady_path)
151    ///                     }
152    ///                 }
153    ///             }
154    ///         }   
155    ///     }
156    /// }
157    /// return "All error paths are spurious"
158    /// ```
159    pub fn contains_non_spurious_error_path(
160        &self,
161        smc_ctx: &ZCSModelCheckerContext,
162    ) -> SpuriousResult {
163        // all possible variable assignments
164        let all_possible_assignments = self.get_all_possible_variable_assignments();
165
166        // initial states that are already error states, i.e., error paths
167        // without any transition
168        let (non_empty, initial_error_states) = self.get_error_intersection(self.initial_states());
169        if non_empty {
170            for assignment in all_possible_assignments.iter() {
171                if initial_error_states.contains_sym_assignment(assignment) {
172                    let error_path = SteadyErrorPath::new(
173                        SteadyPath::new(
174                            vec![],
175                            initial_error_states.intersect_assignment(assignment),
176                            assignment.clone(),
177                        ),
178                        self,
179                    );
180
181                    let res = error_path.is_non_spurious(true, smc_ctx);
182                    if res.is_non_spurious() {
183                        return res;
184                    }
185                }
186            }
187        }
188
189        // assignments that are reached except for error states
190        let reachable_assignments = self.compute_reachable_variable_assignments();
191        let mut queue: VecDeque<SteadyErrorPath> = VecDeque::new();
192        for assignment in reachable_assignments.clone() {
193            if self.initial_states().contains_sym_assignment(&assignment) {
194                let initial_states_for_assignment =
195                    self.initial_states.intersect_assignment(&assignment);
196                let initial_steady_path =
197                    self.construct_steady_path(initial_states_for_assignment, assignment);
198                queue.push_back(SteadyErrorPath::new(initial_steady_path, self));
199            }
200        }
201
202        // print spurious counter example from time to time
203        // i.e., the first spurious ce, then the 10th, then the 100th, etc.
204        let mut spurious_ce_count = 0;
205        let mut next_to_print = 1;
206
207        while !queue.is_empty() {
208            let steady_error_path = queue.pop_front().unwrap();
209            let last_states = steady_error_path.get_last_states();
210            let last_assignment = steady_error_path.get_last_assignment();
211            for rule in self.cs.transitions() {
212                let successor_states = self.compute_successors(last_states.clone(), rule.clone());
213
214                // check if an error state can be reached
215                let (non_empty, error_intersection) =
216                    self.get_error_intersection(successor_states.clone());
217                if non_empty {
218                    // check the possible variable assignments of the successor states
219                    for assignment in all_possible_assignments.clone() {
220                        if error_intersection.contains_sym_assignment(&assignment) {
221                            let mut updated_steady_path = steady_error_path.clone();
222                            let error_steady_path =
223                                SteadyPath::new(vec![], error_intersection.clone(), assignment);
224                            updated_steady_path.add_successor(rule, error_steady_path);
225
226                            let res = updated_steady_path.is_non_spurious(true, smc_ctx);
227                            if res.is_non_spurious() {
228                                return res;
229                            } else if smc_ctx.print_spurious_ce() {
230                                info!("Spurious counterexample found: {updated_steady_path}");
231                            }
232                        }
233                    }
234                }
235                // check all other reachable steady paths for non_spuriousness
236                let (non_empty, mut non_error_intersection) =
237                    self.get_non_error_intersection(successor_states.clone());
238                if non_empty {
239                    if smc_ctx.heuristics().is_monotonic()
240                        || steady_error_path.last_is_monotonic(smc_ctx.ta())
241                    {
242                        non_error_intersection =
243                            non_error_intersection.remove_assignment(&last_assignment);
244                    }
245                    if non_error_intersection.is_empty() {
246                        continue;
247                    }
248                    for assignment in reachable_assignments.iter() {
249                        if non_error_intersection.contains_sym_assignment(assignment) {
250                            let mut updated_steady_path = steady_error_path.clone();
251                            let non_error_states_for_assignment =
252                                non_error_intersection.intersect_assignment(assignment);
253                            let successor_steady_path = self.construct_steady_path(
254                                non_error_states_for_assignment,
255                                assignment.clone(),
256                            );
257                            updated_steady_path.add_successor(rule, successor_steady_path);
258                            let res = updated_steady_path.is_non_spurious(false, smc_ctx);
259                            if res.is_non_spurious() {
260                                queue.push_back(updated_steady_path);
261                            } else if smc_ctx.print_spurious_ce() {
262                                spurious_ce_count += 1;
263                                if spurious_ce_count == next_to_print {
264                                    info!("Spurious subpath found: {updated_steady_path}");
265                                    next_to_print *= 10;
266                                }
267                            }
268                        }
269                    }
270                }
271            }
272        }
273        // checked all possible paths, no non-spurious path found
274        SpuriousResult::new_spurious()
275    }
276
277    /// returns all possible variable assignments
278    fn get_all_possible_variable_assignments(&self) -> Vec<SymbolicVariableAssignment> {
279        let mut possible_assignments = vec![VariableAssignment::new()];
280        for shared in self.variables() {
281            let mut updated_assignments = Vec::new();
282            for assignment in possible_assignments {
283                let intervals = self.get_ordered_intervals_for_shared(shared);
284                for interval in intervals {
285                    let mut updated_assignment = assignment.clone();
286                    updated_assignment
287                        .add_shared_var_interval(shared.clone(), interval.clone())
288                        .expect("failed to update variable_assignment");
289                    updated_assignments.push(updated_assignment);
290                }
291            }
292            possible_assignments = updated_assignments;
293        }
294
295        possible_assignments
296            .iter()
297            .map(|assign| self.cs.get_sym_var_assignment(assign.clone()))
298            .collect()
299    }
300
301    /// computes all reachable variable assignments of the error graph (except for error states)
302    fn compute_reachable_variable_assignments(&self) -> Vec<SymbolicVariableAssignment> {
303        let possible_assignments = self.get_all_possible_variable_assignments();
304
305        possible_assignments
306            .into_iter()
307            .filter(|assign| {
308                self.explored_states[1..self.explored_states.len()]
309                    .iter()
310                    .any(|state| state.contains_sym_assignment(assign))
311            })
312            .collect()
313    }
314
315    /// constructs the steady path for a given 'SymbolicState' and a 'SymbolicVariableAssignment'
316    ///
317    /// i.e., it computes all reachable states and possible transitions to stay in the same variable assignment
318    ///
319    /// Note that it only computes reachable states that are not an error state
320    fn construct_steady_path(
321        &self,
322        sym_state: ZCSStates,
323        assignment: SymbolicVariableAssignment,
324    ) -> SteadyPath {
325        let mut reachable_states = sym_state;
326        let mut applied_rules = Vec::new();
327        let mut reachable_states_changed = true;
328        while reachable_states_changed {
329            reachable_states_changed = false;
330            for rule in self.cs.transitions() {
331                let mut succ = self
332                    .cs
333                    .compute_successor(reachable_states.clone(), rule.clone());
334                // remove all states that change the context
335                succ = succ.intersect_assignment(&assignment);
336                // remove all states that are not in the error graph
337                let (not_empty, non_error_succ) = self.get_non_error_intersection(succ.clone());
338                if not_empty {
339                    if !applied_rules.contains(&rule) {
340                        applied_rules.push(rule);
341                    }
342                    let updated_reachable_states = reachable_states.union(&non_error_succ);
343                    if !updated_reachable_states.equal(&reachable_states) {
344                        // we reached new states need to check all transitions again afterwards
345                        reachable_states = updated_reachable_states;
346                        reachable_states_changed = true;
347                        break;
348                    }
349                }
350            }
351        }
352        SteadyPath::new(applied_rules, reachable_states, assignment)
353    }
354
355    /// returns an iterator over the locations of the underlying threshold automaton
356    pub fn locations(&self) -> impl Iterator<Item = &Location> {
357        self.cs.locations()
358    }
359
360    /// returns an iterator over the shared variables of the underlying threshold automaton
361    pub fn variables(&self) -> impl Iterator<Item = &Variable> {
362        self.cs.variables()
363    }
364
365    /// returns an iterator over the ordered intervals for a given shared variable
366    pub fn get_ordered_intervals_for_shared(&self, shared: &Variable) -> &Vec<Interval> {
367        self.cs.get_ordered_intervals_for_shared(shared)
368    }
369}
370
371#[cfg(test)]
372mod tests {
373    use crate::IntervalThresholdAutomaton;
374    use crate::ZCSErrorGraphBuilder;
375    use crate::zcs;
376    use crate::zcs::ZCS;
377    use crate::zcs::ZCSStates;
378    use taco_interval_ta::IntervalTAAction;
379    use taco_interval_ta::IntervalTARule;
380    use taco_interval_ta::builder::IntervalTABuilder;
381    use taco_interval_ta::interval::Interval;
382    use taco_interval_ta::interval::IntervalBoundary;
383    use taco_interval_ta::{IntervalActionEffect, IntervalConstraint};
384    use taco_model_checker::ModelCheckerContext;
385    use taco_model_checker::internal_spec::ErrorTarget;
386    use taco_model_checker::internal_spec::upwards_closed_set::UpwardsClosedSet;
387    use taco_smt_encoder::SMTSolverBuilder;
388    use taco_threshold_automaton::ParameterConstraint;
389    use taco_threshold_automaton::expressions::fraction::Fraction;
390    use taco_threshold_automaton::lia_threshold_automaton::integer_thresholds::Threshold;
391
392    use crate::ZCSModelCheckerContext;
393    use crate::ZCSModelCheckerHeuristics;
394    use taco_model_checker::SMTBddContext;
395
396    use crate::zcs_error_graph::VariableAssignment;
397    use taco_threshold_automaton::RuleDefinition;
398    use taco_threshold_automaton::expressions::BooleanConnective;
399    use taco_threshold_automaton::expressions::{Location, Variable};
400    use taco_threshold_automaton::lia_threshold_automaton::integer_thresholds::WeightedSum;
401    use taco_threshold_automaton::{
402        BooleanVarConstraint, LocationConstraint,
403        expressions::{ComparisonOp, IntegerExpression, Parameter},
404        general_threshold_automaton::{Action, builder::RuleBuilder},
405    };
406    use zcs::builder::ZCSBuilder;
407
408    /// Used to construct the SymbolicErrorGraph for the following threshold automaton:
409    ///
410    /// Threshold Automaton:
411    /// Locations: {l0,l1,l2}
412    /// Initial location: l0
413    /// Parameter: {n,t}
414    /// Shared Variables: x,y
415    /// Initial location constraints: l0 = n - t & l1 = 0 & l2
416    /// Rules:
417    ///     r0: l0 -> l1, guard: true, action: x = x + 1
418    ///     r1: l0 -> l2, guard: x >= n - t, action: none
419    ///     r2: l1 -> l2, guard: x >= n - t, action: none
420    ///
421    /// Abstract Thershold Automaton:
422    /// Intervals for x: I_0 = [0,1), I_1 = [1,n-t), I_2 = [n-t, infty)
423    /// Interval Order: I_0 < I_1 < I_2
424    /// Abstract Rules:
425    ///     r0: l0 -> l1, guard: true, action: x = x + 1
426    ///     r1: l0 -> l1, guard: x = I_2, action: none
427    ///     r2: l1 -> l2, guard: x = I_2, action: none
428    ///
429    /// Structure of the symbolic 01-counter system:
430    ///     [(1,0,0),I_0] --- r0 ---> [(-,1,0),{I_0,I_1}]
431    ///     [(-,1,0),{I_0,I_1}] --- r0 ---> [(-,1,0),{I_0,I_1,I_2}]
432    ///     [(-,1,0),{I_0,I_1,I_2}] --- r0 ---> [(-,1,0),{I_0,I_1,I_2}]
433    ///     [(-,1,0),I_2] --- r1 ---> [(-,1,1),I_2]
434    ///     [(-,1,0),I_2] --- r2 ---> [(-,-,1),I_2]
435    ///
436    /// The backwards reachability analysis for the set of error states {[(0,0,1),-]} looks as follows (already visited states are ignored):
437    ///     level 1: [(0,0,1),-] <---- r1 ---- [(1,0,-),I_2],
438    ///              [(0,0,1),-] <---- r2 ---- [(0,1,-),I_2]
439    ///     level 2: [(1,0,-),I_2] <--- r2 --- [(1,1,-),I_2],
440    ///              [(0,1,-),I_2] <--- r1 --- [(1,1,-),I_2],
441    ///              [(0,1,-),I_1] <--- r0 --- [(1,-,-),{I_1,I_2}],
442    ///     level 3: [(1,-,-),{I_1,I_2}] <--- r0 --- [(1,-,-),{I_0,I_1,I_2}]
443    ///
444    /// The symbol error graph for the set of error states {[(0,0,1),-]} looks as follows:
445    ///     level 0: {[(0,0,1),-]}
446    ///     level 1: {[(1,0,-),I_2]&r1, [(0,1,-),I_2]&r2} \cup {[(1,0,-),I_2]&r0]} (added in level 3)
447    ///     level 2: {[(1,-,-),I_1]&r0), [(1,1,-),I_2] &(r0 | r1 | r2)} (&r1,r2 added in the next iteration)
448    ///     level 3: {[(1,-,-),I_0]&r0}
449    fn get_test_ata() -> IntervalThresholdAutomaton {
450        let ta_builder =
451            taco_threshold_automaton::general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder::new("test")
452                .with_locations(vec![
453                    Location::new("l0"),
454                    Location::new("l1"),
455                    Location::new("l2"),
456                ])
457                .unwrap()
458                .with_variables(vec![Variable::new("x"), Variable::new("y")])
459                .unwrap()
460                .with_parameters(vec![
461                    Parameter::new("n"),
462                    Parameter::new("t"),
463                    Parameter::new("f"),
464                ])
465                .unwrap()
466                .initialize()
467                .with_initial_location_constraints(vec![
468                    LocationConstraint::ComparisonExpression(
469                        Box::new(IntegerExpression::Atom(Location::new("l0"))),
470                        ComparisonOp::Eq,
471                        Box::new(
472                            IntegerExpression::Param(Parameter::new("n"))
473                                - IntegerExpression::Param(Parameter::new("t")),
474                        ),
475                    ),
476                    LocationConstraint::ComparisonExpression(
477                        Box::new(IntegerExpression::Atom(Location::new("l1"))),
478                        ComparisonOp::Eq,
479                        Box::new(IntegerExpression::Const(0)),
480                    ),
481                    LocationConstraint::ComparisonExpression(
482                        Box::new(IntegerExpression::Atom(Location::new("l2"))),
483                        ComparisonOp::Eq,
484                        Box::new(IntegerExpression::Const(0)),
485                    ),
486                ])
487                .unwrap()
488                .with_resilience_conditions([ParameterConstraint::ComparisonExpression(
489                    Box::new(IntegerExpression::Atom(Parameter::new("n")) - IntegerExpression::Atom(Parameter::new("t"))),
490                    ComparisonOp::Gt,
491                    Box::new(IntegerExpression::Const(1)),
492                )])
493                .unwrap()
494                .with_initial_variable_constraints([BooleanVarConstraint::ComparisonExpression(Box::new(IntegerExpression::Atom(Variable::new("x"))), ComparisonOp::Eq, Box::new(IntegerExpression::Const(0))), BooleanVarConstraint::ComparisonExpression(Box::new(IntegerExpression::Atom(Variable::new("y"))), ComparisonOp::Eq, Box::new(IntegerExpression::Const(0)))])
495                .unwrap()
496                .with_rules(vec![
497                    RuleBuilder::new(0, Location::new("l0"), Location::new("l1"))
498                        .with_action(
499                            Action::new(
500                                Variable::new("x"),
501                                IntegerExpression::Atom(Variable::new("x"))
502                                    + IntegerExpression::Const(1),
503                            )
504                            .unwrap(),
505                        )
506                        .build(),
507                    RuleBuilder::new(1, Location::new("l0"), Location::new("l2"))
508                        .with_guard(
509                            BooleanVarConstraint::BinaryExpression(
510                                Box::new(BooleanVarConstraint::ComparisonExpression(
511                                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
512                                    ComparisonOp::Geq,
513                                    Box::new(
514                                        IntegerExpression::Param(Parameter::new("n"))
515                                            - IntegerExpression::Param(Parameter::new("t")),
516                                    ))),
517                                    BooleanConnective::And,
518                                    Box::new(BooleanVarConstraint::ComparisonExpression(
519                                        Box::new(IntegerExpression::Atom(Variable::new("y"))),
520                                        ComparisonOp::Eq,
521                                        Box::new(IntegerExpression::Const(0)),
522                                    )
523                            )
524                        ))
525                        .build(),
526                    RuleBuilder::new(2, Location::new("l1"), Location::new("l2"))
527                    .with_guard(
528                        BooleanVarConstraint::BinaryExpression(
529                            Box::new(BooleanVarConstraint::ComparisonExpression(
530                                Box::new(IntegerExpression::Atom(Variable::new("x"))),
531                                ComparisonOp::Geq,
532                                Box::new(
533                                    IntegerExpression::Param(Parameter::new("n"))
534                                        - IntegerExpression::Param(Parameter::new("t")),
535                                ))),
536                                BooleanConnective::And,
537                                Box::new(BooleanVarConstraint::ComparisonExpression(
538                                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
539                                    ComparisonOp::Eq,
540                                    Box::new(IntegerExpression::Const(0)),
541                                )
542                        )
543                        ))
544                        .build(),
545                ])
546                .unwrap();
547        let ta = ta_builder.build();
548        let lia =
549            taco_threshold_automaton::lia_threshold_automaton::LIAThresholdAutomaton::try_from(
550                ta.clone(),
551            )
552            .unwrap();
553
554        let mut interval_tas = IntervalTABuilder::new(lia, SMTSolverBuilder::default(), vec![])
555            .build()
556            .unwrap();
557        interval_tas.next().unwrap()
558    }
559
560    fn get_error_states(cs: &ZCS) -> ZCSStates {
561        let l0 = cs.get_sym_state_for_loc(&Location::new("l0"));
562        let l1 = cs.get_sym_state_for_loc(&Location::new("l1"));
563        let l2 = cs.get_sym_state_for_loc(&Location::new("l2"));
564        l0.complement()
565            .intersection(&l1.complement())
566            .intersection(&l2)
567    }
568
569    #[test]
570    fn test_is_empty() {
571        let ata = get_test_ata();
572        let mgr = taco_bdd::BDDManager::default();
573        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
574        let cs = builder.build();
575        let error_states = get_error_states(&cs);
576
577        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
578        let error_graph = error_graph_builder.build();
579
580        assert!(!error_graph.is_empty());
581    }
582
583    #[test]
584    fn test_initial_states() {
585        let ata = get_test_ata();
586        let mgr = taco_bdd::BDDManager::default();
587        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
588        let cs = builder.build();
589        let error_states = get_error_states(&cs);
590
591        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
592        let error_graph = error_graph_builder.build();
593
594        let l0 = error_graph.cs.get_sym_state_for_loc(&Location::new("l0"));
595        let l1 = error_graph.cs.get_sym_state_for_loc(&Location::new("l1"));
596        let l2 = error_graph.cs.get_sym_state_for_loc(&Location::new("l2"));
597
598        // I_0 = [0,1)
599        let interval_0 =
600            Interval::new_constant(Fraction::new(0, 1, false), Fraction::new(1, 1, false));
601
602        let i0 = error_graph
603            .cs
604            .get_sym_state_for_shared_interval(&Variable::new("x"), &interval_0);
605        let i0 = i0.intersection(
606            &error_graph
607                .cs
608                .get_sym_state_for_shared_interval(&Variable::new("y"), &interval_0),
609        );
610        // r0: l0 -> l1, guard: true, action: x = x + 1
611        let abstract_rule_0 = IntervalTARule::new(
612            0,
613            Location::new("l0"),
614            Location::new("l1"),
615            IntervalConstraint::True,
616            vec![IntervalTAAction::new(
617                Variable::new("x"),
618                IntervalActionEffect::Inc(1),
619            )],
620        );
621
622        let r0 = error_graph.cs.get_sym_state_for_rule(&abstract_rule_0);
623
624        let initial_states = l0
625            .intersection(&l1.complement())
626            .intersection(&l2.complement())
627            .intersection(&i0)
628            .intersection(&r0);
629
630        assert!(initial_states.equal(&error_graph.initial_states()));
631    }
632
633    #[test]
634    fn test_get_non_error_intersection_empty() {
635        let ata = get_test_ata();
636        let mgr = taco_bdd::BDDManager::default();
637        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
638        let cs = builder.build();
639        let error_states = get_error_states(&cs);
640
641        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
642        let error_graph = error_graph_builder.build();
643
644        let l0 = error_graph.cs.get_sym_state_for_loc(&Location::new("l0"));
645        let l1 = error_graph.cs.get_sym_state_for_loc(&Location::new("l1"));
646        let l2 = error_graph.cs.get_sym_state_for_loc(&Location::new("l2"));
647        let error_states = l0
648            .complement()
649            .intersection(&l1.complement())
650            .intersection(&l2);
651
652        let res = error_graph.get_non_error_intersection(error_states);
653
654        assert!(!res.0);
655        assert!(res.1.is_empty());
656    }
657
658    #[test]
659    fn test_get_non_error_intersection() {
660        let ata = get_test_ata();
661        let mgr = taco_bdd::BDDManager::default();
662        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
663        let cs = builder.build();
664        let error_states = get_error_states(&cs);
665
666        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
667        let error_graph = error_graph_builder.build();
668
669        let l0 = error_graph.cs.get_sym_state_for_loc(&Location::new("l0"));
670        let l1 = error_graph.cs.get_sym_state_for_loc(&Location::new("l1"));
671        let l2 = error_graph.cs.get_sym_state_for_loc(&Location::new("l2"));
672        let error_states = l0
673            .complement()
674            .intersection(&l1.complement())
675            .intersection(&l2);
676
677        // I_0 = [0,1)
678        let interval_0 =
679            Interval::new_constant(Fraction::new(0, 1, false), Fraction::new(1, 1, false));
680
681        let i0 = error_graph
682            .cs
683            .get_sym_state_for_shared_interval(&Variable::new("x"), &interval_0);
684
685        let initial_states = l0
686            .intersection(&l1.complement())
687            .intersection(&l2.complement())
688            .intersection(&i0);
689
690        let res = error_graph.get_non_error_intersection(error_states.union(&initial_states));
691
692        assert!(res.0);
693        assert!(res.1.equal(&initial_states));
694    }
695
696    #[test]
697    fn test_get_error_intersection_empty() {
698        let ata = get_test_ata();
699        let mgr = taco_bdd::BDDManager::default();
700        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
701        let cs = builder.build();
702        let error_states = get_error_states(&cs);
703
704        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
705        let error_graph = error_graph_builder.build();
706
707        let l0 = error_graph.cs.get_sym_state_for_loc(&Location::new("l0"));
708
709        let res = error_graph.get_error_intersection(l0);
710
711        assert!(!res.0);
712        assert!(res.1.is_empty());
713    }
714
715    #[test]
716    fn test_get_error_intersection() {
717        let ata = get_test_ata();
718        let mgr = taco_bdd::BDDManager::default();
719        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
720        let cs = builder.build();
721        let error_states = get_error_states(&cs);
722
723        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
724        let error_graph = error_graph_builder.build();
725
726        let l0 = error_graph.cs.get_sym_state_for_loc(&Location::new("l0"));
727        let l1 = error_graph.cs.get_sym_state_for_loc(&Location::new("l1"));
728        let l2 = error_graph.cs.get_sym_state_for_loc(&Location::new("l2"));
729
730        // I_2 = [n-t,infty)
731        let interval_2 = Interval::new(
732            IntervalBoundary::Bound(Threshold::new(
733                [
734                    (Parameter::new("n"), 1.into()),
735                    (Parameter::new("t"), Fraction::new(1, 1, true)),
736                ],
737                0,
738            )),
739            false,
740            IntervalBoundary::new_infty(),
741            true,
742        );
743
744        let i2 = error_graph
745            .cs
746            .get_sym_state_for_shared_interval(&Variable::new("x"), &interval_2);
747
748        let error_states = l0
749            .complement()
750            .intersection(&l1.complement())
751            .intersection(&l2)
752            .intersection(&i2);
753
754        let builder = ZCSErrorGraphBuilder::new(error_graph.cs.clone(), error_states.clone());
755        let error_graph = builder.build();
756
757        // r0: l0 -> l1, guard: true, action: x = x + 1
758        let abstract_rule_0 = IntervalTARule::new(
759            0,
760            Location::new("l0"),
761            Location::new("l1"),
762            IntervalConstraint::True,
763            vec![IntervalTAAction::new(
764                Variable::new("x"),
765                IntervalActionEffect::Inc(1),
766            )],
767        );
768
769        let r0 = error_graph.cs.get_sym_state_for_rule(&abstract_rule_0);
770
771        let res = error_graph
772            .get_error_intersection(l0.clone().union(&l2).intersection(&i2).intersection(&r0));
773
774        assert!(res.0);
775        assert!(
776            res.1.equal(
777                &l0.complement()
778                    .intersection(&l1.complement())
779                    .intersection(&l2)
780                    .intersection(&i2)
781                    .intersection(&r0)
782            )
783        );
784    }
785
786    #[test]
787    fn test_contains_non_spurious_error_path() {
788        let mgr = taco_bdd::BDDManager::default();
789        let ata = get_test_ata();
790        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
791        let cs = builder.build();
792        let error_states = get_error_states(&cs);
793
794        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
795        let sym_err_graph = error_graph_builder.build();
796
797        let spec = ErrorTarget::Reach(UpwardsClosedSet::new_reach(
798            [(Location::new("l2"), 1)],
799            [Location::new("l0"), Location::new("l1")],
800        ));
801
802        let ctx = SMTBddContext::try_new(None).unwrap();
803
804        let smc_ctx = ZCSModelCheckerContext::new(
805            &ctx,
806            ZCSModelCheckerHeuristics::DecrementAndIncrementHeuristics,
807            &ata,
808            &spec,
809        );
810
811        let res = sym_err_graph.contains_non_spurious_error_path(&smc_ctx);
812
813        assert!(res.is_non_spurious());
814    }
815
816    #[test]
817    fn test_get_sym_state_for_loc() {
818        let ata = get_test_ata();
819        let mgr = taco_bdd::BDDManager::default();
820        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
821        let cs = builder.build();
822        let error_states = get_error_states(&cs);
823
824        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
825        let error_graph = error_graph_builder.build();
826
827        let l0 = error_graph.cs.get_sym_state_for_loc(&Location::new("l0"));
828        let l1 = error_graph.cs.get_sym_state_for_loc(&Location::new("l1"));
829        let l2 = error_graph.cs.get_sym_state_for_loc(&Location::new("l2"));
830
831        assert!(
832            error_graph
833                .get_sym_state_for_loc(&Location::new("l0"))
834                .equal(&l0)
835        );
836        assert!(
837            error_graph
838                .get_sym_state_for_loc(&Location::new("l1"))
839                .equal(&l1)
840        );
841        assert!(
842            error_graph
843                .get_sym_state_for_loc(&Location::new("l2"))
844                .equal(&l2)
845        );
846    }
847
848    #[test]
849    fn test_get_sym_state_for_shared_interval() {
850        let ata = get_test_ata();
851        let mgr = taco_bdd::BDDManager::default();
852        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
853        let cs = builder.build();
854        let error_states = get_error_states(&cs);
855
856        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
857        let error_graph = error_graph_builder.build();
858
859        // I_0 = [0,1)
860        let interval_0 =
861            Interval::new_constant(Fraction::new(0, 1, false), Fraction::new(1, 1, false));
862        let i0 = error_graph
863            .cs
864            .get_sym_state_for_shared_interval(&Variable::new("x"), &interval_0);
865
866        assert!(
867            error_graph
868                .get_sym_state_for_shared_interval(&Variable::new("x"), &interval_0)
869                .equal(&i0)
870        );
871    }
872
873    #[test]
874    fn test_get_sym_state_for_rule() {
875        let ata = get_test_ata();
876        let mgr = taco_bdd::BDDManager::default();
877        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
878        let cs = builder.build();
879        let error_states = get_error_states(&cs);
880
881        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
882        let error_graph = error_graph_builder.build();
883
884        // r0: l0 -> l1, guard: true, action: x = x + 1
885        let abstract_rule_0 = IntervalTARule::new(
886            0,
887            Location::new("l0"),
888            Location::new("l1"),
889            IntervalConstraint::True,
890            vec![IntervalTAAction::new(
891                Variable::new("x"),
892                IntervalActionEffect::Inc(1),
893            )],
894        );
895
896        let r0 = error_graph.cs.get_sym_state_for_rule(&abstract_rule_0);
897
898        assert!(
899            error_graph
900                .cs
901                .get_sym_state_for_rule(&abstract_rule_0)
902                .equal(&r0)
903        );
904    }
905
906    #[test]
907    fn test_transitions() {
908        let ata = get_test_ata();
909        let mgr = taco_bdd::BDDManager::default();
910        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
911        let cs = builder.build();
912        let error_states = get_error_states(&cs);
913        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
914        let error_graph = error_graph_builder.build();
915
916        let transitions = error_graph
917            .transitions()
918            .map(|r| r.abstract_rule().id())
919            .collect::<Vec<_>>();
920        assert_eq!(transitions.len(), 3);
921        assert!(transitions.contains(&0));
922        assert!(transitions.contains(&1));
923        assert!(transitions.contains(&2));
924    }
925
926    #[test]
927    fn test_new_empty_sym_state() {
928        let ata = get_test_ata();
929        let mgr = taco_bdd::BDDManager::default();
930        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
931        let cs = builder.build();
932        let error_states = get_error_states(&cs);
933
934        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
935        let error_graph = error_graph_builder.build();
936
937        let empty_state = error_graph.new_empty_sym_state();
938
939        assert!(empty_state.is_empty());
940    }
941
942    #[test]
943    fn test_compute_reachable_variable_assignments() {
944        let ata = get_test_ata();
945        let mgr = taco_bdd::BDDManager::default();
946        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
947        let cs = builder.build();
948        let error_states = get_error_states(&cs);
949
950        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
951        let error_graph = error_graph_builder.build();
952
953        let assignments = error_graph.compute_reachable_variable_assignments();
954
955        // possible variable assignments are:
956        // x = I_0
957        // x = I_1
958        // x = I_2
959        assert_eq!(assignments.len(), 3);
960
961        // I_0 = [0,1)
962        let interval_0 =
963            Interval::new_constant(Fraction::new(0, 1, false), Fraction::new(1, 1, false));
964
965        // I_2 = [n-t,infty)
966        let interval_2 = Interval::new(
967            IntervalBoundary::Bound(Threshold::new(
968                [
969                    (Parameter::new("n"), 1.into()),
970                    (Parameter::new("t"), Fraction::new(1, 1, true)),
971                ],
972                0,
973            )),
974            false,
975            IntervalBoundary::new_infty(),
976            true,
977        );
978        let mut assign2 = VariableAssignment::new();
979        assign2
980            .add_shared_var_interval(Variable::new("x"), interval_2.clone())
981            .unwrap();
982
983        let mut reached_i_0 = false;
984        let mut reached_i_1 = false;
985        let mut reached_i_2 = false;
986        for assign in assignments {
987            for (var, interval) in assign.assignment().assignments() {
988                if *var == Variable::new("y") {
989                    assert_eq!(interval, &interval_0);
990                }
991                if *var == Variable::new("x") {
992                    if interval == &interval_0 {
993                        reached_i_0 = true;
994                    } else if interval == &interval_2 {
995                        reached_i_2 = true;
996                    } else {
997                        reached_i_1 = true;
998                    }
999                }
1000            }
1001        }
1002        assert!(reached_i_0);
1003        assert!(reached_i_1);
1004        assert!(reached_i_2);
1005
1006        // I_1 = [1,\infty)
1007        let interval_1 = Interval::new(
1008            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
1009            false,
1010            IntervalBoundary::new_infty(),
1011            true,
1012        );
1013
1014        let all_possible_assignments = error_graph.get_all_possible_variable_assignments();
1015        assert_eq!(all_possible_assignments.len(), 6);
1016        assert!(all_possible_assignments.iter().any(|assign| {
1017            assign
1018                .assignment()
1019                .assignments()
1020                .any(|(var, interval)| *var == Variable::new("y") && *interval == interval_1)
1021        }));
1022    }
1023
1024    #[test]
1025    fn test_construct_steady_path() {
1026        let ata = get_test_ata();
1027        let mgr = taco_bdd::BDDManager::default();
1028        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
1029        let cs = builder.build();
1030        let error_states = get_error_states(&cs);
1031
1032        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
1033        let error_graph = error_graph_builder.build();
1034
1035        // I_0 = [0,1)
1036        let interval_0 =
1037            Interval::new_constant(Fraction::new(0, 1, false), Fraction::new(1, 1, false));
1038        let mut assignment = VariableAssignment::new();
1039        assignment
1040            .add_shared_var_interval(Variable::new("x"), interval_0.clone())
1041            .unwrap();
1042        assignment
1043            .add_shared_var_interval(Variable::new("y"), interval_0.clone())
1044            .unwrap();
1045        let assignment = error_graph.cs.get_sym_var_assignment(assignment);
1046
1047        let initial_states = error_graph.initial_states();
1048
1049        let steady_path =
1050            error_graph.construct_steady_path(initial_states.clone(), assignment.clone());
1051
1052        println!("{:?}", steady_path._reachable_states());
1053        println!("{:?}", initial_states);
1054
1055        assert!(steady_path._reachable_states().equal(&initial_states));
1056        assert!(
1057            steady_path
1058                ._reachable_states()
1059                .remove_assignment(&assignment)
1060                .is_empty()
1061        );
1062    }
1063
1064    /// Used to construct the SymbolicErrorGraph for the following threshold automaton
1065    /// where cycles need to be unfolded to find a counterexample:
1066    ///
1067    /// Threshold Automaton:
1068    /// Locations: {l0,l1,l2,l3}
1069    /// Initial location: l0
1070    /// Parameter: {n}
1071    /// Shared Variables: x,y
1072    /// Initial location constraints: l0 = n & l1 = 0 & l2 = 0 & l3 = 0
1073    /// Rules:
1074    ///     r0: l0 -> l1, guard: x < 1, action: x = x + 1
1075    ///     r1: l1 -> l2, guard: true, action: none
1076    ///     r2: l2 -> l1, guard: true, action: y = y + 1
1077    ///     r3: l0 -> l3, guard: y >= 5, action: none
1078    fn get_test_cycle_ata() -> IntervalThresholdAutomaton {
1079        let ta_builder =
1080            taco_threshold_automaton::general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder::new("test")
1081                .with_locations(vec![
1082                    Location::new("l0"),
1083                    Location::new("l1"),
1084                    Location::new("l2"),
1085                    Location::new("l3"),
1086                ])
1087                .unwrap()
1088                .with_variables(vec![Variable::new("x"), Variable::new("y")])
1089                .unwrap()
1090                .with_parameters(vec![
1091                    Parameter::new("n"),
1092                ])
1093                .unwrap()
1094                .initialize()
1095                .with_initial_location_constraints(vec![
1096                    LocationConstraint::ComparisonExpression(
1097                        Box::new(IntegerExpression::Atom(Location::new("l0"))),
1098                        ComparisonOp::Eq,
1099                        Box::new(
1100                            IntegerExpression::Param(Parameter::new("n"))
1101                        ),
1102                    ),
1103                    LocationConstraint::ComparisonExpression(
1104                        Box::new(IntegerExpression::Atom(Location::new("l1"))),
1105                        ComparisonOp::Eq,
1106                        Box::new(IntegerExpression::Const(0)),
1107                    ),
1108                    LocationConstraint::ComparisonExpression(
1109                        Box::new(IntegerExpression::Atom(Location::new("l2"))),
1110                        ComparisonOp::Eq,
1111                        Box::new(IntegerExpression::Const(0)),
1112                    ),
1113                    LocationConstraint::ComparisonExpression(
1114                        Box::new(IntegerExpression::Atom(Location::new("l3"))),
1115                        ComparisonOp::Eq,
1116                        Box::new(IntegerExpression::Const(0)),
1117                    ),
1118                ])
1119                .unwrap()
1120                .with_resilience_conditions([ParameterConstraint::ComparisonExpression(
1121                    Box::new(IntegerExpression::Atom(Parameter::new("n"))),
1122                    ComparisonOp::Gt,
1123                    Box::new(IntegerExpression::Const(1)),
1124                )])
1125                .unwrap()
1126                .with_initial_variable_constraints([BooleanVarConstraint::ComparisonExpression(Box::new(IntegerExpression::Atom(Variable::new("x"))), ComparisonOp::Eq, Box::new(IntegerExpression::Const(0))), BooleanVarConstraint::ComparisonExpression(Box::new(IntegerExpression::Atom(Variable::new("y"))), ComparisonOp::Eq, Box::new(IntegerExpression::Const(0)))])
1127                .unwrap()
1128                .with_rules(vec![
1129                    RuleBuilder::new(0, Location::new("l0"), Location::new("l1"))
1130                        .with_guard(
1131                            BooleanVarConstraint::ComparisonExpression(
1132                                Box::new(IntegerExpression::Atom(Variable::new("x"))),
1133                                ComparisonOp::Lt,
1134                                Box::new(IntegerExpression::Const(1)),
1135                            )
1136                        )
1137                        .with_action(
1138                            Action::new(
1139                                Variable::new("x"),
1140                                IntegerExpression::Atom(Variable::new("x"))
1141                                    + IntegerExpression::Const(1),
1142                            )
1143                            .unwrap(),
1144                        )
1145                        .build(),
1146                        RuleBuilder::new(1, Location::new("l1"), Location::new("l2"))
1147                        .build(),
1148                    RuleBuilder::new(2, Location::new("l2"), Location::new("l1"))
1149                    .with_action(
1150                        Action::new(
1151                            Variable::new("y"),
1152                            IntegerExpression::Atom(Variable::new("y"))
1153                                + IntegerExpression::Const(1),
1154                        )
1155                        .unwrap(),
1156                    )
1157                        .build(),
1158                    RuleBuilder::new(3, Location::new("l0"), Location::new("l3"))
1159                    .with_guard(
1160                        BooleanVarConstraint::ComparisonExpression(
1161                            Box::new(IntegerExpression::Atom(Variable::new("y"))),
1162                            ComparisonOp::Geq,
1163                            Box::new(IntegerExpression::Const(5)),
1164                        )
1165                    )
1166                        .build(),
1167                ])
1168                .unwrap();
1169        let ta = ta_builder.build();
1170        let lia =
1171            taco_threshold_automaton::lia_threshold_automaton::LIAThresholdAutomaton::try_from(
1172                ta.clone(),
1173            )
1174            .unwrap();
1175
1176        let mut interval_tas = IntervalTABuilder::new(lia, SMTSolverBuilder::default(), vec![])
1177            .build()
1178            .unwrap();
1179        interval_tas.next().unwrap()
1180    }
1181
1182    #[test]
1183    fn test_cycle_ta_for_spuriousness() {
1184        let ata = get_test_cycle_ata();
1185        let mgr = taco_bdd::BDDManager::default();
1186        let builder: ZCSBuilder = ZCSBuilder::new(&mgr, &ata);
1187        let cs = builder.build();
1188        let l3 = cs.get_sym_state_for_loc(&Location::new("l3"));
1189        // error states are those where l3 > 0
1190        let error_states = l3;
1191
1192        let error_graph_builder = ZCSErrorGraphBuilder::new(cs, error_states);
1193        let sym_err_graph = error_graph_builder.build();
1194
1195        let spec = ErrorTarget::Reach(UpwardsClosedSet::new_cover([Location::new("l3")]));
1196
1197        let ctx = SMTBddContext::try_new(None).unwrap();
1198        let smc_ctx = ZCSModelCheckerContext::new(
1199            &ctx,
1200            ZCSModelCheckerHeuristics::DecrementAndIncrementHeuristics,
1201            &ata,
1202            &spec,
1203        );
1204
1205        let res = sym_err_graph.contains_non_spurious_error_path(&smc_ctx);
1206
1207        assert!(res.is_non_spurious());
1208    }
1209}
taco_zcs_model_checker/zcs_error_graph.rs

taco_zcs_model_checker/
zcs_error_graph.rs
