From a59756c58e5f69f4f28018a1a350417d0ecac166 Mon Sep 17 00:00:00 2001
From: Marcell Vazquez-Chanlatte <mvc@linux.com>
Date: Thu, 20 Apr 2017 23:16:00 -0700
Subject: [PATCH] implemented untimed until using bitarrays (although somewhat
 terribly)

---
 stl/fastboolean_eval.py  | 21 +++++++++++++++++++++
 stl/test_boolean_eval.py |  2 +-
 2 files changed, 22 insertions(+), 1 deletion(-)

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)