Есть ли у кого-нибудь контакт с проверкой моделей с помощью этого инструмента SPIN , а тем более любой информации проверка модели (параллельные программы)

Я пытаюсь смоделировать проверку простой модели Promela для следующего свойства LTL: ltl { M[0] U M[1] } И я получаю сообщение об ошибке, управляемое моделирование по следу ошибки дает следующий результат: ltl ltl_0: (M[0]) U (M[1]) spin:...

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

Можно ли получить несколько (или все) трассировок нарушений для свойства с помощью Spin? В качестве примера я создал модель Promela ниже: byte mutex = 0; active proctype A() { A1: mutex==0; /* Is free? */ A2: mutex++; /* Get mutex */ A3: /*...

Для проверок (с ispin), в которых никогда не используются утверждения, я получаю выходные данные с depth reached большим, чем количество состояний и количество переходов, например: Full statespace search for: never claim +...

Я смотрю на программное обеспечение SPIN. Я хотел бы использовать его для поиска моделей теорий LTL. Во всех руководствах и туториалах говорится о проверке свойств алгоритмов, но меня это совершенно не интересует. Я просто хочу найти модели формул...

Мне нужно передать массив из родительского процесса в дочерний процесс в Promela , но он не позволяет мне это сделать. Кроме того, у меня есть некоторые ограничения в том, чтобы сделать этот массив глобальным, поэтому я не могу этого сделать. Как...

Я пытаюсь смоделировать один из моих проектов в promela для проверки модели. При этом у меня есть N узлов в сети. Итак, для каждого узла я делаю процесс. Что-то вроде этого: init { byte proc; atomic { proc = 0; do :: proc < N...

Я получаю эту ошибку с Spin 6.4.8 : spin: indexing channels[-1] - size is 3 spin: 2.pml:13, Error: indexing array 'channels' при запуске имитации следующей модели Promela : chan channels[3] = [1] of { pid }; active [3] proctype node ()...

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

Если я напишу следующий код в Promela и запущу его в Spin в режиме верификатора, он завершится с 0 ошибками. Он сообщает, что toogle и init не достигли состояния, но это, похоже, только предупреждения. byte x = 0; byte y = 0; active proctype...

Я уже довольно давно использую подсистему Windows для Linux для SPIN (Promela). Однако без каких-либо изменений в настройке, внезапно с 28 октября 2019 года я получаю сообщение об ошибке «В разрешении отказано» для «/ usr / bin / spin». Другие...