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...

Answer 1

Yes, the current proctype will block until a message arrives on Ch. This behavior is described in the Promela Manual under the receive statement. [Because you are providing a variable x (as in Ch?x) any message in Ch will cause the statement to be executable. That is, the pattern matching aspect of receive does not apply.]

Answer 2

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.
     */
}