Как определить глобальные константы в NuSMV?

Согласно параграфу 2.3.2 (стр. 27) документа Руководство NuSMV 2.6:

Чтобы сделать описания более краткими, символ может быть связан с общим выражением, и объявление 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