taco_zcs_model_checker/zcs/
bdd_var_manager.rs

1//! This module contains the definition of a BDD context manager which
2//! is used to create and manage BDD variables.
3
4use std::collections::HashMap;
5use std::fmt::Display;
6
7use taco_bdd::{BDD, BDDManager, Bdd, BddManager};
8use taco_interval_ta::IntervalThresholdAutomaton;
9use taco_interval_ta::{IntervalTARule, interval::Interval};
10use taco_threshold_automaton::ThresholdAutomaton;
11use taco_threshold_automaton::expressions::{Location, Variable};
12
13/// Manager for BDD variables for an underlying IntervalThresholdAutomaton
14#[derive(Debug, Clone)]
15pub struct BddVarManager {
16    /// The BDD manager
17    manager: BDDManager,
18    /// BDD variables for each location
19    loc_vars: HashMap<Location, BDD>,
20    /// Location successor BDD variables
21    loc_vars_primed: HashMap<Location, BDD>,
22    /// BDD variables for each variable
23    variable_vars: HashMap<Variable, Vec<BDD>>,
24    /// Variable successor BDD variables
25    variable_vars_primed: HashMap<Variable, Vec<BDD>>,
26    /// Mapping for each variable from unprimed interval to the corresponding BDD
27    shared_interval_to_bdd: HashMap<Variable, HashMap<Interval, BDD>>,
28    /// Mapping for each variable from primed interval to the correspond BDD
29    shared_primed_interval_to_bdd: HashMap<Variable, HashMap<Interval, BDD>>,
30    /// BDD variables to represent the rule_id
31    rule_vars: Vec<BDD>,
32    /// Mapping from abstract rule to the corresponding BDD
33    rule_to_bdd: HashMap<IntervalTARule, BDD>,
34    /// All unprimed bdd variables for locations and shared variables
35    unprimed_vars_vec: Vec<BDD>,
36    /// All primed bdd variables for locations and shared variables
37    primed_vars_vec: Vec<BDD>,
38}
39
40impl BddVarManager {
41    /// creates a new BDDVarManager
42    pub fn new(mgr: BDDManager, automaton: &IntervalThresholdAutomaton) -> Self {
43        let mut bdd_mgr = BddVarManager {
44            manager: mgr,
45            loc_vars: HashMap::new(),
46            loc_vars_primed: HashMap::new(),
47            variable_vars: HashMap::new(),
48            variable_vars_primed: HashMap::new(),
49            shared_interval_to_bdd: HashMap::new(),
50            shared_primed_interval_to_bdd: HashMap::new(),
51            rule_vars: Vec::new(),
52            rule_to_bdd: HashMap::new(),
53            unprimed_vars_vec: Vec::new(),
54            primed_vars_vec: Vec::new(),
55        };
56        bdd_mgr.initialize(automaton);
57        bdd_mgr
58    }
59
60    /// initializes the bdd_var_manager
61    ///
62    /// 1. create unprimed and primed location vars
63    /// 2. create unprimed and primed shared variable intervals
64    /// 3. create bdd_variables to represent rules
65    /// 4. create ordered vectors for all unprimed and primed bdd variables
66    fn initialize(&mut self, aut: &IntervalThresholdAutomaton) {
67        // 1. create unprimed and primed location vars
68        self.initialize_loc_vars(aut);
69
70        // 2. create unprimed and primed shared variable intervals
71        self.initialize_shared_vars(aut);
72
73        // 3. create bdd_variables to represent rules
74        self.initialize_rule_vars(aut);
75
76        //4. create ordered vectors for all unprimed and primed bdd variables
77        self.create_unprimed_primed_vecs();
78    }
79
80    /// initializes all unprimed and primed bdd variables for locations
81    fn initialize_loc_vars(&mut self, aut: &IntervalThresholdAutomaton) {
82        let locations = aut.locations();
83        for loc in locations {
84            // create unprimed and primed bdd variables for each location
85            self.new_location_var(loc);
86            self.new_primed_location_var(loc);
87        }
88    }
89
90    /// initializes all unprimed and primed bdd variables for shared variables
91    fn initialize_shared_vars(&mut self, aut: &IntervalThresholdAutomaton) {
92        for shared_var in aut.variables() {
93            // check how many bdd variables are needed to represent all intervals binary
94            // and create as many primed and unprimed bdd variables
95            let num_intervals = aut.get_intervals(shared_var).len();
96            for _ in 0..format!("{:b}", num_intervals - 1).len() {
97                self.new_shared_var(shared_var);
98                self.new_primed_shared_var(shared_var);
99            }
100            // encode each interval as a bdd
101            for (index, interval) in aut.get_intervals(shared_var).iter().enumerate() {
102                let bdd = self.encode_bitwise_bdd(
103                    index as u32,
104                    self.variable_vars
105                        .get(shared_var)
106                        .expect("error getting shared bdd variables"),
107                );
108
109                self.shared_interval_to_bdd
110                    .entry(shared_var.clone())
111                    .or_default()
112                    .insert(interval.clone(), bdd.clone());
113
114                let vars_shared_primed = self
115                    .variable_vars_primed
116                    .get(shared_var)
117                    .expect("error getting shared bdd variables");
118                let bdd = self.encode_bitwise_bdd(index as u32, vars_shared_primed);
119
120                self.shared_primed_interval_to_bdd
121                    .entry(shared_var.clone())
122                    .or_default()
123                    .insert(interval.clone(), bdd.clone());
124            }
125        }
126    }
127
128    // initializes all bdd variables for abstract rules
129    fn initialize_rule_vars(&mut self, aut: &IntervalThresholdAutomaton) {
130        // check how many bdd variables are needed to represent the maximum rule_id binary
131        // and create as many bdd variables
132        let num_rules = aut.rules().count();
133        for _ in 0..num_rules.checked_ilog2().map_or(0, |n| n + 1) {
134            self.new_rule_var();
135        }
136        // encode each rule_id as a bdd
137        for (counter, rule) in aut.rules().enumerate() {
138            let bdd = self.encode_bitwise_bdd(
139                counter.try_into().expect("rule index exceeds u32::MAX"),
140                &self.rule_vars,
141            );
142            self.rule_to_bdd.insert(rule.clone(), bdd.clone());
143        }
144    }
145
146    /// get the BDD variable for a location
147    pub fn get_location_var(&self, loc: &Location) -> Result<&BDD, BDDVarManagerError> {
148        self.loc_vars
149            .get(loc)
150            .ok_or_else(|| BDDVarManagerError::LocationVarsNotDeclared(loc.clone()))
151    }
152
153    /// get the primed BDD variable for a location
154    pub fn get_primed_location_var(&self, loc: &Location) -> Result<&BDD, BDDVarManagerError> {
155        self.loc_vars_primed
156            .get(loc)
157            .ok_or_else(|| BDDVarManagerError::NoPrimedLocationVar(loc.clone()))
158    }
159
160    /// get the BDD variables for a shared variable
161    pub fn get_shared_interval_bdd(
162        &self,
163        shared: &Variable,
164        interval: &Interval,
165    ) -> Result<&BDD, BDDVarManagerError> {
166        self.shared_interval_to_bdd
167            .get(shared)
168            .ok_or_else(|| {
169                BDDVarManagerError::NoSharedIntervalBdd(shared.clone(), Box::new(interval.clone()))
170            })?
171            .get(interval)
172            .ok_or_else(|| {
173                BDDVarManagerError::NoSharedIntervalBdd(shared.clone(), Box::new(interval.clone()))
174            })
175    }
176
177    /// get the primed BDD variables for a shared variable
178    pub fn get_primed_shared_interval_bdd(
179        &self,
180        shared: &Variable,
181        interval: &Interval,
182    ) -> Result<&BDD, BDDVarManagerError> {
183        self.shared_primed_interval_to_bdd
184            .get(shared)
185            .ok_or_else(|| {
186                BDDVarManagerError::NoPrimedSharedIntervalBdd(
187                    shared.clone(),
188                    Box::new(interval.clone()),
189                )
190            })?
191            .get(interval)
192            .ok_or_else(|| {
193                BDDVarManagerError::NoPrimedSharedIntervalBdd(
194                    shared.clone(),
195                    Box::new(interval.clone()),
196                )
197            })
198    }
199
200    /// get the BDD for an abstract rule
201    pub fn get_rule_bdd(&self, rule: &IntervalTARule) -> Result<&BDD, BDDVarManagerError> {
202        self.rule_to_bdd
203            .get(rule)
204            .ok_or_else(|| BDDVarManagerError::NoAbstractRuleBdd(Box::new(rule.clone())))
205    }
206
207    /// get the constant true BDD
208    pub fn get_bdd_true(&self) -> BDD {
209        self.manager.get_bdd_true()
210    }
211
212    /// get the constant false BDD
213    pub fn get_bdd_false(&self) -> BDD {
214        self.manager.get_bdd_false()
215    }
216
217    /// creates and stores a new bdd variable to represent a given location
218    fn new_location_var(&mut self, loc: &Location) {
219        let loc_var = self.manager.new_var();
220        self.loc_vars.insert(loc.clone(), loc_var.clone());
221    }
222
223    /// creates and stores a new primed bdd variable to represent a given location
224    fn new_primed_location_var(&mut self, loc: &Location) {
225        let primed_loc_var = self.manager.new_var();
226        self.loc_vars_primed
227            .insert(loc.clone(), primed_loc_var.clone());
228    }
229
230    /// creates and stores a new bdd variable to represent the interval of a shared variable
231    fn new_shared_var(&mut self, shared: &Variable) {
232        let shared_var = self.manager.new_var();
233        self.variable_vars
234            .entry(shared.clone())
235            .or_default()
236            .push(shared_var.clone());
237    }
238
239    /// creates and stores a new primed bdd variable to represent the interval of a shared variable
240    fn new_primed_shared_var(&mut self, shared: &Variable) {
241        let primed_shared_var = self.manager.new_var();
242        self.variable_vars_primed
243            .entry(shared.clone())
244            .or_default()
245            .push(primed_shared_var.clone());
246    }
247
248    /// creates and stores a new bdd variable to represent a rule
249    fn new_rule_var(&mut self) {
250        let rule_var = self.manager.new_var();
251        self.rule_vars.push(rule_var.clone());
252    }
253
254    /// Given `index` and a vector of bdd variables,
255    /// Returns the bitwise encoded bdd for `index` if enough bdd variables are provided
256    fn encode_bitwise_bdd(&self, index: u32, bdd_vars: &[BDD]) -> BDD {
257        let mut index_binary = index;
258        let mut bitwise_bdd = self.manager.get_bdd_true();
259        for bdd in bdd_vars.iter().rev() {
260            if index_binary % 2 == 1 {
261                bitwise_bdd = bitwise_bdd.and(bdd);
262            } else {
263                bitwise_bdd = bitwise_bdd.and(&bdd.not());
264            }
265            index_binary >>= 1;
266        }
267        bitwise_bdd
268    }
269
270    /// Constructs a constraint which checks that the bdd variables for an unprimed and primed shared variable are unchanged
271    pub fn get_unchanged_interval_bdd(&self, shared: &Variable) -> Result<BDD, BDDVarManagerError> {
272        let unprimed_vars = self
273            .variable_vars
274            .get(shared)
275            .ok_or_else(|| BDDVarManagerError::NoUnprimedSharedVars(shared.clone()))?;
276
277        let primed_vars = self
278            .variable_vars_primed
279            .get(shared)
280            .ok_or_else(|| BDDVarManagerError::NoPrimedSharedVars(shared.clone()))?;
281
282        Ok(unprimed_vars
283            .iter()
284            .zip(primed_vars.iter())
285            .fold(self.get_bdd_true(), |acc, (unprimed_var, primed_var)| {
286                acc.and(&(unprimed_var.equiv(primed_var)))
287            }))
288    }
289
290    /// Creates an ordered vector for all unprimed and primed bdd variables
291    fn create_unprimed_primed_vecs(&mut self) {
292        // add all unprimed and primed bdd variables for locations
293        for (loc, bdd) in self.loc_vars.iter() {
294            self.unprimed_vars_vec.push(bdd.clone());
295            let primed_bdd = self
296                .loc_vars_primed
297                .get(loc)
298                .ok_or_else(|| BDDVarManagerError::NoPrimedLocationVar(loc.clone()))
299                .expect("error getting primed location bdd");
300            self.primed_vars_vec.push(primed_bdd.clone());
301        }
302
303        //add all unprimed and primed bdd variables for shared variables
304        for (shared, bdd_vec) in self.variable_vars.iter() {
305            self.unprimed_vars_vec.extend(bdd_vec.clone());
306
307            let primed_bdd_vec = self
308                .variable_vars_primed
309                .get(shared)
310                .ok_or_else(|| BDDVarManagerError::NoPrimedSharedVars(shared.clone()))
311                .expect("error getting primed shared bdd variable");
312
313            self.primed_vars_vec.extend(primed_bdd_vec.clone());
314        }
315    }
316
317    /// Swaps all unprimed and primed bdd variables for `cur`
318    pub fn swap_unprimed_primed_bdd_vars(&self, cur: &BDD) -> BDD {
319        cur.swap(&self.unprimed_vars_vec, &self.primed_vars_vec)
320    }
321
322    /// abstracts all bdd variables for unprimed locations and unprimed shared variables for a given bdd
323    pub fn exists_unprimed(&self, cur: &BDD) -> BDD {
324        // abstract unprimed locations and unprimed shared variables
325        let vec_unprimed_vars = self
326            .loc_vars
327            .values()
328            .chain(self.variable_vars.values().flatten());
329
330        cur.exists(vec_unprimed_vars)
331    }
332
333    /// abstracts all primed bdd variables for primed locations and primed shared variables for a given bdd `cur`
334    pub fn exists_primed(&self, cur: &BDD) -> BDD {
335        // abstract primed locations and primed shared variables
336        let vec_primed_vars = self
337            .loc_vars_primed
338            .values()
339            .chain(self.variable_vars_primed.values().flatten());
340
341        cur.exists(vec_primed_vars)
342    }
343
344    /// abstracts all bdd variables for rule_ids for a given bdd `cur`
345    pub fn exists_rule_vars(&self, cur: &BDD) -> BDD {
346        cur.exists(&self.rule_vars)
347    }
348}
349
350/// Custom Error type to indicate an error
351/// when creating a new bdd variable or trying to access an uninitialized one
352#[derive(Debug, Clone)]
353pub enum BDDVarManagerError {
354    /// Error indicating that there exists no bdd variable for this location
355    LocationVarsNotDeclared(Location),
356    /// Error indicating that there exists no primed bdd variables for this location
357    NoPrimedLocationVar(Location),
358    /// Error indicating that there exists no unprimed bdd variable for this shared variable
359    NoUnprimedSharedVars(Variable),
360    /// Error indicating that there exists no primed bdd variable for this shared variable
361    NoPrimedSharedVars(Variable),
362    /// Error indicating that there exist no bdd for this shared variable and this interval
363    NoSharedIntervalBdd(Variable, Box<Interval>),
364    /// Error indicating that there exist no primed bdd for this shared variable and this interval
365    NoPrimedSharedIntervalBdd(Variable, Box<Interval>),
366    /// Error indicating that there exist no bdd for this abstract rule
367    NoAbstractRuleBdd(Box<IntervalTARule>),
368}
369
370impl std::error::Error for BDDVarManagerError {}
371
372impl Display for BDDVarManagerError {
373    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
374        match self {
375            BDDVarManagerError::LocationVarsNotDeclared(loc) => {
376                write!(f, "There exists no bdd variable for location {loc}")
377            }
378            BDDVarManagerError::NoPrimedLocationVar(loc) => {
379                write!(f, "There exists no primed bdd variable for location {loc}")
380            }
381            BDDVarManagerError::NoUnprimedSharedVars(shared) => write!(
382                f,
383                "There exists no unprimed bdd variables for shared variable {shared}"
384            ),
385            BDDVarManagerError::NoPrimedSharedVars(shared) => write!(
386                f,
387                "There exists no primed bdd variables for shared variable {shared}"
388            ),
389            BDDVarManagerError::NoSharedIntervalBdd(shared, interval) => write!(
390                f,
391                "There exists no bdd for shared variable {shared} and interval {interval}"
392            ),
393            BDDVarManagerError::NoPrimedSharedIntervalBdd(shared, interval) => write!(
394                f,
395                "There exists no primed bdd for shared variable {shared} and interval {interval}"
396            ),
397            BDDVarManagerError::NoAbstractRuleBdd(rule) => {
398                write!(f, "There exists no bdd for abstract rule {rule}")
399            }
400        }
401    }
402}
403
404#[cfg(test)]
405mod tests {
406
407    use super::BddVarManager;
408    use crate::zcs::bdd_var_manager::BDDVarManagerError;
409    use taco_bdd::BDD;
410    use taco_bdd::BDDManager;
411    use taco_bdd::Bdd;
412    use taco_interval_ta::interval::{Interval, IntervalBoundary};
413    use taco_interval_ta::{IntervalConstraint, IntervalTARule};
414
415    use taco_threshold_automaton::expressions::{
416        ComparisonOp, IntegerExpression, Location, Parameter, Variable,
417    };
418    use taco_threshold_automaton::general_threshold_automaton::builder::RuleBuilder;
419
420    use taco_interval_ta::IntervalThresholdAutomaton;
421    use taco_interval_ta::builder::IntervalTABuilder;
422    use taco_smt_encoder::SMTSolverBuilder;
423    use taco_threshold_automaton::BooleanVarConstraint;
424    use taco_threshold_automaton::RuleDefinition;
425    use taco_threshold_automaton::ThresholdAutomaton;
426    use taco_threshold_automaton::expressions::fraction::Fraction;
427    use taco_threshold_automaton::general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder;
428    use taco_threshold_automaton::lia_threshold_automaton::LIAThresholdAutomaton;
429    use taco_threshold_automaton::lia_threshold_automaton::integer_thresholds::WeightedSum;
430
431    const LOCATION_L0: &str = "l0";
432    const LOCATION_L1: &str = "l1";
433    const VARIABLE_X: &str = "x";
434    const VARIABLE_Y: &str = "y";
435
436    /// this function is used to instantiate a BddVarManager for the following test cases
437    /// for each location { l0, l1 }, a primed and unprimed bdd variable is created
438    /// for shared variable x, one bdd variable is created (primed and unprimed each)
439    /// for shared variable y, two bdd variables are created (primed and unprimed each)
440    /// for rule_ids, two bdd variables are created
441    /// shared variable x has two intervals I_1 and I_2
442    /// shared variable y has four intervals I_1, I_2, I_3 and I_4
443    /// there are 4 abstract rules
444    fn get_test_aut() -> IntervalThresholdAutomaton {
445        let var_x = Variable::new(VARIABLE_X);
446        let var_y = Variable::new(VARIABLE_Y);
447
448        let ta = GeneralThresholdAutomatonBuilder::new("test_ta")
449            .with_variables(vec![var_x.clone(), var_y.clone()])
450            .unwrap()
451            .with_locations([Location::new(LOCATION_L0), Location::new(LOCATION_L1)])
452            .unwrap()
453            .with_parameter(Parameter::new("n"))
454            .unwrap()
455            .initialize()
456            .with_rules(vec![
457                RuleBuilder::new(0, Location::new(LOCATION_L0), Location::new(LOCATION_L0))
458                    .with_guard(
459                        BooleanVarConstraint::ComparisonExpression(
460                            Box::new(IntegerExpression::Atom(var_x.clone())),
461                            ComparisonOp::Eq,
462                            Box::new(IntegerExpression::Const(0)),
463                        ) & BooleanVarConstraint::ComparisonExpression(
464                            Box::new(IntegerExpression::Atom(var_y.clone())),
465                            ComparisonOp::Eq,
466                            Box::new(IntegerExpression::Const(0)),
467                        ),
468                    )
469                    .build(),
470                RuleBuilder::new(1, Location::new(LOCATION_L0), Location::new(LOCATION_L1))
471                    .with_guard(
472                        BooleanVarConstraint::ComparisonExpression(
473                            Box::new(IntegerExpression::Atom(var_x.clone())),
474                            ComparisonOp::Geq,
475                            Box::new(IntegerExpression::Const(1)),
476                        ) & BooleanVarConstraint::ComparisonExpression(
477                            Box::new(IntegerExpression::Atom(var_y.clone())),
478                            ComparisonOp::Eq,
479                            Box::new(IntegerExpression::Const(1)),
480                        ),
481                    )
482                    .build(),
483                RuleBuilder::new(2, Location::new(LOCATION_L1), Location::new(LOCATION_L0))
484                    .with_guard(BooleanVarConstraint::ComparisonExpression(
485                        Box::new(IntegerExpression::Atom(var_y.clone())),
486                        ComparisonOp::Eq,
487                        Box::new(IntegerExpression::Const(2)),
488                    ))
489                    .build(),
490                RuleBuilder::new(3, Location::new(LOCATION_L1), Location::new(LOCATION_L1))
491                    .with_guard(BooleanVarConstraint::ComparisonExpression(
492                        Box::new(IntegerExpression::Atom(var_y.clone())),
493                        ComparisonOp::Geq,
494                        Box::new(IntegerExpression::Const(3)),
495                    ))
496                    .build(),
497            ])
498            .unwrap()
499            .build();
500
501        let lia_ta = LIAThresholdAutomaton::try_from(ta).unwrap();
502
503        let mut interval_tas = IntervalTABuilder::new(lia_ta, SMTSolverBuilder::default(), vec![])
504            .build()
505            .expect("Failed creating IntervalTA");
506        let ita = interval_tas.next().unwrap();
507
508        assert!(
509            interval_tas.next().is_none(),
510            "There should be only one interval ta in this test"
511        );
512
513        ita
514    }
515
516    /// this function creates the following bdd with bdd variables created in get_test_mgr()
517    /// the bdd is used for test purposes
518    /// taco_bdd: (l_0 & (l_1' | !(x & r_0))) | (!l_0' & (r_1 | y_1'))
519    fn get_test_bdd(mgr: &BddVarManager) -> BDD {
520        let l_0 = mgr.get_location_var(&Location::new("l0")).unwrap();
521        let l_0_prime = mgr.get_primed_location_var(&Location::new("l0")).unwrap();
522        let l_1_prime = mgr.get_primed_location_var(&Location::new("l1")).unwrap();
523
524        // x == I_2
525        let i_x_2 = Interval::new(
526            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
527            false,
528            IntervalBoundary::Infty,
529            true,
530        );
531        let x = mgr
532            .get_shared_interval_bdd(&Variable::new("x"), &i_x_2)
533            .unwrap();
534
535        // y_1' = I_3' | I_4'
536        let interval_3 = Interval::new(
537            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(2, 1, false)),
538            false,
539            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(3, 1, false)),
540            true,
541        );
542        let interval_4 = Interval::new(
543            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(3, 1, false)),
544            false,
545            IntervalBoundary::Infty,
546            true,
547        );
548        let y_1_prime = mgr
549            .get_primed_shared_interval_bdd(&Variable::new("y"), &interval_3)
550            .unwrap()
551            .or(mgr
552                .get_primed_shared_interval_bdd(&Variable::new("y"), &interval_4)
553                .unwrap());
554
555        let ata = get_test_aut();
556        // r_0 = rule_1 | rule_3
557        let rule_1 = ata.rules().find(|r| r.id() == 1).unwrap();
558        let rule_2 = ata.rules().find(|r| r.id() == 2).unwrap();
559        let rule_3 = ata.rules().find(|r| r.id() == 3).unwrap();
560
561        let r_0 = mgr
562            .get_rule_bdd(rule_1)
563            .unwrap()
564            .or(mgr.get_rule_bdd(rule_3).unwrap());
565
566        // r_1 = rule_2 | rule_3
567        let r_1 = mgr
568            .get_rule_bdd(rule_2)
569            .unwrap()
570            .or(mgr.get_rule_bdd(rule_3).unwrap());
571
572        let lhs = l_0.and(&(l_1_prime.or(&((x.and(&r_0)).not()))));
573        let rhs = (l_0_prime.not()).and(&(r_1.or(&y_1_prime)));
574        lhs.or(&rhs)
575    }
576
577    #[test]
578    fn test_get_loc_var() {
579        let ata = get_test_aut();
580        let mgr = BddVarManager::new(BDDManager::default(), &ata);
581
582        assert!(
583            mgr.get_location_var(&Location::new("l0"))
584                .unwrap()
585                .satisfiable()
586        );
587        assert!(
588            !mgr.get_location_var(&Location::new("l0"))
589                .unwrap()
590                .eq(&mgr.get_bdd_true())
591        );
592        assert!(
593            mgr.get_primed_location_var(&Location::new("l0"))
594                .unwrap()
595                .satisfiable()
596        );
597        assert!(
598            !mgr.get_primed_location_var(&Location::new("l0"))
599                .unwrap()
600                .eq(&mgr.get_bdd_true())
601        );
602        assert!(
603            !mgr.get_location_var(&Location::new("l0"))
604                .unwrap()
605                .eq(mgr.get_location_var(&Location::new("l1")).unwrap())
606        );
607        assert!(
608            !mgr.get_location_var(&Location::new("l0"))
609                .unwrap()
610                .eq(mgr.get_primed_location_var(&Location::new("l0")).unwrap())
611        );
612    }
613
614    #[test]
615    fn test_error_get_location_var() {
616        let ata = get_test_aut();
617        let mgr = BddVarManager::new(BDDManager::default(), &ata);
618
619        let error = mgr.get_location_var(&Location::new("l2"));
620
621        assert!(error.is_err());
622
623        assert!(matches!(
624            error.clone().unwrap_err(),
625            BDDVarManagerError::LocationVarsNotDeclared(_)
626        ));
627    }
628
629    #[test]
630    fn test_error_get_primed_location_var() {
631        let ata = get_test_aut();
632        let mgr = BddVarManager::new(BDDManager::default(), &ata);
633
634        let error = mgr.get_primed_location_var(&Location::new("l2"));
635
636        assert!(error.is_err());
637
638        assert!(matches!(
639            error.clone().unwrap_err(),
640            BDDVarManagerError::NoPrimedLocationVar(_)
641        ));
642    }
643
644    #[test]
645    fn test_shared_interval_bdd() {
646        let ata = get_test_aut();
647        let mgr = BddVarManager::new(BDDManager::default(), &ata);
648
649        let i_1 = Interval::new(
650            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(0, 1, false)),
651            false,
652            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
653            true,
654        );
655        let i_x_2 = Interval::new(
656            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
657            false,
658            IntervalBoundary::Infty,
659            true,
660        );
661        let i_y_2 = Interval::new(
662            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
663            false,
664            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(2, 1, false)),
665            true,
666        );
667
668        assert!(
669            !mgr.get_shared_interval_bdd(&Variable::new("x"), &i_1)
670                .unwrap()
671                .eq(&mgr.get_bdd_true())
672        );
673        assert!(
674            !mgr.get_shared_interval_bdd(&Variable::new("x"), &i_1)
675                .unwrap()
676                .eq(&mgr.get_bdd_false())
677        );
678        assert!(
679            !mgr.get_shared_interval_bdd(&Variable::new("x"), &i_x_2)
680                .unwrap()
681                .eq(mgr
682                    .get_primed_shared_interval_bdd(&Variable::new("x"), &i_x_2)
683                    .unwrap())
684        );
685        assert!(
686            !mgr.get_shared_interval_bdd(&Variable::new("y"), &i_y_2)
687                .unwrap()
688                .eq(mgr
689                    .get_shared_interval_bdd(&Variable::new("y"), &i_1)
690                    .unwrap())
691        );
692    }
693
694    #[test]
695    fn test_error_get_shared_interval_bdd_unknown_var() {
696        let ata = get_test_aut();
697        let mgr = BddVarManager::new(BDDManager::default(), &ata);
698
699        let i_1 = Interval::new(
700            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(0, 1, false)),
701            false,
702            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
703            true,
704        );
705
706        let error = mgr.get_shared_interval_bdd(&Variable::new("z"), &i_1);
707
708        assert!(error.is_err());
709
710        assert!(matches!(
711            error.clone().unwrap_err(),
712            BDDVarManagerError::NoSharedIntervalBdd(_, _)
713        ));
714    }
715
716    #[test]
717    fn test_error_get_shared_interval_bdd_unknown_interval() {
718        let ata = get_test_aut();
719        let mgr = BddVarManager::new(BDDManager::default(), &ata);
720
721        let interval_2 = Interval::new(
722            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
723            false,
724            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(2, 1, false)),
725            true,
726        );
727
728        let error = mgr.get_shared_interval_bdd(&Variable::new("x"), &interval_2);
729
730        assert!(error.is_err());
731
732        assert!(matches!(
733            error.clone().unwrap_err(),
734            BDDVarManagerError::NoSharedIntervalBdd(_, _)
735        ));
736    }
737
738    #[test]
739    fn test_error_get_primed_shared_interval_bdd_unknown_var() {
740        let ata = get_test_aut();
741        let mgr = BddVarManager::new(BDDManager::default(), &ata);
742
743        let i_1 = Interval::new(
744            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(0, 1, false)),
745            false,
746            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
747            true,
748        );
749
750        let error = mgr.get_primed_shared_interval_bdd(&Variable::new("z"), &i_1);
751
752        assert!(error.is_err());
753
754        assert!(matches!(
755            error.clone().unwrap_err(),
756            BDDVarManagerError::NoPrimedSharedIntervalBdd(_, _)
757        ));
758    }
759
760    #[test]
761    fn test_error_get_primed_shared_interval_bdd_unknown_interval() {
762        let ata = get_test_aut();
763        let mgr = BddVarManager::new(BDDManager::default(), &ata);
764
765        let i_2 = Interval::new(
766            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
767            false,
768            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(2, 1, false)),
769            true,
770        );
771
772        let error = mgr.get_primed_shared_interval_bdd(&Variable::new("x"), &i_2);
773
774        assert!(error.is_err());
775
776        assert!(matches!(
777            error.clone().unwrap_err(),
778            BDDVarManagerError::NoPrimedSharedIntervalBdd(_, _)
779        ));
780    }
781
782    #[test]
783    fn test_get_rule_bdd() {
784        let ata = get_test_aut();
785        let mgr = BddVarManager::new(BDDManager::default(), &ata);
786        let rule_0 = ata.rules().find(|r| r.id() == 0).unwrap();
787        let rule_1 = ata.rules().find(|r| r.id() == 1).unwrap();
788        let rule_2 = ata.rules().find(|r| r.id() == 2).unwrap();
789        let rule_3 = ata.rules().find(|r| r.id() == 3).unwrap();
790
791        assert!(mgr.get_rule_bdd(rule_0).is_ok());
792        assert!(mgr.get_rule_bdd(rule_1).is_ok());
793        assert!(mgr.get_rule_bdd(rule_2).is_ok());
794        assert!(mgr.get_rule_bdd(rule_3).is_ok());
795        assert!(mgr.get_rule_bdd(rule_0).unwrap().satisfiable());
796        assert!(!mgr.get_rule_bdd(rule_0).unwrap().eq(&mgr.get_bdd_true()));
797        assert!(
798            !mgr.get_rule_bdd(rule_0)
799                .unwrap()
800                .eq(mgr.get_rule_bdd(rule_1).unwrap())
801        );
802    }
803
804    #[test]
805    fn test_error_get_rule_bdd() {
806        let ata = get_test_aut();
807        let mgr = BddVarManager::new(BDDManager::default(), &ata);
808
809        let rule = IntervalTARule::new(
810            0,
811            Location::new("l0"),
812            Location::new("l1"),
813            IntervalConstraint::True,
814            Vec::new(),
815        );
816
817        let error = mgr.get_rule_bdd(&rule);
818
819        assert!(error.is_err());
820
821        assert!(matches!(
822            error.clone().unwrap_err(),
823            BDDVarManagerError::NoAbstractRuleBdd(_)
824        ));
825    }
826
827    #[test]
828    fn test_encode_bitwise_bdd() {
829        let ata = get_test_aut();
830        let mut mgr = BddVarManager::new(BDDManager::default(), &ata);
831
832        mgr.new_shared_var(&Variable::new("z"));
833        mgr.new_shared_var(&Variable::new("z"));
834        let vec_variables = mgr.variable_vars.get(&Variable::new("z")).unwrap();
835        let res = mgr.encode_bitwise_bdd(1, vec_variables);
836        assert!(res.eq(&(vec_variables[0].not().and(&vec_variables[1]))));
837    }
838
839    #[test]
840    fn test_get_unchanged_interval_bdd() {
841        let ata = get_test_aut();
842        let mgr = BddVarManager::new(BDDManager::default(), &ata);
843
844        let unprimed_vars = mgr.variable_vars.get(&Variable::new("y")).unwrap();
845        let primed_vars = mgr.variable_vars_primed.get(&Variable::new("y")).unwrap();
846
847        let correct_bdd = unprimed_vars[0]
848            .clone()
849            .equiv(&primed_vars[0])
850            .and(&primed_vars[1].equiv(&unprimed_vars[1]));
851        let res = mgr.get_unchanged_interval_bdd(&Variable::new("y"));
852        assert!(res.is_ok());
853        assert!(res.unwrap().eq(&correct_bdd));
854    }
855
856    #[test]
857    fn test_error_get_unchanged_interval_bdd_no_unprimed_vars() {
858        let ata = get_test_aut();
859        let mgr = BddVarManager::new(BDDManager::default(), &ata);
860
861        let error = mgr.get_unchanged_interval_bdd(&Variable::new("z"));
862
863        assert!(error.is_err());
864
865        assert!(matches!(
866            error.clone().unwrap_err(),
867            BDDVarManagerError::NoUnprimedSharedVars(_)
868        ));
869    }
870
871    #[test]
872    fn test_error_get_unchanged_interval_bdd_no_primed_vars() {
873        let ata = get_test_aut();
874        let mut mgr = BddVarManager::new(BDDManager::default(), &ata);
875
876        mgr.new_shared_var(&Variable::new("z"));
877        let error = mgr.get_unchanged_interval_bdd(&Variable::new("z"));
878
879        assert!(error.is_err());
880
881        assert!(matches!(
882            error.clone().unwrap_err(),
883            BDDVarManagerError::NoPrimedSharedVars(_)
884        ));
885    }
886
887    #[test]
888    fn test_create_unprimed_primed_vecs() {
889        let ata = get_test_aut();
890        let mgr = BddVarManager::new(BDDManager::default(), &ata);
891
892        assert_eq!(mgr.unprimed_vars_vec.len(), mgr.primed_vars_vec.len());
893    }
894
895    #[test]
896    fn test_swap_unprimed_primed_bdd() {
897        let ata = get_test_aut();
898        let mgr = BddVarManager::new(BDDManager::default(), &ata);
899
900        let l_0 = mgr.get_location_var(&Location::new("l0")).unwrap();
901        let l_0_prime = mgr.get_primed_location_var(&Location::new("l0")).unwrap();
902        // r_0 = rule_1 | rule_3
903        let rule_1 = ata.rules().find(|r| r.id() == 1).unwrap();
904        let rule_3 = ata.rules().find(|r| r.id() == 3).unwrap();
905
906        let r_0 = mgr
907            .get_rule_bdd(rule_1)
908            .unwrap()
909            .or(mgr.get_rule_bdd(rule_3).unwrap());
910
911        let mut res = mgr.swap_unprimed_primed_bdd_vars(&l_0.and(&r_0));
912
913        assert_eq!(res, l_0_prime.and(&r_0));
914
915        res = mgr.swap_unprimed_primed_bdd_vars(&l_0.and(&r_0.and(&l_0_prime.not())));
916        assert_eq!(res, l_0_prime.and(&r_0.and(&l_0.not())));
917
918        let interval_1 = Interval::new(
919            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(0, 1, false)),
920            false,
921            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
922            true,
923        );
924
925        let i_0 = mgr
926            .get_shared_interval_bdd(&Variable::new("x"), &interval_1.clone())
927            .unwrap();
928        let i_0_prime = mgr
929            .get_primed_shared_interval_bdd(&Variable::new("x"), &interval_1.clone())
930            .unwrap();
931
932        res = mgr.swap_unprimed_primed_bdd_vars(&i_0.and(&i_0_prime.not()));
933        assert!(res.eq(&i_0_prime.and(&i_0.not())));
934    }
935
936    #[test]
937    fn test_exists_unprimed() {
938        let ata = get_test_aut();
939        let mgr = BddVarManager::new(BDDManager::default(), &ata);
940        let l_0 = mgr.get_location_var(&Location::new("l0")).unwrap();
941        let l_0_prime = mgr.get_primed_location_var(&Location::new("l0")).unwrap();
942
943        // r_1 = rule_2 | rule_3
944        let rule_2 = ata.rules().find(|r| r.id() == 2).unwrap();
945        let rule_3 = ata.rules().find(|r| r.id() == 3).unwrap();
946
947        let r_1 = mgr
948            .get_rule_bdd(rule_2)
949            .unwrap()
950            .or(mgr.get_rule_bdd(rule_3).unwrap());
951
952        // y_1' = I_2' | I_3'
953        let interval_2 = Interval::new(
954            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(2, 1, false)),
955            false,
956            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(3, 1, false)),
957            true,
958        );
959        let interval_3 = Interval::new(
960            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(3, 1, false)),
961            false,
962            IntervalBoundary::Infty,
963            true,
964        );
965        let y_1_prime = mgr
966            .get_primed_shared_interval_bdd(&Variable::new("y"), &interval_2)
967            .unwrap()
968            .or(mgr
969                .get_primed_shared_interval_bdd(&Variable::new("y"), &interval_3)
970                .unwrap());
971
972        // test_bdd & !l_0
973        let test_bdd = get_test_bdd(&mgr).and(&l_0.not());
974        // (r_1 | y_1') & !l_0
975        let correct_bdd = l_0_prime.not().and(&(r_1.or(&y_1_prime)));
976        let abstract_bdd = mgr.exists_unprimed(&test_bdd);
977        assert!(correct_bdd.eq(&abstract_bdd));
978    }
979
980    #[test]
981    fn test_exists_primed() {
982        let ata = get_test_aut();
983        let mgr = BddVarManager::new(BDDManager::default(), &ata);
984        let l_0 = mgr.get_location_var(&Location::new("l0")).unwrap();
985        let l_0_prime = mgr.get_primed_location_var(&Location::new("l0")).unwrap();
986        let l_1_prime = mgr.get_primed_location_var(&Location::new("l1")).unwrap();
987
988        // r_0 = rule_1 | rule_3
989        let rule_1 = ata.rules().find(|r| r.id() == 1).unwrap();
990        let rule_3 = ata.rules().find(|r| r.id() == 3).unwrap();
991
992        let r_0 = mgr
993            .get_rule_bdd(rule_1)
994            .unwrap()
995            .or(mgr.get_rule_bdd(rule_3).unwrap());
996
997        // x = I_2
998        let interval_2 = Interval::new(
999            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
1000            false,
1001            IntervalBoundary::Infty,
1002            true,
1003        );
1004        let x = mgr
1005            .get_shared_interval_bdd(&Variable::new("x"), &interval_2)
1006            .unwrap();
1007
1008        // test_bdd & l_0' & !l_1'
1009        let test_bdd = get_test_bdd(&mgr).and(l_0_prime).and(&l_1_prime.not());
1010        // (l_0 & !(x & r_0))
1011        let correct_bdd = l_0.and(&(x.and(&r_0)).not());
1012        let abstract_bdd = mgr.exists_primed(&test_bdd);
1013        assert!(correct_bdd.eq(&abstract_bdd));
1014    }
1015
1016    #[test]
1017    fn test_exists_rule_vars() {
1018        let ata = get_test_aut();
1019        let mgr = BddVarManager::new(BDDManager::default(), &ata);
1020        let l_0 = mgr.get_location_var(&Location::new("l0")).unwrap();
1021        let l_0_prime = mgr.get_primed_location_var(&Location::new("l0")).unwrap();
1022        // l_0 | !l_0'
1023        let correct_bdd = l_0.or(&l_0_prime.not());
1024        let abstract_bdd = mgr.exists_rule_vars(&get_test_bdd(&mgr));
1025        assert!(correct_bdd.eq(&abstract_bdd));
1026    }
1027
1028    #[test]
1029    fn test_display_error() {
1030        let ata = get_test_aut();
1031        let mut mgr = BddVarManager::new(BDDManager::default(), &ata);
1032
1033        let error_loc = mgr.get_location_var(&Location::new("l2"));
1034        assert!(error_loc.is_err());
1035        assert_eq!(
1036            "There exists no bdd variable for location l2".to_owned(),
1037            format!("{}", error_loc.unwrap_err().to_owned())
1038        );
1039
1040        let error_primed_loc = mgr.get_primed_location_var(&Location::new("l2"));
1041        assert!(error_primed_loc.is_err());
1042        assert_eq!(
1043            "There exists no primed bdd variable for location l2".to_owned(),
1044            format!("{}", error_primed_loc.unwrap_err().to_owned())
1045        );
1046
1047        let i_1 = Interval::new(
1048            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(0, 1, false)),
1049            false,
1050            IntervalBoundary::new_bound(WeightedSum::new_empty(), Fraction::new(1, 1, false)),
1051            true,
1052        );
1053        let error_shared = mgr.get_shared_interval_bdd(&Variable::new("z"), &i_1);
1054        assert!(error_shared.is_err());
1055        assert_eq!(
1056            "There exists no bdd for shared variable z and interval [0, 1[".to_owned(),
1057            format!("{}", error_shared.unwrap_err().to_owned())
1058        );
1059
1060        let error_primed_shared = mgr.get_primed_shared_interval_bdd(&Variable::new("z"), &i_1);
1061        assert!(error_primed_shared.is_err());
1062        assert_eq!(
1063            "There exists no primed bdd for shared variable z and interval [0, 1[".to_owned(),
1064            format!("{}", error_primed_shared.unwrap_err().to_owned())
1065        );
1066
1067        let rule = IntervalTARule::new(
1068            0,
1069            Location::new("l0"),
1070            Location::new("l1"),
1071            IntervalConstraint::True,
1072            Vec::new(),
1073        );
1074        let error_rule = mgr.get_rule_bdd(&rule);
1075        assert!(error_rule.is_err());
1076        assert_eq!(
1077            "There exists no bdd for abstract rule 0: l0 -> l1\n    when ( true )\n    do {  }"
1078                .to_owned(),
1079            format!("{}", error_rule.unwrap_err().to_owned())
1080        );
1081
1082        let error_shared = mgr.get_unchanged_interval_bdd(&Variable::new("z"));
1083        assert!(error_shared.is_err());
1084        assert_eq!(
1085            "There exists no unprimed bdd variables for shared variable z".to_owned(),
1086            format!("{}", error_shared.unwrap_err().to_owned())
1087        );
1088
1089        mgr.variable_vars.insert(Variable::new("z"), vec![]);
1090        let error_primed_shared = mgr.get_unchanged_interval_bdd(&Variable::new("z"));
1091        assert!(error_primed_shared.is_err());
1092        assert_eq!(
1093            "There exists no primed bdd variables for shared variable z".to_owned(),
1094            format!("{}", error_primed_shared.unwrap_err().to_owned())
1095        );
1096    }
1097}
taco_zcs_model_checker/zcs/bdd_var_manager.rs

taco_zcs_model_checker/zcs/
bdd_var_manager.rs
