added Until to AST and added empty case for addf and orf

stl/__init__.py

@@ -6,3 +6,4 @@ from stl.parser import parse
 from stl.synth import lex_param_project
 from stl.boolean_eval import pointwise_sat
 from stl.fastboolean_eval import pointwise_satf
+from stl.types import STL

stl/ast.py

@@ -90,6 +90,14 @@ class G(ModalOp):
     OP = "□"
 
 
+class Until(namedtuple('ModalOp', ['interval', 'arg1', 'arg2']), AST):
+    def __repr__(self):
+        return f"({self.arg1} U{self.interval} ({self.arg2}))"
+    
+    def children(self):
+        return [self.arg1, self.arg2]
+
+
 class Neg(namedtuple('Neg', ['arg']), AST):
     def __repr__(self):
         return f"¬({self.arg})"

stl/parser.py

@@ -21,7 +21,7 @@ from sympy import Symbol, Number
 from stl import ast
 
 STL_GRAMMAR = Grammar(u'''
-phi = (g / f / lineq / AP / or / and / paren_phi)
+phi = (g / f / until / lineq / AP / or / and / paren_phi)
 
 paren_phi = "(" __ phi __ ")"
 
@@ -30,9 +30,12 @@ and = paren_phi _ ("∧" / "and") _ (and / paren_phi)
 
 f = F interval phi
 g = G interval phi
+until = "(" __ phi _ U interval _ phi __ ")"
 
 F = "F" / "◇"
 G = "G" / "□"
+U = "U"
+
 interval = "[" __ const_or_unbound __ "," __ const_or_unbound __ "]"
 
 const_or_unbound = unbound / const
@@ -98,6 +101,10 @@ class STLVisitor(NodeVisitor):
     visit_or = partialmethod(binop_visitor, op=ast.Or)
     visit_and = partialmethod(binop_visitor, op=ast.And)
 
+    def visit_until(self, _, children):
+        _, _, phi1, _, _, i, _, phi2, *_ = children
+        return ast.Until(i, phi1, phi2)
+
     def visit_id(self, name, _):
         return Symbol(name.text)
 

stl/utils.py

@@ -141,7 +141,7 @@ def until(phi, *, lo, hi):
     raise NotImplementedError
 
 def andf(*args):
-    return reduce(op.and_, args)
+    return reduce(op.and_, args, stl.And(tuple()))
 
-def orf():
-    return reduce(op.or_, args)
+def orf(*args):
+    return reduce(op.or_, args, stl.Or(tuple()))