check for invertability in parser

stl/ast.py

@@ -194,3 +194,17 @@ class Neg(namedtuple('Neg', ['arg']), AST):
     def __hash__(self):
         # TODO: compute hash based on contents
         return hash(repr(self))
+
+
+class Next(namedtuple('Next', ['arg']), AST):
+    __slots__ = ()
+
+    def __repr__(self):
+        return f"X({self.arg})"
+
+    def children(self):
+        return [self.arg]
+
+    def __hash__(self):
+        # TODO: compute hash based on contents
+        return hash(repr(self))

stl/parser.py

@@ -21,7 +21,7 @@ from stl import ast
 from stl.utils import implies, xor, iff, env, alw
 
 STL_GRAMMAR = Grammar(u'''
-phi = (timed_until / until / neg / g / f / lineq / AP / or / and / implies / xor / iff / paren_phi)
+phi = (timed_until / until / neg / next / g / f / lineq / AP / or / and / implies / xor / iff / paren_phi)
 
 paren_phi = "(" __ phi __ ")"
 
@@ -32,7 +32,7 @@ iff = paren_phi _ ("⇔" / "<->" / "iff") _ (and / paren_phi)
 xor = paren_phi _ ("⊕" / "^" / "xor") _ (and / paren_phi)
 
 neg = ("~" / "¬") phi
-
+next = "X" paren_phi
 f = F interval? phi
 g = G interval? phi
 until = paren_phi __ U __ paren_phi
@@ -72,7 +72,7 @@ EOL = "\\n"
 class STLVisitor(NodeVisitor):
     def __init__(self, H=float('inf')):
         super().__init__()
-        self.default_interval = ast.Interval(0, H)
+        self.default_interval = ast.Interval(0.0, H)
 
     def generic_visit(self, _, children):
         return children
@@ -87,6 +87,10 @@ class STLVisitor(NodeVisitor):
         _, _, (left,), _, _, _, (right,), _, _ = children
         left = left if left != [] else float("inf")
         right = right if right != [] else float("inf")
+        if isinstance(left, int):
+            left = float(left)
+        if isinstance(right, int):
+            left = float(right)
         return ast.Interval(left, right)
 
     def get_text(self, node, _):
@@ -186,6 +190,9 @@ class STLVisitor(NodeVisitor):
     def visit_neg(self, _, children):
         return ast.Neg(children[1])
 
+    def visit_next(self, _, children):
+        return ast.Next(children[1])
+
 
 def parse(stl_str:str, rule:str="phi", H=float('inf')) -> "STL":
     return STLVisitor(H).visit(STL_GRAMMAR[rule].parse(stl_str))

stl/test_parser.py

@@ -1,40 +1,21 @@
 # -*- coding: utf-8 -*-
 import stl
-import unittest
+from hypothesis import given, note
-from sympy import Symbol
+from hypothesis_cfg import ContextFreeGrammarStrategy
 
-ex1 = ('x1 > 2', stl.LinEq(
+GRAMMAR = {
-    (stl.Var(1, Symbol("x1"), stl.t_sym),),
+    'phi': (('Unary', '(', 'phi', ')'),
-    ">",
+            ('(', 'phi', ')',  'Binary', '(', 'phi', ')'),
-    2.0
+            ('AP',)),
-))
+    'Unary': (('~',), ('G',), ('F',), ('X',)),
-ex1_ = ('x1 > a?', stl.LinEq(
+    'Binary': ((' | ',), (' & ',), (' U ',)),
-    (stl.Var(1, Symbol("x1"), stl.t_sym),),
+}
-    ">",
-    Symbol("a?")
-))
 
-ex1__ = ('x1', stl.AtomicPred(Symbol('x1'), stl.t_sym))
 
-i1 = stl.Interval(0., 1.)
+@given(ContextFreeGrammarStrategy(GRAMMAR, length=20, start='phi'))
-i1_ = stl.Interval(0., Symbol("b?"))
+def test_invertable_repr(foo):
-i2 = stl.Interval(2., 3.)
+    note(''.join(foo))
-ex2 = ('◇[0,1](x1 > 2)', stl.F(i1, ex1[1]))
+    phi = stl.parse(''.join(foo))
-ex3 = ('□[2,3]◇[0,1](x1 > 2)', stl.G(i2, ex2[1]))
+    assert str(phi) == str(stl.parse(str(phi)))
-ex4 = ('(x1 > 2) or ((x1 > 2) or (x1 > 2))', 
-       stl.Or((ex1[1], ex1[1], ex1[1])))
-ex5 = ('G[0, b?](x1 > a?)',
-       stl.G(i1_, ex1_[1]))
-ex6 = ('◇[0,1](x1)', stl.F(i1, ex1__[1]))
-ex7 = ('F[0, inf](x)', stl.parse("F(x)"))
 
-'''
-class TestSTLParser(unittest.TestCase):
-    @params(ex1, ex2, ex3, ex4, ex5, ex6, ex7)
-    def test_stl(self, phi_str, phi):
-        self.assertEqual(stl.parse(phi_str), phi)
 
-    def test_smoke_test(self):
-        """Previously broken parses"""
-        stl.parse("◇[0,inf]((1*Lane_ID(t) = 1.0) ∧ (◇[0.0,eps?]((◇[eps?,tau1?](¬(1*Lane_ID(t) = 1.0))) ∧ (□[0,tau1?]((1*Lane_ID(t) = 1.0) U (¬(1*Lane_ID(t) = 1.0)))))))")
-'''