UPPAAL: Инварианты нарушены, но никто не был явно установлен - как устранить тупик?
Я хотел бы узнать больше о Timed Automata для проверки систем в реальном времени. В настоящее время я пытаюсь ознакомиться с инструментом UPPAAL.
Я нарисовал несколько простых графиков и добавил разные свойства. Предполагается, что вся модель представляет собой систему производственных ячеек, в которой разные механические узлы передают блок друг другу.
Я смоделировал блок (BlockCycle), 2 механических блока (Feeder, FeederBelt) и 2 датчика, которые определяют прибытие блока.
Хотя я думал, что моя система будет иметь смысл, она зашла в тупик:
Целевые состояния этого перехода нарушают инварианты. Это не проблема, если вы хотели, чтобы ваша модель вела себя так.
(Нет, я не.;P)
Кажется, я не могу найти причину тупика. Инструмент указывает мне на модель BlockCycle, но я не указал там никакого инварианта. Фактически, все требования перехода выполнены, поэтому переход (от Pos7 к Pos8) обязательно должен быть выполнен.
Ниже вы увидите, как система развивается и, наконец, застревает (появляется сообщение об ошибке).
Метки:
- зеленый: проверка свойства (например, FB_Running означает FB_Running == true)
- темно-синий: обновление / назначение недвижимости
- темно-красный: места (например, Pos7 или Pos8)
Модель BlockCycle с соответствующим переходом:
Мой вопрос: почему система заходит в тупик, хотя есть еще транзакции, которые могут быть приняты.
Edit1: Когда я удаляю свойство invariant местоположения Sensor7 Active (называемое BlockAtPos [7]), тупик устраняется. Таким образом, я предполагаю, что поскольку нет синхронизации между Sensor7 и BlockCycle для последнего перехода перед его блокировкой, это может привести к противоречию (BlockAtPos [7] станет ложным, в то время как у датчика еще нет возможности принять переход InActive) и, таким образом, нарушая инвариант.
Примечание: Вы можете найти мой код / файл UPPAAL здесь: pcs.xml.