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

Предположим, я кодирую модель в 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?

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


logic automata nusmv
person user_1_1_1    schedule 05.09.2018    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

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

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

S1->S2->S3->S2

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

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

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

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

ИЗМЕНИТЬ

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

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

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

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

person Patrick Trentin    schedule 06.09.2018
comment
Я использую только свойства LTL. - person user_1_1_1; 07.09.2018
comment
@ userNuSMV1_1, если встречный пример, найденный NuSMV, не имеет причин для появления в реальном приложении, которое вы моделируете, вы можете рассмотреть возможность использования некоторого условия справедливости, чтобы исключить такое выполнение. - person Patrick Trentin; 07.09.2018
comment
Не могли бы вы предложить, как написать условия fariness, чтобы исключить условия, подобные приведенным выше, при которых продолжается цикл. - person user_1_1_1; 07.09.2018
comment
@user_1_1_1 user_1_1_1 да, я могу отредактировать свой ответ, чтобы включить эту часть. Но я не могу получить доступ к компьютеру до завтра. Если вам нужен предварительный просмотр, вы можете прочитать слайды, которые я уже связал. - person Patrick Trentin; 07.09.2018