Avoid rewrite when mon last is T / F

hkff · Jan 26, 2016 · ac43676 · ac43676
1 parent 572a416
commit ac43676
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 20 deletions.
diff --git a/dtl/dtlmon.py b/dtl/dtlmon.py
@@ -33,17 +33,6 @@ def __init__(self, formula, trace, actor=None, parent=None, fid=""):
         self.fid = fid
         self.rewrite = copy.deepcopy(self.formula)
 
-    # def monitor(self, once=False):
-    #     for e in self.get_trace().events[self.counter:]:
-    #         self.counter += 1
-    #         self.rewrite = self.prg(self.rewrite, e)
-    #         Debug(self.rewrite)
-    #         self.last = B3(self.rewrite.eval()) if isinstance(self.rewrite, Formula) else self.rewrite
-    #         if self.last == Boolean3.Top or self.last == Boolean3.Bottom or once: break
-    #     ret = "Result Progression: %s after %s events." % (self.last, self.counter)
-    #     # print(ret)
-    #     return ret
-
     def prg(self, formula, event, valuation=None):
         if isinstance(formula, At):
             # Check in KV

diff --git a/ltl/ltlmon.py b/ltl/ltlmon.py
@@ -22,7 +22,7 @@
 import os
 import copy
 import time
-DEBUG = False
+DEBUG = True
 
 
 def Debug(*args):
@@ -41,6 +41,7 @@ def __init__(self, formula, trace):
         self.trace = trace
         self.counter = 0
         self.last = Boolean3.Unknown
+        self.counter2 = 0
         self.rewrite = copy.deepcopy(self.formula)
 
     def monitor(self, *args, **kargs):
@@ -52,23 +53,34 @@ def prg(self, *args, **kargs):
     def push_event(self, event):
         self.trace.push_event(event)
 
+    def reset(self):
+        self.rewrite = copy.deepcopy(self.formula)
+
 
 class Ltlmon(Mon):
     """
-    LTL monitor using progression technique
+    LTL monitor using progression technique.
     """
 
-    def monitor(self, once=False, debug=False):
+    def monitor(self, once=False, debug=False, struct_res=False):
         if debug:
             start_time = time.time()
 
         for e in self.trace.events[self.counter:]:
-            self.counter += 1
-            self.rewrite = self.prg(self.rewrite, e)
-            Debug(self.rewrite)
-            self.last = B3(self.rewrite.eval()) if isinstance(self.rewrite, Formula) else self.rewrite
-            if self.last == Boolean3.Top or self.last == Boolean3.Bottom or once: break
-        ret = "Result Progression: %s after %s events." % (self.last, self.counter)
+            if self.last == Boolean3.Top or self.last == Boolean3.Bottom:
+                break
+            else:
+                self.counter += 1
+                self.counter2 += 1
+                self.rewrite = self.prg(self.rewrite, e)
+                Debug(self.rewrite)
+                self.last = B3(self.rewrite.eval()) if isinstance(self.rewrite, Formula) else self.rewrite
+                if once:break
+
+        if struct_res:
+            ret = {"result": self.last, "at": self.counter2, "step": self.counter}
+        else:
+            ret = "Result Progression: %s after %s events." % (self.last, self.counter)
         # print(ret)
         if debug:
             exec_time = time.time() - start_time