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    lia_threshold_automaton::{LIAThresholdAutomaton, LIAVariableConstraint},
11    {RuleDefinition, ThresholdAutomaton},
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                Some(
160                    order_builder
161                        .add_single_variable_interval(thr_guard.get_atom(), &interval_boundary),
162                )
163            }
164            LIAVariableConstraint::SumVarConstraint(thr_guard) => {
165                let interval_boundary = IntervalBoundary::from_threshold_constraint(
166                    thr_guard.get_threshold_constraint(),
167                );
168
169                Some(
170                    order_builder
171                        .add_multi_variable_interval(thr_guard.get_atoms(), &interval_boundary),
172                )
173            }
174        }
175    }
176}
177
178#[cfg(test)]
179mod test {
180    use taco_smt_encoder::SMTSolverBuilder;
181    use taco_threshold_automaton::{
182        expressions::{
183            BooleanExpression, ComparisonOp, IntegerExpression, Location, Parameter, Variable,
184        },
185        general_threshold_automaton::{
186            Action,
187            builder::{GeneralThresholdAutomatonBuilder, RuleBuilder},
188        },
189        lia_threshold_automaton::{LIARule, LIAThresholdAutomaton, LIAVariableConstraint},
190    };
191
192    use crate::{IntervalTATransformationError, builder::IntervalTABuilder};
193
194    #[test]
195    fn test_builder_for_lia_ta_err_on_comparison_constr_target() {
196        let var = Variable::new("x");
197
198        let rc = BooleanExpression::ComparisonExpression(
199            Box::new(IntegerExpression::Param(Parameter::new("n"))),
200            ComparisonOp::Gt,
201            Box::new(IntegerExpression::Const(3)),
202        );
203
204        let ta = GeneralThresholdAutomatonBuilder::new("test_ta")
205            .with_variables([var.clone(), Variable::new("y")])
206            .unwrap()
207            .with_locations([Location::new("l1"), Location::new("l2")])
208            .unwrap()
209            .with_parameter(Parameter::new("n"))
210            .unwrap()
211            .initialize()
212            .with_resilience_condition(rc.clone())
213            .unwrap()
214            .with_initial_location_constraint(BooleanExpression::ComparisonExpression(
215                Box::new(IntegerExpression::Atom(Location::new("l1"))),
216                ComparisonOp::Eq,
217                Box::new(IntegerExpression::Const(0)),
218            ))
219            .unwrap()
220            .with_rule(
221                RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
222                    .with_guard(BooleanExpression::ComparisonExpression(
223                        Box::new(IntegerExpression::Atom(var.clone())),
224                        ComparisonOp::Gt,
225                        Box::new(IntegerExpression::Const(2)),
226                    ))
227                    .with_action(
228                        Action::new(
229                            var.clone(),
230                            IntegerExpression::Const(1) + IntegerExpression::Atom(var.clone()),
231                        )
232                        .unwrap(),
233                    )
234                    .build(),
235            )
236            .unwrap()
237            .build();
238
239        let lia_ta = LIAThresholdAutomaton::try_from(ta).unwrap();
240
241        let lia_constr: LIAVariableConstraint = (&BooleanExpression::ComparisonExpression(
242            Box::new(IntegerExpression::Atom(Variable::new("x"))),
243            ComparisonOp::Eq,
244            Box::new(IntegerExpression::Atom(Variable::new("y"))),
245        ))
246            .try_into()
247            .unwrap();
248
249        let interval_tas = IntervalTABuilder::new(
250            lia_ta,
251            SMTSolverBuilder::default(),
252            vec![lia_constr.clone()],
253        )
254        .build();
255
256        assert!(interval_tas.is_err());
257        if let Err(e) = interval_tas {
258            assert_eq!(
259                e,
260                IntervalTATransformationError::ComparisonGuardFoundVariableTarget(Box::new(
261                    lia_constr.clone()
262                ))
263            );
264        }
265    }
266
267    #[test]
268    fn test_builder_for_lia_ta_err_on_comparison_constr_init_loc() {
269        let var = Variable::new("x");
270
271        let rc = BooleanExpression::ComparisonExpression(
272            Box::new(IntegerExpression::Param(Parameter::new("n"))),
273            ComparisonOp::Gt,
274            Box::new(IntegerExpression::Const(3)),
275        );
276
277        let ta = GeneralThresholdAutomatonBuilder::new("test_ta")
278            .with_variables([var.clone(), Variable::new("y")])
279            .unwrap()
280            .with_locations([Location::new("l1"), Location::new("l2")])
281            .unwrap()
282            .with_parameter(Parameter::new("n"))
283            .unwrap()
284            .initialize()
285            .with_resilience_condition(rc.clone())
286            .unwrap()
287            .with_initial_variable_constraint(BooleanExpression::ComparisonExpression(
288                Box::new(IntegerExpression::Atom(Variable::new("x"))),
289                ComparisonOp::Eq,
290                Box::new(IntegerExpression::Atom(Variable::new("y"))),
291            ))
292            .unwrap()
293            .with_rule(
294                RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
295                    .with_guard(BooleanExpression::ComparisonExpression(
296                        Box::new(IntegerExpression::Atom(var.clone())),
297                        ComparisonOp::Gt,
298                        Box::new(IntegerExpression::Const(2)),
299                    ))
300                    .with_action(
301                        Action::new(
302                            var.clone(),
303                            IntegerExpression::Const(1) + IntegerExpression::Atom(var.clone()),
304                        )
305                        .unwrap(),
306                    )
307                    .build(),
308            )
309            .unwrap()
310            .build();
311
312        let lia_ta = LIAThresholdAutomaton::try_from(ta).unwrap();
313
314        let interval_tas =
315            IntervalTABuilder::new(lia_ta, SMTSolverBuilder::default(), vec![]).build();
316
317        let lia_constr: LIAVariableConstraint = (&BooleanExpression::ComparisonExpression(
318            Box::new(IntegerExpression::Atom(Variable::new("x"))),
319            ComparisonOp::Eq,
320            Box::new(IntegerExpression::Atom(Variable::new("y"))),
321        ))
322            .try_into()
323            .unwrap();
324
325        assert!(interval_tas.is_err());
326        if let Err(e) = interval_tas {
327            assert_eq!(
328                e,
329                IntervalTATransformationError::ComparisonGuardFoundInitialVariableConstraint(
330                    Box::new(lia_constr.clone())
331                )
332            );
333        }
334    }
335
336    #[test]
337    fn test_builder_for_lia_ta_err_on_comparison_rule() {
338        let var = Variable::new("x");
339
340        let rc = BooleanExpression::ComparisonExpression(
341            Box::new(IntegerExpression::Param(Parameter::new("n"))),
342            ComparisonOp::Gt,
343            Box::new(IntegerExpression::Const(3)),
344        );
345
346        let ta = GeneralThresholdAutomatonBuilder::new("test_ta")
347            .with_variables([var.clone(), Variable::new("y")])
348            .unwrap()
349            .with_locations([Location::new("l1"), Location::new("l2")])
350            .unwrap()
351            .with_parameter(Parameter::new("n"))
352            .unwrap()
353            .initialize()
354            .with_resilience_condition(rc.clone())
355            .unwrap()
356            .with_initial_location_constraint(BooleanExpression::ComparisonExpression(
357                Box::new(IntegerExpression::Atom(Location::new("l1"))),
358                ComparisonOp::Eq,
359                Box::new(IntegerExpression::Const(0)),
360            ))
361            .unwrap()
362            .with_rule(
363                RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
364                    .with_guard(BooleanExpression::ComparisonExpression(
365                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
366                        ComparisonOp::Eq,
367                        Box::new(IntegerExpression::Atom(Variable::new("y"))),
368                    ))
369                    .with_action(
370                        Action::new(
371                            var.clone(),
372                            IntegerExpression::Const(1) + IntegerExpression::Atom(var.clone()),
373                        )
374                        .unwrap(),
375                    )
376                    .build(),
377            )
378            .unwrap()
379            .build();
380
381        let lia_ta = LIAThresholdAutomaton::try_from(ta).unwrap();
382
383        let interval_tas =
384            IntervalTABuilder::new(lia_ta, SMTSolverBuilder::default(), vec![]).build();
385
386        let rule = LIARule::try_from(
387            RuleBuilder::new(0, Location::new("l1"), Location::new("l2"))
388                .with_guard(BooleanExpression::ComparisonExpression(
389                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
390                    ComparisonOp::Eq,
391                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
392                ))
393                .with_action(
394                    Action::new(
395                        var.clone(),
396                        IntegerExpression::Const(1) + IntegerExpression::Atom(var.clone()),
397                    )
398                    .unwrap(),
399                )
400                .build(),
401        )
402        .unwrap();
403
404        assert!(interval_tas.is_err());
405        if let Err(e) = interval_tas {
406            assert_eq!(
407                e,
408                IntervalTATransformationError::ComparisonGuardFoundRule(Box::new(rule))
409            );
410        }
411    }
412}
taco_interval_ta/builder.rs

taco_interval_ta/
builder.rs
