NuSMV:IVAR和VAR之间的区别

Question

我知道NuSMV中IVAR(输入变量(和VAR(状态变量(之间的区别。但是，当使用VAR时，我能够理解反例，但我不是另一种情况。

让我举个例子来说明它。

MODULE main
VAR
v1: 0..20;
v2: 0..20;
v3: 0..100;

INIT
v3 = 0;
TRANS
((v2+v1 = 0)  -> (next(v3) = 10)) &
(!(v2+v1 = 0) -> (next(v3) = v1 + v2))
LTLSPEC
G(v3 = 10);

NuSMV给出的反例(足够清楚(是：

Trace Type: Counterexample 
-> State: 1.1 <-
v1 = 0
v2 = 0
v3 = 0
-- Loop starts here
-> State: 1.2 <-
v3 = 10
-> State: 1.3 <-
v1 = 7
v2 = 6
-> State: 1.4 <-
v1 = 0
v2 = 0
v3 = 13
-> State: 1.5 <-
v3 = 10

现在，将 v1 和 v2 更改为 IVAR。

MODULE main
IVAR
v1: 0..20;
v2: 0..20;
VAR
v3: 0..100;
INIT
v3 = 0;
TRANS
((v2+v1 = 0)  -> (next(v3) = 10)) &
(!(v2+v1 = 0) -> (next(v3) = v1 + v2))
LTLSPEC
G(v3 = 10);

反例是：

Trace Type: Counterexample 
-> State: 1.1 <-
v3 = 0
-> Input: 1.2 <-
v1 = 7
v2 = 3
-- Loop starts here
-> State: 1.2 <-
v3 = 10
-> Input: 1.3 <-
-- Loop starts here
-> State: 1.3 <-
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
-> Input: 1.5 <-
-- Loop starts here
-> State: 1.5 <-
-> Input: 1.6 <-
-- Loop starts here
-> State: 1.6 <-
-> Input: 1.7 <-
-> State: 1.7 <-

有人能解释为什么这个反例如此奇怪吗？它有几个嵌套循环。输出是什么意思？

Answer 1

这两个反例都在执行跟踪的第一个状态下伪造属性，因此接下来发生的事情有点不相关。

---

来自nuXmv的文档：

4.7 痕迹

跟踪由初始状态组成，可以选择后跟 对应于可能执行的状态-输入对序列 的模型。除此之外，从初始状态开始，每对都包含 导致转换到新状态和新状态的输入 本身。初始状态没有像它那样定义这样的输入值 不依赖于任何输入的值。[...]

因此，跟踪通常具有以下结构：

S_0 | I_0 -> S_1 | I_1 -> S_2 | ... | I_{N-1} -> S_N

这个想法是通过在状态S_k上应用输入I_k来获得状态S_{k+1}。

可以尝试使用命令goto_state和print_current_state，来导航反例并打印每个状态的内容。或者，人们可能还记得NuSMV和nuXmv只打印从一个状态到下一个状态的更改变量，因此执行跟踪应如下所示：

-> State: 1.1 <-
v3 = 0
-> Input: 1.2 <-
v1 = 7
v2 = 3
-- Loop starts here
-> State: 1.2 <-
v3 = 10
-> Input: 1.3 <-
v1 = 7
v2 = 3
-- Loop starts here
-> State: 1.3 <-
v3 = 10
-> Input: 1.4 <-
v1 = 7
v2 = 3
-- Loop starts here
-> State: 1.4 <-
v3 = 10
-> Input: 1.5 <-
v1 = 7
v2 = 3
-> State: 1.5 <-
v3 = 10

所以基本上在第一次转换之后，我们最终会永远处于相同的状态，输入和输出永远不会改变。

---

您可能需要联系NuSMV或nuXmv邮件列表，并在输出例程中提及此问题。