taco_threshold_automaton/
lia_threshold_automaton.rs

1//! A linear arithmetic threshold automaton or [`LIAThresholdAutomaton`]
2//! is a threshold automaton containing linear arithmetic guards. The
3//! goal of the [`LIAThresholdAutomaton`] is to stay as close to the formal
4//! definition of a threshold automaton as possible.
5//!
6//! To convert a [`GeneralThresholdAutomaton`] to a [`LIAThresholdAutomaton`]
7//! all guards are translated into one of these forms:
8//! - [`SingleAtomConstraint`]: Which represents a threshold in the form
9//!   `x <COMPARISON_OP> c_1 * p_1 + ... c_n * p_n + c`
10//!   where `c_1, ..., c_n, c` are rational constants, `p_1, ..., p_n` are
11//!   Parameters and x is a single shared variable.
12//! - [`SumAtomConstraint`]: Represents a threshold of the form
13//!   `cx_1 * x_1 + ... + cx_m * x_m <COMPARISON_OP> c_1 * p_1 + ... c_n * p_n + c`
14//!   where `c_1, ..., c_n, cx_1, ..., cx_m, c` are rational constants, `p_1,
15//!   ..., p_n` are Parameters and x_1, ..., x_m are shared variables.
16//!   Additionally, all coefficients `cx_1, ..., cx_m` must be all positive.
17//! - [`ComparisonConstraint`]: Comparison constraints are structured analog to
18//!   a [`SumAtomConstraint`], but allow mixing positive and negative constants
19//!   in the constants `cx_1, ..., cx_m`.
20//!
21//! Note that not all algorithms support all types of guards. Especially the
22//! [`ComparisonConstraint`] makes the verification problem undecidable (even without
23//! decrements and or resets). For more information see:
24//!     
25//! > All Flavors of Threshold Automata - Jure Kukovec, Igor Konnov,
26//! > Josef Widder - <https://doi.org/10.4230/LIPIcs.CONCUR.2018.19>
27
28use std::collections::HashMap;
29use std::fmt::Debug;
30use std::hash::Hash;
31
32use crate::expressions::{Atomic, BooleanConnective, BooleanExpression, Location, Variable};
33
34use crate::general_threshold_automaton::{Action, GeneralThresholdAutomaton, Rule};
35use crate::lia_threshold_automaton::integer_thresholds::{ThresholdConstraintOver, WeightedSum};
36
37pub mod general_to_lia;
38pub mod integer_thresholds;
39pub mod no_sum_var_ta;
40pub mod properties;
41
42/// A linear arithmetic threshold automaton or [`LIAThresholdAutomaton`]
43/// is a threshold automaton containing linear arithmetic guards. The
44/// goal of the [`LIAThresholdAutomaton`] is to stay as close to the formal
45/// definition of a threshold automaton as possible.
46///
47/// To convert a [`GeneralThresholdAutomaton`] to a [`LIAThresholdAutomaton`]
48/// all guards are translated into one of these forms:
49/// - [`SingleAtomConstraint`]: Which represents a threshold in the form
50///   `x <COMPARISON_OP> c_1 * p_1 + ... c_n * p_n + c`
51///   where `c_1, ..., c_n, c` are rational constants, `p_1, ..., p_n` are
52///   Parameters and x is a single shared variable.
53/// - [`SumAtomConstraint`]: Represents a threshold of the form
54///   `cx_1 * x_1 + ... + cx_m * x_m <COMPARISON_OP> c_1 * p_1 + ... c_n * p_n + c`
55///   where `c_1, ..., c_n, cx_1, ..., cx_m, c` are rational constants, `p_1,
56///   ..., p_n` are Parameters and x_1, ..., x_m are shared variables.
57///   Additionally, all coefficients `cx_1, ..., cx_m` must be all positive.
58/// - [`ComparisonConstraint`]: Comparison constraints are structured analog to
59///   a [`SumAtomConstraint`], but allow mixing positive and negative constants in
60///   the constants `cx_1, ..., cx_m`.
61///
62/// Note that not all algorithms support all types of guards. Especially the
63/// [`ComparisonConstraint`] makes the verification problem undecidable (even without
64/// decrements and or resets). For more information see:
65///     
66/// > All Flavors of Threshold Automata - Jure Kukovec, Igor Konnov,
67/// > Josef Widder - <https://doi.org/10.4230/LIPIcs.CONCUR.2018.19>
68#[derive(Debug, PartialEq, Clone)]
69pub struct LIAThresholdAutomaton {
70    /// [`GeneralThresholdAutomaton`] the canonical automaton has been constructed from
71    ta: GeneralThresholdAutomaton,
72    /// Initial conditions on variables in linear arithmetic
73    init_variable_constr: Vec<LIAVariableConstraint>,
74    /// Transition rules of the threshold automaton indexed by source location
75    rules: HashMap<Location, Vec<LIARule>>,
76    /// Additional variables that are used to replace sums
77    /// TODO: remove when a proper ordering for sums of variables is implemented
78    additional_vars_for_sums: HashMap<Variable, WeightedSum<Variable>>,
79}
80
81/// Rule type of [`LIAThresholdAutomaton`]
82///
83/// A rule guarded by a constraint representable in linear arithmetic (see
84/// [`LIAVariableConstraint`]).
85#[derive(Debug, PartialEq, Clone, Eq, Hash)]
86pub struct LIARule {
87    /// Id assigned to the rule in the specification
88    id: u32,
89    /// Source location of the rule
90    source: Location,
91    /// Target location of the rule
92    target: Location,
93    /// Guard of the rule
94    guard: LIAVariableConstraint,
95    /// Effect of the rule
96    actions: Vec<Action>,
97}
98
99/// Errors that can occur when trying to transform a threshold automaton in a
100/// linear arithmetic threshold automaton
101#[derive(Debug, Clone, PartialEq)]
102pub enum LIATransformationError {
103    /// Error occurred during transformation of a guard of a rule, see
104    /// [`ConstraintRewriteError`] for more details on the error
105    GuardError(
106        Box<Rule>,
107        Box<BooleanExpression<Variable>>,
108        Box<ConstraintRewriteError>,
109    ),
110    /// Error occurred during the transformation of an initial variable
111    /// constraint, see [`ConstraintRewriteError`] for more details on the error
112    InitialConstraintError(
113        Box<BooleanExpression<Variable>>,
114        Box<ConstraintRewriteError>,
115    ),
116}
117
118/// Abstract constraint type for linear arithmetic formulas over shared
119/// variables
120///  
121/// This struct allows to represent combinations the different types of
122/// constraints over evaluations of shared variables. It allows to reference:
123///
124/// - [`SingleAtomConstraint`]: Which represents a threshold in the form
125///   `x <COMPARISON_OP> c_1 * p_1 + ... c_n * p_n + c`
126///   where `c_1, ..., c_n, c` are rational constants, `p_1, ..., p_n` are
127///   Parameters and x is a single shared variable.
128/// - [`SumAtomConstraint`]: Represents a threshold of the form
129///   `cx_1 * x_1 + ... + cx_m * x_m <COMPARISON_OP> c_1 * p_1 + ... c_n * p_n + c`
130///   where `c_1, ..., c_n, cx_1, ..., cx_m, c` are rational constants, `p_1,
131///   ..., p_n` are Parameters and x_1, ..., x_m are shared variables.
132///   Additionally, all coefficients `cx_1, ..., cx_m` must be all positive.
133/// - [`ComparisonConstraint`]: Comparison constraints are structured analog to
134///   a [`SumAtomConstraint`], but allow mixing positive and negative constants in
135///   the constants `cx_1, ..., cx_m`.
136///
137/// and boolean combinations of these guards
138#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
139pub enum LIAVariableConstraint {
140    /// Constraint over the difference between variables / comparing variables
141    ComparisonConstraint(ComparisonConstraint<Variable>),
142    /// Constraint over a single variable
143    SingleVarConstraint(SingleAtomConstraint<Variable>),
144    /// Constraint over the sum of multiple variables
145    SumVarConstraint(SumAtomConstraint<Variable>),
146    /// Boolean Combination of multiple constraints over variables
147    BinaryGuard(
148        Box<LIAVariableConstraint>,
149        BooleanConnective,
150        Box<LIAVariableConstraint>,
151    ),
152    /// True / always enabled
153    True,
154    /// False / always disabled
155    False,
156}
157
158/// Error that can occur during the transformation of a guard
159#[derive(Debug, Clone, PartialEq)]
160pub enum ConstraintRewriteError {
161    /// Constraint is not a linear arithmetic constraint (e.g. it could contain
162    /// multiplications of atoms)
163    NotLinearArithmetic,
164    /// Constraint over parameters values instead of shared memory values
165    ///
166    /// Constraints like this should be part of the resilience condition
167    ParameterConstraint(Box<BooleanExpression<Variable>>),
168}
169
170/// Threshold guard over a single atom
171///
172/// This struct represents a guard over a single atom, i.e., it represents a
173/// constraint formula of the form `v COMPOP cp_1 * p_1 + ... + cp_n * p_m + c`
174/// where `cp_1, ..., cp_m` are rational factors, `COMPOP` is a comparison
175/// operator (i.e.,`<, >, <=, >=, ==, !=`), `v` is a atom, `p_1, ..., p_m`
176/// are parameters, and `c` is a rational constant.
177#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
178pub struct SingleAtomConstraint<T: Atomic>(ThresholdConstraintOver<T>);
179
180/// Error that can occur when trying to construct a [`SingleAtomConstraint`]
181#[derive(Debug, Clone, PartialEq)]
182pub enum SingleAtomConstrExtractionError {
183    /// The constraint references multiple atoms, it could be a
184    /// [`SumAtomConstraint`] or [`ComparisonConstraint`]
185    HasMultipleAtoms,
186    /// Rewriting of the constraint failed
187    TransformationFailed(ConstraintRewriteError),
188}
189
190/// Constraint over the evaluation over a sum of multiple atoms
191///
192/// This struct represents a guard over the values of a sum of atoms, i.e., it
193/// represents a constraint formula of the form
194/// `cv_1 * v_1 + ... + cv_n * v_n <COMPOP> cp_1 * p_1 + ... + cp_n * p_m + c`
195/// where `cv_1, ..., cv_n, cp_1, ..., cp_m` are rational factors, `COMPOP` is
196/// a comparison operator (i.e.,`<, >, <=, >=, ==, !=`), `v_1, ..., v_n` are
197/// variables, `p_1, ..., p_m` are parameters, and `c` is a rational constant.
198///
199/// Additionally, all variable coefficients, i.e., `cv_1, ..., cv_n`, must be
200/// greater than zero.
201#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
202pub struct SumAtomConstraint<T: Atomic>(ThresholdConstraintOver<WeightedSum<T>>);
203
204/// Error that can occur during the creation of a [`SumAtomConstraint`]
205#[derive(Debug, Clone, PartialEq)]
206pub enum SumVarConstraintCreationError {
207    /// Guard is a [`ComparisonConstraint`] not a [`SumAtomConstraint`]
208    IsComparisonConstraint,
209    /// Guard is a [`SingleAtomConstraint`] not a [`SumAtomConstraint`]
210    IsSingleAtomConstraint,
211}
212
213/// Constraint over the difference between atoms / comparing atoms
214///
215/// This struct represents a comparison guard, i.e., it represents a guard of
216/// the form
217/// `cv_1 * v_1 + ... + cv_n * v_n <COMPOP> cp_1 * p_1 + ... + cp_n * p_m + c`
218/// where `cv_1, ..., cv_n, cp_1, ..., cp_m` are rational factors, `<COMPOP>` is
219/// a comparison operator (i.e.,`<, >, <=, >=, ==, !=`), `v_1, ..., v_n` are
220/// atoms, `p_1, ..., p_m` are parameters, and `c` is a rational constant.
221///
222/// Additionally, at least one of the atom coefficients, i.e.,
223/// `cv_1, ..., cv_n`, must be smaller than zero and at least one greater than
224/// zero. Otherwise the guard would be a [`SumAtomConstraint`].
225#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
226pub struct ComparisonConstraint<T: Atomic>(ThresholdConstraintOver<WeightedSum<T>>);
227
228/// Error that can occur during the creation of a comparison guard
229#[derive(Debug, Clone, PartialEq)]
230pub enum ComparisonConstraintCreationError {
231    /// Guard is a [`SumAtomConstraint`] not a [`ComparisonConstraint`]
232    IsSumVarConstraint,
233}
taco_threshold_automaton/lia_threshold_automaton.rs

taco_threshold_automaton/
lia_threshold_automaton.rs
