1

I'm trying to write the following model in NuSMV

enter image description here

In other words, z becomes bad only when x AND y are in the state bad too. This is the code I've written

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));

But I got only these reachable states

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
  -------------------------
######################################################################

How can I modify my code to get also

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

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

in the reachable states?

In addition, I'm not sure if I've to add or not that red arrow printed in the model picture: if x and y are in state bad, I want that for sure sooner or later also z becomes bad.

Thank you so much for helping!

4

1 回答 1

2

美国

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

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

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

要修复您的模型，您只需要声明 --in case x(resp. y) is good-- 您希望next(x)(resp. next(y)) 成为goodor 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));

注意：我还简化了 module 的规则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。这完全等同于我提供给您的代码，尽管乍一看不太清楚，因为它隐藏了非确定性而不是使其明确。

于 2017-09-25T17:25:52.783 回答