Описание тега uppaal
Uppaal - это интегрированная инструментальная среда для моделирования, валидации и проверки систем реального времени, смоделированных как сети временных автоматов, расширенных типами данных (ограниченные целые числа, массивы и т. Д.).
2
ответа
Установить реализацию в UPPAAL
У меня есть модель, в которой процесс должен выбрать элемент s случайно из набора S, Выбор части является одной операцией. Единственная похожая структура данных, которую я знаю в UPPAAL, это массивы. Существует ли заданная структура данных в UPPAAL?…
20 май '14 в 05:43
1
ответ
Неограниченная задержка, но нет положительного показателя
Я создал эту спецификацию UPPAAL: https://pastebin.com/v4AkYUuy Но при выполнении запроса: simulate 100 [<=500] { time } Я получаю ошибку: Location Person.Rijssen has unbounded delay but no positive rate. Я искал несколько часов, но у UPPAAL нет …
11 ноя '18 в 10:09
1
ответ
UPPAAL тупик неясен
Я использую UPPAAL и пытаюсь смоделировать обувную фабрику, где 5 систем работают паралельно. Я могу написать об этом более подробно, если кому-то это нужно, но я не хочу тратить время на описание модели. Итак, прямо к проблеме: UPPAAL тупиковое сос…
26 мар '18 в 16:51
1
ответ
UPPAAL: что заставило часы перестать работать
В настоящее время я использую симулятор UPPAAL. Мой симулятор перестает запускать код после определенного момента. Этот момент варьируется в зависимости от декларации, которую я предоставляю. Но я хотел бы знать, вообще, когда часы перестают работат…
24 фев '14 в 05:08
0
ответов
Уппал: оценка вероятности на примере железнодорожных ворот
Я использую пример Train Gate и хочу запустить свойство проверки Pr[<=100] (<> Train(0).Cross) Сказать, какова вероятность пересечения поезда (0) в 100-кратных единицах . Я добавил часы в безопасное состояние, как показано в прикрепленном файле. Зап…
04 сен '18 в 08:57
1
ответ
Ошибка проверки UPPAAL - значение индекса находится вне диапазона
Я использую Uppaal для проверки системы. Симуляция работает отлично, но когда я проверяю, используя это свойство A[] not deadlock это дает мне следующую ошибку: _The successors of this state are not well defined. Index value 3 is out of range. Array…
31 авг '18 в 05:33
1
ответ
Как вернуть массив в UPPAAL?
Я пытаюсь вернуть целочисленный массив в функции UPPAAL. Какой правильный синтаксис для этого? Этот фрагмент кода не работает: int[] randomTest(int N) { int test[2]; test[0] = 0; test[1] = 1; return test; }
31 янв '19 в 10:42
0
ответов
Как преобразовать двойное значение в целочисленное в UPPAAL?
Как можно привести двойное значение к целочисленному значению в Уппале? double rand; rand = random(2); int i; i = (int) rand; Согласно документации API ( http://www.it.uu.se/research/group/darts/uppaal/help.php?file=System_Descriptions/Expressions.s…
31 янв '19 в 12:25
1
ответ
Простая основная проблема проверки в Уппале
Я борюсь с простой проверкой. У меня есть автоматы и значение х, как это: automata2 Когда x в начале отличается от 0, то E<> x!=0 удовлетворяется, но когда x = 0, тогда его не удовлетворяют, и E<> x == 0 и A<> x == 0 удовлетворяются. Но я хотел бы п…
12 фев '19 в 14:14
1
ответ
Модель проверки синхронной схемы в UPPAAL
Я использую модель проверки UPPAAL для моделирования синхронной схемы на уровне затвора, у меня есть некоторая путаница в том, как я могу смоделировать часы, моя цель - убедиться, что время установки и время удержания не нарушены. Я нашел некоторые …
09 сен '16 в 07:00
1
ответ
Как выбрать массив целых чисел в UPPAAL?
Я использую Uppaal для класса, и я хотел бы создать массив целых чисел в пределах диапазона, используя оператор выбора. Для фона я моделирую модифицированную игру nim с 3 игроками и 3 кучами, где игрок может выбрать до 3 матчей из одной кучи или выб…
25 ноя '15 в 19:24
0
ответов
Параметры шаблона Uppaal
Я использую UPPAAL 4.1.19, и я следую обучающему обучению, данному в этом. В шаблоне Train я поставил параметры int[0,N] e, const int id и в системном объявлении я объявляю Train1=Train(el, 1); и система возвращает мне ошибку "Несовместимый аргумент…
06 июл '18 в 11:49
1
ответ
Государственный космический взрыв в UPPAAL
Я смоделировал синхронизированную модель с двумя триггерами в UPPAAL, когда я попытался проверить некоторые свойства, я достиг состояния 6M, и на моем ноутбуке не было оперативной памяти, было использовано около 5Go, может кто-нибудь сказать, какое …
30 ноя '16 в 05:41
1
ответ
Генерация случайного числа в Уппале
У меня вопрос: можно ли сгенерировать случайное число в Уппале? Я хотел бы сгенерировать число из диапазона значений. Более того, я хотел бы генерировать не только целые числа, но и двойные значения. например: двойной [7.25,18.3] Я нашел этот вопрос…
25 июн '15 в 17:52
0
ответов
Связь между исследуемыми состояниями и используемой памятью при проверке моделей
Какова возможная связь между состояниями и используемой памятью при проверке модели. Можем ли мы оценить общий объем памяти, который может быть использован нашей моделью (пространством состояний), прежде чем фактически внедрить ее в средство проверк…
27 июн '18 в 12:58
0
ответов
Создание шаблона в UPPAAL
Я делаю схемы в UPPAAL, используя базовые ворота. Для этого я создаю эти ворота в системном объявлении для создания требуемой схемы. Я объявил ввод / вывод вентилей в разделе параметров, а затем создал эти значения параметров с необходимыми переменн…
24 окт '17 в 07:46
0
ответов
UPPAAL: Инварианты нарушены, но никто не был явно установлен - как устранить тупик?
Я хотел бы узнать больше о Timed Automata для проверки систем в реальном времени. В настоящее время я пытаюсь ознакомиться с инструментом UPPAAL. Я нарисовал несколько простых графиков и добавил разные свойства. Предполагается, что вся модель предст…
08 авг '15 в 16:17
0
ответов
Не ворота в уппааль
У меня есть модель просто НЕ ворота в Уппале с задержкой распространения. Но я не могу доказать одно свойство. Скриншот автомата прилагается. Xinp - это вход, xout - это выход. 3 здесь используется как задержка распространения. P1: A[] (xinp &&a…
30 мар '17 в 05:33
0
ответов
Уппал: кофе-машина
Здравствуйте, я разрабатываю проблему с кофейным автоматом в Уппале, где заказчик заказывает мока или латте после ввода монеты. Машина должна удостовериться, что монета вставлена и достаточно воды, чтобы хотя бы сделать 5 заказов. Если это условие…
02 май '17 в 12:03
1
ответ
Нахождение общего количества состояний и переходов в UPPAAL
У меня есть большая модель UPPAAL. Я хочу проанализировать общее количество состояний и переходов в моей модели. Есть ли способ узнать эти вещи. Спасибо и всего наилучшего
03 апр '18 в 15:07