taco_model_checker/eltl/
remove_negations.rs

1//! Restricted version of LTL expressions without negations and implications.
2//!
3//! This module contains the logic to convert general LTL expressions into a
4//! more restricted form, which does not contain negations and implications.
5//!
6//! Negations are pushed down to the atomic expressions, and implications are
7//! transformed into disjunctions.
8//!
9//! This type is a more restricted version of LTL expressions, yet is equally
10//! expressive. Therefore, it is easier to work with and to implement algorithms
11//! for.
12
13use std::fmt;
14
15use taco_threshold_automaton::expressions::{
16    ComparisonOp, IntegerExpression, Location, Parameter, Variable,
17};
18
19use super::ELTLExpression;
20
21/// LTL Expression without negations and implications
22#[derive(Debug, PartialEq, Clone)]
23pub enum NonNegatedELTLExpression {
24    /// Globally □
25    Globally(Box<NonNegatedELTLExpression>),
26    /// Eventually ◇
27    Eventually(Box<NonNegatedELTLExpression>),
28    /// And ∧
29    And(Box<NonNegatedELTLExpression>, Box<NonNegatedELTLExpression>),
30    /// Or ∨
31    Or(Box<NonNegatedELTLExpression>, Box<NonNegatedELTLExpression>),
32    /// Boolean constraint over the number of processes in a location
33    LocationExpr(
34        Box<IntegerExpression<Location>>,
35        ComparisonOp,
36        Box<IntegerExpression<Location>>,
37    ),
38    /// Boolean constraint over the value of a variable
39    VariableExpr(
40        Box<IntegerExpression<Variable>>,
41        ComparisonOp,
42        Box<IntegerExpression<Variable>>,
43    ),
44    /// Boolean constraint over parameters
45    ParameterExpr(
46        Box<IntegerExpression<Parameter>>,
47        ComparisonOp,
48        Box<IntegerExpression<Parameter>>,
49    ),
50    /// Always true
51    True,
52    /// Always false
53    False,
54}
55
56impl ELTLExpression {
57    /// Remove boolean negations from an expression, transforming the expression
58    /// into a `NonNegatedELTLExpression` expression.
59    ///
60    /// This method is used to remove negations and implications from an LTL
61    /// expression. Implications are simply transformed into disjunctions, and
62    /// negations are pushed down to the atomic expressions.
63    ///
64    /// # Example
65    ///
66    /// ```rust
67    /// use taco_model_checker::eltl::ELTLExpression;
68    /// use taco_threshold_automaton::expressions::{ComparisonOp, Variable, IntegerExpression};
69    /// use taco_model_checker::eltl::remove_negations::NonNegatedELTLExpression;
70    ///
71    /// // (1 = 2) => (x = 1)
72    /// let ltl = ELTLExpression::Implies(
73    ///     Box::new(ELTLExpression::LocationExpr(
74    ///         Box::new(IntegerExpression::Const(1)),
75    ///         ComparisonOp::Eq,
76    ///         Box::new(IntegerExpression::Const(2)),
77    ///     )),
78    ///     Box::new(ELTLExpression::VariableExpr(
79    ///         Box::new(IntegerExpression::Atom(Variable::new("x"))),
80    ///         ComparisonOp::Eq,
81    ///         Box::new(IntegerExpression::Const(1)),
82    ///     )),
83    /// );
84    ///
85    /// let non_negated_ltl = ltl.remove_negations();
86    ///
87    /// // (1 != 2) ∨ (x = 1)
88    /// let expected = NonNegatedELTLExpression::Or(
89    ///     Box::new(NonNegatedELTLExpression::LocationExpr(
90    ///         Box::new(IntegerExpression::Const(1)),
91    ///         ComparisonOp::Neq,
92    ///         Box::new(IntegerExpression::Const(2)),
93    ///     )),
94    ///     Box::new(NonNegatedELTLExpression::VariableExpr(
95    ///         Box::new(IntegerExpression::Atom(Variable::new("x"))),
96    ///         ComparisonOp::Eq,
97    ///         Box::new(IntegerExpression::Const(1)),
98    ///    )),
99    /// );
100    ///
101    /// assert_eq!(non_negated_ltl, expected);
102    /// ```
103    pub fn remove_negations(&self) -> NonNegatedELTLExpression {
104        match self {
105            ELTLExpression::Implies(lhs, rhs) => {
106                // (a → b) ≡ ¬a ∨ b
107                let lhs = lhs.negate_expression();
108                let rhs = rhs.remove_negations();
109
110                NonNegatedELTLExpression::Or(Box::new(lhs), Box::new(rhs))
111            }
112            ELTLExpression::Globally(expr) => {
113                let expr = expr.remove_negations();
114                NonNegatedELTLExpression::Globally(Box::new(expr))
115            }
116            ELTLExpression::Eventually(expr) => {
117                let expr = expr.remove_negations();
118                NonNegatedELTLExpression::Eventually(Box::new(expr))
119            }
120            ELTLExpression::And(lhs, rhs) => {
121                let lhs = lhs.remove_negations();
122                let rhs = rhs.remove_negations();
123                NonNegatedELTLExpression::And(Box::new(lhs), Box::new(rhs))
124            }
125            ELTLExpression::Or(lhs, rhs) => {
126                let lhs = lhs.remove_negations();
127                let rhs = rhs.remove_negations();
128                NonNegatedELTLExpression::Or(Box::new(lhs), Box::new(rhs))
129            }
130            ELTLExpression::Not(expr) => expr.negate_expression(),
131            ELTLExpression::LocationExpr(lhs, comparison_op, rhs) => {
132                let lhs = lhs.clone();
133                let rhs = rhs.clone();
134                NonNegatedELTLExpression::LocationExpr(lhs, *comparison_op, rhs)
135            }
136            ELTLExpression::VariableExpr(lhs, comparison_op, rhs) => {
137                let lhs = lhs.clone();
138                let rhs = rhs.clone();
139                NonNegatedELTLExpression::VariableExpr(lhs, *comparison_op, rhs)
140            }
141            ELTLExpression::ParameterExpr(lhs, comparison_op, rhs) => {
142                let lhs = lhs.clone();
143                let rhs = rhs.clone();
144                NonNegatedELTLExpression::ParameterExpr(lhs, *comparison_op, rhs)
145            }
146            ELTLExpression::True => NonNegatedELTLExpression::True,
147            ELTLExpression::False => NonNegatedELTLExpression::False,
148        }
149    }
150
151    fn negate_expression(&self) -> NonNegatedELTLExpression {
152        match self {
153            ELTLExpression::Implies(lhs, rhs) => {
154                // ¬(a → b) ≡ a ∧ ¬b
155                let lhs = lhs.remove_negations();
156                let rhs = rhs.negate_expression();
157
158                NonNegatedELTLExpression::And(Box::new(lhs), Box::new(rhs))
159            }
160            ELTLExpression::Globally(expr) => {
161                let expr = expr.negate_expression();
162                NonNegatedELTLExpression::Eventually(Box::new(expr))
163            }
164            ELTLExpression::Eventually(expr) => {
165                let expr = expr.negate_expression();
166                NonNegatedELTLExpression::Globally(Box::new(expr))
167            }
168            ELTLExpression::And(lhs, rhs) => {
169                let lhs = lhs.negate_expression();
170                let rhs = rhs.negate_expression();
171                NonNegatedELTLExpression::Or(Box::new(lhs), Box::new(rhs))
172            }
173            ELTLExpression::Or(lhs, rhs) => {
174                let lhs = lhs.negate_expression();
175                let rhs = rhs.negate_expression();
176                NonNegatedELTLExpression::And(Box::new(lhs), Box::new(rhs))
177            }
178            ELTLExpression::Not(expr) => expr.remove_negations(),
179            ELTLExpression::LocationExpr(lhs, op, rhs) => {
180                let lhs = lhs.clone();
181                let rhs = rhs.clone();
182                NonNegatedELTLExpression::LocationExpr(lhs, op.invert(), rhs)
183            }
184            ELTLExpression::VariableExpr(lhs, op, rhs) => {
185                let lhs = lhs.clone();
186                let rhs = rhs.clone();
187                NonNegatedELTLExpression::VariableExpr(lhs, op.invert(), rhs)
188            }
189            ELTLExpression::ParameterExpr(lhs, op, rhs) => {
190                let lhs = lhs.clone();
191                let rhs = rhs.clone();
192                NonNegatedELTLExpression::ParameterExpr(lhs, op.invert(), rhs)
193            }
194            ELTLExpression::True => NonNegatedELTLExpression::False,
195            ELTLExpression::False => NonNegatedELTLExpression::True,
196        }
197    }
198}
199
200impl From<ELTLExpression> for NonNegatedELTLExpression {
201    fn from(value: ELTLExpression) -> Self {
202        value.remove_negations()
203    }
204}
205
206impl fmt::Display for NonNegatedELTLExpression {
207    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
208        match self {
209            NonNegatedELTLExpression::Globally(expression) => write!(f, "[]({expression})"),
210            NonNegatedELTLExpression::Eventually(expression) => write!(f, "<>({expression})"),
211            NonNegatedELTLExpression::And(lhs, rhs) => write!(f, "({lhs}) && ({rhs})"),
212            NonNegatedELTLExpression::Or(lhs, rhs) => write!(f, "({lhs}) || ({rhs})"),
213            NonNegatedELTLExpression::LocationExpr(lhs, op, rhs) => write!(f, "{lhs} {op} {rhs}"),
214            NonNegatedELTLExpression::VariableExpr(lhs, op, rhs) => write!(f, "{lhs} {op} {rhs}"),
215            NonNegatedELTLExpression::ParameterExpr(lhs, op, rhs) => write!(f, "{lhs} {op} {rhs}"),
216            NonNegatedELTLExpression::True => write!(f, "true"),
217            NonNegatedELTLExpression::False => write!(f, "false"),
218        }
219    }
220}
221
222#[cfg(test)]
223mod tests {
224    use super::*;
225    use taco_threshold_automaton::expressions::{ComparisonOp, IntegerExpression, Variable};
226
227    #[test]
228    fn test_remove_negations_trivial() {
229        let ltl = ELTLExpression::True;
230        let non_negated_ltl = ltl.remove_negations();
231        let expected = NonNegatedELTLExpression::True;
232        assert_eq!(non_negated_ltl, expected);
233
234        let ltl = ELTLExpression::False;
235        let non_negated_ltl = ltl.remove_negations();
236        let expected = NonNegatedELTLExpression::False;
237        assert_eq!(non_negated_ltl, expected);
238
239        let ltl = ELTLExpression::Not(Box::new(ELTLExpression::False));
240        let non_negated_ltl = ltl.remove_negations();
241        let expected = NonNegatedELTLExpression::True;
242        assert_eq!(non_negated_ltl, expected);
243
244        let ltl = ELTLExpression::Not(Box::new(ELTLExpression::True));
245        let non_negated_ltl = ltl.remove_negations();
246        let expected = NonNegatedELTLExpression::False;
247        assert_eq!(non_negated_ltl, expected);
248    }
249
250    #[test]
251    fn test_remove_negations() {
252        // (1 = 2) => (x = 1)
253        let ltl = ELTLExpression::Implies(
254            Box::new(ELTLExpression::LocationExpr(
255                Box::new(IntegerExpression::Const(1)),
256                ComparisonOp::Eq,
257                Box::new(IntegerExpression::Const(2)),
258            )),
259            Box::new(ELTLExpression::VariableExpr(
260                Box::new(IntegerExpression::Atom(Variable::new("x"))),
261                ComparisonOp::Eq,
262                Box::new(IntegerExpression::Const(1)),
263            )),
264        );
265
266        let non_negated_ltl = ltl.remove_negations();
267
268        // (1 != 2) ∨ (x = 1)
269        let expected = NonNegatedELTLExpression::Or(
270            Box::new(NonNegatedELTLExpression::LocationExpr(
271                Box::new(IntegerExpression::Const(1)),
272                ComparisonOp::Neq,
273                Box::new(IntegerExpression::Const(2)),
274            )),
275            Box::new(NonNegatedELTLExpression::VariableExpr(
276                Box::new(IntegerExpression::Atom(Variable::new("x"))),
277                ComparisonOp::Eq,
278                Box::new(IntegerExpression::Const(1)),
279            )),
280        );
281
282        assert_eq!(non_negated_ltl, expected);
283    }
284
285    #[test]
286    fn test_remove_negations_nested() {
287        // ¬(□(1 = 2) ∧ ◇(x = 1))
288        let ltl = ELTLExpression::Not(Box::new(ELTLExpression::And(
289            Box::new(ELTLExpression::Globally(Box::new(
290                ELTLExpression::LocationExpr(
291                    Box::new(IntegerExpression::Const(1)),
292                    ComparisonOp::Eq,
293                    Box::new(IntegerExpression::Const(2)),
294                ),
295            ))),
296            Box::new(ELTLExpression::Eventually(Box::new(
297                ELTLExpression::VariableExpr(
298                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
299                    ComparisonOp::Eq,
300                    Box::new(IntegerExpression::Const(1)),
301                ),
302            ))),
303        )));
304
305        let non_negated_ltl = ltl.remove_negations();
306
307        // (◇(1 != 2) ∨ □(x != 1))
308        let expected = NonNegatedELTLExpression::Or(
309            Box::new(NonNegatedELTLExpression::Eventually(Box::new(
310                NonNegatedELTLExpression::LocationExpr(
311                    Box::new(IntegerExpression::Const(1)),
312                    ComparisonOp::Neq,
313                    Box::new(IntegerExpression::Const(2)),
314                ),
315            ))),
316            Box::new(NonNegatedELTLExpression::Globally(Box::new(
317                NonNegatedELTLExpression::VariableExpr(
318                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
319                    ComparisonOp::Neq,
320                    Box::new(IntegerExpression::Const(1)),
321                ),
322            ))),
323        );
324
325        assert_eq!(non_negated_ltl, expected);
326    }
327
328    #[test]
329    fn test_negated_or() {
330        // □(◇(¬((1 = 2) ∨ ¬(x = 1)))
331        let ltl = ELTLExpression::Globally(Box::new(ELTLExpression::Eventually(Box::new(
332            ELTLExpression::Not(Box::new(ELTLExpression::Or(
333                Box::new(ELTLExpression::LocationExpr(
334                    Box::new(IntegerExpression::Const(1)),
335                    ComparisonOp::Eq,
336                    Box::new(IntegerExpression::Const(2)),
337                )),
338                Box::new(ELTLExpression::Not(Box::new(ELTLExpression::LocationExpr(
339                    Box::new(IntegerExpression::Atom(Location::new("x"))),
340                    ComparisonOp::Eq,
341                    Box::new(IntegerExpression::Const(1)),
342                )))),
343            ))),
344        ))));
345        let non_negated_ltl = ltl.remove_negations();
346
347        // □(◇(1 != 2 ∧ x = 1))
348        let expected = NonNegatedELTLExpression::Globally(Box::new(
349            NonNegatedELTLExpression::Eventually(Box::new(NonNegatedELTLExpression::And(
350                Box::new(NonNegatedELTLExpression::LocationExpr(
351                    Box::new(IntegerExpression::Const(1)),
352                    ComparisonOp::Neq,
353                    Box::new(IntegerExpression::Const(2)),
354                )),
355                Box::new(NonNegatedELTLExpression::LocationExpr(
356                    Box::new(IntegerExpression::Atom(Location::new("x"))),
357                    ComparisonOp::Eq,
358                    Box::new(IntegerExpression::Const(1)),
359                )),
360            ))),
361        ));
362
363        assert_eq!(non_negated_ltl, expected);
364    }
365
366    #[test]
367    fn test_and_or() {
368        // ((1 = 2) ∧ (x = 1)) ∨ (y = 2)
369        let ltl = ELTLExpression::Or(
370            Box::new(ELTLExpression::And(
371                Box::new(ELTLExpression::LocationExpr(
372                    Box::new(IntegerExpression::Const(1)),
373                    ComparisonOp::Eq,
374                    Box::new(IntegerExpression::Const(2)),
375                )),
376                Box::new(ELTLExpression::VariableExpr(
377                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
378                    ComparisonOp::Eq,
379                    Box::new(IntegerExpression::Const(1)),
380                )),
381            )),
382            Box::new(ELTLExpression::LocationExpr(
383                Box::new(IntegerExpression::Atom(Location::new("y"))),
384                ComparisonOp::Eq,
385                Box::new(IntegerExpression::Const(2)),
386            )),
387        );
388
389        let non_negated_ltl = ltl.remove_negations();
390
391        // ((1 = 2) ∧ (x = 1)) ∨  (y = 2)
392        let expected = NonNegatedELTLExpression::Or(
393            Box::new(NonNegatedELTLExpression::And(
394                Box::new(NonNegatedELTLExpression::LocationExpr(
395                    Box::new(IntegerExpression::Const(1)),
396                    ComparisonOp::Eq,
397                    Box::new(IntegerExpression::Const(2)),
398                )),
399                Box::new(NonNegatedELTLExpression::VariableExpr(
400                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
401                    ComparisonOp::Eq,
402                    Box::new(IntegerExpression::Const(1)),
403                )),
404            )),
405            Box::new(NonNegatedELTLExpression::LocationExpr(
406                Box::new(IntegerExpression::Atom(Location::new("y"))),
407                ComparisonOp::Eq,
408                Box::new(IntegerExpression::Const(2)),
409            )),
410        );
411
412        assert_eq!(non_negated_ltl, expected);
413    }
414
415    #[test]
416    fn test_double_neg() {
417        // !(!((l < 1) && (v < 3)))
418        let eltl = ELTLExpression::Not(Box::new(ELTLExpression::Not(Box::new(
419            ELTLExpression::And(
420                Box::new(ELTLExpression::LocationExpr(
421                    Box::new(IntegerExpression::Atom(Location::new("l"))),
422                    ComparisonOp::Lt,
423                    Box::new(IntegerExpression::Const(1)),
424                )),
425                Box::new(ELTLExpression::VariableExpr(
426                    Box::new(IntegerExpression::Atom(Variable::new("v"))),
427                    ComparisonOp::Lt,
428                    Box::new(IntegerExpression::Const(3)),
429                )),
430            ),
431        ))));
432
433        let non_negated_ltl = eltl.remove_negations();
434
435        //(l < 1) && (v < 3)
436        let expected = NonNegatedELTLExpression::And(
437            Box::new(NonNegatedELTLExpression::LocationExpr(
438                Box::new(IntegerExpression::Atom(Location::new("l"))),
439                ComparisonOp::Lt,
440                Box::new(IntegerExpression::Const(1)),
441            )),
442            Box::new(NonNegatedELTLExpression::VariableExpr(
443                Box::new(IntegerExpression::Atom(Variable::new("v"))),
444                ComparisonOp::Lt,
445                Box::new(IntegerExpression::Const(3)),
446            )),
447        );
448
449        assert_eq!(non_negated_ltl, expected);
450    }
451}
taco_model_checker/eltl/remove_negations.rs

taco_model_checker/eltl/
remove_negations.rs
