NuSMV：使用参数初始化范围常数

Question

我是 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.

来解决此问题

在我的主模块中，我希望计算 total_duration（或者实际计算状态持续时间的所有可能组合，并确保没有组合超过 e.i.3，如 SPEC 中所示）运行调整我的模型并确保变量不超过特定限制。

这是我的主要模块：

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

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

Answer 1

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

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 的域中。

NuSMV：使用参数初始化范围常数

NuSMV: Initialising range constant with parameter

model-checking

nusmv