TLDR; ответить.
Если автомат начинается с x==0 и перемещается по местоположениям без инвариантов, то автомат может задержать, скажем, 5 единицы времени, затем переместиться в другое местоположение с x==5, а затем снова задержать, скажем, 3.141 единицы времени, что перемещается x к значению 8.141 и так далее. Обратите внимание, что часы x могут получить произвольное реальное значение (отсюда мой произвольный выбор), задерживая и принимая переходы, что означает, что все эти возможности необходимо проанализировать. Uppaal фиксирует все эти возможные значения в виде ограничений (или их отсутствие в этом случае, когда нет инвариантов или охранников, симулятор может показать только x==y, потому что все часы синхронизированы).
Некоторый контекст.
В Uppaal реализованы синхронизированные автоматы с переменными часов, значения которых непрерывно изменяются со скоростью (производной по времени), равной 1.
Таким образом, если часы сбрасываются на 0, и автомат прибывает в местоположение без инвариантов (также не срочных и не зафиксированных), то часы могут свободно развиваться, поэтому могут иметь произвольное значение от 0 до infinity. Uppaal представляет такие оценки символически , используя ограничения (интервалы), упакованные в матрицы разностей (DBM). Если автомат берет переход, то Uppaal проанализирует все возможные переходы, удовлетворяющие ограничениям сразу. Например, если местоположение имеет инвариант x<=5, а ребро имеет охрану x>=2, то переход доступен, когда x находится где-то между 2 и 5, поэтому Uppaal примет символический переход с ограничениями 2<=x && x<=5, который фиксирует все эти возможные переходы одновременно. Это позволяет анализировать бесконечно много переходов в конечных структурах данных и за конечное время.
Некоторые распространенные случаи, которые могут запутать новичка.
Если в системе несколько автоматов, то ход времени анализируется глобально, то есть инвариант в одном автомате будет влиять на другие часы в других автоматах, потому что все часы синхронизированы через глобальное время .
Временные автоматы допускают в целых числах и инвариантах только целые числа, которые в принципе можно масштабировать для размещения моделей с рациональными числами. Uppaal также расширяет синхронизированные автоматы срочными, зафиксированными местоположениями, операторами выбора, широковещательной синхронизацией, целочисленными переменными, вызовами функций и т. Д., Которые все еще можно анализировать по той же теории синхронизированных автоматов , но делает моделирование более выразительным и лаконичным.
Вы можете прочитать больше в Tutorial на Uppaal, в разделе документации http://uppaal.org:
http://www.it.uu.se/research/group/darts/uppaal/documentation.shtml#tutorials