Я хотел бы знать, есть ли способ генерировать различные возможные контрпримеры для данной формулы LTL в NuSMV.Если нам нужно сгенерировать контрпример для формулы LTL, он сгенерирует ее для нас.Но тот, что генерируется NuSMV, может быть не самым захватывающим или проницательным, потому что могут быть другие контрпримеры к той же формуле LTL.
Можете ли вы предложить несколько общих способов попросить NuSMV представить какой-то другой контрпример, чем тот, который он создал?
Один из способов - изменить саму формулу LTL, чтобы нам был интересен контрпример, созданный NuSMV за один прием.Но я считаю, что это слишком много фальсификации системы, чтобы получить желаемый результат.
Плюс нужно заранее знать интересный результат.Но если я уже знаю интересный контрпример, зачем мне просить NuSMV подтвердить это мне?И зачем тогда проходить хлопоты по созданию выражения LTL, которое даст желаемый контрпример?Я хочу, чтобы NuSMV генерировал другие интересные контрпримеры, о которых я не задумывался, тем самым добавляя ценность.
И если это невозможно в NuSMV, можете ли вы предложить какой-либо другой инструмент проверки модели LTL, где это возможно?