On Thu, 2026-05-28 at 10:27 +0200, Nam Cao wrote: > 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]> > ---
Reviewed-by: Gabriele Monaco <[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):
