NuSMV

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 处于不良状态，我希望 z 迟早会变成不好。

非常感谢您的帮助！

Answer 1

各州

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

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

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

要修复您的模型，您只需要说明——如果 x（相应的 y）是 good——您想要 next(x)（ resp. next(y)) 为 good 或 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。这完全等同于我提供给您的代码，尽管乍一看不太清楚，因为它隐藏了 非确定性 而不是使其显式化。

NuSMV - 和模型

NuSMV - AND model

model-checking