問題タブ [nusmv]

私はこのコマンドを持つべきバッチファイルを作成しようとしています：

私が遭遇する問題はこれです：2行目が実行された後、NuSMV.exeはcmdで実行され、残りのコマンドはNuSMVを終了するまで実行されませんが、NuSMVでコマンド3〜8を実行したいと思います。.batファイルで何を変更する必要がありますか。ありがとう。

NuSMV でモデル チェック用の有効な CTL または LTL 式を作成しようとしています。

ゲーム内に変数があり、アクターがお互いを捕まえようとして走り回っています。変数は State_Of_Game : {Win,Lose,Playing}

そして、すべての開始状態から、ゲームは勝ったり負けたりする可能性があることを表現したいと思います。

では、これを CTL または LTL でどのように実装すればよいでしょうか?

AG (S_O_G = Win | S_O_G = Lose) のようなものを考えていましたが、すべての開始状態から見られるように実装する方法がわかりません。

NuSMV プログラムがあり、プログラム (ゲーム) が 5 タイム ステップ未満で勝てないことを CTL または LTL で指定する必要があります。またはより形式的: ゲームに勝つためには、少なくとも 5 つのタイム ステップが必要です。

私は明示的な時間変数を持っていないので、検証用に作成したくありません。すでに行われた移行の量を数える方法はありますか? 訪問した州の数、そのようなものですか？

現時点で私はこれを持っています：

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

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

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

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

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

NuSMV で信号機システムの実装を作成しようとしています。現在、NS/EW 赤、黄、緑の 6 つのブール値があります。ただし、将来の状態でそれぞれが常に true であると指定すると、false が返されます。誰かが私のコードにエラーを見つけたら、助けていただければ幸いです。ありがとう。

NuSMV ツールを使用して CTL が正しいかどうかを検証すると、混乱する問題に遭遇します。

私のモデルは

NuSMVコードは次のとおりです。

私のCTL式は次のとおりです。

1. "AG( A1 -> AX ( A [ B1 U ( D1 -> EX ( F1) ) ] ) )"
2. "AG( A1 -> AX ( A [ B1 U ( F1 -> EX ( C1) ) ] ) )"
3. "AG( A1 -> AX ( A [ M1 U ( F1 -> EX ( C1) ) ] ) )"

NuSMV は上記の 3 つの公式を検証し、すべてが真であることが判明しました。

では、私の質問は、なぜ式 2 と式 3 が真になるのかということです。

固定長ビット配列と比較して、16 ビットの符号付き整数変数を間隔 (-32768..32767) として表すと、パフォーマンスが大幅に低下するのはなぜですか?

前処理された NuSMV/NuXMV モデルを調べると、間隔タイプが列挙型に変換されていることがわかります。

ただし、BDD の統計には、関連する情報は表示されません。

コードを修正しようとしています。デッドロックと相互排除の問題を解決しましたが、promela (PML) にはモニターがないため、飢餓を回避する方法がわかりません。誰かが私を助けることができますか？前もって感謝します

NuSMV で単純なバブル ソートを FSM としてプログラムしようとしていますが、大きな問題に直面しています。配列の 2 つの要素間でスワップを実行しようとすると、配列でスワップを実行できません。プログラムが停止します。誰でもこれを解決できますか？どうもありがとう。