SPIN / Promela Verification 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  (&gt;= 2*N) */

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

   byte nr_leaders = 0;

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

    xr in;  /* exclusive recv access to channel in */
    xs out; /* exclusive send access to channel out */

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

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

  init {
    byte proc;
    atomic {
        proc = 1;
        do      /* iterate through the processes */
        :: proc &lt;= N -&gt;
            run node (q[proc-1], q[proc%N], (N+I-proc)%N+1);
            proc++
        :: proc &gt; N -&gt;
            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!
For the "all the processes agree about the one elected leader" part:

It is a combination (conjunction) of 


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