The LTL parser is built using Ply. However, Ply is no longer maintained [1].
Switch to use Lark instead. In addition to being actively maintained, Lark also offers additional features (namely, automatically creating the abstract syntax tree) which make the parser simpler. Link: https://github.com/dabeaz/ply/commit/9d7c40099e23ff78f9d86ef69a26c1e8a83e706a [1] Signed-off-by: Nam Cao <[email protected]> --- v2: - fix identifier starting with a digit is allowed [Wander] - fixup ast node uid [Gabriele] - Fix up Literal AST node construction [Wander, Sashiko] - FIx up unary op error message [Sashiko] - Add nice exception handling [Gabriele] --- tools/verification/rvgen/__main__.py | 5 +- tools/verification/rvgen/rvgen/ltl2ba.py | 202 +++++++++-------------- 2 files changed, 82 insertions(+), 125 deletions(-) diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py index 5c923dc10d0f..0915cf86e43b 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -14,6 +14,7 @@ if __name__ == '__main__': from rvgen.container import Container from rvgen.ltl2k import ltl2k from rvgen.automata import AutomataError + from rvgen.ltl2ba import LTLError import argparse import sys @@ -57,8 +58,8 @@ if __name__ == '__main__': sys.exit(1) else: monitor = Container(vars(params)) - except AutomataError as e: - print(f"There was an error processing {params.spec}: {e}", file=sys.stderr) + except (AutomataError, LTLError) as e: + print(f"There was an error processing {params.spec}:\n{e}", file=sys.stderr) sys.exit(1) print(f"Writing the monitor into the directory {monitor.name}") diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py index 016e7cf93bbb..7cebda61bce8 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -7,9 +7,7 @@ # https://doi.org/10.1007/978-0-387-34892-6_1 # With extra optimizations -from ply.lex import lex -from ply.yacc import yacc -from .automata import AutomataError +import lark # Grammar: # ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl @@ -30,42 +28,41 @@ from .automata import AutomataError # imply # equivalent -tokens = ( - 'AND', - 'OR', - 'IMPLY', - 'UNTIL', - 'ALWAYS', - 'EVENTUALLY', - 'NEXT', - 'VARIABLE', - 'LITERAL', - 'NOT', - 'LPAREN', - 'RPAREN', - 'ASSIGN', -) - -t_AND = r'and' -t_OR = r'or' -t_IMPLY = r'imply' -t_UNTIL = r'until' -t_ALWAYS = r'always' -t_NEXT = r'next' -t_EVENTUALLY = r'eventually' -t_VARIABLE = r'[A-Z_0-9]+' -t_LITERAL = r'true|false' -t_NOT = r'not' -t_LPAREN = r'\(' -t_RPAREN = r'\)' -t_ASSIGN = r'=' -t_ignore_COMMENT = r'\#.*' -t_ignore = ' \t\n' - -def t_error(t): - raise AutomataError(f"Illegal character '{t.value[0]}'") - -lexer = lex() +GRAMMAR = r''' +start: assign+ + +assign: VARIABLE "=" _ltl + +_ltl: _opd | binop | unop + +_opd : VARIABLE + | LITERAL + | "(" _ltl ")" + +unop: UNOP _ltl +UNOP: "always" + | "eventually" + | "next" + | "not" + +binop: _opd BINOP _ltl +BINOP: "until" + | "and" + | "or" + | "imply" + +VARIABLE: /[A-Z_][A-Z0-9_]*/ +LITERAL: "true" | "false" + +COMMENT: "#" /.*/ "\n" +%ignore COMMENT + +%import common.WS +%ignore WS +''' + +class LTLError(Exception): + "Exception raised for malformed linear temporal logic" class GraphNode: uid = 0 @@ -97,7 +94,7 @@ class GraphNode: return self.id < other.id class ASTNode: - uid = 1 + uid = 0 def __init__(self, op): self.op = op @@ -433,90 +430,49 @@ class Literal: node.old |= {n} return node.expand(node_set) -def p_spec(p): - ''' - spec : assign - | assign spec - ''' - if len(p) == 3: - p[2].append(p[1]) - p[0] = p[2] - else: - p[0] = [p[1]] - -def p_assign(p): - ''' - assign : VARIABLE ASSIGN ltl - ''' - p[0] = (p[1], p[3]) - -def p_ltl(p): - ''' - ltl : opd - | binop - | unop - ''' - p[0] = p[1] - -def p_opd(p): - ''' - opd : VARIABLE - | LITERAL - | LPAREN ltl RPAREN - ''' - if p[1] == "true": - p[0] = ASTNode(Literal(True)) - elif p[1] == "false": - p[0] = ASTNode(Literal(False)) - elif p[1] == '(': - p[0] = p[2] - else: - p[0] = ASTNode(Variable(p[1])) - -def p_unop(p): - ''' - unop : ALWAYS ltl - | EVENTUALLY ltl - | NEXT ltl - | NOT ltl - ''' - if p[1] == "always": - op = AlwaysOp(p[2]) - elif p[1] == "eventually": - op = EventuallyOp(p[2]) - elif p[1] == "next": - op = NextOp(p[2]) - elif p[1] == "not": - op = NotOp(p[2]) - else: - raise AutomataError(f"Invalid unary operator {p[1]}") - - p[0] = ASTNode(op) - -def p_binop(p): - ''' - binop : opd UNTIL ltl - | opd AND ltl - | opd OR ltl - | opd IMPLY ltl - ''' - if p[2] == "and": - op = AndOp(p[1], p[3]) - elif p[2] == "until": - op = UntilOp(p[1], p[3]) - elif p[2] == "or": - op = OrOp(p[1], p[3]) - elif p[2] == "imply": - op = ImplyOp(p[1], p[3]) - else: - raise AutomataError(f"Invalid binary operator {p[2]}") - - p[0] = ASTNode(op) - -parser = yacc() +class Transform(lark.visitors.Transformer): + def unop(self, node): + if node[0] == "always": + return ASTNode(AlwaysOp(node[1])) + if node[0] == "eventually": + return ASTNode(EventuallyOp(node[1])) + if node[0] == "next": + return ASTNode(NextOp(node[1])) + if node[0] == "not": + return ASTNode(NotOp(node[1])) + raise ValueError("Unknown operator %s" % node[0]) + + def binop(self, node): + if node[1] == "until": + return ASTNode(UntilOp(node[0], node[2])) + if node[1] == "and": + return ASTNode(AndOp(node[0], node[2])) + if node[1] == "or": + return ASTNode(OrOp(node[0], node[2])) + if node[1] == "imply": + return ASTNode(ImplyOp(node[0], node[2])) + raise ValueError("Unknown operator %s" % node[1]) + + def VARIABLE(self, args): + return ASTNode(Variable(args)) + + def LITERAL(self, args): + return ASTNode(Literal(args == "true")) + + def start(self, node): + return node + + def assign(self, node): + return node[0].op.name, node[1] + +parser = lark.Lark(GRAMMAR) def parse_ltl(s: str) -> ASTNode: - spec = parser.parse(s) + try: + spec = parser.parse(s) + except lark.exceptions.UnexpectedInput as e: + raise LTLError(str(e)) + spec = Transform().transform(spec) rule = None subexpr = {} @@ -528,7 +484,7 @@ def parse_ltl(s: str) -> ASTNode: subexpr[assign[0]] = assign[1] if rule is None: - raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format") + raise LTLError("Please define your specification in the \"RULE = <LTL spec>\" format") for node in rule: if not isinstance(node.op, Variable): -- 2.47.3
