spin

1зной

1ответ

Расчеты с плавающей точкой в ​​Promela

Я хочу моделировать траекторию снаряда объекта в Промеле и проверить некоторые свойства модели. Но у Promela нет типа данных с плавающей точкой. Таким образом, он не может, например, вычислить парамет

spin model-checking promela 2014-11-22

---

0зной

1ответ

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

У меня есть следующие typedefs. Тип паба хранит два ints, а pub_table хранит массив издателей и int. typedef pub{ int nodeid; int tid }; typedef pub_table{ pub table[TABLE_SIZE];

spin promela 2015-02-01

---

1зной

1ответ

Изготовление автомата изображения моей модели Promela

Я использую модель проверки SPIN GUI - iSPIN. GUI поставляется с красивым генератором представлений Automaton, однако для того, чтобы увидеть полный автомат, мне нужно увеличить/уменьшить масштаб. Так

automata spin promela model-checking 2015-03-23

---

1зной

1ответ

Промела атомарные предложения для нескольких экземпляров proctype

Мне было интересно, как писать никогда не претензий, которые выступают за все экземпляры proctype. Например, если у меня есть следующее предложение: #define c (camera_node[SomePid]:start_publishing ==

verification spin promela model-checking 2015-03-26

---