diff --git a/stl/fastboolean_eval.py b/stl/fastboolean_eval.py index b2cec06..becada7 100644 --- a/stl/fastboolean_eval.py +++ b/stl/fastboolean_eval.py @@ -38,6 +38,27 @@ def temporal_op(stl, lo, hi, conjunction=False): return sat_comp +@pointwise_satf.register(stl.Until) +def _(stl): + f1, f2 = pointwise_satf(stl.arg1), pointwise_satf(stl.arg2) + def __until(x, t): + f1, f2 = pointwise_satf(stl.arg1), pointwise_satf(stl.arg2) + + state = False + for phi, tau in zip(reversed(f1(x, x.index)), reversed(x.index)): + if not phi: + state = f2(x, [tau]) + if tau in t: + yield state + + def _until(x, t): + retval = bitarray(__until(x, t)) + retval.reverse() + return retval + + return _until + + @pointwise_satf.register(stl.F) def _(stl): lo, hi = stl.interval diff --git a/stl/test_boolean_eval.py b/stl/test_boolean_eval.py index 25fab18..8762ea0 100644 --- a/stl/test_boolean_eval.py +++ b/stl/test_boolean_eval.py @@ -31,7 +31,7 @@ class TestSTLEval(unittest.TestCase): - @params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9) + @params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9, ex10, ex11) def test_fasteval(self, phi_str, _): phi = stl.parse(phi_str) stl_eval = stl.boolean_eval.pointwise_sat(phi)