理解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 : a;或x1=d & x2=d : a;替换x1=d & next(x2)=c : a;。

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

并解释为什么变量x2没有错误。它的转换规则是用下一个运算符来定义的。

Answer 1

比那简单多了。

您有一个循环依赖项，而该软件无法为您解决这个问题。

next(x1) := case
     ... & next(x2) : ...
esac;

next(x2) := case
     ... & next(x1) : ...
esac;

计算机(或人类)如何在下一个状态下决定x1和x2的值，而决定这样的赋值需要事先知道答案？

您违反了所谓的循环依赖规则，如文档 2.3.8节所示。

作业的规则 作业描述了一组方程，描述FSM是如何随时间发展的。对于任意一组方程，不能保证存在一个解或它是唯一的。我们通过在赋值结构上设置一定的限制语法规则来解决这个问题，从而保证程序是可实现的。 转让的限制规则是：

• 单一赋值规则-每个变量只能分配一次。
• 循环依赖规则--一组方程在其依赖图中不能有“循环”，不能被延迟破坏。

..。

如果我们有像x := y ;这样的赋值，那么我们就说x依赖于y。组合循环是依赖于不被延迟打破的循环。例如，分配：

X := y；y := x；

形成一个组合循环。实际上，我们不存在计算x和y的固定顺序，因为在每个时刻，x的值取决于y的值，反之亦然，我们可以使用next()运算符引入“单位延迟依赖项”。

   x := y; next(y) := x;

在这种情况下，x和y之间存在单位延迟依赖关系。组合回路是一个依赖关系的循环，其总延迟为零。在NUSMV中，组合循环是非法的。这保证了对于描述变量行为的任何一组方程，至少有一个解。

..。

你问：

..。为什么上面的修复解决了错误。

它修复了错误，因为它破坏了组合循环。改变后，软件仍然需要计算x1的未来值，以便计算x2的未来值。然而，现在要计算x1的未来值，它不再需要知道x2的未来值(或者任何其他不可用的信息，不管有什么关系)，这样它就可以解决这两个赋值问题。

你问：

并解释为什么变量x2没有错误。它的转换规则是用下一个运算符来定义的。

在x1和x2上独立完成的两项作业都是完全合法的。但是，错误并不发生在单个赋值上，而是在这两个赋值的组合上。由于只有一个循环依赖项，涉及两个变量，因此一旦发现错误，就只报告一次。因此，通过更改x1上的赋值或x2上的赋值来修复它并不重要，只要依赖关系图中不再存在循环。