NuSMV 通过了错误的规范

Question

我是 NuSMV 和 CTL 的新手，正在尝试简单的示例。我有 3 个状态 A、B 和 C，并且有一个从 A-> B

的转换

我在 NuSMV 中对其建模，并想检查是否存在从 B 到 A 的任何执行路径。尽管我尚未定义此类转换，但规范给出了反例。

Module main
VAR
state:{a,b};
ASSIGN
init(state):=a;
next(state):=b;
SPEC !EF(state=a -> state=c)
SPEC !EF(state=b -> state=a)

谁能告诉我这是怎么回事？

我如何为 "is A reachable from B?" 编写规范 - 这应该 return false 因为没有定义转换

Answer 1

注意：您的代码示例在我的机器上无法运行，它报告了一些语法错误，所以我实际上将其更改为看起来像这样：

MODULE main ()
VAR
  state : {a,b,c};

ASSIGN
  init(state):=a;
  next(state):=b;

对您的方法发表评论。 属性 SPEC !EF(state=a -> state=c) 可以读作：

it is not true that there exists a path starting from the initial state such that sooner or later the logic condition state=a -> state=c is true.

条件 state = a -> state = c 对于所有状态 true 只有 state != a，因为不存在条件 state = a 和 state = c可以同时持有

如果你运行NuSMV，你得到以下反例：

NuSMV > reset; read_model -i test.smv; go; check_property
-- specification !(EF (state = a -> state = c))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  state = a
-> State: 1.2 <-
  state = b

在状态 1.2 中，变量 state 等于 b，因此 state = a -> state = c 是 true 并且违反了 !EF(state = a -> state = c)。

对于属性 SPEC !EF(state=b -> state=a).

也有类似的考虑

一步可达性。 如果你想检查不存在 one-step transition 从 state = a 保持到 state = c 成立，那么你可以使用下面的属性:

SPEC AG (state = a -> AX state != c)

内容如下：

for all states, that can be reached following all execution paths starting from all initial states, the CTL property state = a -> AX state != c is always verified. Such property says that, if in the current state state = a, then it is necessarily the case that in all possible immediate next states the value of state is different from c.

如果我们用NuSMV检查这样的属性，我们发现它被验证了：

NuSMV > reset; read_model -i test.smv; go; check_property
-- specification AG (state = a -> AX state != c)  is true

类似的示例适用于您要编码的另一个属性。

路径可达性。如果你想检查不存在路径，由任意和变量数量的 中间转换 ，达到 state = c 成立的状态，从 state = c 的状态开始=28=]成立，那么编码略有不同：

SPEC AG (state = a -> AX AG state != c)

内容如下：

for all states, that can be reached following all executions paths starting from all initial states, the CTL property state = a -> AX AG state != c is always verified. Such property is true for all states s' s.t.

state != a in s'

or

state = a in s', and state != c for all reachable states s'' on all the outgoing paths that start at s'

如果我们用NuSMV检查这样的属性，我们发现它被验证了：

NuSMV > reset; read_model -i test.smv; go; check_property
-- specification AG (state = a -> AX (AG state != c))  is true

为了更好地概述两种编码之间的差异，我将在此处放置一个模型示例，第一个属性 是 false 但第二个是 true:

MODULE main ()
VAR
  state : {a,b,c};

ASSIGN
  init(state):=a;
  next(state) := case
     state = a : b;
     state = b : c;
     TRUE : state;
    esac;

SPEC AG (state = a -> AX state != c)
SPEC AG (state = a -> AX AG state != c)

如果你运行 NuSMV 超过这个例子，输出如下：

NuSMV > reset; read_model -i test.smv; go; check_property
-- specification AG (state = a -> AX state != c)  is true
-- specification AG (state = a -> AX (AG state != c))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  state = a
-> State: 1.2 <-
  state = b
-> State: 1.3 <-
  state = c

显然，如果第一个属性被发现是false，那么第二个属性也必须是 false。

K 步可达性。 一步可达性编码可以推广到精确k步可达AX 公式中：

SPEC AG (state = a -> AX state != c)       -- state != c after 1 transition
SPEC AG (state = a -> AX AX state != c)    -- state != c after 2 transitions
SPEC AG (state = a -> AX AX AX state != c) -- state != c after 3 transitions
SPEC AG (state = a -> AX ... state != c)   -- state != c after 1 + |...| transitions

预计到达时间：

在此用例场景中，属性

SPEC AG (state = a -> AX AG state != c)

可以简化为

SPEC AG (state = a -> AG state != c)

而且，显然，它仍然有效。

但是，我没有这样做是有原因的：两种编码之间存在微妙的语义差异，尽管后者可以用来验证reachability 属性在某些情况下，前者 encoding more robust 因为它更紧密匹配 可达性 问题的实际语义。例如模板 B_COND_1 -> AG B_COND_2 每当 B_COND_2 := !B_COND_1 时都会惨败，因为对于任何验证前提 B_COND_1 的状态 s' 结论 AG B_COND_2 -- 可以重写为 AG !B_COND_1-- 不可能成立；在结论前添加 AX 增加了一层间接性，它更正确，因为结论只需要从 下一个状态 在执行树中。

预计到达时间#2：

你写：

how do i write specification for "is A reachable from B?" - this should return false as there is no transition defined

A 属性 that returns false 当没有 path 从 state = b 到 state = a,如下：

SPEC AG (state = b -> EF state = a)

如果您想验证 永远不会state = a可以从state = b到达, 那么这实际上是一个坏主意，原因有二：

如果属性得到验证，您不会返回 witness counter-example 执行跟踪s.t。 state = a 可从 state = b 访问，因此您需要自行确定为什么您的模型会出现这种情况
如果属性是 false，该工具将需要列出所有 （可能呈指数级增长） 路径开始来自 state = b 这样就无法到达 state = a。

出于这些原因，我实际上以相反的方式对可达性问题进行了编码，当无法从 state = b 和 false + [=143 访问 state = a 时返回 true =]单个反例否则。

NuSMV 通过了错误的规范

NuSMV passes wrong specification

logic

temporal

ctl

nusmv