model-checking - 如何在 NuSMV 中以易于处理的数据结构返回反例？

Question

在我的 NuSMV 脚本中，我试图捕捉 LTLSPEC 的反例的踪迹，但我设法得到它的唯一方法是通过 shell。

是否有可能在易于处理的数据结构中捕获该跟踪？我读过可以以 XML 格式返回，但不幸的是我没能做到。

一定有办法的。