У меня есть следующий промел-код: chan level = [0] of {int}; proctype Sensor (chan levelChan) { int x; do :: true -> levelChan ? x; if :: (x < 2) -> printf("low %d", x); :: (x...

Я пытаюсь воспроизвести код ALGOL 60, написанный Дейкстрой в статье под названием «Взаимодействующие последовательные процессы», код является первой попыткой решить проблему мьютекса, вот синтаксис: begin integer turn; turn:= 1; parbegin...

Я прочитал руководство по спину, но нет ответа на следующий вопрос: У меня есть строка в моем коде следующим образом: Ch?x где Ch — это канал, а x — тип канала (для получения MSG). Что произойдет, если Ch пуст? будет ли он ждать прибытия...

Ниже приведен код, вызывающий это. if :: ((fromProc[0] == MSG_SLEEP) && nempty(proc2clk[0])) -> proc2clk[0] ? fromProc[0]; // Woke up :: (!(fromProc[0] == MSG_SLEEP) &&...

У меня есть следующие typedefs. Тип Pub хранит два целых числа, а pub_table хранит массив издателей и целое число. typedef pub{ int nodeid; int tid }; typedef pub_table{ pub table[TABLE_SIZE]; int last }; Затем в строке...

Я создаю модель с помощью Promela, и мне нужно дождаться завершения 2 процессов, чтобы продолжить. Как я могу добиться этого с помощью Promela?