Сгенерировать случайное число в Уппаале

Мой вопрос: Могу ли я сгенерировать случайное число в Uppaal?

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

например: двойной [7.25,18.3]

Я нашел этот вопрос, в котором говорилось об одном и том же. Я пробовал. Однако я получил эту ошибку: непредвиденная синтаксическая ошибка T_SELECT.

Это не работает. Я новичок в мире Uppaal, я был бы признателен за любую помощь, которую вы можете мне оказать.

С уважением,


random numbers uppaal
person Cesar Nieto Coria    schedule 25.06.2015    source источник
comment
Select работает только с целочисленными диапазонами. Для типов double есть функция random(), но она работает только с алгоритмами SMC, включенными в версии 4.1.   -  person mariusm    schedule 31.05.2016

Ответы (1)


arrow_upward
3
arrow_downward

Это распространенный и неправильно понимаемый вопрос в Уппаале.

Простой ответ:

    double val; // declaration
    val = random(18.3-7.25)+7.25; // use in update, works in SMC (Uppaal v4.1)

Подробный ответ:

  1. Uppaal поддерживает как символический, так и статистический анализ, а подходы и возможности радикально различаются. Поэтому сначала нужно решить, какой анализ необходим. Обычно начинают с простого символического анализа, а затем дополняют стохастическими признаками, иногда стохастическое поведение также необходимо проверять символически.

  2. В символьном анализе (запросы A[], A<>, E<>, E[] и т.д.) случайный является синонимом недетерминированного, т.е. если модель содержит какое-то "случайное" поведение, то проверка должна проверять их все так или иначе. Поэтому такое поведение моделируется как недетерминированный выбор между ребрами. Легко настроить набор ребер в диапазоне целых чисел, используя оператор select на ребре, где объявлена ​​временная переменная, и ее значение может использоваться в охранах, синхронизации и обновлении. Символьный анализ поддерживает только целочисленные типы данных (без типов с плавающей запятой, таких как double) и непрерывные диапазоны по часам (заданные ограничениями в охранах и инвариантах).

  3. Статистический анализ (путем моделирования Монте-Карло, запросов типа Pr[...](<> p), E[...](max: var), simulate и т. д.) поддерживает double типов и функций с плавающей запятой, таких как sin, cos, sqrt, random(MAX) (равномерное распределение по [0, MAX)), random_normal(mean, dev) и т. д. в дополнение к int типам данных . Переменные часов также можно рассматривать как тип с плавающей запятой, за исключением того, что их производная по умолчанию установлена ​​в 1 (может быть изменена в инвариантах, которые допускают ОДУ - обыкновенные дифференциальные уравнения).

  4. Можно создавать модели с операциями с плавающей запятой (включая random) и по-прежнему применять символьный анализ при условии, что переменные с плавающей запятой не влияют/не ограничивают поведение модели и действуют просто как функция стоимости в пространстве состояний. Вот систематические правила для достижения этого:

    а) часы, используемые в ODE, должны быть объявлены типа hybrid clock.

    б) Переменные типа hybrid clock и double не могут появляться в защитных и инвариантных ограничениях. В инварианте разрешены только ОДУ над hybrid clocks.

person mariusm    schedule 14.06.2016