Merge pull request #21 from whitemech/ltl-termination

Support for LTLfLast.

flloat/base.py

@@ -223,7 +223,7 @@ class FiniteTraceTruth:
     """Interface for formulas that support the trace semantics."""
 
     @abstractmethod
-    def truth(self, i: FiniteTrace, pos: int) -> bool:
+    def truth(self, i: FiniteTrace, pos: int = 0) -> bool:
         """
         Return the truth evaluation of the formula wrt the trace.
 

flloat/ldlf.py

@@ -166,7 +166,7 @@ def _delta(self, i: PropositionalInterpretation, epsilon=False):
         """Apply the delta function."""
         return self.to_nnf()._delta(i, epsilon=epsilon)
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return self.to_nnf().truth(i, pos)
 
@@ -263,7 +263,7 @@ def negate(self) -> LDLfFormula:
         """Negate the formula."""
         return self.f
 
-    def truth(self, i: FiniteTrace, pos: int) -> bool:
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return not self.f.truth(i, pos)
 
@@ -300,7 +300,7 @@ def negate(self) -> LDLfFormula:
         """Negate the formula."""
         return LDLfOr([f.negate() for f in self.formulas])
 
-    def truth(self, i: FiniteTrace, pos: int) -> bool:
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return all(f.truth(i, pos) for f in self.formulas)
 
@@ -321,7 +321,7 @@ def negate(self) -> LDLfFormula:
         """Negate the formula."""
         return LDLfOr([f.negate() for f in self.formulas])
 
-    def truth(self, i: FiniteTrace, pos: int) -> bool:
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return any(f.truth(i, pos) for f in self.formulas)
 
@@ -338,7 +338,7 @@ def operator_symbol(self) -> OpSymbol:
         """Get the operator symbol."""
         return Symbols.IMPLIES.value
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return self.to_nnf().truth(i, pos)
 
@@ -369,7 +369,7 @@ def operator_symbol(self) -> OpSymbol:
         """Get the operator symbol."""
         return Symbols.EQUIVALENCE.value
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return self.to_nnf().truth(i, pos)
 
@@ -685,7 +685,7 @@ def find_labels(self) -> Set[AtomSymbol]:
         """Find the labels."""
         return self.to_nnf().find_labels()
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return self.to_nnf().truth(i, pos)
 
@@ -716,7 +716,7 @@ def find_labels(self) -> Set[AtomSymbol]:
         """Find the labels."""
         return self.to_nnf().find_labels()
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return self.to_nnf().truth(i, pos)
 
@@ -768,7 +768,7 @@ def find_labels(self):
         """Find the labels."""
         return super().find_labels()
 
-    def truth(self, tr: FiniteTrace, pos: int):
+    def truth(self, tr: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         raise NotImplementedError
 
@@ -805,7 +805,7 @@ def find_labels(self):
         """Find the labels."""
         return super().find_labels()
 
-    def truth(self, tr: FiniteTrace, pos: int):
+    def truth(self, tr: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         raise NotImplementedError
 

flloat/ltlf.py

@@ -219,7 +219,7 @@ def _delta(self, i: PropositionalInterpretation, epsilon=False):
         """Apply the delta function."""
         return PLAnd([f._delta(i, epsilon) for f in self.formulas])
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return all(f.truth(i, pos) for f in self.formulas)
 
@@ -247,7 +247,7 @@ def _delta(self, i: PropositionalInterpretation, epsilon=False):
         """Apply the delta function."""
         return PLOr([f._delta(i, epsilon) for f in self.formulas])
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return any(f.truth(i, pos) for f in self.formulas)
 
@@ -268,7 +268,7 @@ def operator_symbol(self) -> OpSymbol:
         """Get the operator symbol."""
         return Symbols.IMPLIES.value
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return self.to_nnf().truth(i, pos)
 
@@ -299,7 +299,7 @@ def operator_symbol(self) -> OpSymbol:
         """Get the operator symbol."""
         return Symbols.EQUIVALENCE.value
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return self.to_nnf().truth(i, pos)
 
@@ -504,7 +504,7 @@ def negate(self) -> LTLfFormula:
         """Negate the formula."""
         return self.to_nnf().negate()
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return self.to_nnf().truth(i, pos)
 
@@ -535,7 +535,7 @@ def negate(self) -> LTLfFormula:
         """Negate the formula."""
         return self.to_nnf().negate()
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return self.to_nnf().truth(i, pos)
 
@@ -544,6 +544,37 @@ def _delta(self, i: PropositionalInterpretation, epsilon=False):
         return self.to_nnf()._delta(i, epsilon=epsilon)
 
 
+class LTLfLast(LTLfFormula):
+    """Class for the LTLf Last formula."""
+
+    def _delta(self, i: PropositionalInterpretation, epsilon=False):
+        """Apply the delta function."""
+        return self.to_nnf()._delta(i, epsilon=epsilon)
+
+    def to_nnf(self) -> LTLfFormula:
+        """Transform to NNF."""
+        return LTLfAnd([LTLfWeakNext(LTLfFalse()), LTLfNot(LTLfEnd())]).to_nnf()
+
+    def negate(self) -> LTLfFormula:
+        """Negate the formula."""
+        return self.to_nnf().negate()
+
+    def truth(self, i: FiniteTrace, pos: int = 0):
+        """Evaluate the formula."""
+        return self.to_nnf().truth(i, pos)
+
+    def find_labels(self) -> Set[AtomSymbol]:
+        """Find the labels."""
+        return set()
+
+    def _members(self):
+        return (Symbols.LAST.value,)
+
+    def __str__(self):
+        """Get the string representation."""
+        return Symbols.LAST.value
+
+
 class LTLfEnd(LTLfFormula):
     """Class for the LTLf End formula."""
 
@@ -553,9 +584,9 @@ def _delta(self, i: PropositionalInterpretation, epsilon=False):
 
     def find_labels(self) -> Set[AtomSymbol]:
         """Find the labels."""
-        return self.to_nnf().find_labels()
+        return set()
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         """Evaluate the formula."""
         return self.to_nnf().truth(i, pos)
 

flloat/parser/ltlf.py

@@ -22,6 +22,7 @@
     LTLfTrue,
     LTLfAtomic,
     LTLfFalse,
+    LTLfLast,
 )
 from flloat.parser import CUR_DIR
 from flloat.parser.pl import PLTransformer
@@ -159,7 +160,7 @@ def ltlf_false(self, args):
         return LTLfFalse()
 
     def ltlf_last(self, args):
-        raise NotImplementedError("LTLf last not supported, yet")
+        return LTLfLast()
 
     def ltlf_end(self, args):
         raise NotImplementedError("LTLf end not supported, yet")

flloat/pl.py

@@ -102,7 +102,7 @@ def to_sympy(
 class PLAtomic(AtomicFormula, PLFormula):
     """A class to represent propositional atomic formulas."""
 
-    def truth(self, i: PropInt, *args) -> bool:
+    def truth(self, i: PropInt, *args):
         """Evaluate the formula."""
         return i.get(self.s, False)
 
@@ -138,7 +138,7 @@ def __init__(self):
         """Initialize the PL true formula."""
         PLAtomic.__init__(self, Symbols.TRUE.value)
 
-    def truth(self, *args) -> bool:
+    def truth(self, *args):
         """Evaluate the formula."""
         return True
 
@@ -162,7 +162,7 @@ def __init__(self):
         """Initialize the formula."""
         PLAtomic.__init__(self, Symbols.FALSE.value)
 
-    def truth(self, *args) -> bool:
+    def truth(self, *args):
         """Evaluate the formula."""
         return False
 

flloat/symbols.py

@@ -39,7 +39,6 @@ class Symbols(Enum):
     CARET = "^"
     TRUE = "true"
     FALSE = "false"
-    LTLf_LAST = "last"
 
 
 ALL_SYMBOLS = {v.value for v in Symbols}  # type: Set[str]

tests/conftest.py

@@ -58,15 +58,15 @@
     "F a",
     "F(a & b)",
     "F(a | b)",
-    # "F(a & last)",
+    "F(a & last)",
     "G a",
     "F(G(a))",
     "G(F(a))",
     "G(true)",
     "F(true)",
     "G(false)",
     "F(false)",
-    # "last",
+    "last",
     # "end",
     "true",
     "false",

tests/test_ltlf.py

@@ -144,6 +144,30 @@ def test_always(self):
         assert parser("G c").truth(t, 10)
         assert parser("G F c").truth(t, 0)
 
+    def test_last(self):
+        parser = self.parser
+        t = self.trace
+
+        last = parser("last")
+        not_last = parser("! last")
+
+        assert last.negate() == not_last.to_nnf()
+
+        for pos in range(0, 5):
+            assert not parser("last").truth(t, pos)
+        assert parser("last").truth(t, 5)
+        assert not parser("last").truth(t, 6)
+
+        assert parser("XXXXX last").truth(t)
+        assert not parser("XXXX last").truth(t)
+        assert not parser("XXXXX !last").truth(t)
+        assert parser("XXXX !last").truth(t)
+
+        assert parser("c&last").truth(t, 5)
+
+        assert parser("last").truth(t[5:])
+        assert not parser("last").truth(t[6:])
+
 
 def test_nnf():
     parser = LTLfParser()