formal-verification - 如何在 NuSMV 中定义全局常量？

Question

我不知道如何在 NuSMV 中声明全局常量，方式类似于

#define n 5

在C.

我怎样才能在 NuSMV 中做到这一点？

Answer 1

根据NuSMV 2.6 手册的第2.3.2段（第 27 页）：

为了使描述更简洁，一个符号可以与一个通用表达式相关联，一个DEFINE声明引入了这样一个符号。这种声明的语法是：

define_declaration :: DEFINE define_body

define_body :: identifier := simple_expr ;
             | define_body identifier := simple_expr ;

DEFINEidentifier将左侧的:=an 与右侧的表达式相关联。定义语句可以被认为是一个宏。每当identifier在表达式中出现定义时，都会在identifier语法上将其替换为与之关联的表达式。关联的表达式总是在声明 的语句的上下文中求值（有关上下文的identifier解释，请参见第 2.3.16 节 [上下文]，第 36 页）。允许对已定义符号的前向引用，但不允许循环定义，并且会导致错误。定义的符号和变量之间的区别在于，虽然变量是静态类型的，但定义不是。

---

因此，这应该有效：

DEFINE n := 5 ;

您只能将此定义放在一个模块中，因为它必须属于某个上下文。

但是，您可以通过让一个特殊模块充当所有全局定义的容器来“模拟”全局范围。例如：

MODULE global
DEFINE
  n := 5;

MODULE pippo(global)
VAR
  pluto : {0, 1, 2, 3, 4, 5};
ASSIGN
  init(pluto) := global.n;

MODULE main()
VAR
  global : global();
  pippo  : pippo(global);

您可以像这样测试示例：

~$ NuSMV -int
NuSMV > reset; read_model -i example.smv; go; pick_state -i -v

***************  AVAILABLE STATES  *************

================= State =================
0) -------------------------
  global.n = 5
  pippo.pluto = 5