为 NuSMV 中的变量分配随机值

Question

我在 NuSMV 中有以下代码。

MODULE main
VAR
   x : 0..5

所以x是一个可以取整数值0,1,2,3,4,5的变量。接下来，我对其进行初始化并制定其转换规则。

ASSIGN
    init(x):=1;
    next(x) := case
         y=1 & z=23: 4;
         TRUE: 0..5;
    esac;

上面应该说的是 x 最初是 1。然后如果 y=1 且 z=23，x 变为 4，否则 x 可以从其域中取任何随机值。这 'otherwise' 部分逻辑是我所怀疑的。我是否正确编码？ y 和 z 是其代码未在此处显示的变量。假设 y 和 z。

或者我应该写成：

TRUE: {0,1,2,3,4,5};

因为我从 this 文档的第 4 页确定上述内容是正确的。

但这对于非常大的域来说是不可行的。假设 x 可以取 0 到 293 之间的任意值。

Answer 1

是的，没错。

integer set{0, 1, 2, 3, 4, 5}也可以写成0 .. 5, 根据以下 documentation:

2.1.6 Set Types

set types are used to identify expressions representing a set of values. There are four set types: boolean set, integer set, symbolic set, integers-and-symbolic set. The set types can be used in a very limited number of ways. In particular, a variable cannot be of a set type. Only range constant and union operator can be used to create an expression of a set type, and only in, case, (• ? • : •) and assignment expressions can have imediate operands of a set type.

Every set type has a counterpart among other types. In particular,

the counterpart of a boolean set type is boolean,

the counterpart of a integer set type is integer,

the counterpart of a symbolic set type is symbolic enum,

the counterpart of a integers-and-symbolic set type is integers-and-symbolic enum.

Some types such as unsigned word[•] and signed word[•] do not have a set type counterpart.

和

Range Constant

A range constant specifies a set of consecutive integer numbers. For example, a constant -1..5 indicates the set of numbers -1, 0, 1, 2, 3, 4 and 5. Other examples of range constant can be 1..10, -10..-10, 1..300. The syntactic rule of the range constant is the following:
range_constant
    :: integer_number .. integer_number
with an additional constraint that the first integer number must be less than or equal to the second integer number. The type of a range constant is integer set.

为 NuSMV 中的变量分配随机值

Assign random value to variables in NuSMV

nusmv