2

当我尝试在SMV中检查“EG（！s11included＆！s10included）”时，它被报告为错误并给出了一个反例如下，我认为相反它支持这个CTL规范。我的 CTL 规范有问题吗？

-- specification EG (!s11included & !s10included)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 9.1 <-
    s00included = TRUE
    s01included = TRUE
    s10included = FALSE
    s11included = FALSE
4

1 回答 1

0

简短的回答：

不，您的CTL规范没有任何问题：您观察到的情况是正常的，完全取决于您的模型规范。

该工具会打印一个反例，直到违反给定属性的第一个状态（包括在内） 。尽管对于人类操作员来说似乎有点武断，因为有时会从执行跟踪本身隐藏属性违规的原因，但从CTL模型检查的角度来看，这种设计选择非常有意义。需要注意的重要一点是结果可以信任，更重要的是，可以通过运行模拟进行双重检查。

例子：

我邀请你看下面的例子。

MODULE main
VAR a : boolean;
VAR b : boolean;

ASSIGN
next(a) := case
    a = FALSE : { TRUE };
    TRUE      : { TRUE, FALSE };
  esac;

next(b) := case
    b = FALSE : { TRUE };
    TRUE      : { TRUE, FALSE };
  esac;

CTLSPEC EG (!a & !b);

在这个模型中，每当a(resp. b) 是FALSE我们确定地将其设置为TRUE，否则我们允许它任意改变。

如果我们检查与您的完全相同的CTL属性，我们会得到以下反例：

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

如您所见，反例与您的匹配100%。到底是怎么回事？

好吧，基本上NuSMV保守地打印了最少的必要状态，以达到违反属性的状态。在这种情况下，执行跟踪的初始状态已经违反了该属性，因为下一个确定性的转换会导致一个状态，在这种状态下，要么是要么a是b（TRUE 在这种特定情况下，两者都是）：

NuSMV > pick_state -s 1.1
NuSMV > simulate -iv -k 2
********  Simulation Starting From State 3.1   ********

***************  AVAILABLE STATES  *************

================= State =================
0) -------------------------
  a = TRUE
  b = TRUE


There's only one available state. Press Return to Proceed.

Chosen state is: 0

***************  AVAILABLE STATES  *************

================= State =================
0) -------------------------
  a = TRUE
  b = TRUE


================= State =================
1) -------------------------
  b = FALSE


================= State =================
2) -------------------------
  a = FALSE
  b = TRUE


================= State =================
3) -------------------------
  b = FALSE


Choose a state from the above (0-3): ^C

我的猜想是您的模型具有相似的行为，这就是您获得相同结果的原因。

于 2017-07-30T16:47:10.877 回答