[funkyjohny]

Ifound this but i don't think that it's c...

/* dolev-klawe-rodeh leader election */

#define N	5
#define I	3
#define L	10

chan ch[N] = [L] of {int};
int nr_of_leaders = 0;

proctype process(chan in, out; int id) {

int d, e, f;

printf("MSC: identitiy is %d\n", id);

act:
  d = id;
  do 
    :: true ->
      printf("MSC: value of d is %d\n", d);
      out!d; in?e;
      if 
        :: (e == d) ->
          printf("MSC: %d is the leader.\n", d);
          nr_of_leaders = nr_of_leaders+1;
          goto stop
        :: else ->
           skip
      fi;
      out!e; in?f;
      if 
        :: (e >= d) && (e >= f) ->
          d = e
        :: else ->
          printf("MSC: I become passive.\n");
          goto pas
      fi;
  od;

pas:
  do :: in?d -> out!d od;

stop:
  skip

}

init {
  byte i;
  atomic {
    i=1;
    do 
      :: i <= N -> 
        run process(ch[i-1], ch[i%N], (I+N-i)%(N+1));
        i = i+1
      :: i > N ->
        break
    od
  }
}