Описание тега promela

Описание тега Вопросы с тегом
Мета-язык процессов / протоколов - это язык верификационного моделирования, используемый для проверки логики параллельных систем.
1 ответ

Как указать путь к библиотекам C в jspin?

Я использую jspin и пытаюсь включить библиотеку stdio.h в выражение c_code: c_code { #include <stdio.h> } Однако я получаю следующую ошибку: spin: error: No file 'stdio.h' Я проверил каталог, в котором установлен mingw, и в нем есть stdio.h. Т…
08 апр '13 в 07:54
1 ответ

Рекурсивные типы данных в Promela

Я пытаюсь создать B-Tree в Promela, чтобы я мог доказать что-то об этом, однако кажется, что Promela не поддерживает рекурсивные типы данных. Это не работает: #define n 2 typedef BTreeNode { int keys[2*n-1]; BTreeNode children[2*n]; int c; }; Как я …
31 дек '13 в 15:30
2 ответа

Установить реализацию в UPPAAL

У меня есть модель, в которой процесс должен выбрать элемент s случайно из набора S, Выбор части является одной операцией. Единственная похожая структура данных, которую я знаю в UPPAAL, это массивы. Существует ли заданная структура данных в UPPAAL?…
20 май '14 в 05:43
1 ответ

Ошибка синтаксиса Promela: Ошибка: неполная структура ref 'table' saw 'operator: ='

У меня есть следующие typedefs. Тип pub содержит два целых числа, а pub_table содержит массив издателей и int. typedef pub{ int nodeid; int tid }; typedef pub_table{ pub table[TABLE_SIZE]; int last }; Тогда на линии pt.table[pt.last] = p; Я получаю …
01 фев '15 в 20:05
1 ответ

Spin Verification, проверка переменной достигает определенного значения

Это мой первый вопрос на Stack Exchange, так что если есть что-то, что нарушает правила, пожалуйста, дайте мне знать. У меня есть программа, написанная на Promela для ОС колледжа и класса параллельных систем. Есть два запущенных процесса, которые ув…
08 мар '17 в 11:47
1 ответ

iSpin LTL свойство оценки только с активированными "нарушениями утверждения"?

Я пытаюсь привыкнуть к iSpin/Promela. Я использую: Версия Spin 6.4.3 - 16 декабря 2014 года, версия iSpin 1.1.4 - 27 ноября 2014 года, версия 8cl /8.6 TclTk, Windows 8.1. Вот пример, где я пытаюсь использовать LTL. Проверка свойства LTL должна приве…
18 июн '15 в 14:26
1 ответ

Как изменить порядок сообщений в канале?

У меня есть этот код необходимо изменить, чтобы каналы могли переупорядочить сообщения, и я должен добавить механизм, чтобы справиться с этим chan linkA = [10] of {byte}; chan linkB = [10] of {byte}; proctype sender () { byte n; do :: n<10 -> …
15 янв '19 в 21:14
1 ответ

Как я могу связать данный ввод с другой функцией proctype?

Мне нужна помощь в соответствии с последующей задачей, которую я должен реализовать, используя jSpin а также promela язык. Домашняя сигнализация может быть активирована и деактивирована с помощью персонального идентификационного ключа или пароля, по…
13 ноя '17 в 20:05
1 ответ

Как смоделировать очередь в промеле?

Итак, я пытаюсь смоделировать замок CLH-RW в Promela. Способ блокировки прост: действительно: Очередь состоит из tail, к которому и читатели и писатели ставят в очередь узел, содержащий единственный bool succ_must_wait они делают это, создавая новый…
03 ноя '17 в 09:28
1 ответ

Представлен в виде выписки LTl, спин

Извините за мой английский, я из Украины) только начал изучать проверку спиновой системы. Мы задали следующую задачу: "Представьте в форме ниже выражение LTL: если я люблю Машу, я не могу любить Дашу". Я не могу понять, как это сделать. Вот что я по…
04 мар '14 в 18:17
1 ответ

Отправить сообщение на множество каналов в недетерминированном порядке

Я строю модель Promela, в которой один процесс отправляет запрос N другим процессам, ждет ответов и затем вычисляет значение. В основном типичный поток выполнения карты с уменьшением стилей. В настоящее время моя модель отправляет запросы в фиксиров…
14 ноя '17 в 01:50
2 ответа

Какие шаги для проверки LTL с помощью инструмента SPIN?

Я написал модель в Spin. Я хочу проверить некоторые LTL на модели. например: ltl L1 {<>[]Working} в окне проверки я выбираю опцию "использовать заявку" и нажимаю "выполнить": ltl L1: <> ([] (Working)) gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o…
20 июн '13 в 07:03
1 ответ

LTL свойства и программа Promela

У меня есть следующая программа, которая моделирует FIFO с процессом в PROMELA: mtype = { PUSH, POP, IS_EMPTY, IS_FULL }; #define PRODUCER_UID 0 #define CONSUMER_UID 1 proctype fifo(chan inputs, outputs) { mtype command; int data, tmp, src_uid; bool…
09 фев '17 в 23:21
1 ответ

Как мне моделировать логическое И-вычисление в Promela неатомно?

Как мне моделировать логическое И-вычисление в Promela неатомно? Я хочу смоделировать утверждение while (flag[j] == true && victim == i) где И-оценка должна быть сделана неатомно. Как это возможно?
22 ноя '15 в 10:37
1 ответ

Создание автоматического изображения моей модели Promela

Я использую графический интерфейс SPIN - iSPIN. Графический интерфейс поставляется с хорошим генератором представления Automaton, однако, чтобы увидеть полный автомат, мне нужно увеличить / уменьшить масштаб. Также я хотел бы сохранить этот автомат …
23 мар '15 в 21:26
1 ответ

Как SPIN определяет порядок выполнения процессов в атомарных процессах?

Я пытаюсь понять, как SPIN выбирает порядок выполнения и завершения процессов в следующем примере. Я понимаю, что основное внимание в SPIN уделяется анализу параллельных процессов, но для моих целей я просто заинтересован в простом линейном выполнен…
25 июл '17 в 02:50
1 ответ

Проверка вращения - неопределенная ссылка на случайное и случайное

В настоящее время я изучаю Promela/Spin. Проблема в том, что я не могу проверить свои программы. Я создаю свои файлы панорамы с помощью: spin_64bits.exe -a x.pr --- пока все в порядке. Теперь, когда я пытаюсь скомпилировать pan.c через gcc pan.c (gc…
28 ноя '14 в 10:29
0 ответов

Promela, Испин: модель проверки Promela моделирования со спином

Я работаю над проверкой проверки модели с использованием средства проверки модели вращения каждый раз, когда пытаюсь запустить код, я получаю сообщение об ошибке: spin: traffic_controller: 12, ошибка: необъявленная переменная: to_green saw '')' = 41…
10 фев '19 в 12:19
0 ответов

Промела: Почему этот атомарный блок не эквивалентен оператору присваивания?

Я написал следующий код Promela. Этот код моделирует ситуацию, когда два процесса увеличивают общий счетчик. Я ожидал assert в коде должно быть значение true, но SPIN говорит "утверждение нарушено". Странно, когда я заменил atomic блокировать с coun…
02 фев '19 в 08:11
0 ответов

Внесите поправки в модель Promela, приведенную выше, с механизмом искажения сообщений.

Я готовлюсь к итоговому экзамену по проверке системы, и этот вопрос был в последней экзаменационной работе. Мне нужна помощь, чтобы решить это. Интуитивно, отправитель отправляет квадраты первых пяти неотрицательных целых чисел двум процессам-получа…
23 дек '18 в 18:22