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

taco_model_checker/eltl/
remove_negations.rs
