taco_acs_model_checker/
acs_threshold_automaton.rs

1//! A ThresholdAutomaton representation for efficient operations on counter
2//! systems and counter configurations
3//!
4//! This module and its submodule define the [`ACSThresholdAutomaton`] type,
5//! along with the [`ACSTAConfig`] type, which are compact representations of
6//! counter states in a threshold automaton.
7//! The main goal of these types is to have a representation of configurations
8//! with a small memory footprint, which allow for efficient computations of
9//! (certain) predecessor configurations.
10//!
11//! Therefore, internally a configuration is just implemented as a vector of
12//! integers, to indicate the current interval and the number of processes per
13//! variable.
14//!
15//! These types correspond to the `ACS` described in the paper
16//! [Parameterized Verification of Round-based Distributed Algorithms via
17//! Extended Threshold Automata](https://arxiv.org/pdf/2406.19880)
18
19use std::{collections::HashSet, fmt};
20
21use taco_display_utils::indent_all;
22use taco_interval_ta::{
23    IntervalActionEffect, IntervalConstraint, IntervalTAAction, IntervalTARule,
24    IntervalThresholdAutomaton,
25};
26
27use taco_threshold_automaton::{
28    ActionDefinition, RuleDefinition, ThresholdAutomaton,
29    expressions::{IsDeclared, Location, Parameter, Variable},
30    general_threshold_automaton::Rule,
31};
32
33use crate::acs_threshold_automaton::{
34    configuration::{ACSIntervalState, ACSTAConfig},
35    index_ctx::IndexCtx,
36};
37
38pub mod configuration;
39mod index_ctx;
40
41/// A location in a [`ACSThresholdAutomaton`]
42///
43/// Such a location is internally only represents an index in the representation
44/// of location state, i.e., it describes which position of the vector holds the
45/// number of processes in its concrete counter part (a
46/// [`Location`]).
47///
48/// The mapping from [`Location`] to [`ACSLocation`] is
49/// maintained by the[`ACSThresholdAutomaton`]. It is important to not
50/// mix [`ACSLocation`] of different automata as it can result in panics and
51/// wrong results, as validation has been omitted for better performance.
52#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
53pub struct ACSLocation(usize);
54
55impl ACSLocation {
56    /// Get a string representation of the location, i.e. the name of the
57    /// corresponding [`Location`]
58    pub fn display(&self, ta: &ACSThresholdAutomaton) -> String {
59        ta.idx_ctx.get_loc(self).to_string()
60    }
61}
62
63/// A variable in a [`ACSThresholdAutomaton`]
64///
65/// Such a variable is internally only represents an index in the representation
66/// of an interval state, i.e., it describes which position of the vector holds
67/// the value of the interval in its concrete counter part (a
68/// [`Variable`]).
69///
70/// The mapping from [`Variable`] to [`CSVariable`] is
71/// maintained by the[`ACSThresholdAutomaton`]. It is important to not
72/// mix [`CSVariable`] of different automata as it can result in panics and
73/// wrong results, as validation has been omitted for better performance.
74#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
75pub struct CSVariable(usize);
76
77impl CSVariable {
78    /// Get a string representation of the variable, i.e., the name of the
79    /// [`Variable`] this variable corresponds to
80    pub fn display(&self, ta: &ACSThresholdAutomaton) -> String {
81        ta.idx_ctx.get_var(self).to_string()
82    }
83}
84
85/// An interval in a [`ACSThresholdAutomaton`]
86///
87/// Such a interval is internally only represents an integer, which is the index
88/// of the interval in the current interval order. That is it describes the
89/// index of an [`taco_interval_ta::interval::Interval`] for a
90/// specific variable, as defined by the
91/// [`IntervalThresholdAutomaton`].
92///
93/// It is important to not mix [`ACSInterval`] of different automata as it
94/// can result in panics and wrong results, as validation has been omitted for
95/// better performance.
96#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
97pub struct ACSInterval(usize);
98
99impl ACSInterval {
100    /// Get a string representation of the interval, i.e., get the string
101    /// representation of the corresponding
102    /// [`taco_interval_ta::interval::Interval`]
103    pub fn display(&self, var: &CSVariable, ta: &ACSThresholdAutomaton) -> String {
104        ta.idx_ctx.get_interval(var, self).to_string()
105    }
106}
107
108/// A variant of an [`IntervalThresholdAutomaton`] allowing for low-memory
109/// representations of configurations (by a [`ACSTAConfig`]) and efficient
110/// predecessor computations
111///
112/// This type is a variant of an [`IntervalThresholdAutomaton`] that translates
113/// variables (see [`CSVariable`]), locations (see [`ACSLocation`]) and intervals
114/// (see [`ACSInterval`]) into indices, that can then be used to in
115/// [`ACSTAConfig`] instead of the corresponding concrete types. The mapping is
116/// then maintained in this type.
117///
118/// Additionally, initial location configurations and intervals, as well
119/// as rules (see [`CSRule`]) are already translated into operations on the
120/// abstracted states, such that they do not need to be translated on the fly.
121#[derive(Debug, Clone)]
122pub struct ACSThresholdAutomaton {
123    /// Main index maintaining the mapping of locations, variables and intervals
124    idx_ctx: IndexCtx,
125    /// [`IntervalThresholdAutomaton`] that this threshold automaton is an
126    /// abstraction of
127    interval_ta: IntervalThresholdAutomaton,
128    /// Initial locations (as [`ACSLocation`]s)
129    initial_locs: Vec<ACSLocation>,
130    /// Initial intervals (as [`ACSInterval`]s, indexed by [`CSVariable`])
131    initial_intervals: Vec<HashSet<ACSInterval>>,
132    /// Rules operation on cs types
133    rules: Vec<CSRule>,
134}
135
136impl ACSThresholdAutomaton {
137    /// Create the corresponding [`ACSThresholdAutomaton`] from the given
138    /// [`IntervalThresholdAutomaton`]
139    pub fn new(interval_ta: IntervalThresholdAutomaton) -> Self {
140        let idx_ctx = IndexCtx::new(&interval_ta);
141
142        let initial_locs = interval_ta
143            .locations()
144            .filter(|loc| interval_ta.can_be_initial_location(loc))
145            .map(|loc| idx_ctx.to_cs_loc(loc))
146            .collect();
147
148        let mut initial_intervals = vec![HashSet::new(); idx_ctx.variables().count()];
149        for (var, var_cs) in idx_ctx.variables() {
150            for interval in interval_ta.get_initial_interval(var) {
151                initial_intervals[var_cs.0].insert(idx_ctx.to_cs_interval(var_cs, interval));
152            }
153        }
154
155        let rules: Vec<_> = interval_ta
156            .rules()
157            .map(|r| CSRule::from_interval_rule(&idx_ctx, r))
158            .collect();
159
160        debug_assert!(
161            !rules
162                .iter()
163                .any(|r1| rules.iter().any(|r2| r1.id() == r2.id() && r1 != r2)),
164            "Rule ids in the threshold automaton must be unique"
165        );
166
167        Self {
168            idx_ctx,
169            interval_ta,
170            initial_locs,
171            initial_intervals,
172            rules,
173        }
174    }
175
176    /// Check whether the location is an initial location, i.e. processes can
177    /// start in this location
178    pub fn is_initial_loc(&self, loc: &ACSLocation) -> bool {
179        self.initial_locs.contains(loc)
180    }
181
182    /// Check whether the interval `i` is an initial interval for variable
183    /// `var`
184    pub fn is_initial_interval(&self, var: &CSVariable, i: &ACSInterval) -> bool {
185        self.initial_intervals[var.0].contains(i)
186    }
187
188    /// Get the zero interval for variable `var`
189    pub fn get_zero_interval(&self, var: &CSVariable) -> ACSInterval {
190        let zero_interval = self
191            .interval_ta
192            .get_zero_interval(self.idx_ctx.get_var(var));
193
194        self.idx_ctx.to_cs_interval(var, zero_interval)
195    }
196
197    /// Get all intervals for the variable
198    pub fn get_all_intervals<'a>(
199        &'a self,
200        var: &'a CSVariable,
201    ) -> impl Iterator<Item = &'a ACSInterval> {
202        self.idx_ctx.intervals(var).map(|(_, i)| i)
203    }
204
205    /// Get the previous interval
206    pub fn get_prev_interval(
207        &self,
208        _var: &CSVariable,
209        interval: &ACSInterval,
210    ) -> Option<ACSInterval> {
211        if interval.0 == 0 {
212            return None;
213        }
214
215        // We rely on the fact that the interval indices  in `IndexCtx`
216        // are created with respect to the interval order and that there are no
217        // jumps. Therefore we can simply compute the predecessor on the index.
218        //
219        // The next assertion checks this invariant at runtime
220        debug_assert!(
221            self.interval_ta.get_previous_interval(
222                self.idx_ctx.get_var(_var),
223                self.idx_ctx.get_interval(_var, interval)
224            ) == Some(
225                self.idx_ctx
226                    .get_interval(_var, &ACSInterval(interval.0 - 1))
227            ),
228            "IndexCtx was not initialized respecting the variable ordering"
229        );
230
231        Some(ACSInterval(interval.0 - 1))
232    }
233
234    /// Get the next interval
235    pub fn get_next_interval(
236        &self,
237        var: &CSVariable,
238        interval: &ACSInterval,
239    ) -> Option<ACSInterval> {
240        let res = ACSInterval(interval.0 + 1);
241
242        if !self.idx_ctx.interval_exists(var, res) {
243            return None;
244        }
245
246        // We rely on the fact that the interval indices  in `IndexCtx`
247        // are created with respect to the interval order and that there are no
248        // jumps. Therefore we can simply compute the predecessor on the index.
249        //
250        // The next assertion checks this invariant at runtime
251        debug_assert!(
252            self.interval_ta.get_next_interval(
253                self.idx_ctx.get_var(var),
254                self.idx_ctx.get_interval(var, interval)
255            ) == Some(self.idx_ctx.get_interval(var, &res)),
256            "IndexCtx was not initialized respecting the variable ordering"
257        );
258
259        Some(res)
260    }
261
262    /// Get all variables appearing in the threshold automaton
263    pub fn variables(&self) -> impl Iterator<Item = &CSVariable> {
264        self.idx_ctx.variables().map(|(_, v)| v)
265    }
266
267    /// Get all [`ACSLocation`]s of the automaton
268    pub fn locations(&self) -> impl Iterator<Item = &ACSLocation> {
269        self.idx_ctx.locations().map(|(_, loc)| loc)
270    }
271
272    /// Get all rules of the automaton
273    pub fn rules(&self) -> impl Iterator<Item = &CSRule> {
274        self.rules.iter()
275    }
276
277    /// Get rule by id
278    pub fn get_rule_by_id(&self, id: u32) -> Option<&Rule> {
279        self.interval_ta.get_ta().rules().find(|r| r.id() == id)
280    }
281
282    /// Get a reference to the interval threshold automaton the automaton
283    /// has been derived from
284    pub fn get_interval_ta(&self) -> &IntervalThresholdAutomaton {
285        &self.interval_ta
286    }
287}
288
289impl From<IntervalThresholdAutomaton> for ACSThresholdAutomaton {
290    fn from(value: IntervalThresholdAutomaton) -> Self {
291        Self::new(value)
292    }
293}
294
295impl IsDeclared<Parameter> for ACSThresholdAutomaton {
296    fn is_declared(&self, obj: &Parameter) -> bool {
297        self.interval_ta.is_declared(obj)
298    }
299}
300
301impl IsDeclared<Variable> for ACSThresholdAutomaton {
302    fn is_declared(&self, obj: &Variable) -> bool {
303        self.interval_ta.is_declared(obj)
304    }
305}
306
307impl IsDeclared<Location> for ACSThresholdAutomaton {
308    fn is_declared(&self, obj: &Location) -> bool {
309        self.interval_ta.is_declared(obj)
310    }
311}
312
313impl fmt::Display for ACSThresholdAutomaton {
314    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
315        write!(
316            f,
317            "CSThresholdAutomaton {{\n {}\n}}",
318            indent_all(self.interval_ta.to_string())
319        )
320    }
321}
322
323impl ThresholdAutomaton for ACSThresholdAutomaton {
324    type Rule = IntervalTARule;
325
326    type InitialVariableConstraintType = IntervalConstraint;
327
328    fn name(&self) -> &str {
329        self.interval_ta.name()
330    }
331
332    fn parameters(
333        &self,
334    ) -> impl Iterator<Item = &taco_threshold_automaton::expressions::Parameter> {
335        self.interval_ta.parameters()
336    }
337
338    fn initial_location_constraints(
339        &self,
340    ) -> impl Iterator<Item = &taco_threshold_automaton::LocationConstraint> {
341        self.interval_ta.initial_location_constraints()
342    }
343
344    fn initial_variable_constraints(
345        &self,
346    ) -> impl Iterator<Item = &Self::InitialVariableConstraintType> {
347        self.interval_ta.initial_variable_constraints()
348    }
349
350    fn resilience_conditions(
351        &self,
352    ) -> impl Iterator<
353        Item = &taco_threshold_automaton::expressions::BooleanExpression<
354            taco_threshold_automaton::expressions::Parameter,
355        >,
356    > {
357        self.interval_ta.resilience_conditions()
358    }
359
360    fn variables(&self) -> impl Iterator<Item = &taco_threshold_automaton::expressions::Variable> {
361        self.interval_ta.variables()
362    }
363
364    fn locations(&self) -> impl Iterator<Item = &taco_threshold_automaton::expressions::Location> {
365        self.interval_ta.locations()
366    }
367
368    fn can_be_initial_location(
369        &self,
370        location: &taco_threshold_automaton::expressions::Location,
371    ) -> bool {
372        self.interval_ta.can_be_initial_location(location)
373    }
374
375    fn rules(&self) -> impl Iterator<Item = &Self::Rule> {
376        self.interval_ta.rules()
377    }
378
379    fn incoming_rules(
380        &self,
381        location: &taco_threshold_automaton::expressions::Location,
382    ) -> impl Iterator<Item = &Self::Rule> {
383        self.interval_ta.incoming_rules(location)
384    }
385
386    fn outgoing_rules(
387        &self,
388        location: &taco_threshold_automaton::expressions::Location,
389    ) -> impl Iterator<Item = &Self::Rule> {
390        self.interval_ta.outgoing_rules(location)
391    }
392}
393
394/// Constraints on interval states operating on [`ACSInterval`]s and
395/// [`CSVariable`]s
396#[derive(Debug, Clone, PartialEq, Eq, Hash)]
397pub enum CSIntervalConstraint {
398    /// Always enabled
399    True,
400    /// Always disabled
401    False,
402    /// A conjunction of two [`CSIntervalConstraint`]s
403    Conj(Box<CSIntervalConstraint>, Box<CSIntervalConstraint>),
404    /// A disjunction of two [`CSIntervalConstraint`]s
405    Disj(Box<CSIntervalConstraint>, Box<CSIntervalConstraint>),
406    /// Constraint on an interval the variable should be in
407    VarGuard(CSVariable, Vec<ACSInterval>),
408}
409
410impl CSIntervalConstraint {
411    /// Translate from a [`IntervalConstraint`] to a [`CSIntervalConstraint`]
412    fn from_interval_constr(ta_cs: &IndexCtx, ics: &IntervalConstraint) -> Self {
413        match ics {
414            IntervalConstraint::True => Self::True,
415            IntervalConstraint::False => Self::False,
416            IntervalConstraint::Conj(lhs, rhs) => {
417                let lhs = Self::from_interval_constr(ta_cs, lhs);
418                let rhs = Self::from_interval_constr(ta_cs, rhs);
419
420                CSIntervalConstraint::Conj(Box::new(lhs), Box::new(rhs))
421            }
422            IntervalConstraint::Disj(lhs, rhs) => {
423                let lhs = Self::from_interval_constr(ta_cs, lhs);
424                let rhs = Self::from_interval_constr(ta_cs, rhs);
425
426                CSIntervalConstraint::Disj(Box::new(lhs), Box::new(rhs))
427            }
428            IntervalConstraint::SingleVarIntervalConstr(var, intervals) => {
429                let var = ta_cs.to_cs_var(var);
430                let intervals = intervals
431                    .iter()
432                    .map(|i| ta_cs.to_cs_interval(&var, i))
433                    .collect();
434
435                CSIntervalConstraint::VarGuard(var, intervals)
436            }
437            IntervalConstraint::MultiVarIntervalConstr(_weighted_sum, _intervals) => todo!(),
438        }
439    }
440
441    /// Check whether the given interval state satisfies the constraint
442    fn is_satisfied(&self, interval_state: &ACSIntervalState) -> bool {
443        match self {
444            CSIntervalConstraint::True => true,
445            CSIntervalConstraint::False => false,
446            CSIntervalConstraint::Conj(lhs, rhs) => {
447                lhs.is_satisfied(interval_state) && rhs.is_satisfied(interval_state)
448            }
449            CSIntervalConstraint::Disj(lhs, rhs) => {
450                lhs.is_satisfied(interval_state) || rhs.is_satisfied(interval_state)
451            }
452            CSIntervalConstraint::VarGuard(var, intervals) => {
453                intervals.contains(&interval_state[*var])
454            }
455        }
456    }
457}
458
459/// Effect of the application of a [`CSRule`] on [`CSVariable`]
460#[derive(Debug, Clone, PartialEq, Eq, Hash)]
461pub struct CSIntervalAction {
462    /// Variable
463    var: CSVariable,
464    /// Effect
465    effect: IntervalActionEffect,
466}
467
468impl CSIntervalAction {
469    /// Translate from an [`IntervalTAAction`] to a [`CSIntervalAction`]
470    fn from_interval_action(ctx: &IndexCtx, act: &IntervalTAAction) -> Self {
471        let var = ctx.to_cs_var(act.variable());
472        Self {
473            var,
474            effect: act.effect().clone(),
475        }
476    }
477
478    /// Get the variable the action is applied to
479    pub fn variable(&self) -> &CSVariable {
480        &self.var
481    }
482
483    /// Get the effect of the action
484    pub fn effect(&self) -> &IntervalActionEffect {
485        &self.effect
486    }
487}
488
489/// Rule of a [`ACSThresholdAutomaton`] that can be directly applied to a the
490/// cs types
491#[derive(Debug, Clone, PartialEq, Eq, Hash)]
492pub struct CSRule {
493    /// Unique ID
494    id: u32,
495    /// Source location of the rule
496    source: ACSLocation,
497    /// target location of the rule
498    target: ACSLocation,
499    /// Guard of the rule
500    guard: CSIntervalConstraint,
501    /// Actions of the rule
502    actions: Vec<CSIntervalAction>,
503}
504
505impl CSRule {
506    /// Translate from an [`IntervalTARule`] to a [`CSRule`]
507    fn from_interval_rule(ctx: &IndexCtx, r: &IntervalTARule) -> Self {
508        let source = ctx.to_cs_loc(r.source());
509        let target = ctx.to_cs_loc(r.target());
510        let guard = CSIntervalConstraint::from_interval_constr(ctx, r.guard());
511        let actions = r
512            .actions()
513            .map(|act| CSIntervalAction::from_interval_action(ctx, act))
514            .collect();
515
516        Self {
517            id: r.id(),
518            source,
519            target,
520            guard,
521            actions,
522        }
523    }
524
525    /// Check whether the rule is enabled in the current configuration
526    pub fn is_enabled(&self, cfg: &ACSTAConfig) -> bool {
527        self.guard.is_satisfied(cfg.interval_state()) && cfg.location_state()[self.source()] > 0
528    }
529
530    /// Get the id of the rule
531    pub fn id(&self) -> u32 {
532        self.id
533    }
534
535    /// Get the target of the rule
536    pub fn target(&self) -> &ACSLocation {
537        &self.target
538    }
539
540    /// Get the source location of the rule
541    pub fn source(&self) -> &ACSLocation {
542        &self.source
543    }
544
545    /// Get the actions of the rule
546    pub fn actions(&self) -> impl Iterator<Item = &CSIntervalAction> {
547        self.actions.iter()
548    }
549
550    /// Get the guard of the rule
551    pub fn guard(&self) -> &CSIntervalConstraint {
552        &self.guard
553    }
554}
555
556#[cfg(test)]
557mod mock_objects {
558
559    use taco_threshold_automaton::expressions::{Location, Variable};
560
561    use crate::acs_threshold_automaton::{
562        ACSInterval, ACSLocation, ACSThresholdAutomaton, CSIntervalAction, CSIntervalConstraint,
563        CSRule, CSVariable,
564    };
565
566    impl ACSLocation {
567        pub fn new_mock(l: usize) -> Self {
568            ACSLocation(l)
569        }
570    }
571
572    impl CSVariable {
573        pub fn new_mock(l: usize) -> Self {
574            CSVariable(l)
575        }
576    }
577
578    impl ACSInterval {
579        pub fn new_mock(l: usize) -> Self {
580            ACSInterval(l)
581        }
582    }
583
584    impl CSRule {
585        pub fn new_mock(
586            id: u32,
587            source: ACSLocation,
588            target: ACSLocation,
589            guard: CSIntervalConstraint,
590            actions: Vec<CSIntervalAction>,
591        ) -> Self {
592            Self {
593                id,
594                source,
595                target,
596                guard,
597                actions,
598            }
599        }
600    }
601
602    impl ACSThresholdAutomaton {
603        pub fn to_cs_loc(&self, loc: &Location) -> ACSLocation {
604            self.idx_ctx.to_cs_loc(loc)
605        }
606
607        pub fn to_cs_var(&self, var: &Variable) -> CSVariable {
608            self.idx_ctx.to_cs_var(var)
609        }
610    }
611}
612
613#[cfg(test)]
614mod tests {
615    use std::{
616        collections::{HashMap, HashSet},
617        vec,
618    };
619
620    use taco_interval_ta::{
621        IntervalActionEffect, IntervalConstraint, IntervalTAAction, IntervalTARule,
622        builder::IntervalTABuilder, interval::Interval,
623    };
624    use taco_smt_encoder::SMTSolverBuilder;
625    use taco_threshold_automaton::{
626        ThresholdAutomaton, VariableConstraint,
627        expressions::{
628            BooleanExpression, ComparisonOp, IntegerExpression, IsDeclared, Location, Parameter,
629            Variable,
630        },
631        general_threshold_automaton::{
632            Action,
633            builder::{GeneralThresholdAutomatonBuilder, RuleBuilder},
634        },
635        lia_threshold_automaton::LIAThresholdAutomaton,
636    };
637
638    use crate::acs_threshold_automaton::{
639        ACSInterval, ACSLocation, ACSThresholdAutomaton, CSIntervalAction, CSIntervalConstraint,
640        CSRule, CSVariable,
641        configuration::{ACSIntervalState, ACSTAConfig},
642        index_ctx::IndexCtx,
643    };
644
645    #[test]
646    fn test_from_cs_ta_automaton() {
647        let ta = GeneralThresholdAutomatonBuilder::new("test_ta")
648            .with_variables([Variable::new("x"), Variable::new("y")])
649            .unwrap()
650            .with_locations([
651                Location::new("l1"),
652                Location::new("l2"),
653                Location::new("l3"),
654            ])
655            .unwrap()
656            .with_parameter(Parameter::new("n"))
657            .unwrap()
658            .initialize()
659            .with_resilience_condition(BooleanExpression::ComparisonExpression(
660                Box::new(IntegerExpression::Param(Parameter::new("n"))),
661                ComparisonOp::Gt,
662                Box::new(IntegerExpression::Const(3)),
663            ))
664            .unwrap()
665            .with_initial_location_constraints([
666                BooleanExpression::ComparisonExpression(
667                    Box::new(IntegerExpression::Atom(Location::new("l2"))),
668                    ComparisonOp::Eq,
669                    Box::new(IntegerExpression::Const(0)),
670                ),
671                BooleanExpression::ComparisonExpression(
672                    Box::new(IntegerExpression::Atom(Location::new("l3"))),
673                    ComparisonOp::Eq,
674                    Box::new(IntegerExpression::Const(0)),
675                ),
676            ])
677            .unwrap()
678            .with_initial_variable_constraints([
679                BooleanExpression::ComparisonExpression(
680                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
681                    ComparisonOp::Eq,
682                    Box::new(IntegerExpression::Const(0)),
683                ),
684                BooleanExpression::ComparisonExpression(
685                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
686                    ComparisonOp::Eq,
687                    Box::new(IntegerExpression::Const(0)),
688                ),
689            ])
690            .unwrap()
691            .with_rule(
692                RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
693                    .with_guard(BooleanExpression::ComparisonExpression(
694                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
695                        ComparisonOp::Gt,
696                        Box::new(IntegerExpression::Const(2)),
697                    ))
698                    .with_action(
699                        Action::new(
700                            Variable::new("x"),
701                            IntegerExpression::Const(1)
702                                + IntegerExpression::Atom(Variable::new("x")),
703                        )
704                        .unwrap(),
705                    )
706                    .build(),
707            )
708            .unwrap()
709            .build();
710        let lia_ta = LIAThresholdAutomaton::try_from(ta).unwrap();
711        let mut interval_tas = IntervalTABuilder::new(lia_ta, SMTSolverBuilder::default(), vec![])
712            .build()
713            .unwrap();
714        let interval_ta = interval_tas.next().unwrap();
715        assert!(interval_tas.next().is_none());
716        let ta = ACSThresholdAutomaton::from(interval_ta);
717
718        assert!(ta.is_declared(&Parameter::new("n")));
719        assert!(ta.is_declared(&Location::new("l1")));
720        assert!(ta.is_declared(&Variable::new("y")));
721
722        assert_eq!(
723            ta.initial_location_constraints().collect::<HashSet<_>>(),
724            HashSet::from([
725                &BooleanExpression::ComparisonExpression(
726                    Box::new(IntegerExpression::Atom(Location::new("l2"))),
727                    ComparisonOp::Eq,
728                    Box::new(IntegerExpression::Const(0)),
729                ),
730                &BooleanExpression::ComparisonExpression(
731                    Box::new(IntegerExpression::Atom(Location::new("l3"))),
732                    ComparisonOp::Eq,
733                    Box::new(IntegerExpression::Const(0)),
734                ),
735            ])
736        );
737        assert_eq!(
738            ta.initial_variable_constraints()
739                .map(|c| { c.as_boolean_expr() })
740                .collect::<HashSet<_>>(),
741            HashSet::from([
742                (BooleanExpression::False
743                    | (BooleanExpression::ComparisonExpression(
744                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
745                        ComparisonOp::Geq,
746                        Box::new(IntegerExpression::Const(0)),
747                    ) & BooleanExpression::ComparisonExpression(
748                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
749                        ComparisonOp::Lt,
750                        Box::new(IntegerExpression::Const(1)),
751                    ))),
752                (BooleanExpression::False
753                    | (BooleanExpression::ComparisonExpression(
754                        Box::new(IntegerExpression::Atom(Variable::new("y"))),
755                        ComparisonOp::Geq,
756                        Box::new(IntegerExpression::Const(0)),
757                    ) & BooleanExpression::ComparisonExpression(
758                        Box::new(IntegerExpression::Atom(Variable::new("y"))),
759                        ComparisonOp::Lt,
760                        Box::new(IntegerExpression::Const(1)),
761                    ))),
762            ])
763        );
764        assert_eq!(
765            ta.resilience_conditions().collect::<HashSet<_>>(),
766            HashSet::from([
767                &BooleanExpression::ComparisonExpression(
768                    Box::new(IntegerExpression::Param(Parameter::new("n"))),
769                    ComparisonOp::Gt,
770                    Box::new(IntegerExpression::Const(3)),
771                ),
772                &BooleanExpression::ComparisonExpression(
773                    Box::new(IntegerExpression::Const(0)),
774                    ComparisonOp::Lt,
775                    Box::new(IntegerExpression::Const(1)),
776                ),
777                &BooleanExpression::ComparisonExpression(
778                    Box::new(IntegerExpression::Const(1)),
779                    ComparisonOp::Lt,
780                    Box::new(IntegerExpression::Const(3)),
781                ),
782            ])
783        );
784
785        assert_eq!(
786            ta.locations().collect::<HashSet<_>>(),
787            HashSet::from([&ACSLocation(0), &ACSLocation(1), &ACSLocation(2)])
788        );
789        assert_eq!(
790            ta.variables().collect::<HashSet<_>>(),
791            HashSet::from([&CSVariable(0), &CSVariable(1)])
792        );
793        assert_eq!(ta.name(), "test_ta");
794        assert_eq!(
795            ta.rules().collect::<HashSet<_>>(),
796            HashSet::from([&CSRule {
797                id: 0,
798                source: ta.idx_ctx.to_cs_loc(&Location::new("l1")),
799                target: ta.idx_ctx.to_cs_loc(&Location::new("l2")),
800                guard: CSIntervalConstraint::VarGuard(
801                    ta.idx_ctx.to_cs_var(&Variable::new("x")),
802                    vec![ACSInterval(2)]
803                ),
804                actions: vec![CSIntervalAction {
805                    var: ta.idx_ctx.to_cs_var(&Variable::new("x")),
806                    effect: IntervalActionEffect::Inc(1)
807                }]
808            }])
809        );
810        assert_eq!(
811            ta.get_rule_by_id(0),
812            Some(
813                &RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
814                    .with_guard(BooleanExpression::ComparisonExpression(
815                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
816                        ComparisonOp::Gt,
817                        Box::new(IntegerExpression::Const(2)),
818                    ))
819                    .with_action(
820                        Action::new(
821                            Variable::new("x"),
822                            IntegerExpression::Const(1)
823                                + IntegerExpression::Atom(Variable::new("x")),
824                        )
825                        .unwrap(),
826                    )
827                    .build()
828            )
829        );
830        assert_eq!(ta.get_rule_by_id(1), None);
831
832        assert_eq!(ta.get_zero_interval(&CSVariable(0)), ACSInterval(0));
833        assert_eq!(ta.get_zero_interval(&CSVariable(1)), ACSInterval(0));
834
835        assert!(ta.is_initial_loc(&ta.idx_ctx.to_cs_loc(&Location::new("l1"))));
836        assert!(!ta.is_initial_loc(&ta.idx_ctx.to_cs_loc(&Location::new("l2"))));
837        assert!(!ta.is_initial_loc(&ta.idx_ctx.to_cs_loc(&Location::new("l3"))));
838
839        assert!(ta.is_initial_interval(&CSVariable(1), &ACSInterval(0)));
840        assert!(ta.is_initial_interval(&CSVariable(0), &ACSInterval(0)));
841        assert!(!ta.is_initial_interval(&CSVariable(0), &ACSInterval(1)));
842        assert!(!ta.is_initial_interval(&CSVariable(1), &ACSInterval(1)));
843
844        assert_eq!(ta.get_zero_interval(&CSVariable(0)), ACSInterval(0));
845        assert_eq!(ta.get_zero_interval(&CSVariable(1)), ACSInterval(0));
846
847        assert_eq!(
848            ta.get_all_intervals(&ta.idx_ctx.to_cs_var(&Variable::new("x")))
849                .collect::<HashSet<_>>(),
850            HashSet::from([&ACSInterval(0), &ACSInterval(1), &ACSInterval(2)])
851        );
852        assert_eq!(
853            ta.get_all_intervals(&ta.idx_ctx.to_cs_var(&Variable::new("y")))
854                .collect::<HashSet<_>>(),
855            HashSet::from([&ACSInterval(0), &ACSInterval(1)])
856        );
857
858        assert_eq!(
859            ta.get_next_interval(&ta.idx_ctx.to_cs_var(&Variable::new("x")), &ACSInterval(2)),
860            None
861        );
862        assert_eq!(
863            ta.get_next_interval(&ta.idx_ctx.to_cs_var(&Variable::new("x")), &ACSInterval(1)),
864            Some(ACSInterval(2))
865        );
866
867        assert_eq!(
868            ta.get_prev_interval(&ta.idx_ctx.to_cs_var(&Variable::new("x")), &ACSInterval(2)),
869            Some(ACSInterval(1))
870        );
871        assert_eq!(
872            ta.get_prev_interval(&ta.idx_ctx.to_cs_var(&Variable::new("x")), &ACSInterval(0)),
873            None,
874        );
875    }
876
877    #[test]
878    fn test_cs_interval_constr_from_interval_constraint() {
879        // Test translation of True constraint
880        let index_ctx = IndexCtx::new_mock(
881            HashMap::new(),
882            HashMap::from([(Variable::new("x"), CSVariable(0))]),
883            vec![HashMap::from([(
884                Interval::new_constant(0, 1),
885                ACSInterval(0),
886            )])],
887        );
888        let ic = IntervalConstraint::True;
889        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
890        assert_eq!(cs_ic, CSIntervalConstraint::True);
891
892        // Test translation of False constraint
893        let ic = IntervalConstraint::False;
894        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
895        assert_eq!(cs_ic, CSIntervalConstraint::False);
896
897        // Test translation of SingleVarIntervalConstr
898        let ic = IntervalConstraint::SingleVarIntervalConstr(
899            Variable::new("x"),
900            vec![Interval::new_constant(0, 1)],
901        );
902        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
903        assert_eq!(
904            cs_ic,
905            CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(0)])
906        );
907
908        // Test translation of Conj
909        let ic = IntervalConstraint::Conj(
910            Box::new(IntervalConstraint::True),
911            Box::new(IntervalConstraint::False),
912        );
913        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
914        assert_eq!(
915            cs_ic,
916            CSIntervalConstraint::Conj(
917                Box::new(CSIntervalConstraint::True),
918                Box::new(CSIntervalConstraint::False)
919            )
920        );
921
922        // Test translation of Disj
923        let ic = IntervalConstraint::Disj(
924            Box::new(IntervalConstraint::False),
925            Box::new(IntervalConstraint::True),
926        );
927        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
928        assert_eq!(
929            cs_ic,
930            CSIntervalConstraint::Disj(
931                Box::new(CSIntervalConstraint::False),
932                Box::new(CSIntervalConstraint::True)
933            )
934        );
935
936        // Test translation of nested constraints
937        let ic = IntervalConstraint::Disj(
938            Box::new(IntervalConstraint::Conj(
939                Box::new(IntervalConstraint::SingleVarIntervalConstr(
940                    Variable::new("x"),
941                    vec![Interval::new_constant(0, 1)],
942                )),
943                Box::new(IntervalConstraint::True),
944            )),
945            Box::new(IntervalConstraint::False),
946        );
947        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
948        assert_eq!(
949            cs_ic,
950            CSIntervalConstraint::Disj(
951                Box::new(CSIntervalConstraint::Conj(
952                    Box::new(CSIntervalConstraint::VarGuard(
953                        CSVariable(0),
954                        vec![ACSInterval(0)]
955                    )),
956                    Box::new(CSIntervalConstraint::True)
957                )),
958                Box::new(CSIntervalConstraint::False)
959            )
960        );
961    }
962
963    #[test]
964    fn test_cs_interval_constraint_is_sat() {
965        let interval_state = ACSIntervalState::new_mock_from_vec(vec![ACSInterval(1)]);
966
967        let ic = CSIntervalConstraint::True;
968        assert!(ic.is_satisfied(&interval_state));
969
970        // Test False constraint
971        let ic = CSIntervalConstraint::False;
972        assert!(!ic.is_satisfied(&interval_state));
973
974        // Test VarGuard with matching interval
975        let ic = CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(1)]);
976        assert!(ic.is_satisfied(&interval_state));
977
978        // Test VarGuard with non-matching interval
979        let ic = CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(2)]);
980        assert!(!ic.is_satisfied(&interval_state));
981
982        // Test Conj (True && True)
983        let ic = CSIntervalConstraint::Conj(
984            Box::new(CSIntervalConstraint::True),
985            Box::new(CSIntervalConstraint::True),
986        );
987        assert!(ic.is_satisfied(&interval_state));
988
989        // Test Conj (True && False)
990        let ic = CSIntervalConstraint::Conj(
991            Box::new(CSIntervalConstraint::True),
992            Box::new(CSIntervalConstraint::False),
993        );
994        assert!(!ic.is_satisfied(&interval_state));
995
996        // Test Disj (False || True)
997        let ic = CSIntervalConstraint::Disj(
998            Box::new(CSIntervalConstraint::False),
999            Box::new(CSIntervalConstraint::True),
1000        );
1001        assert!(ic.is_satisfied(&interval_state));
1002
1003        // Test Disj (False || False)
1004        let ic = CSIntervalConstraint::Disj(
1005            Box::new(CSIntervalConstraint::False),
1006            Box::new(CSIntervalConstraint::False),
1007        );
1008        assert!(!ic.is_satisfied(&interval_state));
1009
1010        // Test nested constraints: (VarGuard(0, [1]) && True) || False
1011        let ic = CSIntervalConstraint::Disj(
1012            Box::new(CSIntervalConstraint::Conj(
1013                Box::new(CSIntervalConstraint::VarGuard(
1014                    CSVariable(0),
1015                    vec![ACSInterval(1)],
1016                )),
1017                Box::new(CSIntervalConstraint::True),
1018            )),
1019            Box::new(CSIntervalConstraint::False),
1020        );
1021        assert!(ic.is_satisfied(&interval_state));
1022
1023        // Test nested constraints: (VarGuard(0, [2]) && True) || False
1024        let ic = CSIntervalConstraint::Disj(
1025            Box::new(CSIntervalConstraint::Conj(
1026                Box::new(CSIntervalConstraint::VarGuard(
1027                    CSVariable(0),
1028                    vec![ACSInterval(2)],
1029                )),
1030                Box::new(CSIntervalConstraint::True),
1031            )),
1032            Box::new(CSIntervalConstraint::False),
1033        );
1034        assert!(!ic.is_satisfied(&interval_state));
1035    }
1036
1037    #[test]
1038    fn test_cs_interval_action_from_interval_action() {
1039        let index_ctx = IndexCtx::new_mock(
1040            HashMap::new(),
1041            HashMap::from([(Variable::new("x"), CSVariable(0))]),
1042            vec![HashMap::new()],
1043        );
1044
1045        // Test with Inc effect
1046        let interval_action =
1047            IntervalTAAction::new(Variable::new("x"), IntervalActionEffect::Inc(5));
1048
1049        let cs_action = CSIntervalAction::from_interval_action(&index_ctx, &interval_action);
1050        assert_eq!(cs_action.variable(), &CSVariable(0));
1051        assert_eq!(cs_action.effect(), &IntervalActionEffect::Inc(5));
1052
1053        // Test with Reset effect
1054        let interval_action_reset =
1055            IntervalTAAction::new(Variable::new("x"), IntervalActionEffect::Reset);
1056        let cs_action_reset =
1057            CSIntervalAction::from_interval_action(&index_ctx, &interval_action_reset);
1058        assert_eq!(cs_action_reset.variable(), &CSVariable(0));
1059        assert_eq!(cs_action_reset.effect(), &IntervalActionEffect::Reset);
1060
1061        // Test with Dec effect
1062        let interval_action_dec =
1063            IntervalTAAction::new(Variable::new("x"), IntervalActionEffect::Dec(2));
1064        let cs_action_dec =
1065            CSIntervalAction::from_interval_action(&index_ctx, &interval_action_dec);
1066        assert_eq!(cs_action_dec.variable(), &CSVariable(0));
1067        assert_eq!(cs_action_dec.effect(), &IntervalActionEffect::Dec(2));
1068    }
1069
1070    #[test]
1071    fn test_getters_csrule() {
1072        let rule = CSRule {
1073            id: 0,
1074            source: ACSLocation(1),
1075            target: ACSLocation(2),
1076            guard: CSIntervalConstraint::True,
1077            actions: vec![CSIntervalAction {
1078                var: CSVariable(0),
1079                effect: IntervalActionEffect::Inc(43),
1080            }],
1081        };
1082
1083        assert_eq!(rule.id(), 0);
1084        assert_eq!(rule.target(), &ACSLocation(2));
1085        assert_eq!(rule.source(), &ACSLocation(1));
1086        assert_eq!(
1087            rule.actions().collect::<Vec<_>>(),
1088            vec![&CSIntervalAction {
1089                var: CSVariable(0),
1090                effect: IntervalActionEffect::Inc(43),
1091            }]
1092        );
1093        assert_eq!(rule.guard(), &CSIntervalConstraint::True);
1094    }
1095
1096    #[test]
1097    fn test_csrule_is_enabled() {
1098        let rule = CSRule {
1099            id: 0,
1100            source: ACSLocation(1),
1101            target: ACSLocation(2),
1102            guard: CSIntervalConstraint::True,
1103            actions: vec![CSIntervalAction {
1104                var: CSVariable(0),
1105                effect: IntervalActionEffect::Inc(43),
1106            }],
1107        };
1108        let cfg = ACSTAConfig::new_mock_from_vecs(vec![0, 1, 2], vec![ACSInterval(0)]);
1109        assert!(rule.is_enabled(&cfg));
1110
1111        let rule = CSRule {
1112            id: 0,
1113            source: ACSLocation(1),
1114            target: ACSLocation(2),
1115            guard: CSIntervalConstraint::True,
1116            actions: vec![CSIntervalAction {
1117                var: CSVariable(0),
1118                effect: IntervalActionEffect::Inc(43),
1119            }],
1120        };
1121        let cfg = ACSTAConfig::new_mock_from_vecs(vec![0, 0, 2], vec![ACSInterval(0)]);
1122        assert!(!rule.is_enabled(&cfg));
1123
1124        let rule = CSRule {
1125            id: 0,
1126            source: ACSLocation(1),
1127            target: ACSLocation(2),
1128            guard: CSIntervalConstraint::False,
1129            actions: vec![CSIntervalAction {
1130                var: CSVariable(0),
1131                effect: IntervalActionEffect::Inc(43),
1132            }],
1133        };
1134        let cfg = ACSTAConfig::new_mock_from_vecs(vec![2, 2, 2], vec![ACSInterval(0)]);
1135        assert!(!rule.is_enabled(&cfg));
1136
1137        let rule = CSRule {
1138            id: 0,
1139            source: ACSLocation(1),
1140            target: ACSLocation(2),
1141            guard: CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(1)]),
1142            actions: vec![CSIntervalAction {
1143                var: CSVariable(0),
1144                effect: IntervalActionEffect::Inc(43),
1145            }],
1146        };
1147        let cfg = ACSTAConfig::new_mock_from_vecs(vec![2, 2, 2], vec![ACSInterval(1)]);
1148        assert!(rule.is_enabled(&cfg));
1149
1150        let rule = CSRule {
1151            id: 0,
1152            source: ACSLocation(1),
1153            target: ACSLocation(2),
1154            guard: CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(2)]),
1155            actions: vec![CSIntervalAction {
1156                var: CSVariable(0),
1157                effect: IntervalActionEffect::Inc(43),
1158            }],
1159        };
1160        let cfg = ACSTAConfig::new_mock_from_vecs(vec![2, 2, 2], vec![ACSInterval(1)]);
1161        assert!(!rule.is_enabled(&cfg));
1162    }
1163
1164    #[test]
1165    fn test_csrule_from_interval_rule() {
1166        let index_ctx = IndexCtx::new_mock(
1167            HashMap::from([
1168                (Location::new("loc0"), ACSLocation(0)),
1169                (Location::new("loc1"), ACSLocation(1)),
1170            ]),
1171            HashMap::from([(Variable::new("var0"), CSVariable(0))]),
1172            vec![HashMap::from([(
1173                Interval::new_constant(0, 1),
1174                ACSInterval(0),
1175            )])],
1176        );
1177
1178        let interval_rule = IntervalTARule::new(
1179            0,
1180            Location::new("loc0"),
1181            Location::new("loc1"),
1182            IntervalConstraint::SingleVarIntervalConstr(
1183                Variable::new("var0"),
1184                vec![Interval::new_constant(0, 1)],
1185            ),
1186            vec![IntervalTAAction::new(
1187                Variable::new("var0"),
1188                IntervalActionEffect::Inc(1),
1189            )],
1190        );
1191
1192        let expected_rule = CSRule {
1193            id: 0,
1194            source: ACSLocation(0),
1195            target: ACSLocation(1),
1196            guard: CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(0)]),
1197            actions: vec![CSIntervalAction {
1198                var: CSVariable(0),
1199                effect: IntervalActionEffect::Inc(1),
1200            }],
1201        };
1202
1203        assert_eq!(
1204            CSRule::from_interval_rule(&index_ctx, &interval_rule),
1205            expected_rule
1206        )
1207    }
1208}
taco_acs_model_checker/acs_threshold_automaton.rs

taco_acs_model_checker/
acs_threshold_automaton.rs
