Re: [PATCH 01/13] verification/rvgen: Switch LTL parser to Lark

[Gabriele Monaco <gmonaco@redhat.com>]

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 = {}