Add Not operator, remove NNF

Author: GBathie

src/algos/meta/mod.rs

@@ -22,7 +22,7 @@ pub mod meta_res;
 /// LTL search followed by Divide and Conquer.
 pub fn divide_conquer<P>(
     traces: &[Trace],
-    alphabet: Vec<String>,
+    atomic_propositions: Vec<String>,
     operators: Operators,
     target: Vec<bool>,
     max_size_ltl: usize,
@@ -34,7 +34,7 @@ where
 {
     let start = Instant::now();
 
-    let atoms = atoms(traces, alphabet);
+    let atoms = atoms(traces, atomic_propositions);
     // Add initial formulas
     let (atom, mut ltl_cache) = create_initial_cache(atoms, &target);
     // Check if target is an atom

src/algos/mod.rs

@@ -14,18 +14,18 @@
 //!
 //! Implementing a Boolean Synthesis for use with meta-algorithms is done via
 //! the [`BoolAlgoParams`] trait.
-use std::{ops::Not, rc::Rc};
+use std::rc::Rc;
 
 use meta::cache::InitialBoolCache;
 
 use crate::{
     cache::{EnumFormulaCache, EnumFormulaCacheLine},
-    formula::{tree::FormulaTree, Formula},
+    formula::{Formula, tree::FormulaTree},
     ltl::{
+        AtomicProposition, LtlFormula,
         cache::LtlCache,
         charac::LtlCharac,
         trace::{Operators, Trace},
-        LtlFormula, Predicate, PredicateForm,
     },
     traits::EqTarget,
 };
@@ -51,34 +51,20 @@ pub trait BoolAlgoParams {
     fn name() -> &'static str;
 }
 
-/// Return a [`Vec`] containing all size-1 LTL formulas: the predicates and their negation.
-fn atoms(traces: &[Trace], alphabet: Vec<String>) -> Vec<LtlFormula> {
+/// Return a [`Vec`] containing all size-1 LTL formulas, that consist only of an atomic proposition.
+fn atoms(traces: &[Trace], atomic_propositions: Vec<String>) -> Vec<LtlFormula> {
     let mut atoms = Vec::new();
-    for (i, s) in alphabet.into_iter().enumerate() {
-        let charac = traces.iter().map(|t| t.alphabet[i]).collect::<LtlCharac>();
-        let f = Formula::new_base(
-            charac,
-            1,
-            Rc::from(FormulaTree::Atom(Predicate(
-                s.clone(),
-                PredicateForm::Positive(i),
-            ))),
-        );
-        atoms.push(f);
-
+    for (i, s) in atomic_propositions.into_iter().enumerate() {
         let charac = traces
             .iter()
-            .map(|t| t.alphabet[i].not())
+            .map(|t| t.atomic_propositions[i])
             .collect::<LtlCharac>();
-        let not_f = Formula::new_base(
+        let f = Formula::new_base(
             charac,
             1,
-            Rc::from(FormulaTree::Atom(Predicate(
-                format!("!{s}"),
-                PredicateForm::Negative(i),
-            ))),
+            Rc::from(FormulaTree::Atom(AtomicProposition(s, i))),
         );
-        atoms.push(not_f);
+        atoms.push(f);
     }
 
     atoms

src/bin/experiments.rs

@@ -60,7 +60,7 @@ fn main() {
 
 fn get_name_time_sol<P: BoolAlgoParams + Clone>(
     traces: Vec<Trace>,
-    alphabet: Vec<String>,
+    atomic_propositions: Vec<String>,
     operators: Operators,
     target: Vec<bool>,
     max_size_ltl: usize,
@@ -69,7 +69,7 @@ fn get_name_time_sol<P: BoolAlgoParams + Clone>(
 ) -> (f64, Option<FormulaTree>, &'static str) {
     let res = divide_conquer(
         &traces,
-        alphabet,
+        atomic_propositions,
         operators,
         target.clone(),
         max_size_ltl,

src/formula/tree.rs

@@ -1,15 +1,15 @@
 //! Explicit formula tree representation.
-use std::{fmt::Display, ops::Not, rc::Rc};
+use std::{fmt::Display, rc::Rc};
 
 use crate::{
-    ltl::{cm::CharMatrix, trace::Trace, Predicate, PredicateForm},
+    ltl::{AtomicProposition, cm::CharMatrix, trace::Trace},
     ops::{binary::LtlBinaryOp, unary::LtlUnaryOp},
 };
 
 /// Representation of an LTL as a tree of operators.
 #[derive(Debug, PartialEq, Eq, Hash, Clone)]
 pub enum FormulaTree {
-    Atom(Predicate),
+    Atom(AtomicProposition),
     UnaryNode {
         op: LtlUnaryOp,
         child: Rc<FormulaTree>,
@@ -34,10 +34,9 @@ impl FormulaTree {
     /// Evaluate the formula on a set of input traces.
     pub fn eval(&self, traces: &[Trace]) -> CharMatrix {
         match self {
-            FormulaTree::Atom(Predicate(_, pf)) => match *pf {
-                PredicateForm::Positive(i) => traces.iter().map(|t| t.alphabet[i]).collect(),
-                PredicateForm::Negative(i) => traces.iter().map(|t| t.alphabet[i].not()).collect(),
-            },
+            FormulaTree::Atom(AtomicProposition(_, i)) => {
+                traces.iter().map(|t| t.atomic_propositions[*i]).collect()
+            }
             FormulaTree::UnaryNode { op, child } => {
                 let cm = child.eval(traces);
                 LtlUnaryOp::apply_cm(*op, &cm)
@@ -54,7 +53,7 @@ impl FormulaTree {
 impl Display for FormulaTree {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
-            FormulaTree::Atom(Predicate(p, _)) => write!(f, "{p}"),
+            FormulaTree::Atom(AtomicProposition(p, _)) => write!(f, "{p}"),
             FormulaTree::UnaryNode { op, child } => write!(f, "{op} ({child})"),
             FormulaTree::BinaryNode { op, left, right } => write!(f, "({left}) {op} ({right})"),
         }

src/ltl/cm.rs

@@ -1,7 +1,7 @@
 //! Characteristic Matrix of LTL formulas.
 use std::{
     hash::{Hash, Hasher},
-    ops::{BitAnd, BitOr},
+    ops::{BitAnd, BitOr, Not},
 };
 
 use crate::HashType;
@@ -74,7 +74,7 @@ impl CharMatrix {
         self.seqs.iter().map(|x| x.accepts()).collect()
     }
 
-    op_for_cm!(weak_next, strong_next, globally, finally);
+    op_for_cm!(not, weak_next, strong_next, globally, finally);
     binop_for_cm!(bitor as or);
     binop_for_cm!(bitand as and);
     binop_for_cm!(until);

src/ltl/mod.rs

@@ -10,17 +10,12 @@ pub mod cs;
 pub mod hash;
 pub mod trace;
 
+/// Represents an atomic proposition, e.g. `p`, `q`, `var0`, etc.
+///
+/// The first component is the string representation of the proposition,
+/// the second is its index in the vector of atomic propositions.
 #[derive(Debug, Hash, PartialEq, Eq, Clone)]
-pub struct Predicate(pub(crate) String, pub(crate) PredicateForm);
-
-/// Formula corresponding to a single variable `x_i`, which may be negated.
-#[derive(Debug, Hash, PartialEq, Eq, Clone)]
-pub enum PredicateForm {
-    /// Formula `x_i`
-    Positive(usize),
-    /// Formula `not x_i`
-    Negative(usize),
-}
+pub struct AtomicProposition(pub(crate) String, pub(crate) usize);
 
 pub(crate) type LtlFormula = Formula<LtlCharac>;
 

src/ltl/trace.rs

@@ -14,10 +14,10 @@ pub struct Instance {
     pub operators: Operators,
 }
 
-/// Stores the [`CharSeq`] of each predicate on a given trace.
+/// Stores the [`CharSeq`] of each atomic_proposition on a given trace.
 #[derive(Debug, PartialEq, Eq, Hash, Clone)]
 pub struct Trace {
-    pub alphabet: Vec<CharSeq>,
+    pub atomic_propositions: Box<[CharSeq]>,
 }
 
 #[derive(Debug, PartialEq, Eq, Clone)]
@@ -66,12 +66,12 @@ pub fn parse_traces(buf: &str) -> Instance {
     let traces: Option<Vec<_>> = parsed_input
         .positive_traces
         .into_iter()
-        .map(|pt| pt.traces_vec_from_alphabet(&parsed_input.atomic_propositions))
+        .map(|pt| pt.traces_vec_from_atomic_props(&parsed_input.atomic_propositions))
         .chain(
             parsed_input
                 .negative_traces
                 .into_iter()
-                .map(|pt| pt.traces_vec_from_alphabet(&parsed_input.atomic_propositions)),
+                .map(|pt| pt.traces_vec_from_atomic_props(&parsed_input.atomic_propositions)),
         )
         .collect();
     let traces = traces.expect("Incorrect traces format");
@@ -95,7 +95,7 @@ pub fn parse_traces(buf: &str) -> Instance {
 #[derive(Debug, Clone, Deserialize)]
 pub struct ParsedTrace {
     #[serde(flatten)]
-    alphabet: HashMap<String, Vec<String>>,
+    atomic_propositions: HashMap<String, Vec<String>>,
 }
 
 /// Converts a vector of "0"/"1" strings to a CharSeq
@@ -110,13 +110,13 @@ fn vec_to_cs(v: &Vec<String>) -> CharSeq {
 }
 
 impl ParsedTrace {
-    pub fn traces_vec_from_alphabet(&self, alphabet: &[String]) -> Option<Trace> {
-        let char_seqs: Option<Vec<CharSeq>> = alphabet
+    pub fn traces_vec_from_atomic_props(&self, atomic_propositions: &[String]) -> Option<Trace> {
+        let char_seqs: Option<Box<[CharSeq]>> = atomic_propositions
             .iter()
-            .map(|s| self.alphabet.get(s).map(vec_to_cs))
+            .map(|s| self.atomic_propositions.get(s).map(vec_to_cs))
             .collect();
         Some(Trace {
-            alphabet: char_seqs?,
+            atomic_propositions: char_seqs?,
         })
     }
 }

src/ops/unary.rs

@@ -7,7 +7,7 @@ use crate::ltl::cm::CharMatrix;
 
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
 pub enum LtlUnaryOp {
-    // Not,
+    Not,
     WeakNext,
     StrongNext,
     Finally,
@@ -17,14 +17,13 @@ pub enum LtlUnaryOp {
 impl LtlUnaryOp {
     pub(crate) fn all() -> Vec<LtlUnaryOp> {
         use LtlUnaryOp::*;
-        vec![WeakNext, StrongNext, Finally, Globally]
-        // vec![Not, WeakNext, StrongNext, Finally, Globally]
+        vec![Not, WeakNext, StrongNext, Finally, Globally]
     }
 
     pub(crate) fn is_boolean_monotone(&self) -> bool {
         match self {
-            // LtlUnaryOp::Not => true,
-            LtlUnaryOp::WeakNext
+            LtlUnaryOp::Not
+            | LtlUnaryOp::WeakNext
             | LtlUnaryOp::StrongNext
             | LtlUnaryOp::Finally
             | LtlUnaryOp::Globally => false,
@@ -33,7 +32,7 @@ impl LtlUnaryOp {
 
     pub(crate) fn apply_cm(op: Self, cm: &CharMatrix) -> CharMatrix {
         match op {
-            // LtlUnaryOp::Not => cm.not(),
+            LtlUnaryOp::Not => cm.not(),
             LtlUnaryOp::WeakNext => cm.weak_next(),
             LtlUnaryOp::StrongNext => cm.strong_next(),
             LtlUnaryOp::Finally => cm.finally(),
@@ -55,13 +54,15 @@ impl<'a> TryFrom<&'a str> for LtlUnaryOp {
     ///
     /// | String |   Result  |
     /// |:-------|:---------------------|
+    /// | `"!"`  | [`LtlUnaryOp::Not`]  |
     /// | `"X"`  | [`LtlUnaryOp::WeakNext`]  |
     /// | `"X[!]"`  | [`LtlUnaryOp::StrongNext`]  |
     /// | `"F"`  | [`LtlUnaryOp::Finally`]   |
     /// | `"G"`  | [`LtlUnaryOp::Globally`]|
-    /// | Other value  | `Error` |
+    /// | Other value  | [`InvalidUnaryOp`] |
     fn try_from(value: &'a str) -> Result<Self, Self::Error> {
         match value {
+            "!" => Ok(LtlUnaryOp::Not),
             "X" => Ok(LtlUnaryOp::WeakNext),
             "X[!]" => Ok(LtlUnaryOp::StrongNext),
             "F" => Ok(LtlUnaryOp::Finally),
@@ -74,6 +75,7 @@ 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::Not => write!(f, "!"),
             LtlUnaryOp::WeakNext => write!(f, "X"),
             LtlUnaryOp::StrongNext => write!(f, "X[!]"),
             LtlUnaryOp::Finally => write!(f, "F"),
@@ -88,6 +90,9 @@ mod test {
 
     #[test]
     fn string_try_into_unary_op() {
+        let parsed = "!".try_into();
+        assert_eq!(parsed, Ok(LtlUnaryOp::Not));
+
         let parsed = "X".try_into();
         assert_eq!(parsed, Ok(LtlUnaryOp::WeakNext));
 
@@ -105,7 +110,7 @@ mod test {
     }
 
     #[test]
-    fn binary_op_display_then_parse_is_ident() {
+    fn unary_op_display_then_parse_is_ident() {
         for op in LtlUnaryOp::all() {
             assert_eq!(Ok(op), format!("{op}").as_str().try_into())
         }