fix 'to_nnf' of LDLfNot

flloat/ldlf.py

@@ -3,7 +3,7 @@
 from functools import lru_cache
 from typing import Set
 
-from flloat.base.convertible import ConvertibleFormula
+from flloat.base.convertible import ConvertibleFormula, BaseConvertibleFormula
 from flloat.base.delta import (
     Delta,
     DeltaConvertibleFormula,
@@ -220,12 +220,13 @@ def _delta(self, i: PLInterpretation, epsilon=False):
 
 
 class LDLfNot(NotTruth, LDLfFormula, NotNNF):
+
     def _to_nnf(self):
-        neg = self.f.negate()
-        return neg.to_nnf()
+        if isinstance(self.f, AtomicNNF) and not isinstance(self.f, BaseConvertibleFormula):
+            return self.f.negate()
+        else:
+            return self.f.negate().to_nnf()
 
-    def negate(self):
-        return self.f
 
     def _delta(self, i: PLInterpretation, epsilon=False):
         # should never called, since it is called from NNF formulas
@@ -347,6 +348,10 @@ def __str__(self):
     def _to_nnf(self):
         return RegExpTest(self.f.to_nnf())
 
+    def negate(self):
+        return self.Dual(self.Not(self.f))
+
+
     def delta_diamond(self, f: LDLfFormula, i: PLInterpretation, epsilon=False):
         return PLAnd([self.f._delta(i, epsilon), f._delta(i, epsilon)])
 
@@ -483,7 +488,7 @@ def convert(self):
         return LDLfBox(RegExpPropositional(PLTrue()), LDLfLogicalFalse())
 
 
-class LDLfLast(DeltaConvertibleFormula, LDLfAtomic):
+class LDLfLast(DeltaConvertibleFormula, LDLfAtomic, ):
     def __init__(self):
         super().__init__(Symbols.LAST.value)
 

tests/test_ldlf.py

@@ -157,7 +157,9 @@ def test_delta():
     assert parser("[B]ff").delta(i_b) == PLAtomic(ff)
     assert parser("[B]ff").delta(i_ab) == PLAtomic(ff)
 
-    f = parser("!(<!(A<->B)+(B;A)*+(!last)?>[(true)*]end)")
+    f = parser("!(<(!last)?>end)")
+    a = f.delta(i_)
+    b = f.to_nnf().delta(i_)
     assert f.delta(i_) == f.to_nnf().delta(i_)
     assert f.delta(i_ab) == f.to_nnf().delta(i_ab)