NuSMV -和模型

Question

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

​

​

换句话说，只有当x和y处于坏状态时，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 (resp )。y)是good--你想要next(x)。( 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));

注意：I也简化了模块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。这完全等同于我提供给您的代码，尽管乍一看不太清楚，因为它隐藏了不确定的内容，而不是将其显式化。