NuSMV - AND 模型

Question

我正在尝试在 NuSMV 中编写以下模型

换句话说，只有当 x AND y 也处于 bad 状态时，z 才会变坏。这是我写的代码

MODULE singleton
    VAR state: {good, bad};
    INIT state = good
    TRANS (state = good) -> next(state) = bad
    TRANS (state = bad) -> next(state) = bad

MODULE effect(cond)
    VAR state: {good, bad};
    ASSIGN
    init(state) := good;
    next(state) := case
        (state = bad) : bad;
        (state = good & cond) : bad;
        (!cond) : good;
        TRUE : state;
        esac;

MODULE main 
    VAR x : singleton;
    VAR y : singleton;
    VAR z : effect((x.state = bad) & (y.state = bad));

但我只有这些可达状态

NuSMV > print_reachable_states -v
######################################################################
system diameter: 3
reachable states: 3 (2^1.58496) out of 8 (2^3)
  ------- State    1 ------
  x.state = good
  y.state = good
  z.state = good
  ------- State    2 ------
  x.state = bad
  y.state = bad
  z.state = bad
  ------- State    3 ------
  x.state = bad
  y.state = bad
  z.state = good
  -------------------------
######################################################################

如何修改我的代码以获得也

x.state = good
y.state = bad
z.state = good

x.state = bad
y.state = good
z.state = good

处于可达状态？

此外，我不确定我是否必须添加模型图片中打印的红色箭头：如果 x 和 y 处于错误状态，我希望它迟早也会变得错误。

非常感谢您的帮助！

Answer 1

各州

x.state = good
y.state = bad
z.state = good

x.state = bad
y.state = good
z.state = good

无法访问，因为main 的每个子模块同时执行其他子模块的转换，并且因为您强制为您的确定性转换>状态变量;也就是说，在您的模型中，x 和 y 同时将状态从 good 更改为 bad。此外，与您的漂亮图片相比，您的smv 代码不允许任何自循环，除了最终状态的自循环。

---

要修复你的模型，你只需要声明——如果x（或y）是good——你希望next(x)（或next(y)）是@ 987654333@ 或 bad，但不强制任何一个决定。 例如

MODULE singleton
VAR
  state: { good, bad };

ASSIGN
  init(state) := good;
  next(state) := case
      state = good : { good, bad };
      TRUE         : bad;
    esac;


MODULE effect(cond)
VAR
  state: { good, bad };

ASSIGN
  init(state) := good;
  next(state) := case
      (state = bad | cond) : bad;
      TRUE                 : state;
    esac;


MODULE main
VAR
    x : singleton;
    y : singleton;
    z : effect((x.state = bad) & (y.state = bad));

注意：我还简化了模块 effect 的规则，虽然这是不必要的。

您可以按如下方式测试模型：

nuXmv > reset; read_model -i test.smv ; go; print_reachable_states -v
######################################################################
system diameter: 3
reachable states: 5 (2^2.32193) out of 8 (2^3)
  ------- State    1 ------
  x.state = good
  y.state = bad
  z.state = good
  ------- State    2 ------
  x.state = good
  y.state = good
  z.state = good
  ------- State    3 ------
  x.state = bad
  y.state = good
  z.state = good
  ------- State    4 ------
  x.state = bad
  y.state = bad
  z.state = bad
  ------- State    5 ------
  x.state = bad
  y.state = bad
  z.state = good
  -------------------------
######################################################################

---

关于您的第二个问题，我提供给您的代码示例保证了您要验证的属性：

nuXmv > check_ltlspec -p "G ((x.state = bad & y.state = bad) -> F z.state = bad)"
-- specification  G ((x.state = bad & y.state = bad) ->  F z.state = bad)  is true

显然是这种情况，因为您图片中红边勾勒出的自环不存在。如果您考虑一下，该转换将允许至少执行一次 当前状态 保持等于

x.state = bad
y.state = bad
z.state = good

无限期，这将是您规范的反例。

---

编辑：

您也可以通过简单地编写以下代码来修复代码：

MODULE singleton
    VAR state: {good, bad};
    INIT state = good
    TRANS (state = bad) -> next(state) = bad

删除TRANS (state = good) -> next(state) = bad 行允许x 和y 在state = good 时任意更改，这意味着它们可以非确定性地保持good 或变为bad。这完全等同于我提供给您的代码，尽管乍一看不太清楚，因为它隐藏了 非确定性 而不是使其明确。