How to receive message from 'any' channel in PROMELA/SPIN

Question

I'm modeling an algorithm in Spin. I have a process that has several channels and at some point, I know a message is going to come but don't know from which channel. So want to wait (block) the process until it a message comes from any of the channels. how can I do that?

Answer 1

I think you need Promela's if construct (see http://spinroot.com/spin/Man/if.html).

In the process you're referring to, you probably need the following:

byte var;
if
:: ch1?var -> skip
:: ch2?var -> skip
:: ch3?var -> skip
fi

If none of the channels have anything on them, then "the selection construct as a whole blocks" (quoting the manual), which is exactly the behaviour you want.

To quote the relevant part of the manual more fully: "An option [each of the :: lines] can be selected for execution only when its guard statement is executable [the guard statement is the part before the ->]. If more than one guard statement is executable, one of them will be selected non-deterministically. If none of the guards are executable, the selection construct as a whole blocks."

By the way, I haven't syntax checked or simulated the above in Spin. Hopefully it's right. I'm quite new to Promela and Spin myself.

Answer 2

If you want to have your number of channels variable without having to change the implementation of the send and receive parts, you might use the approach of the following producer-consumer example:

#define NUMCHAN 4

chan channels[NUMCHAN];

init {
    chan ch1 = [1] of { byte };
    chan ch2 = [1] of { byte };
    chan ch3 = [1] of { byte };
    chan ch4 = [1] of { byte };

    channels[0] = ch1;
    channels[1] = ch2;
    channels[2] = ch3;
    channels[3] = ch4;
    // Add further channels above, in
    // accordance with NUMCHAN

    // First let the producer write
    // something, then start the consumer
    run producer();
    atomic { _nr_pr == 1 ->
        run consumer();
    }
}

proctype consumer() {
    byte var, i;
    chan theChan;

    i = 0;
    do
        :: i == NUMCHAN -> break
        :: else ->
             theChan = channels[i];
             if
               :: skip // non-deterministic skip
               :: nempty(theChan) ->
                  theChan ? var;
                  printf("Read value %d from channel %d\n", var, i+1)
             fi;
             i++
    od
}

proctype producer() {
    byte var, i;
    chan theChan;

    i = 0;
    do
        :: i == NUMCHAN -> break
        :: else ->
             theChan = channels[i];
             if
               :: skip;
               :: theChan ! 1;
                  printf("Write value 1 to channel %d\n", i+1)
             fi;
             i++
    od
}

The do loop in the consumer process non-deterministically chooses an index between 0 and NUMCHAN-1 and reads from the respective channel, if there is something to read, else this channel is always skipped. Naturally, during a simulation with Spin the probability to read from channel NUMCHAN is much smaller than that of channel 0, but this does not make any difference in model checking, where any possible path is explored.