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

[Gabriele Monaco]

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 <namcao@xxxxxxxxxxxxx>
> ---

Reviewed-by: Gabriele Monaco <gmonaco@xxxxxxxxxx>

> 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):