I am a beginner in the spin. I am trying that the model runs the two receiving processes (function called consumer in the model) alternatively, ie. (consumer 1, consumer 2, consumer 1, consumer 2,...). But when I run this code, my output for 2 consumer processes are showing randomly. Can someone help me? This is my code I am struggling with.
mtype = {P, C};
mtype turn = P;
chan ch1 = [1] of {bit};
byte current_consumer = 1;
byte previous_consumer;
active [2] proctype Producer()
{`
bit a = 0;
do
:: atomic {
turn == P ->
ch1 ! a;
printf("The producer %d --> sent %d!\n", _pid, a);
a = 1 - a;
turn = C;
}
od
}
active [2] proctype Consumer()
{
bit b;
do
:: atomic{
turn == C ->
current_consumer = _pid;
ch1 ? b;
printf("The consumer %d --> received %d!\n\n", _pid, b);
assert(current_consumer == _pid);
turn = P;
}
od
}
First of all, let me draw your attention to this excerpt of atomic's documentation:
In your model, this is currently not causing any problem because
ch1
is a buffered channel (i.e. it has size>= 1
). However, any small change in the model could break this invariant.From the comments, I understand that your goal is to alternate consumers, but you don't really care which producer is sending the data.
To be honest, your model already contains two examples of how processes can alternate with one another:
turn
, by assigning a different value each timech1
, since this has size1
However, both approaches are alternating Producer/Consumers rather than Consumers themselves.
One approach I like is message filtering with
eval
(see docs): each Consumer knows its ownid
, waits for a token with its ownid
in a separate channel, and only when that is available it starts doing some work.This model, briefly:
prod2cons
, a channel of size1
. This enforces the following behavior: after some producers created a message some consumer must consume it.cons
, a channel of size1
containing atoken
value indicating which consumer is currently allowed to perform some work. All consumers peek on the contents ofcons
, but only the one with a matchingid
is allowed to consume the token and move on. At the end of its turn, the consumer creates a new token with the nextid
in the chain. Consumers alternate in a round robin fashion.The output is:
Notice that producers do not necessarily alternate with one another, whereas consumers do -- as requested.