From 2cff512933cc72c7daac4fb09f8a4cc87e8c2562 Mon Sep 17 00:00:00 2001 From: Gaudeval Date: Wed, 6 Jan 2021 10:56:05 +0000 Subject: [PATCH 1/3] Fix until output not valued at signal start --- mtl/evaluator.py | 6 ++++++ mtl/test_eval.py | 10 ++++++++++ 2 files changed, 16 insertions(+) diff --git a/mtl/evaluator.py b/mtl/evaluator.py index 9650df5..69e0e41 100644 --- a/mtl/evaluator.py +++ b/mtl/evaluator.py @@ -33,6 +33,11 @@ def interp(sig, t, tag=None): return sig[key][tag] +def interp_all(sig, t, end=OO): + v = fn.map(lambda u: signal([(t, interp(sig, t, u))], t, end, u), sig.tags) + return reduce(op.__or__, v) + + def dense_compose(sig1, sig2, init=None): sig12 = sig1 | sig2 tags = sig12.tags @@ -110,6 +115,7 @@ def eval_mtl_until(phi, dt): def _eval(x): sig = dense_compose(f1(x), f2(x), init=-OO) + sig = sig | interp_all(sig, x.start, OO) # Force valuation at start data = apply_weak_until(phi.arg1, phi.arg2, sig) return signal(data, x.start, OO, tag=phi) diff --git a/mtl/test_eval.py b/mtl/test_eval.py index dcbb896..9bd3683 100644 --- a/mtl/test_eval.py +++ b/mtl/test_eval.py @@ -20,3 +20,13 @@ def test_eval_regression_next_neg(): v = f(d, quantitative=False, dt=1, time=None) assert not f(d, quantitative=False, dt=1) assert min(t for t, _ in v) >= 0 + + +def test_eval_regression_until_start(): + """From issue #221""" + x = { + "ap1": [(0, True), (0.1, True), (0.2, False)], + } + + phi = (mtl.parse("(X TRUE W X TRUE)")) + phi(x, 0, quantitative=False) From 927d259fff70813f50440b53c8e913a6f175f3de Mon Sep 17 00:00:00 2001 From: Gaudeval Date: Wed, 6 Jan 2021 14:10:58 +0000 Subject: [PATCH 2/3] Add test for missing values in timed until evaluation --- mtl/test_eval.py | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/mtl/test_eval.py b/mtl/test_eval.py index 09d34fe..3aa6c31 100644 --- a/mtl/test_eval.py +++ b/mtl/test_eval.py @@ -42,3 +42,27 @@ def test_eval_regression_until_start(): phi = (mtl.parse("(X TRUE W X TRUE)")) phi(x, 0, quantitative=False) + + +def test_eval_regression_timed_until(): + """From issue #217""" + x = { + 'start': [(0, True), (200, False)], + 'success': [(0, False), (300, True)] + } + phi = mtl.parse('(~start U[0,120] success)') + assert phi(x, time=200, quantitative=False, dt=1) + + y = { + 'start': [(0, True), (1, False), (5, True), (6, True)], + 'success': [(0, False), (20, True)] + } + phi1 = mtl.parse('(start U[0,20] success)') + assert phi1(y, time=6, quantitative=False, dt=1) + + z = { + 'start': [(0, True), (200, False)], + 'success': [(0, False), (300, True)] + } + phi2 = mtl.parse('F[0,120]success') + assert phi2(z, time=181, quantitative=False, dt=1) From c53e490f80f14cde853e8a33c346fe5e474d30a9 Mon Sep 17 00:00:00 2001 From: Gaudeval Date: Wed, 6 Jan 2021 14:37:05 +0000 Subject: [PATCH 3/3] Force evaluation of timed always at candidate pivot points --- mtl/evaluator.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mtl/evaluator.py b/mtl/evaluator.py index cc3ada1..2af8cc4 100644 --- a/mtl/evaluator.py +++ b/mtl/evaluator.py @@ -135,6 +135,12 @@ def _eval(x): tmp = f(x) assert b >= a if b > a: + # Force valuation at pivot points + if a < b < OO: + ts = fn.map( + lambda t: interp_all(tmp, t - b - a + dt, tmp.end), + tmp.times()) + tmp = reduce(op.__or__, ts, tmp)[tmp.start:tmp.end] return tmp.rolling(a, b).map(_min, tag=phi) return tmp.retag({phi.arg: phi})