了解 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

现在我可以通过删除与 x1 的转换规则的 x2 关联的下一个语句来轻松解决此错误，这意味着我将 x1=d & next(x2)=c : a; 替换为 x1=d : a; 或 x1=d & x2=d : a;

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

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

Answer 1

比那简单多了。

您有循环依赖，软件无法为您解决。

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

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

计算机（或人类）应该如何决定下一个状态下的 x1 和 x2 的值，当决定此类分配需要提前知道答案时？

您违反了所谓的循环依赖规则，如docs第 2.3.8 节

中所述

Rules for assignments

Assignments describe a system of equations that say how the FSM evolves through time. With an arbitrary set of equations there is no guarantee that a solution exists or that it is unique. We tackle this problem by placing certain restrictive syntactic rules on the structure of assignments, thus guaranteeing that the program is implementable.

The restriction rules for assignments are:

The single assignment rule – each variable may be assigned only once.

The circular dependency rule – a set of equations must not have “cycles” in its dependency graph not broken by delays.

[...]

If we have an assignment like x := y ;, then we say that x depends on y. A combinatorial loop is a cycle of dependencies not broken by delays. For instance, the assignments:
x := y;
y := x;
form a combinatorial loop. Indeed, there is no fixed order in which we can compute x and y, since at each time instant the value of x depends on the value of y and vice-versa We can introduce a “unit delay dependency” using the next() operator.
      x := y;
next(y) := x;
In this case, there is a unit delay dependency between x and y. A combinatorial loop is a cycle of dependencies whose total delay is zero. In NUSMV combinatorial loops are illegal. This guarantees that for any set of equations describing the behavior of variable, there is at least one solution.

[...]

你问：

[...] why the above fix resolves the error.

它修复了错误，因为它打破了组合循环。更改后，软件仍需要计算 x1 的未来值，以便计算 x2 的未来值。然而，为了计算 x1 的未来值，现在它不再需要知道 x2 的未来值（或任何其他不可用的信息，对于所有重要的事情），因此它可以解决这两个分配。

你问：

And also explain why there is no error with variable x2. Its transition rules are aslo defined using the next operator.

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

了解 NuSMV 中递归定义的错误

Understanding recursively defined error in NuSMV

logic

nusmv