taco_zcs_model_checker/
paths.rs

1//! This file contains the definitions of steady error paths
2//! that are used in the symbolic model checker (ZCS model checker).
3
4use std::collections::HashMap;
5use std::fmt::Display;
6use taco_interval_ta::IntervalThresholdAutomaton;
7use taco_interval_ta::interval::Interval;
8use taco_model_checker::internal_spec::ErrorTarget;
9use taco_threshold_automaton::RuleDefinition;
10use taco_threshold_automaton::expressions::Variable;
11use taco_threshold_automaton::general_threshold_automaton::Rule;
12use zcs::{SymbolicTransition, ZCSStates};
13
14use crate::ZCSModelCheckerContext;
15use crate::smt_encoder_steady::SMTEncoderSteady;
16use crate::smt_encoder_steady::SpuriousResult;
17use crate::zcs;
18use crate::zcs::SymbolicVariableAssignment;
19use crate::zcs_error_graph::ZCSErrorGraph;
20use taco_threshold_automaton::ActionDefinition;
21use taco_threshold_automaton::general_threshold_automaton::UpdateExpression;
22use taco_threshold_automaton::general_threshold_automaton::UpdateExpression::{Dec, Inc};
23
24/// Type that represents a steady error path
25///
26/// A steady error path consists of a sequence of steady paths π_0, ... , π_k
27/// and a sequence of symbolic transitions r_0,...,r_{k-1}
28/// where ∀ 0 < i \leq k: π_i is reached by applying rule r_{i-1} from π_{i-1}
29#[derive(Debug, Clone)]
30pub struct SteadyErrorPath<'a> {
31    steady_paths: Vec<SteadyPath>,
32    step_transitions: Vec<SymbolicTransition>,
33    // underlying symbolic error graph
34    error_graph: &'a ZCSErrorGraph<'a>,
35}
36impl<'a> SteadyErrorPath<'a> {
37    /// creates a new Steady Error Path for a given SteadyPath
38    pub fn new(steady_path: SteadyPath, error_graph: &'a ZCSErrorGraph) -> Self {
39        SteadyErrorPath {
40            steady_paths: vec![steady_path],
41            step_transitions: Vec::new(),
42            error_graph,
43        }
44    }
45    /// returns the last SymbolicState of the last steady path
46    pub fn get_last_states(&self) -> ZCSStates {
47        self.steady_paths
48            .last()
49            .expect("the steady error path is empty")
50            .reachable_states
51            .clone()
52    }
53    /// returns the last SymbolicVariableAssignment of the last steady path
54    pub fn get_last_assignment(&self) -> SymbolicVariableAssignment {
55        self.steady_paths
56            .last()
57            .expect("the steady error path is empty")
58            .variable_assignment
59            .clone()
60    }
61    /// adds a new steady path to the steady error path that is reached with the given transition rule
62    pub fn add_successor(&mut self, step_transition: &SymbolicTransition, steady_path: SteadyPath) {
63        self.step_transitions.push(step_transition.clone());
64        self.steady_paths.push(steady_path);
65    }
66
67    /// checks if the steady error path is non-spurious
68    ///
69    /// `reached_error_states` indicates if the last steady path reached an error state
70    pub fn is_non_spurious(
71        &self,
72        reached_error_state: bool,
73        smc_ctx: &ZCSModelCheckerContext,
74    ) -> SpuriousResult {
75        let mut smt_encoder = SMTEncoderSteady::new(
76            smc_ctx.smt_bdd_context().smt_solver_builder().clone(),
77            smc_ctx.ta(),
78            self,
79        );
80
81        let ErrorTarget::Reach(spec) = smc_ctx.spec() else {
82            todo!("Remove once implemented");
83        };
84
85        if reached_error_state {
86            smt_encoder.steady_is_non_spurious(Some(spec))
87        } else {
88            smt_encoder.steady_is_non_spurious(None)
89        }
90    }
91
92    /// returns the length of different contexts that is defined by the number of steady paths
93    pub fn length_configurations(&self) -> u32 {
94        self.steady_paths.len().try_into().unwrap()
95    }
96    /// returns an ordered iterator over all applied rules including the step rules
97    pub fn concrete_rules_ordered(
98        &self,
99        ta: &'a IntervalThresholdAutomaton,
100    ) -> impl Iterator<Item = &'a Rule> {
101        let mut ordered_rule_vec = Vec::new();
102        for i in 0..self.steady_paths.len() {
103            let path = &self.steady_paths[i];
104            for tr in &path.transitions {
105                ordered_rule_vec.push(ta.get_derived_rule(tr.abstract_rule()));
106            }
107            // add step rule
108            if i < self.steady_paths.len() - 1 {
109                let step_rule = &self.step_transitions[i];
110                ordered_rule_vec.push(ta.get_derived_rule(step_rule.abstract_rule()));
111            }
112        }
113        ordered_rule_vec.into_iter()
114    }
115
116    /// returns an ordered iterator over the steady paths
117    pub fn steady_paths(&self) -> impl Iterator<Item = &SteadyPath> {
118        self.steady_paths.iter()
119    }
120
121    /// returns if the last steady error path is monotonic
122    /// i.e., if for every shared variable the value is either only increasing or only decreasing
123    pub fn last_is_monotonic(&self, ta: &IntervalThresholdAutomaton) -> bool {
124        let last_steady_path = self
125            .steady_paths
126            .last()
127            .expect("the steady error path is empty");
128        for shared in self.error_graph.variables() {
129            let mut inc_rules = false;
130            let mut dec_rules = false;
131            for rule in last_steady_path.transitions() {
132                let rule = ta.get_derived_rule(rule.abstract_rule());
133                let action_map = rule
134                    .actions()
135                    .map(|action| (action.variable(), action.update().clone()))
136                    .collect::<HashMap<_, _>>();
137                let update = action_map
138                    .get(shared)
139                    .unwrap_or(&UpdateExpression::Unchanged);
140                match update {
141                    Inc(_) => {
142                        inc_rules = true;
143                        if dec_rules {
144                            return false;
145                        }
146                    }
147                    Dec(_) => {
148                        dec_rules = true;
149                        if inc_rules {
150                            return false;
151                        }
152                    }
153                    UpdateExpression::Reset | UpdateExpression::Unchanged => {}
154                }
155            }
156        }
157        true
158    }
159}
160
161impl Display for SteadyErrorPath<'_> {
162    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
163        writeln!(
164            f,
165            "Symbolic Path with {} steady paths:",
166            self.steady_paths.len(),
167        )?;
168
169        fn possible_locations(
170            f: &mut std::fmt::Formatter<'_>,
171            error_graph: &ZCSErrorGraph,
172            sym_states: &ZCSStates,
173        ) -> Result<(), Box<dyn std::error::Error>> {
174            let mut uncovered_locations = Vec::new();
175            let mut covered_locations = Vec::new();
176            let mut both_locations = Vec::new();
177            for loc in error_graph.locations() {
178                let loc_sym_states = error_graph.get_sym_state_for_loc(loc);
179                let covered = !sym_states.intersection(&loc_sym_states).is_empty();
180                let uncovered = !sym_states
181                    .intersection(&loc_sym_states.complement())
182                    .is_empty();
183                if covered && uncovered {
184                    both_locations.push(loc);
185                } else if covered {
186                    covered_locations.push(loc.clone());
187                } else if uncovered {
188                    uncovered_locations.push(loc.clone());
189                }
190            }
191            writeln!(f, "covered locations: {:?}", covered_locations)?;
192            writeln!(f, "uncovered locations: {:?}", uncovered_locations)?;
193            writeln!(
194                f,
195                "locations which can be covered or uncovered: {:?}",
196                both_locations
197            )?;
198            Ok(())
199        }
200
201        let mut rule_index = 0;
202        for steady_path in &self.steady_paths {
203            writeln!(f, "Steady Path")?;
204
205            let _ = possible_locations(f, self.error_graph, &steady_path.reachable_states);
206            let rules = steady_path.transitions.clone();
207            writeln!(
208                f,
209                "Possible rules: {:?}",
210                rules
211                    .iter()
212                    .map(|r| "r_".to_owned() + &r.abstract_rule().id().to_string())
213                    .collect::<Vec<String>>()
214            )?;
215            writeln!(
216                f,
217                "Variable Assignment:\n {}",
218                steady_path.variable_assignment.assignment()
219            )?;
220
221            if rule_index < self.step_transitions.len() {
222                writeln!(f, "        |",)?;
223                writeln!(
224                    f,
225                    "        | reach new fragment by applying rule {}",
226                    "r_".to_owned()
227                        + &self.step_transitions[rule_index]
228                            .abstract_rule()
229                            .id()
230                            .to_string()
231                )?;
232                writeln!(f, "        V")?;
233                rule_index += 1;
234            }
235        }
236
237        Ok(())
238    }
239}
240
241/// Type that represents a steady path
242///
243/// A steady path describes a path fragment in which the context (variable) doesn't change
244/// where `reachable_state` describes the set of symbolic states that can be reached within this path fragment
245/// and `transitions` describes the set of transitions that can be applied.
246#[derive(Debug, Clone)]
247pub struct SteadyPath {
248    transitions: Vec<SymbolicTransition>,
249    reachable_states: ZCSStates,
250    variable_assignment: SymbolicVariableAssignment,
251}
252impl SteadyPath {
253    /// creates a new steady path for a given set of transitions, set of reachable states and a variable assignment
254    pub fn new(
255        transitions: Vec<&SymbolicTransition>,
256        reachable_states: ZCSStates,
257        variable_assignment: SymbolicVariableAssignment,
258    ) -> Self {
259        let mut transitions_without_duplicates = Vec::new();
260        for tr in transitions {
261            if !transitions_without_duplicates.contains(tr) {
262                transitions_without_duplicates.push(tr.clone());
263            }
264        }
265        SteadyPath {
266            transitions: transitions_without_duplicates,
267            reachable_states,
268            variable_assignment,
269        }
270    }
271    /// returns the length of the transitions inside the steady path
272    pub fn length_transitions(&self) -> u32 {
273        self.transitions.len().try_into().unwrap()
274    }
275    /// returns an iterator over the transitions
276    pub fn transitions(&self) -> impl Iterator<Item = &SymbolicTransition> {
277        self.transitions.iter()
278    }
279    /// returns the concrete variable assignment of the steady path
280    pub fn variable_assignment(&self) -> &VariableAssignment {
281        self.variable_assignment.assignment()
282    }
283    /// returns the reachable states of the steady path
284    pub fn _reachable_states(&self) -> &ZCSStates {
285        &self.reachable_states
286    }
287}
288
289/// Type that represents a variable assignment
290///
291/// An variable assignment maps each shared variable to an interval
292#[derive(Debug, Clone)]
293pub struct VariableAssignment {
294    assignment: HashMap<Variable, Interval>,
295}
296impl VariableAssignment {
297    /// creates a new variable assignment
298    pub fn new() -> Self {
299        VariableAssignment {
300            assignment: HashMap::new(),
301        }
302    }
303
304    /// this function is only used for generating tests in smt_encoder
305    pub fn new_for_testing(assignment: HashMap<Variable, Interval>) -> Self {
306        VariableAssignment { assignment }
307    }
308
309    /// add a new assignment for the given shared variable with the given interval
310    /// returns an error if there already exists an entry for Variable `shared`
311    pub fn add_shared_var_interval(
312        &mut self,
313        shared: Variable,
314        interval: Interval,
315    ) -> Result<(), VariableAssignmentError> {
316        if self.assignment.contains_key(&shared) {
317            return Err(VariableAssignmentError::VariableAlreadyAssigned(shared));
318        }
319        self.assignment.insert(shared, interval);
320        Ok(())
321    }
322    /// iterator over interval assignments for each shared variable
323    pub fn assignments(&self) -> impl Iterator<Item = (&Variable, &Interval)> {
324        self.assignment.iter()
325    }
326}
327impl Default for VariableAssignment {
328    fn default() -> Self {
329        Self::new()
330    }
331}
332impl Display for VariableAssignment {
333    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
334        for (shared, interval) in self.assignment.iter() {
335            writeln!(f, "    {shared}: {interval}")?;
336        }
337        Ok(())
338    }
339}
340
341/// Custom Error type to indicate an error
342/// when operating on a VariableAssignment
343#[derive(Debug, Clone)]
344pub enum VariableAssignmentError {
345    /// Error indicating that there already exists entry for this shared variable
346    VariableAlreadyAssigned(Variable),
347}
348
349impl std::error::Error for VariableAssignmentError {}
350
351impl Display for VariableAssignmentError {
352    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
353        match self {
354            VariableAssignmentError::VariableAlreadyAssigned(shared) => {
355                write!(
356                    f,
357                    "There already exists an entry for the shared variable {shared}"
358                )
359            }
360        }
361    }
362}
363
364#[cfg(test)]
365mod tests {
366
367    use super::VariableAssignment;
368    use crate::paths::VariableAssignmentError;
369    use crate::zcs::ZCS;
370    use crate::zcs::ZCSStates;
371    use std::vec;
372    use taco_interval_ta::IntervalThresholdAutomaton;
373    use taco_interval_ta::builder::IntervalTABuilder;
374    use taco_interval_ta::interval::Interval;
375    use taco_interval_ta::interval::IntervalBoundary;
376    use taco_smt_encoder::SMTSolverBuilder;
377    use taco_threshold_automaton::BooleanVarConstraint;
378    use taco_threshold_automaton::LocationConstraint;
379    use taco_threshold_automaton::ParameterConstraint;
380    use taco_threshold_automaton::expressions::ComparisonOp;
381    use taco_threshold_automaton::expressions::IntegerExpression;
382    use taco_threshold_automaton::expressions::{Location, Parameter, Variable};
383    use taco_threshold_automaton::general_threshold_automaton::Action;
384    use taco_threshold_automaton::general_threshold_automaton::builder::RuleBuilder;
385
386    /// returns the underlying threshold automaton for these test cases
387    ///
388    ///  /// Threshold Automaton:
389    /// Locations: {l0,l1,l2}
390    /// Initial location: l0
391    /// Parameter: {n,t}
392    /// Shared Variable: x
393    /// Initial location constraints: l0 = n - t & l1 = 0 & l2 = 0
394    /// Rules:
395    ///     r0: l0 -> l1, guard: true, action: x = x + 1
396    ///     r1: l0 -> l2, guard: x >= n - t, action: none
397    ///     r2: l1 -> l2, guard: x >= n - t, action: none
398    ///
399    /// Abstract Threshold Automaton:
400    /// Intervals for x: I_0 = [0,1), I_1 = [1,n-t), I_2 = [n-t, infty)
401    /// Interval Order: I_0 < I_1 < I_2
402    /// Abstract Rules:
403    ///     r0: l0 -> l1, guard: true, action: x = x + 1
404    ///     r1: l0 -> l1, guard: x = I_2, action: none
405    ///     r2: l1 -> l2, guard: x = I_2, action: none
406    ///
407    /// Structure of the symbolic 01-counter system:
408    ///     [(1,0,0),I_0] --- r0 ---> [(-,1,0),{I_0,I_1}]
409    ///     [(-,1,0),{I_0,I_1}] --- r0 ---> [(-,1,0),{I_0,I_1,I_2}]
410    ///     [(-,1,0),{I_0,I_1,I_2}] --- r0 ---> [(-,1,0),{I_0,I_1,I_2}]
411    ///     [(-,1,0),I_2] --- r1 ---> [(-,1,1),I_2]
412    ///     [(-,1,0),I_2] --- r2 ---> [(-,-,1),I_2]
413    ///
414    /// The backwards reachability analysis for the set of error states {[(0,0,1),-]} looks as follows (already visited states are ignored):
415    ///     level 1: [(0,0,1),-] <---- r1 ---- [(1,0,-),I_2],
416    ///              [(0,0,1),-] <---- r2 ---- [(0,1,-),I_2]
417    ///     level 2: [(1,0,-),I_2] <--- r2 --- [(1,1,-),I_2],
418    ///              [(0,1,-),I_2] <--- r1 --- [(1,1,-),I_2],
419    ///              [(0,1,-),I_1] <--- r0 --- [(1,-,-),{I_1,I_2}],
420    ///     level 3: [(1,-,-),{I_1,I_2}] <--- r0 --- [(1,-,-),{I_0,I_1,I_2}]
421    ///
422    /// The symbolic error graph for the set of error states {[(0,0,1),-]} looks as follows:
423    ///     level 0: {[(0,0,1),-]}
424    ///     level 1: {[(1,0,-),I_2]&r1, [(0,1,-),I_2]&r2} \cup {[(1,0,-),I_2]&r0]} (added in level 3)
425    ///     level 2: {[(1,-,-),I_1]&r0), [(1,1,-),I_2] &(r0 | r1 | r2)} (&r1,r2 added in the next iteration)
426    ///     level 3: {[(1,-,-),I_0]&r0}
427    fn _get_ata() -> IntervalThresholdAutomaton {
428        let ta_builder =
429            taco_threshold_automaton::general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder::new("test")
430                .with_locations(vec![
431                    Location::new("l0"),
432                    Location::new("l1"),
433                    Location::new("l2"),
434                ])
435                .unwrap()
436                .with_variable(Variable::new("x"))
437                .unwrap()
438                .with_parameters(vec![
439                    Parameter::new("n"),
440                    Parameter::new("t"),
441                    Parameter::new("f"),
442                ])
443                .unwrap()
444                .initialize()
445                .with_resilience_conditions([ParameterConstraint::ComparisonExpression(
446                    Box::new(IntegerExpression::Atom(Parameter::new("n")) - IntegerExpression::Atom(Parameter::new("t"))),
447                    ComparisonOp::Gt,
448                    Box::new(IntegerExpression::Const(1)),
449                )])
450                .unwrap()
451                .with_initial_location_constraints(vec![
452                    LocationConstraint::ComparisonExpression(
453                        Box::new(IntegerExpression::Atom(Location::new("l0"))),
454                        ComparisonOp::Eq,
455                        Box::new(
456                            IntegerExpression::Param(Parameter::new("n"))
457                                - IntegerExpression::Param(Parameter::new("t")),
458                        ),
459                    ),
460                    LocationConstraint::ComparisonExpression(
461                        Box::new(IntegerExpression::Atom(Location::new("l1"))),
462                        ComparisonOp::Eq,
463                        Box::new(IntegerExpression::Const(0)),
464                    ),
465                    LocationConstraint::ComparisonExpression(
466                        Box::new(IntegerExpression::Atom(Location::new("l2"))),
467                        ComparisonOp::Eq,
468                        Box::new(IntegerExpression::Const(0)),
469                    ),
470                ])
471                .unwrap()
472                .with_initial_variable_constraints(vec![
473                    BooleanVarConstraint::ComparisonExpression(
474                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
475                        ComparisonOp::Eq,
476                        Box::new(IntegerExpression::Const(0)),
477                    ),
478                ])
479                .unwrap()
480                .with_rules(vec![
481                    RuleBuilder::new(0, Location::new("l0"), Location::new("l1"))
482                        .with_action(
483                            Action::new(
484                                Variable::new("x"),
485                                IntegerExpression::Atom(Variable::new("x"))
486                                    + IntegerExpression::Const(1),
487                            )
488                            .unwrap(),
489                        )
490                        .build(),
491                    RuleBuilder::new(1, Location::new("l0"), Location::new("l2"))
492                        .with_guard(BooleanVarConstraint::ComparisonExpression(
493                            Box::new(IntegerExpression::Atom(Variable::new("x"))),
494                            ComparisonOp::Geq,
495                            Box::new(
496                                IntegerExpression::Param(Parameter::new("n"))
497                                    - IntegerExpression::Param(Parameter::new("t")),
498                            ),
499                        ))
500                        .build(),
501                    RuleBuilder::new(2, Location::new("l1"), Location::new("l2"))
502                        .with_guard(BooleanVarConstraint::ComparisonExpression(
503                            Box::new(IntegerExpression::Atom(Variable::new("x"))),
504                            ComparisonOp::Geq,
505                            Box::new(
506                                IntegerExpression::Param(Parameter::new("n"))
507                                    - IntegerExpression::Param(Parameter::new("t")),
508                            ),
509                        ))
510                        .build(),
511                ])
512                .unwrap();
513        let ta = ta_builder.build();
514        let lia =
515            taco_threshold_automaton::lia_threshold_automaton::LIAThresholdAutomaton::try_from(
516                ta.clone(),
517            )
518            .unwrap();
519
520        let mut interval_tas = IntervalTABuilder::new(lia, SMTSolverBuilder::default(), vec![])
521            .build()
522            .unwrap();
523        let ata = interval_tas.next().unwrap();
524
525        let nxt = interval_tas.next();
526        assert!(nxt.is_none(), "Got additional ta {}", nxt.unwrap());
527
528        ata
529    }
530
531    /// returns the set of error states for these test cases
532    fn _get_error_states(cs: &ZCS) -> ZCSStates {
533        let l0 = cs.get_sym_state_for_loc(&Location::new("l0"));
534        let l1 = cs.get_sym_state_for_loc(&Location::new("l1"));
535        let l2 = cs.get_sym_state_for_loc(&Location::new("l2"));
536        l0.complement()
537            .intersection(&l1.complement())
538            .intersection(&l2)
539    }
540
541    #[test]
542    fn test_variable_assignment() {
543        let mut var_assignment = VariableAssignment::new();
544
545        let test_interval = Interval::new(
546            IntervalBoundary::new_infty(),
547            true,
548            IntervalBoundary::new_infty(),
549            true,
550        );
551
552        let mut res =
553            var_assignment.add_shared_var_interval(Variable::new("x"), test_interval.clone());
554
555        assert!(res.is_ok());
556
557        assert!(var_assignment.assignment.contains_key(&Variable::new("x")));
558        assert_eq!(var_assignment.assignment.len(), 1);
559
560        let cloned_assign = var_assignment.clone();
561        let mut assign_it = cloned_assign.assignments();
562
563        let mut next = assign_it.next();
564
565        assert!(next.is_some());
566        assert_eq!(*next.unwrap().0, Variable::new("x"));
567
568        next = assign_it.next();
569
570        assert!(next.is_none());
571
572        res = var_assignment.add_shared_var_interval(Variable::new("x"), test_interval);
573
574        assert!(res.is_err());
575
576        assert!(matches!(
577            res.clone().unwrap_err(),
578            VariableAssignmentError::VariableAlreadyAssigned(_)
579        ));
580    }
581
582    /// Construct the following threshold automaton for these test cases:
583    ///
584    /// Threshold Automaton:
585    /// Locations: {l0,l1,l2}
586    /// Initial location: l0
587    /// Parameter: {n,t}
588    /// Shared Variable: x, y(dummy variable)
589    /// Initial location constraints: l0 = n - t & l1 = 0 & l2 = 0
590    /// Rules:
591    ///     r0: l0 -> l1, guard: true, action: x = x + 1
592    ///     r1: l0 -> l2, guard: x >= n - t, action: none
593    ///     r2: l1 -> l2, guard: x >= n - t, action: none
594    ///
595    /// Abstract Threshold Automaton:
596    /// Intervals for x: I_0 = [0,1), I_1 = [1,n-t), I_2 = [n-t, infty)
597    /// Interval Order: I_0 < I_1 < I_2
598    /// Abstract Rules:
599    ///     r0: l0 -> l1, guard: true, action: x = x + 1
600    ///     r1: l0 -> l1, guard: x = I_2, action: none
601    ///     r2: l1 -> l2, guard: x = I_2, action: none
602    ///
603    /// Structure of the symbolic 01-counter system:
604    ///     [(1,0,0),I_0] --- r0 ---> [(-,1,0),{I_0,I_1}]
605    ///     [(-,1,0),{I_0,I_1}] --- r0 ---> [(-,1,0),{I_0,I_1,I_2}]
606    ///     [(-,1,0),{I_0,I_1,I_2}] --- r0 ---> [(-,1,0),{I_0,I_1,I_2}]
607    ///     [(-,1,0),I_2] --- r1 ---> [(-,1,1),I_2]
608    ///     [(-,1,0),I_2] --- r2 ---> [(-,-,1),I_2]
609    ///
610    /// The backwards reachability analysis for the set of error states {[(0,0,1),-]} looks as follows (already visited states are ignored):
611    ///     level 1: [(0,0,1),-] <---- r1 ---- [(1,0,-),I_2],
612    ///              [(0,0,1),-] <---- r2 ---- [(0,1,-),I_2]
613    ///     level 2: [(1,0,-),I_2] <--- r2 --- [(1,1,-),I_2],
614    ///              [(0,1,-),I_2] <--- r1 --- [(1,1,-),I_2],
615    ///              [(0,1,-),I_1] <--- r0 --- [(1,-,-),{I_1,I_2}],
616    ///     level 3: [(1,-,-),{I_1,I_2}] <--- r0 --- [(1,-,-),{I_0,I_1,I_2}]
617    ///
618    /// The symbolic error graph for the set of error states {[(-,-,1),-]} looks as follows:
619    ///     level 0: {[(-,-,1),-]}
620    ///     level 1: {[(1,0,-),I_2]&r1, [(0,1,-),I_2]&r2} \cup {[(1,0,-),I_2]&r0]} (added in level 3)
621    ///     level 2: {[(1,-,-),I_1]&r0), [(1,1,-),I_2] &(r0 | r1 | r2)} (&r1,r2 added in the next iteration)
622    ///     level 3: {[(1,-,-),I_0]&r0}
623    fn _get_ata_for_spurious_checking() -> IntervalThresholdAutomaton {
624        let ta_builder =
625            taco_threshold_automaton::general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder::new("test")
626                .with_locations(vec![
627                    Location::new("l0"),
628                    Location::new("l1"),
629                    Location::new("l2"),
630                ])
631                .unwrap()
632                .with_variables(vec![Variable::new("x"), Variable::new("y")])
633                .unwrap()
634                .with_parameters(vec![
635                    Parameter::new("n"),
636                    Parameter::new("t"),
637                    Parameter::new("f"),
638                ])
639                .unwrap()
640                .initialize()
641                .with_initial_location_constraints(vec![
642                    LocationConstraint::ComparisonExpression(
643                        Box::new(IntegerExpression::Atom(Location::new("l0"))),
644                        ComparisonOp::Eq,
645                        Box::new(
646                            IntegerExpression::Param(Parameter::new("n"))
647                                - IntegerExpression::Param(Parameter::new("t")),
648                        ),
649                    ),
650                    LocationConstraint::ComparisonExpression(
651                        Box::new(IntegerExpression::Atom(Location::new("l1"))),
652                        ComparisonOp::Eq,
653                        Box::new(IntegerExpression::Const(0)),
654                    ),
655                    LocationConstraint::ComparisonExpression(
656                        Box::new(IntegerExpression::Atom(Location::new("l2"))),
657                        ComparisonOp::Eq,
658                        Box::new(IntegerExpression::Const(0)),
659                    ),
660                ])
661                .unwrap()
662                .with_resilience_conditions([ParameterConstraint::ComparisonExpression(
663                    Box::new(IntegerExpression::Atom(Parameter::new("n")) - IntegerExpression::Atom(Parameter::new("t"))),
664                    ComparisonOp::Gt,
665                    Box::new(IntegerExpression::Const(1)),
666                )])
667                .unwrap()
668                .with_initial_variable_constraints(vec![BooleanVarConstraint::ComparisonExpression(
669                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
670                    ComparisonOp::Eq,
671                    Box::new(IntegerExpression::Const(0)),
672                )])
673                .unwrap()
674                .with_rules(vec![
675                    RuleBuilder::new(0, Location::new("l0"), Location::new("l1"))
676                        .with_action(
677                            Action::new(
678                                Variable::new("x"),
679                                IntegerExpression::Atom(Variable::new("x"))
680                                    + IntegerExpression::Const(1),
681                            )
682                            .unwrap(),
683                        )
684                        .build(),
685                    RuleBuilder::new(1, Location::new("l0"), Location::new("l2"))
686                        .with_guard(BooleanVarConstraint::ComparisonExpression(
687                            Box::new(IntegerExpression::Atom(Variable::new("x"))),
688                            ComparisonOp::Geq,
689                            Box::new(
690                                IntegerExpression::Param(Parameter::new("n"))
691                                    - IntegerExpression::Param(Parameter::new("t")),
692                            ),
693                        ))
694                        .build(),
695                    RuleBuilder::new(2, Location::new("l1"), Location::new("l2"))
696                        .with_guard(BooleanVarConstraint::ComparisonExpression(
697                            Box::new(IntegerExpression::Atom(Variable::new("x"))),
698                            ComparisonOp::Geq,
699                            Box::new(
700                                IntegerExpression::Param(Parameter::new("n"))
701                                    - IntegerExpression::Param(Parameter::new("t")),
702                            ),
703                        ))
704                        .build(),
705                ])
706                .unwrap();
707        let ta = ta_builder.build();
708        let lia =
709            taco_threshold_automaton::lia_threshold_automaton::LIAThresholdAutomaton::try_from(
710                ta.clone(),
711            )
712            .unwrap();
713
714        let mut interval_tas = IntervalTABuilder::new(lia, SMTSolverBuilder::default(), vec![])
715            .build()
716            .unwrap();
717        let ata = interval_tas.next().unwrap();
718
719        let nxt = interval_tas.next();
720        assert!(nxt.is_none(), "Got additional ta {}", nxt.unwrap());
721
722        ata
723    }
724
725    /// constructs the error states for these test cases
726    fn _get_error_states_for_spurious_checking(cs: &ZCS) -> ZCSStates {
727        cs.get_sym_state_for_loc(&Location::new("l2"))
728    }
729}
taco_zcs_model_checker/paths.rs

taco_zcs_model_checker/
paths.rs
