Fix constants

Author: GBathie

src/algos/mod.rs

@@ -25,6 +25,7 @@ use crate::{
         AtomicProposition, Constant, LtlFormula,
         cache::LtlCache,
         charac::LtlCharac,
+        cm::CharMatrix,
         trace::{Operators, Trace},
     },
     traits::EqTarget,
@@ -56,22 +57,16 @@ pub(crate) fn atoms(traces: &[Trace], atomic_propositions: Vec<String>) -> Vec<L
     let mut atoms = Vec::new();
 
     let true_f = Formula::new_base(
-        traces
-            .iter()
-            .filter_map(|t| t.atomic_propositions.first().map(|&p| p | !p))
-            .collect::<LtlCharac>(),
+        LtlCharac::new(CharMatrix::true_like(traces)),
         1,
         Rc::from(FormulaTree::Const(Constant::True)),
     );
     atoms.push(true_f);
 
     let false_f = Formula::new_base(
-        traces
-            .iter()
-            .filter_map(|t| t.atomic_propositions.first().map(|&p| p | !p))
-            .collect::<LtlCharac>(),
+        LtlCharac::new(CharMatrix::false_like(traces)),
         1,
-        Rc::from(FormulaTree::Const(Constant::True)),
+        Rc::from(FormulaTree::Const(Constant::False)),
     );
     atoms.push(false_f);
 

src/tests/end_to_end.rs

@@ -3,10 +3,10 @@ use itertools::Itertools;
 use crate::{
     algos::{atoms, create_initial_cache, enumeration::aux::enum_aux},
     formula::{rebuild_formula, tree::FormulaTree},
-    ltl::trace::parse_traces,
+    ltl::{Constant, trace::parse_traces},
 };
 
-use super::{AND, F, G, Not, OR, SX, build_atom};
+use super::{AND, F, G, Not, OR, SX, build_atom, build_const};
 
 fn test_ltl_search(instance: &str, expected: FormulaTree) {
     let instance = parse_traces(&instance);
@@ -17,6 +17,7 @@ fn test_ltl_search(instance: &str, expected: FormulaTree) {
     );
 
     let atoms = atoms(&instance.traces, instance.atomic_propositions);
+
     // Add initial formulas
     let (atom, mut ltl_cache) = create_initial_cache(atoms, &instance.target);
     if let Some(f) = atom {
@@ -120,6 +121,14 @@ fn instance_str(
 }
 
 macro_rules! make_instance {
+    (pos : [],
+     neg: [$( { $( $name:ident : [$($v2:literal),*]),* }), *]) => {
+        &instance_str(
+            &[ ],
+            &[ $( &[ $( &[ $( $v2),* ]),* ]),*],
+            & helper!{ $([ $( $name ),* ]),* }
+        )
+    };
     (pos : [$( { $( $name:ident : [$($v:literal),*]),* }), *],
      neg: [$( { $( $name2:ident : [$($v2:literal),*]),* }), *]) => {
         &instance_str(
@@ -308,3 +317,43 @@ fn a_and_b_and_c() {
     );
     test_ltl_search(example, exp);
 }
+
+#[test]
+fn empty_neg_is_true() {
+    let example = make_instance!(
+    pos: [
+        {
+            a: [1, 0, 1, 1],
+            b: [1, 0, 0, 1],
+            c: [1, 0, 1, 0]
+        },
+        {
+            a: [1, 1, 0],
+            b: [1, 0, 1],
+            c: [1, 1, 1]
+        }
+    ],
+    neg: []);
+    let exp = build_const(Constant::True);
+    test_ltl_search(example, exp);
+}
+
+#[test]
+fn empty_pos_is_false() {
+    let example = make_instance!(
+    pos: [ ],
+    neg: [
+        {
+            a: [1, 0, 1, 1],
+            b: [1, 0, 0, 1],
+            c: [1, 0, 1, 0]
+        },
+        {
+            a: [1, 1, 0],
+            b: [1, 0, 1],
+            c: [1, 1, 1]
+        }
+    ]);
+    let exp = build_const(Constant::False);
+    test_ltl_search(example, exp);
+}