Я хотел бы иметь возможность использовать цикл for для перебора массива значений typedef, как показано ниже: typedef chanArray { chan ch[5] = [1] of {bit}; } chanArray comms[5]; active proctype Reliable() { chanArray channel; for (...

Кто-нибудь знает, можете ли вы использовать (или конвертировать) файлы определения выделения синтаксиса vim с Sublime Text? Я ищу маркер для промелы и нашел только один для vim, но использую возвышенный текст в качестве редактора по умолчанию....

bool p = true; active proctype q() { do :: p=false; p=true; p=false od } never { do :: !p -> goto acceptRun :: else -> skip; skip od; acceptRun : skip } В этой модели промелы утверждение «никогда» проверяет, что сначала, а...

Следующий алгоритм пытается обеспечить взаимное исключение между двумя процессами P1 и P2, каждый из которых выполняет приведенный ниже код. Можно считать, что изначально sema = 0. while true do{ atomic{if sema = 0 then sema:= 1 else go to line...

Я хотел бы распечатать все состояния при проверке моей модели. Мы получаем файл следа, когда происходит нарушение утверждения, но я хочу видеть состояния, даже если нарушения утверждения отсутствуют. Как я могу это сделать?

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

Ниже приведен код Promela, который я пишу. 491 byte api1[5]; 492 byte api2[5]; 493 byte api3[5]; 494 byte reftask1[5] 495 byte reftask2[5]; 496 byte reftask3[5]; 497 byte rid1[5]; 498 byte rid2[5]; 499 byte...

Я новичок в SPIN и Promela, и я столкнулся с этой ошибкой, когда пытался проверить свойство живости в своих моделях. Код ошибки: unreached in proctype P (0 of 29 states) unreached in proctype monitor mutex_assert.pml:39, state...

Здесь http://spinroot.com/spin/Man/Manual.html , написано что: В Promela есть еще один способ избежать проблемы проверки и установки: атомарные последовательности. Добавляя префикс ключевого слова atomic к последовательности операторов,...

Я написал следующую модель алгоритма Петерсона: bool want[2], turn ltl { []<>P[0]@cs } active [2] proctype P() { pid me = _pid pid you = 1 - me do :: want[me] = true turn = you !want[you] || turn == me cs:...

Допустим, у меня есть этот фрагмент кода PROMELA. active proctype A(){ do :: !x -> break :: else -> skip od … //more code } Что именно делают break и skip в данном случае? Разрывает ли break весь процесс...

Допустим, у нас есть этот фрагмент кода: int x = 3; int y = 5; int z = 0; active proctype P(){ if :: x > y -> z = x :: else -> z = y fi } active proctype Q(){ x++ } active proctype R(){ y = y - x } Я не...

Я получаю это сообщение об ошибке при попытке использовать библиотеку Python в Promela и вращаться ( скриншот сообщения об ошибке ): spin: /usr/include/unistd.h:778, Error: inline text too long near '/usr/include/unistd.h' Мой код Промела...