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

Мне было интересно, как написать никогда утверждения, которые обозначают все экземпляры proctype. Например, если у меня есть следующее предложение:

#define c (camera_node[SomePid]:start_publishing == 0)

Теперь, если я создам 5 экземпляров camera_node, как я могу создать атомарное предложение, проверяющее, равно ли start_publishing нулю для всех этих 5 экземпляров?


verification promela spin model-checking
person Anton Belev    schedule 26.03.2015    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Ну, это не самое красивое, но я делал подобные вещи в прошлом. (Примечание: этот код, вероятно, не соответствует Промеле, но вы поняли)

#define NUMBER_OF_CAMERA_NODES  5

pid_t  cameraPids [NUMBER_OF_CAMERA_NODES];
byte_t cameraPidIndex = 0

active [NUMBER_OF_CAMERA_NODES] proctype cameraTask () {
  atomic { cameraPids[cameraPidIndex++] = _pid }
  // ...
}

#define cameraCheck( index ) (0 == camera_node[cameraPids[(index)]]:start_publishing)

#define checkAllCameras  (cameraCheck(0) && cameraCheck(1) && ...)
person GoZoner    schedule 28.03.2015
comment
Что ж, было слишком поздно, чтобы включить это в мою диссертацию, но все равно приятно знать! : ) Спасибо - person Anton Belev; 28.03.2015