From 6a77e54d1c78e3a48179b873553cae207997dbb9 Mon Sep 17 00:00:00 2001 From: nickovic Date: Tue, 10 Jun 2025 23:28:11 +0200 Subject: [PATCH] Fixed the pastification of predicates bug --- rtamt/pastifier/stl/pastifier.py | 4 ++-- tests/python/api/test_stl_pastification.py | 24 ++++++++++++++++++++++ 2 files changed, 26 insertions(+), 2 deletions(-) diff --git a/rtamt/pastifier/stl/pastifier.py b/rtamt/pastifier/stl/pastifier.py index cceba2f2..ee6d062a 100644 --- a/rtamt/pastifier/stl/pastifier.py +++ b/rtamt/pastifier/stl/pastifier.py @@ -149,8 +149,8 @@ def visitPredicate(self, node, *args, **kwargs): node_horizon = self.subformula_horizons[node] remaining_horizon = args[0] horizon = remaining_horizon - node_horizon - child1_node = self.visit(node.children[0], *args, **kwargs) - child2_node = self.visit(node.children[1], *args, **kwargs) + child1_node = self.visit(node.children[0], node_horizon) + child2_node = self.visit(node.children[1], node_horizon) node = Predicate(child1_node, child2_node, node.operator) if horizon > 0: node = TimedOnce(node, Interval(horizon, horizon)) diff --git a/tests/python/api/test_stl_pastification.py b/tests/python/api/test_stl_pastification.py index 48bf7648..2b5eaa05 100755 --- a/tests/python/api/test_stl_pastification.py +++ b/tests/python/api/test_stl_pastification.py @@ -487,5 +487,29 @@ def test_complex_mixed_1(self): self.assertEqual('(once[0,1](req))->(once[4,5](gnt))', ast.specs[0].name, 'Complex pastification assertion') + def test_implication_1(self): + ast = StlAst() + ast.declare_var('req', 'float') + ast.declare_var('gnt', 'float') + ast.spec = 'req==1 -> (eventually[0,3] gnt==2)' + ast.parse() + + pastifier = StlPastifier() + ast = pastifier.pastify(ast) + + self.assertEqual('(once[3,3]((req)==(1.0)))->(once[0,3]((gnt)==(2.0)))', ast.specs[0].name, 'Complex pastification assertion') + + def test_implication_2(self): + ast = StlAst() + ast.declare_var('req', 'float') + ast.declare_var('gnt', 'float') + ast.spec = 'always[0,6](req==1 -> (eventually[0,3] gnt==2))' + ast.parse() + + pastifier = StlPastifier() + ast = pastifier.pastify(ast) + + self.assertEqual('historically[0,6]((once[3,3]((req)==(1.0)))->(once[0,3]((gnt)==(2.0))))', ast.specs[0].name, 'Complex pastification assertion') + if __name__ == '__main__': unittest.main() \ No newline at end of file