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

Question

我不知道如何在NuSMV声明全局常量，在某种程度上类似于

#define n 5 

在C。

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

Answer 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