我在 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 运算符定义。