diff --git a/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py b/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py index 6a5af93..28aedd8 100644 --- a/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py +++ b/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py @@ -409,25 +409,27 @@ def visitTimedUntil(self, node, *args, **kwargs): begin, end = self.time_unit_transformer(node) sample_return = [] - buffer_left = collections.deque(maxlen=(end + 1)) - buffer_right = collections.deque(maxlen=(end + 1)) + L = end+1 + + buffer_left = collections.deque([ float("inf")] * L, maxlen=L) + buffer_right = collections.deque([-float("inf")] * L, maxlen=L) - for i in range(end + 1): - s_left = float("inf") - s_right = - float("inf") - buffer_left.append(s_left) - buffer_right.append(s_right) for i in range(len(sample_left)-1, -1, -1): buffer_left.append(sample_left[i]) buffer_right.append(sample_right[i]) + left = list(buffer_left) + right = list(buffer_right) out_sample = - float("inf") - for j in range(end-begin+1): - c_left = float("inf") - c_right = buffer_right[j] - for k in range(j+1, end+1): - c_left = min(c_left, buffer_left[k]) - out_sample = max(out_sample, min(c_left, c_right)) + # build the suffix minimum of the sample_left buffer + suf_min_left = [float("inf")]*(L+1) + for k in range(L-1,-1,-1): + lt = left[k] + st = suf_min_left[k+1] + suf_min_left[k] = lt if lt