diff --git a/mtl/evaluator.py b/mtl/evaluator.py index c4159dd..2af8cc4 100644 --- a/mtl/evaluator.py +++ b/mtl/evaluator.py @@ -32,6 +32,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 @@ -109,6 +114,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) @@ -129,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}) diff --git a/mtl/test_eval.py b/mtl/test_eval.py index b356f18..3aa6c31 100644 --- a/mtl/test_eval.py +++ b/mtl/test_eval.py @@ -32,3 +32,37 @@ def test_eval_with_signal(): assert not spec(processed, quantitative=False) assert spec(processed, quantitative=True) == 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) + + +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)