Похоже, что Promela инициализирует каждую переменную (по умолчанию 0 или значение, указанное в объявлении). Как я могу объявить переменную, которая инициализируется неизвестным значением? Документация предлагает if :: p = 0 :: p = 1 fi , но я...

A: if :: q?a -> ... :: else -> ... fi Обратите внимание, что состояние гонки встроено в этот тип кода. Как долго процесс должен ждать, например, прежде чем решить, что операция получения сообщения не будет выполняться? Этой...

ispin генерирует это сообщение в окне прогресса (средний нижний экран на вкладке имитации): Ошибка: отправка на неинициализированный канал Странно то, что сообщение об ошибке начинает появляться в середине симуляции (я установил максимальное число...

Как я могу сгенерировать автомат Buchi, начиная с формулы LTL? например [] (a <-> ! b) То есть, Во все времена в будущем если a верно, то b неверно если b верно, то a неверно

По сути, проверка модели имеет дело с моделью «m» (описание поведения системы) и свойством «p», которому должна удовлетворять система. С обоими артефактами средство проверки модели определяет, удовлетворяет ли модель свойству. Мой вопрос...

Я создал замок пекарни, используя Spin 1 int n=3; 2 int choosing[4] ; // initially 0 3 int number[4]; // initially 0 4 5 active [3] proctype p() 6 { 7 8 choosing[_pid] = 1; 9 int max = 0; 10...

Я выучил Промелу и Спин, но когда я пытаюсь проверить модель, мне возвращаются эти строки. Что они имеют в виду? Спасибо

Я запускаю вращение в режиме проверки с кодом, как показано ниже. Возникла проблема с функцией под названием «никогда». При выполнении выдает ошибку, что функции inc(), dec() и reset() никогда не выполнялись. Но если я добавлю цикл, он отлично...

Скажем, например, у меня есть следующее mtype = {ONE, TWO, THREE} ; mtype array[3] ; mtype test ; test = array[0] ; printf("Test is %e\n", test) ; я получил Test is 1 что я понимаю, потому что базовая переменная является типом char....

Я хочу использовать средство проверки модели SPIN на Windows7-64, и я установил все необходимые для этого средства. Ниже процедура, как я это сделал Я установил компилятор gcc с cygwin .. обновленный путь проверен с помощью командной строки, он...

У меня есть много формул LTL, которые я пытаюсь протестировать в одном и том же файле .pml. Моя проблема заключается в том, что при обнаружении ошибки в какой-либо одной формуле ltl файл следа записывается (или перезаписывается) с тем же именем файла...

Я новичок в Jspin и Promela . Я попытался реализовать следующую систему: Систему домашней сигнализации можно активировать и деактивировать с помощью личного идентификационного ключа или пароля. После активации система переходит в режим...

Когда я пытаюсь сопоставить сообщение в операторе приема, я получаю сообщение об ошибке "плохой тип узла 44". Это происходит, когда тип сообщения является typedef. Сообщение об ошибке довольно загадочно и не дает большого понимания. typedef t {...

Учитывая утверждение "Когда CM бездействует и получает запрос на обновление от WCP, он устанавливает ...." . Некоторый контекст: в канале может быть только один тип сообщения, т. е. он будет содержать только запросы на обновление от wcp. Я могу...