From 1924f58dae213e49a9484803177f0c1d5fa755ad Mon Sep 17 00:00:00 2001 From: ManCla Date: Tue, 13 Jan 2026 13:15:35 +0100 Subject: [PATCH 1/3] cleaner initialisation of buffers --- .../stl/discrete_time/offline/ast_visitor.py | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py b/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py index 6a5af93..f983801 100644 --- a/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py +++ b/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py @@ -409,14 +409,11 @@ 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]) From e72166bb23200d699dd1f880dc936093fffca1fe Mon Sep 17 00:00:00 2001 From: ManCla Date: Tue, 13 Jan 2026 13:15:52 +0100 Subject: [PATCH 2/3] indexing lists is more efficient --- rtamt/semantics/stl/discrete_time/offline/ast_visitor.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py b/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py index f983801..13f4e8f 100644 --- a/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py +++ b/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py @@ -417,6 +417,8 @@ def visitTimedUntil(self, node, *args, **kwargs): 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): From 02a1168081578f0e207cf4e5484eef35afc03865 Mon Sep 17 00:00:00 2001 From: ManCla Date: Tue, 13 Jan 2026 13:17:12 +0100 Subject: [PATCH 3/3] use suffix minimum of buffer_left instead of nested loops --- .../stl/discrete_time/offline/ast_visitor.py | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py b/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py index 13f4e8f..28aedd8 100644 --- a/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py +++ b/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py @@ -421,12 +421,15 @@ def visitTimedUntil(self, node, *args, **kwargs): 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