model-checking - NuSMV で扱いやすいデータ構造で反例を返すにはどうすればよいですか?

Question

私の NuSMV スクリプトでは、LTLSPEC の反例のトレースを取得しようとしていますが、取得できた唯一の方法は、シェルを使用することでした。

扱いやすいデータ構造でその痕跡を捉える可能性はありますか? XML 形式で返される可能性があることを読みましたが、残念ながらできませんでした。

方法があるはずです。