taco_threshold_automaton/
expressions.rs

1//! Type definitions for arithmetic and boolean expressions over components
2//! of a threshold automaton
3//!
4//! This module contains the low-level expressions that make up a threshold
5//! automaton. These expressions are for example, what here is named `Atomic`
6//! expressions, such as
7//! - [`Parameter`]s
8//! - [`Location`]s, and
9//! - [`Variable`]s.
10//!
11//! These expressions all have to implement the `Atomic` trait, which allows
12//! them to be used in constraints.
13//!
14//! Constraints, in the most general form are represented by
15//! [`IntegerExpression`]s that are combined into [`BooleanExpression`]s by
16//! comparing them using Comparison operators ([`ComparisonOp`]).
17//!
18//! Note that the expressions defined here, are more general than what is
19//! allowed in the theoretical threshold automaton framework, which is why most
20//! model checkers work on a transformed version.
21
22use std::{
23    fmt::{Debug, Display},
24    hash::Hash,
25};
26
27pub mod fraction;
28pub mod properties;
29
30/// Atomic trait implemented by atomic expressions
31///
32/// This trait is implemented by types that can be used in atomic expressions,
33/// i.e., for threshold automata these can be parameters, variables, and
34/// locations.
35///
36/// All atomic expressions have a name associated with them, that must be unique
37/// within the threshold automaton.
38pub trait Atomic: Debug + Display + Hash + Clone + Eq + for<'a> From<&'a str> + Ord {
39    /// Returns the name of the atom
40    fn name(&self) -> &str;
41}
42
43/// Trait for checking if an object of type `T` has already been declared
44///
45/// Objects implementing this trait can be used during parsing to check if
46/// a location, variable or parameter is known. This is useful to validate
47/// parsed expressions, e.g., LTL expressions or update expressions, to ensure
48/// that expressions only reference known locations, variables and parameters.
49pub trait IsDeclared<T> {
50    /// Check if object of type T is declared
51    fn is_declared(&self, obj: &T) -> bool;
52}
53
54/// Parameter appearing in a threshold automaton
55///
56/// Parameters are used to represent for example the number of processes and
57/// faulty processes. They are constrained by the resilience conditions and do
58/// not change during execution. Typical parameter names are n, t and f.
59#[derive(Debug, PartialEq, Eq, Hash, Clone, PartialOrd, Ord)]
60pub struct Parameter(String);
61impl Parameter {
62    /// Create a new parameter with given name
63    pub fn new(name: impl ToString) -> Self {
64        Parameter(name.to_string())
65    }
66}
67
68impl From<&str> for Parameter {
69    fn from(s: &str) -> Self {
70        Parameter::new(s)
71    }
72}
73
74impl Atomic for Parameter {
75    fn name(&self) -> &str {
76        &self.0
77    }
78}
79
80/// Shared variable used in a threshold automaton
81///
82/// Transitions in a threshold automaton can be guarded with constraints over a
83/// shared variable valuation and can be updated when taking a transition.
84#[derive(Debug, PartialEq, Eq, Hash, Clone, PartialOrd, Ord)]
85pub struct Variable(String);
86impl Variable {
87    /// Create a new variable with given name
88    pub fn new(name: impl ToString) -> Self {
89        Variable(name.to_string())
90    }
91}
92
93impl From<&str> for Variable {
94    fn from(value: &str) -> Self {
95        Variable::new(value)
96    }
97}
98
99impl Atomic for Variable {
100    fn name(&self) -> &str {
101        &self.0
102    }
103}
104
105/// Location of a threshold automaton
106///
107/// A location is a state in the threshold automaton template.
108#[derive(Debug, PartialEq, Eq, Hash, Clone, PartialOrd, Ord)]
109pub struct Location(String);
110
111impl Location {
112    /// Create a new location with given name
113    pub fn new(name: impl ToString) -> Self {
114        Location(name.to_string())
115    }
116}
117
118impl From<&str> for Location {
119    fn from(value: &str) -> Self {
120        Location::new(value)
121    }
122}
123
124impl Atomic for Location {
125    fn name(&self) -> &str {
126        &self.0
127    }
128}
129
130/// Boolean constraint over type T
131///
132/// This enum represents a boolean expression over integer expressions and
133/// can be used to for example guards in rules of a threshold automaton.
134///
135/// # Example
136///
137/// ```
138/// use taco_threshold_automaton::expressions::*;
139///
140/// // y > 0
141/// let _ = BooleanExpression::ComparisonExpression(
142///     Box::new(IntegerExpression::Atom(Variable::new("y"))),
143///     ComparisonOp::Gt,
144///     Box::new(IntegerExpression::Const(0))
145/// );
146///
147/// // x > 0 && y < 10
148/// let _ = BooleanExpression::ComparisonExpression(
149///           Box::new(IntegerExpression::Atom(Variable::new("x"))),
150///           ComparisonOp::Gt,
151///           Box::new(IntegerExpression::Const(0)),
152///    ) & BooleanExpression::ComparisonExpression(
153///           Box::new(IntegerExpression::Atom(Variable::new("y"))),
154///           ComparisonOp::Lt,
155///           Box::new(IntegerExpression::Const(10)),
156///     );
157/// ```
158#[derive(Debug, PartialEq, Eq, Hash, Clone, PartialOrd, Ord)]
159pub enum BooleanExpression<T: Atomic> {
160    /// Comparison between two integer expressions
161    ComparisonExpression(
162        Box<IntegerExpression<T>>,
163        ComparisonOp,
164        Box<IntegerExpression<T>>,
165    ),
166    /// Boolean expressions combined through boolean connective
167    BinaryExpression(
168        Box<BooleanExpression<T>>,
169        BooleanConnective,
170        Box<BooleanExpression<T>>,
171    ),
172    /// Negation of boolean expression
173    Not(Box<BooleanExpression<T>>),
174    /// true
175    True,
176    /// false
177    False,
178}
179
180/// Integer expressions over objects of type T, parameters and integers
181///
182/// This enum represents integer expressions over objects of type T, parameters and integers.
183///
184/// # Example
185///
186/// ```
187/// use taco_threshold_automaton::expressions::*;
188///
189/// // x + 5
190/// let _ = IntegerExpression::Atom(Variable::new("x"))
191///             + IntegerExpression::Const(5);
192///
193/// // -x
194/// let _ = -IntegerExpression::Atom(Variable::new("x"));
195/// ```
196#[derive(Debug, PartialEq, Eq, Hash, Clone, PartialOrd, Ord)]
197pub enum IntegerExpression<T: Atomic> {
198    /// Atomic of type T
199    Atom(T),
200    /// Integer constant
201    Const(u32),
202    /// Parameter
203    Param(Parameter),
204    /// Integer expression combining two Integer expressions through an arithmetic operator
205    BinaryExpr(
206        Box<IntegerExpression<T>>,
207        IntegerOp,
208        Box<IntegerExpression<T>>,
209    ),
210    /// Negated expression
211    Neg(Box<IntegerExpression<T>>),
212}
213
214/// Operators for comparing integer values
215#[derive(Debug, PartialEq, Eq, Hash, Clone, Copy, PartialOrd, Ord)]
216pub enum ComparisonOp {
217    /// Greater
218    Gt,
219    /// Greater equal
220    Geq,
221    /// Equal
222    Eq,
223    /// Not equal
224    Neq,
225    /// Less equal
226    Leq,
227    /// Less
228    Lt,
229}
230
231/// Connectives for boolean expressions
232#[derive(Debug, PartialEq, Eq, Hash, Clone, Copy, PartialOrd, Ord)]
233pub enum BooleanConnective {
234    /// And
235    And,
236    /// Or
237    Or,
238}
239
240/// Binary operators for Integer expressions
241#[derive(Debug, PartialEq, Eq, Hash, Clone, Copy, PartialOrd, Ord)]
242pub enum IntegerOp {
243    /// Addition
244    Add,
245    /// Subtraction
246    Sub,
247    /// Multiplication
248    Mul,
249    /// Division
250    Div,
251}
252
253impl Display for Parameter {
254    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
255        write!(f, "{}", self.0)
256    }
257}
258
259impl Display for Location {
260    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
261        write!(f, "{}", self.0)
262    }
263}
264
265impl Display for Variable {
266    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
267        write!(f, "{}", self.0)
268    }
269}
270
271impl<T: Atomic> Display for BooleanExpression<T> {
272    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
273        match self {
274            BooleanExpression::ComparisonExpression(lhs, op, rhs) => {
275                write!(f, "{lhs} {op} {rhs}")
276            }
277            BooleanExpression::BinaryExpression(lhs, op, rhs) => {
278                write!(f, "({lhs} {op} {rhs})")
279            }
280            BooleanExpression::True => write!(f, "true"),
281            BooleanExpression::False => write!(f, "false"),
282            BooleanExpression::Not(b) => write!(f, "!{b}"),
283        }
284    }
285}
286
287impl<T: Atomic> Display for IntegerExpression<T> {
288    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
289        match self {
290            IntegerExpression::Atom(a) => write!(f, "{a}"),
291            IntegerExpression::Const(c) => write!(f, "{c}"),
292            IntegerExpression::Param(p) => write!(f, "{p}"),
293            IntegerExpression::BinaryExpr(lhs, op, rhs) => write!(f, "({lhs} {op} {rhs})"),
294            IntegerExpression::Neg(ex) => write!(f, "-{ex}"),
295        }
296    }
297}
298
299impl Display for ComparisonOp {
300    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
301        match self {
302            ComparisonOp::Gt => write!(f, ">"),
303            ComparisonOp::Geq => write!(f, ">="),
304            ComparisonOp::Eq => write!(f, "=="),
305            ComparisonOp::Neq => write!(f, "!="),
306            ComparisonOp::Leq => write!(f, "<="),
307            ComparisonOp::Lt => write!(f, "<"),
308        }
309    }
310}
311
312impl Display for BooleanConnective {
313    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
314        match self {
315            BooleanConnective::And => write!(f, "&&"),
316            BooleanConnective::Or => write!(f, "||"),
317        }
318    }
319}
320
321impl Display for IntegerOp {
322    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
323        match self {
324            IntegerOp::Add => write!(f, "+"),
325            IntegerOp::Sub => write!(f, "-"),
326            IntegerOp::Mul => write!(f, "*"),
327            IntegerOp::Div => write!(f, "/"),
328        }
329    }
330}
331
332#[cfg(test)]
333mod tests {
334    use super::*;
335
336    #[test]
337    fn test_parameter_new() {
338        let param = Parameter::new("n");
339        assert_eq!(param.0, "n");
340    }
341
342    #[test]
343    fn test_variable_new() {
344        let var = Variable::new("x");
345        assert_eq!(var.0, "x");
346    }
347
348    #[test]
349    fn test_location_new() {
350        let loc = Location::new("start");
351        assert_eq!(loc.0, "start");
352    }
353
354    #[test]
355    fn test_constraint_display() {
356        let lhs = IntegerExpression::Atom(Variable::new("x"));
357        let rhs = IntegerExpression::Const(5);
358        let constraint = BooleanExpression::ComparisonExpression(
359            Box::new(lhs),
360            ComparisonOp::Geq,
361            Box::new(rhs),
362        );
363        assert_eq!(constraint.to_string(), "x >= 5");
364    }
365
366    #[test]
367    fn test_integer_expression_display() {
368        let lhs = IntegerExpression::Atom(Variable::new("x"));
369        let rhs = IntegerExpression::Const(5);
370        let expr = IntegerExpression::BinaryExpr(Box::new(lhs), IntegerOp::Add, Box::new(rhs));
371        assert_eq!(expr.to_string(), "(x + 5)");
372    }
373
374    #[test]
375    fn test_comparison_op_display() {
376        assert_eq!(ComparisonOp::Gt.to_string(), ">");
377        assert_eq!(ComparisonOp::Geq.to_string(), ">=");
378        assert_eq!(ComparisonOp::Eq.to_string(), "==");
379        assert_eq!(ComparisonOp::Neq.to_string(), "!=");
380        assert_eq!(ComparisonOp::Leq.to_string(), "<=");
381        assert_eq!(ComparisonOp::Lt.to_string(), "<");
382    }
383
384    #[test]
385    fn test_boolean_connective_display() {
386        assert_eq!(BooleanConnective::And.to_string(), "&&");
387        assert_eq!(BooleanConnective::Or.to_string(), "||");
388    }
389
390    #[test]
391    fn test_arithmetic_op_display() {
392        assert_eq!(IntegerOp::Add.to_string(), "+");
393        assert_eq!(IntegerOp::Sub.to_string(), "-");
394        assert_eq!(IntegerOp::Mul.to_string(), "*");
395        assert_eq!(IntegerOp::Div.to_string(), "/");
396    }
397
398    #[test]
399    fn test_negated_expression_display() {
400        let expr = -IntegerExpression::Atom(Variable::new("x"));
401        assert_eq!(expr.to_string(), "-x");
402    }
403
404    #[test]
405    fn test_binary_boolean_expression_display() {
406        let lhs = BooleanExpression::ComparisonExpression(
407            Box::new(IntegerExpression::Atom(Variable::new("x"))),
408            ComparisonOp::Gt,
409            Box::new(IntegerExpression::Const(0)),
410        );
411        let rhs = BooleanExpression::ComparisonExpression(
412            Box::new(IntegerExpression::Atom(Variable::new("y"))),
413            ComparisonOp::Lt,
414            Box::new(IntegerExpression::Const(10)),
415        );
416        let expr = lhs & rhs;
417        assert_eq!(expr.to_string(), "(x > 0 && y < 10)");
418    }
419
420    #[test]
421    fn test_true_boolean_expression_display() {
422        let expr: BooleanExpression<Location> = BooleanExpression::True;
423        assert_eq!(expr.to_string(), "true");
424    }
425
426    #[test]
427    fn test_false_boolean_expression_display() {
428        let expr: BooleanExpression<Location> = BooleanExpression::False;
429        assert_eq!(expr.to_string(), "false");
430    }
431
432    #[test]
433    fn test_not_boolean_expression_display() {
434        let expr: BooleanExpression<Location> = !BooleanExpression::True;
435        assert_eq!(expr.to_string(), "!true");
436    }
437}
taco_threshold_automaton/expressions.rs

taco_threshold_automaton/
expressions.rs
