создание правильного выражения CTL или LTL (в NuSMV)

Question

Я пытаюсь создать допустимое выражение CTL или LTL для проверки модели в NuSMV.

У меня есть переменная в игре, с участием актеров, которые пытаются поймать друг друга. Переменная is, State_Of_Game: {Win, Lose, Playing}

и я хочу выразить, что из каждого начального состояния игра может быть как выиграна, так и проиграна.

Итак, как бы реализовать это в CTL или LTL?

Я думал что-то вроде AG (S_O_G = Win | S_O_G = Lose), но не знаю, как реализовать это, как видно из каждого начального состояния.

Answer 1

Я не знаком с обозначениями SMV, поэтому я предполагаю, что об этом, но ключевые моменты:

1. Чтобы избежать количественной оценки по всем состояниям снаружи: вы не хотите скажем, что все игры можно выиграть или проиграть, но только стартовая игра. Так что есть формула в исходном состоянии, без внешней модальности

2. Чтобы использовать конъюнкцию, а не дизъюнкции: вы хотите, чтобы утверждать, как winnability и losability

3. Вам необходимо отдельные условия упаковочных каждые из ветвей: winnability , неприемлемость является экзистенциальным утверждением, говорящим, что можно достичь условия.

Я думаю, что формула вам нужно, это: (EG SOG = Win) & (EG SOG = Lose) в корне, что может означать, в чем-то вроде инициализации/запуска пункта или утверждений в имени корень пункт. Если у SMV нет мода EG, вы можете перевести в просто AG с использованием эквивалентности EG p =! (AG! P), так как эти два являются двойниками Де Моргана.