Генерация случайного числа в Уппале

Question

У меня вопрос: можно ли сгенерировать случайное число в Уппале?

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

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

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

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

С Уважением,

Answer 1

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

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

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

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

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

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

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

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

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

   б) гибридные часы и переменные двойного типа не могут появляться в защитных и инвариантных ограничениях. Только ОДУ разрешены через гибридные часы в инварианте.