taco_model_checker/
eltl.rs

1//! ELTL (LTL without next) expressions for threshold automata
2//!
3//! This module provides the types defining ELTL expressions  without a next
4//! operator for threshold automata. In the literature these formulas are also
5//! called ELTL or fault-tolerant temporal logic.
6//!
7//! Use the [`ELTLSpecificationBuilder`] to create a new ELTL specification, which
8//! is guaranteed to only contain variables, locations and parameters that are
9//! declared in the threshold automaton associated with the builder.
10//!
11//! Note that these ELTL formulas do not match the formal definition outlined in
12//! many papers. The reason for that is that benchmarks do not conform to the
13//! formal specification. We recommend using the more restricted internal
14//! specification types when writing a model checker.
15
16use std::{
17    collections::HashMap,
18    fmt,
19    ops::{BitAnd, BitOr, Not},
20    vec,
21};
22use taco_display_utils::TAB_SIZE;
23use taco_threshold_automaton::{
24    ThresholdAutomaton,
25    expressions::{
26        Atomic, BooleanExpression, ComparisonOp, IntegerExpression, IsDeclared, Location,
27        Parameter, Variable,
28    },
29};
30
31pub mod remove_negations;
32
33/// ELTL (LTL without next) expressions for threshold automata
34///
35/// This module provides the types defining ELTL expressions  without a next
36/// operator for threshold automata. In the literature these formulas are also
37/// called ELTL or fault-tolerant temporal logic.
38///
39/// # Example
40///
41/// ```
42/// use taco_threshold_automaton::expressions::{IntegerExpression, ComparisonOp, Location};
43/// use taco_model_checker::eltl::ELTLExpression;
44///
45/// // loc1 = 0 => □(loc_agree_1 = 0)
46/// let _ = ELTLExpression::Implies(
47///  Box::new(ELTLExpression::LocationExpr(
48///     Box::new(IntegerExpression::Atom(Location::new("loc1"))),
49///     ComparisonOp::Eq,
50///     Box::new(IntegerExpression::Const(0)),
51///  )),
52///  Box::new(ELTLExpression::Globally(
53///     Box::new(ELTLExpression::LocationExpr(
54///         Box::new(IntegerExpression::Atom(Location::new("loc_agree_1"))),
55///         ComparisonOp::Eq,
56///         Box::new(IntegerExpression::Const(0)),
57///     )),
58///  )));
59/// ```
60#[derive(Debug, Clone, PartialEq, Hash)]
61pub enum ELTLExpression {
62    /// Implication ⟹
63    Implies(Box<ELTLExpression>, Box<ELTLExpression>),
64    /// Globally □
65    Globally(Box<ELTLExpression>),
66    /// Eventually ◇
67    Eventually(Box<ELTLExpression>),
68    /// And ∧
69    And(Box<ELTLExpression>, Box<ELTLExpression>),
70    /// Or ∨
71    Or(Box<ELTLExpression>, Box<ELTLExpression>),
72    /// Not ¬
73    Not(Box<ELTLExpression>),
74    /// Boolean constraint over the number of processes in a location
75    LocationExpr(
76        Box<IntegerExpression<Location>>,
77        ComparisonOp,
78        Box<IntegerExpression<Location>>,
79    ),
80    /// Boolean constraint over the value of a variable
81    VariableExpr(
82        Box<IntegerExpression<Variable>>,
83        ComparisonOp,
84        Box<IntegerExpression<Variable>>,
85    ),
86    /// Expression over the value of parameters
87    ParameterExpr(
88        Box<IntegerExpression<Parameter>>,
89        ComparisonOp,
90        Box<IntegerExpression<Parameter>>,
91    ),
92    /// Always true
93    True,
94    /// Always false
95    False,
96}
97
98impl ELTLExpression {
99    /// Check if the expression contains a temporal operator
100    ///
101    /// Returns `true` if the expression contains a temporal operator,
102    /// otherwise `false`
103    ///
104    /// # Example
105    ///
106    /// ```
107    /// use taco_threshold_automaton::expressions::{IntegerExpression, ComparisonOp, Location};
108    /// use taco_model_checker::eltl::ELTLExpression;
109    ///
110    /// let expression = ELTLExpression::LocationExpr(
111    ///     Box::new(IntegerExpression::Atom(Location::new("loc1"))),
112    ///     ComparisonOp::Eq,
113    ///     Box::new(IntegerExpression::Atom(Location::new("loc2"))),
114    /// );
115    /// assert!(!expression.contains_temporal_operator());
116    ///
117    /// let expression = ELTLExpression::Globally(Box::new(ELTLExpression::LocationExpr(
118    ///     Box::new(IntegerExpression::Atom(Location::new("loc1"))),
119    ///     ComparisonOp::Eq,
120    ///     Box::new(IntegerExpression::Atom(Location::new("loc2"))),
121    /// )));
122    /// assert!(expression.contains_temporal_operator());
123    /// ```
124    pub fn contains_temporal_operator(&self) -> bool {
125        match self {
126            ELTLExpression::Globally(_) | ELTLExpression::Eventually(_) => true,
127            ELTLExpression::True
128            | ELTLExpression::False
129            | ELTLExpression::LocationExpr(_, _, _)
130            | ELTLExpression::ParameterExpr(_, _, _)
131            | ELTLExpression::VariableExpr(_, _, _) => false,
132            ELTLExpression::Implies(lhs, rhs) => {
133                lhs.contains_temporal_operator() || rhs.contains_temporal_operator()
134            }
135            ELTLExpression::And(lhs, rhs) | ELTLExpression::Or(lhs, rhs) => {
136                lhs.contains_temporal_operator() || rhs.contains_temporal_operator()
137            }
138            ELTLExpression::Not(expr) => expr.contains_temporal_operator(),
139        }
140    }
141}
142
143impl Not for ELTLExpression {
144    type Output = Self;
145
146    fn not(self) -> Self::Output {
147        ELTLExpression::Not(Box::new(self))
148    }
149}
150
151impl BitAnd for ELTLExpression {
152    type Output = Self;
153
154    fn bitand(self, rhs: Self) -> Self::Output {
155        ELTLExpression::And(Box::new(self), Box::new(rhs))
156    }
157}
158
159impl BitOr for ELTLExpression {
160    type Output = Self;
161
162    fn bitor(self, rhs: Self) -> Self::Output {
163        ELTLExpression::Or(Box::new(self), Box::new(rhs))
164    }
165}
166
167impl fmt::Display for ELTLExpression {
168    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
169        match self {
170            ELTLExpression::Implies(lhs, rhs) => write!(f, "({lhs}) -> ({rhs})"),
171            ELTLExpression::Globally(expression) => write!(f, "[]({expression})"),
172            ELTLExpression::Eventually(expression) => write!(f, "<>({expression})"),
173            ELTLExpression::And(lhs, rhs) => write!(f, "({lhs}) && ({rhs})"),
174            ELTLExpression::Or(lhs, rhs) => write!(f, "({lhs}) || ({rhs})"),
175            ELTLExpression::Not(expression) => write!(f, "!({expression})"),
176            ELTLExpression::LocationExpr(lhs, op, rhs) => write!(f, "{lhs} {op} {rhs}"),
177            ELTLExpression::VariableExpr(lhs, op, rhs) => write!(f, "{lhs} {op} {rhs}"),
178            ELTLExpression::ParameterExpr(lhs, op, rhs) => write!(f, "{lhs} {op} {rhs}"),
179            ELTLExpression::True => write!(f, "true"),
180            ELTLExpression::False => write!(f, "false"),
181        }
182    }
183}
184
185/// [`ELTLExpression`] with associated name
186///
187/// This type represents an ELTLExpression that has a name associated with it
188pub type ELTLProperty = (String, ELTLExpression);
189
190/// A collection of [`ELTLProperty`] that in conjunction describe correct
191/// behavior
192///
193/// An [`ELTLSpecification`] is a collection of [`ELTLProperty`]s (i.e.,
194/// collection of named [`ELTLExpression`]s) that describe the desired behavior
195/// of a threshold automaton. If threshold automaton fulfills all of the
196/// properties, it can be considered safe with respect to the specification
197#[derive(Debug, Clone, PartialEq)]
198pub struct ELTLSpecification {
199    /// Expressions and their associated names
200    expressions: Vec<ELTLProperty>,
201}
202
203impl ELTLSpecification {
204    /// Get a slice of the contained [`ELTLProperty`]s
205    pub fn expressions(&self) -> &[ELTLProperty] {
206        &self.expressions
207    }
208}
209
210impl IntoIterator for ELTLSpecification {
211    type Item = ELTLProperty;
212    type IntoIter = vec::IntoIter<Self::Item>;
213
214    fn into_iter(self) -> Self::IntoIter {
215        self.expressions.into_iter()
216    }
217}
218
219impl fmt::Display for ELTLSpecification {
220    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
221        writeln!(f, "specifications({}) {{", self.expressions.len())?;
222        let indent = " ".repeat(TAB_SIZE);
223
224        for (name, expression) in &self.expressions {
225            writeln!(f, "{indent}{name}: {expression};")?;
226        }
227
228        write!(f, "}}")
229    }
230}
231
232/// Builder for building an [`ELTLSpecification`] over a threshold automaton
233///
234/// # Example
235///
236/// ```
237/// use taco_threshold_automaton::general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder;
238/// use taco_threshold_automaton::expressions::{IntegerExpression, ComparisonOp, Location, Variable};
239/// use taco_model_checker::eltl::{ELTLExpression, ELTLSpecificationBuilder};
240///
241/// let ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
242///     .with_variables(vec![
243///         Variable::new("var1"),
244///         Variable::new("var2"),
245///         Variable::new("var3"),
246///     ])
247///     .unwrap()
248///     .with_locations(vec![
249///         Location::new("loc1"),
250///         Location::new("loc2"),
251///     ])
252///     .unwrap()
253///     .initialize()
254///     .build();
255///
256/// let mut builder = ELTLSpecificationBuilder::new(&ta);
257///
258/// let expr1 = ELTLExpression::LocationExpr(
259///     Box::new(IntegerExpression::Atom(Location::new("loc1"))),
260///     ComparisonOp::Eq,
261///     Box::new(IntegerExpression::Const(2)),
262/// );
263///
264/// let expr2 = ELTLExpression::LocationExpr(
265///     Box::new(IntegerExpression::Atom(Location::new("loc2"))),
266///     ComparisonOp::Eq,
267///     Box::new(IntegerExpression::Const(0)),
268/// );
269///
270/// builder.add_expressions(vec![
271///     ("spec1".to_string(), expr1),
272///     ("spec2".to_string(), expr2),
273/// ]).unwrap();
274///
275/// let spec = builder.build();
276///
277/// assert_eq!(spec.expressions().len(), 2);
278/// assert!(spec.expressions().iter().any(|(name, _)| name == "spec1"));
279/// assert!(spec.expressions().iter().any(|(name, _)| name == "spec2"));
280/// ```
281pub struct ELTLSpecificationBuilder<'a, T: ThresholdAutomaton> {
282    /// Threshold automaton associated with the expressions
283    ta: &'a T,
284    /// Collection of tuples of expression names and the ELTL expression
285    properties: Vec<ELTLProperty>,
286}
287
288impl<T: ThresholdAutomaton> ELTLSpecificationBuilder<'_, T> {
289    /// Check if all identifiers in the expression are known
290    ///
291    /// Returns `()` if no unknown identifier is found, otherwise the name of
292    /// the unknown identifier
293    fn check_for_unknown_identifier<S>(
294        &self,
295        expr: &IntegerExpression<S>,
296    ) -> Result<(), InternalELTLExpressionBuilderError>
297    where
298        S: Atomic,
299        Self: IsDeclared<S>,
300    {
301        match expr {
302            IntegerExpression::Atom(a) => {
303                if self.is_declared(a) {
304                    Ok(())
305                } else {
306                    Err(InternalELTLExpressionBuilderError::UnknownIdentifier(
307                        a.to_string(),
308                    ))
309                }
310            }
311            IntegerExpression::Const(_) => Ok(()),
312            IntegerExpression::Param(p) => {
313                if self.ta.is_declared(p) {
314                    Ok(())
315                } else {
316                    Err(InternalELTLExpressionBuilderError::UnknownIdentifier(
317                        p.to_string(),
318                    ))
319                }
320            }
321            IntegerExpression::BinaryExpr(lhs, _op, rhs) => {
322                self.check_for_unknown_identifier(lhs)?;
323                self.check_for_unknown_identifier(rhs)
324            }
325            IntegerExpression::Neg(expr) => self.check_for_unknown_identifier(expr),
326        }
327    }
328
329    /// Check whether an ELTL expression contains a parameter expression
330    fn check_contains_parameter_expression(
331        expr: &ELTLExpression,
332    ) -> Result<(), InternalELTLExpressionBuilderError> {
333        match expr {
334            ELTLExpression::Implies(lhs, rhs)
335            | ELTLExpression::And(lhs, rhs)
336            | ELTLExpression::Or(lhs, rhs) => {
337                Self::check_contains_parameter_expression(lhs)?;
338                Self::check_contains_parameter_expression(rhs)
339            }
340            ELTLExpression::Globally(expr)
341            | ELTLExpression::Eventually(expr)
342            | ELTLExpression::Not(expr) => Self::check_contains_parameter_expression(expr),
343            ELTLExpression::True
344            | ELTLExpression::False
345            | ELTLExpression::LocationExpr(_, _, _)
346            | ELTLExpression::VariableExpr(_, _, _) => Ok(()),
347            ELTLExpression::ParameterExpr(lhs, op, rhs) => Err(
348                InternalELTLExpressionBuilderError::ParameterExprBehindTemporalOperator(
349                    lhs.clone(),
350                    *op,
351                    rhs.clone(),
352                ),
353            ),
354        }
355    }
356
357    /// Replaces parameter expressions that do not contain parameters
358    fn replace_trivial_expressions(expr: ELTLExpression) -> ELTLExpression {
359        match expr {
360            ELTLExpression::Globally(expr) => {
361                ELTLExpression::Globally(Box::new(Self::replace_trivial_expressions(*expr)))
362            }
363            ELTLExpression::Eventually(expr) => {
364                ELTLExpression::Eventually(Box::new(Self::replace_trivial_expressions(*expr)))
365            }
366            ELTLExpression::Not(expr) => {
367                ELTLExpression::Not(Box::new(Self::replace_trivial_expressions(*expr)))
368            }
369            ELTLExpression::Implies(lhs, rhs) => ELTLExpression::Implies(
370                Box::new(Self::replace_trivial_expressions(*lhs)),
371                Box::new(Self::replace_trivial_expressions(*rhs)),
372            ),
373            ELTLExpression::And(lhs, rhs) => ELTLExpression::And(
374                Box::new(Self::replace_trivial_expressions(*lhs)),
375                Box::new(Self::replace_trivial_expressions(*rhs)),
376            ),
377            ELTLExpression::Or(lhs, rhs) => ELTLExpression::Or(
378                Box::new(Self::replace_trivial_expressions(*lhs)),
379                Box::new(Self::replace_trivial_expressions(*rhs)),
380            ),
381            ELTLExpression::LocationExpr(lhs, op, rhs) => {
382                ELTLExpression::LocationExpr(lhs, op, rhs)
383            }
384            ELTLExpression::VariableExpr(lhs, op, rhs) => {
385                ELTLExpression::VariableExpr(lhs, op, rhs)
386            }
387            ELTLExpression::ParameterExpr(lhs, op, rhs) => {
388                if let Ok(eval) =
389                    BooleanExpression::ComparisonExpression(lhs.clone(), op, rhs.clone())
390                        .check_satisfied(&HashMap::new(), &HashMap::new())
391                {
392                    if eval {
393                        return ELTLExpression::True;
394                    }
395                    return ELTLExpression::False;
396                }
397                ELTLExpression::ParameterExpr(lhs, op, rhs)
398            }
399            ELTLExpression::True => ELTLExpression::True,
400            ELTLExpression::False => ELTLExpression::False,
401        }
402    }
403
404    /// Check if all atoms in the expression are known in the threshold
405    /// automaton associated with the builder and that all location expressions
406    /// are valid
407    fn validate_property(
408        &self,
409        expr: &ELTLExpression,
410    ) -> Result<(), InternalELTLExpressionBuilderError> {
411        match expr {
412            ELTLExpression::Implies(lhs, rhs) => {
413                self.validate_property(lhs)?;
414                self.validate_property(rhs)
415            }
416            ELTLExpression::Globally(expression) | ELTLExpression::Eventually(expression) => {
417                Self::check_contains_parameter_expression(expr)?;
418                self.validate_property(expression)
419            }
420            ELTLExpression::And(lhs, rhs) => {
421                self.validate_property(lhs)?;
422                self.validate_property(rhs)
423            }
424            ELTLExpression::Or(lhs, rhs) => {
425                self.validate_property(lhs)?;
426                self.validate_property(rhs)
427            }
428            ELTLExpression::Not(expression) => self.validate_property(expression),
429            ELTLExpression::LocationExpr(lhs, _, rhs) => {
430                self.check_for_unknown_identifier(lhs)?;
431                self.check_for_unknown_identifier(rhs)
432            }
433            ELTLExpression::VariableExpr(lhs, _, rhs) => {
434                self.check_for_unknown_identifier(lhs)?;
435                self.check_for_unknown_identifier(rhs)
436            }
437            ELTLExpression::ParameterExpr(lhs, _, rhs) => {
438                self.check_for_unknown_identifier(lhs)?;
439                self.check_for_unknown_identifier(rhs)
440            }
441            ELTLExpression::True | ELTLExpression::False => Ok(()),
442        }
443    }
444
445    /// Add a new ELTL expression to the specification
446    ///
447    /// This function checks if all atoms in the expression are known in the
448    /// threshold automaton associated with the builder. If an unknown atom is
449    /// found, an error is returned. Otherwise the expression is added to the
450    /// specification.
451    ///
452    /// This function also returns an error if the name of the expression is
453    /// already used in the specification.
454    pub fn add_expression(
455        &mut self,
456        name: String,
457        expr: ELTLExpression,
458    ) -> Result<(), ELTLExpressionBuilderError> {
459        // check whether a property with the same name has already been added
460        if self.properties.iter().any(|(n, _)| *n == name) {
461            return Err(ELTLExpressionBuilderError::DuplicateName {
462                property_name: name,
463            });
464        }
465
466        // remove trivial parameter constraints
467        let expr = Self::replace_trivial_expressions(expr);
468
469        // validate the new property
470        self.validate_property(&expr)
471            .map_err(|internal_err| internal_err.into_builder_error(name.clone(), expr.clone()))?;
472
473        self.properties.push((name, expr));
474        Ok(())
475    }
476
477    /// Add multiple ELTL expressions to the specification
478    ///
479    /// This function checks if all atoms in the expression are known in the
480    /// threshold automaton associated with the builder. If an unknown atom is
481    /// found, an error is returned. Otherwise the expression is added to the
482    /// specification.
483    ///
484    /// This function also returns an error if the name of the expression is
485    /// already used in the specification.
486    pub fn add_expressions(
487        &mut self,
488        expressions: impl IntoIterator<Item = ELTLProperty>,
489    ) -> Result<(), ELTLExpressionBuilderError> {
490        for (name, expression) in expressions {
491            self.add_expression(name, expression)?;
492        }
493        Ok(())
494    }
495
496    /// Build the ELTL specification
497    ///
498    /// Returns the ELTL specification containing all added expressions
499    pub fn build(self) -> ELTLSpecification {
500        ELTLSpecification {
501            expressions: self.properties,
502        }
503    }
504}
505
506impl<'a, T: ThresholdAutomaton> ELTLSpecificationBuilder<'a, T> {
507    /// Create a new empty ELTL specification builder
508    pub fn new(ta: &'a T) -> Self {
509        ELTLSpecificationBuilder {
510            ta,
511            properties: Vec::new(),
512        }
513    }
514}
515
516impl<T: ThresholdAutomaton> IsDeclared<Variable> for ELTLSpecificationBuilder<'_, T> {
517    fn is_declared(&self, obj: &Variable) -> bool {
518        self.ta.is_declared(obj)
519    }
520}
521
522impl<T: ThresholdAutomaton> IsDeclared<Location> for ELTLSpecificationBuilder<'_, T> {
523    fn is_declared(&self, obj: &Location) -> bool {
524        self.ta.is_declared(obj)
525    }
526}
527
528impl<T: ThresholdAutomaton> IsDeclared<Parameter> for ELTLSpecificationBuilder<'_, T> {
529    fn is_declared(&self, obj: &Parameter) -> bool {
530        self.ta.is_declared(obj)
531    }
532}
533
534/// Errors that can occur when building ELTL expressions over a threshold automaton
535#[derive(Debug, Clone, PartialEq)]
536pub enum ELTLExpressionBuilderError {
537    /// Found an unknown atomic identifier
538    UnknownIdentifier {
539        /// Name of the ELTL expression
540        property_name: String,
541        /// Expression containing the unknown identifier
542        expr: Box<ELTLExpression>,
543        /// Unknown identifier
544        ident: String,
545    },
546    /// Tried to add a specification with the same name twice to the specification
547    DuplicateName {
548        /// Name of the expression
549        property_name: String,
550    },
551    /// Found an expression over parameters behind a temporal operator, which syntax is not defined
552    ParameterConstraintBehindTemporalOperator {
553        /// lhs of the constraint
554        lhs: Box<IntegerExpression<Parameter>>,
555        /// Comparison operator of the constraint
556        op: ComparisonOp,
557        /// rhs of the constraint
558        rhs: Box<IntegerExpression<Parameter>>,
559        /// Name of the expression
560        property_name: String,
561    },
562}
563
564/// Internal error type without the higher level property name
565enum InternalELTLExpressionBuilderError {
566    UnknownIdentifier(String),
567    ParameterExprBehindTemporalOperator(
568        Box<IntegerExpression<Parameter>>,
569        ComparisonOp,
570        Box<IntegerExpression<Parameter>>,
571    ),
572}
573
574impl InternalELTLExpressionBuilderError {
575    fn into_builder_error(
576        self,
577        property_name: String,
578        expr: ELTLExpression,
579    ) -> ELTLExpressionBuilderError {
580        match self {
581            InternalELTLExpressionBuilderError::UnknownIdentifier(ident) => {
582                ELTLExpressionBuilderError::UnknownIdentifier {
583                    property_name,
584                    expr: Box::new(expr),
585                    ident,
586                }
587            }
588            InternalELTLExpressionBuilderError::ParameterExprBehindTemporalOperator(
589                lhs,
590                op,
591                rhs,
592            ) => ELTLExpressionBuilderError::ParameterConstraintBehindTemporalOperator {
593                lhs,
594                op,
595                rhs,
596                property_name,
597            },
598        }
599    }
600}
601
602impl std::error::Error for ELTLExpressionBuilderError {}
603
604impl fmt::Display for ELTLExpressionBuilderError {
605    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
606        match self {
607            ELTLExpressionBuilderError::UnknownIdentifier {
608                property_name: name,
609                expr: _,
610                ident,
611            } => {
612                write!(
613                    f,
614                    "Unknown identifier in specification '{name}': Identifier '{ident}' not known as parameter, location or variable"
615                )
616            }
617            ELTLExpressionBuilderError::DuplicateName {
618                property_name: name,
619            } => {
620                write!(
621                    f,
622                    "Duplicate name in specification: The name '{name}' is defined twice in the specification"
623                )
624            }
625            ELTLExpressionBuilderError::ParameterConstraintBehindTemporalOperator {
626                lhs,
627                op,
628                rhs,
629                property_name,
630            } => write!(
631                f,
632                "Constraint over parameters values found behind temporal operator in specification '{property_name}'. The constraint '{lhs} {op} {rhs}' only constrains the value of parameters, which do not update over time. Still the constraint appears behind a temporal operator. This is likely a mistake"
633            ),
634        }
635    }
636}
637
638#[cfg(test)]
639mod tests {
640    use std::vec;
641
642    use crate::eltl::ELTLExpressionBuilderError;
643
644    use super::{ELTLExpression, ELTLSpecificationBuilder};
645    use taco_threshold_automaton::expressions::{
646        ComparisonOp, IntegerExpression, IntegerOp, Location, Parameter, Variable,
647    };
648
649    use taco_threshold_automaton::general_threshold_automaton::builder::{
650        GeneralThresholdAutomatonBuilder, RuleBuilder,
651    };
652    use taco_threshold_automaton::general_threshold_automaton::{
653        Action, GeneralThresholdAutomaton,
654    };
655    use taco_threshold_automaton::{BooleanVarConstraint, LocationConstraint, ParameterConstraint};
656
657    lazy_static::lazy_static! {
658        static ref TEST_TA: GeneralThresholdAutomaton = {
659            GeneralThresholdAutomatonBuilder::new("test_ta1")
660            .with_parameters(vec![
661                Parameter::new("n"),
662                Parameter::new("t"),
663                Parameter::new("f"),
664            ])
665            .unwrap()
666            .with_variables(vec![
667                Variable::new("var1"),
668                Variable::new("var2"),
669                Variable::new("var3"),
670            ])
671            .unwrap()
672            .with_locations(vec![
673                Location::new("loc1"),
674                Location::new("loc2"),
675                Location::new("loc3"),
676            ])
677            .unwrap()
678            .initialize()
679            .with_initial_variable_constraints(vec![BooleanVarConstraint::ComparisonExpression(
680                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
681                ComparisonOp::Eq,
682                Box::new(IntegerExpression::Const(1)),
683            )])
684            .unwrap()
685            .with_initial_location_constraints(vec![
686                LocationConstraint::ComparisonExpression(
687                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
688                    ComparisonOp::Eq,
689                    Box::new(
690                        IntegerExpression::Param(Parameter::new("n"))
691                            - IntegerExpression::Param(Parameter::new("f")),
692                    ),
693                ) & LocationConstraint::ComparisonExpression(
694                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
695                    ComparisonOp::Eq,
696                    Box::new(IntegerExpression::Const(0)),
697                ),
698            ])
699            .unwrap()
700            .with_resilience_conditions(vec![ParameterConstraint::ComparisonExpression(
701                Box::new(IntegerExpression::Atom(Parameter::new("n"))),
702                ComparisonOp::Gt,
703                Box::new(IntegerExpression::BinaryExpr(
704                    Box::new(IntegerExpression::Const(3)),
705                    IntegerOp::Mul,
706                    Box::new(IntegerExpression::Atom(Parameter::new("f"))),
707                )),
708            )])
709            .unwrap()
710            .with_rules(vec![
711                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2"))
712                    .with_actions(vec![Action::new(
713                        Variable::new("var1"),
714                        IntegerExpression::Atom(Variable::new("var1")),
715                    )
716                    .unwrap()])
717                    .build(),
718                RuleBuilder::new(1, Location::new("loc2"), Location::new("loc3"))
719                    .with_guard(
720                        BooleanVarConstraint::ComparisonExpression(
721                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
722                            ComparisonOp::Eq,
723                            Box::new(IntegerExpression::Const(1)),
724                        ) & BooleanVarConstraint::ComparisonExpression(
725                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
726                            ComparisonOp::Eq,
727                            Box::new(IntegerExpression::Param(Parameter::new("n")) - IntegerExpression::Const(2)),
728                        ),
729                    )
730                    .with_actions(vec![
731                        Action::new(Variable::new("var3"), IntegerExpression::Const(0)).unwrap(),
732                        Action::new(
733                            Variable::new("var1"),
734                            IntegerExpression::BinaryExpr(
735                                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
736                                IntegerOp::Add,
737                                Box::new(IntegerExpression::Const(1)),
738                            ),
739                        )
740                        .unwrap(),
741                    ])
742                    .build(),
743            ])
744            .unwrap()
745            .build()
746        };
747    }
748
749    #[test]
750    fn test_contains_temporal_operator() {
751        let expression = ELTLExpression::LocationExpr(
752            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
753            ComparisonOp::Eq,
754            Box::new(IntegerExpression::Atom(Location::new("loc2"))),
755        );
756        assert!(!expression.contains_temporal_operator());
757
758        let expression = ELTLExpression::Implies(
759            Box::new(ELTLExpression::LocationExpr(
760                Box::new(IntegerExpression::Atom(Location::new("loc1"))),
761                ComparisonOp::Eq,
762                Box::new(IntegerExpression::Atom(Location::new("loc2"))),
763            )),
764            Box::new(ELTLExpression::LocationExpr(
765                Box::new(IntegerExpression::Atom(Location::new("loc3"))),
766                ComparisonOp::Eq,
767                Box::new(IntegerExpression::Atom(Location::new("loc4"))),
768            )),
769        );
770        assert!(!expression.contains_temporal_operator());
771
772        let expression = ELTLExpression::Globally(Box::new(ELTLExpression::LocationExpr(
773            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
774            ComparisonOp::Eq,
775            Box::new(IntegerExpression::Atom(Location::new("loc2"))),
776        )));
777        assert!(expression.contains_temporal_operator());
778
779        let expression = ELTLExpression::Eventually(Box::new(ELTLExpression::LocationExpr(
780            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
781            ComparisonOp::Eq,
782            Box::new(IntegerExpression::Atom(Location::new("loc2"))),
783        )));
784        assert!(expression.contains_temporal_operator());
785
786        let expression = ELTLExpression::And(
787            Box::new(ELTLExpression::LocationExpr(
788                Box::new(IntegerExpression::Atom(Location::new("loc1"))),
789                ComparisonOp::Eq,
790                Box::new(IntegerExpression::Atom(Location::new("loc2"))),
791            )),
792            Box::new(ELTLExpression::VariableExpr(
793                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
794                ComparisonOp::Eq,
795                Box::new(IntegerExpression::Atom(Variable::new("var2"))),
796            )),
797        );
798        assert!(!expression.contains_temporal_operator());
799
800        let expression = ELTLExpression::Or(
801            Box::new(ELTLExpression::LocationExpr(
802                Box::new(IntegerExpression::Atom(Location::new("loc1"))),
803                ComparisonOp::Eq,
804                Box::new(IntegerExpression::Atom(Location::new("loc2"))),
805            )),
806            Box::new(ELTLExpression::Not(Box::new(ELTLExpression::LocationExpr(
807                Box::new(IntegerExpression::Atom(Location::new("loc3"))),
808                ComparisonOp::Eq,
809                Box::new(IntegerExpression::Atom(Location::new("loc4"))),
810            )))),
811        );
812        assert!(!expression.contains_temporal_operator());
813    }
814
815    #[test]
816    fn test_ltl_expression_display() {
817        let expression = ELTLExpression::True;
818        assert_eq!(format!("{expression}"), "true");
819
820        let expression = ELTLExpression::False;
821        assert_eq!(format!("{expression}"), "false");
822
823        let expression = ELTLExpression::LocationExpr(
824            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
825            ComparisonOp::Eq,
826            Box::new(IntegerExpression::Atom(Location::new("loc2"))),
827        );
828        assert_eq!(format!("{expression}"), "loc1 == loc2");
829
830        let expression = ELTLExpression::Implies(
831            Box::new(ELTLExpression::LocationExpr(
832                Box::new(IntegerExpression::Atom(Location::new("loc1"))),
833                ComparisonOp::Eq,
834                Box::new(IntegerExpression::Atom(Location::new("loc2"))),
835            )),
836            Box::new(ELTLExpression::LocationExpr(
837                Box::new(IntegerExpression::Atom(Location::new("loc3"))),
838                ComparisonOp::Eq,
839                Box::new(IntegerExpression::Atom(Location::new("loc4"))),
840            )),
841        );
842        assert_eq!(format!("{expression}"), "(loc1 == loc2) -> (loc3 == loc4)");
843
844        let expression = ELTLExpression::Globally(Box::new(ELTLExpression::LocationExpr(
845            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
846            ComparisonOp::Eq,
847            Box::new(IntegerExpression::Atom(Location::new("loc2"))),
848        )));
849        assert_eq!(format!("{expression}"), "[](loc1 == loc2)");
850
851        let expression = ELTLExpression::Eventually(Box::new(ELTLExpression::LocationExpr(
852            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
853            ComparisonOp::Eq,
854            Box::new(IntegerExpression::Atom(Location::new("loc2"))),
855        )));
856        assert_eq!(format!("{expression}"), "<>(loc1 == loc2)");
857
858        let expression = ELTLExpression::And(
859            Box::new(ELTLExpression::LocationExpr(
860                Box::new(IntegerExpression::Atom(Location::new("loc1"))),
861                ComparisonOp::Eq,
862                Box::new(IntegerExpression::Atom(Location::new("loc2"))),
863            )),
864            Box::new(ELTLExpression::LocationExpr(
865                Box::new(IntegerExpression::Atom(Location::new("loc3"))),
866                ComparisonOp::Eq,
867                Box::new(IntegerExpression::Atom(Location::new("loc4"))),
868            )),
869        );
870        assert_eq!(format!("{expression}"), "(loc1 == loc2) && (loc3 == loc4)");
871
872        let expression = ELTLExpression::Or(
873            Box::new(ELTLExpression::LocationExpr(
874                Box::new(IntegerExpression::Atom(Location::new("loc1"))),
875                ComparisonOp::Eq,
876                Box::new(IntegerExpression::Atom(Location::new("loc2"))),
877            )),
878            Box::new(ELTLExpression::LocationExpr(
879                Box::new(IntegerExpression::Atom(Location::new("loc3"))),
880                ComparisonOp::Eq,
881                Box::new(IntegerExpression::Atom(Location::new("loc4"))),
882            )),
883        );
884        assert_eq!(format!("{expression}"), "(loc1 == loc2) || (loc3 == loc4)");
885
886        let expression = ELTLExpression::Not(Box::new(ELTLExpression::LocationExpr(
887            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
888            ComparisonOp::Eq,
889            Box::new(IntegerExpression::Atom(Location::new("loc2"))),
890        )));
891        assert_eq!(format!("{expression}"), "!(loc1 == loc2)");
892    }
893
894    #[test]
895    fn test_display_ltl_specification() {
896        use super::{ELTLExpression, ELTLSpecification};
897        use taco_threshold_automaton::expressions::{ComparisonOp, IntegerExpression, Location};
898
899        let spec = ELTLSpecification {
900            expressions: vec![
901                (
902                    "spec1".to_string(),
903                    ELTLExpression::LocationExpr(
904                        Box::new(IntegerExpression::Atom(Location::new("loc1"))),
905                        ComparisonOp::Eq,
906                        Box::new(IntegerExpression::Atom(Location::new("loc2"))),
907                    ),
908                ),
909                (
910                    "spec2".to_string(),
911                    ELTLExpression::LocationExpr(
912                        Box::new(IntegerExpression::Atom(Location::new("loc3"))),
913                        ComparisonOp::Eq,
914                        Box::new(IntegerExpression::Atom(Location::new("loc4"))),
915                    ),
916                ),
917                (
918                    "spec3".to_string(),
919                    ELTLExpression::VariableExpr(
920                        Box::new(IntegerExpression::Atom(Variable::new("var1"))),
921                        ComparisonOp::Eq,
922                        Box::new(IntegerExpression::Param(Parameter::new("n"))),
923                    ),
924                ),
925            ],
926        };
927
928        assert_eq!(
929            format!("{spec}"),
930            "specifications(3) {\n    spec1: loc1 == loc2;\n    spec2: loc3 == loc4;\n    spec3: var1 == n;\n}"
931        );
932    }
933
934    #[test]
935    fn test_operator_impl() {
936        let ltl = ELTLExpression::True & ELTLExpression::False;
937        let expected = ELTLExpression::And(
938            Box::new(ELTLExpression::True),
939            Box::new(ELTLExpression::False),
940        );
941
942        assert_eq!(ltl, expected);
943
944        let ltl = ELTLExpression::True | ELTLExpression::False;
945        let expected = ELTLExpression::Or(
946            Box::new(ELTLExpression::True),
947            Box::new(ELTLExpression::False),
948        );
949
950        assert_eq!(ltl, expected);
951    }
952
953    #[test]
954    fn test_getter_ltl_specification() {
955        use super::{ELTLExpression, ELTLSpecification};
956        use taco_threshold_automaton::expressions::{ComparisonOp, IntegerExpression, Location};
957
958        let spec = ELTLSpecification {
959            expressions: vec![
960                (
961                    "spec1".to_string(),
962                    ELTLExpression::LocationExpr(
963                        Box::new(IntegerExpression::Atom(Location::new("loc1"))),
964                        ComparisonOp::Eq,
965                        Box::new(IntegerExpression::Atom(Location::new("loc2"))),
966                    ),
967                ),
968                (
969                    "spec2".to_string(),
970                    ELTLExpression::LocationExpr(
971                        Box::new(IntegerExpression::Atom(Location::new("loc3"))),
972                        ComparisonOp::Eq,
973                        Box::new(IntegerExpression::Atom(Location::new("loc4"))),
974                    ),
975                ),
976            ],
977        };
978
979        assert_eq!(spec.expressions().len(), 2);
980        assert_eq!(
981            spec.expressions(),
982            &[
983                (
984                    "spec1".to_string(),
985                    ELTLExpression::LocationExpr(
986                        Box::new(IntegerExpression::Atom(Location::new("loc1"))),
987                        ComparisonOp::Eq,
988                        Box::new(IntegerExpression::Atom(Location::new("loc2"))),
989                    ),
990                ),
991                (
992                    "spec2".to_string(),
993                    ELTLExpression::LocationExpr(
994                        Box::new(IntegerExpression::Atom(Location::new("loc3"))),
995                        ComparisonOp::Eq,
996                        Box::new(IntegerExpression::Atom(Location::new("loc4"))),
997                    ),
998                ),
999            ]
1000        );
1001    }
1002
1003    #[test]
1004    fn test_ltl_builder_add_expressions() {
1005        let ta = TEST_TA.clone();
1006
1007        let mut builder = ELTLSpecificationBuilder::new(&ta);
1008
1009        let expr1 = ELTLExpression::LocationExpr(
1010            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1011            ComparisonOp::Eq,
1012            Box::new(IntegerExpression::Const(2)),
1013        );
1014
1015        let expr2 = ELTLExpression::LocationExpr(
1016            Box::new(IntegerExpression::Atom(Location::new("loc3"))),
1017            ComparisonOp::Eq,
1018            Box::new(-IntegerExpression::Const(3)),
1019        );
1020
1021        let expr3 = ELTLExpression::True;
1022
1023        builder
1024            .add_expressions(vec![
1025                ("spec1".to_string(), expr1),
1026                ("spec2".to_string(), expr2),
1027                ("spec3".to_string(), expr3),
1028            ])
1029            .unwrap();
1030
1031        let spec = builder.build();
1032        assert_eq!(spec.expressions().len(), 3);
1033        assert_eq!(
1034            spec.expressions(),
1035            &[
1036                (
1037                    "spec1".to_string(),
1038                    ELTLExpression::LocationExpr(
1039                        Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1040                        ComparisonOp::Eq,
1041                        Box::new(IntegerExpression::Const(2)),
1042                    ),
1043                ),
1044                (
1045                    "spec2".to_string(),
1046                    ELTLExpression::LocationExpr(
1047                        Box::new(IntegerExpression::Atom(Location::new("loc3"))),
1048                        ComparisonOp::Eq,
1049                        Box::new(-IntegerExpression::Const(3)),
1050                    ),
1051                ),
1052                ("spec3".to_string(), ELTLExpression::True),
1053            ]
1054        );
1055    }
1056
1057    #[test]
1058    fn test_ltl_expr_builder_removes_trivial_param_expr() {
1059        let ta = TEST_TA.clone();
1060
1061        let mut builder = ELTLSpecificationBuilder::new(&ta);
1062
1063        let expr = ELTLExpression::ParameterExpr(
1064            Box::new(IntegerExpression::Const(2)),
1065            ComparisonOp::Eq,
1066            Box::new(IntegerExpression::Const(2)),
1067        );
1068
1069        builder
1070            .add_expressions(vec![("spec1".to_string(), expr)])
1071            .unwrap();
1072
1073        let spec = builder.build();
1074
1075        assert_eq!(spec.expressions().len(), 1);
1076        assert_eq!(
1077            spec.expressions(),
1078            &[("spec1".to_string(), ELTLExpression::True),]
1079        );
1080
1081        let mut builder = ELTLSpecificationBuilder::new(&ta);
1082
1083        let expr1 = ELTLExpression::Globally(Box::new(ELTLExpression::ParameterExpr(
1084            Box::new(IntegerExpression::Const(2)),
1085            ComparisonOp::Neq,
1086            Box::new(IntegerExpression::Const(2)),
1087        )));
1088
1089        builder
1090            .add_expressions(vec![("spec1".to_string(), expr1)])
1091            .unwrap();
1092
1093        let spec = builder.build();
1094
1095        assert_eq!(spec.expressions().len(), 1);
1096        assert_eq!(
1097            spec.expressions(),
1098            &[(
1099                "spec1".to_string(),
1100                ELTLExpression::Globally(Box::new(ELTLExpression::False))
1101            ),]
1102        );
1103    }
1104
1105    #[test]
1106    fn test_error_on_duplicate_spec_name() {
1107        let ta = TEST_TA.clone();
1108
1109        let mut builder = ELTLSpecificationBuilder::new(&ta);
1110
1111        let expr = ELTLExpression::ParameterExpr(
1112            Box::new(IntegerExpression::Const(2)),
1113            ComparisonOp::Eq,
1114            Box::new(IntegerExpression::Const(3)),
1115        );
1116
1117        builder
1118            .add_expressions(vec![("spec1".to_string(), expr)])
1119            .unwrap();
1120
1121        let expr = ELTLExpression::True;
1122
1123        let err = builder.add_expressions(vec![("spec1".to_string(), expr)]);
1124
1125        assert!(err.is_err());
1126        let err = err.unwrap_err();
1127
1128        let expected_err = ELTLExpressionBuilderError::DuplicateName {
1129            property_name: "spec1".into(),
1130        };
1131
1132        assert_eq!(err, expected_err);
1133
1134        assert!(err.to_string().contains("spec1"));
1135        assert!(err.to_string().contains("Duplicate"));
1136    }
1137
1138    #[test]
1139    fn test_ltl_expr_builder_err_for_param_behind_temporal() {
1140        let ta = TEST_TA.clone();
1141
1142        let mut builder = ELTLSpecificationBuilder::new(&ta);
1143
1144        let expr = ELTLExpression::Eventually(Box::new(ELTLExpression::Implies(
1145            Box::new(ELTLExpression::True),
1146            Box::new(ELTLExpression::ParameterExpr(
1147                Box::new(IntegerExpression::Const(2)),
1148                ComparisonOp::Eq,
1149                Box::new(IntegerExpression::Param(Parameter::new("n"))),
1150            )),
1151        )));
1152
1153        let err = builder.add_expressions(vec![("spec1".to_string(), expr)]);
1154
1155        assert!(err.is_err());
1156        let err = err.unwrap_err();
1157
1158        let expected_err = ELTLExpressionBuilderError::ParameterConstraintBehindTemporalOperator {
1159            lhs: Box::new(IntegerExpression::Const(2)),
1160            op: ComparisonOp::Eq,
1161            rhs: Box::new(IntegerExpression::Param(Parameter::new("n"))),
1162            property_name: "spec1".into(),
1163        };
1164
1165        assert_eq!(err, expected_err);
1166
1167        assert!(err.to_string().contains("temporal operator"));
1168        assert!(err.to_string().contains("spec1"));
1169        assert!(err.to_string().contains("parameter"));
1170    }
1171
1172    #[test]
1173    fn test_ltl_builder_test_add_expression_err_unknown_param() {
1174        let ta = TEST_TA.clone();
1175
1176        let mut builder = ELTLSpecificationBuilder::new(&ta);
1177
1178        let expr1 = ELTLExpression::LocationExpr(
1179            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1180            ComparisonOp::Eq,
1181            Box::new(IntegerExpression::Const(2)),
1182        );
1183
1184        let expr2 = ELTLExpression::LocationExpr(
1185            Box::new(IntegerExpression::Atom(Location::new("loc3"))),
1186            ComparisonOp::Eq,
1187            Box::new(IntegerExpression::Param(Parameter::new("x"))),
1188        );
1189
1190        let result = builder.add_expressions(vec![
1191            ("spec1".to_string(), expr1),
1192            ("spec2".to_string(), expr2),
1193        ]);
1194
1195        assert!(result.is_err());
1196        let err = result.unwrap_err();
1197        assert!(err.to_string().contains("Unknown"));
1198        assert!(err.to_string().contains(&Parameter::new("x").to_string()));
1199
1200        let spec = builder.build();
1201        assert_eq!(spec.expressions().len(), 1);
1202    }
1203
1204    #[test]
1205    fn test_ltl_builder_test_add_expression_err_unknown_loc() {
1206        let ta = TEST_TA.clone();
1207
1208        let mut builder = ELTLSpecificationBuilder::new(&ta);
1209
1210        let expr1 = ELTLExpression::LocationExpr(
1211            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1212            ComparisonOp::Eq,
1213            Box::new(IntegerExpression::Const(2)),
1214        );
1215
1216        let expr2 = ELTLExpression::LocationExpr(
1217            Box::new(IntegerExpression::Atom(Location::new("loc3"))),
1218            ComparisonOp::Eq,
1219            Box::new(IntegerExpression::Atom(Location::new("loc4"))),
1220        );
1221
1222        let result = builder.add_expressions(vec![
1223            ("spec1".to_string(), expr1),
1224            ("spec2".to_string(), expr2),
1225        ]);
1226
1227        assert!(result.is_err());
1228        let err = result.unwrap_err();
1229        assert!(err.to_string().contains("Unknown"));
1230        assert!(err.to_string().contains(&Location::new("loc4").to_string()));
1231
1232        let spec = builder.build();
1233        assert_eq!(spec.expressions().len(), 1);
1234    }
1235}
taco_model_checker/eltl.rs

taco_model_checker/
eltl.rs
