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(或实际计算状态持续时间的所有可能组合，并确保没有任何组合超过SPEC中的e.I.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

我该怎么解决这个问题？要么以另一种方式声明持续时间，要么更改其他内容？

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