A Model of Leader Election on Promela/SPIN

promela_leader.pml

/*
 * Leader Election by Chang-Roberts Algorithm
 */

byte leader = 0;  /* number of leaders */

proctype Node(chan ch_in, ch_out) {
    
    byte tok;
    
    ch_out ! _pid;
    
    end:
    do
    ::  ch_in ? tok ->
            if
            ::  tok <  _pid -> skip                  /* discard */
            ::  tok >  _pid -> ch_out ! tok          /* pass */
            ::  tok == _pid -> leader = leader + 1;  /* elected */
                               break
            fi
    od
}

init {
    
    bool flg[5] = true;
    
    chan a_to_b = [1] of { byte };
    chan b_to_c = [1] of { byte };
    chan c_to_d = [1] of { byte };
    chan d_to_e = [1] of { byte };
    chan e_to_a = [1] of { byte };
    
    /* randomize ID numbers */
    do
    ::  flg[0] -> atomic { run Node(e_to_a, a_to_b); flg[0] = false }
    ::  flg[1] -> atomic { run Node(a_to_b, b_to_c); flg[1] = false }
    ::  flg[2] -> atomic { run Node(b_to_c, c_to_d); flg[2] = false }
    ::  flg[3] -> atomic { run Node(c_to_d, d_to_e); flg[3] = false }
    ::  flg[4] -> atomic { run Node(d_to_e, e_to_a); flg[4] = false }
    ::  else -> break
    od
}

promela_leader_elect.prp

!<>(leader == 1)

promela_leader_unique.prp

![](leader <= 1)