In SPIN/Promela, how to receive a MSG from a channel in the correct way?

Question

I read the spin guide yet there is no answer for the following question:

I have a line in my code as following:

Ch?x

where Ch is a channel and x is channel type (to receive MSG) What happens if Ch is empty? will it wait for MSG to arrive or not? Do i need to check first if Ch is not empty?

basically all I want is that if Ch is empty then wait till MSG arrives and when it's arrive continue...

Malte Schwerhoff Malte Schwerhoff · Accepted Answer · 2013-06-17T08:06:16

Bottom line: the semantics of Promela guarantee your desired behaviour, namely, that the receive-operation blocks until a message can be received.

From the receive man page

EXECUTABILITY
The first and the third form of the statement, written with a single question mark, are executable if the first message in the channel matches the pattern from the receive statement.

This tells you when a receive-operation is executable.

The semantics of Promela then tells you why executability matters:

As long as there are executable transitions (corresponding to the basic statements of Promela), the semantics engine will select one of them at random and execute it.

Granted, the quote doesn't make it very explicit, but it means that a statement that is currently not executable will block the executing process until it becomes executable.

Here is a small program that demonstrates the behaviour of the receive-operation.

chan ch = [1] of {byte};
  /* Must be a buffered channel. A non-buffered, i.e., rendezvous channel,
   * won't work, because it won't be possible to execute the atomic block
   * around ch ! 0 atomically since sending over a rendezvous channel blocks
   * as well.
   */

short n = -1;

proctype sender() {
  atomic  {
    ch ! 0;
    n = n + 1;
  }
}

proctype receiver() {
  atomic  {
    ch ? 0;
    n = -n;
  }
}

init {
  atomic {
    run sender();
    run receiver();
  }

  _nr_pr == 1;

  assert n == 0;
    /* Only true if both processes are executed and if sending happened
     * before receiving.
     */
}

In SPIN/Promela, how to receive a MSG from a channel in the correct way?

2 Answers