SPIN / Promela Verification [closed]

Question

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};

   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) ->
        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 */
            printf("MSC: LEADER\n");
            nr_leaders++;
            assert(nr_leaders == 1)
        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!