aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGabriele Monaco <gmonaco@redhat.com>2026-05-14 17:20:48 +0200
committerGabriele Monaco <gmonaco@redhat.com>2026-06-04 16:44:25 +0200
commitdf996599cc69a9b74ff437c67751cf8a61f62e39 (patch)
tree8225f1f3f825d5c3a5c7057d987be74ad5c40c68
parent5f845ad706c0b394ae274e9a930044f78bef782e (diff)
verification/rvgen: Fix ltl2k writing True as a literal
The rvgen parser for LTL stores literal true values in the python representation (capitalised True), this doesn't build in C. The Literal class should already handle this case but ASTNode skips its strigification method and converts the value (true/false) directly. Fix by delegating ASTNode stringification to the Literal and Variable classes instead of bypassing them. Fixes: 97ffa4ce6ab32 ("verification/rvgen: Add support for linear temporal logic") Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20260514152055.229162-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
-rw-r--r--tools/verification/rvgen/rvgen/ltl2ba.py9
1 files changed, 5 insertions, 4 deletions
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index 7f538598a868..016e7cf93bbb 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -122,10 +122,8 @@ class ASTNode:
return self.op.expand(self, node, node_set)
def __str__(self):
- if isinstance(self.op, Literal):
- return str(self.op.value)
- if isinstance(self.op, Variable):
- return self.op.name.lower()
+ if isinstance(self.op, (Literal, Variable)):
+ return str(self.op)
return "val" + str(self.id)
def normalize(self):
@@ -382,6 +380,9 @@ class Variable:
def __iter__(self):
yield from ()
+ def __str__(self):
+ return self.name.lower()
+
def negate(self):
new = ASTNode(self)
return NotOp(new)