我在 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 之间的任何值。
是的，它是正确的。
该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 constant和union操作者可以被用来创建一个的表达set类型，以及唯一的in，case，(• ? • : •)和赋值表达式可具有的imediate操作数set类型。每种
set类型在其他类型中都有一个对应物。特别是，
boolean set类型的对应物是boolean，
integer set类型的对应物是integer，
symbolic set类型的对应物是symbolic enum，
integers-and-symbolic set类型的对应物是integers-and-symbolic enum。某些类型，例如 unsigned
word[•]并且signed word[•]没有set类型对应物。
和
范围常数
A
range constant指定一组连续的整数。例如，一个恒定的-1..5指示组数字-1，0，1，2，3，4和5。的其他示例range constant可以是1..10、-10..-10、1..300。的语法规则range constant如下：range_constant :: integer_number .. integer_number附加的约束是第一个整数必须小于或等于第二个整数。a 的类型
range constant是integer set。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句