# SPIN / Promela Verification [closed]

I have this code here which performs the 'leader election' among a specified number of processes. In Promela, it is written as:

  #define N 5       /* this is the number of processes */
#define I 3   /* node that is given the smallest number    */
#define L 10  /* size of the buffer, channel of channels  (>= 2*N) */

mtype = { one, two, winner };
chan q[N] = [L] of { mtype, byte};

proctype node (chan in, out; byte mynumber)
{ bit Active = 1, know_winner = 0;
byte nr, maximum = mynumber, neighbourR;

printf("MSC: %d\n", mynumber);
out!one(mynumber);
end:  do
:: in?one(nr) ->
if
:: Active ->
if
:: nr != maximum ->
out!two(nr);
neighbourR = nr
:: else ->
/* in case the number equals the max one */
assert(nr == N);
know_winner = 1;
out!winner,nr;
fi
:: else ->
out!one(nr)
fi

:: in?two(nr) ->
if
:: Active ->
if
:: neighbourR > nr && neighbourR > maximum ->
maximum = neighbourR;
out!one(neighbourR)
:: else ->
Active = 0
fi
:: else ->
out!two(nr)
fi
:: in?winner,nr ->
if
:: nr != mynumber ->
printf("MSC: LOST\n");
:: else ->      /* declare the winner */
fi;
if
:: know_winner
:: else -> out!winner,nr
fi;
break
od
}

init {
byte proc;
atomic {
proc = 1;
do      /* iterate through the processes */
:: proc <= N ->
run node (q[proc-1], q[proc%N], (N+I-proc)%N+1);
proc++
:: proc > N ->
break
od
}
}


I'm interested in how I can edit this so I can verify that all processes terminate after I run the code through Spin and that all the processes agree about the one elected leader (that there's one leader).

On this link: http://spinroot.com/spin/Doc/SpinTutorial.pdf on page 31, there's a SPIN property liveliness which includes the verification of termination, so that's what I'm trying to implement now, besides the mutual agreement of the leader.

Thanks for the input!

## closed as off-topic by Yuval Filmus, Juho, Luke Mathieson, Raphael♦Apr 20 '15 at 14:24

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "Questions about software development or programming tools are off-topic here, but can be asked on Stack Overflow." – Yuval Filmus, Juho, Luke Mathieson, Raphael
If this question can be reworded to fit the rules in the help center, please edit the question.

• Anyone? :) How can I verify that this model terminates by adding some additional Promela code? I presume it's something to do with some more assume or assert statements. – Boris Jakovljevic Apr 20 '15 at 13:30
• This seems to be about how to use the specific tools, not computer science concepts. If you edit to pose a question about concepts (i.e. independent of Promela and SPIN), we can reopen. – Raphael Apr 20 '15 at 14:24
• @Raphael Sorry for the inconvenience. This isn't about how to use something. It may appear like it, but it's not. I'm asking how I can solve something through programming. Not how to use Promela and SPIN (which I read the manuals for). – Boris Jakovljevic Apr 20 '15 at 15:11
• Your question lists code and specifically asks how to edit the code to (do something). So, that sounds very much like how to use Spin and how to write code in the Promela language. If you were intending to ask about concepts, I suggest editing the question -- or better yet, post a new question -- to ask about the concepts. Code is almost always out of place in concepts questions. So are manuals. Also if you want to ask about concepts, please tell us what kind of answer you are looking for. For instance, are you looking for how to express some property in temporal logic? – D.W. Apr 21 '15 at 19:03
• @D.W. Hi. :) I'm not looking for ways to express any of the temporal logic. An answer below is a sample answer I was looking for: ideas and ways to do something. The thing is that I do know how to use both Promela and SPIN, so I don't need the help on that, but rather the help on what you guys think how I can achieve my desired goal. That's all. If you still believe I should rephrase the topic, tell me what you think I should name it. – Boris Jakovljevic Apr 21 '15 at 19:23

1. No more than one process can ever be declared to be the leader: $\Box (\textrm{nr} \_ \textrm{leaders} \le 1).$
2. Eventually a leader is elected: $\Diamond (\textrm{nr} \_ \textrm{leaders} = 1).$