Uppaal Проверка не работает, как задумано

Question

Итак, я пытаюсь выполнить очень простую проверку моей модели, однако я получаю сообщение о том, что свойство не удовлетворено.

Я пытаюсь убедиться, что в моей модели, если когда-нибудь Person (0) уйдет In, в конце концов Person (0) придет Out.

Персона (0). В -> Персона (0) .Вне

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

Есть ли проблема с синтаксисом, который я использую, или UPPAAL имеет известную проблему с такого рода проверками?

Answer 1

Вы можете загрузить контрпример в симулятор, выбрав Параметры -> Диагностический след -> Некоторые.Для этого конкретного запроса (приводит к свойству) общая проблема заключается в том, что система может оставаться в каком-то месте навсегда (или проходить через несколько переходов), что в основном препятствует достижению цели.Часть цикла примера счетчика выделена красным.Может быть трудно наблюдать / понимать, если в цикле только одно место.Симулятор по-прежнему позволяет пользователю добавлять переходы к трассе, что является законным и может создать впечатление, что система в конечном итоге достигнет цели, но суть трассы в том, что есть способ, которым система не достигнет, и это путем остановки (и остановка также разрешена, если нет инвариантов).

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