taco_threshold_automaton/lia_threshold_automaton/
general_to_lia.rs

1//! Logic to try to convert a [`GeneralThresholdAutomaton`] into a
2//! [`LIAThresholdAutomaton`].
3//!
4//! This module contains the logic to transform a [`GeneralThresholdAutomaton`]
5//! into a  [`LIAThresholdAutomaton`], i.e., into a threshold automaton where all
6//! expressions are in linear arithmetic.
7//!
8//! The transformation works in the following way:
9//!
10//! First boolean negations are removed by pushing them inwards. This logic can
11//! be found in the `remove_boolean_neg` module. This step converts
12//! `BooleanExpression` into
13//! `remove_boolean_neg::NonNegatedBooleanExpression`.
14//!
15//! Next, the integer expressions in the boolean expressions are transformed.
16//! First, any subtractions are removed by transforming them into additions with
17//! a negative number or by adding a factor `-1`. This logic can be found in the
18//! `remove_minus` module. This step converts `IntegerExpressions` into
19//! `NonMinusIntegerExpr`.
20//!
21//! Next, divisions are removed by transforming them into multiplications with
22//! rational factors. This is the first incomplete step, as this is only
23//! possible if there are no atoms appearing in a divisor. This logic can be
24//! found in the `remove_div` module. This step converts
25//! `NonMinusIntegerExpr` into `NonDivIntegerExpr`.
26//!
27//! If all expressions could be transformed we can now transform integer
28//! expressions into weighted sums, with rational factors. This is the form
29//! assumed by many papers in the formal definition of threshold automata. This
30//! is done in the module `split_pairs`.
31//!
32//! The final step in processing integer expressions is to bring all variables
33//! to the left side of the equation, and then classify them into the 3 LIAGuard
34//! types. This logic can be found in the `classify_into_lia` module.
35//!
36//! Afterwards, the guards can finally be assembled back into the
37//! [`LIAVariableConstraint`] type, which is a boolean combination of the 3
38//! guard types.
39
40use std::{collections::HashMap, error::Error, fmt::Display};
41
42pub(crate) mod classify_into_lia;
43mod remove_boolean_neg;
44mod remove_div;
45mod remove_minus;
46mod split_pair;
47
48use crate::{
49    ActionDefinition, RuleDefinition,
50    expressions::Location,
51    general_threshold_automaton::{GeneralThresholdAutomaton, Rule},
52};
53
54use super::{
55    ConstraintRewriteError, LIARule, LIAThresholdAutomaton, LIATransformationError,
56    LIAVariableConstraint,
57};
58
59impl Error for ConstraintRewriteError {}
60
61impl Display for ConstraintRewriteError {
62    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
63        match self {
64            ConstraintRewriteError::NotLinearArithmetic => write!(
65                f,
66                "Non linear integer arithmetic expression detected. Threshold automata only allow for linear arithmetic formula in their guards.",
67            ),
68            ConstraintRewriteError::ParameterConstraint(expr) => write!(
69                f,
70                "Found a constraint over the parameter evaluation instead of the variable valuation ! The constraint {expr} restricts the parameter values, which is only allowed in the resilience condition."
71            ),
72        }
73    }
74}
75
76impl TryFrom<GeneralThresholdAutomaton> for LIAThresholdAutomaton {
77    type Error = LIATransformationError;
78
79    fn try_from(ta: GeneralThresholdAutomaton) -> Result<Self, Self::Error> {
80        let init_variable_constr = ta
81            .initial_variable_conditions()
82            .map(|c| {
83                let c: LIAVariableConstraint = c.try_into().map_err(|err| {
84                    LIATransformationError::InitialConstraintError(
85                        Box::new(c.clone()),
86                        Box::new(err),
87                    )
88                })?;
89
90                Ok::<_, Self::Error>(c)
91            })
92            .collect::<Result<Vec<LIAVariableConstraint>, Self::Error>>()?;
93
94        let rules: HashMap<Location, Vec<_>> = ta
95            .get_rule_map()
96            .into_iter()
97            .map(|(loc, rules)| {
98                let rules: Vec<LIARule> = rules
99                    .into_iter()
100                    .map(|r| LIARule::try_from(&r))
101                    .collect::<Result<Vec<LIARule>, LIATransformationError>>()?;
102
103                Ok::<(Location, Vec<LIARule>), LIATransformationError>((loc, rules))
104            })
105            .collect::<Result<HashMap<Location, Vec<_>>, LIATransformationError>>()?;
106
107        Ok(Self {
108            ta,
109            init_variable_constr,
110            rules,
111            additional_vars_for_sums: HashMap::new(),
112        })
113    }
114}
115
116impl TryFrom<&Rule> for LIARule {
117    type Error = LIATransformationError;
118
119    /// Try to convert a rule into a [`LIARule`].
120    ///
121    /// A rule can be converted into a [`LIARule`] if the guard is a linear
122    /// arithmetic formula. This means for example that it does not contain any
123    /// multiplications between variables
124    ///
125    /// This function will return an [`LIATransformationError`] if the guard is
126    /// no linear arithmetic formula.
127    fn try_from(rule: &Rule) -> Result<Self, Self::Error> {
128        let guard = rule.guard().try_into().map_err(|err| {
129            LIATransformationError::GuardError(
130                Box::new(rule.clone()),
131                Box::new(rule.guard().clone()),
132                Box::new(err),
133            )
134        })?;
135        let actions = rule
136            .actions()
137            .filter(|ac| !ac.is_unchanged())
138            .cloned()
139            .collect();
140
141        Ok(Self {
142            id: rule.id(),
143            source: rule.source().clone(),
144            target: rule.target().clone(),
145            guard,
146            actions,
147        })
148    }
149}
150
151impl TryFrom<Rule> for LIARule {
152    type Error = LIATransformationError;
153
154    fn try_from(value: Rule) -> Result<Self, Self::Error> {
155        (&value).try_into()
156    }
157}
158
159#[cfg(test)]
160mod tests {
161    use std::collections::HashMap;
162
163    use crate::{
164        BooleanVarConstraint, LocationConstraint, ParameterConstraint,
165        expressions::{
166            BooleanConnective, ComparisonOp, IntegerExpression, IntegerOp, Location, Parameter,
167            Variable, fraction::Fraction,
168        },
169        general_threshold_automaton::{
170            Action,
171            builder::{GeneralThresholdAutomatonBuilder, RuleBuilder},
172        },
173        lia_threshold_automaton::{
174            LIARule, LIAThresholdAutomaton, LIATransformationError, LIAVariableConstraint,
175            SingleAtomConstraint,
176            integer_thresholds::{ThresholdCompOp, ThresholdConstraint},
177        },
178    };
179
180    #[test]
181    fn test_full_ta_lia_ta() {
182        let ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
183            .with_parameters(vec![
184                Parameter::new("n"),
185                Parameter::new("t"),
186                Parameter::new("f"),
187            ])
188            .unwrap()
189            .with_variables(vec![
190                Variable::new("var1"),
191                Variable::new("var2"),
192                Variable::new("var3"),
193            ])
194            .unwrap()
195            .with_locations(vec![
196                Location::new("loc1"),
197                Location::new("loc2"),
198                Location::new("loc3"),
199            ])
200            .unwrap()
201            .initialize()
202            .with_initial_variable_constraints(vec![BooleanVarConstraint::ComparisonExpression(
203                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
204                ComparisonOp::Eq,
205                Box::new(IntegerExpression::Const(1)),
206            )])
207            .unwrap()
208            .with_initial_location_constraints(vec![
209                LocationConstraint::ComparisonExpression(
210                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
211                    ComparisonOp::Eq,
212                    Box::new(
213                        IntegerExpression::Param(Parameter::new("n"))
214                            - IntegerExpression::Param(Parameter::new("f")),
215                    ),
216                ) | LocationConstraint::ComparisonExpression(
217                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
218                    ComparisonOp::Eq,
219                    Box::new(IntegerExpression::Const(0)),
220                ),
221            ])
222            .unwrap()
223            .with_resilience_conditions(vec![ParameterConstraint::ComparisonExpression(
224                Box::new(IntegerExpression::Atom(Parameter::new("n"))),
225                ComparisonOp::Gt,
226                Box::new(IntegerExpression::BinaryExpr(
227                    Box::new(IntegerExpression::Const(3)),
228                    IntegerOp::Mul,
229                    Box::new(IntegerExpression::Atom(Parameter::new("f"))),
230                )),
231            )])
232            .unwrap()
233            .with_rules(vec![
234                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2"))
235                    .with_actions(vec![
236                        Action::new(
237                            Variable::new("var1"),
238                            IntegerExpression::Atom(Variable::new("var1")),
239                        )
240                        .unwrap(),
241                    ])
242                    .build(),
243                RuleBuilder::new(1, Location::new("loc2"), Location::new("loc3"))
244                    .with_guard(
245                        BooleanVarConstraint::ComparisonExpression(
246                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
247                            ComparisonOp::Eq,
248                            Box::new(IntegerExpression::Const(1)),
249                        ) & BooleanVarConstraint::ComparisonExpression(
250                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
251                            ComparisonOp::Eq,
252                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
253                        ),
254                    )
255                    .with_actions(vec![
256                        Action::new(Variable::new("var3"), IntegerExpression::Const(0)).unwrap(),
257                        Action::new(
258                            Variable::new("var1"),
259                            IntegerExpression::BinaryExpr(
260                                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
261                                IntegerOp::Add,
262                                Box::new(IntegerExpression::Const(1)),
263                            ),
264                        )
265                        .unwrap(),
266                    ])
267                    .build(),
268            ])
269            .unwrap()
270            .build();
271
272        let lia_ta = LIAThresholdAutomaton::try_from(ta.clone()).unwrap();
273
274        let expected_lia = LIAThresholdAutomaton {
275            ta: ta.clone(),
276            rules: HashMap::from([
277                (
278                    Location::new("loc1"),
279                    vec![LIARule {
280                        id: 0,
281                        source: Location::new("loc1"),
282                        target: Location::new("loc2"),
283                        guard: LIAVariableConstraint::True,
284                        actions: vec![],
285                    }],
286                ),
287                (
288                    Location::new("loc2"),
289                    vec![LIARule {
290                        id: 1,
291                        source: Location::new("loc2"),
292                        target: Location::new("loc3"),
293                        guard: LIAVariableConstraint::BinaryGuard(
294                            Box::new(LIAVariableConstraint::BinaryGuard(
295                                Box::new(LIAVariableConstraint::SingleVarConstraint(
296                                    SingleAtomConstraint::new(
297                                        Variable::new("var1"),
298                                        ThresholdConstraint::new(
299                                            ThresholdCompOp::Lt,
300                                            Vec::<(Parameter, Fraction)>::new(),
301                                            2,
302                                        ),
303                                    ),
304                                )),
305                                BooleanConnective::And,
306                                Box::new(LIAVariableConstraint::SingleVarConstraint(
307                                    SingleAtomConstraint::new(
308                                        Variable::new("var1"),
309                                        ThresholdConstraint::new(
310                                            ThresholdCompOp::Geq,
311                                            Vec::<(Parameter, Fraction)>::new(),
312                                            1,
313                                        ),
314                                    ),
315                                )),
316                            )),
317                            BooleanConnective::And,
318                            Box::new(LIAVariableConstraint::BinaryGuard(
319                                Box::new(LIAVariableConstraint::SingleVarConstraint(
320                                    SingleAtomConstraint::new(
321                                        Variable::new("var2"),
322                                        ThresholdConstraint::new(
323                                            ThresholdCompOp::Lt,
324                                            [(Parameter::new("n"), 1)],
325                                            1,
326                                        ),
327                                    ),
328                                )),
329                                BooleanConnective::And,
330                                Box::new(LIAVariableConstraint::SingleVarConstraint(
331                                    SingleAtomConstraint::new(
332                                        Variable::new("var2"),
333                                        ThresholdConstraint::new(
334                                            ThresholdCompOp::Geq,
335                                            [(Parameter::new("n"), 1)],
336                                            0,
337                                        ),
338                                    ),
339                                )),
340                            )),
341                        ),
342                        actions: vec![
343                            Action::new(Variable::new("var3"), IntegerExpression::Const(0))
344                                .unwrap(),
345                            Action::new(
346                                Variable::new("var1"),
347                                IntegerExpression::BinaryExpr(
348                                    Box::new(IntegerExpression::Atom(Variable::new("var1"))),
349                                    IntegerOp::Add,
350                                    Box::new(IntegerExpression::Const(1)),
351                                ),
352                            )
353                            .unwrap(),
354                        ],
355                    }],
356                ),
357            ]),
358            init_variable_constr: vec![LIAVariableConstraint::BinaryGuard(
359                Box::new(LIAVariableConstraint::SingleVarConstraint(
360                    SingleAtomConstraint::new(
361                        Variable::new("var1"),
362                        ThresholdConstraint::new(
363                            ThresholdCompOp::Lt,
364                            Vec::<(Parameter, Fraction)>::new(),
365                            2,
366                        ),
367                    ),
368                )),
369                BooleanConnective::And,
370                Box::new(LIAVariableConstraint::SingleVarConstraint(
371                    SingleAtomConstraint::new(
372                        Variable::new("var1"),
373                        ThresholdConstraint::new(
374                            ThresholdCompOp::Geq,
375                            Vec::<(Parameter, Fraction)>::new(),
376                            1,
377                        ),
378                    ),
379                )),
380            )],
381            additional_vars_for_sums: HashMap::new(),
382        };
383
384        assert_eq!(lia_ta, expected_lia);
385    }
386
387    #[test]
388    fn test_error_on_non_lia() {
389        let violating_rule = RuleBuilder::new(1, Location::new("loc2"), Location::new("loc3"))
390            .with_guard(
391                BooleanVarConstraint::ComparisonExpression(
392                    Box::new(IntegerExpression::Atom(Variable::new("var1"))),
393                    ComparisonOp::Eq,
394                    Box::new(IntegerExpression::Const(1)),
395                ) & BooleanVarConstraint::ComparisonExpression(
396                    Box::new(IntegerExpression::Atom(Variable::new("var2"))),
397                    ComparisonOp::Eq,
398                    Box::new(
399                        IntegerExpression::Param(Parameter::new("n"))
400                            * IntegerExpression::Atom(Variable::new("var2")),
401                    ),
402                ),
403            )
404            .with_actions(vec![
405                Action::new(Variable::new("var3"), IntegerExpression::Const(0)).unwrap(),
406                Action::new(
407                    Variable::new("var1"),
408                    IntegerExpression::BinaryExpr(
409                        Box::new(IntegerExpression::Atom(Variable::new("var1"))),
410                        IntegerOp::Add,
411                        Box::new(IntegerExpression::Const(1)),
412                    ),
413                )
414                .unwrap(),
415            ])
416            .build();
417
418        let ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
419            .with_parameters(vec![
420                Parameter::new("n"),
421                Parameter::new("t"),
422                Parameter::new("f"),
423            ])
424            .unwrap()
425            .with_variables(vec![
426                Variable::new("var1"),
427                Variable::new("var2"),
428                Variable::new("var3"),
429            ])
430            .unwrap()
431            .with_locations(vec![
432                Location::new("loc1"),
433                Location::new("loc2"),
434                Location::new("loc3"),
435            ])
436            .unwrap()
437            .initialize()
438            .with_initial_location_constraints(vec![
439                LocationConstraint::ComparisonExpression(
440                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
441                    ComparisonOp::Eq,
442                    Box::new(
443                        IntegerExpression::Param(Parameter::new("n"))
444                            - IntegerExpression::Param(Parameter::new("f")),
445                    ),
446                ) | LocationConstraint::ComparisonExpression(
447                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
448                    ComparisonOp::Eq,
449                    Box::new(IntegerExpression::Const(0)),
450                ),
451            ])
452            .unwrap()
453            .with_rules(vec![
454                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2"))
455                    .with_actions(vec![
456                        Action::new(
457                            Variable::new("var1"),
458                            IntegerExpression::Atom(Variable::new("var1")),
459                        )
460                        .unwrap(),
461                    ])
462                    .build(),
463                violating_rule.clone(),
464            ])
465            .unwrap()
466            .with_resilience_conditions(vec![ParameterConstraint::ComparisonExpression(
467                Box::new(IntegerExpression::Atom(Parameter::new("n"))),
468                ComparisonOp::Gt,
469                Box::new(IntegerExpression::BinaryExpr(
470                    Box::new(IntegerExpression::Atom(Parameter::new("f"))),
471                    IntegerOp::Mul,
472                    Box::new(IntegerExpression::Atom(Parameter::new("f"))),
473                )),
474            )])
475            .unwrap()
476            .build();
477        let lia_ta = LIAThresholdAutomaton::try_from(ta.clone());
478        assert!(lia_ta.is_err());
479
480        let err = lia_ta.unwrap_err();
481        assert!(matches!(
482            err.clone(),
483            LIATransformationError::GuardError(_, _, _)
484        ));
485        assert!(err.to_string().contains(&violating_rule.to_string()))
486    }
487}
taco_threshold_automaton/lia_threshold_automaton/general_to_lia.rs

taco_threshold_automaton/lia_threshold_automaton/
general_to_lia.rs
