Messages in this thread Patch in this message |  | | Subject | Re: [PATCH 01/13] verification/rvgen: Switch LTL parser to Lark | | From | Gabriele Monaco <> | | Date | Wed, 06 May 2026 09:37:40 +0200 |
| |
On Tue, 2026-05-05 at 08:59 +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 <namcao@linutronix.de>
It looks very neat! I didn't go through it fully just yet, though. This one works fine but there's a nit: the ASTNode's id starts from 1, but apparently the new grammar consider RULE as a node too, this results in variables in the generated header file starting from val2 (rather than val1).
Unless I missed something here, we should probably start from 0:
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py index b2dee2dbe257..9b6a20db4acb 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -92,7 +92,7 @@ class GraphNode: return self.id < other.id class ASTNode: - uid = 1 + uid = 0 def __init__(self, op): self.op = op Also it doesn't gracefully handle an invalid syntax, but that's probably still a work in progress.
Thanks, Gabriele
> --- > tools/verification/rvgen/rvgen/ltl2ba.py | 189 +++++++++-------------- > 1 file changed, 70 insertions(+), 119 deletions(-) > > diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py > b/tools/verification/rvgen/rvgen/ltl2ba.py > index 7f538598a868..b2dee2dbe257 100644 > --- a/tools/verification/rvgen/rvgen/ltl2ba.py > +++ b/tools/verification/rvgen/rvgen/ltl2ba.py > @@ -7,8 +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 > +import lark > from .automata import AutomataError > > # Grammar: > @@ -30,42 +29,38 @@ 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_0-9]+/ > +LITERAL: "true" | "false" > + > +COMMENT: "#" /.*/ "\n" > +%ignore COMMENT > + > +%import common.WS > +%ignore WS > +''' > > class GraphNode: > uid = 0 > @@ -432,90 +427,46 @@ 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[1]) > + > + 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(Variable(args)) > + > + 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) > + spec = Transform().transform(spec) > > rule = None > subexpr = {}
|  |