Implication is not monotone

Author: GBathie

src/ltl/trace.rs

@@ -28,8 +28,8 @@ pub struct Operators {
 
 impl Operators {
     pub(crate) fn filter_bool(mut self) -> Self {
-        self.unary.retain(|op| op.is_boolean());
-        self.binary.retain(|op| op.is_boolean());
+        self.unary.retain(|op| op.is_boolean_monotone());
+        self.binary.retain(|op| op.is_boolean_monotone());
         self
     }
 

src/ops/binary.rs

@@ -29,10 +29,10 @@ impl LtlBinaryOp {
     }
 
     /// Whether this LTL operator is boolean.
-    pub(crate) fn is_boolean(&self) -> bool {
+    pub(crate) fn is_boolean_monotone(&self) -> bool {
         matches!(
             self,
-            LtlBinaryOp::Or | LtlBinaryOp::And | LtlBinaryOp::Implies | LtlBinaryOp::Equivalent
+            LtlBinaryOp::Or | LtlBinaryOp::And | LtlBinaryOp::Equivalent
         )
     }
 

src/ops/unary.rs

@@ -21,7 +21,7 @@ impl LtlUnaryOp {
         // vec![Not, WeakNext, StrongNext, Finally, Globally]
     }
 
-    pub(crate) fn is_boolean(&self) -> bool {
+    pub(crate) fn is_boolean_monotone(&self) -> bool {
         match self {
             // LtlUnaryOp::Not => true,
             LtlUnaryOp::WeakNext