2

我是 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)

谁能告诉这有什么问题？

我如何编写“A 是否可以从 B 到达”的规范？- 这应该返回 false，因为没有定义转换

4

1 回答 1

1

注意：您的代码示例在我的机器上不起作用，它报告了一些语法错误，所以我实际上将其更改为如下所示：

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

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

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

存在一条从初始状态开始的路径是不正确的，这样逻辑条件迟早state=a -> state=c是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)。

一步可达。 如果要检查是否存在从保持状态到保持状态的单步 转换，则可以使用以下属性：state = astate = c

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

内容如下：

对于从所有初始状态开始的所有执行路径可以达到的所有状态，CTL属性始终state = a -> AX state != c是经过验证的。这样的性质表明，如果在当前状态state = a中，那么在所有可能的直接下一个状态中， 的值必然不同于。statec

如果我们用NuSMV检查这样的属性，我们会发现它已经过验证：

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

类似的示例适用于您要编码的其他属性。

路径可达性。如果要检查是否存在由任意且可变数量的中间转换形成的路径，该路径从保持状态开始达到保持状态，则编码略有不同：state = cstate = a

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

内容如下：

对于从所有初始状态开始的所有执行路径之后可以达到的所有状态，CTL属性始终state = a -> AX AG state != c是经过验证的。此类属性适用true于所有s'州

  • state != a在s'

或者

  • state = a在s', 并且对于所有出站路径上state != c的所有可达状态s''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)

而且，显然，它仍然可以工作。

但是，我没有这样做是有原因的：两种编码之间存在细微的语义差异，即使后者在某些情况下可用于验证可达性属性，但前一种编码更健壮，因为它更与可达性问题的实际语义紧密匹配。例如，模板在任何时候都惨遭失败，因为对于任何验证前提的状态，结论——可以重写为——不可能成立；前置B_COND_1 -> AG B_COND_2B_COND_2 := !B_COND_1s'B_COND_1AG B_COND_2AG !B_COND_1AX结论增加了一层间接性，并且更正确，因为只需要从执行树中的下一个状态开始就要求结论。

预计到达时间 #2：

你写：

我如何编写“A 是否可以从 B 到达”的规范？- 这应该返回 false，因为没有定义转换

false当没有来自to的路径时返回的属性如下：state = bstate = a

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

如果您想验证从永远无法state = a到达state = b的情况，那么这实际上是一个坏主意，原因有两个：

  • 如果该属性得到验证，则不会向您返回执行跟踪st可从 访问的见证反例，因此您可以自行确定为什么您的模型会出现这种情况state = astate = b

  • 如果属性是，则该false工具需要列出从无法到达的路径开始的所有（可能成倍增加）路径。state = bstate = a

由于这些原因，我实际上以相反的方式编码了可达性问题，在无法访问true时返回，否则返回+单个反例。state = astate = bfalse

于 2017-03-03T15:30:44.647 回答