检查 SMV 中的 CTL 规范答案

【问题标题】：Check CTL specification in SMV检查 SMV 中的 CTL 规范
【发布时间】：2017-07-28 22:31:48
【问题描述】：

当我尝试在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

【问题讨论】：

如果可以的话，请让我们看看你的模型。

标签： model-checking ctl nusmv

【解决方案1】：

简短回答：

不，您的 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（或b）为FALSE，我们就确定地将其设置为TRUE，否则我们允许它任意更改。

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

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 保守地打印最少的必要状态，以达到违反属性的状态。在这种情况下，执行跟踪的 initial-state 已经违反了该属性，因为 下一个确定性转换 会导致 a 或 @ 987654328@ 是 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

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

【讨论】：

谢谢帕特里克。但是我发现即使我添加了INIT约束“INIT a = FALSE; INIT b = FALSE”。您的示例“EG (!a & !b)”中的 CTLSPEC 仍被评估为 FALSE。然后我将 CTLSPEC 更改为“！AG (a|b)”，它应该是等效的。结果被评估为真。因此，我怀疑 NuSMV (NuXMV) 在 CTLSPEC 中不支持 EG。
@YulinZhang 正确EG (!a & !b) 是TRUE 即使INIT a = FALSE & b = FALSE，因为只有一个下一个状态，它等于a = TRUE & b = TRUE，这违反了!a & !b，因此从初始状态!a & !b开始没有没有执行路径这样!a & !b 就永远存在。 EG (!a & !b) 的等效公式是 ! AF (a | b)。
你是对的。我在使用德摩根定律时犯了一些错误。谢谢。