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

taco_zcs_model_checker/
paths.rs
