1

我在 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 可以假设其域中的任何随机值。逻辑的这个“否则”部分是我怀疑的。我是否正确编码？y 和 z 是变量，其代码未在此处显示。为 y 和 z 假设一些东西。

或者我应该写：

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

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

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

4

1 回答 1

0

是的，这是正确的。

integer set {0, 1, 2, 3, 4, 5}也可以写成，根据0 .. 5以下文档：

2.1.6 集合类型

集合类型用于标识表示一组值的表达式。有四种set类型：boolean set, integer set, symbolic set, integers-and-symbolic set。这些set 类型可以以非常有限的方式使用。特别是，变量不能是set类型。只有range constantandunion 运算符可以用来创建一个set类型的表达式，并且只有 in, case,(• ? • : •)和赋值表达式可以有一个set类型的直接操作数。

每种set类型都有其他类型的对应物。尤其是，

  • 类型的对应物boolean set是boolean,

  • 类型的对应物integer set是integer,

  • 类型的对应物symbolic set是symbolic enum,

  • 类型的对应物integers-and-symbolic set是integers-and-symbolic enum.

某些类型，例如 unsignedword[•]并且signed word[•]没有 set对应的类型。

和

范围常数

Arange constant指定一组连续整数。例如，常数 表示-1..5一组数字-1、0、1、2、3和。的其他示例可以是, , 。的语法规则如下：45range constant1..10-10..-101..300range constant

range_constant
    :: integer_number .. integer_number

有一个附加约束，即第一个整数必须小于或等于第二个整数。a 的类型 range constant是integer set。

于 2018-08-22T07:03:14.530 回答