The Variable.expand() method in ltl2ba.py performs contradiction
detection by checking if a negated variable already exists in the
graph node's old set. However, the isinstance check was incorrectly
testing the ASTNode wrapper instead of the wrapped operator, causing
the check to always return False.

The old set contains ASTNode instances which wrap LTL operators via
their .op attribute. The fix changes isinstance(f, NotOp) to
isinstance(f.op, NotOp) to correctly examine the wrapped operator
type. This follows the established pattern used elsewhere in the
file, such as the iteration at lines 572-574 which accesses
o.op.is_temporal() on items from node.old.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/rvgen/ltl2ba.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index 49f6b9200ff0a..79b45a1d61130 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -404,7 +404,7 @@ class Variable:
     @staticmethod
     def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
         for f in node.old:
-            if isinstance(f, NotOp) and f.op.child is n:
+            if isinstance(f.op, NotOp) and f.op.child is n:
                 return node_set
         node.old |= {n}
         return node.expand(node_set)
-- 
2.52.0

Wander Lairson Costa <wander@redhat.com> writes:
> The Variable.expand() method in ltl2ba.py performs contradiction
> detection by checking if a negated variable already exists in the
> graph node's old set. However, the isinstance check was incorrectly
> testing the ASTNode wrapper instead of the wrapped operator, causing
> the check to always return False.
>
> The old set contains ASTNode instances which wrap LTL operators via
> their .op attribute. The fix changes isinstance(f, NotOp) to
> isinstance(f.op, NotOp) to correctly examine the wrapped operator
> type. This follows the established pattern used elsewhere in the
> file, such as the iteration at lines 572-574 which accesses
> o.op.is_temporal() on items from node.old.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>

These isinstance() usages deserve to be buried. But I'm not sure yet how
to replace them. So, for now:

Reviewed-by: Nam Cao <namcao@linutronix.de>