From f04f1b3eeb7bdf66bd4ed6c7c1a76611500c6bba Mon Sep 17 00:00:00 2001 From: Marcell Vazquez-Chanlatte Date: Mon, 24 Apr 2017 23:31:56 -0700 Subject: [PATCH] untimed until bug fixes --- stl/boolean_eval.py | 7 ++++--- stl/fastboolean_eval.py | 1 + stl/parser.py | 2 +- stl/test_boolean_eval.py | 7 +++++-- 4 files changed, 11 insertions(+), 6 deletions(-) diff --git a/stl/boolean_eval.py b/stl/boolean_eval.py index 84daa4a..dbc672e 100644 --- a/stl/boolean_eval.py +++ b/stl/boolean_eval.py @@ -38,10 +38,11 @@ def _(stl): def get_times(x, tau, lo=None, hi=None): + domain = fn.first(x.values()).domain if lo is None or lo is -oo: - lo = min(v.first()[0] for v in x.values()) + lo = domain.start() if hi is None or hi is oo: - hi = max(v.last()[0] for v in x.values()) + hi = domain.end() end = min(v.domain.end() for v in x.values()) hi = hi + tau if hi + tau <= end else end lo = lo + tau if lo + tau <= end else end @@ -72,9 +73,9 @@ def eval_unary_temporal_op(phi, always=True): if lo > hi: retval = True if always else False return lambda x, t: retval + f = eval_stl(phi.arg) if hi == lo: return lambda x, t: f(x, t) - f = eval_stl(phi.arg) return lambda x, t: fold(f(x, tau) for tau in get_times(x, t, lo, hi)) diff --git a/stl/fastboolean_eval.py b/stl/fastboolean_eval.py index 17d0b06..3189415 100644 --- a/stl/fastboolean_eval.py +++ b/stl/fastboolean_eval.py @@ -49,6 +49,7 @@ def _(stl): for phi, tau in zip(reversed(f1(x, times)), reversed(times)): if not phi: state = f2(x, [tau]) + if tau in t: yield state diff --git a/stl/parser.py b/stl/parser.py index 805b256..4483190 100644 --- a/stl/parser.py +++ b/stl/parser.py @@ -126,7 +126,7 @@ class STLVisitor(NodeVisitor): def visit_timed_until(self, _, children): phi, _, _, (lo, hi), _, psi = children - return env(psi, lo=lo, hi=hi) & alw(ast.Until(phi, psi), lo=0, hi=hi) + return env(psi, lo=lo, hi=hi) & alw(ast.Until(phi, psi), lo=0, hi=lo) def visit_id(self, name, _): return Symbol(name.text) diff --git a/stl/test_boolean_eval.py b/stl/test_boolean_eval.py index c22a65a..1bec255 100644 --- a/stl/test_boolean_eval.py +++ b/stl/test_boolean_eval.py @@ -19,14 +19,17 @@ ex8 = ("G[0, 0.2](C)", False) ex9 = ("(F[0, 0.2](C)) and (F[0, 1](2*A > 3))", True) ex10 = ("(A = 1) U (A = 4)", True) ex11 = ("(A < 5) U (A = 4)", False) +ex12 = ("(D > 10) U (D > 10)", False) +ex13 = ("(D = 2) U[1, 20] (D = 3)", True) x = { "A": traces.TimeSeries([(0, 1), (0.1, 1), (0.2, 4)]), "B": traces.TimeSeries([(0, 2), (0.1, 4), (0.2, 2)]), "C": traces.TimeSeries([(0, True), (0.1, True), (0.2, False)]), + 'D': traces.TimeSeries({0.0: 2, 13.8: 3, 19.7: 2}), } class TestSTLEval(unittest.TestCase): - @params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9, ex10, ex11) + @params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9, ex10, ex11, ex12, ex13) def test_eval(self, phi_str, r): phi = stl.parse(phi_str) stl_eval = stl.boolean_eval.pointwise_sat(phi) @@ -35,7 +38,7 @@ class TestSTLEval(unittest.TestCase): self.assertEqual(stl_eval2(x, 0), not r) - @params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9, ex10, ex11) + @params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9, ex10, ex11, ex12, ex13) def test_fasteval(self, phi_str, _): phi = stl.parse(phi_str) stl_eval = stl.boolean_eval.pointwise_sat(phi)