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

Question

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

#define n 5

在C中。

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

Answer 1

根据2.3.2段( NuSMV 2.6手册第27页)

为了使描述更加简洁，符号可以与通用表达式相关联，定义声明引入了这样的符号。这种声明的语法是： define_declaration :：定义define_body define_body :：标识符:= simple_expr； 定义将:=左侧的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