1

我是 NuSMV 的新手。我正在尝试定义一个模块，其中每个状态都有一个持续时间变量，其范围可以从 0 到指定范围。

MODULE state(inc, bound)
 VAR 
   duration : 0..bound;
 
 ASSIGN 
  init(duration) := 0;
  next(duration) := inc ? (duration + 1) mod (bound+1) : duration ;

 DEFINE limit := duration = bound;

但是，这会产生语法错误：A variable is expected in left-hand-side of assignment: init(duration) := 0. 我可以通过声明duration来解决这个问题duration : 0..1+bound。

在我的主模块中，我希望计算运行我的模型的总持续时间（或实际计算状态持续时间的所有可能组合，并确保没有组合超过规范中的 ei 3），并确保该变量不超过特定限制.

这是我的主要模块：

MODULE main
 VAR 
  s0 : state(TRUE, 0);
  s1 : state(s0.limit, 0);
  s2 : state(s1.limit, 3);
  state : {s0, s1, s2};

 DEFINE
  max_duration := s0.bound + s1.bound + s2.bound;

 VAR
  total_duration : 0..max_duration;

 ASSIGN
  init(state) := s0;

  next(state) := 
    case
      state = s0 : s1;
      state = s1 : s2;
      state = s2 : s2;
    esac;

  total_duration := s0.duration + s1.duration + s2.duration;

SPEC
  AG (state = s2 -> AF total_duration <= 3);

我的问题是：当我运行模型时，NuSMV 不断添加到total_duration变量中，因此失败并显示消息“ line 39: cannot assign value 5 to variable total_duration”。这是由于 的声明duration : 0..1+bound，因为在 s0.duration = 0、s1.duration = 0 和 s2.duration = 3 的特定示例中，它将尝试将 1 + 1 + 4 添加到total_duration，因为那是状态的绑定+1。

但是，如果我检查跟踪，total_duration 不会超过 3。我检查了以下规格：

-- specification AG total_duration < 4  is true

-- specification  F total_duration = 4  is false
-- specification EF total_duration >= 4  is false

我怎样才能解决这个问题？通过以其他方式声明持续时间或更改其他任何内容？

4

1 回答 1

2

该软件做了一些非常简单的事情。它获取每个加数的域，并检查结果变量是否能够保存每个可能的值组合的结果。在这种情况下：

  • 的域s0.duration是0..1
  • 的域s1.duration是0..1
  • 的域s2.duration是0..4

因此，原则上，最大值total_duration可能是6，因此它的域应该是0..6。所以：

DEFINE
  max_duration := s0.bound + s1.bound + s2.bound + 3

您可能希望NuSMV使用以下选项运行：

-keep_single_value_vars
  Does not convert variables that have only one
  single possible value into constant DEFINEs

这样，您将能够运行模型而无需添加+1到bound.

于 2020-11-27T22:34:53.907 回答