Commit 8aee49c5 authored by Wander Lairson Costa's avatar Wander Lairson Costa Committed by Gabriele Monaco
Browse files

rv/rvgen: fix isinstance check in Variable.expand() 



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: default avatarWander Lairson Costa <wander@redhat.com>
Reviewed-by: default avatarNam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260223162407.147003-16-wander@redhat.com


Signed-off-by: default avatarGabriele Monaco <gmonaco@redhat.com>
parent d7ee9623

tools/verification/rvgen/rvgen/ltl2ba.py

+1 −1
Original line number Diff line number Diff line
@@ -395,7 +395,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)