add more tests for the equivalence of formulas and automata.

Pipfile

@@ -17,6 +17,7 @@ pytest-cov = "*"
 mkdocs = "*"
 markdown-include = "*"
 tox-pipenv = "*"
+hypothesis = {extras = ["lark"],version = "*"}
 
 [packages]
 pythomata = {git = "https://github.com/logics4ai-sapienza/pythomata.git",ref = "develop"}

flloat/base/convertible.py

@@ -65,12 +65,13 @@ def Not(self):
     def convert(self):
         """Convert the formula."""
         fs = self.formulas
-        if len(fs) > 2:
-            a, b = self.And(fs[:-1]), fs[-1]
-        else:
-            a, b = fs
-        res = self.Or([self.Not(a), b])
-        return res
+
+        a, b = fs[0], fs[1]
+        result = self.Or([self.Not(a), b])
+        for idx in range(2, len(fs)):
+            result = self.Or([self.Not(result), fs[idx]])
+
+        return result
 
 
 class EquivalenceConvertible(

flloat/flloat.py

@@ -4,11 +4,11 @@
 import sympy
 from pythomata import PropInt, SymbolicAutomaton, SimpleDFA
 from pythomata.alphabets import MapAlphabet
-from sympy.logic.boolalg import BooleanFalse
+from sympy.logic.boolalg import BooleanFalse, BooleanTrue
 
 from flloat.base.formulas import Formula
 from flloat.base.symbols import Symbol
-from flloat.helpers import powerset
+from flloat.helpers import powerset, iter_powerset
 from flloat.pl import PLFormula, PLAtomic, PLNot, PLAnd, PLOr, PLImplies, PLEquivalence, PLTrue, PLFalse, to_sympy
 
 
@@ -157,16 +157,24 @@ def _make_transition(Q: FrozenSet[FrozenSet[Symbol]], i: PropInt):
 #         self.cur_state = _make_transition(self.cur_state, i)
 #
 
+def get_labels_from_macrostate(macrostate):
+    """Get labels from macrostate."""
+    labels = set()
+    for states in macrostate:
+        for state in states:
+            labels = labels.union(state.s.find_labels())
+    return labels
+
+
 def to_automaton(f):
     f = f.to_nnf()
     initial_state = frozenset({frozenset({PLAtomic(f)})})
     states = {initial_state}
     final_states = set()
     transition_function = {}
 
-    # the alphabet is the powerset of the set of fluents
-    labels = f.find_labels()
-    alphabet = powerset(labels)
+    all_labels = f.find_labels()
+    alphabet = powerset(all_labels)
 
     if f.delta({}, epsilon=True) == PLTrue():
         final_states.add(initial_state)
@@ -208,7 +216,7 @@ def to_automaton(f):
             source_idx = state2idx[source]
             dest_idx = state2idx[destination]
             pos_expr = sympy.And(*map(sympy.Symbol, symbol))
-            neg_expr = sympy.And(*map(lambda x: sympy.Not(sympy.Symbol(x)), labels.difference(symbol)))
+            neg_expr = sympy.And(*map(lambda x: sympy.Not(sympy.Symbol(x)), all_labels.difference(symbol)))
             automaton.add_transition(source_idx, sympy.And(pos_expr, neg_expr), dest_idx)
 
     dfa = automaton.determinize().minimize()

flloat/ldlf.py

@@ -208,10 +208,10 @@ class LDLfEquivalence(EquivalenceDeltaConvertible, LDLfCommBinaryOperator):
 class LDLfDiamond(LDLfTemporalFormulaNNF, FiniteTraceTruth):
     temporal_brackets = "<>"
 
-    def truth(self, i: FiniteTrace, pos: int = 0):
+    def truth(self, tr: FiniteTrace, pos: int = 0):
         # last + 1 in order to include the last step
         return any(
-            self.r.truth(i, pos, j) and self.f.truth(i, j) for j in range(pos, len(i))
+            self.r.truth(tr, pos, j) and self.f.truth(tr, j) for j in range(pos, len(tr) + 1)
         )
 
     def _delta(self, i: PropInt, epsilon=False):
@@ -224,8 +224,8 @@ class LDLfBox(ConvertibleFormula, LDLfTemporalFormulaNNF):
     def convert(self):
         return LDLfNot(LDLfDiamond(self.r, LDLfNot(self.f)))
 
-    def truth(self, i: FiniteTrace, pos: int = 0):
-        return self.convert().truth(i, pos)
+    def truth(self, tr: FiniteTrace, pos: int = 0):
+        return self.convert().truth(tr, pos)
 
     def _delta(self, i: PropInt, epsilon=False):
         return self.r.delta_box(self.f, i, epsilon)
@@ -240,7 +240,7 @@ def __init__(self, pl_formula: PLFormula):
     def truth(self, tr: FiniteTrace, start: int = 0, end: int = 0):
         return (
             end == start + 1
-            and end <= len(tr) - 1
+            and start < len(tr)
             and self.pl_formula.truth(tr[start])
         )
 
@@ -477,7 +477,7 @@ def negate(self):
     def find_labels(self):
         return super().find_labels()
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, tr: FiniteTrace, pos: int):
         raise NotImplementedError
 
 
@@ -508,7 +508,7 @@ def negate(self):
     def find_labels(self):
         return super().find_labels()
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, tr: FiniteTrace, pos: int):
         raise NotImplementedError
 
 

flloat/ltlf.py

@@ -121,7 +121,10 @@ def _delta(self, i: PropInt, epsilon: bool = False):
         return PLTrue() if PLAtomic(self.s).truth(i) else PLFalse()
 
     def truth(self, i: FiniteTrace, pos: int = 0):
-        return PLAtomic(self.s).truth(i[pos])
+        if len(i) > 0:
+            return PLAtomic(self.s).truth(i[pos])
+        else:
+            return False
 
     def find_labels(self) -> Set[Symbol]:
         return PLAtomic(self.s).find_labels()
@@ -144,7 +147,7 @@ def _delta(self, i: PropInt, epsilon: bool = False):
             return PLTrue()
 
     def truth(self, i: FiniteTrace, pos: int = 0):
-        return True
+        return len(i) > 0
 
     def find_labels(self) -> Set[Symbol]:
         """Return the set of symbols."""
@@ -183,6 +186,12 @@ def _delta(self, i: PropInt, epsilon=False):
     def to_LDLf(self):
         return LDLfNot(self.f.to_LDLf())
 
+    def truth(self, i: FiniteTrace, pos: int = 0):
+        if len(i) > 0:
+            return NotTruth.truth(self, i, pos)
+        else:
+            return False
+
 
 class LTLfAnd(LTLfCommBinaryOperator, AndTruth, DualBinaryOperatorNNF):
     def _delta(self, i: PropInt, epsilon=False):
@@ -208,6 +217,12 @@ class LTLfImplies(ImpliesDeltaConvertible, LTLfFormula):
     def to_LDLf(self):
         return self.convert().to_LDLf()
 
+    def truth(self, i: FiniteTrace, pos: int):
+        if len(i) > 0:
+            return ImpliesDeltaConvertible.truth(self, i, pos)
+        else:
+            return False
+
 
 class LTLfEquivalence(EquivalenceDeltaConvertible, LTLfCommBinaryOperator):
     And = LTLfAnd
@@ -217,13 +232,22 @@ class LTLfEquivalence(EquivalenceDeltaConvertible, LTLfCommBinaryOperator):
     def to_LDLf(self):
         return self.convert().to_LDLf()
 
+    def truth(self, i: FiniteTrace, pos: int):
+        if len(i) > 0:
+            return EquivalenceDeltaConvertible.truth(self, i, pos)
+        else:
+            return False
+
 
 class LTLfNext(DualUnaryOperatorNNF, LTLfTemporalFormula):
     operator_symbol = "X"
     Not = LTLfNot
 
     def truth(self, i: FiniteTrace, pos: int = 0):
-        return pos < len(i) - 1 and self.f.truth(i, pos + 1)
+        if len(i) > 0:
+            return pos < len(i) - 1 and self.f.truth(i, pos + 1)
+        else:
+            return False
 
     def _delta(self, i: PropInt, epsilon=False):
         if epsilon:
@@ -246,7 +270,10 @@ def convert(self):
         return LTLfNot(LTLfNext(LTLfNot(self.f)))
 
     def truth(self, i: FiniteTrace, pos: int = 0):
-        return self.convert().truth(i, pos)
+        if len(i) > 0:
+            return self.convert().truth(i, pos)
+        else:
+            return True
 
     def _delta(self, i: PropInt, epsilon=False):
         if epsilon:
@@ -329,6 +356,12 @@ def convert(self):
     def to_LDLf(self):
         return self.convert().to_LDLf()
 
+    def truth(self, i: PropInt, pos: int) -> bool:
+        if len(i) == 0:
+            return True
+        else:
+            return BaseConvertibleFormula.truth(self, i, pos)
+
 
 class LTLfRelease(DualBinaryOperatorNNF, BaseConvertibleFormula, LTLfTemporalFormula):
     operator_symbol = "R"
@@ -353,6 +386,13 @@ def _delta(self, i: PropInt, epsilon=False):
             ]
         )
 
+    def truth(self, i: FiniteTrace, pos: int = 0):
+        if len(i) == 0:
+            return True
+        else:
+            return BaseConvertibleFormula.truth(self, i, pos)
+
+
     def to_LDLf(self):
         return self.convert().to_LDLf()
 

tests/conftest.py

@@ -0,0 +1,74 @@
+# -*- coding: utf-8 -*-
+
+ldlf_formulas = [
+    "tt",
+    "ff",
+    "!tt",
+    "!ff",
+    "tt & tt",
+    "tt & ff",
+    "ff & ff",
+    "tt | ff",
+    "tt | ff",
+    "<true>tt",
+    "<true>ff",
+    "[true]tt",
+    "[true]ff",
+    "<A>tt",
+    "<A>ff",
+    "[A]tt",
+    "[A]ff",
+    "<A & B>tt",
+    "<A & B>ff",
+    "<A | C>tt",
+    "<A | C>ff",
+    "<A + B>tt",
+    "<A + B>ff",
+    "<A ; B>tt",
+    "<A ; B>ff",
+    "<A*>tt",
+    "<A*>ff",
+    "<<A>tt?>tt",
+    "<<A>tt?>ff",
+    "[A & B]tt",
+    "[A & B]ff",
+    "[A | C]tt",
+    "[A | C]ff",
+    "[A + B]tt",
+    "[A + B]ff",
+    "[A ; B]tt",
+    "[A ; B]ff",
+    "[A*]tt",
+    "[A*]ff",
+    "[<A>tt?]tt",
+    "[<A>tt?]ff",
+]
+
+
+ltlf_formulas = [
+    "A",
+    "!A",
+    "A | B",
+    "A & B",
+    "X A",
+    "WX A",
+    "A U B",
+    "A R B",
+    "F A",
+    "G A",
+    "F(G(A))",
+    "G(F(A))",
+    "G(true)",
+    "F(true)",
+    "G(false)",
+    "F(false)",
+    "last",
+    "end",
+    "true",
+    "false",
+    "A -> B",
+    "A <-> B",
+    "G(A -> B)",
+    "G(A -> F(B))",
+    "G(A -> B -> C)",
+]

tests/strategies.py

@@ -0,0 +1,13 @@
+# -*- coding: utf-8 -*-
+"""Hypothesis strategies."""
+from typing import Sequence
+
+from hypothesis.strategies import lists, dictionaries, booleans, sampled_from
+
+
+def propositional_words(propositions: Sequence[str], min_size=0, max_size=None):
+    return lists(
+        dictionaries(sampled_from(propositions), booleans()),
+        min_size=min_size,
+        max_size=max_size,
+    )

tests/test_ldlf.py

@@ -1,9 +1,17 @@
 # -*- coding: utf-8 -*-
+import pytest
+from hypothesis import given
+
 from flloat.ldlf import LDLfLogicalTrue, LDLfLogicalFalse, LDLfNot, LDLfAnd, LDLfPropositional, \
     RegExpPropositional, LDLfDiamond, LDLfEquivalence, LDLfBox, RegExpStar, LDLfOr, RegExpUnion, RegExpSequence, \
     LDLfEnd, RegExpTest, LDLfLast
 from flloat.parser.ldlf import LDLfParser
 from flloat.pl import PLTrue, PLFalse, PLAnd, PLNot, PLAtomic, PLEquivalence
+from .conftest import ldlf_formulas
+from .strategies import propositional_words
+
+
+parser = LDLfParser()
 
 
 def test_parser():
@@ -258,3 +266,17 @@ def test_box_safety(self):
         assert dfa.accepts([i_ab, i_ab])
         assert dfa.accepts([i_a, i_b])
         assert not dfa.accepts([i_a, i_a])
+
+
+@pytest.fixture(scope="session", params=ldlf_formulas)
+def formula_automa_pair(request):
+    formula_obj = parser(request.param)
+    automaton = formula_obj.to_automaton()
+    return formula_obj, automaton
+
+
+@given(propositional_words(["A", "B", "C"], min_size=0, max_size=5))
+def test_hypothesis(formula_automa_pair, word):
+    formula_obj, automaton = formula_automa_pair
+    print(formula_obj, word)
+    assert formula_obj.truth(word, 0) == automaton.accepts(word)

tests/test_ltlf.py

@@ -1,8 +1,15 @@
 # -*- coding: utf-8 -*-
+import pytest
+from hypothesis import given
+
 from flloat.ltlf import LTLfAtomic, LTLfAnd, LTLfEquivalence, LTLfOr, LTLfNot, LTLfImplies, LTLfEventually, \
     LTLfAlways, LTLfUntil, LTLfRelease, LTLfNext, LTLfWeakNext, LTLfTrue, LTLfFalse
 from flloat.parser.ltlf import LTLfParser
 from flloat.pl import PLAtomic, PLTrue, PLFalse, PLAnd, PLOr
+from tests.conftest import ltlf_formulas
+from tests.strategies import propositional_words
+
+parser = LTLfParser()
 
 
 def test_parser():
@@ -615,3 +622,16 @@ def test_conditional_response(self):
         assert dfa.accepts([i_ab, i_ab])
         assert dfa.accepts([i_a, i_b])
         assert not dfa.accepts([i_a, i_a])
+
+
+@pytest.fixture(scope="session", params=ltlf_formulas)
+def formula_automa_pair(request):
+    formula_obj = parser(request.param)
+    automaton = formula_obj.to_automaton()
+    return formula_obj, automaton
+
+
+@given(propositional_words(["A", "B", "C"], min_size=0, max_size=5))
+def test_hypothesis(formula_automa_pair, word):
+    formula_obj, automaton = formula_automa_pair
+    assert formula_obj.truth(word, 0) == automaton.accepts(word)