taco_acs_model_checker/acs_threshold_automaton/
index_ctx.rs

1//! This module defines the `IndexCtx` type that serves as a mapping from
2//! indices (`usize`) to elements in an [`IntervalThresholdAutomaton`].
3//!
4//! It enables to use vectors instead of maps in order to save on memory.
5
6use std::collections::HashMap;
7
8use taco_interval_ta::{IntervalThresholdAutomaton, interval::Interval};
9
10use taco_threshold_automaton::{
11    ThresholdAutomaton,
12    expressions::{Location, Variable},
13};
14
15use crate::acs_threshold_automaton::{ACSInterval, ACSLocation, CSVariable};
16
17/// Context providing a mapping from locations, variables and intervals to
18/// indices or in this case types that can be used as indices
19#[derive(Debug, Clone, PartialEq)]
20pub struct IndexCtx {
21    /// Map from [`Location`]s to [`ACSLocation`]s
22    loc_to_index: HashMap<Location, ACSLocation>,
23    /// Map from [`ACSLocation`]s to [`Location`]s
24    index_to_loc: HashMap<ACSLocation, Location>,
25    /// Map from [`Variable`]s to [`CSVariable`]s
26    var_to_index: HashMap<Variable, CSVariable>,
27    /// Map from [`CSVariable`]s to [`Variable`]s
28    index_to_var: HashMap<CSVariable, Variable>,
29    /// Map from a [`CSVariable`] and an [`Interval`] to [`ACSInterval`]
30    interval_to_index: Vec<HashMap<Interval, ACSInterval>>,
31    /// Map from a [`CSVariable`] and an [`ACSInterval`] to an [`Interval`]
32    index_to_interval: Vec<HashMap<ACSInterval, Interval>>,
33}
34
35impl IndexCtx {
36    /// Create a new [`IndexCtx`] for the given interval threshold automaton
37    pub fn new(ta: &IntervalThresholdAutomaton) -> Self {
38        // Initialize index mappings
39        let loc_to_index: HashMap<_, _> = ta
40            .locations()
41            .enumerate()
42            .map(|(i, l)| (l.clone(), ACSLocation(i)))
43            .collect();
44        let index_to_loc = loc_to_index
45            .iter()
46            .map(|(l, csl)| (*csl, l.clone()))
47            .collect();
48
49        let var_to_index: HashMap<_, _> = ta
50            .variables()
51            .enumerate()
52            .map(|(i, v)| (v.clone(), CSVariable(i)))
53            .collect();
54        let index_to_var = var_to_index
55            .iter()
56            .map(|(v, csv)| (*csv, v.clone()))
57            .collect();
58
59        let mut interval_to_index = vec![HashMap::new(); var_to_index.len()];
60        let mut index_to_interval = vec![HashMap::new(); var_to_index.len()];
61
62        for (var, cs_var) in var_to_index.iter() {
63            interval_to_index[cs_var.0] = ta
64                .get_intervals(var)
65                .iter()
66                .enumerate()
67                .map(|(i, interval)| (interval.clone(), ACSInterval(i)))
68                .collect();
69
70            index_to_interval[cs_var.0] = interval_to_index[cs_var.0]
71                .iter()
72                .map(|(int, csint)| (*csint, int.clone()))
73                .collect();
74        }
75
76        Self {
77            loc_to_index,
78            index_to_loc,
79            var_to_index,
80            index_to_var,
81            interval_to_index,
82            index_to_interval,
83        }
84    }
85
86    /// Translate from a [`Location`] to the corresponding [`ACSLocation`]
87    pub fn to_cs_loc(&self, loc: &Location) -> ACSLocation {
88        self.loc_to_index[loc]
89    }
90
91    /// Translate from a [`ACSLocation`] to the corresponding [`Location`]
92    pub fn get_loc(&self, loc: &ACSLocation) -> &Location {
93        &self.index_to_loc[loc]
94    }
95
96    /// Iterate over all locations in the index
97    pub fn locations(&self) -> impl Iterator<Item = (&Location, &ACSLocation)> {
98        self.loc_to_index.iter()
99    }
100
101    /// Translate from a [`Variable`] to the corresponding [`CSVariable`]
102    pub fn to_cs_var(&self, var: &Variable) -> CSVariable {
103        self.var_to_index[var]
104    }
105
106    /// Translate from a [`CSVariable`] to the corresponding [`Variable`]
107    pub fn get_var(&self, var: &CSVariable) -> &Variable {
108        &self.index_to_var[var]
109    }
110
111    /// Iterate over all variables in the context
112    pub fn variables(&self) -> impl Iterator<Item = (&Variable, &CSVariable)> {
113        self.var_to_index.iter()
114    }
115
116    /// Translate from an [`Interval`] of [`CSVariable`] to the corresponding
117    /// [`ACSInterval`]
118    pub fn to_cs_interval(&self, var: &CSVariable, i: &Interval) -> ACSInterval {
119        self.interval_to_index[var.0][i]
120    }
121
122    /// Translate from an [`ACSInterval`] of [`CSVariable`] to the corresponding
123    /// [`Interval`]
124    pub fn get_interval(&self, var: &CSVariable, i: &ACSInterval) -> &Interval {
125        &self.index_to_interval[var.0][i]
126    }
127
128    /// Check whether the interval [`ACSInterval`] for variable [`CSVariable`]
129    /// exists
130    pub fn interval_exists(&self, var: &CSVariable, interval: ACSInterval) -> bool {
131        interval.0 < self.interval_to_index[var.0].len()
132    }
133
134    /// Iterate over all intervals of the given [`CSVariable`]
135    pub fn intervals(&self, var: &CSVariable) -> impl Iterator<Item = (&Interval, &ACSInterval)> {
136        self.interval_to_index[var.0].iter()
137    }
138}
139
140#[cfg(test)]
141mod mock_objects {
142    use std::collections::HashMap;
143
144    use taco_interval_ta::interval::Interval;
145    use taco_threshold_automaton::expressions::{Location, Variable};
146
147    use crate::acs_threshold_automaton::{
148        ACSInterval, ACSLocation, CSVariable, index_ctx::IndexCtx,
149    };
150
151    impl IndexCtx {
152        /// Directly create a new indexctx for testing purposes
153        pub fn new_mock(
154            loc_to_index: HashMap<Location, ACSLocation>,
155            var_to_index: HashMap<Variable, CSVariable>,
156            interval_to_index: Vec<HashMap<Interval, ACSInterval>>,
157        ) -> Self {
158            Self {
159                loc_to_index: loc_to_index.clone(),
160                index_to_loc: loc_to_index.into_iter().map(|(k, v)| (v, k)).collect(),
161                var_to_index: var_to_index.clone(),
162                index_to_var: var_to_index.into_iter().map(|(k, v)| (v, k)).collect(),
163                interval_to_index: interval_to_index.clone(),
164                index_to_interval: interval_to_index
165                    .into_iter()
166                    .map(|inner| inner.into_iter().map(|(k, v)| (v, k)).collect())
167                    .collect(),
168            }
169        }
170    }
171}
172
173#[cfg(test)]
174mod tests {
175    use std::collections::HashMap;
176
177    use taco_interval_ta::{
178        builder::IntervalTABuilder,
179        interval::{Interval, IntervalBoundary},
180    };
181
182    use taco_smt_encoder::SMTSolverBuilder;
183    use taco_threshold_automaton::{
184        expressions::{
185            BooleanExpression, ComparisonOp, IntegerExpression, Location, Parameter, Variable,
186        },
187        general_threshold_automaton::{
188            Action,
189            builder::{GeneralThresholdAutomatonBuilder, RuleBuilder},
190        },
191        lia_threshold_automaton::LIAThresholdAutomaton,
192    };
193
194    use crate::acs_threshold_automaton::{
195        ACSInterval, ACSLocation, CSVariable, index_ctx::IndexCtx,
196    };
197
198    #[test]
199    fn test_new_index_ctx() {
200        let var = Variable::new("x");
201
202        let rc = BooleanExpression::ComparisonExpression(
203            Box::new(IntegerExpression::Param(Parameter::new("n"))),
204            ComparisonOp::Gt,
205            Box::new(IntegerExpression::Const(3)),
206        );
207
208        let ta = GeneralThresholdAutomatonBuilder::new("test_ta")
209            .with_variables([var.clone()])
210            .unwrap()
211            .with_locations([Location::new("l1")])
212            .unwrap()
213            .with_parameter(Parameter::new("n"))
214            .unwrap()
215            .initialize()
216            .with_resilience_condition(rc.clone())
217            .unwrap()
218            .with_initial_location_constraint(BooleanExpression::ComparisonExpression(
219                Box::new(IntegerExpression::Atom(Location::new("l1"))),
220                ComparisonOp::Eq,
221                Box::new(IntegerExpression::Const(0)),
222            ))
223            .unwrap()
224            .with_rule(
225                RuleBuilder::new(0, Location::new("l1"), Location::new("l1"))
226                    .with_guard(BooleanExpression::ComparisonExpression(
227                        Box::new(IntegerExpression::Atom(var.clone())),
228                        ComparisonOp::Gt,
229                        Box::new(IntegerExpression::Const(2)),
230                    ))
231                    .with_action(
232                        Action::new(
233                            var.clone(),
234                            IntegerExpression::Const(1) + IntegerExpression::Atom(var.clone()),
235                        )
236                        .unwrap(),
237                    )
238                    .build(),
239            )
240            .unwrap()
241            .build();
242
243        let lia_ta = LIAThresholdAutomaton::try_from(ta).unwrap();
244
245        let mut interval_tas = IntervalTABuilder::new(lia_ta, SMTSolverBuilder::default(), vec![])
246            .build()
247            .unwrap();
248        let interval_threshold_automaton = interval_tas.next().unwrap();
249        assert!(interval_tas.next().is_none());
250
251        let got_idx_ctx = IndexCtx::new(&interval_threshold_automaton);
252
253        let expected_idx_ctx = IndexCtx {
254            loc_to_index: HashMap::from([(Location::new("l1"), ACSLocation(0))]),
255            index_to_loc: HashMap::from([(ACSLocation(0), Location::new("l1"))]),
256            var_to_index: HashMap::from([(Variable::new("x"), CSVariable(0))]),
257            index_to_var: HashMap::from([(CSVariable(0), Variable::new("x"))]),
258            interval_to_index: vec![HashMap::from([
259                (Interval::new_constant(0, 1), ACSInterval(0)),
260                (Interval::new_constant(1, 3), ACSInterval(1)),
261                (
262                    Interval::new(
263                        IntervalBoundary::from_const(3),
264                        false,
265                        IntervalBoundary::new_infty(),
266                        true,
267                    ),
268                    ACSInterval(2),
269                ),
270            ])],
271            index_to_interval: vec![HashMap::from([
272                (ACSInterval(0), Interval::new_constant(0, 1)),
273                (ACSInterval(1), Interval::new_constant(1, 3)),
274                (
275                    ACSInterval(2),
276                    Interval::new(
277                        IntervalBoundary::from_const(3),
278                        false,
279                        IntervalBoundary::new_infty(),
280                        true,
281                    ),
282                ),
283            ])],
284        };
285
286        assert_eq!(got_idx_ctx, expected_idx_ctx);
287    }
288
289    #[test]
290    fn test_to_cs_loc() {
291        let ctx = IndexCtx {
292            loc_to_index: HashMap::from([
293                (Location::new("l1"), ACSLocation(0)),
294                (Location::new("l2"), ACSLocation(1)),
295            ]),
296            index_to_loc: HashMap::from([
297                (ACSLocation(0), Location::new("l1")),
298                (ACSLocation(1), Location::new("l2")),
299            ]),
300            var_to_index: HashMap::from([]),
301            index_to_var: HashMap::from([]),
302            interval_to_index: vec![],
303            index_to_interval: vec![],
304        };
305
306        assert_eq!(ctx.to_cs_loc(&Location::new("l1")), ACSLocation(0));
307        assert_eq!(ctx.to_cs_loc(&Location::new("l2")), ACSLocation(1));
308    }
309
310    #[test]
311    fn test_from_cs_loc() {
312        let ctx = IndexCtx {
313            loc_to_index: HashMap::from([
314                (Location::new("l1"), ACSLocation(0)),
315                (Location::new("l2"), ACSLocation(1)),
316            ]),
317            index_to_loc: HashMap::from([
318                (ACSLocation(0), Location::new("l1")),
319                (ACSLocation(1), Location::new("l2")),
320            ]),
321            var_to_index: HashMap::from([]),
322            index_to_var: HashMap::from([]),
323            interval_to_index: vec![],
324            index_to_interval: vec![],
325        };
326
327        assert_eq!(ctx.get_loc(&ACSLocation(0)), &Location::new("l1"));
328        assert_eq!(ctx.get_loc(&ACSLocation(1)), &Location::new("l2"));
329    }
330
331    #[test]
332    fn test_locations() {
333        let ctx = IndexCtx {
334            loc_to_index: HashMap::from([
335                (Location::new("l1"), ACSLocation(0)),
336                (Location::new("l2"), ACSLocation(1)),
337            ]),
338            index_to_loc: HashMap::from([
339                (ACSLocation(0), Location::new("l1")),
340                (ACSLocation(1), Location::new("l2")),
341            ]),
342            var_to_index: HashMap::from([]),
343            index_to_var: HashMap::from([]),
344            interval_to_index: vec![],
345            index_to_interval: vec![],
346        };
347
348        assert_eq!(
349            ctx.locations().collect::<HashMap<_, _>>(),
350            HashMap::from([
351                (&Location::new("l1"), &ACSLocation(0)),
352                (&Location::new("l2"), &ACSLocation(1)),
353            ])
354        );
355    }
356
357    #[test]
358    fn test_to_cs_var() {
359        let ctx = IndexCtx {
360            loc_to_index: HashMap::from([]),
361            index_to_loc: HashMap::from([]),
362            var_to_index: HashMap::from([
363                (Variable::new("x"), CSVariable(0)),
364                (Variable::new("y"), CSVariable(1)),
365            ]),
366            index_to_var: HashMap::from([
367                (CSVariable(0), Variable::new("x")),
368                (CSVariable(1), Variable::new("y")),
369            ]),
370            interval_to_index: vec![],
371            index_to_interval: vec![],
372        };
373
374        assert_eq!(ctx.to_cs_var(&Variable::new("x")), CSVariable(0));
375        assert_eq!(ctx.to_cs_var(&Variable::new("y")), CSVariable(1));
376    }
377
378    #[test]
379    fn test_from_cs_var() {
380        let ctx = IndexCtx {
381            loc_to_index: HashMap::from([]),
382            index_to_loc: HashMap::from([]),
383            var_to_index: HashMap::from([
384                (Variable::new("x"), CSVariable(0)),
385                (Variable::new("y"), CSVariable(1)),
386            ]),
387            index_to_var: HashMap::from([
388                (CSVariable(0), Variable::new("x")),
389                (CSVariable(1), Variable::new("y")),
390            ]),
391            interval_to_index: vec![],
392            index_to_interval: vec![],
393        };
394
395        assert_eq!(ctx.get_var(&CSVariable(0)), &Variable::new("x"));
396        assert_eq!(ctx.get_var(&CSVariable(1)), &Variable::new("y"));
397    }
398
399    #[test]
400    fn test_variables() {
401        let ctx = IndexCtx {
402            loc_to_index: HashMap::from([]),
403            index_to_loc: HashMap::from([]),
404            var_to_index: HashMap::from([
405                (Variable::new("x"), CSVariable(0)),
406                (Variable::new("y"), CSVariable(1)),
407            ]),
408            index_to_var: HashMap::from([
409                (CSVariable(0), Variable::new("x")),
410                (CSVariable(1), Variable::new("y")),
411            ]),
412            interval_to_index: vec![],
413            index_to_interval: vec![],
414        };
415
416        assert_eq!(
417            ctx.variables().collect::<HashMap<_, _>>(),
418            HashMap::from([
419                (&Variable::new("x"), &CSVariable(0)),
420                (&Variable::new("y"), &CSVariable(1)),
421            ])
422        );
423    }
424
425    #[test]
426    fn test_to_cs_interval() {
427        let ctx = IndexCtx {
428            loc_to_index: HashMap::from([]),
429            index_to_loc: HashMap::from([]),
430            var_to_index: HashMap::from([]),
431            index_to_var: HashMap::from([]),
432            interval_to_index: vec![
433                HashMap::from([
434                    (Interval::new_constant(0, 1), ACSInterval(0)),
435                    (Interval::new_constant(1, 2), ACSInterval(1)),
436                    (
437                        Interval::new(
438                            IntervalBoundary::from_const(2),
439                            false,
440                            IntervalBoundary::new_infty(),
441                            true,
442                        ),
443                        ACSInterval(2),
444                    ),
445                ]),
446                HashMap::from([
447                    (Interval::new_constant(0, 1), ACSInterval(0)),
448                    (
449                        Interval::new(
450                            IntervalBoundary::from_const(1),
451                            false,
452                            IntervalBoundary::new_infty(),
453                            true,
454                        ),
455                        ACSInterval(1),
456                    ),
457                ]),
458            ],
459            index_to_interval: vec![
460                HashMap::from([
461                    (ACSInterval(0), Interval::new_constant(0, 1)),
462                    (ACSInterval(1), Interval::new_constant(1, 2)),
463                    (
464                        ACSInterval(2),
465                        Interval::new(
466                            IntervalBoundary::from_const(2),
467                            false,
468                            IntervalBoundary::new_infty(),
469                            true,
470                        ),
471                    ),
472                ]),
473                HashMap::from([
474                    (ACSInterval(0), Interval::new_constant(0, 1)),
475                    (
476                        ACSInterval(1),
477                        Interval::new(
478                            IntervalBoundary::from_const(1),
479                            false,
480                            IntervalBoundary::new_infty(),
481                            true,
482                        ),
483                    ),
484                ]),
485            ],
486        };
487
488        assert_eq!(
489            ctx.to_cs_interval(&CSVariable(0), &Interval::new_constant(0, 1)),
490            ACSInterval(0)
491        );
492        assert_eq!(
493            ctx.to_cs_interval(&CSVariable(0), &Interval::new_constant(1, 2)),
494            ACSInterval(1)
495        );
496        assert_eq!(
497            ctx.to_cs_interval(
498                &CSVariable(0),
499                &Interval::new(
500                    IntervalBoundary::from_const(2),
501                    false,
502                    IntervalBoundary::new_infty(),
503                    true,
504                ),
505            ),
506            ACSInterval(2)
507        );
508        assert_eq!(
509            ctx.to_cs_interval(&CSVariable(1), &Interval::new_constant(0, 1)),
510            ACSInterval(0)
511        );
512        assert_eq!(
513            ctx.to_cs_interval(
514                &CSVariable(1),
515                &Interval::new(
516                    IntervalBoundary::from_const(1),
517                    false,
518                    IntervalBoundary::new_infty(),
519                    true,
520                ),
521            ),
522            ACSInterval(1)
523        );
524    }
525
526    #[test]
527    fn test_from_cs_interval() {
528        let ctx = IndexCtx {
529            loc_to_index: HashMap::from([]),
530            index_to_loc: HashMap::from([]),
531            var_to_index: HashMap::from([]),
532            index_to_var: HashMap::from([]),
533            interval_to_index: vec![
534                HashMap::from([
535                    (Interval::new_constant(0, 1), ACSInterval(0)),
536                    (Interval::new_constant(1, 2), ACSInterval(1)),
537                    (
538                        Interval::new(
539                            IntervalBoundary::from_const(2),
540                            false,
541                            IntervalBoundary::new_infty(),
542                            true,
543                        ),
544                        ACSInterval(2),
545                    ),
546                ]),
547                HashMap::from([
548                    (Interval::new_constant(0, 1), ACSInterval(0)),
549                    (
550                        Interval::new(
551                            IntervalBoundary::from_const(1),
552                            false,
553                            IntervalBoundary::new_infty(),
554                            true,
555                        ),
556                        ACSInterval(1),
557                    ),
558                ]),
559            ],
560            index_to_interval: vec![
561                HashMap::from([
562                    (ACSInterval(0), Interval::new_constant(0, 1)),
563                    (ACSInterval(1), Interval::new_constant(1, 2)),
564                    (
565                        ACSInterval(2),
566                        Interval::new(
567                            IntervalBoundary::from_const(2),
568                            false,
569                            IntervalBoundary::new_infty(),
570                            true,
571                        ),
572                    ),
573                ]),
574                HashMap::from([
575                    (ACSInterval(0), Interval::new_constant(0, 1)),
576                    (
577                        ACSInterval(1),
578                        Interval::new(
579                            IntervalBoundary::from_const(1),
580                            false,
581                            IntervalBoundary::new_infty(),
582                            true,
583                        ),
584                    ),
585                ]),
586            ],
587        };
588
589        assert_eq!(
590            ctx.get_interval(&CSVariable(0), &ACSInterval(0)),
591            &Interval::new_constant(0, 1)
592        );
593        assert_eq!(
594            ctx.get_interval(&CSVariable(0), &ACSInterval(1)),
595            &Interval::new_constant(1, 2)
596        );
597        assert_eq!(
598            ctx.get_interval(&CSVariable(0), &ACSInterval(2)),
599            &Interval::new(
600                IntervalBoundary::from_const(2),
601                false,
602                IntervalBoundary::new_infty(),
603                true,
604            ),
605        );
606        assert_eq!(
607            ctx.get_interval(&CSVariable(1), &ACSInterval(0)),
608            &Interval::new_constant(0, 1)
609        );
610        assert_eq!(
611            ctx.get_interval(&CSVariable(1), &ACSInterval(1)),
612            &Interval::new(
613                IntervalBoundary::from_const(1),
614                false,
615                IntervalBoundary::new_infty(),
616                true,
617            ),
618        );
619    }
620
621    #[test]
622    fn test_exists_interval() {
623        let ctx = IndexCtx {
624            loc_to_index: HashMap::from([]),
625            index_to_loc: HashMap::from([]),
626            var_to_index: HashMap::from([]),
627            index_to_var: HashMap::from([]),
628            interval_to_index: vec![
629                HashMap::from([
630                    (Interval::new_constant(0, 1), ACSInterval(0)),
631                    (Interval::new_constant(1, 2), ACSInterval(1)),
632                    (
633                        Interval::new(
634                            IntervalBoundary::from_const(2),
635                            false,
636                            IntervalBoundary::new_infty(),
637                            true,
638                        ),
639                        ACSInterval(2),
640                    ),
641                ]),
642                HashMap::from([
643                    (Interval::new_constant(0, 1), ACSInterval(0)),
644                    (
645                        Interval::new(
646                            IntervalBoundary::from_const(1),
647                            false,
648                            IntervalBoundary::new_infty(),
649                            true,
650                        ),
651                        ACSInterval(1),
652                    ),
653                ]),
654            ],
655            index_to_interval: vec![
656                HashMap::from([
657                    (ACSInterval(0), Interval::new_constant(0, 1)),
658                    (ACSInterval(1), Interval::new_constant(1, 2)),
659                    (
660                        ACSInterval(2),
661                        Interval::new(
662                            IntervalBoundary::from_const(2),
663                            false,
664                            IntervalBoundary::new_infty(),
665                            true,
666                        ),
667                    ),
668                ]),
669                HashMap::from([
670                    (ACSInterval(0), Interval::new_constant(0, 1)),
671                    (
672                        ACSInterval(1),
673                        Interval::new(
674                            IntervalBoundary::from_const(1),
675                            false,
676                            IntervalBoundary::new_infty(),
677                            true,
678                        ),
679                    ),
680                ]),
681            ],
682        };
683
684        assert!(ctx.interval_exists(&CSVariable(0), ACSInterval(0)));
685        assert!(ctx.interval_exists(&CSVariable(1), ACSInterval(0)));
686
687        assert!(!ctx.interval_exists(&CSVariable(0), ACSInterval(5)));
688        assert!(!ctx.interval_exists(&CSVariable(0), ACSInterval(3)));
689    }
690
691    #[test]
692    fn test_intervals() {
693        let ctx = IndexCtx {
694            loc_to_index: HashMap::from([]),
695            index_to_loc: HashMap::from([]),
696            var_to_index: HashMap::from([]),
697            index_to_var: HashMap::from([]),
698            interval_to_index: vec![
699                HashMap::from([
700                    (Interval::new_constant(0, 1), ACSInterval(0)),
701                    (Interval::new_constant(1, 2), ACSInterval(1)),
702                    (
703                        Interval::new(
704                            IntervalBoundary::from_const(2),
705                            false,
706                            IntervalBoundary::new_infty(),
707                            true,
708                        ),
709                        ACSInterval(2),
710                    ),
711                ]),
712                HashMap::from([
713                    (Interval::new_constant(0, 1), ACSInterval(0)),
714                    (
715                        Interval::new(
716                            IntervalBoundary::from_const(1),
717                            false,
718                            IntervalBoundary::new_infty(),
719                            true,
720                        ),
721                        ACSInterval(1),
722                    ),
723                ]),
724            ],
725            index_to_interval: vec![
726                HashMap::from([
727                    (ACSInterval(0), Interval::new_constant(0, 1)),
728                    (ACSInterval(1), Interval::new_constant(1, 2)),
729                    (
730                        ACSInterval(2),
731                        Interval::new(
732                            IntervalBoundary::from_const(2),
733                            false,
734                            IntervalBoundary::new_infty(),
735                            true,
736                        ),
737                    ),
738                ]),
739                HashMap::from([
740                    (ACSInterval(0), Interval::new_constant(0, 1)),
741                    (
742                        ACSInterval(1),
743                        Interval::new(
744                            IntervalBoundary::from_const(1),
745                            false,
746                            IntervalBoundary::new_infty(),
747                            true,
748                        ),
749                    ),
750                ]),
751            ],
752        };
753
754        assert_eq!(
755            ctx.intervals(&CSVariable(0))
756                .map(|(a, b)| (a.clone(), *b))
757                .collect::<HashMap<_, _>>(),
758            HashMap::from([
759                (Interval::new_constant(0, 1), ACSInterval(0)),
760                (Interval::new_constant(1, 2), ACSInterval(1)),
761                (
762                    Interval::new(
763                        IntervalBoundary::from_const(2),
764                        false,
765                        IntervalBoundary::new_infty(),
766                        true,
767                    ),
768                    ACSInterval(2),
769                ),
770            ])
771        );
772        assert_eq!(
773            ctx.intervals(&CSVariable(1))
774                .map(|(a, b)| (a.clone(), *b))
775                .collect::<HashMap<_, _>>(),
776            HashMap::from([
777                (Interval::new_constant(0, 1), ACSInterval(0)),
778                (
779                    Interval::new(
780                        IntervalBoundary::from_const(1),
781                        false,
782                        IntervalBoundary::new_infty(),
783                        true,
784                    ),
785                    ACSInterval(1),
786                ),
787            ])
788        );
789    }
790}
taco_acs_model_checker/acs_threshold_automaton/index_ctx.rs

taco_acs_model_checker/acs_threshold_automaton/
index_ctx.rs
