2

現在、LTL および CTL モデル チェック用の NuSMV を学習しています。

私はコーディング作業に notepad++ を使用しています (主に Python で)。notepad++ を使用して Python スクリプト (.py ファイル) を実行できることを知っています。

私は NuSMV が初めてで、メモ帳 ++ で .smv スクリプトを実行する方法があるかどうか疑問に思っています。

実行する予定の .smv コードの例を次に示します。

MODULE main
 VAR
  variable : boolean;
 ASSIGN
  init(variable) := true;
  next(variable) := !variable;
 LTLSPEC
  G (variable & X !variable)
 CTLSPEC
  EF (!variable & AX variable)

ただし、NuSMV インタラクティブ シェルを使用して上記の SMV スクリプトを実行することも困難です。上記のスクリプト名が test.smv であるとします。NuSMV インタラクティブ シェルを使用してどのように実行すればよいですか?

4

1 に答える 1

1

コードを実行するコマンド ラインを理解できる場合、解決策は次のとおりです。

  1. NPPExec プラグインをインストールする
  2. 実行したいコマンドラインを見つけてテストする
  3. N++ では、F6NPPExec プラグイン メニューから同等のメニュー項目を押すか使用します。
  4. 必要なコマンドラインを入力してください
  5. コマンドラインのファイル名をトークンで置き換えます"$(FULL_CURRENT_PATH)"-N++は現在のファイルのファイル名をここに置きます
  6. [オプション] [保存... ] ボタンを押して、コマンドを保存します
  7. OKボタンを押してコマンドを実行します
  8. 同じコマンドを繰り返し実行するには、押すだけですCtrl+F6

コマンド出力をコンソールに表示するにCtrl+`は、(1234567890 の左のキー) を押します。

NuSMV はコマンド ラインからの起動をサポートしており、ドキュメントの第 4 章にある多くのコマンド ライン オプションがあります (現在のバージョン)。ただし、それでも要件を満たせず、コマンド ラインからコードを実行する方法がない場合は、カスタム プログラム ソリューションを検討する必要があるかもしれません (十分な時間とスキルがある場合) - 独自の N++ プラグインを作成することを検討してください。または、API を使用して必要なすべての NuSMV メソッドを呼び出す、コマンド ラインから制御可能な小さなツールを作成します。多分これはPythonでも実行できます。次に、NPPExec からツールを呼び出すだけです。

于 2014-04-04T11:50:01.597 に答える