私はプログラムの修正/合成プロジェクトに取り組んでいます。私のタスクは、エラー トレース (反例) を取得し、それを完全な状態空間で見つけて、その場所でモデルを修復することです。これを NuSMV 拡張機能として実装したいと考えています。
NuSMV をデバッグして、そのソース コードを理解し、調査しています。ここまでで、BDD FSM を作成する方法を見つけました (compile.c の 520 行目)。状態空間へのプログラムによるアクセスを取得し、モデルに対して修正作業を実行するために、bdd をトラバースする方法を見つけようとしています。NuSMV が bdd fsm を介してプロパティを検証するために使用する再帰的な探索関数をまだ理解できていません。
ドットなどのツールを使用して視覚化できるように、bdd 構造をトラバースする方法を知りたいです。また、そのようなまたは類似のビジュアライゼーションがすでに作成されているかどうかも知りたいです (検索しましたが、空になります)。第二に、私が取り上げた方向が正しいかどうか、または特定のモデルの完全な状態空間を取得するためのより良い方法があるかどうかを確認し、特に得られた反例に関して、それを調査したいと思いますNuSMV を介して。