CODEWITHSUNDEEP
verificationspinpromelamodel-checking
Anton Belev
Anton Belev

Reputation: 13503

Promela atomic propositions for multiple proctype instances

I was wondering how to write never claims that stand for all instances of a proctype. For example if I have the following proposition:

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

Now if I instantiate 5 instances of the camera_node how can I create an atomic proposition checking if start_publishing is equal to zero for all of these 5 instances?

Upvotes: 1

Views: 146

Answers (1)

GoZoner
GoZoner

Reputation: 70135

Well, it isn't the most beautiful, but I've done this sort of thing in the past. (Note: this code probably isn't proper Promela but you get the point)

#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) && ...)

Upvotes: 1

Related Questions