問題タブ [nusmv]

NuSMV Web サイトからファイルをダウンロードしましたが、システムで実際にアプリケーションを実行できません。任意のリードをいただければ幸いです。

ファイルにはフォルダーが含まれています-bin、lib、share、include

私はプログラムの修正/合成プロジェクトに取り組んでいます。私のタスクは、エラー トレース (反例) を取得し、それを完全な状態空間で見つけて、その場所でモデルを修復することです。これを NuSMV 拡張機能として実装したいと考えています。

NuSMV をデバッグして、そのソース コードを理解し、調査しています。ここまでで、BDD FSM を作成する方法を見つけました (compile.c の 520 行目)。状態空間へのプログラムによるアクセスを取得し、モデルに対して修正作業を実行するために、bdd をトラバースする方法を見つけようとしています。NuSMV が bdd fsm を介してプロパティを検証するために使用する再帰的な探索関数をまだ理解できていません。

ドットなどのツールを使用して視覚化できるように、bdd 構造をトラバースする方法を知りたいです。また、そのようなまたは類似のビジュアライゼーションがすでに作成されているかどうかも知りたいです (検索しましたが、空になります)。第二に、私が取り上げた方向が正しいかどうか、または特定のモデルの完全な状態空間を取得するためのより良い方法があるかどうかを確認し、特に得られた反例に関して、それを調査したいと思いますNuSMV を介して。

NuSMVなどの最新のモデル チェッカーの最大状態空間サイズのおおよそのサイズはどれくらいですか。正確な数値は必要ありませんが、実行時間が許容できる場合 (数週間など) の状態サイズの値は必要ありません。

その限界を引き上げるために、シンボリック モデル チェック以外にどのような改善が行われているのでしょうか?