From 5b3b8bef6df1e35f2d9ac89302441ed3148029db Mon Sep 17 00:00:00 2001
From: ainnoot <ai6chr+github@gmail.com>
Date: Tue, 4 Jun 2024 20:03:32 +0200
Subject: [PATCH 1/2] fix: no stray print

---
 ltlf2asp/parser/parser.py | 1 -
 1 file changed, 1 deletion(-)

diff --git a/ltlf2asp/parser/parser.py b/ltlf2asp/parser/parser.py
index b8725a7..25d0466 100644
--- a/ltlf2asp/parser/parser.py
+++ b/ltlf2asp/parser/parser.py
@@ -166,7 +166,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)
 

From 956da51b36a3f2b137ed99e1572df7877eb9c474 Mon Sep 17 00:00:00 2001
From: ainnoot <ai6chr+github@gmail.com>
Date: Mon, 17 Jun 2024 09:57:39 +0200
Subject: [PATCH 2/2] fix: bug fixing formulae X^k True

---
 ltlf2asp/parser/grammar.lark                  | 2 +-
 ltlf2asp/parser/parser.py                     | 3 +++
 ltlf2asp/solve/decode_model.py                | 8 ++++++++
 ltlf2asp/solve/encodings/solve_incremental.lp | 4 ++--
 4 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/ltlf2asp/parser/grammar.lark b/ltlf2asp/parser/grammar.lark
index 5758b5e..e2f74fc 100644
--- a/ltlf2asp/parser/grammar.lark
+++ b/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: "!" | "~"
diff --git a/ltlf2asp/parser/parser.py b/ltlf2asp/parser/parser.py
index 25d0466..7a49220 100644
--- a/ltlf2asp/parser/parser.py
+++ b/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]
diff --git a/ltlf2asp/solve/decode_model.py b/ltlf2asp/solve/decode_model.py
index 3958658..abb8f60 100644
--- a/ltlf2asp/solve/decode_model.py
+++ b/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)
 
diff --git a/ltlf2asp/solve/encodings/solve_incremental.lp b/ltlf2asp/solve/encodings/solve_incremental.lp
index ef123bc..8cd82dd 100644
--- a/ltlf2asp/solve/encodings/solve_incremental.lp
+++ b/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).