1

IVAR我知道 . 中（输入变量）和VAR（状态变量）之间的区别NuSMV。但是，我能够理解使用时的反例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 <-

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

4

1 回答 1

0

这两个反例都在执行跟踪的第一个状态中伪造了属性，因此接下来发生的事情在某种程度上并不重要。

来自以下文档nuXmv：

4.7 痕迹

跟踪由初始状态组成，可选地，后跟一系列状态-输入对，对应于模型的可能执行。除了初始状态之外，每一对都包含导致转换到新状态的输入，以及新状态本身。初始状态没有定义这样的输入值，因为它不依赖于任何输入的值。[...]

所以一条trace一般有如下结构：

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

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

可以尝试使用命令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邮寄名单，并在输出例程中提及此问题。

于 2018-05-11T17:49:49.530 回答