From 39885d3fe010e1658dd3019cb18a027558db47cc Mon Sep 17 00:00:00 2001
From: Marcell Vazquez-Chanlatte <mvc@linux.com>
Date: Tue, 3 Jan 2017 19:19:15 -0800
Subject: [PATCH] added Until to AST and added empty case for addf and orf

---
 stl/__init__.py | 1 +
 stl/ast.py      | 8 ++++++++
 stl/parser.py   | 9 ++++++++-
 stl/utils.py    | 6 +++---
 4 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/stl/__init__.py b/stl/__init__.py
index fc7e15e..e9e248a 100644
--- a/stl/__init__.py
+++ b/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
diff --git a/stl/ast.py b/stl/ast.py
index 92830a6..66d50fc 100644
--- a/stl/ast.py
+++ b/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})"
diff --git a/stl/parser.py b/stl/parser.py
index 81ccd51..805b523 100644
--- a/stl/parser.py
+++ b/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)
 
diff --git a/stl/utils.py b/stl/utils.py
index de7560f..d5e9365 100644
--- a/stl/utils.py
+++ b/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()))