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    pub fn is_guard_enabled(&self, is: &ACSIntervalState) -> bool {
531        self.guard.is_satisfied(is)
532    }
533
534    /// Get the id of the rule
535    pub fn id(&self) -> u32 {
536        self.id
537    }
538
539    /// Get the target of the rule
540    pub fn target(&self) -> &ACSLocation {
541        &self.target
542    }
543
544    /// Get the source location of the rule
545    pub fn source(&self) -> &ACSLocation {
546        &self.source
547    }
548
549    /// Get the actions of the rule
550    pub fn actions(&self) -> impl Iterator<Item = &CSIntervalAction> {
551        self.actions.iter()
552    }
553
554    /// Get the guard of the rule
555    pub fn guard(&self) -> &CSIntervalConstraint {
556        &self.guard
557    }
558}
559
560#[cfg(test)]
561mod mock_objects {
562
563    use taco_threshold_automaton::expressions::{Location, Variable};
564
565    use crate::acs_threshold_automaton::{
566        ACSInterval, ACSLocation, ACSThresholdAutomaton, CSIntervalAction, CSIntervalConstraint,
567        CSRule, CSVariable,
568    };
569
570    impl ACSLocation {
571        pub fn new_mock(l: usize) -> Self {
572            ACSLocation(l)
573        }
574    }
575
576    impl CSVariable {
577        pub fn new_mock(l: usize) -> Self {
578            CSVariable(l)
579        }
580    }
581
582    impl ACSInterval {
583        pub fn new_mock(l: usize) -> Self {
584            ACSInterval(l)
585        }
586    }
587
588    impl CSRule {
589        pub fn new_mock(
590            id: u32,
591            source: ACSLocation,
592            target: ACSLocation,
593            guard: CSIntervalConstraint,
594            actions: Vec<CSIntervalAction>,
595        ) -> Self {
596            Self {
597                id,
598                source,
599                target,
600                guard,
601                actions,
602            }
603        }
604    }
605
606    impl ACSThresholdAutomaton {
607        pub fn to_cs_loc(&self, loc: &Location) -> ACSLocation {
608            self.idx_ctx.to_cs_loc(loc)
609        }
610
611        pub fn to_cs_var(&self, var: &Variable) -> CSVariable {
612            self.idx_ctx.to_cs_var(var)
613        }
614    }
615}
616
617#[cfg(test)]
618mod tests {
619    use std::{
620        collections::{HashMap, HashSet},
621        vec,
622    };
623
624    use taco_interval_ta::{
625        IntervalActionEffect, IntervalConstraint, IntervalTAAction, IntervalTARule,
626        builder::IntervalTABuilder, interval::Interval,
627    };
628    use taco_smt_encoder::SMTSolverBuilder;
629    use taco_threshold_automaton::{
630        ThresholdAutomaton, VariableConstraint,
631        expressions::{
632            BooleanExpression, ComparisonOp, IntegerExpression, IsDeclared, Location, Parameter,
633            Variable,
634        },
635        general_threshold_automaton::{
636            Action,
637            builder::{GeneralThresholdAutomatonBuilder, RuleBuilder},
638        },
639        lia_threshold_automaton::LIAThresholdAutomaton,
640    };
641
642    use crate::acs_threshold_automaton::{
643        ACSInterval, ACSLocation, ACSThresholdAutomaton, CSIntervalAction, CSIntervalConstraint,
644        CSRule, CSVariable,
645        configuration::{ACSIntervalState, ACSTAConfig},
646        index_ctx::IndexCtx,
647    };
648
649    #[test]
650    fn test_from_cs_ta_automaton() {
651        let ta = GeneralThresholdAutomatonBuilder::new("test_ta")
652            .with_variables([Variable::new("x"), Variable::new("y")])
653            .unwrap()
654            .with_locations([
655                Location::new("l1"),
656                Location::new("l2"),
657                Location::new("l3"),
658            ])
659            .unwrap()
660            .with_parameter(Parameter::new("n"))
661            .unwrap()
662            .initialize()
663            .with_resilience_condition(BooleanExpression::ComparisonExpression(
664                Box::new(IntegerExpression::Param(Parameter::new("n"))),
665                ComparisonOp::Gt,
666                Box::new(IntegerExpression::Const(3)),
667            ))
668            .unwrap()
669            .with_initial_location_constraints([
670                BooleanExpression::ComparisonExpression(
671                    Box::new(IntegerExpression::Atom(Location::new("l2"))),
672                    ComparisonOp::Eq,
673                    Box::new(IntegerExpression::Const(0)),
674                ),
675                BooleanExpression::ComparisonExpression(
676                    Box::new(IntegerExpression::Atom(Location::new("l3"))),
677                    ComparisonOp::Eq,
678                    Box::new(IntegerExpression::Const(0)),
679                ),
680            ])
681            .unwrap()
682            .with_initial_variable_constraints([
683                BooleanExpression::ComparisonExpression(
684                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
685                    ComparisonOp::Eq,
686                    Box::new(IntegerExpression::Const(0)),
687                ),
688                BooleanExpression::ComparisonExpression(
689                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
690                    ComparisonOp::Eq,
691                    Box::new(IntegerExpression::Const(0)),
692                ),
693            ])
694            .unwrap()
695            .with_rule(
696                RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
697                    .with_guard(BooleanExpression::ComparisonExpression(
698                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
699                        ComparisonOp::Gt,
700                        Box::new(IntegerExpression::Const(2)),
701                    ))
702                    .with_action(
703                        Action::new(
704                            Variable::new("x"),
705                            IntegerExpression::Const(1)
706                                + IntegerExpression::Atom(Variable::new("x")),
707                        )
708                        .unwrap(),
709                    )
710                    .build(),
711            )
712            .unwrap()
713            .build();
714        let lia_ta = LIAThresholdAutomaton::try_from(ta).unwrap();
715        let mut interval_tas = IntervalTABuilder::new(lia_ta, SMTSolverBuilder::default(), vec![])
716            .build()
717            .unwrap();
718        let interval_ta = interval_tas.next().unwrap();
719        assert!(interval_tas.next().is_none());
720        let ta = ACSThresholdAutomaton::from(interval_ta);
721
722        assert!(ta.is_declared(&Parameter::new("n")));
723        assert!(ta.is_declared(&Location::new("l1")));
724        assert!(ta.is_declared(&Variable::new("y")));
725
726        assert_eq!(
727            ta.initial_location_constraints().collect::<HashSet<_>>(),
728            HashSet::from([
729                &BooleanExpression::ComparisonExpression(
730                    Box::new(IntegerExpression::Atom(Location::new("l2"))),
731                    ComparisonOp::Eq,
732                    Box::new(IntegerExpression::Const(0)),
733                ),
734                &BooleanExpression::ComparisonExpression(
735                    Box::new(IntegerExpression::Atom(Location::new("l3"))),
736                    ComparisonOp::Eq,
737                    Box::new(IntegerExpression::Const(0)),
738                ),
739            ])
740        );
741        assert_eq!(
742            ta.initial_variable_constraints()
743                .map(|c| { c.as_boolean_expr() })
744                .collect::<HashSet<_>>(),
745            HashSet::from([
746                (BooleanExpression::False
747                    | (BooleanExpression::ComparisonExpression(
748                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
749                        ComparisonOp::Geq,
750                        Box::new(IntegerExpression::Const(0)),
751                    ) & BooleanExpression::ComparisonExpression(
752                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
753                        ComparisonOp::Lt,
754                        Box::new(IntegerExpression::Const(1)),
755                    ))),
756                (BooleanExpression::False
757                    | (BooleanExpression::ComparisonExpression(
758                        Box::new(IntegerExpression::Atom(Variable::new("y"))),
759                        ComparisonOp::Geq,
760                        Box::new(IntegerExpression::Const(0)),
761                    ) & BooleanExpression::ComparisonExpression(
762                        Box::new(IntegerExpression::Atom(Variable::new("y"))),
763                        ComparisonOp::Lt,
764                        Box::new(IntegerExpression::Const(1)),
765                    ))),
766            ])
767        );
768        assert_eq!(
769            ta.resilience_conditions().collect::<HashSet<_>>(),
770            HashSet::from([
771                &BooleanExpression::ComparisonExpression(
772                    Box::new(IntegerExpression::Param(Parameter::new("n"))),
773                    ComparisonOp::Gt,
774                    Box::new(IntegerExpression::Const(3)),
775                ),
776                &BooleanExpression::ComparisonExpression(
777                    Box::new(IntegerExpression::Const(0)),
778                    ComparisonOp::Lt,
779                    Box::new(IntegerExpression::Const(1)),
780                ),
781                &BooleanExpression::ComparisonExpression(
782                    Box::new(IntegerExpression::Const(1)),
783                    ComparisonOp::Lt,
784                    Box::new(IntegerExpression::Const(2)),
785                ),
786            ])
787        );
788
789        assert_eq!(
790            ta.locations().collect::<HashSet<_>>(),
791            HashSet::from([&ACSLocation(0), &ACSLocation(1), &ACSLocation(2)])
792        );
793        assert_eq!(
794            ta.variables().collect::<HashSet<_>>(),
795            HashSet::from([&CSVariable(0), &CSVariable(1)])
796        );
797        assert_eq!(ta.name(), "test_ta");
798        assert_eq!(
799            ta.rules().collect::<HashSet<_>>(),
800            HashSet::from([&CSRule {
801                id: 0,
802                source: ta.idx_ctx.to_cs_loc(&Location::new("l1")),
803                target: ta.idx_ctx.to_cs_loc(&Location::new("l2")),
804                guard: CSIntervalConstraint::VarGuard(
805                    ta.idx_ctx.to_cs_var(&Variable::new("x")),
806                    vec![ACSInterval(3)]
807                ),
808                actions: vec![CSIntervalAction {
809                    var: ta.idx_ctx.to_cs_var(&Variable::new("x")),
810                    effect: IntervalActionEffect::Inc(1)
811                }]
812            }])
813        );
814        assert_eq!(
815            ta.get_rule_by_id(0),
816            Some(
817                &RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
818                    .with_guard(BooleanExpression::ComparisonExpression(
819                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
820                        ComparisonOp::Gt,
821                        Box::new(IntegerExpression::Const(2)),
822                    ))
823                    .with_action(
824                        Action::new(
825                            Variable::new("x"),
826                            IntegerExpression::Const(1)
827                                + IntegerExpression::Atom(Variable::new("x")),
828                        )
829                        .unwrap(),
830                    )
831                    .build()
832            )
833        );
834        assert_eq!(ta.get_rule_by_id(1), None);
835
836        assert_eq!(ta.get_zero_interval(&CSVariable(0)), ACSInterval(0));
837        assert_eq!(ta.get_zero_interval(&CSVariable(1)), ACSInterval(0));
838
839        assert!(ta.is_initial_loc(&ta.idx_ctx.to_cs_loc(&Location::new("l1"))));
840        assert!(!ta.is_initial_loc(&ta.idx_ctx.to_cs_loc(&Location::new("l2"))));
841        assert!(!ta.is_initial_loc(&ta.idx_ctx.to_cs_loc(&Location::new("l3"))));
842
843        assert!(ta.is_initial_interval(&CSVariable(1), &ACSInterval(0)));
844        assert!(ta.is_initial_interval(&CSVariable(0), &ACSInterval(0)));
845        assert!(!ta.is_initial_interval(&CSVariable(0), &ACSInterval(1)));
846        assert!(!ta.is_initial_interval(&CSVariable(1), &ACSInterval(1)));
847
848        assert_eq!(ta.get_zero_interval(&CSVariable(0)), ACSInterval(0));
849        assert_eq!(ta.get_zero_interval(&CSVariable(1)), ACSInterval(0));
850
851        assert_eq!(
852            ta.get_all_intervals(&ta.idx_ctx.to_cs_var(&Variable::new("x")))
853                .collect::<HashSet<_>>(),
854            HashSet::from([
855                &ACSInterval(0),
856                &ACSInterval(1),
857                &ACSInterval(2),
858                &ACSInterval(3)
859            ])
860        );
861        assert_eq!(
862            ta.get_all_intervals(&ta.idx_ctx.to_cs_var(&Variable::new("y")))
863                .collect::<HashSet<_>>(),
864            HashSet::from([&ACSInterval(0), &ACSInterval(1)])
865        );
866
867        assert_eq!(
868            ta.get_next_interval(&ta.idx_ctx.to_cs_var(&Variable::new("x")), &ACSInterval(3)),
869            None
870        );
871        assert_eq!(
872            ta.get_next_interval(&ta.idx_ctx.to_cs_var(&Variable::new("x")), &ACSInterval(1)),
873            Some(ACSInterval(2))
874        );
875
876        assert_eq!(
877            ta.get_prev_interval(&ta.idx_ctx.to_cs_var(&Variable::new("x")), &ACSInterval(2)),
878            Some(ACSInterval(1))
879        );
880        assert_eq!(
881            ta.get_prev_interval(&ta.idx_ctx.to_cs_var(&Variable::new("x")), &ACSInterval(0)),
882            None,
883        );
884    }
885
886    #[test]
887    fn test_cs_interval_constr_from_interval_constraint() {
888        // Test translation of True constraint
889        let index_ctx = IndexCtx::new_mock(
890            HashMap::new(),
891            HashMap::from([(Variable::new("x"), CSVariable(0))]),
892            vec![HashMap::from([(
893                Interval::new_constant(0, 1),
894                ACSInterval(0),
895            )])],
896        );
897        let ic = IntervalConstraint::True;
898        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
899        assert_eq!(cs_ic, CSIntervalConstraint::True);
900
901        // Test translation of False constraint
902        let ic = IntervalConstraint::False;
903        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
904        assert_eq!(cs_ic, CSIntervalConstraint::False);
905
906        // Test translation of SingleVarIntervalConstr
907        let ic = IntervalConstraint::SingleVarIntervalConstr(
908            Variable::new("x"),
909            vec![Interval::new_constant(0, 1)],
910        );
911        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
912        assert_eq!(
913            cs_ic,
914            CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(0)])
915        );
916
917        // Test translation of Conj
918        let ic = IntervalConstraint::Conj(
919            Box::new(IntervalConstraint::True),
920            Box::new(IntervalConstraint::False),
921        );
922        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
923        assert_eq!(
924            cs_ic,
925            CSIntervalConstraint::Conj(
926                Box::new(CSIntervalConstraint::True),
927                Box::new(CSIntervalConstraint::False)
928            )
929        );
930
931        // Test translation of Disj
932        let ic = IntervalConstraint::Disj(
933            Box::new(IntervalConstraint::False),
934            Box::new(IntervalConstraint::True),
935        );
936        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
937        assert_eq!(
938            cs_ic,
939            CSIntervalConstraint::Disj(
940                Box::new(CSIntervalConstraint::False),
941                Box::new(CSIntervalConstraint::True)
942            )
943        );
944
945        // Test translation of nested constraints
946        let ic = IntervalConstraint::Disj(
947            Box::new(IntervalConstraint::Conj(
948                Box::new(IntervalConstraint::SingleVarIntervalConstr(
949                    Variable::new("x"),
950                    vec![Interval::new_constant(0, 1)],
951                )),
952                Box::new(IntervalConstraint::True),
953            )),
954            Box::new(IntervalConstraint::False),
955        );
956        let cs_ic = CSIntervalConstraint::from_interval_constr(&index_ctx, &ic);
957        assert_eq!(
958            cs_ic,
959            CSIntervalConstraint::Disj(
960                Box::new(CSIntervalConstraint::Conj(
961                    Box::new(CSIntervalConstraint::VarGuard(
962                        CSVariable(0),
963                        vec![ACSInterval(0)]
964                    )),
965                    Box::new(CSIntervalConstraint::True)
966                )),
967                Box::new(CSIntervalConstraint::False)
968            )
969        );
970    }
971
972    #[test]
973    fn test_cs_interval_constraint_is_sat() {
974        let interval_state = ACSIntervalState::new_mock_from_vec(vec![ACSInterval(1)]);
975
976        let ic = CSIntervalConstraint::True;
977        assert!(ic.is_satisfied(&interval_state));
978
979        // Test False constraint
980        let ic = CSIntervalConstraint::False;
981        assert!(!ic.is_satisfied(&interval_state));
982
983        // Test VarGuard with matching interval
984        let ic = CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(1)]);
985        assert!(ic.is_satisfied(&interval_state));
986
987        // Test VarGuard with non-matching interval
988        let ic = CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(2)]);
989        assert!(!ic.is_satisfied(&interval_state));
990
991        // Test Conj (True && True)
992        let ic = CSIntervalConstraint::Conj(
993            Box::new(CSIntervalConstraint::True),
994            Box::new(CSIntervalConstraint::True),
995        );
996        assert!(ic.is_satisfied(&interval_state));
997
998        // Test Conj (True && False)
999        let ic = CSIntervalConstraint::Conj(
1000            Box::new(CSIntervalConstraint::True),
1001            Box::new(CSIntervalConstraint::False),
1002        );
1003        assert!(!ic.is_satisfied(&interval_state));
1004
1005        // Test Disj (False || True)
1006        let ic = CSIntervalConstraint::Disj(
1007            Box::new(CSIntervalConstraint::False),
1008            Box::new(CSIntervalConstraint::True),
1009        );
1010        assert!(ic.is_satisfied(&interval_state));
1011
1012        // Test Disj (False || False)
1013        let ic = CSIntervalConstraint::Disj(
1014            Box::new(CSIntervalConstraint::False),
1015            Box::new(CSIntervalConstraint::False),
1016        );
1017        assert!(!ic.is_satisfied(&interval_state));
1018
1019        // Test nested constraints: (VarGuard(0, [1]) && True) || False
1020        let ic = CSIntervalConstraint::Disj(
1021            Box::new(CSIntervalConstraint::Conj(
1022                Box::new(CSIntervalConstraint::VarGuard(
1023                    CSVariable(0),
1024                    vec![ACSInterval(1)],
1025                )),
1026                Box::new(CSIntervalConstraint::True),
1027            )),
1028            Box::new(CSIntervalConstraint::False),
1029        );
1030        assert!(ic.is_satisfied(&interval_state));
1031
1032        // Test nested constraints: (VarGuard(0, [2]) && True) || False
1033        let ic = CSIntervalConstraint::Disj(
1034            Box::new(CSIntervalConstraint::Conj(
1035                Box::new(CSIntervalConstraint::VarGuard(
1036                    CSVariable(0),
1037                    vec![ACSInterval(2)],
1038                )),
1039                Box::new(CSIntervalConstraint::True),
1040            )),
1041            Box::new(CSIntervalConstraint::False),
1042        );
1043        assert!(!ic.is_satisfied(&interval_state));
1044    }
1045
1046    #[test]
1047    fn test_cs_interval_action_from_interval_action() {
1048        let index_ctx = IndexCtx::new_mock(
1049            HashMap::new(),
1050            HashMap::from([(Variable::new("x"), CSVariable(0))]),
1051            vec![HashMap::new()],
1052        );
1053
1054        // Test with Inc effect
1055        let interval_action =
1056            IntervalTAAction::new(Variable::new("x"), IntervalActionEffect::Inc(5));
1057
1058        let cs_action = CSIntervalAction::from_interval_action(&index_ctx, &interval_action);
1059        assert_eq!(cs_action.variable(), &CSVariable(0));
1060        assert_eq!(cs_action.effect(), &IntervalActionEffect::Inc(5));
1061
1062        // Test with Reset effect
1063        let interval_action_reset =
1064            IntervalTAAction::new(Variable::new("x"), IntervalActionEffect::Reset);
1065        let cs_action_reset =
1066            CSIntervalAction::from_interval_action(&index_ctx, &interval_action_reset);
1067        assert_eq!(cs_action_reset.variable(), &CSVariable(0));
1068        assert_eq!(cs_action_reset.effect(), &IntervalActionEffect::Reset);
1069
1070        // Test with Dec effect
1071        let interval_action_dec =
1072            IntervalTAAction::new(Variable::new("x"), IntervalActionEffect::Dec(2));
1073        let cs_action_dec =
1074            CSIntervalAction::from_interval_action(&index_ctx, &interval_action_dec);
1075        assert_eq!(cs_action_dec.variable(), &CSVariable(0));
1076        assert_eq!(cs_action_dec.effect(), &IntervalActionEffect::Dec(2));
1077    }
1078
1079    #[test]
1080    fn test_getters_csrule() {
1081        let rule = CSRule {
1082            id: 0,
1083            source: ACSLocation(1),
1084            target: ACSLocation(2),
1085            guard: CSIntervalConstraint::True,
1086            actions: vec![CSIntervalAction {
1087                var: CSVariable(0),
1088                effect: IntervalActionEffect::Inc(43),
1089            }],
1090        };
1091
1092        assert_eq!(rule.id(), 0);
1093        assert_eq!(rule.target(), &ACSLocation(2));
1094        assert_eq!(rule.source(), &ACSLocation(1));
1095        assert_eq!(
1096            rule.actions().collect::<Vec<_>>(),
1097            vec![&CSIntervalAction {
1098                var: CSVariable(0),
1099                effect: IntervalActionEffect::Inc(43),
1100            }]
1101        );
1102        assert_eq!(rule.guard(), &CSIntervalConstraint::True);
1103    }
1104
1105    #[test]
1106    fn test_csrule_is_enabled() {
1107        let rule = CSRule {
1108            id: 0,
1109            source: ACSLocation(1),
1110            target: ACSLocation(2),
1111            guard: CSIntervalConstraint::True,
1112            actions: vec![CSIntervalAction {
1113                var: CSVariable(0),
1114                effect: IntervalActionEffect::Inc(43),
1115            }],
1116        };
1117        let cfg = ACSTAConfig::new_mock_from_vecs(vec![0, 1, 2], vec![ACSInterval(0)]);
1118        assert!(rule.is_enabled(&cfg));
1119
1120        let rule = CSRule {
1121            id: 0,
1122            source: ACSLocation(1),
1123            target: ACSLocation(2),
1124            guard: CSIntervalConstraint::True,
1125            actions: vec![CSIntervalAction {
1126                var: CSVariable(0),
1127                effect: IntervalActionEffect::Inc(43),
1128            }],
1129        };
1130        let cfg = ACSTAConfig::new_mock_from_vecs(vec![0, 0, 2], vec![ACSInterval(0)]);
1131        assert!(!rule.is_enabled(&cfg));
1132
1133        let rule = CSRule {
1134            id: 0,
1135            source: ACSLocation(1),
1136            target: ACSLocation(2),
1137            guard: CSIntervalConstraint::False,
1138            actions: vec![CSIntervalAction {
1139                var: CSVariable(0),
1140                effect: IntervalActionEffect::Inc(43),
1141            }],
1142        };
1143        let cfg = ACSTAConfig::new_mock_from_vecs(vec![2, 2, 2], vec![ACSInterval(0)]);
1144        assert!(!rule.is_enabled(&cfg));
1145
1146        let rule = CSRule {
1147            id: 0,
1148            source: ACSLocation(1),
1149            target: ACSLocation(2),
1150            guard: CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(1)]),
1151            actions: vec![CSIntervalAction {
1152                var: CSVariable(0),
1153                effect: IntervalActionEffect::Inc(43),
1154            }],
1155        };
1156        let cfg = ACSTAConfig::new_mock_from_vecs(vec![2, 2, 2], vec![ACSInterval(1)]);
1157        assert!(rule.is_enabled(&cfg));
1158
1159        let rule = CSRule {
1160            id: 0,
1161            source: ACSLocation(1),
1162            target: ACSLocation(2),
1163            guard: CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(2)]),
1164            actions: vec![CSIntervalAction {
1165                var: CSVariable(0),
1166                effect: IntervalActionEffect::Inc(43),
1167            }],
1168        };
1169        let cfg = ACSTAConfig::new_mock_from_vecs(vec![2, 2, 2], vec![ACSInterval(1)]);
1170        assert!(!rule.is_enabled(&cfg));
1171    }
1172
1173    #[test]
1174    fn test_csrule_from_interval_rule() {
1175        let index_ctx = IndexCtx::new_mock(
1176            HashMap::from([
1177                (Location::new("loc0"), ACSLocation(0)),
1178                (Location::new("loc1"), ACSLocation(1)),
1179            ]),
1180            HashMap::from([(Variable::new("var0"), CSVariable(0))]),
1181            vec![HashMap::from([(
1182                Interval::new_constant(0, 1),
1183                ACSInterval(0),
1184            )])],
1185        );
1186
1187        let interval_rule = IntervalTARule::new(
1188            0,
1189            Location::new("loc0"),
1190            Location::new("loc1"),
1191            IntervalConstraint::SingleVarIntervalConstr(
1192                Variable::new("var0"),
1193                vec![Interval::new_constant(0, 1)],
1194            ),
1195            vec![IntervalTAAction::new(
1196                Variable::new("var0"),
1197                IntervalActionEffect::Inc(1),
1198            )],
1199        );
1200
1201        let expected_rule = CSRule {
1202            id: 0,
1203            source: ACSLocation(0),
1204            target: ACSLocation(1),
1205            guard: CSIntervalConstraint::VarGuard(CSVariable(0), vec![ACSInterval(0)]),
1206            actions: vec![CSIntervalAction {
1207                var: CSVariable(0),
1208                effect: IntervalActionEffect::Inc(1),
1209            }],
1210        };
1211
1212        assert_eq!(
1213            CSRule::from_interval_rule(&index_ctx, &interval_rule),
1214            expected_rule
1215        )
1216    }
1217}
taco_acs_model_checker/acs_threshold_automaton.rs

taco_acs_model_checker/
acs_threshold_automaton.rs
