From c495216626aa005ef068e25b7dca622be7da6b80 Mon Sep 17 00:00:00 2001
From: Marcell Vazquez-Chanlatte <mvc@linux.com>
Date: Sun, 12 Nov 2017 11:47:00 -0800
Subject: [PATCH] fixed bug in next operator and global operator

---
 stl/boolean_eval.py      | 28 ++++++++++++++++++----------
 stl/hypothesis.py        |  2 +-
 stl/test_boolean_eval.py | 12 ++++++++++--
 3 files changed, 29 insertions(+), 13 deletions(-)

diff --git a/stl/boolean_eval.py b/stl/boolean_eval.py
index d9d698f..e2467ed 100644
--- a/stl/boolean_eval.py
+++ b/stl/boolean_eval.py
@@ -116,18 +116,25 @@ def eval_stl_g(phi, dt):
         )])
         for (start, val), (end, val2) in intervals:
             start2, end2 = start - b, end + a
-            if end2 > start2 and start2:
+            if end2 > start2:
                 yield (start2, val)
 
-    def _eval(x):
-        y = f(x)
-        if len(y) <= 1:
-            return y
+    if b == float('inf'):
+        def _eval(x):
+            y = f(x)
+            val = len(y.slice(a, b)) == 1 and y[a]
+            return traces.TimeSeries(
+                [(y.domain.start(), val)], domain=y.domain)
+    else:
+        def _eval(x):
+            y = f(x)
+            if len(y) <= 1:
+                return y
 
-        out = traces.TimeSeries(process_intervals(y)).slice(
-            y.domain.start(), y.domain.end())
-        out.compact()
-        return out
+            out = traces.TimeSeries(process_intervals(y)).slice(
+                y.domain.start(), y.domain.end())
+            out.compact()
+            return out
 
     return _eval
 
@@ -150,7 +157,8 @@ def eval_stl_next(phi, dt):
 
     def _eval(x):
         y = f(x)
-        out = traces.TimeSeries(((t + dt, v) for t, v in y), domain=y.domain)
+        out = traces.TimeSeries(((t - dt, v) for t, v in y))
+        out = out.slice(y.domain.start(), y.domain.end())
         out.compact()
 
         return out
diff --git a/stl/hypothesis.py b/stl/hypothesis.py
index 5f1aeea..5fa39ef 100644
--- a/stl/hypothesis.py
+++ b/stl/hypothesis.py
@@ -18,5 +18,5 @@ GRAMMAR = {
 SignalTemporalLogicStrategy = st.builds(lambda term: stl.parse(''.join(term)),
                                         ContextFreeGrammarStrategy(
                                             GRAMMAR,
-                                            max_length=15,
+                                            max_length=14,
                                             start='phi'))
diff --git a/stl/test_boolean_eval.py b/stl/test_boolean_eval.py
index 39d6c5d..c9afc7b 100644
--- a/stl/test_boolean_eval.py
+++ b/stl/test_boolean_eval.py
@@ -1,6 +1,6 @@
 import hypothesis.strategies as st
 import traces
-from hypothesis import given
+from hypothesis import given, settings, Verbosity, Phase
 from pytest import raises
 
 import stl
@@ -81,6 +81,11 @@ def test_eval_smoke_tests(phi):
 
 
 @given(SignalTemporalLogicStrategy)
+@settings(
+    max_shrinks=0,
+    verbosity=Verbosity.verbose,
+    perform_health_check=False,
+    phases=[Phase.generate])
 def test_temporal_identities(phi):
     stl_eval = stl.boolean_eval.pointwise_sat(phi)
     stl_eval2 = stl.boolean_eval.pointwise_sat(~phi)
@@ -93,10 +98,13 @@ def test_temporal_identities(phi):
     assert not stl_eval5(x, 0)
     stl_eval6 = stl.boolean_eval.pointwise_sat(phi | ~phi)
     assert stl_eval6(x, 0)
+    stl_eval7 = stl.boolean_eval.pointwise_sat(stl.ast.Until(stl.TOP, phi))
+    stl_eval8 = stl.boolean_eval.pointwise_sat(stl.env(phi))
+    assert stl_eval7(x, 0) == stl_eval8(x, 0)
 
 
 @given(st.just(stl.BOT))
-def test_temporal_identities2(phi):
+def test_fastboolean_equiv(phi):
     stl_eval = stl.fastboolean_eval.pointwise_sat(stl.alw(phi, lo=0, hi=4))
     stl_eval2 = stl.fastboolean_eval.pointwise_sat(~stl.env(~phi, lo=0, hi=4))
     assert stl_eval2(x, 0) == stl_eval(x, 0)