diff --git a/stl/ast.py b/stl/ast.py index f65b179..41d9001 100644 --- a/stl/ast.py +++ b/stl/ast.py @@ -65,14 +65,11 @@ TOP = _Top() BOT = _Bot() -class AtomicPred(namedtuple("AP", ["id", "time"]), AST): +class AtomicPred(namedtuple("AP", ["id"]), AST): __slots__ = () def __repr__(self): - # TODO: fix this hack... - if str(self.time) in ("t + dt", "dt + t"): - return f"{self.id}'" - return f"{self.id}({self.time})" + return f"{self.id}" def children(self): return [] @@ -92,14 +89,11 @@ class LinEq(namedtuple("LinEquality", ["terms", "op", "const"]), AST): return hash(repr(self)) -class Var(namedtuple("Var", ["coeff", "id", "time"])): +class Var(namedtuple("Var", ["coeff", "id"])): __slots__ = () def __repr__(self): - # TODO: fix this hack... - if str(self.time) in ("t + dt", "dt + t"): - return f"{self.coeff}*{self.id}'" - return f"{self.coeff}*{self.id}({self.time})" + return f"{self.coeff}*{self.id}" class Interval(namedtuple('I', ['lower', 'upper'])): diff --git a/stl/parser.py b/stl/parser.py index 7b716af..38e916a 100644 --- a/stl/parser.py +++ b/stl/parser.py @@ -21,7 +21,8 @@ from stl import ast from stl.utils import implies, xor, iff, env, alw STL_GRAMMAR = Grammar(u''' -phi = (timed_until / until / neg / next / 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 __ ")" @@ -31,7 +32,7 @@ implies = paren_phi _ ("→" / "->") _ (and / paren_phi) iff = paren_phi _ ("⇔" / "<->" / "iff") _ (and / paren_phi) xor = paren_phi _ ("⊕" / "^" / "xor") _ (and / paren_phi) -neg = ("~" / "¬") phi +neg = ("~" / "¬") paren_phi next = "X" paren_phi f = F interval? phi g = G interval? phi @@ -51,12 +52,8 @@ term = coeff? var coeff = ((dt __ "*" __)? const __ "*" __) / (dt __ "*") terms = (term __ pm __ terms) / term -var = id time? -time = prime / time_index -time_index = "(" ("t" / const) ")" -prime = "'" - -AP = id time? +var = id +AP = ~r"[a-zA-z\d]+" pm = "+" / "-" dt = "dt" @@ -135,13 +132,6 @@ class STLVisitor(NodeVisitor): def visit_id(self, name, _): return Symbol(name.text) - def visit_var(self, _, children): - iden, time_node = children - - time_node = list(flatten(time_node)) - time = time_node[0] if len(time_node) > 0 else ast.t_sym - - return iden, time def visit_time_index(self, _, children): children = list(flatten(children)) @@ -185,7 +175,7 @@ class STLVisitor(NodeVisitor): return Number(1) if node.text == "+" else Number(-1) def visit_AP(self, *args): - return ast.AtomicPred(*self.visit_var(*args)) + return ast.AtomicPred(self.visit_id(*args)) def visit_neg(self, _, children): return ast.Neg(children[1]) diff --git a/stl/test_parser.py b/stl/test_parser.py index 379cd36..92de3b8 100644 --- a/stl/test_parser.py +++ b/stl/test_parser.py @@ -12,7 +12,7 @@ GRAMMAR = { } -@given(ContextFreeGrammarStrategy(GRAMMAR, length=20, start='phi')) +@given(ContextFreeGrammarStrategy(GRAMMAR, length=15, start='phi')) def test_invertable_repr(foo): note(''.join(foo)) phi = stl.parse(''.join(foo))