teaching/mtl-aas
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix timed until

Browse source
This commit is contained in:
Marcell Vazquez-Chanlatte 2020-04-06 13:04:04 -07:00
parent 31c3d3bead
commit 74f6efa314
2 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
mtl/evaluator.py
View file

@ -125,7 +125,12 @@ def eval_mtl_g(phi, dt):
return min(val[phi.arg]) return min(val[phi.arg])
def _eval(x): def _eval(x):
return f(x).rolling(a, b).map(_min, tag=phi) tmp = f(x)
assert b >= a
if b > a:
return tmp.rolling(a, b).map(_min, tag=phi)
return tmp.retag({phi.arg: phi})
return _eval return _eval

10
mtl/sugar.py
View file

@ -25,5 +25,11 @@ def until(phi, psi):
return ast.WeakUntil(phi, psi) & env(psi) return ast.WeakUntil(phi, psi) & env(psi)
def timed_until(phi, psi, lo, hi): def timed_until(left, right, lo, hi):
return env(psi, lo=lo, hi=hi) & alw(until(phi, psi), lo=0, hi=lo) assert 0 <= lo < hi
expr = env(right, lo=lo, hi=hi)
expr &= alw(left, lo=0, hi=lo)
expr &= alw(until(left, right), lo=lo, hi=lo)
return expr