Search code examples
spinpromela

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

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

Solution

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