diff --git a/lib/include/atom_visitor.hpp b/lib/include/atom_visitor.hpp
index d15036d1..e1939c66 100644
--- a/lib/include/atom_visitor.hpp
+++ b/lib/include/atom_visitor.hpp
@@ -31,6 +31,30 @@ class AtomsVisitor : public Visitor {
 public:
   static Logger logger;
 
+  // callbacks for LDLf
+  void visit(const Symbol &) override{};
+  void visit(const LDLfBooleanAtom &) override{};
+  void visit(const LDLfAnd &) override{};
+  void visit(const LDLfOr &) override{};
+  void visit(const LDLfNot &) override{};
+  void visit(const LDLfDiamond<PropositionalRegExp> &x) override {
+    this->visit_temporal(x);
+  };
+  void visit(const LDLfDiamond<TestRegExp> &x) override {
+    this->visit_temporal(x);
+  };
+  void visit(const LDLfBox<PropositionalRegExp> &x) override {
+    this->visit_temporal(x);
+  };
+  void visit(const LDLfBox<TestRegExp> &x) override {
+    this->visit_temporal(x);
+  };
+
+  // callbacks for regular expressions
+  void visit(const PropositionalRegExp &) override;
+  void visit(const TestRegExp &) override;
+
+  // callbacks for propositional logic
   void visit(const PropositionalTrue &) override;
   void visit(const PropositionalFalse &) override;
   void visit(const PropositionalAtom &) override;
@@ -39,12 +63,16 @@ class AtomsVisitor : public Visitor {
   void visit(const PropositionalNot &) override;
 
   void visit(const QuotedFormula &) override{};
-  void visit(const Symbol &) override{};
-  void visit(const LDLfDiamond<PropositionalRegExp> &) override;
-  void visit(const LDLfBox<PropositionalRegExp> &) override;
+
+  template <class R> void inline visit_temporal(const LDLfTemporal<R> &x) {
+    result = apply(*x.get_regex());
+    auto y = apply(*x.get_formula());
+    result.insert(y.begin(), y.end());
+  }
 
   set_atoms_ptr apply(const PropositionalFormula &b);
   set_atoms_ptr apply(const LDLfFormula &b);
+  set_atoms_ptr apply(const RegExp &b);
 };
 
 set_atoms_ptr find_atoms(const LDLfFormula &);
diff --git a/lib/include/basic.hpp b/lib/include/basic.hpp
index 0025d50b..8bef3dc0 100644
--- a/lib/include/basic.hpp
+++ b/lib/include/basic.hpp
@@ -34,6 +34,7 @@ enum TypeID {
   t_LDLfDiamond,
   t_LDLfBox,
   t_PropositionalRegExp,
+  t_TestRegExp,
   t_NFAState,
   t_DFAState,
   t_PropositionalTrue,
diff --git a/lib/include/delta.hpp b/lib/include/delta.hpp
index c976b167..b754200d 100644
--- a/lib/include/delta.hpp
+++ b/lib/include/delta.hpp
@@ -46,13 +46,31 @@ class DeltaVisitor : public Visitor {
   explicit DeltaVisitor(const set_atoms_ptr &prop_interpretation)
       : prop_interpretation{prop_interpretation}, epsilon{false} {}
 
+  // callbacks for LDLf
   void visit(const Symbol &) override{};
   void visit(const LDLfBooleanAtom &) override;
   void visit(const LDLfAnd &) override;
   void visit(const LDLfOr &) override;
   void visit(const LDLfNot &) override;
   void visit(const LDLfDiamond<PropositionalRegExp> &x) override;
+  void visit(const LDLfDiamond<TestRegExp> &) override;
   void visit(const LDLfBox<PropositionalRegExp> &x) override;
+  void visit(const LDLfBox<TestRegExp> &) override;
+  // TODO add all the combinations of temporal formulas + regular expression
+
+  // callbacks for regular expressions
+  void visit(const PropositionalRegExp &) override{};
+  void visit(const TestRegExp &) override{};
+
+  // callbacks for propositional logic
+  void visit(const PropositionalTrue &) override{};
+  void visit(const PropositionalFalse &) override{};
+  void visit(const PropositionalAtom &) override{};
+  void visit(const PropositionalAnd &) override{};
+  void visit(const PropositionalOr &) override{};
+  void visit(const PropositionalNot &) override{};
+
+  void visit(const QuotedFormula &) override{};
 
   std::shared_ptr<const PropositionalFormula> apply(const LDLfFormula &b);
 };
diff --git a/lib/include/logic.hpp b/lib/include/logic.hpp
index 2d9021e7..67af0392 100644
--- a/lib/include/logic.hpp
+++ b/lib/include/logic.hpp
@@ -111,7 +111,11 @@ class LDLfNot : public LDLfFormula {
 
 // TODO consider template check "enable_if_t" vs static_assert in constructor
 // template <class T, class=std::enable_if_t<std::is_base_of_v<RegExp, T>>>
-template <class T> class LDLfTemporal : public LDLfFormula {
+// template <class T>
+// template <typename T, typename = typename
+// std::enable_if<std::is_base_of<RegExp, T>::value, T>::type>
+// template <typename T, typename>
+template <typename T> class LDLfTemporal : public LDLfFormula {
 private:
   const ldlf_ptr arg_;
   const std::shared_ptr<const T> regex_;
@@ -123,6 +127,9 @@ template <class T> class LDLfTemporal : public LDLfFormula {
     static_assert(std::is_base_of<RegExp, T>::value,
                   "concrete RegExp class not derived from RegExp");
   }
+  explicit LDLfTemporal<T>(const std::shared_ptr<const RegExp> &regex,
+                           const ldlf_ptr &formula)
+      : regex_{std::dynamic_pointer_cast<const T>(regex)}, arg_{formula} {}
   ldlf_ptr get_formula() const { return arg_; };
   std::shared_ptr<const T> get_regex() const { return regex_; };
   hash_t compute_hash_() const override {
@@ -133,7 +140,11 @@ template <class T> class LDLfTemporal : public LDLfFormula {
   };
 };
 
-template <class T> class LDLfDiamond : public LDLfTemporal<T> {
+// template <class T>
+// template <typename T, typename = typename
+// std::enable_if<std::is_base_of<RegExp, T>::value, T>::type>
+// template <typename T, typename>
+template <typename T> class LDLfDiamond : public LDLfTemporal<T> {
 public:
   const static TypeID type_code_id = TypeID::t_LDLfDiamond;
   bool is_canonical(const set_formulas &container_) const;
@@ -143,6 +154,11 @@ template <class T> class LDLfDiamond : public LDLfTemporal<T> {
       : LDLfTemporal<T>(regex, formula) {
     this->type_code_ = type_code_id;
   }
+  explicit LDLfDiamond<T>(const std::shared_ptr<const RegExp> &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<LDLfDiamond<T>>(o) and
@@ -160,12 +176,17 @@ template <class T> class LDLfDiamond : public LDLfTemporal<T> {
                            dynamic_cast<const LDLfDiamond &>(o).get_formula());
   };
   std::shared_ptr<const LDLfFormula> logical_not() const override {
-    return std::make_shared<LDLfBox<T>>(this->get_regex(),
-                                        this->get_formula()->logical_not());
+    //    return std::make_shared<LDLfBox<T>>(this->get_regex(),
+    //                                        this->get_formula()->logical_not());
+    return std::make_shared<LDLfDiamond<T>>(this->get_regex(),
+                                            this->get_formula()->logical_not());
   };
 };
 
-template <class T> class LDLfBox : public LDLfTemporal<T> {
+// template <typename T, typename = typename
+// std::enable_if<std::is_base_of<RegExp, T>::value, T>::type>
+// template <typename T, typename>
+template <typename T> class LDLfBox : public LDLfTemporal<T> {
 public:
   const static TypeID type_code_id = TypeID::t_LDLfBox;
   bool is_canonical(const set_formulas &container_) const;
@@ -175,6 +196,11 @@ template <class T> class LDLfBox : public LDLfTemporal<T> {
       : LDLfTemporal<T>(regex, formula) {
     this->type_code_ = type_code_id;
   }
+  explicit LDLfBox<T>(const std::shared_ptr<const RegExp> &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
@@ -205,15 +231,30 @@ class PropositionalRegExp : public RegExp {
 
 public:
   const static TypeID type_code_id = TypeID::t_PropositionalRegExp;
-  void accept(Visitor &v) const override{};
+  void accept(Visitor &v) const override;
   explicit PropositionalRegExp(std::shared_ptr<const PropositionalFormula> f);
-  bool is_canonical(const set_formulas &container_) const;
+  bool is_canonical(const PropositionalFormula &f) const;
   hash_t compute_hash_() const override;
   std::shared_ptr<const PropositionalFormula> get_arg() const;
   bool is_equal(const Basic &o) const override;
   int compare(const Basic &o) const override;
 };
 
+class TestRegExp : public RegExp {
+private:
+  const std::shared_ptr<const LDLfFormula> arg_;
+
+public:
+  const static TypeID type_code_id = TypeID::t_TestRegExp;
+  void accept(Visitor &v) const override;
+  explicit TestRegExp(std::shared_ptr<const LDLfFormula> f);
+  bool is_canonical(const LDLfFormula &f) const;
+  hash_t compute_hash_() const override;
+  std::shared_ptr<const LDLfFormula> get_arg() const;
+  bool is_equal(const Basic &o) const override;
+  int compare(const Basic &o) const override;
+};
+
 class QuotedFormula : public Basic {
 private:
 protected:
diff --git a/lib/include/nnf.hpp b/lib/include/nnf.hpp
index 76d8eb14..8dbb3dcc 100644
--- a/lib/include/nnf.hpp
+++ b/lib/include/nnf.hpp
@@ -26,20 +26,61 @@ namespace lydia {
 class NNFTransformer : public Visitor {
 private:
 protected:
-  std::shared_ptr<LDLfFormula> result;
+  // TODO split into several transformers?
+  std::shared_ptr<const LDLfFormula> result;
+  std::shared_ptr<const RegExp> regex_result;
 
 public:
+  // callbacks for LDLf
   void visit(const Symbol &) override{};
   void visit(const LDLfBooleanAtom &) override;
   void visit(const LDLfAnd &) override;
   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);
+  void visit(const LDLfDiamond<PropositionalRegExp> &x) override {
+    this->visit_temporal(x);
+  };
+  void visit(const LDLfDiamond<TestRegExp> &x) override {
+    this->visit_temporal(x);
+  };
+  void visit(const LDLfBox<PropositionalRegExp> &x) override {
+    this->visit_temporal(x);
+  };
+  void visit(const LDLfBox<TestRegExp> &x) override {
+    this->visit_temporal(x);
+  };
+
+  // callbacks for regular expressions
+  void visit(const PropositionalRegExp &) override;
+  void visit(const TestRegExp &) override;
+
+  // callbacks for propositional logic
+  void visit(const PropositionalTrue &) override{};
+  void visit(const PropositionalFalse &) override{};
+  void visit(const PropositionalAtom &) override{};
+  void visit(const PropositionalAnd &) override{};
+  void visit(const PropositionalOr &) override{};
+  void visit(const PropositionalNot &) override{};
+
+  void visit(const QuotedFormula &) override{};
+
+  std::shared_ptr<const LDLfFormula> apply(const LDLfFormula &b);
+  std::shared_ptr<const RegExp> apply(const RegExp &b);
+
+  template <typename T, typename = typename std::enable_if<
+                            std::is_base_of<RegExp, T>::value, T>::type>
+  void inline visit_temporal(const LDLfTemporal<T> &x) {
+    if (x.type_code_ == TypeID::t_LDLfDiamond) {
+      result = std::make_shared<LDLfDiamond<T>>(apply(*x.get_regex()),
+                                                apply(*x.get_formula()));
+    } else if (x.type_code_ == TypeID::t_LDLfBox) {
+      result = std::make_shared<LDLfBox<T>>(apply(*x.get_regex()),
+                                            apply(*x.get_formula()));
+    }
+  }
 };
 
-std::shared_ptr<LDLfFormula> to_nnf(const LDLfFormula &);
+std::shared_ptr<const LDLfFormula> to_nnf(const LDLfFormula &);
 
 } // namespace lydia
 } // namespace whitemech
\ No newline at end of file
diff --git a/lib/include/propositional_logic.hpp b/lib/include/propositional_logic.hpp
index fc7796d5..f8da0ac0 100644
--- a/lib/include/propositional_logic.hpp
+++ b/lib/include/propositional_logic.hpp
@@ -128,12 +128,33 @@ class EvalVisitor : public Visitor {
 public:
   explicit EvalVisitor(const set_atoms_ptr &interpretation)
       : interpretation{interpretation} {};
+
+  // callbacks for LDLf
+  void visit(const Symbol &) override{};
+  void visit(const LDLfBooleanAtom &) override{};
+  void visit(const LDLfAnd &) override{};
+  void visit(const LDLfOr &) override{};
+  void visit(const LDLfNot &) override{};
+  void visit(const LDLfDiamond<PropositionalRegExp> &) override{};
+  void visit(const LDLfDiamond<TestRegExp> &) override{};
+  void visit(const LDLfBox<PropositionalRegExp> &) override{};
+  void visit(const LDLfBox<TestRegExp> &) override{};
+  // TODO add all the combinations of temporal formulas + regular expression
+
+  // callbacks for regular expressions
+  void visit(const PropositionalRegExp &) override{};
+  void visit(const TestRegExp &) override{};
+
+  // callbacks for propositional logic
   void visit(const PropositionalTrue &) override;
   void visit(const PropositionalFalse &) override;
   void visit(const PropositionalAtom &) override;
   void visit(const PropositionalAnd &) override;
   void visit(const PropositionalOr &) override;
   void visit(const PropositionalNot &) override;
+
+  void visit(const QuotedFormula &) override{};
+
   bool apply(const PropositionalFormula &b);
 };
 
diff --git a/lib/include/types.hpp b/lib/include/types.hpp
index 4f0fd6e6..bcd4e1b7 100644
--- a/lib/include/types.hpp
+++ b/lib/include/types.hpp
@@ -29,15 +29,17 @@ namespace lydia {
 
 class Basic;
 class Symbol;
-class RegExp;
 class LDLfFormula;
 class LDLfBooleanAtom;
 class LDLfAnd;
 class LDLfOr;
 class LDLfNot;
-template <class T> class LDLfDiamond;
-template <class T> class LDLfBox;
+class RegExp;
 class PropositionalRegExp;
+class TestRegExp;
+template <typename T> class LDLfTemporal;
+template <typename T> class LDLfDiamond;
+template <typename T> class LDLfBox;
 class PropositionalFormula;
 class PropositionalAtom;
 class PropositionalTrue;
diff --git a/lib/include/utils/print.hpp b/lib/include/utils/print.hpp
index 365654ee..f41d3fc9 100644
--- a/lib/include/utils/print.hpp
+++ b/lib/include/utils/print.hpp
@@ -32,12 +32,34 @@ class StrPrinter : public Visitor {
   std::string result;
 
 public:
+  // callbacks for LDLf
   void visit(const Symbol &) override;
   void visit(const LDLfBooleanAtom &) override;
   void visit(const LDLfAnd &) override;
   void visit(const LDLfOr &) override;
   void visit(const LDLfNot &) override;
+  void visit(const LDLfDiamond<PropositionalRegExp> &) override{};
+  void visit(const LDLfDiamond<TestRegExp> &) override{};
+  void visit(const LDLfBox<PropositionalRegExp> &) override{};
+  void visit(const LDLfBox<TestRegExp> &) override{};
+  // TODO add all the combinations of temporal formulas + regular expression
+
+  // callbacks for regular expressions
+  void visit(const PropositionalRegExp &) override{};
+  void visit(const TestRegExp &) override{};
+
+  // callbacks for propositional logic
+  void visit(const PropositionalTrue &) override{};
+  void visit(const PropositionalFalse &) override{};
+  void visit(const PropositionalAtom &) override{};
+  void visit(const PropositionalAnd &) override{};
+  void visit(const PropositionalOr &) override{};
+  void visit(const PropositionalNot &) override{};
+
+  void visit(const QuotedFormula &) override{};
+
   template <class T> void visit(const LDLfDiamond<T> &);
+
   std::string apply(const vec_basic &v);
   std::string apply(const set_formulas &v);
   std::string apply(const Basic &b);
diff --git a/lib/include/visitor.hpp b/lib/include/visitor.hpp
index 763eb4fd..56a10407 100644
--- a/lib/include/visitor.hpp
+++ b/lib/include/visitor.hpp
@@ -24,23 +24,31 @@ namespace lydia {
 
 class Visitor {
 public:
-  virtual void visit(const Symbol &){};
-  virtual void visit(const LDLfBooleanAtom &){};
-  virtual void visit(const LDLfAnd &){};
-  virtual void visit(const LDLfOr &){};
-  virtual void visit(const LDLfNot &){};
-  virtual void visit(const LDLfDiamond<PropositionalRegExp> &x){};
-  virtual void visit(const LDLfBox<PropositionalRegExp> &x){};
+  // callbacks for LDLf
+  virtual void visit(const Symbol &) = 0;
+  virtual void visit(const LDLfBooleanAtom &) = 0;
+  virtual void visit(const LDLfAnd &) = 0;
+  virtual void visit(const LDLfOr &) = 0;
+  virtual void visit(const LDLfNot &) = 0;
+  virtual void visit(const LDLfDiamond<PropositionalRegExp> &) = 0;
+  virtual void visit(const LDLfDiamond<TestRegExp> &) = 0;
+  virtual void visit(const LDLfBox<PropositionalRegExp> &) = 0;
+  virtual void visit(const LDLfBox<TestRegExp> &) = 0;
   // TODO add all the combinations of temporal formulas + regular expression
 
+  // callbacks for regular expressions
+  virtual void visit(const PropositionalRegExp &) = 0;
+  virtual void visit(const TestRegExp &) = 0;
+
   // callbacks for propositional logic
-  virtual void visit(const PropositionalTrue &){};
-  virtual void visit(const PropositionalFalse &){};
-  virtual void visit(const PropositionalAtom &){};
-  virtual void visit(const QuotedFormula &){};
-  virtual void visit(const PropositionalAnd &){};
-  virtual void visit(const PropositionalOr &){};
-  virtual void visit(const PropositionalNot &){};
+  virtual void visit(const PropositionalTrue &) = 0;
+  virtual void visit(const PropositionalFalse &) = 0;
+  virtual void visit(const PropositionalAtom &) = 0;
+  virtual void visit(const PropositionalAnd &) = 0;
+  virtual void visit(const PropositionalOr &) = 0;
+  virtual void visit(const PropositionalNot &) = 0;
+
+  virtual void visit(const QuotedFormula &) = 0;
 };
 
 } // namespace lydia
diff --git a/lib/src/atom_visitor.cpp b/lib/src/atom_visitor.cpp
index ad3a8f95..cb620284 100644
--- a/lib/src/atom_visitor.cpp
+++ b/lib/src/atom_visitor.cpp
@@ -53,15 +53,11 @@ 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 PropositionalRegExp &r) {
+  result = apply(*r.get_arg());
 }
 
-void AtomsVisitor::visit(const LDLfBox<PropositionalRegExp> &f) {
-  result = apply(*f.get_regex()->get_arg());
-}
+void AtomsVisitor::visit(const TestRegExp &r) { result = apply(*r.get_arg()); }
 
 set_atoms_ptr AtomsVisitor::apply(const PropositionalFormula &b) {
   b.accept(*this);
@@ -73,6 +69,11 @@ set_atoms_ptr AtomsVisitor::apply(const LDLfFormula &b) {
   return result;
 }
 
+set_atoms_ptr AtomsVisitor::apply(const RegExp &b) {
+  b.accept(*this);
+  return result;
+}
+
 set_atoms_ptr find_atoms(const PropositionalFormula &f) {
   AtomsVisitor atomsVisitor;
   return atomsVisitor.apply(f);
diff --git a/lib/src/delta.cpp b/lib/src/delta.cpp
index cc6992e7..6eda6027 100644
--- a/lib/src/delta.cpp
+++ b/lib/src/delta.cpp
@@ -18,6 +18,7 @@
 #include <cassert>
 #include <delta.hpp>
 #include <logger.hpp>
+#include <nnf.hpp>
 
 namespace whitemech {
 namespace lydia {
@@ -94,6 +95,22 @@ DeltaVisitor::apply(const LDLfFormula &b) {
   return result;
 }
 
+void DeltaVisitor::visit(const LDLfDiamond<TestRegExp> &x) {
+  auto regex_delta = apply(*x.get_regex()->get_arg());
+  auto ldlf_delta = apply(*x.get_formula());
+  result = std::make_shared<PropositionalAnd>(
+      set_prop_formulas{regex_delta, ldlf_delta});
+}
+
+void DeltaVisitor::visit(const LDLfBox<TestRegExp> &x) {
+  NNFTransformer nnfTransformer;
+  auto regex_delta =
+      apply(*nnfTransformer.apply(LDLfNot(x.get_regex()->get_arg())));
+  auto ldlf_delta = apply(*x.get_formula());
+  result = std::make_shared<PropositionalOr>(
+      set_prop_formulas{regex_delta, ldlf_delta});
+}
+
 std::shared_ptr<const PropositionalFormula> delta(const LDLfFormula &x) {
   // epsilon = true
   DeltaVisitor deltaVisitor;
diff --git a/lib/src/logic.cpp b/lib/src/logic.cpp
index 11152bc0..ce1e786c 100644
--- a/lib/src/logic.cpp
+++ b/lib/src/logic.cpp
@@ -193,6 +193,7 @@ std::shared_ptr<const LDLfFormula> LDLfNot::logical_not() const {
 }
 
 hash_t QuotedFormula::compute_hash_() const {
+  // TODO is this correct? shouldn't be combined with TypeID?
   return this->formula->compute_hash_();
 }
 
@@ -226,8 +227,9 @@ PropositionalRegExp::PropositionalRegExp(
 }
 
 hash_t PropositionalRegExp::compute_hash_() const {
-  // TODO
-  return 0;
+  hash_t seed = TypeID::t_PropositionalRegExp;
+  hash_combine<Basic>(seed, *arg_);
+  return seed;
 }
 
 std::shared_ptr<const PropositionalFormula>
@@ -246,7 +248,35 @@ int PropositionalRegExp::compare(const Basic &o) const {
       *dynamic_cast<const PropositionalRegExp &>(o).get_arg());
 }
 
-bool PropositionalRegExp::is_canonical(const set_formulas &container_) const {
+bool PropositionalRegExp::is_canonical(const PropositionalFormula &f) const {
+  // TODO
+  return true;
+}
+
+TestRegExp::TestRegExp(std::shared_ptr<const LDLfFormula> f)
+    : arg_{std::move(f)} {
+  this->type_code_ = type_code_id;
+}
+
+hash_t TestRegExp::compute_hash_() const {
+  hash_t seed = TypeID::t_TestRegExp;
+  hash_combine<Basic>(seed, *arg_);
+  return seed;
+}
+
+std::shared_ptr<const LDLfFormula> TestRegExp::get_arg() const { return arg_; }
+
+bool TestRegExp::is_equal(const Basic &o) const {
+  return is_a<TestRegExp>(o) and
+         eq(*arg_, *dynamic_cast<const TestRegExp &>(o).get_arg());
+}
+
+int TestRegExp::compare(const Basic &o) const {
+  assert(is_a<TestRegExp>(o));
+  return arg_->compare_(*dynamic_cast<const TestRegExp &>(o).get_arg());
+}
+
+bool TestRegExp::is_canonical(const LDLfFormula &f) const {
   // TODO
   return true;
 }
diff --git a/lib/src/nnf.cpp b/lib/src/nnf.cpp
index 89451ccf..b03e2aa9 100644
--- a/lib/src/nnf.cpp
+++ b/lib/src/nnf.cpp
@@ -16,8 +16,6 @@
  */
 
 #include "nnf.hpp"
-#include <sstream>
-#include <stdexcept>
 
 namespace whitemech {
 namespace lydia {
@@ -49,22 +47,25 @@ void NNFTransformer::visit(const LDLfNot &x) {
   result = new_formula;
 }
 
-void NNFTransformer::visit(const LDLfDiamond<PropositionalRegExp> &x) {
-  result = std::make_shared<LDLfDiamond<PropositionalRegExp>>(
-      x.get_regex(), apply(*x.get_formula()));
+std::shared_ptr<const LDLfFormula> NNFTransformer::apply(const LDLfFormula &b) {
+  b.accept(*this);
+  return result;
 }
 
-void NNFTransformer::visit(const LDLfBox<PropositionalRegExp> &x) {
-  result = std::make_shared<LDLfBox<PropositionalRegExp>>(
-      x.get_regex(), apply(*x.get_formula()));
+std::shared_ptr<const RegExp> NNFTransformer::apply(const RegExp &b) {
+  b.accept(*this);
+  return regex_result;
 }
 
-std::shared_ptr<LDLfFormula> NNFTransformer::apply(const LDLfFormula &b) {
-  b.accept(*this);
-  return result;
+void NNFTransformer::visit(const PropositionalRegExp &x) {
+  regex_result = std::make_shared<PropositionalRegExp>(x.get_arg());
+}
+
+void NNFTransformer::visit(const TestRegExp &x) {
+  regex_result = std::make_shared<TestRegExp>(apply(*x.get_arg()));
 }
 
-std::shared_ptr<LDLfFormula> to_nnf(const LDLfFormula &x) {
+std::shared_ptr<const LDLfFormula> to_nnf(const LDLfFormula &x) {
   NNFTransformer nnfTransformer;
   return nnfTransformer.apply(x);
 }
diff --git a/lib/src/visitor.cpp b/lib/src/visitor.cpp
index 93f0ebeb..aa1416d6 100644
--- a/lib/src/visitor.cpp
+++ b/lib/src/visitor.cpp
@@ -27,10 +27,9 @@ void LDLfBooleanAtom::accept(Visitor &v) const { v.visit(*this); }
 void LDLfOr::accept(Visitor &v) const { v.visit(*this); }
 void LDLfAnd::accept(Visitor &v) const { v.visit(*this); }
 void LDLfNot::accept(Visitor &v) const { v.visit(*this); }
-// template<class T> void LDLfDiamond<T>::accept(Visitor &v) const {
-// v.visit(*this); }; template<> void
-// LDLfDiamond<PropositionalRegExp>::accept(Visitor &v) const { v.visit(*this);
-// };
+
+void PropositionalRegExp::accept(Visitor &v) const { v.visit(*this); }
+void TestRegExp::accept(Visitor &v) const { v.visit(*this); }
 
 // TODO add other accept methods
 
diff --git a/lib/test/src/test_translate.cpp b/lib/test/src/test_translate.cpp
index a8150b11..cdfc8aa3 100644
--- a/lib/test/src/test_translate.cpp
+++ b/lib/test/src/test_translate.cpp
@@ -254,4 +254,49 @@ TEST_CASE("Translate {a}ff", "[translate]") {
   REQUIRE(my_dfa->accepts(trace{e, e, e}));
 }
 
+TEST_CASE("Translate <<true>tt?>tt", "[translate]") {
+  std::string formula_name = "<<true>tt?>tt";
+  auto true_ = std::make_shared<const PropositionalTrue>();
+  auto regex_true = std::make_shared<const PropositionalRegExp>(true_);
+  auto tt = boolean(true);
+  auto diamond_formula_true_tt =
+      std::make_shared<LDLfDiamond<PropositionalRegExp>>(regex_true, tt);
+  auto regex_test = std::make_shared<const TestRegExp>(diamond_formula_true_tt);
+  auto diamond_test = std::make_shared<LDLfDiamond<TestRegExp>>(regex_test, tt);
+
+  auto *my_dfa = to_dfa(*diamond_test);
+
+  // 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 <{true}ff?>tt", "[translate]") {
+  std::string formula_name = "<[true]ff?>tt";
+  auto true_ = std::make_shared<const PropositionalTrue>();
+  auto regex_true = std::make_shared<const PropositionalRegExp>(true_);
+  auto tt = boolean(true);
+  auto ff = boolean(false);
+  auto box_formula_true_ff =
+      std::make_shared<LDLfBox<PropositionalRegExp>>(regex_true, ff);
+  auto regex_test = std::make_shared<const TestRegExp>(box_formula_true_ff);
+  auto diamond_test = std::make_shared<LDLfDiamond<TestRegExp>>(regex_test, tt);
+
+  auto *my_dfa = to_dfa(*diamond_test);
+
+  // 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_}));
+}
+
 } // namespace whitemech::lydia::Test
\ No newline at end of file