Add LTL operators: Release, Strong Next, Weak Next

GBathie · GBathie · commit 49a8359063c5 · 2025-05-06T11:15:52.000+02:00
diff --git a/src/bool/cv.rs b/src/bool/cv.rs
@@ -48,6 +48,39 @@ impl CharVec {
         let values = self.values.bitxor(sv.values);
         SatVec { values }
     }
+
+    #[inline]
+    pub fn implies(self, rhs: Self) -> Self {
+        let CharVec { values: x, length } = self;
+        let CharVec {
+            values: y,
+            length: _l2,
+        } = rhs;
+        let values = x.not().bitor(y);
+        let values = if self.length < 128 {
+            values & ((1u128 << self.length) - 1)
+        } else {
+            values
+        };
+        CharVec { values, length }
+    }
+
+    #[inline]
+    pub fn equiv(self, rhs: Self) -> Self {
+        let CharVec { values: x, length } = self;
+        let CharVec {
+            values: y,
+            length: _l2,
+        } = rhs;
+
+        let values = (x.bitxor(y)).not();
+        let values = if self.length < 128 {
+            values & ((1u128 << self.length) - 1)
+        } else {
+            values
+        };
+        CharVec { values, length }
+    }
 }
 
 impl Not for CharVec {
@@ -135,7 +168,7 @@ impl FromIterator<bool> for CharVec {
 
 #[cfg(test)]
 mod tests {
-    use rand::{rng, Rng};
+    use rand::{Rng, rng};
 
     use super::*;
 
@@ -207,4 +240,44 @@ mod tests {
             assert_eq!(!(x1 | x2), !x1 & !x2);
         }
     }
+
+    #[test]
+    fn x_implies_x() {
+        for _ in 0..100 {
+            let x = random_vec();
+            assert_eq!(x.implies(x).values, (1 << x.length) - 1);
+        }
+    }
+
+    #[test]
+    fn implies_def() {
+        for _ in 0..100 {
+            let (x, y) = random_pair();
+            assert_eq!(x.implies(y), x.not() | y);
+        }
+    }
+
+    #[test]
+    fn x_equiv_x() {
+        for _ in 0..100 {
+            let x = random_vec();
+            assert_eq!(x.equiv(x).values, (1 << x.length) - 1);
+        }
+    }
+
+    #[test]
+    fn equiv_iff_double_implies() {
+        for _ in 0..100 {
+            let (x, y) = random_pair();
+            assert_eq!(x.equiv(y), x.implies(y) & y.implies(x));
+        }
+    }
+
+    #[test]
+    fn equiv_def() {
+        for _ in 0..100 {
+            let (x, y) = random_pair();
+            assert_eq!(x.equiv(y), (x & y) | (x.not() & y.not()));
+        }
+    }
 }
diff --git a/src/ltl/cm.rs b/src/ltl/cm.rs
@@ -74,10 +74,11 @@ impl CharMatrix {
         self.seqs.iter().map(|x| x.accepts()).collect()
     }
 
-    op_for_cm!(next, globally, finally);
+    op_for_cm!(weak_next, strong_next, globally, finally);
     binop_for_cm!(bitor as or);
     binop_for_cm!(bitand as and);
     binop_for_cm!(until);
+    binop_for_cm!(release);
     binop_for_cm!(implies);
     binop_for_cm!(equiv);
 }
diff --git a/src/ltl/cs.rs b/src/ltl/cs.rs
@@ -109,13 +109,23 @@ impl CharSeq {
         CharSeq { values, length }
     }
 
-    /// LTL Next operator (X)
+    /// LTL (strong) Next operator (X[!])
     #[inline]
-    pub(crate) fn next(mut self) -> Self {
+    pub(crate) fn strong_next(mut self) -> Self {
         self.values >>= 1;
         self
     }
 
+    /// LTL (weak) Next operator (X)
+    #[inline]
+    pub(crate) fn weak_next(mut self) -> Self {
+        self.values >>= 1;
+        if self.length > 0 {
+            self.values |= 1u64 << (self.length - 1);
+        }
+        self
+    }
+
     /// LTL Globally operator (G)
     #[inline]
     pub(crate) fn globally(self) -> Self {
@@ -162,6 +172,12 @@ impl CharSeq {
         y |= x & (y >> 32);
         CharSeq { values: y, length }
     }
+
+    /// LTL Release operator (R)
+    #[inline]
+    pub(crate) fn release(self, rhs: Self) -> Self {
+        self.not().until(rhs.not()).not()
+    }
 }
 
 impl Debug for CharSeq {
@@ -208,7 +224,12 @@ mod tests {
 
     #[allow(non_snake_case)]
     pub(crate) fn X(phi: CharSeq) -> CharSeq {
-        phi.next()
+        phi.weak_next()
+    }
+
+    #[allow(non_snake_case)]
+    pub(crate) fn X_s(phi: CharSeq) -> CharSeq {
+        phi.strong_next()
     }
 
     #[allow(non_snake_case)]
@@ -226,6 +247,11 @@ mod tests {
         phi.until(psi)
     }
 
+    #[allow(non_snake_case)]
+    pub(crate) fn R(phi: CharSeq, psi: CharSeq) -> CharSeq {
+        phi.release(psi)
+    }
+
     fn random_seq_with_len(len: usize, rng: &mut impl Rng) -> CharSeq {
         let x: u64 = rng.random();
         let x = if len < 64 { x & ((1u64 << len) - 1) } else { x };
@@ -320,7 +346,7 @@ mod tests {
     fn f_as_phi_or_x_f_phi() {
         for _ in 0..100 {
             let x = random_seq();
-            assert_eq!(F(x), x | X(F(x)));
+            assert_eq!(F(x), x | X_s(F(x)));
         }
     }
 
@@ -352,7 +378,23 @@ mod tests {
     fn expand_u() {
         for _ in 0..100 {
             let (x, y) = random_pair();
-            assert_eq!(U(x, y), y | (x & X(U(x, y))));
+            assert_eq!(U(x, y), y | (x & X_s(U(x, y))));
+        }
+    }
+
+    #[test]
+    fn expand_r() {
+        for _ in 0..100 {
+            let (x, y) = random_pair();
+            assert_eq!(R(x, y), y & (x | X(R(x, y))));
+        }
+    }
+
+    #[test]
+    fn r_dual_u() {
+        for _ in 0..100 {
+            let (x, y) = random_pair();
+            assert_eq!(R(x, y), !(U(!x, !y)));
         }
     }
 
diff --git a/src/ops/binary.rs b/src/ops/binary.rs
@@ -11,11 +11,12 @@ use crate::{bool::cv::CharVec, ltl::cm::CharMatrix};
 use super::traits::Commutativity;
 
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
-/// Binary LTL Operators: Or, And, Until
+/// Binary LTL Operators: Or, And, Until, Release, Implication and Equivalence
 pub enum LtlBinaryOp {
     Or,
     And,
     Until,
+    Release,
     Implies,
     Equivalent,
 }
@@ -24,12 +25,15 @@ impl LtlBinaryOp {
     /// Returns a list of all binary operators.
     pub(crate) fn all() -> Vec<LtlBinaryOp> {
         use LtlBinaryOp::*;
-        vec![Or, And, Until, Implies, Equivalent]
+        vec![Or, And, Until, Release, Implies, Equivalent]
     }
 
     /// Whether this LTL operator is boolean.
     pub(crate) fn is_boolean(&self) -> bool {
-        matches!(self, LtlBinaryOp::Or | LtlBinaryOp::And)
+        matches!(
+            self,
+            LtlBinaryOp::Or | LtlBinaryOp::And | LtlBinaryOp::Implies | LtlBinaryOp::Equivalent
+        )
     }
 
     /// Apply the operator to two characteristic vectors.
@@ -41,6 +45,8 @@ impl LtlBinaryOp {
         match op {
             LtlBinaryOp::Or => lhs.bitor(rhs),
             LtlBinaryOp::And => lhs.bitand(rhs),
+            LtlBinaryOp::Implies => lhs.implies(rhs),
+            LtlBinaryOp::Equivalent => lhs.equiv(rhs),
             _ => panic!(
                 "Cannot apply non-boolean operator {} to characteristic vectors",
                 op
@@ -54,6 +60,7 @@ impl LtlBinaryOp {
             LtlBinaryOp::Or => lhs.or(rhs),
             LtlBinaryOp::And => lhs.and(rhs),
             LtlBinaryOp::Until => lhs.until(rhs),
+            LtlBinaryOp::Release => lhs.release(rhs),
             LtlBinaryOp::Implies => lhs.implies(rhs),
             LtlBinaryOp::Equivalent => lhs.equiv(rhs),
         }
@@ -64,7 +71,7 @@ impl Commutativity for LtlBinaryOp {
     fn commutes(&self) -> bool {
         match self {
             LtlBinaryOp::Or | LtlBinaryOp::And | LtlBinaryOp::Equivalent => true,
-            LtlBinaryOp::Until | LtlBinaryOp::Implies => false,
+            LtlBinaryOp::Until | LtlBinaryOp::Release | LtlBinaryOp::Implies => false,
         }
     }
 }
@@ -85,6 +92,7 @@ impl<'a> TryFrom<&'a str> for LtlBinaryOp {
     /// | `"\|"` | [`LtlBinaryOp::Or`]   |
     /// | `"&"`  | [`LtlBinaryOp::And`]  |
     /// | `"U"`  | [`LtlBinaryOp::Until`]|
+    /// | `"R"`  | [`LtlBinaryOp::Release`]|
     /// | `"->"`  | [`LtlBinaryOp::Implies`]|
     /// | `"<->"`  | [`LtlBinaryOp::Equivalent`]|
     /// | Other value  | `Error`  |
@@ -93,6 +101,7 @@ impl<'a> TryFrom<&'a str> for LtlBinaryOp {
             "|" => Ok(LtlBinaryOp::Or),
             "&" => Ok(LtlBinaryOp::And),
             "U" => Ok(LtlBinaryOp::Until),
+            "R" => Ok(LtlBinaryOp::Release),
             "->" => Ok(LtlBinaryOp::Implies),
             "<->" => Ok(LtlBinaryOp::Equivalent),
             _ => Err(InvalidBinaryOp(value)),
@@ -106,6 +115,7 @@ impl Display for LtlBinaryOp {
             LtlBinaryOp::And => write!(f, "&"),
             LtlBinaryOp::Or => write!(f, "|"),
             LtlBinaryOp::Until => write!(f, "U"),
+            LtlBinaryOp::Release => write!(f, "R"),
             LtlBinaryOp::Implies => write!(f, "->"),
             LtlBinaryOp::Equivalent => write!(f, "<->"),
         }
@@ -127,6 +137,15 @@ mod test {
         let parsed = "U".try_into();
         assert_eq!(parsed, Ok(LtlBinaryOp::Until));
 
+        let parsed = "R".try_into();
+        assert_eq!(parsed, Ok(LtlBinaryOp::Release));
+
+        let parsed = "->".try_into();
+        assert_eq!(parsed, Ok(LtlBinaryOp::Implies));
+
+        let parsed = "<->".try_into();
+        assert_eq!(parsed, Ok(LtlBinaryOp::Equivalent));
+
         let parsed: Result<LtlBinaryOp, _> = ":".try_into();
         assert!(parsed.is_err());
     }
diff --git a/src/ops/unary.rs b/src/ops/unary.rs
@@ -8,29 +8,34 @@ use crate::ltl::cm::CharMatrix;
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
 pub enum LtlUnaryOp {
     // Not,
-    Next,
+    WeakNext,
+    StrongNext,
     Finally,
     Globally,
 }
 
 impl LtlUnaryOp {
     pub(crate) fn all() -> Vec<LtlUnaryOp> {
         use LtlUnaryOp::*;
-        vec![Next, Finally, Globally]
-        // vec![Not, Next, Finally, Globally]
+        vec![WeakNext, StrongNext, Finally, Globally]
+        // vec![Not, WeakNext, StrongNext, Finally, Globally]
     }
 
     pub(crate) fn is_boolean(&self) -> bool {
         match self {
             // LtlUnaryOp::Not => true,
-            LtlUnaryOp::Next | LtlUnaryOp::Finally | LtlUnaryOp::Globally => false,
+            LtlUnaryOp::WeakNext
+            | LtlUnaryOp::StrongNext
+            | LtlUnaryOp::Finally
+            | LtlUnaryOp::Globally => false,
         }
     }
 
     pub(crate) fn apply_cm(op: Self, cm: &CharMatrix) -> CharMatrix {
         match op {
             // LtlUnaryOp::Not => cm.not(),
-            LtlUnaryOp::Next => cm.next(),
+            LtlUnaryOp::WeakNext => cm.weak_next(),
+            LtlUnaryOp::StrongNext => cm.strong_next(),
             LtlUnaryOp::Finally => cm.finally(),
             LtlUnaryOp::Globally => cm.globally(),
         }
@@ -50,13 +55,15 @@ impl<'a> TryFrom<&'a str> for LtlUnaryOp {
     ///
     /// | String |   Result  |
     /// |:-------|:---------------------|
-    /// | `"X"`  | [`LtlUnaryOp::Next`]  |
+    /// | `"X"`  | [`LtlUnaryOp::WeakNext`]  |
+    /// | `"X[!]"`  | [`LtlUnaryOp::StrongNext`]  |
     /// | `"F"`  | [`LtlUnaryOp::Finally`]   |
     /// | `"G"`  | [`LtlUnaryOp::Globally`]|
     /// | Other value  | `Error` |
     fn try_from(value: &'a str) -> Result<Self, Self::Error> {
         match value {
-            "X" => Ok(LtlUnaryOp::Next),
+            "X" => Ok(LtlUnaryOp::WeakNext),
+            "X[!]" => Ok(LtlUnaryOp::StrongNext),
             "F" => Ok(LtlUnaryOp::Finally),
             "G" => Ok(LtlUnaryOp::Globally),
             _ => Err(InvalidUnaryOp(value)),
@@ -67,7 +74,8 @@ impl<'a> TryFrom<&'a str> for LtlUnaryOp {
 impl Display for LtlUnaryOp {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
-            LtlUnaryOp::Next => write!(f, "X"),
+            LtlUnaryOp::WeakNext => write!(f, "X"),
+            LtlUnaryOp::StrongNext => write!(f, "X[!]"),
             LtlUnaryOp::Finally => write!(f, "F"),
             LtlUnaryOp::Globally => write!(f, "G"),
         }
@@ -81,7 +89,9 @@ mod test {
     #[test]
     fn string_try_into_binary_op() {
         let parsed = "X".try_into();
-        assert_eq!(parsed, Ok(LtlUnaryOp::Next));
+        assert_eq!(parsed, Ok(LtlUnaryOp::WeakNext));
+        let parsed = "X[!]".try_into();
+        assert_eq!(parsed, Ok(LtlUnaryOp::StrongNext));
 
         let parsed = "F".try_into();
         assert_eq!(parsed, Ok(LtlUnaryOp::Finally));

Original file line number	Diff line number	Diff line change
`@@ -74,10 +74,11 @@ impl CharMatrix {`
`74`	`74`	`self.seqs.iter().map(\|x\| x.accepts()).collect()`
`75`	`75`	`}`
`76`	`76`
`77`		`- op_for_cm!(next, globally, finally);`
	`77`	`+ op_for_cm!(weak_next, strong_next, globally, finally);`
`78`	`78`	`binop_for_cm!(bitor as or);`
`79`	`79`	`binop_for_cm!(bitand as and);`
`80`	`80`	`binop_for_cm!(until);`
	`81`	`+ binop_for_cm!(release);`
`81`	`82`	`binop_for_cm!(implies);`
`82`	`83`	`binop_for_cm!(equiv);`
`83`	`84`	`}`