NuSMVでグローバル定数を定義するにはどうすればよいですか？

Question

私はCで

#define n 5 

に類似した方法で、NuSMVでグローバル定数を宣言するのか分かりません。

NuSMVでどうすればいいですか？

Answer 1

段落2.3.2NuSMV 2.6 Manualの（27ページ）によれば、説明をより簡潔にするために

、シンボルは共通の発現と関連することができ、を宣言紹介を定義そのようなシンボル。宣言のこの種のための構文は次のとおりです。

define_declaration :: DEFINE define_body 

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

が仲間右側の式と:=の左側のidentifierを定義します。 defineステートメントはマクロと見なすことができます。式でidentifierが定義されるたびに、identifierは、それが関連付けられている式に構文的に置き換えられます。関連する式は、identifierが宣言されているステートメント（）のコンテキストで常に評価されます（コンテキストの説明については、2.3.16 [コンテキスト]、36ページを参照してください）。定義されたシンボルへの前方参照は許可されますが、循環定義は行われず、エラーが発生します。定義済みのシンボルと変数の違いは ですが、変数は静的に型付けされていますが、定義はそうではありません。

---

したがって、この作業をする必要があります：

DEFINE n := 5 ; 

それはいくつかのコンテキストに属している必要がありますので、あなただけ、1つのモジュール以内にこの定義を置くことができます。

ただし、すべてグローバル定義のコンテナとして機能する1つの特別なモジュールを持つことによってにグローバルスコープを「シミュレート」することができます。例えば、。：

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