Merge pull request #44 from ainnoot/fix-mypy-typing

fix mypy typing

ltlf2asp/parser/grammar.lark

@@ -35,7 +35,7 @@ RELEASE.2: /R(?=[^a-zA-Z]|$)/
 ALWAYS.2: /G(?=[^a-zA-Z]|$)/
 EVENTUALLY.2: /F(?=[^a-zA-Z]|$)/
 NEXT.2: /X(?=[^a-zA-Z]|$)/
-WEAK_NEXT.2: /WX(?=[^a-zA-Z]|$)/
+WEAK_NEXT.2: /WX(?=[^a-zA-Z]|$)/ | /wX(?=[^a-zA-Z]|$)/
 WEAK_UNTIL.2: /W(?=[^a-zA-Z]|$)/
 STRONG_RELEASE.2: /M(?=[^a-zA-Z]|$)/
 NOT: "!" | "~"

ltlf2asp/parser/parser.py

@@ -27,6 +27,9 @@ def start(self, args: Sequence[T]) -> G:  # type: ignore
     def ltlf_formula(self, args: Sequence[T]) -> T:
         return args[0]
 
+    def ltlf_unaryop(self, args: Sequence[T]) -> T:
+        return args[0]
+
     def ltlf_equivalence(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
@@ -166,7 +169,6 @@ def symbol(self, args: Sequence[lark.Token]) -> str:
         return string.replace("'", '"')
 
     def ltlf_atom(self, args: Sequence[str]) -> T:
-        print("Got:", args, type(args[0]))
         if args[0].lower() == Constants.TRUE:
             return self.ltlf_true(args)
 

ltlf2asp/solve/decode_model.py

@@ -60,9 +60,17 @@ def __iter__(self) -> Generator[Tuple[str, bool], None, None]:
     @staticmethod
     def from_clingo_model(model: clingo.Model) -> Tuple["State", ...]:
         trace_dict: Dict[int, Dict[str, bool]] = defaultdict(dict)
+        last_instant = None
+        for x in model.context.symbolic_atoms.by_signature("last_state", 1):
+            if model.contains(x.symbol):
+                last_instant = x.symbol.arguments[0].number
+
         for x in model.context.symbolic_atoms.by_signature("trace", 2):
             symbol = x.symbol
             t = symbol.arguments[0].number
+            if t > last_instant:
+                continue
+
             a = symbol.arguments[1].string
             trace_dict[t][a] = model.contains(symbol)
 

ltlf2asp/solve/encodings/solve_incremental.lp

@@ -31,8 +31,8 @@ time(a..T) :- last_state(T), search(a, b).
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Atomic Formula %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 holds(t,X) :- atomic(X,A), trace(t,A).
 holds(t,X) :- last(X), last_state(t), time(t).
-holds(t,X) :- next(X,F), holds(t+1,F).
-holds(t,X) :- true(X).
+holds(t,X) :- next(X,F), holds(t+1,F), time(t+1).
+holds(t,X) :- true(X), time(t).
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Temporal Formula %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 holds(t,X) :- until(X,LHS,RHS), holds(t,RHS).