Как развиваются часы Uppaal? У меня есть две локации 1 и 2 без инварианта, часы сбрасываются на ноль (0) при переходе в локацию 1. На границе между локацией 1 и 2, как мне узнать значение часов в это время? (То есть значение часов между двумя точками перед точкой 2). Продолжают ли часы развиваться от локации 1 к локации 2 и далее или происходит автоматический сброс при входе в новую локацию?
Как развиваются часы Uppaal? У меня есть две локации 1 и 2 без инварианта. Что такое тактовое значение?
Ответы (1)
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 on Uppaal в разделе документации на http://uppaal.org: http://www.it.uu.se/research/group/darts/uppaal/documentation.shtml#tutorials
person
mariusm
schedule
08.05.2019
Большое спасибо. Это то же самое для местных часов? Я имею в виду часы, объявленные локально для процесса.
- person user993257; 08.05.2019
Да, со всеми часами обращаются одинаково. Просто локальные часы могут быть созданы вместе с новым процессом, и они имеют локальную область доступа (процессы не могут обновлять часы других процессов).
- person mariusm; 08.05.2019
Мое понимание часов как-то правильно основано на вашем объяснении. Но я все еще не получаю желаемого результата на моей модели.
- person user993257; 08.05.2019
Какова семантика местоположения без указанных часов в Уппаале?
- person user993257; 09.05.2019
@ user993257 что вы подразумеваете под без указанных часов? Если в местоположении нет инвариантов, то время может пройти (если нет другого процесса с инвариантом в его текущем местоположении).
- person mariusm; 09.05.2019
Спасибо @mariusm. Проблема в том, что у меня есть случай, когда нет инварианта, но время отказывается идти. Время не развивается. На ребре от местоположения 1 до 2 (без инварианта в обоих местоположениях) находится защита x==y, где x — часы, а y — целое число, которое было обновлено до 5 при входном переходе к местоположению 1, но это условие не выполнено. встретиться. Таким образом, приводит к тупику. Я ожидал, что время изменится, так что x в конечном итоге станет равным 5, и переход можно будет включить.
- person user993257; 10.05.2019
@user993257 user993257 вы, вероятно, смотрите на симулятор, если это так, выберите переход в тупик и проверьте ограничения часов. Я думаю, вы обнаружите, что взаимоблокировка происходит при передаче значения 5, т.е. е. переход разрешен только в 5, но процесс может задерживаться больше (нет инварианта), а через 5 единиц времени x›5 переход уже недоступен, следовательно, тупик.
- person mariusm; 12.05.2019
Спасибо @mariusm, очень правильно, все, хотя я не могу категорично сказать значение x, то, что я вижу как ограничение в точке тупика, равно x›0. каким образом я могу это решить? Спасибо
- person user993257; 12.05.2019
@ user993257 какие охранники на исходящих краях? Было бы лучше, если бы вы выложили скриншот симулятора.
- person mariusm; 12.05.2019
Я попытался вставить скриншот, но безуспешно. Я не делал этого раньше на этом форуме, так что я думаю, что делаю это неправильно.
- person user993257; 12.05.2019
Используйте gimp: захватите, затем скопируйте и вставьте в текст вопроса
- person mariusm; 12.05.2019
Не повезло при вставке скриншота
- person user993257; 12.05.2019
