added code for discretizing bounded stl

stl/ast.py

@@ -1,5 +1,4 @@
 # -*- coding: utf-8 -*-
-# TODO: supress + given a + (-b). i.e. want a - b
 
 from collections import deque, namedtuple
 from functools import lru_cache
@@ -265,7 +264,7 @@ class Next(namedtuple('Next', ['arg']), AST):
     __slots__ = ()
 
     def __repr__(self):
-        return f"X({self.arg})"
+        return f"◯({self.arg})"
 
     @property
     def children(self):
@@ -291,13 +290,8 @@ def ast_lens(phi,
              bind=True,
              *,
              pred=lambda _: False,
-             focus_lens=None,
+             focus_lens=lambda _: [lens],
              getter=False):
-    if focus_lens is None:
-
-        def focus_lens(_):
-            return [lens]
-
     child_lenses = _ast_lens(phi, pred=pred, focus_lens=focus_lens)
     phi = lenses.bind(phi) if bind else lens
     return (phi.Tuple if getter else phi.Fork)(*child_lenses)

stl/parser.py

@@ -2,7 +2,6 @@
 
 # TODO: allow multiplication to be distributive
 # TODO: support variables on both sides of ineq
-# TODO: Allow -x = -1*x
 
 from functools import partialmethod
 
@@ -24,12 +23,13 @@ iff = paren_phi _ ("⇔" / "<->" / "iff") _ (and / paren_phi)
 xor = paren_phi _ ("⊕" / "^" / "xor") _ (and / paren_phi)
 
 neg = ("~" / "¬") paren_phi
-next = "X" paren_phi
+next = next_sym paren_phi
 f = F interval? phi
 g = G interval? phi
 until = paren_phi __ U __ paren_phi
 timed_until = paren_phi __ U interval __ paren_phi
 
+next_sym = "X" / "◯"
 F = "F" / "◇"
 G = "G" / "□"
 U = "U"

stl/test_utils.py

@@ -4,7 +4,6 @@ from stl.hypothesis import SignalTemporalLogicStrategy
 from hypothesis import given
 from pytest import raises
 
-
 CONTEXT = {
     stl.parse('AP1'): stl.parse('F(x > 4)'),
     stl.parse('AP2'): stl.parse('(AP1) U (AP1)'),
@@ -61,3 +60,28 @@ def test_linear_stl_lipschitz(phi1, phi2):
 @given(SignalTemporalLogicStrategy, SignalTemporalLogicStrategy)
 def test_timed_until_smoke_test(phi1, phi2):
     stl.utils.timed_until(phi1, phi2, lo=2, hi=20)
+
+
+def test_discretize():
+    dt = 0.3
+
+    phi = stl.parse('X(AP1)')
+    assert stl.utils.is_discretizable(phi, dt)
+    phi2 = stl.utils.discretize(phi, dt)
+    phi3 = stl.utils.discretize(phi2, dt)
+    assert phi2 == phi3
+
+    phi = stl.parse('G[0.3, 1.2](F[0.6, 1.5](AP1))')
+    assert stl.utils.is_discretizable(phi, dt)
+    phi2 = stl.utils.discretize(phi, dt)
+    phi3 = stl.utils.discretize(phi2, dt)
+    assert phi2 == phi3
+
+    phi = stl.parse('G[0.3, 1.4](F[0.6, 1.5](AP1))')
+    assert not stl.utils.is_discretizable(phi, dt)
+
+    phi = stl.parse('G[0.3, 1.2](F(AP1))')
+    assert not stl.utils.is_discretizable(phi, dt)
+
+    phi = stl.parse('G[0.3, 1.2]((AP1) U (AP2))')
+    assert not stl.utils.is_discretizable(phi, dt)

stl/utils.py

@@ -1,16 +1,16 @@
 import operator as op
 from functools import reduce
+from math import isfinite
 
 import traces
+import numpy as np
 from lenses import bind
 
 import stl.ast
-from stl.ast import (And, F, G, Interval, LinEq, Neg,
-                     Or, Next, Until, AtomicPred,
-                     _Top, _Bot)
+from stl.ast import (And, F, G, Interval, LinEq, Neg, Or, Next, Until,
+                     AtomicPred, _Top, _Bot)
 from stl.types import STL
 
-
 oo = float('inf')
 
 
@@ -67,7 +67,7 @@ def const_trace(x, start=0):
 
 
 def eval_lineq(lineq, x, domain, compact=True):
-    lhs = sum(const_trace(term.coeff)*x[term.id] for term in lineq.terms)
+    lhs = sum(const_trace(term.coeff) * x[term.id] for term in lineq.terms)
     compare = op_lookup.get(lineq.op)
     output = lhs.operation(const_trace(lineq.const), compare)
     output.domain = domain
@@ -98,6 +98,48 @@ def implicit_validity_domain(phi, trace):
     return oracle, order
 
 
+# Code to discretize a bounded STL formula
+
+
+def discretize(phi, dt):
+    assert is_discretizable(phi, dt)
+    return _discretize(phi, dt)
+
+
+def _discretize(phi, dt):
+    if isinstance(phi, (LinEq, AtomicPred)):
+        return phi
+
+    children = tuple(_discretize(arg, dt) for arg in phi.children)
+    if isinstance(phi, (And, Or)):
+        return bind(phi).args.set(children)
+    elif isinstance(phi, (Neg, Next)):
+        return bind(phi).arg.set(children[0])
+
+    # Only remaining cases are G and F
+    psi = children[0]
+    l, u = round(phi.interval.lower / dt), round(phi.interval.upper / dt)
+    psis = (next(psi, i) for i in range(l, u + 1))
+    opf = andf if isinstance(phi, G) else orf
+    return opf(*psis)
+
+
+def _interval_discretizable(itvl, dt):
+    l, u = itvl.lower / dt, itvl.upper / dt
+    if not (isfinite(l) and isfinite(u)):
+        return False
+    return np.isclose(l, round(l)) and np.isclose(u, round(u))
+
+
+def is_discretizable(phi, dt):
+    if any(c for c in phi.walk() if isinstance(c, Until)):
+        return False
+
+    return all(
+        _interval_discretizable(c.interval, dt) for c in phi.walk()
+        if isinstance(c, (F, G)))
+
+
 # EDSL
 
 
@@ -129,5 +171,11 @@ def iff(x, y):
     return (x & y) | (~x & ~y)
 
 
+def next(phi, i=1):
+    for _ in range(i):
+        phi = Next(phi)
+    return phi
+
+
 def timed_until(phi, psi, lo, hi):
     return env(psi, lo=lo, hi=hi) & alw(stl.ast.Until(phi, psi), lo=0, hi=lo)