如何在 NuSMV 中定义全局常量？答案

【问题标题】：How can I define global constants in NuSMV?如何在 NuSMV 中定义全局常量？
【发布时间】：2017-03-28 22:08:13
【问题描述】：

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

#define n 5

在C.

我如何在 NuSMV 中做到这一点？

【问题讨论】：

标签： formal-verification model-checking nusmv

【解决方案1】：

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

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

define_body :: identifier := simple_expr ;
             | define_body identifier := simple_expr ;
DEFINE 将:= 左侧的identifier 与右侧的表达式相关联。定义语句可以被认为是一个宏。每当在表达式中出现定义 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

【讨论】：