Merge pull request #32 from whitemech/feature/ldlf

Add box formula (only with propositional regexes)

lib/include/atom_visitor.hpp

@@ -41,6 +41,7 @@ class AtomsVisitor : public Visitor {
   void visit(const QuotedFormula &) override{};
   void visit(const Symbol &) override{};
   void visit(const LDLfDiamond<PropositionalRegExp> &) override;
+  void visit(const LDLfBox<PropositionalRegExp> &) override;
 
   set_atoms_ptr apply(const PropositionalFormula &b);
   set_atoms_ptr apply(const LDLfFormula &b);

lib/include/basic.hpp

@@ -32,6 +32,7 @@ enum TypeID {
   t_LDLfOr,
   t_LDLfNot,
   t_LDLfDiamond,
+  t_LDLfBox,
   t_PropositionalRegExp,
   t_NFAState,
   t_DFAState,

lib/include/delta.hpp

@@ -52,6 +52,7 @@ class DeltaVisitor : public Visitor {
   void visit(const LDLfOr &) override;
   void visit(const LDLfNot &) override;
   void visit(const LDLfDiamond<PropositionalRegExp> &x) override;
+  void visit(const LDLfBox<PropositionalRegExp> &x) override;
 
   std::shared_ptr<const PropositionalFormula> apply(const LDLfFormula &b);
 };

lib/include/logic.hpp

@@ -160,8 +160,40 @@ template <class T> class LDLfDiamond : public LDLfTemporal<T> {
                            dynamic_cast<const LDLfDiamond &>(o).get_formula());
   };
   std::shared_ptr<const LDLfFormula> logical_not() const override {
-    // TODO return the associated LDLfBoxFormula
-    return nullptr;
+    return std::make_shared<LDLfBox<T>>(this->get_regex(),
+                                        this->get_formula()->logical_not());
+  };
+};
+
+template <class T> class LDLfBox : public LDLfTemporal<T> {
+public:
+  const static TypeID type_code_id = TypeID::t_LDLfBox;
+  bool is_canonical(const set_formulas &container_) const;
+  void accept(Visitor &v) const override { v.visit(*this); };
+  explicit LDLfBox<T>(const std::shared_ptr<const T> &regex,
+                      const ldlf_ptr &formula)
+      : LDLfTemporal<T>(regex, formula) {
+    this->type_code_ = type_code_id;
+  }
+
+  bool is_equal(const Basic &o) const override {
+    return is_a<LDLfBox<T>>(o) and
+           unified_eq(this->get_regex(),
+                      dynamic_cast<const LDLfBox<T> &>(o).get_regex()) and
+           unified_eq(this->get_formula(),
+                      dynamic_cast<const LDLfBox<T> &>(o).get_formula());
+  };
+  int compare(const Basic &o) const override {
+    auto regex_compare = unified_compare(
+        this->get_regex(), dynamic_cast<const LDLfBox &>(o).get_regex());
+    if (regex_compare != 0)
+      return regex_compare;
+    return unified_compare(this->get_formula(),
+                           dynamic_cast<const LDLfBox &>(o).get_formula());
+  };
+  std::shared_ptr<const LDLfFormula> logical_not() const override {
+    return std::make_shared<LDLfDiamond<T>>(this->get_regex(),
+                                            this->get_formula()->logical_not());
   };
 };
 

lib/include/nnf.hpp

@@ -35,6 +35,7 @@ class NNFTransformer : public Visitor {
   void visit(const LDLfOr &) override;
   void visit(const LDLfNot &) override;
   void visit(const LDLfDiamond<PropositionalRegExp> &x) override;
+  void visit(const LDLfBox<PropositionalRegExp> &x) override;
   std::shared_ptr<LDLfFormula> apply(const LDLfFormula &b);
 };
 

lib/include/visitor.hpp

@@ -30,6 +30,7 @@ class Visitor {
   virtual void visit(const LDLfOr &){};
   virtual void visit(const LDLfNot &){};
   virtual void visit(const LDLfDiamond<PropositionalRegExp> &x){};
+  virtual void visit(const LDLfBox<PropositionalRegExp> &x){};
   // TODO add all the combinations of temporal formulas + regular expression
 
   // callbacks for propositional logic

lib/src/atom_visitor.cpp

@@ -53,10 +53,16 @@ void AtomsVisitor::visit(const PropositionalOr &x) {
 
 void AtomsVisitor::visit(const PropositionalNot &x) { apply(*x.get_arg()); }
 
+// TODO merge the two temporal formulas in one single template,
+//  and implement visit for each regex
 void AtomsVisitor::visit(const LDLfDiamond<PropositionalRegExp> &f) {
   result = apply(*f.get_regex()->get_arg());
 }
 
+void AtomsVisitor::visit(const LDLfBox<PropositionalRegExp> &f) {
+  result = apply(*f.get_regex()->get_arg());
+}
+
 set_atoms_ptr AtomsVisitor::apply(const PropositionalFormula &b) {
   b.accept(*this);
   return result;

lib/src/delta.cpp

@@ -71,6 +71,23 @@ void DeltaVisitor::visit(const LDLfDiamond<PropositionalRegExp> &f) {
   }
 }
 
+void DeltaVisitor::visit(const LDLfBox<PropositionalRegExp> &f) {
+  //  TODO epsilon return false only if regexp is propositional
+  if (epsilon) {
+    result = std::make_shared<PropositionalTrue>();
+  } else {
+    assert(this->prop_interpretation.has_value());
+    auto prop = f.get_regex()->get_arg();
+
+    if (eval(*prop, this->prop_interpretation.value())) {
+      // TODO Implement the "E(phi)" in the delta function (Brafman et. al 2018)
+      result = std::make_shared<PropositionalAtom>(quote(f.get_formula()));
+    } else {
+      result = std::make_shared<PropositionalTrue>();
+    }
+  }
+}
+
 std::shared_ptr<const PropositionalFormula>
 DeltaVisitor::apply(const LDLfFormula &b) {
   b.accept(*this);

lib/src/logic.cpp

@@ -213,6 +213,12 @@ bool LDLfDiamond<T>::is_canonical(const set_formulas &container_) const {
   return true;
 }
 
+template <class T>
+bool LDLfBox<T>::is_canonical(const set_formulas &container_) const {
+  // TODO
+  return true;
+}
+
 PropositionalRegExp::PropositionalRegExp(
     std::shared_ptr<const PropositionalFormula> f)
     : arg_{std::move(f)} {

lib/src/nnf.cpp

@@ -54,6 +54,11 @@ void NNFTransformer::visit(const LDLfDiamond<PropositionalRegExp> &x) {
       x.get_regex(), apply(*x.get_formula()));
 }
 
+void NNFTransformer::visit(const LDLfBox<PropositionalRegExp> &x) {
+  result = std::make_shared<LDLfBox<PropositionalRegExp>>(
+      x.get_regex(), apply(*x.get_formula()));
+}
+
 std::shared_ptr<LDLfFormula> NNFTransformer::apply(const LDLfFormula &b) {
   b.accept(*this);
   return result;

lib/test/src/test_translate.cpp

@@ -73,7 +73,7 @@ TEST_CASE("Translate (ff & tt)", "[translate]") {
   REQUIRE(!my_dfa->accepts(trace_two));
 }
 
-TEST_CASE("Translate <true>tt>", "[translate]") {
+TEST_CASE("Translate <true>tt", "[translate]") {
   std::string formula_name = "<true>tt";
   auto true_ = std::make_shared<const PropositionalTrue>();
   auto regex_true = std::make_shared<const PropositionalRegExp>(true_);
@@ -93,7 +93,7 @@ TEST_CASE("Translate <true>tt>", "[translate]") {
   REQUIRE(my_dfa->accepts(trace{false_, false_, false_}));
 }
 
-TEST_CASE("Translate <a>tt>", "[translate]") {
+TEST_CASE("Translate <a>tt", "[translate]") {
   std::string formula_name = "<a>tt";
   auto a = std::make_shared<const PropositionalAtom>("a");
   auto regex_a = std::make_shared<const PropositionalRegExp>(a);
@@ -118,7 +118,7 @@ TEST_CASE("Translate <a>tt>", "[translate]") {
   REQUIRE(!my_dfa->accepts(trace{e, e, e}));
 }
 
-TEST_CASE("Translate <a & b>tt>", "[translate]") {
+TEST_CASE("Translate <a & b>tt", "[translate]") {
   std::string formula_name = "<a & b>tt";
   auto a = std::make_shared<const PropositionalAtom>("a");
   auto b = std::make_shared<const PropositionalAtom>("b");
@@ -151,4 +151,107 @@ TEST_CASE("Translate <a & b>tt>", "[translate]") {
   REQUIRE(my_dfa->accepts(trace{ab_}));
 }
 
+TEST_CASE("Translate {true}tt", "[translate]") {
+  std::string formula_name = "[true]tt";
+  auto true_ = std::make_shared<const PropositionalTrue>();
+  auto regex_true = std::make_shared<const PropositionalRegExp>(true_);
+  auto tt = boolean(true);
+  auto box_formula_true_tt =
+      std::make_shared<LDLfBox<PropositionalRegExp>>(regex_true, tt);
+
+  auto *my_dfa = to_dfa(*box_formula_true_tt);
+
+  // print the DFA
+  dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg");
+
+  auto false_ = interpretation{};
+  REQUIRE(my_dfa->accepts(trace{}));
+  REQUIRE(my_dfa->accepts(trace{false_}));
+  REQUIRE(my_dfa->accepts(trace{false_, false_}));
+  REQUIRE(my_dfa->accepts(trace{false_, false_, false_}));
+}
+
+TEST_CASE("Translate {a}tt", "[translate]") {
+  std::string formula_name = "[a]tt";
+  auto a = std::make_shared<const PropositionalAtom>("a");
+  auto regex_a = std::make_shared<const PropositionalRegExp>(a);
+  auto tt = boolean(true);
+  auto box_formula_a_tt =
+      std::make_shared<LDLfBox<PropositionalRegExp>>(regex_a, tt);
+
+  auto *my_dfa = to_dfa(*box_formula_a_tt);
+
+  // print the DFA
+  dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg");
+
+  auto e = interpretation{0};
+  auto a_ = interpretation{1};
+  REQUIRE(my_dfa->accepts(trace{}));
+  REQUIRE(my_dfa->accepts(trace{e}));
+  REQUIRE(my_dfa->accepts(trace{a_}));
+  REQUIRE(my_dfa->accepts(trace{e, e}));
+  REQUIRE(my_dfa->accepts(trace{e, a_}));
+  REQUIRE(my_dfa->accepts(trace{a_, e}));
+  REQUIRE(my_dfa->accepts(trace{a_, a_}));
+  REQUIRE(my_dfa->accepts(trace{e, e, e}));
+}
+
+TEST_CASE("Translate {a & b}tt", "[translate]") {
+  std::string formula_name = "[a & b]tt";
+  auto a = std::make_shared<const PropositionalAtom>("a");
+  auto b = std::make_shared<const PropositionalAtom>("b");
+  auto a_and_b =
+      std::make_shared<const PropositionalAnd>(set_prop_formulas{a, b});
+  auto regex_a_and_b = std::make_shared<const PropositionalRegExp>(a_and_b);
+  auto tt = boolean(true);
+  auto box_formula_a_and_b_tt =
+      std::make_shared<LDLfBox<PropositionalRegExp>>(regex_a_and_b, tt);
+
+  auto *my_dfa = to_dfa(*box_formula_a_and_b_tt);
+
+  // print the DFA
+  dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg");
+
+  auto e = interpretation{0, 0};
+  auto a_ = interpretation{1, 0};
+  auto b_ = interpretation{0, 1};
+  auto ab_ = interpretation{1, 1};
+  REQUIRE(my_dfa->accepts(trace{}));
+  REQUIRE(my_dfa->accepts(trace{e}));
+  REQUIRE(my_dfa->accepts(trace{a_}));
+  REQUIRE(my_dfa->accepts(trace{b_}));
+  REQUIRE(my_dfa->accepts(trace{e, e}));
+  REQUIRE(my_dfa->accepts(trace{e, a_}));
+  REQUIRE(my_dfa->accepts(trace{a_, e}));
+  REQUIRE(my_dfa->accepts(trace{a_, a_}));
+  REQUIRE(my_dfa->accepts(trace{a_, a_}));
+  REQUIRE(my_dfa->accepts(trace{b_}));
+  REQUIRE(my_dfa->accepts(trace{ab_}));
+}
+
+TEST_CASE("Translate {a}ff", "[translate]") {
+  std::string formula_name = "[a]ff";
+  auto a = std::make_shared<const PropositionalAtom>("a");
+  auto regex_a = std::make_shared<const PropositionalRegExp>(a);
+  auto tt = boolean(false);
+  auto box_formula_a_tt =
+      std::make_shared<LDLfBox<PropositionalRegExp>>(regex_a, tt);
+
+  auto *my_dfa = to_dfa(*box_formula_a_tt);
+
+  // print the DFA
+  dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg");
+
+  auto e = interpretation{0};
+  auto a_ = interpretation{1};
+  REQUIRE(my_dfa->accepts(trace{}));
+  REQUIRE(my_dfa->accepts(trace{e}));
+  REQUIRE(!my_dfa->accepts(trace{a_}));
+  REQUIRE(my_dfa->accepts(trace{e, e}));
+  REQUIRE(my_dfa->accepts(trace{e, a_}));
+  REQUIRE(!my_dfa->accepts(trace{a_, e}));
+  REQUIRE(!my_dfa->accepts(trace{a_, a_}));
+  REQUIRE(my_dfa->accepts(trace{e, e, e}));
+}
+
 } // namespace whitemech::lydia::Test