Skip to content

Commit

Permalink
Merge pull request #222 from Gaudeval/fix/221-until-slicing
Browse files Browse the repository at this point in the history
Fix missing value on signal start after until
  • Loading branch information
mvcisback committed Jan 7, 2021
2 parents 5a6abd1 + c53e490 commit 2aaa340
Show file tree
Hide file tree
Showing 2 changed files with 46 additions and 0 deletions.
12 changes: 12 additions & 0 deletions mtl/evaluator.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)

Expand All @@ -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})
Expand Down
34 changes: 34 additions & 0 deletions mtl/test_eval.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)

0 comments on commit 2aaa340

Please sign in to comment.