Как узнать всевозможные встречные примеры Nusmv
У меня есть модель в NuSMV и после проверки спецификации ltl NuSMV дает мне контрольный пример Можно ли найти все пути, которые содержат контрольный пример, не один из них?
2 ответа
Вы можете использовать свой контрпример для уточнения своей спецификации LTL, а затем снова использовать уточненную спецификацию для проверки моделей. повторяйте это, пока NuSMV не найдет больше контрпримеров, но в некоторых случаях это может никогда не закончиться.
По сути, это называется CEGAR - контр-уточнение управляемой контрпримером, за исключением того, что это не модель абстракции, а спецификация уточняется на каждой итерации.
Вообще говоря, это невозможно, поскольку системы разумного размера способны производить бесконечно много таких контрпримеров. Представьте, что в вашей системе есть "плохой цикл", который можно вводить произвольно часто или после конечной, но произвольной задержки: каждая такая задержка приведет к новому контрпримеру.