#model-checking #nusmv
Вопрос:
В моем сценарии NuSMV я пытаюсь уловить след контрпримера LTLSPEC, но единственный способ, которым мне удалось его получить, — это пройти через оболочку.
Есть ли какая-либо возможность уловить эту трассировку в простой в обработке структуре данных? Я читал, что это можно вернуть в формате XML, но, к сожалению, мне это не удалось.
Должен быть какой-то способ.