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

taco_zcs_model_checker/
zcs_error_graph.rs
