NuSMV застрял в тривиальном тупике

Question

Предположим, я кодирую модель в NuSMV, которая запускается в состоянии S1. Я хочу проверить состояние в этой модели проверки, достигаю ли я в конечном итоге состояние S70 при любых обстоятельствах. Теперь представьте модель NuSMV, которую я кодировал, как показано ниже:

Сверху очевидно, что в конечном итоге S70 будет достигнут, но это может занять гораздо более 70 временных шагов. Зачем? Потому что вы можете перейти к S2, затем к S3, а затем вместо перехода к S4 снова вернуться к S2, и этот шаблон повторяется, скажем, 100 раз. Такие возможности учитываются программным обеспечением NuSMV также для подтверждения того, что S70 определенно будет достигнут.

Проблема в том, что NuSMV сказал, что S70 не будет достигнут, и сгенерировал контрпример, а именно: -

S1->S2->S3->S2

Так что контрпример - это только эти 4 шага. Но я поражен тем, что NuSMV не может понять, что этот тупик со временем будет разрешен. Почему я получаю неинтуитивный результат?

Может быть шанс, что автоматы, которые я показываю на рисунке, - это то, что я хочу, чтобы мой код NuSMV представлял, но я неправильно кодировал одну или две строки, но я так не думаю. В противном случае NuSMV может понять, что он может перейти от S2 к S3. Если он может понять, что можно перейти от S2 к S3, тогда зачем прекращать приведенный выше контрпример на S2?

Может кто-нибудь объяснить?

Answer 1

Но я поражен, что NuSMV не может понять, что этот тупик со временем будет разрешен

Я не уверен, что эта ситуация соответствует определению "тупика" . В любом случае, NuSMV правильно указывает, что существует выполнение, в котором программа никогда не достигнет состояния S70.

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

S1->S2->S3->S2

состоит из двух частей:

• a prefix part: последовательность состояний, начиная с начального состояния, которое достигает части бесконечного цикла . В данном случае это просто S1.
• a loop part: самоподходящая последовательность состояний, которую легко идентифицировать, поскольку она заканчивается в том же состоянии, в котором она запускается. В этом случае это S2 -> S3 -> S2

Это действительный бесконечный путь выполнения вашего автомата, означающий, что программа вправе всегда переходить с S3 на S2 и никогда не переходить на S4, и поскольку она никогда не трогает S70 это также контрпример для вашей собственности.

---

Я не уверен, как я могу помочь вам в вашей проблеме, поскольку вы не указали, используете ли вы LTL или CTL , а также не дали никакой дополнительной информации о твоя модель Может быть необходимо изменить вашу модель, ваши свойства или оба. Если можно, я бы посоветовал вам взглянуть на слайды во второй части этого курса по NuSMV / nuXmv, чтобы лучше понять инструмент.

EDIT

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

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

 (! (G (F S2))) -> (F S70)

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