Merge branch 'release-0.1.4' for postfix 1.

Author: marcofavorito

flloat/__init__.py

@@ -4,4 +4,4 @@
 
 __author__ = """Marco Favorito"""
 __email__ = '[email protected]'
-__version__ = '0.1.4'
+__version__ = '0.1.4.post1'

flloat/base/Alphabet.py

@@ -15,7 +15,7 @@ def _members(self):
 
     def powerset(self):
         if self._powerset is None:
-            self._powerset = powerset(self.symbols)
+            self._powerset = _Alphabet(powerset(self.symbols))
         return self._powerset
 
 
@@ -25,7 +25,7 @@ def __call__(self, symbols: Set[Symbol]) -> _Alphabet:
         return super().__call__(f_symbols)
 
     @classmethod
-    def fromStrings(symbol_strings: Set[str]):
+    def fromStrings(cls, symbol_strings: Set[str]):
         f_symbols = frozenset(Symbol(s) for s in symbol_strings)
         return alphabet_factory.new(f_symbols)
 

flloat/base/Formula.py

@@ -83,7 +83,7 @@ def _popup(self):
         res = ()
         for child in self.formulas:
             if type(child) == type(self):
-                superchilds = child._popup()
+                superchilds = child.formulas
                 res += superchilds
             else:
                 res += (child, )
@@ -105,7 +105,7 @@ def __init__(self, formulas:OperatorChilds, idempotence=True):
             # remove duplicates -> set operation
             self.formulas_set = frozenset(self.formulas)
             # unique representation -> sorting
-            self.members = tuple(sorted(self.formulas_set, key=lambda x: str(x)))
+            self.members = tuple(sorted(self.formulas_set, key=lambda x: hash(x)))
 
     def simplify(self):
         if self.idempotence:

flloat/base/nnf.py

@@ -7,9 +7,6 @@
 
 class NNF(ABC):
 
-    def __init__(self):
-        self._cache_id = None
-
     @lru_cache(maxsize=MAX_CACHE_SIZE)
     def to_nnf(self):
         return self._to_nnf()
@@ -50,7 +47,7 @@ def Not(self):
 
     @Not.setter
     def Not(self, x):
-        self.Not= x
+        self.Not = x
 
     def _to_nnf(self):
         return type(self)(self.f.to_nnf())

flloat/flloat.py

@@ -180,7 +180,8 @@ def word_acceptance(self, action_set_list:List[PLInterpretation]):
     def is_true(self):
         return self._is_true(self.cur_state)
 
-    def _is_true(self, Q):
+    @staticmethod
+    def _is_true(Q):
         if frozenset() in Q:
             return True
         conj = [PLAnd([subf.delta(None, epsilon=True) for subf in q]) if len(q) >= 2 else
@@ -198,8 +199,8 @@ def get_current_state(self):
     def make_transition(self, i:PLInterpretation):
         self.cur_state = self._make_transition(self.cur_state, i)
 
-
-    def _make_transition(self, Q, i: PLInterpretation):
+    @staticmethod
+    def _make_transition(Q, i: PLInterpretation):
         actions_set = i.true_propositions
         new_macrostate = set()
 
@@ -247,18 +248,16 @@ def _make_transition(self, Q, i: PLInterpretation):
 
 
 def to_automaton(f, labels:Set[Symbol]=None, minimize=True):
-    dfaotf = DFAOTF(f)
-
 
-    initial_state = frozenset({frozenset({dfaotf.f})})
+    initial_state = frozenset({frozenset({f.to_nnf()})})
     states = {initial_state}
     final_states = set()
     transition_function = {}
 
     # the alphabet is the powerset of the set of fluents
     alphabet = powerset(labels)
 
-    if dfaotf.is_true():
+    if DFAOTF._is_true(initial_state):
         final_states.add(initial_state)
 
     visited = set()
@@ -269,7 +268,7 @@ def to_automaton(f, labels:Set[Symbol]=None, minimize=True):
         for q in list(to_be_visited):
             to_be_visited.remove(q)
             for actions_set in alphabet:
-                new_state = dfaotf._make_transition(q, PLInterpretation(actions_set))
+                new_state = DFAOTF._make_transition(q, PLInterpretation(actions_set))
                 if not new_state in states:
                     states.add(new_state)
                     to_be_visited.add(new_state)
@@ -278,7 +277,7 @@ def to_automaton(f, labels:Set[Symbol]=None, minimize=True):
 
                 if new_state not in visited:
                     visited.add(new_state)
-                    if dfaotf._is_true(new_state): final_states.add(new_state)
+                    if DFAOTF._is_true(new_state): final_states.add(new_state)
 
 
     new_alphabet = PythomataAlphabet({PLInterpretation(set(sym)) for sym in alphabet})

flloat/parser/pl.py

@@ -44,7 +44,6 @@ def t_ATOM(self, t):
         return t
 
 
-# Yacc example
 class PLParser(Parser):
 
     def __init__(self):

flloat/semantics/pl.py

@@ -1,4 +1,4 @@
-from typing import FrozenSet, Set
+from typing import FrozenSet, Set, List
 
 from flloat.base.Interpretation import Interpretation
 from flloat.base.Symbol import Symbol
@@ -49,6 +49,9 @@ def __call__(self, true_propositions:Set[Symbol]):
         f_sym = frozenset(true_propositions)
         return super().__call__(f_sym)
 
+    def fromStrings(self, strings:List[str]):
+        return self(set(Symbol(s) for s in strings))
+
 
 
 plinterpretation_factory = ObjFactory(_PLInterpretation)

flloat/syntax/ldlf.py

@@ -20,7 +20,7 @@
 
 class RegExpTruth(Truth):
     @abstractmethod
-    def truth(self, tr: FiniteTrace, start: int, end: int):
+    def truth(self, tr: FiniteTrace, start: int=0, end: int=0):
         raise NotImplementedError
 
 class LDLfFormula(Formula, FiniteTraceTruth, NNF, Delta):
@@ -190,7 +190,7 @@ class LDLfEquivalence(EquivalenceDeltaConvertible, LDLfCommBinaryOperator):
 class LDLfDiamond(LDLfTemporalFormulaNNF, FiniteTraceTruth):
     temporal_brackets = "<>"
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int=0):
         return any(self.r.truth(i, pos, j) and self.f.truth(i, j) for j in range(pos, i.last()+1))
         # last + 1 in order to include the last step
 
@@ -204,7 +204,7 @@ class LDLfBox(ConvertibleFormula, LDLfTemporalFormulaNNF):
     def _convert(self):
         return LDLfNot(LDLfDiamond(self.r, LDLfNot(self.f)))
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int=0):
         return self._convert().truth(i, pos)
 
     def _delta(self, i:PLInterpretation, epsilon=False):
@@ -217,7 +217,7 @@ def __init__(self, pl_formula:PLFormula):
         RegExpFormula.__init__(self)
         self.pl_formula = pl_formula
 
-    def truth(self, tr: FiniteTrace, start: int, end: int):
+    def truth(self, tr: FiniteTrace, start: int=0, end: int=0):
         return end == start + 1 \
                 and end <= tr.last() \
                 and self.pl_formula.truth(tr.get(start))
@@ -265,7 +265,7 @@ class RegExpTest(UnaryOperator, RegExpFormula):
     #     RegExpFormula.__init__(self)
     #     UnaryOperator.__init__(self, f)
 
-    def truth(self, tr: FiniteTrace, start: int, end: int):
+    def truth(self, tr: FiniteTrace, start: int=0, end: int=0):
         return start == end and self.f.truth(tr, start)
 
     def __str__(self):
@@ -294,7 +294,7 @@ def __init__(self, formulas):
         RegExpFormula.__init__(self)
         CommutativeBinaryOperator.__init__(self, formulas)
 
-    def truth(self, tr: FiniteTrace, start: int, end: int):
+    def truth(self, tr: FiniteTrace, start: int=0, end: int=0):
         return any(f.truth(tr, start, end) for f in self.formulas_set)
 
     def _to_nnf(self):
@@ -313,7 +313,7 @@ def __init__(self, formulas: OperatorChilds):
         RegExpFormula.__init__(self)
         BinaryOperator.__init__(self, formulas)
 
-    def truth(self, tr: FiniteTrace, start: int, end: int):
+    def truth(self, tr: FiniteTrace, start: int=0, end: int=0):
         f1 = self.formulas[0]
         if len(self.formulas) == 2:
             f2 = self.formulas[1]
@@ -346,7 +346,7 @@ class RegExpStar(UnaryOperator, RegExpFormula):
     #     UnaryOperator.__init__(self, f)
     #     RegExpFormula.__init__(self)
 
-    def truth(self, tr: FiniteTrace, start: int, end: int):
+    def truth(self, tr: FiniteTrace, start: int=0, end: int=0):
         return start == end \
             or any(self.f.truth(tr, start, k) and self.truth(tr, k, end)
                    for k in range(start, end + 1))

flloat/syntax/ltlf.py

@@ -2,7 +2,7 @@
 from functools import lru_cache
 from typing import Set
 
-from flloat.base.Formula import Formula, CommutativeBinaryOperator, AtomicFormula, BinaryOperator
+from flloat.base.Formula import Formula, CommutativeBinaryOperator, AtomicFormula, BinaryOperator, UnaryOperator
 from flloat.base.Symbol import Symbol
 from flloat.base.Symbols import Symbols
 from flloat.base.convertible import ImpliesDeltaConvertible, EquivalenceDeltaConvertible, ConvertibleFormula, \
@@ -20,7 +20,7 @@
 
 class LTLfTruth(Truth):
     @abstractmethod
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int = 0):
         raise NotImplementedError
 
 
@@ -35,7 +35,7 @@ def delta(self, i: PLInterpretation, epsilon=False):
             # By definition, if epsilon=True, then the result must be either PLTrue or PLFalse
             # Now, the output is a Propositional Formula with only PLTrue or PLFalse as atomics
             # Hence, we just evaluate the formula with a dummy PLInterpretation
-            d = PLTrue() if d.truth(PLFalseInterpretation()) else PLFalse()
+            d = PLTrue() if d.truth(None) else PLFalse()
         return d
 
     @abstractmethod
@@ -91,7 +91,7 @@ def _delta(self, i:PLInterpretation, epsilon=False):
             return PLFalse()
         return PLTrue() if self.a.truth(i) else PLFalse()
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int=0):
         return self.a.truth(i.get(pos))
 
     def find_labels(self):
@@ -171,7 +171,7 @@ class LTLfNext(DualUnaryOperatorNNF, LTLfTemporalFormula):
     operator_symbol = "X"
     Not = LTLfNot
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int=0):
         return pos < i.last() and self.f.truth(i, pos + 1)
 
     def _delta(self, i: PLInterpretation, epsilon=False):
@@ -191,7 +191,7 @@ class LTLfWeakNext(DualUnaryOperatorNNF, ConvertibleFormula, LTLfTemporalFormula
     def _convert(self):
         return LTLfNot(LTLfNext(LTLfNot(self.f)))
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int=0):
         return self._convert().truth(i, pos)
 
     def _delta(self, i: PLInterpretation, epsilon=False):
@@ -218,7 +218,7 @@ def _to_nnf(self):
     def negate(self):
         return LTLfRelease([LTLfNot(f) for f in self.formulas])
 
-    def truth(self, i: FiniteTrace, pos: int):
+    def truth(self, i: FiniteTrace, pos: int=0):
         f1 = self.formulas[0]
         f2 = LTLfUntil(self.formulas[1:]) if len(self.formulas)>2 else self.formulas[1]
 
@@ -246,36 +246,37 @@ def to_LDLf(self):
         return LDLfDiamond(RegExpStar(RegExpSequence([RegExpTest(f1), RegExpPropositional(PLTrue())])), LDLfAnd([f2, LDLfNot(LDLfEnd())]))
 
 
-class LTLfEventually(DualUnaryOperatorNNF, BaseConvertibleFormula, LTLfTemporalFormula):
+class LTLfEventually(UnaryOperator, DeltaConvertibleFormula, LTLfTemporalFormula):
     operator_symbol = "F"
     Not = LTLfNot
 
     def _convert(self):
         return LTLfUntil([LTLfTrue(), self.f])
 
-    def _delta(self, i:PLInterpretation, epsilon=False):
-        if epsilon:
-            return PLFalse()
-        else:
-            return PLOr([self.f._delta(i, epsilon), LTLfNext(self)._delta(i, epsilon)])
+    # def _delta(self, i:PLInterpretation, epsilon=False):
+        # if epsilon:
+        #     return PLFalse()
+        # else:
+        #     return PLOr([self.f._delta(i, epsilon), LTLfNext(self)._delta(i, epsilon)])
+
 
     def to_LDLf(self):
         # return self._convert().to_LDLf()
         return LDLfDiamond(RegExpStar(RegExpPropositional(PLTrue())), LDLfAnd([self.f.to_LDLf(), LDLfNot(LDLfEnd())]))
 
 
-class LTLfAlways(DualUnaryOperatorNNF,  BaseConvertibleFormula, LTLfTemporalFormula):
+class LTLfAlways(UnaryOperator, DeltaConvertibleFormula, LTLfTemporalFormula):
     operator_symbol = "G"
     Not = LTLfNot
 
     def _convert(self):
-        return LTLfNot(LTLfEventually(LTLfNot(self.f)))
+        return LTLfNot(LTLfEventually(LTLfNot(self.f))._convert())
 
-    def _delta(self, i:PLInterpretation, epsilon=False):
-        if epsilon:
-            return PLTrue()
-        else:
-            return PLAnd([self.f._delta(i, epsilon), LTLfWeakNext(self)._delta(i, epsilon)])
+    # def _delta(self, i:PLInterpretation, epsilon=False):
+    #     if epsilon:
+    #         return PLTrue()
+    #     else:
+    #         return PLAnd([self.f._delta(i, epsilon), LTLfWeakNext(self)._delta(i, epsilon)])
 
     def to_LDLf(self):
         return self._convert().to_LDLf()
@@ -313,10 +314,10 @@ def _members(self):
         return (self.s, )
 
     def _convert(self):
-        return LTLfAlways(LTLfFalse())
+        return LTLfAlways(LTLfFalse()).to_nnf()
 
     def negate(self):
-        return LTLfEventually(LTLfTrue())
+        return LTLfEventually(LTLfTrue()).to_nnf()
 
     def __str__(self):
         return "_".join(map(str, self._members()))

flloat/syntax/pl.py

@@ -3,7 +3,7 @@
 from typing import Set
 
 
-from flloat.base.Alphabet import _Alphabet
+from flloat.base.Alphabet import _Alphabet, Alphabet
 from flloat.base.Formula import Formula, CommutativeBinaryOperator, BinaryOperator, AtomicFormula
 from flloat.base.Symbol import Symbol
 from flloat.base.Symbols import Symbols
@@ -19,7 +19,7 @@ class PLTruth(Truth):
     def truth(self, i: PLInterpretation, *args):
         raise NotImplementedError
 
-class PLFormula(Formula, Truth, NNF):
+class PLFormula(Formula, PLTruth, NNF):
     def __init__(self):
         Formula.__init__(self)
 
@@ -30,7 +30,7 @@ def __init__(self):
     def all_models(self, alphabet: _Alphabet) -> Set[PLInterpretation]:
         """Find all the possible interpretations given a set of symbols"""
 
-        all_possible_interpretations = alphabet.powerset()
+        all_possible_interpretations = alphabet.powerset().symbols
         all_models = set()
         for i in all_possible_interpretations:
             # compute current Interpretation, considering False
@@ -84,7 +84,6 @@ def _find_atomics(self):
                 res.add(subf)
         return res
 
-
 class PLCommBinaryOperator(DualCommutativeOperatorNNF, PLFormula):
     # def __init__(self, formulas):
     #     PLFormula.__init__(self)
@@ -157,10 +156,10 @@ def _find_atomics(self):
         return self.f.find_atomics()
 
 
-
 class PLOr(PLCommBinaryOperator, OrTruth):
     pass
 
+
 class PLAnd(PLCommBinaryOperator, AndTruth):
     pass
 
@@ -170,6 +169,7 @@ class PLImplies(PLBinaryOperator, ImpliesConvertible):
     Or = PLOr
     Not = PLNot
 
+
 class PLEquivalence(PLCommBinaryOperator, EquivalenceConvertible):
     And = PLAnd
     Or = PLOr