From 94934b56c900f8241e3f45c81a33087352d90cd9 Mon Sep 17 00:00:00 2001 From: Marcell Vazquez-Chanlatte Date: Thu, 20 Apr 2017 20:40:49 -0700 Subject: [PATCH] remove timed until --- stl/ast.py | 4 ++-- stl/parser.py | 7 +++---- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/stl/ast.py b/stl/ast.py index 80a8d74..92f4b26 100644 --- a/stl/ast.py +++ b/stl/ast.py @@ -139,9 +139,9 @@ class G(ModalOp): return hash(repr(self)) -class Until(namedtuple('ModalOp', ['interval', 'arg1', 'arg2']), AST): +class Until(namedtuple('ModalOp', ['arg1', 'arg2']), AST): def __repr__(self): - return f"({self.arg1} U{self.interval} ({self.arg2}))" + return f"({self.arg1} U ({self.arg2}))" def children(self): return [self.arg1, self.arg2] diff --git a/stl/parser.py b/stl/parser.py index a6f3310..4b8f4b9 100644 --- a/stl/parser.py +++ b/stl/parser.py @@ -35,7 +35,7 @@ neg = ("~" / "¬") phi f = F interval? phi g = G interval? phi -until = paren_phi __ U interval? __ paren_phi +until = paren_phi __ U __ paren_phi F = "F" / "◇" G = "G" / "□" @@ -118,9 +118,8 @@ class STLVisitor(NodeVisitor): visit_implies = partialmethod(sugar_binop_visitor, op=implies) def visit_until(self, _, children): - phi1, _, _, i, _, phi2 = children - i = self.default_interval if not i else i[0] - return ast.Until(i, phi1, phi2) + phi1, _, _, _, phi2 = children + return ast.Until(phi1, phi2) def visit_id(self, name, _): return Symbol(name.text)