taco_interval_ta/
builder.rs

1//! Builder for interval threshold automaton
2//!
3//! This module provides a builder for generating interval threshold automata
4//! from linear integer arithmetic threshold automata. In the process, the
5//! builder also generates all possible interval orders for the given threshold
6//! automaton.
7
8use taco_smt_encoder::SMTSolverBuilder;
9use taco_threshold_automaton::{
10    RuleDefinition, ThresholdAutomaton,
11    lia_threshold_automaton::{LIAThresholdAutomaton, LIAVariableConstraint},
12};
13
14use crate::{
15    IntervalConstraint, IntervalTARule, IntervalTATransformationError, IntervalThresholdAutomaton,
16    builder::static_interval_order::{StaticIntervalOrder, StaticIntervalOrderBuilder},
17    interval::{IntervalBoundary, IntervalOrder},
18};
19
20use log::error;
21
22pub mod static_interval_order;
23
24/// Builder for generating interval threshold automata
25///
26/// This builder takes a linear integer arithmetic threshold automaton and
27/// derives all valid interval threshold automata.
28///
29/// An interval threshold automaton is a threshold automaton where the guards
30/// are abstracted to intervals and the order of the intervals is defined.
31///
32/// The builder generates all possible interval orders for the given threshold
33/// linear integer arithmetic automaton, and for each interval order, it
34/// generates the corresponding interval threshold automaton.
35pub struct IntervalTABuilder {
36    /// Underlying threshold automaton
37    lia_ta: LIAThresholdAutomaton,
38    /// Solver builder for generating the interval orders
39    solver_builder: SMTSolverBuilder,
40    /// Additional variable constraints derived from the target specification
41    target_constr: Vec<LIAVariableConstraint>,
42}
43
44impl IntervalTABuilder {
45    /// Create a new interval threshold automaton builder from a linear integer
46    /// arithmetic threshold automaton
47    ///
48    /// The solver builder is used to generate the interval orders.
49    pub fn new(
50        lia_ta: LIAThresholdAutomaton,
51        solver_builder: SMTSolverBuilder,
52        target_constr: Vec<LIAVariableConstraint>,
53    ) -> Self {
54        Self {
55            lia_ta,
56            solver_builder,
57            target_constr,
58        }
59    }
60
61    /// Generate all possible orders on the intervals and derive the interval
62    /// automaton for every possible order
63    pub fn build(
64        self,
65    ) -> Result<impl Iterator<Item = IntervalThresholdAutomaton>, IntervalTATransformationError>
66    {
67        let order_builder = StaticIntervalOrderBuilder::new(&self.lia_ta, self.solver_builder);
68
69        let order_builder =
70            self.lia_ta
71                .initial_variable_constraints()
72                .try_fold(order_builder, |acc, constr| {
73                    Self::discover_interval_boundaries_in_lia_variable_constraint(constr, acc)
74                        .ok_or_else(|| {
75                            IntervalTATransformationError::ComparisonGuardFoundInitialVariableConstraint(Box::new(constr.clone()))
76                        })
77                })?;
78
79        let order_builder = self.lia_ta.rules().try_fold(order_builder, |acc, rule| {
80            Self::discover_interval_boundaries_in_lia_variable_constraint(rule.guard(), acc)
81                .ok_or_else(|| {
82                    IntervalTATransformationError::ComparisonGuardFoundRule(Box::new(rule.clone()))
83                })
84        })?;
85
86        let order_builder =
87            self.target_constr
88                .into_iter()
89                .try_fold(order_builder, |acc, constr| {
90                    Self::discover_interval_boundaries_in_lia_variable_constraint(&constr, acc)
91                        .ok_or_else(|| {
92                            IntervalTATransformationError::ComparisonGuardFoundVariableTarget(
93                                Box::new(constr.clone()),
94                            )
95                        })
96                })?;
97
98        let orders = order_builder.build();
99
100        Ok(orders.into_iter().map(move |order| {
101            Self::derive_interval_threshold_automaton(self.lia_ta.clone(), order)
102        }))
103    }
104
105    /// Given a fixed order, derive the abstract threshold automaton
106    fn derive_interval_threshold_automaton(
107        lia_ta: LIAThresholdAutomaton,
108        interval_order: StaticIntervalOrder,
109    ) -> IntervalThresholdAutomaton {
110        let rules = lia_ta
111            .rules()
112            .map(|rule| IntervalTARule::from_lia_rule(rule, &interval_order))
113            .collect::<Vec<_>>();
114
115        let initial_variable_constraints = lia_ta
116            .initial_variable_constraints()
117            .map(|constr| {
118                IntervalConstraint::from_lia_constr(constr, &interval_order)
119                    .expect("Failed to derive interval constraint from initial constraint")
120            })
121            .collect();
122
123        let order_expr = interval_order.order_to_boolean_expr();
124        IntervalThresholdAutomaton {
125            lia_ta,
126            rules,
127            initial_variable_constraints,
128            order: interval_order,
129            order_expr,
130        }
131    }
132
133    /// Extract variable intervals from a rule guard of the threshold automaton
134    ///
135    /// Returns None if a comparison guard has been discovered
136    fn discover_interval_boundaries_in_lia_variable_constraint(
137        guard: &LIAVariableConstraint,
138        order_builder: StaticIntervalOrderBuilder,
139    ) -> Option<StaticIntervalOrderBuilder> {
140        match guard {
141            LIAVariableConstraint::True | LIAVariableConstraint::False => Some(order_builder),
142            LIAVariableConstraint::ComparisonConstraint(_guard) => {
143                error!("Comparison Guard found. Guard {guard}");
144                None
145            }
146            LIAVariableConstraint::BinaryGuard(lhs, _op, rhs) => {
147                // Recursively extract interval boundaries from the left and right hand side
148                let order_builder = Self::discover_interval_boundaries_in_lia_variable_constraint(
149                    lhs,
150                    order_builder,
151                )?;
152                Self::discover_interval_boundaries_in_lia_variable_constraint(rhs, order_builder)
153            }
154            LIAVariableConstraint::SingleVarConstraint(thr_guard) => {
155                let interval_boundary = IntervalBoundary::from_threshold_constraint(
156                    thr_guard.get_threshold_constraint(),
157                );
158
159                // We need to add the exact interval into the order to correctly
160                // determine when constraints are satisfied
161                let exact_required = thr_guard
162                    .get_threshold_constraint()
163                    .get_op()
164                    .needs_exact_interval();
165
166                Some(order_builder.add_single_variable_interval(
167                    thr_guard.get_atom(),
168                    &interval_boundary,
169                    exact_required,
170                ))
171            }
172            LIAVariableConstraint::SumVarConstraint(thr_guard) => {
173                let interval_boundary = IntervalBoundary::from_threshold_constraint(
174                    thr_guard.get_threshold_constraint(),
175                );
176
177                let exact_required = thr_guard
178                    .get_threshold_constraint()
179                    .get_op()
180                    .needs_exact_interval();
181
182                Some(order_builder.add_multi_variable_interval(
183                    thr_guard.get_atoms(),
184                    &interval_boundary,
185                    exact_required,
186                ))
187            }
188        }
189    }
190}
191
192#[cfg(test)]
193mod test {
194    use taco_smt_encoder::SMTSolverBuilder;
195    use taco_threshold_automaton::{
196        expressions::{
197            BooleanExpression, ComparisonOp, IntegerExpression, Location, Parameter, Variable,
198        },
199        general_threshold_automaton::{
200            Action,
201            builder::{GeneralThresholdAutomatonBuilder, RuleBuilder},
202        },
203        lia_threshold_automaton::{LIARule, LIAThresholdAutomaton, LIAVariableConstraint},
204    };
205
206    use crate::{IntervalTATransformationError, builder::IntervalTABuilder};
207
208    #[test]
209    fn test_builder_for_lia_ta_err_on_comparison_constr_target() {
210        let var = Variable::new("x");
211
212        let rc = BooleanExpression::ComparisonExpression(
213            Box::new(IntegerExpression::Param(Parameter::new("n"))),
214            ComparisonOp::Gt,
215            Box::new(IntegerExpression::Const(3)),
216        );
217
218        let ta = GeneralThresholdAutomatonBuilder::new("test_ta")
219            .with_variables([var.clone(), Variable::new("y")])
220            .unwrap()
221            .with_locations([Location::new("l1"), Location::new("l2")])
222            .unwrap()
223            .with_parameter(Parameter::new("n"))
224            .unwrap()
225            .initialize()
226            .with_resilience_condition(rc.clone())
227            .unwrap()
228            .with_initial_location_constraint(BooleanExpression::ComparisonExpression(
229                Box::new(IntegerExpression::Atom(Location::new("l1"))),
230                ComparisonOp::Eq,
231                Box::new(IntegerExpression::Const(0)),
232            ))
233            .unwrap()
234            .with_rule(
235                RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
236                    .with_guard(BooleanExpression::ComparisonExpression(
237                        Box::new(IntegerExpression::Atom(var.clone())),
238                        ComparisonOp::Gt,
239                        Box::new(IntegerExpression::Const(2)),
240                    ))
241                    .with_action(
242                        Action::new(
243                            var.clone(),
244                            IntegerExpression::Const(1) + IntegerExpression::Atom(var.clone()),
245                        )
246                        .unwrap(),
247                    )
248                    .build(),
249            )
250            .unwrap()
251            .build();
252
253        let lia_ta = LIAThresholdAutomaton::try_from(ta).unwrap();
254
255        let lia_constr: LIAVariableConstraint = (&BooleanExpression::ComparisonExpression(
256            Box::new(IntegerExpression::Atom(Variable::new("x"))),
257            ComparisonOp::Eq,
258            Box::new(IntegerExpression::Atom(Variable::new("y"))),
259        ))
260            .try_into()
261            .unwrap();
262
263        let interval_tas = IntervalTABuilder::new(
264            lia_ta,
265            SMTSolverBuilder::default(),
266            vec![lia_constr.clone()],
267        )
268        .build();
269
270        assert!(interval_tas.is_err());
271        if let Err(e) = interval_tas {
272            assert_eq!(
273                e,
274                IntervalTATransformationError::ComparisonGuardFoundVariableTarget(Box::new(
275                    lia_constr.clone()
276                ))
277            );
278        }
279    }
280
281    #[test]
282    fn test_builder_for_lia_ta_err_on_comparison_constr_init_loc() {
283        let var = Variable::new("x");
284
285        let rc = BooleanExpression::ComparisonExpression(
286            Box::new(IntegerExpression::Param(Parameter::new("n"))),
287            ComparisonOp::Gt,
288            Box::new(IntegerExpression::Const(3)),
289        );
290
291        let ta = GeneralThresholdAutomatonBuilder::new("test_ta")
292            .with_variables([var.clone(), Variable::new("y")])
293            .unwrap()
294            .with_locations([Location::new("l1"), Location::new("l2")])
295            .unwrap()
296            .with_parameter(Parameter::new("n"))
297            .unwrap()
298            .initialize()
299            .with_resilience_condition(rc.clone())
300            .unwrap()
301            .with_initial_variable_constraint(BooleanExpression::ComparisonExpression(
302                Box::new(IntegerExpression::Atom(Variable::new("x"))),
303                ComparisonOp::Eq,
304                Box::new(IntegerExpression::Atom(Variable::new("y"))),
305            ))
306            .unwrap()
307            .with_rule(
308                RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
309                    .with_guard(BooleanExpression::ComparisonExpression(
310                        Box::new(IntegerExpression::Atom(var.clone())),
311                        ComparisonOp::Gt,
312                        Box::new(IntegerExpression::Const(2)),
313                    ))
314                    .with_action(
315                        Action::new(
316                            var.clone(),
317                            IntegerExpression::Const(1) + IntegerExpression::Atom(var.clone()),
318                        )
319                        .unwrap(),
320                    )
321                    .build(),
322            )
323            .unwrap()
324            .build();
325
326        let lia_ta = LIAThresholdAutomaton::try_from(ta).unwrap();
327
328        let interval_tas =
329            IntervalTABuilder::new(lia_ta, SMTSolverBuilder::default(), vec![]).build();
330
331        let lia_constr: LIAVariableConstraint = (&BooleanExpression::ComparisonExpression(
332            Box::new(IntegerExpression::Atom(Variable::new("x"))),
333            ComparisonOp::Eq,
334            Box::new(IntegerExpression::Atom(Variable::new("y"))),
335        ))
336            .try_into()
337            .unwrap();
338
339        assert!(interval_tas.is_err());
340        if let Err(e) = interval_tas {
341            assert_eq!(
342                e,
343                IntervalTATransformationError::ComparisonGuardFoundInitialVariableConstraint(
344                    Box::new(lia_constr.clone())
345                )
346            );
347        }
348    }
349
350    #[test]
351    fn test_builder_for_lia_ta_err_on_comparison_rule() {
352        let var = Variable::new("x");
353
354        let rc = BooleanExpression::ComparisonExpression(
355            Box::new(IntegerExpression::Param(Parameter::new("n"))),
356            ComparisonOp::Gt,
357            Box::new(IntegerExpression::Const(3)),
358        );
359
360        let ta = GeneralThresholdAutomatonBuilder::new("test_ta")
361            .with_variables([var.clone(), Variable::new("y")])
362            .unwrap()
363            .with_locations([Location::new("l1"), Location::new("l2")])
364            .unwrap()
365            .with_parameter(Parameter::new("n"))
366            .unwrap()
367            .initialize()
368            .with_resilience_condition(rc.clone())
369            .unwrap()
370            .with_initial_location_constraint(BooleanExpression::ComparisonExpression(
371                Box::new(IntegerExpression::Atom(Location::new("l1"))),
372                ComparisonOp::Eq,
373                Box::new(IntegerExpression::Const(0)),
374            ))
375            .unwrap()
376            .with_rule(
377                RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
378                    .with_guard(BooleanExpression::ComparisonExpression(
379                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
380                        ComparisonOp::Eq,
381                        Box::new(IntegerExpression::Atom(Variable::new("y"))),
382                    ))
383                    .with_action(
384                        Action::new(
385                            var.clone(),
386                            IntegerExpression::Const(1) + IntegerExpression::Atom(var.clone()),
387                        )
388                        .unwrap(),
389                    )
390                    .build(),
391            )
392            .unwrap()
393            .build();
394
395        let lia_ta = LIAThresholdAutomaton::try_from(ta).unwrap();
396
397        let interval_tas =
398            IntervalTABuilder::new(lia_ta, SMTSolverBuilder::default(), vec![]).build();
399
400        let rule = LIARule::try_from(
401            RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
402                .with_guard(BooleanExpression::ComparisonExpression(
403                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
404                    ComparisonOp::Eq,
405                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
406                ))
407                .with_action(
408                    Action::new(
409                        var.clone(),
410                        IntegerExpression::Const(1) + IntegerExpression::Atom(var.clone()),
411                    )
412                    .unwrap(),
413                )
414                .build(),
415        )
416        .unwrap();
417
418        assert!(interval_tas.is_err());
419        if let Err(e) = interval_tas {
420            assert_eq!(
421                e,
422                IntervalTATransformationError::ComparisonGuardFoundRule(Box::new(rule))
423            );
424        }
425    }
426}
taco_interval_ta/builder.rs

taco_interval_ta/
builder.rs
