Post Closed as "off-topic" by Yuval Filmus, Juho, Luke Mathieson, Raphael
2 added 246 characters in body
source | link

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!

Thanks for the input!

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!

1
source | link

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  (>= 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).

Thanks for the input!