taco_zcs_model_checker/
zcs.rs

1//! This module contains the symbolic representation
2//! of a 01-CS (ZCS) for a given IntervalThresholdAutomaton.
3
4pub mod builder;
5
6use bdd_var_manager::BddVarManager;
7use taco_bdd::BDD;
8use taco_bdd::Bdd;
9use taco_interval_ta::IntervalTARule;
10use taco_interval_ta::IntervalThresholdAutomaton;
11use taco_interval_ta::interval::Interval;
12use taco_threshold_automaton::ThresholdAutomaton;
13use taco_threshold_automaton::expressions::{Location, Variable};
14
15use crate::paths::VariableAssignment;
16
17mod bdd_var_manager;
18
19/// Type representing a symbolic 01-CS (ZCS)
20#[derive(Debug, Clone)]
21pub struct ZCS<'a> {
22    /// bdd manager to perform all bdd operations
23    bdd_mgr: BddVarManager,
24    /// underlying abstract threshold automaton
25    ata: &'a IntervalThresholdAutomaton,
26    /// initial states of the 01-CS (ZCS)
27    initial_states: ZCSStates,
28    /// set of transitions of the 01-CS (ZCS)
29    transitions: Vec<SymbolicTransition>,
30    /// transition relation of the 01-CS (ZCS) as a single bdd
31    transition_relation: BDD,
32}
33impl ZCS<'_> {
34    /// Computes the set of successors for a symbolic state `from`
35    /// rule_ids for `with` are not abstracted
36    pub fn compute_successor(&self, from: ZCSStates, with: SymbolicTransition) -> ZCSStates {
37        // intersect transition `with` with symbolic state `from`
38        let mut succ = from.set_of_states.and(&with.transition_bdd);
39        // abstract unprimed variables
40        succ = self.bdd_mgr.exists_unprimed(&succ);
41        // unprime all bdd variables in `succ`
42        succ = self.bdd_mgr.swap_unprimed_primed_bdd_vars(&succ);
43
44        ZCSStates {
45            set_of_states: succ,
46        }
47    }
48
49    /// Computes the set of predecessors for a symbolic state `to`
50    /// Bdd variables for rule_ids are not abstracted
51    pub fn compute_predecessor(&self, to: ZCSStates) -> ZCSStates {
52        // prime all bdd variables in `to`
53        let primed_to = self
54            .bdd_mgr
55            .swap_unprimed_primed_bdd_vars(&to.set_of_states);
56        // intersect with transition relation
57        let mut pred = primed_to.and(&self.transition_relation);
58        // abstract primed variables
59        pred = self.bdd_mgr.exists_primed(&pred);
60        ZCSStates {
61            set_of_states: pred,
62        }
63    }
64
65    /// returns a new empty set of states
66    pub fn new_empty_sym_state(&self) -> ZCSStates {
67        ZCSStates {
68            set_of_states: self.bdd_mgr.get_bdd_false(),
69        }
70    }
71
72    /// returns a new "full" set of states
73    pub fn new_full_sym_state(&self) -> ZCSStates {
74        ZCSStates {
75            set_of_states: self.bdd_mgr.get_bdd_true(),
76        }
77    }
78
79    /// returns the set of states where a given location is occupied
80    pub fn get_sym_state_for_loc(&self, loc: &Location) -> ZCSStates {
81        ZCSStates {
82            set_of_states: self
83                .bdd_mgr
84                .get_location_var(loc)
85                .expect("failed to get location bdd")
86                .clone(),
87        }
88    }
89
90    /// returns the set of states where a given shared variable is in the given 'interval'
91    pub fn get_sym_state_for_shared_interval(
92        &self,
93        shared: &Variable,
94        interval: &Interval,
95    ) -> ZCSStates {
96        ZCSStates {
97            set_of_states: self
98                .bdd_mgr
99                .get_shared_interval_bdd(shared, interval)
100                .expect("failed to get shared interval bdd")
101                .clone(),
102        }
103    }
104
105    /// returns the set of states where the rule_id of a given 'rule' is applied
106    pub fn get_sym_state_for_rule(&self, rule: &IntervalTARule) -> ZCSStates {
107        ZCSStates {
108            set_of_states: self
109                .bdd_mgr
110                .get_rule_bdd(rule)
111                .expect("failed to get rule bdd")
112                .clone(),
113        }
114    }
115
116    /// returns the symbolic states that abstracts rule_ids from 'states'
117    pub fn abstract_rule_vars(&self, states: ZCSStates) -> ZCSStates {
118        ZCSStates {
119            set_of_states: self.bdd_mgr.exists_rule_vars(&states.set_of_states),
120        }
121    }
122
123    /// set of initial states of the 01-CS (ZCS)
124    pub fn initial_states(&self) -> ZCSStates {
125        self.initial_states.clone()
126    }
127
128    /// returns an iterator over the encoded transition rules
129    pub fn transitions(&self) -> impl Iterator<Item = &SymbolicTransition> {
130        self.transitions.iter()
131    }
132
133    /// returns an iterator over the locations of the underlying threshold automaton
134    pub fn locations(&self) -> impl Iterator<Item = &Location> {
135        self.ata.locations()
136    }
137
138    /// returns an iterator over the shared variables of the underlying threshold automaton
139    pub fn variables(&self) -> impl Iterator<Item = &Variable> {
140        self.ata.variables()
141    }
142
143    /// returns an iterator over the ordered intervals for a given shared variable
144    pub fn get_ordered_intervals_for_shared(&self, shared: &Variable) -> &Vec<Interval> {
145        self.ata
146            .get_ordered_intervals(shared)
147            .expect("failed to get ordered intervals for shared variable")
148    }
149
150    /// returns the symbolic variable assignment for a given variable assignment
151    pub fn get_sym_var_assignment(&self, assign: VariableAssignment) -> SymbolicVariableAssignment {
152        let mut assign_bdd = self.bdd_mgr.get_bdd_true();
153        for (shared, interval) in assign.assignments() {
154            let interval_bdd = self
155                .bdd_mgr
156                .get_shared_interval_bdd(shared, interval)
157                .expect("failed to get shared interval bdd");
158            assign_bdd = assign_bdd.and(interval_bdd);
159        }
160        SymbolicVariableAssignment::new(assign_bdd, assign)
161    }
162
163    /// returns if the underlying threshold automaton contains any decrementing rules
164    pub fn has_decrements(&self) -> bool {
165        self.ata.has_decrements()
166    }
167}
168
169/// Type to represent a set of states in the 01-CS (ZCS)
170#[derive(Debug, Clone, PartialEq)]
171pub struct ZCSStates {
172    /// bdd to represent a set of states
173    set_of_states: BDD,
174}
175impl ZCSStates {
176    /// creates a new 'ZCSStates'
177    pub fn new(node: BDD) -> Self {
178        ZCSStates {
179            set_of_states: node,
180        }
181    }
182    /// returns the underlying set_of_states
183    pub fn set_of_states(&self) -> &BDD {
184        &self.set_of_states
185    }
186
187    /// performs the `intersection` operation
188    pub fn intersection(&self, states: &ZCSStates) -> ZCSStates {
189        ZCSStates {
190            set_of_states: self.set_of_states.and(&states.set_of_states),
191        }
192    }
193
194    /// checks if the symbolic state contains a given symbolic variable assignment
195    pub fn contains_sym_assignment(&self, sym_assignment: &SymbolicVariableAssignment) -> bool {
196        self.set_of_states
197            .and(&sym_assignment.assignment_bdd)
198            .satisfiable()
199    }
200
201    /// performs the intersection of a symbolic_states and a symbolic variable assignment
202    pub fn intersect_assignment(&self, sym_assignment: &SymbolicVariableAssignment) -> ZCSStates {
203        ZCSStates {
204            set_of_states: self.set_of_states.and(&sym_assignment.assignment_bdd),
205        }
206    }
207
208    /// performs the restriction of a symbolic_states and a symbolic variable assignment
209    ///
210    /// i.e., removes all states that satisfy the variable assignment
211    pub fn remove_assignment(&self, sym_assignment: &SymbolicVariableAssignment) -> ZCSStates {
212        ZCSStates {
213            set_of_states: self
214                .set_of_states
215                .and(&!sym_assignment.assignment_bdd.clone()),
216        }
217    }
218
219    /// performs the `union` operation
220    pub fn union(&self, states: &ZCSStates) -> ZCSStates {
221        ZCSStates {
222            set_of_states: self.set_of_states.or(&states.set_of_states),
223        }
224    }
225
226    /// returns the complement
227    pub fn complement(&self) -> ZCSStates {
228        ZCSStates {
229            set_of_states: self.set_of_states.not(),
230        }
231    }
232    /// checks if the set of states is empty
233    pub fn is_empty(&self) -> bool {
234        !self.set_of_states.satisfiable()
235    }
236
237    /// checks if two SymbolicStates are equal
238    pub fn equal(&self, other: &ZCSStates) -> bool {
239        self.set_of_states.eq(&other.set_of_states)
240    }
241}
242
243/// Type to represent a symbolic transition in the 01-CS (ZCS)
244#[derive(Debug, Clone, PartialEq)]
245pub struct SymbolicTransition {
246    /// underlying rule of the TA
247    abstract_rule: IntervalTARule,
248    /// bdd to represent all possible transitions of the 01-CS (ZCS)
249    /// based on the underlying rule of the TA
250    transition_bdd: BDD,
251}
252impl SymbolicTransition {
253    /// Creates a new `SymbolicTransition`.
254    pub fn new(node: BDD, transition: IntervalTARule) -> Self {
255        SymbolicTransition {
256            abstract_rule: transition,
257            transition_bdd: node,
258        }
259    }
260    /// return the underlying abstract rule
261    pub fn abstract_rule(&self) -> &IntervalTARule {
262        &self.abstract_rule
263    }
264}
265
266/// Type that represents a symbolic variable assignment
267#[derive(Debug, Clone)]
268pub struct SymbolicVariableAssignment {
269    /// bdd representation of the variable assignment
270    assignment_bdd: BDD,
271    /// concrete variable assignment
272    assignment: VariableAssignment,
273}
274impl SymbolicVariableAssignment {
275    /// creates a new 'SymbolicVariableAssignment'
276    pub fn new(assignment_bdd: BDD, assignment: VariableAssignment) -> Self {
277        SymbolicVariableAssignment {
278            assignment_bdd,
279            assignment,
280        }
281    }
282
283    /// returns the bdd representation of the variable assignment
284    pub fn assignment_bdd(&self) -> &BDD {
285        &self.assignment_bdd
286    }
287
288    /// returns the concrete variable assignment
289    pub fn assignment(&self) -> &VariableAssignment {
290        &self.assignment
291    }
292}
293
294#[cfg(test)]
295mod tests {
296    use super::*;
297    use builder::ZCSBuilder;
298    use taco_bdd::Bdd;
299    use taco_interval_ta::builder::IntervalTABuilder;
300    use taco_interval_ta::interval::Interval;
301    use taco_interval_ta::interval::IntervalBoundary;
302    use taco_smt_encoder::SMTSolverBuilder;
303    use taco_threshold_automaton::expressions::Location;
304    use taco_threshold_automaton::expressions::Variable;
305    use taco_threshold_automaton::expressions::fraction::Fraction;
306    use taco_threshold_automaton::lia_threshold_automaton::integer_thresholds::Threshold;
307    use taco_threshold_automaton::lia_threshold_automaton::integer_thresholds::WeightedSum;
308    use taco_threshold_automaton::{
309        BooleanVarConstraint, LocationConstraint, ParameterConstraint, RuleDefinition,
310    };
311    use taco_threshold_automaton::{
312        expressions::{ComparisonOp, IntegerExpression, Parameter},
313        general_threshold_automaton::{Action, builder::RuleBuilder},
314    };
315
316    /// Constructs the 01-CS for the abstract threshold automaton in `symbolic-01-cs/src/builder` constructed in `test_automaton()`
317    fn get_ata() -> IntervalThresholdAutomaton {
318        let ta_builder =
319            taco_threshold_automaton::general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder::new("test")
320                .with_locations(vec![
321                    Location::new("v0"),
322                    Location::new("v1"),
323                    Location::new("wait"),
324                    Location::new("d0"),
325                    Location::new("d1"),
326                ])
327                .unwrap()
328                .with_variables(vec![Variable::new("x0"), Variable::new("x1")])
329                .unwrap()
330                .with_parameters(vec![
331                    Parameter::new("n"),
332                    Parameter::new("t"),
333                    Parameter::new("f"),
334                ])
335                .unwrap()
336                .initialize()
337                .with_initial_location_constraints(vec![
338                    LocationConstraint::ComparisonExpression(
339                        Box::new(
340                            IntegerExpression::Atom(Location::new("v0"))
341                                + IntegerExpression::Atom(Location::new("v1")),
342                        ),
343                        ComparisonOp::Eq,
344                        Box::new(
345                            IntegerExpression::Param(Parameter::new("n"))
346                                - IntegerExpression::Param(Parameter::new("t")),
347                        ),
348                    ),
349                    LocationConstraint::ComparisonExpression(
350                        Box::new(IntegerExpression::Atom(Location::new("wait"))),
351                        ComparisonOp::Eq,
352                        Box::new(IntegerExpression::Const(0)),
353                    ),
354                    LocationConstraint::ComparisonExpression(
355                        Box::new(IntegerExpression::Atom(Location::new("d0"))),
356                        ComparisonOp::Eq,
357                        Box::new(IntegerExpression::Const(0)),
358                    ),
359                    LocationConstraint::ComparisonExpression(
360                        Box::new(IntegerExpression::Atom(Location::new("d1"))),
361                        ComparisonOp::Eq,
362                        Box::new(IntegerExpression::Const(0)),
363                    ),
364                ])
365                .unwrap()
366                .with_initial_variable_constraints([
367                    BooleanVarConstraint::ComparisonExpression(
368                        Box::new(IntegerExpression::Atom(Variable::new("x0"))),
369                        ComparisonOp::Eq,
370                        Box::new(IntegerExpression::Const(0)),
371                    ),
372                    BooleanVarConstraint::ComparisonExpression(
373                        Box::new(IntegerExpression::Atom(Variable::new("x1"))),
374                        ComparisonOp::Eq,
375                        Box::new(IntegerExpression::Const(0)),
376                    ),
377                ]
378                ).unwrap()
379                .with_resilience_conditions(vec![
380                    ParameterConstraint::ComparisonExpression(
381                        Box::new(IntegerExpression::Atom(Parameter::new("n"))),
382                        ComparisonOp::Gt,
383                        Box::new(
384                            IntegerExpression::Const(3)
385                                * IntegerExpression::Atom(Parameter::new("t")),
386                        ),
387                    ),
388                    ParameterConstraint::ComparisonExpression(
389                        Box::new(IntegerExpression::Atom(Parameter::new("t"))),
390                        ComparisonOp::Geq,
391                        Box::new(IntegerExpression::Atom(Parameter::new("f"))),
392                    ),
393                    ParameterConstraint::ComparisonExpression(
394                        Box::new(IntegerExpression::Atom(Parameter::new("n")) - IntegerExpression::Atom(Parameter::new("t"))),
395                        ComparisonOp::Gt,
396                        Box::new(IntegerExpression::Const(1)),
397                    ),
398                ])
399                .unwrap()
400                .with_rules(vec![
401                    RuleBuilder::new(0, Location::new("v0"), Location::new("wait"))
402                        .with_action(
403                            Action::new(
404                                Variable::new("x0"),
405                                IntegerExpression::Atom(Variable::new("x0"))
406                                    + IntegerExpression::Const(1),
407                            )
408                            .unwrap(),
409                        )
410                        .build(),
411                    RuleBuilder::new(1, Location::new("v1"), Location::new("wait"))
412                        .with_action(
413                            Action::new(
414                                Variable::new("x1"),
415                                IntegerExpression::Atom(Variable::new("x1"))
416                                    + IntegerExpression::Const(1),
417                            )
418                            .unwrap(),
419                        )
420                        .build(),
421                    RuleBuilder::new(2, Location::new("wait"), Location::new("d0"))
422                        .with_guard(BooleanVarConstraint::ComparisonExpression(
423                            Box::new(IntegerExpression::Atom(Variable::new("x0"))),
424                            ComparisonOp::Geq,
425                            Box::new(
426                                IntegerExpression::Param(Parameter::new("n"))
427                                    - IntegerExpression::Param(Parameter::new("t")),
428                            ),
429                        ))
430                        .build(),
431                    RuleBuilder::new(3, Location::new("wait"), Location::new("d1"))
432                        .with_guard(BooleanVarConstraint::ComparisonExpression(
433                            Box::new(IntegerExpression::Atom(Variable::new("x1"))),
434                            ComparisonOp::Geq,
435                            Box::new(
436                                IntegerExpression::Param(Parameter::new("n"))
437                                    - IntegerExpression::Param(Parameter::new("t")),
438                            ),
439                        ))
440                        .build(),
441                ])
442                .unwrap();
443        let ta = ta_builder.build();
444        let lia =
445            taco_threshold_automaton::lia_threshold_automaton::LIAThresholdAutomaton::try_from(
446                ta.clone(),
447            )
448            .unwrap();
449
450        let mut interval_tas = IntervalTABuilder::new(lia, SMTSolverBuilder::default(), vec![])
451            .build()
452            .unwrap();
453        interval_tas.next().unwrap()
454    }
455
456    #[test]
457    fn test_compute_successor_update() {
458        let ata = get_ata();
459        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
460        let cs = builder.build();
461
462        // initial_states: ((-,-,0,0,0),(I_0,I_0))
463        let mut t_0: Option<&SymbolicTransition> = None;
464        for t in &cs.transitions {
465            if t.abstract_rule().id() == 0 {
466                t_0 = Some(t);
467            }
468        }
469        assert!(t_0.is_some());
470        let succ = cs.compute_successor(cs.initial_states.clone(), t_0.unwrap().clone());
471
472        let wait = cs.bdd_mgr.get_location_var(&Location::new("wait")).unwrap();
473        let d0 = cs.bdd_mgr.get_location_var(&Location::new("d0")).unwrap();
474        let d1 = cs.bdd_mgr.get_location_var(&Location::new("d1")).unwrap();
475
476        // succ = initial_states -> rule_0 = ((-,-,1,0,0),({I_0,I_1}, I_0)) & r_0_ids
477        let mut correct_succ = wait.and(&d0.not()).and(&d1.not());
478        // I_0 = [0,1)
479        let interval_0 = Interval::zero();
480        // I_1 = [1,n-t)
481        let interval_1 = Interval::new(
482            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
483            false,
484            IntervalBoundary::Bound(Threshold::new(
485                [
486                    (Parameter::new("n"), 1.into()),
487                    (Parameter::new("t"), Fraction::new(1, 1, true)),
488                ],
489                0,
490            )),
491            true,
492        );
493        correct_succ = correct_succ.and(
494            cs.bdd_mgr
495                .get_shared_interval_bdd(&Variable::new("x0"), &interval_1)
496                .unwrap(),
497        );
498        correct_succ = correct_succ.and(
499            cs.bdd_mgr
500                .get_shared_interval_bdd(&Variable::new("x1"), &interval_0)
501                .unwrap(),
502        );
503
504        correct_succ = correct_succ.and(
505            cs.bdd_mgr
506                .get_rule_bdd(t_0.unwrap().abstract_rule())
507                .unwrap(),
508        );
509        assert!(correct_succ.eq(&succ.set_of_states));
510    }
511
512    #[test]
513    fn test_compute_successor_guard() {
514        let ata = get_ata();
515        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
516        let cs = builder.build();
517
518        // from = ((-,-,-,0,-),(I_2,-))
519        let mut from = cs
520            .bdd_mgr
521            .get_location_var(&Location::new("d0"))
522            .unwrap()
523            .not();
524        // I_2 = [n-t,infty)
525        let interval_2 = Interval::new(
526            IntervalBoundary::Bound(Threshold::new(
527                [
528                    (Parameter::new("n"), 1.into()),
529                    (Parameter::new("t"), Fraction::new(1, 1, true)),
530                ],
531                0,
532            )),
533            false,
534            IntervalBoundary::new_infty(),
535            true,
536        );
537        from = from.and(
538            cs.bdd_mgr
539                .get_shared_interval_bdd(&Variable::new("x0"), &interval_2)
540                .unwrap(),
541        );
542
543        let mut t_3: Option<&SymbolicTransition> = None;
544        for t in &cs.transitions {
545            if t.abstract_rule().id() == 3 {
546                t_3 = Some(t);
547            }
548        }
549        assert!(t_3.is_some());
550
551        // succ = from -> rule_3 = ((-,-,-,0,1),(I_2, I_2)) & r_3_ids
552        let succ = cs.compute_successor(
553            ZCSStates {
554                set_of_states: from,
555            },
556            t_3.unwrap().clone(),
557        );
558
559        let mut correct_succ = cs
560            .bdd_mgr
561            .get_location_var(&Location::new("d0"))
562            .unwrap()
563            .not();
564        correct_succ = correct_succ.and(cs.bdd_mgr.get_location_var(&Location::new("d1")).unwrap());
565
566        correct_succ = correct_succ.and(
567            cs.bdd_mgr
568                .get_shared_interval_bdd(&Variable::new("x0"), &interval_2)
569                .unwrap(),
570        );
571        correct_succ = correct_succ.and(
572            cs.bdd_mgr
573                .get_shared_interval_bdd(&Variable::new("x1"), &interval_2)
574                .unwrap(),
575        );
576
577        correct_succ = correct_succ.and(
578            cs.bdd_mgr
579                .get_rule_bdd(t_3.unwrap().abstract_rule())
580                .unwrap(),
581        );
582
583        assert!(correct_succ.eq(&succ.set_of_states));
584    }
585
586    #[test]
587    fn test_compute_predecessor_update() {
588        let ata = get_ata();
589        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
590        let cs = builder.build();
591
592        // to = ((0,0,1,-,0),(I_1,I_2)
593        let v0 = cs.bdd_mgr.get_location_var(&Location::new("v0")).unwrap();
594        let v1 = cs.bdd_mgr.get_location_var(&Location::new("v1")).unwrap();
595        let wait = cs.bdd_mgr.get_location_var(&Location::new("wait")).unwrap();
596        let d1 = cs.bdd_mgr.get_location_var(&Location::new("d1")).unwrap();
597        let mut to = v0.not().and(&v1.not()).and(wait).and(&d1.not());
598        // I_0 = [0,1)
599        let interval_0 = Interval::zero();
600        // I_1 = [1,n-t)
601        let interval_1 = Interval::new(
602            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
603            false,
604            IntervalBoundary::Bound(Threshold::new(
605                [
606                    (Parameter::new("n"), 1.into()),
607                    (Parameter::new("t"), Fraction::new(1, 1, true)),
608                ],
609                0,
610            )),
611            true,
612        );
613        // I_2 = [n-t,infty)
614        let interval_2 = Interval::new(
615            IntervalBoundary::Bound(Threshold::new(
616                [
617                    (Parameter::new("n"), 1.into()),
618                    (Parameter::new("t"), Fraction::new(1, 1, true)),
619                ],
620                0,
621            )),
622            false,
623            IntervalBoundary::new_infty(),
624            true,
625        );
626        to = to.and(
627            cs.bdd_mgr
628                .get_shared_interval_bdd(&Variable::new("x0"), &interval_1)
629                .unwrap(),
630        );
631        to = to.and(
632            cs.bdd_mgr
633                .get_shared_interval_bdd(&Variable::new("x1"), &interval_2)
634                .unwrap(),
635        );
636
637        let from = cs.compute_predecessor(ZCSStates {
638            set_of_states: to.clone(),
639        });
640
641        let mut t_0: Option<&SymbolicTransition> = None;
642        let mut t_1: Option<&SymbolicTransition> = None;
643        for t in &cs.transitions {
644            if t.abstract_rule().id() == 0 {
645                t_0 = Some(t);
646            }
647            if t.abstract_rule().id() == 1 {
648                t_1 = Some(t);
649            }
650        }
651        assert!(t_0.is_some());
652        assert!(t_1.is_some());
653
654        // from = ((1,0,-,-,0),({I_0,I_1},I_2)) & rule_0_ids (or no valid interval for x0)
655        //      | ((0,1,-,-,0),(I_1,{I_1,I_2})) & rule_1_ids (or no valid interval for x1)
656
657        let mut correct_from_0 = v0.and(&v1.not()).and(&d1.not());
658        let x_0_interval_0 = cs
659            .bdd_mgr
660            .get_shared_interval_bdd(&Variable::new("x0"), &interval_0)
661            .unwrap();
662        let x_0_interval_1 = cs
663            .bdd_mgr
664            .get_shared_interval_bdd(&Variable::new("x0"), &interval_1)
665            .unwrap();
666        let x_0_interval_2 = cs
667            .bdd_mgr
668            .get_shared_interval_bdd(&Variable::new("x0"), &interval_2)
669            .unwrap();
670        let invalid_interval_x_0 = x_0_interval_0
671            .not()
672            .and(&x_0_interval_1.not())
673            .and(&x_0_interval_2.not());
674        correct_from_0 =
675            correct_from_0.and(&(invalid_interval_x_0.or(x_0_interval_0).or(x_0_interval_1)));
676        correct_from_0 = correct_from_0.and(
677            cs.bdd_mgr
678                .get_shared_interval_bdd(&Variable::new("x1"), &interval_2)
679                .unwrap(),
680        );
681        correct_from_0 = correct_from_0.and(
682            cs.bdd_mgr
683                .get_rule_bdd(t_0.unwrap().abstract_rule())
684                .unwrap(),
685        );
686
687        let mut correct_from_1 = v1.and(&v0.not()).and(&d1.not());
688        let x_1_interval_0 = cs
689            .bdd_mgr
690            .get_shared_interval_bdd(&Variable::new("x1"), &interval_0)
691            .unwrap();
692        let x_1_interval_1 = cs
693            .bdd_mgr
694            .get_shared_interval_bdd(&Variable::new("x1"), &interval_1)
695            .unwrap();
696        let x_1_interval_2 = cs
697            .bdd_mgr
698            .get_shared_interval_bdd(&Variable::new("x1"), &interval_2)
699            .unwrap();
700        let invalid_interval_x_1 = x_1_interval_0
701            .not()
702            .and(&x_1_interval_1.not())
703            .and(&x_1_interval_2.not());
704        correct_from_1 =
705            correct_from_1.and(&(invalid_interval_x_1.or(x_1_interval_1).or(x_1_interval_2)));
706        correct_from_1 = correct_from_1.and(
707            cs.bdd_mgr
708                .get_shared_interval_bdd(&Variable::new("x0"), &interval_1)
709                .unwrap(),
710        );
711        correct_from_1 = correct_from_1.and(
712            cs.bdd_mgr
713                .get_rule_bdd(t_1.unwrap().abstract_rule())
714                .unwrap(),
715        );
716
717        assert!((correct_from_0.or(&correct_from_1)).eq(&from.set_of_states));
718    }
719
720    #[test]
721    fn test_compute_predecessor_guard() {
722        let ata = get_ata();
723        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
724        let cs = builder.build();
725
726        // to = ((0,-,0,1,1),(-,-)
727        let v0 = cs.bdd_mgr.get_location_var(&Location::new("v0")).unwrap();
728        let wait = cs.bdd_mgr.get_location_var(&Location::new("wait")).unwrap();
729        let d0 = cs.bdd_mgr.get_location_var(&Location::new("d0")).unwrap();
730        let d1 = cs.bdd_mgr.get_location_var(&Location::new("d1")).unwrap();
731        let to = v0.not().and(&wait.not()).and(d0).and(d1);
732        // I_2 = [n-t,infty)
733        let interval_2 = Interval::new(
734            IntervalBoundary::Bound(Threshold::new(
735                [
736                    (Parameter::new("n"), 1.into()),
737                    (Parameter::new("t"), Fraction::new(1, 1, true)),
738                ],
739                0,
740            )),
741            false,
742            IntervalBoundary::new_infty(),
743            true,
744        );
745
746        let from = cs.compute_predecessor(ZCSStates { set_of_states: to });
747
748        let mut t_2: Option<&SymbolicTransition> = None;
749        let mut t_3: Option<&SymbolicTransition> = None;
750        for t in &cs.transitions {
751            if t.abstract_rule().id() == 2 {
752                t_2 = Some(t);
753            }
754            if t.abstract_rule().id() == 3 {
755                t_3 = Some(t);
756            }
757        }
758        assert!(t_2.is_some());
759        assert!(t_3.is_some());
760
761        // from = ((0,-,1,-,1),(I_2,-)) & rule_2_ids
762        //      | ((0,-,1,1,-),(-,I_2)) & rule_3_ids
763        let mut correct_from_2 = v0.not().and(wait).and(d1);
764        correct_from_2 = correct_from_2.and(
765            cs.bdd_mgr
766                .get_shared_interval_bdd(&Variable::new("x0"), &interval_2)
767                .unwrap(),
768        );
769        correct_from_2 = correct_from_2.and(
770            cs.bdd_mgr
771                .get_rule_bdd(&t_2.unwrap().abstract_rule.clone())
772                .unwrap(),
773        );
774
775        let mut correct_from_3 = v0.not().and(wait).and(d0);
776        correct_from_3 = correct_from_3.and(
777            cs.bdd_mgr
778                .get_shared_interval_bdd(&Variable::new("x1"), &interval_2)
779                .unwrap(),
780        );
781        correct_from_3 = correct_from_3.and(
782            cs.bdd_mgr
783                .get_rule_bdd(&t_3.unwrap().abstract_rule.clone())
784                .unwrap(),
785        );
786
787        assert!((correct_from_2.or(&correct_from_3)).eq(&from.set_of_states));
788    }
789
790    #[test]
791    fn test_locations() {
792        let ata = get_ata();
793        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
794        let cs = builder.build();
795
796        let locs: Vec<Location> = cs.locations().cloned().collect();
797        assert_eq!(locs.len(), 5);
798        assert!(locs.contains(&Location::new("v0")));
799        assert!(locs.contains(&Location::new("v1")));
800        assert!(locs.contains(&Location::new("wait")));
801        assert!(locs.contains(&Location::new("d0")));
802        assert!(locs.contains(&Location::new("d1")));
803    }
804
805    #[test]
806    fn test_variables() {
807        let ata = get_ata();
808        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
809        let cs = builder.build();
810
811        let vars: Vec<Variable> = cs.variables().cloned().collect();
812        assert_eq!(vars.len(), 2);
813        assert!(vars.contains(&Variable::new("x0")));
814        assert!(vars.contains(&Variable::new("x1")));
815    }
816
817    #[test]
818    fn test_get_ordered_intervals_for_shared_variable() {
819        let ata = get_ata();
820        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
821        let cs = builder.build();
822
823        let intervals_x0 = cs.get_ordered_intervals_for_shared(&Variable::new("x0"));
824        let intervals_x1 = cs.get_ordered_intervals_for_shared(&Variable::new("x1"));
825
826        assert_eq!(intervals_x0.len(), 3);
827        assert_eq!(intervals_x1.len(), 3);
828
829        // I_0 = [0,1)
830        let interval_0 = Interval::zero();
831        // I_1 = [1,n-t)
832        let interval_1 = Interval::new(
833            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
834            false,
835            IntervalBoundary::Bound(Threshold::new(
836                [
837                    (Parameter::new("n"), 1.into()),
838                    (Parameter::new("t"), Fraction::new(1, 1, true)),
839                ],
840                0,
841            )),
842            true,
843        );
844        // I_2 = [n-t,infty)
845        let interval_2 = Interval::new(
846            IntervalBoundary::Bound(Threshold::new(
847                [
848                    (Parameter::new("n"), 1.into()),
849                    (Parameter::new("t"), Fraction::new(1, 1, true)),
850                ],
851                0,
852            )),
853            false,
854            IntervalBoundary::new_infty(),
855            true,
856        );
857
858        assert_eq!(intervals_x0[0], interval_0);
859        assert_eq!(intervals_x0[1], interval_1);
860        assert_eq!(intervals_x0[2], interval_2);
861
862        assert_eq!(intervals_x1[0], interval_0);
863        assert_eq!(intervals_x1[1], interval_1);
864        assert_eq!(intervals_x1[2], interval_2);
865    }
866
867    #[test]
868    fn test_get_sym_var_assignment() {
869        let ata = get_ata();
870        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
871        let cs = builder.build();
872
873        let mut var_assign = VariableAssignment::new();
874        // x0 in I_1
875        let interval_1 = Interval::new(
876            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
877            false,
878            IntervalBoundary::Bound(Threshold::new(
879                [
880                    (Parameter::new("n"), 1.into()),
881                    (Parameter::new("t"), Fraction::new(1, 1, true)),
882                ],
883                0,
884            )),
885            true,
886        );
887        let _ = var_assign.add_shared_var_interval(Variable::new("x0"), interval_1.clone());
888        // x1 in I_2
889        let interval_2 = Interval::new(
890            IntervalBoundary::Bound(Threshold::new(
891                [
892                    (Parameter::new("n"), 1.into()),
893                    (Parameter::new("t"), Fraction::new(1, 1, true)),
894                ],
895                0,
896            )),
897            false,
898            IntervalBoundary::new_infty(),
899            true,
900        );
901        let _ = var_assign.add_shared_var_interval(Variable::new("x1"), interval_2.clone());
902
903        let sym_var_assign = cs.get_sym_var_assignment(var_assign.clone());
904
905        let correct_bdd = cs
906            .bdd_mgr
907            .get_shared_interval_bdd(&Variable::new("x0"), &interval_1)
908            .unwrap()
909            .and(
910                cs.bdd_mgr
911                    .get_shared_interval_bdd(&Variable::new("x1"), &interval_2)
912                    .unwrap(),
913            );
914
915        assert!(correct_bdd.eq(sym_var_assign.assignment_bdd()));
916        let assign = sym_var_assign.assignment();
917        let assignments: Vec<(&Variable, &Interval)> = assign.assignments().collect();
918        assert_eq!(assignments.len(), 2);
919        assert!(assignments.contains(&(&Variable::new("x0"), &interval_1)));
920        assert!(assignments.contains(&(&Variable::new("x1"), &interval_2)));
921    }
922
923    #[test]
924    fn test_contains_sym_assignment() {
925        let ata = get_ata();
926        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
927        let cs = builder.build();
928
929        let initial_states = cs.initial_states();
930
931        let mut var_assign = VariableAssignment::new();
932        // x0 in I_0
933        let interval_0 = Interval::zero();
934        let _ = var_assign.add_shared_var_interval(Variable::new("x0"), interval_0.clone());
935        // x1 in I_0
936        let _ = var_assign.add_shared_var_interval(Variable::new("x1"), interval_0.clone());
937
938        let sym_var_assign = cs.get_sym_var_assignment(var_assign.clone());
939
940        assert!(initial_states.contains_sym_assignment(&sym_var_assign));
941
942        let mut var_assign2 = VariableAssignment::new();
943        // x0 in I_1
944        let interval_1 = Interval::new(
945            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
946            false,
947            IntervalBoundary::Bound(Threshold::new(
948                [
949                    (Parameter::new("n"), 1.into()),
950                    (Parameter::new("t"), Fraction::new(1, 1, true)),
951                ],
952                0,
953            )),
954            true,
955        );
956        let _ = var_assign2.add_shared_var_interval(Variable::new("x0"), interval_1.clone());
957        // x1 in I_0
958        let _ = var_assign2.add_shared_var_interval(Variable::new("x1"), interval_0.clone());
959
960        let sym_var_assign2 = cs.get_sym_var_assignment(var_assign2.clone());
961
962        assert!(!initial_states.contains_sym_assignment(&sym_var_assign2));
963    }
964
965    #[test]
966    fn test_intersect_assignment() {
967        let ata = get_ata();
968        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
969        let cs = builder.build();
970
971        let initial_states = cs.initial_states();
972
973        let mut var_assign = VariableAssignment::new();
974        // x0 in I_0
975        let interval_0 = Interval::zero();
976        let _ = var_assign.add_shared_var_interval(Variable::new("x0"), interval_0.clone());
977        // x1 in I_0
978        let _ = var_assign.add_shared_var_interval(Variable::new("x1"), interval_0.clone());
979
980        let sym_var_assign = cs.get_sym_var_assignment(var_assign.clone());
981
982        let intersected = initial_states.intersect_assignment(&sym_var_assign);
983        assert!(intersected.equal(&initial_states));
984
985        let mut var_assign2 = VariableAssignment::new();
986        // x0 in I_1
987        let interval_1 = Interval::new(
988            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
989            false,
990            IntervalBoundary::Bound(Threshold::new(
991                [
992                    (Parameter::new("n"), 1.into()),
993                    (Parameter::new("t"), Fraction::new(1, 1, true)),
994                ],
995                0,
996            )),
997            true,
998        );
999        let _ = var_assign2.add_shared_var_interval(Variable::new("x0"), interval_1.clone());
1000        // x1 in I_0
1001        let _ = var_assign2.add_shared_var_interval(Variable::new("x1"), interval_0.clone());
1002
1003        let sym_var_assign2 = cs.get_sym_var_assignment(var_assign2.clone());
1004
1005        let intersected2 = initial_states.intersect_assignment(&sym_var_assign2);
1006        assert!(intersected2.is_empty());
1007
1008        let changed_initial_states = initial_states.union(&ZCSStates {
1009            set_of_states: sym_var_assign2.assignment_bdd().clone(),
1010        });
1011        let intersected3 = changed_initial_states.intersect_assignment(&sym_var_assign2);
1012        assert!(intersected3.equal(&ZCSStates {
1013            set_of_states: sym_var_assign2.assignment_bdd().clone()
1014        }));
1015
1016        let intersected4 = changed_initial_states.intersect_assignment(&sym_var_assign);
1017        assert!(intersected4.equal(&initial_states));
1018    }
1019
1020    #[test]
1021    fn test_remove_assignment() {
1022        let ata = get_ata();
1023        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
1024        let cs = builder.build();
1025
1026        let initial_states = cs.initial_states();
1027
1028        let mut var_assign = VariableAssignment::new();
1029        // x0 in I_0
1030        let interval_0 = Interval::zero();
1031        let _ = var_assign.add_shared_var_interval(Variable::new("x0"), interval_0.clone());
1032        // x1 in I_0
1033        let _ = var_assign.add_shared_var_interval(Variable::new("x1"), interval_0.clone());
1034
1035        let sym_var_assign = cs.get_sym_var_assignment(var_assign.clone());
1036
1037        let removed = initial_states.remove_assignment(&sym_var_assign);
1038        assert!(removed.is_empty());
1039
1040        let mut var_assign2 = VariableAssignment::new();
1041        // x0 in I_1
1042        let interval_1 = Interval::new(
1043            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
1044            false,
1045            IntervalBoundary::Bound(Threshold::new(
1046                [
1047                    (Parameter::new("n"), 1.into()),
1048                    (Parameter::new("t"), Fraction::new(1, 1, true)),
1049                ],
1050                0,
1051            )),
1052            true,
1053        );
1054        let _ = var_assign2.add_shared_var_interval(Variable::new("x0"), interval_1.clone());
1055        // x1 in I_0
1056        let _ = var_assign2.add_shared_var_interval(Variable::new("x1"), interval_0.clone());
1057
1058        let sym_var_assign2 = cs.get_sym_var_assignment(var_assign2.clone());
1059
1060        let removed2 = initial_states.remove_assignment(&sym_var_assign2);
1061        assert!(removed2.equal(&initial_states));
1062
1063        let changed_initial_states = initial_states.union(&ZCSStates {
1064            set_of_states: sym_var_assign2.assignment_bdd().clone(),
1065        });
1066        let removed3 = changed_initial_states.remove_assignment(&sym_var_assign2);
1067        assert!(removed3.equal(&initial_states));
1068
1069        let removed4 = changed_initial_states.remove_assignment(&sym_var_assign);
1070        assert!(removed4.equal(&ZCSStates {
1071            set_of_states: sym_var_assign2.assignment_bdd().clone()
1072        }));
1073    }
1074
1075    #[test]
1076    fn test_symbolic_transition() {
1077        let ata = get_ata();
1078        let builder: ZCSBuilder = ZCSBuilder::new(&taco_bdd::BDDManager::default(), &ata);
1079        let cs = builder.build();
1080
1081        let mut t_0: Option<&SymbolicTransition> = None;
1082        for t in &cs.transitions {
1083            if t.abstract_rule().id() == 0 {
1084                t_0 = Some(t);
1085            }
1086        }
1087        assert!(t_0.is_some());
1088        let t_0 = t_0.unwrap();
1089
1090        let r_0 = t_0.abstract_rule();
1091        let r_0_bdd = t_0.transition_bdd.clone();
1092
1093        let sym_trans = SymbolicTransition::new(r_0_bdd.clone(), r_0.clone());
1094        assert_eq!(sym_trans.abstract_rule, *r_0);
1095        assert!(sym_trans.transition_bdd.eq(&r_0_bdd));
1096    }
1097}
taco_zcs_model_checker/zcs.rs

taco_zcs_model_checker/
zcs.rs
