logic - 了解 NuSMV 中递归定义的错误

Question

我在 NuSMV 中有一段代码出现了错误。代码是： -

MODULE main
VAR
    x1: {a,b,c,d,e};
    x2: {a,b,c,d,e};
ASSIGN

    next(x1) := case
        x1=a & x2=c: e;

        x1=d & next(x2)=c : a;
        TRUE : x1;
    esac;
    next(x2) := case
            x1=b & x2=b: c;

            x2=d & next(x1)=e : e;
            TRUE : x2;
        esac;

所以当我在 NuSMV 中编译它时，它给出了一个错误：recursively defined: x1

现在我可以通过删除与 x2 关联的下一个语句来处理 x1 的转换规则，这意味着我替换x1=d & next(x2)=c : a;为x1=d : a;orx1=d & x2=d : a;

我想了解导致错误的 NuSMV 软件的机制以及上述修复解决错误的原因。我认为这与我不明白的同步实现有关。有人可以给出精确的详细技术解释吗？

并解释为什么 variable 没有错误x2。它的转换规则也使用 next 运算符定义。

标签： logicnusmv

Answer 1