teaching/mtl-aas
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

remove timed until

Browse source
This commit is contained in:
Marcell Vazquez-Chanlatte 2017-04-20 20:40:49 -07:00
parent 476917860e
commit 94934b56c9
2 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
stl/ast.py
View file

@ -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]

7
stl/parser.py
View file

@ -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)