diff --git a/dtl/dtlmon.py b/dtl/dtlmon.py index 0f3526b..e3ce25a 100644 --- 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 index 37212ec..c92095d 100644 --- 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