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

taco_threshold_automaton/
expressions.rs
