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 <[email protected]>
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 = {}
