#include <stdlib.h>

#define N 10
#define I 1
#define L 20

typedef enum { one, two, winner } Mtype;

typedef struct Chan
{
  Mtype type;
  int par;
  struct Chan *next;
} Chan;

Chan *challoc(Mtype type, int par)
{
  Chan *ch = (Chan *) malloc(sizeof(Chan));
  ch->type = type;
  ch->par = par;
  ch->next = NULL;
  return ch;
}

int send_ok(Chan *ch)
{
  int len;

  for (len = 0; ch; len++, ch = ch->next);
  return (len < L);
}

void send(Chan **chan, Mtype type, int par)
{
  Chan *ch;

  if (!*chan) *chan = challoc(type, par);
  else
    {
      for (ch = *chan; ch->next; ch = ch->next);
      ch->next = challoc(type, par);
    }
}

int recv_ok(Chan *ch, Mtype type)
{
  return (ch && ch->type == type);
}

void recv(Chan **chan, int *par)
{
  Chan *ch = *chan;

  *par = ch->par;
  *chan = (*chan)->next;
  free(ch);
  ch = NULL;
}

Chan *q[N];
int nr_leaders;
int election_started;

int atomic_ok(int active, Chan *out)
{
  return (!election_started && !active && send_ok(out));
}

void atomic(int *active, Chan **out, int mynumber, int *first_message)
{
  if (!election_started && !*active)
    {
       election_started = 1;
       send(out, one, mynumber);
       *first_message = 0;
       *active = 1;
    }
}

#define in1 q[0]
#define out1 q[1]
#define mynumber1 1
int first_message1, active1, know_winner1, nr1, maximum1, neighborR1;

#define in2 q[1]
#define out2 q[2]
#define mynumber2 10
int first_message2, active2, know_winner2, nr2, maximum2, neighborR2;

#define in3 q[2]
#define out3 q[3]
#define mynumber3 9
int first_message3, active3, know_winner3, nr3, maximum3, neighborR3;

#define in4 q[3]
#define out4 q[4]
#define mynumber4 8
int first_message4, active4, know_winner4, nr4, maximum4, neighborR4;

#define in5 q[4]
#define out5 q[5]
#define mynumber5 7
int first_message5, active5, know_winner5, nr5, maximum5, neighborR5;

#define in6 q[5]
#define out6 q[6]
#define mynumber6 6
int first_message6, active6, know_winner6, nr6, maximum6, neighborR6;

#define in7 q[6]
#define out7 q[7]
#define mynumber7 5
int first_message7, active7, know_winner7, nr7, maximum7, neighborR7;

#define in8 q[7]
#define out8 q[8]
#define mynumber8 4
int first_message8, active8, know_winner8, nr8, maximum8, neighborR8;

#define in9 q[8]
#define out9 q[9]
#define mynumber9 3
int first_message9, active9, know_winner9, nr9, maximum9, neighborR9;

#define in10 q[9]
#define out10 q[0]
#define mynumber10 2
int first_message10, active10, know_winner10, nr10, maximum10, neighborR10;

void _before_all(void)
{
  int i;

  for (i = 0; i < N; i++) q[i] = NULL;
}

void _before(void)
{
  int i;
  Chan *ch;

  for (i = 0; i < N; i++)
    while (q[i])
      {
        ch = q[i];
        q[i] = q[i]->next;
        free(ch);
        ch = NULL;
      }

  nr_leaders = 0;
  election_started = 0;


  first_message1 = 1;
  active1 = know_winner1 = nr1 = neighborR1 = 0;
  maximum1 = mynumber1;

  first_message2 = 1;
  active2 = know_winner2 = nr2 = neighborR2 = 0;
  maximum2 = mynumber2;

  first_message3 = 1;
  active3 = know_winner3 = nr3 = neighborR3 = 0;
  maximum3 = mynumber3;

  first_message4 = 1;
  active4 = know_winner4 = nr4 = neighborR4 = 0;
  maximum4 = mynumber4;

  first_message5 = 1;
  active5 = know_winner5 = nr5 = neighborR5 = 0;
  maximum5 = mynumber5;

  first_message6 = 1;
  active6 = know_winner6 = nr6 = neighborR6 = 0;
  maximum6 = mynumber6;

  first_message7 = 1;
  active7 = know_winner7 = nr7 = neighborR7 = 0;
  maximum7 = mynumber7;

  first_message8 = 1;
  active8 = know_winner8 = nr8 = neighborR8 = 0;
  maximum8 = mynumber8;

  first_message9 = 1;
  active9 = know_winner9 = nr9 = neighborR9 = 0;
  maximum9 = mynumber9;

  first_message10 = 1;
  active10 = know_winner10 = nr10 = neighborR10 = 0;
  maximum10 = mynumber10;
}

void _print(char *tmp)
{
  int i, j;
  Chan *ch;
  char c[8];

  *c = '\0';

  for (i = 0; i < N; i++)
    {
      j = 0;

    if (q[i])
      {
        j = 1;
        switch (q[i]->type)
          {
            case 0 : strcpy(c, "one"); break;
            case 1 : strcpy(c, "two"); break;
            case 2 : strcpy(c, "winner");
          }

        sprintf(&tmp[strlen(tmp)], "   q[%i]: %s(%i)", i, c, q[i]->par);

        for (ch = q[i]->next; ch; ch = ch->next)
          {
            switch (ch->type)
              {
                case 0 : strcpy(c, "one"); break;
                case 1 : strcpy(c, "two"); break;
                case 2 : strcpy(c, "winner");
              }

            sprintf(&tmp[strlen(tmp)], ", %s(%i)", c, ch->par);
          }
      }

      if (j) sprintf(&tmp[strlen(tmp)], "\n");
    }
}

void _hash(unsigned int *h)
{
  int i;
  Chan *ch;

  for (i = 0; i < N; i++)
    if (q[i])
      for (ch = q[i]; ch; ch = ch->next)
        {
          _hash_int(i, h);
          _hash_int(ch->type, h);
          _hash_int(ch->par, h);
        }
}

%%

a1_ok.
a1_violated.

a2_ok.
a2_violated.

1_1; -; -; 1_2.
1_2. (atomic_ok(active1, out1)); {atomic(&active1, &out1, mynumber1, &first_message1);}; 1_2.
1_2. (recv_ok(in1, one)); {recv(&in1, &nr1);}; 1_3;
1_2. (recv_ok(in1, two)); {recv(&in1, &nr1);}; 1_15;
1_2. (recv_ok(in1, winner)); {recv(&in1, &nr1);}; 1_25;
1_3; (first_message1 && !active1); -; 1_4;
1_3; (!first_message1 || active1); -; 1_6;
1_4; -; {active1 = 1;}; 1_5;
1_4; -; -; 1_6;
1_5; (send_ok(out1)); {send(&out1, one, mynumber1);}; 1_6;
1_6; -; {first_message1 = 0;}; 1_7;
1_7; (active1); -; 1_8;
1_7; (!active1); -; 1_14;
1_8; (nr1 != maximum1); -; 1_9;
1_8; (nr1 == maximum1); -; 1_11;
1_9; (send_ok(out1)); {send(&out1, two, nr1);}; 1_10;
1_10; -; {neighborR1 = nr1;}; 1_2.
1_11; (nr1 == N); a1_ok; 1_12;
1_11; (nr1 != N); a1_violated; 1_12;
1_12; -; {know_winner1 = 1;}; 1_13;
1_13; (send_ok(out1)); {send(&out1, winner, nr1);}; 1_2.
1_14; (send_ok(out1)); {send(&out1, two, nr1);}; 1_2.
1_15; (first_message1 && !active1); -; 1_16;
1_15; (!first_message1 || active1); -; 1_19;
1_16; -; {active1 = 1;}; 1_17;
1_16; -; -; 1_18;
1_17; (send_ok(out1)); {send(&out1, one, mynumber1);}; 1_18;
1_18; -; {first_message1 = 0;}; 1_19;
1_19; (active1); -; 1_20;
1_19; (!active1); -; 1_24;
1_20; (neighborR1 > nr1 && neighborR1 > maximum1); -; 1_21;
1_20; (neighborR1 <= nr1 || neighborR1 <= maximum1); -; 1_23;
1_21; -; {maximum1 = neighborR1;}; 1_22;
1_22; (send_ok(out1)); {send(&out1, one, neighborR1);}; 1_2.
1_23; -; {active1 = 0;}; 1_2.
1_24; (send_ok(out1)); {send(&out1, two, nr1);}; 1_2.
1_25; (nr1 != mynumber1); -; 1_26;
1_25; (nr1 == mynumber1); -; 1_27;
1_26; -; -; 1_30;
1_27; -; -; 1_28;
1_28; -; {nr_leaders++;}; 1_29;
1_29; (nr_leaders == 1); a2_ok; 1_30;
1_29; (nr_leaders != 1); a2_violated; 1_30;
1_30; (know_winner1); -; 1_32.
1_30; (!know_winner1); -; 1_31;
1_31; (send_ok(out1)); {send(&out1, winner, nr1);}; 1_32.

2_1; -; -; 2_2.
2_2. (atomic_ok(active2, out2)); {atomic(&active2, &out2, mynumber2, &first_message2);}; 2_2.
2_2. (recv_ok(in2, one)); {recv(&in2, &nr2);}; 2_3;
2_2. (recv_ok(in2, two)); {recv(&in2, &nr2);}; 2_15;
2_2. (recv_ok(in2, winner)); {recv(&in2, &nr2);}; 2_25;
2_3; (first_message2 && !active2); -; 2_4;
2_3; (!first_message2 || active2); -; 2_6;
2_4; -; {active2 = 1;}; 2_5;
2_4; -; -; 2_6;
2_5; (send_ok(out2)); {send(&out2, one, mynumber2);}; 2_6;
2_6; -; {first_message2 = 0;}; 2_7;
2_7; (active2); -; 2_8;
2_7; (!active2); -; 2_14;
2_8; (nr2 != maximum2); -; 2_9;
2_8; (nr2 == maximum2); -; 2_11;
2_9; (send_ok(out2)); {send(&out2, two, nr2);}; 2_10;
2_10; -; {neighborR2 = nr2;}; 2_2.
2_11; (nr2 == N); a1_ok; 2_12;
2_11; (nr2 != N); a1_violated; 2_12;
2_12; -; {know_winner2 = 1;}; 2_13;
2_13; (send_ok(out2)); {send(&out2, winner, nr2);}; 2_2.
2_14; (send_ok(out2)); {send(&out2, two, nr2);}; 2_2.
2_15; (first_message2 && !active2); -; 2_16;
2_15; (!first_message2 || active2); -; 2_19;
2_16; -; {active2 = 1;}; 2_17;
2_16; -; -; 2_18;
2_17; (send_ok(out2)); {send(&out2, one, mynumber2);}; 2_18;
2_18; -; {first_message2 = 0;}; 2_19;
2_19; (active2); -; 2_20;
2_19; (!active2); -; 2_24;
2_20; (neighborR2 > nr2 && neighborR2 > maximum2); -; 2_21;
2_20; (neighborR2 <= nr2 || neighborR2 <= maximum2); -; 2_23;
2_21; -; {maximum2 = neighborR2;}; 2_22;
2_22; (send_ok(out2)); {send(&out2, one, neighborR2);}; 2_2.
2_23; -; {active2 = 0;}; 2_2.
2_24; (send_ok(out2)); {send(&out2, two, nr2);}; 2_2.
2_25; (nr2 != mynumber2); -; 2_26;
2_25; (nr2 == mynumber2); -; 2_27;
2_26; -; -; 2_30;
2_27; -; -; 2_28;
2_28; -; {nr_leaders++;}; 2_29;
2_29; (nr_leaders == 1); a2_ok; 2_30;
2_29; (nr_leaders != 1); a2_violated; 2_30;
2_30; (know_winner2); -; 2_32.
2_30; (!know_winner2); -; 2_31;
2_31; (send_ok(out2)); {send(&out2, winner, nr2);}; 2_32.

3_1; -; -; 3_2.
3_2. (atomic_ok(active3, out3)); {atomic(&active3, &out3, mynumber3, &first_message3);}; 3_2.
3_2. (recv_ok(in3, one)); {recv(&in3, &nr3);}; 3_3;
3_2. (recv_ok(in3, two)); {recv(&in3, &nr3);}; 3_15;
3_2. (recv_ok(in3, winner)); {recv(&in3, &nr3);}; 3_25;
3_3; (first_message3 && !active3); -; 3_4;
3_3; (!first_message3 || active3); -; 3_6;
3_4; -; {active3 = 1;}; 3_5;
3_4; -; -; 3_6;
3_5; (send_ok(out3)); {send(&out3, one, mynumber3);}; 3_6;
3_6; -; {first_message3 = 0;}; 3_7;
3_7; (active3); -; 3_8;
3_7; (!active3); -; 3_14;
3_8; (nr3 != maximum3); -; 3_9;
3_8; (nr3 == maximum3); -; 3_11;
3_9; (send_ok(out3)); {send(&out3, two, nr3);}; 3_10;
3_10; -; {neighborR3 = nr3;}; 3_2.
3_11; (nr3 == N); a1_ok; 3_12;
3_11; (nr3 != N); a1_violated; 3_12;
3_12; -; {know_winner3 = 1;}; 3_13;
3_13; (send_ok(out3)); {send(&out3, winner, nr3);}; 3_2.
3_14; (send_ok(out3)); {send(&out3, two, nr3);}; 3_2.
3_15; (first_message3 && !active3); -; 3_16;
3_15; (!first_message3 || active3); -; 3_19;
3_16; -; {active3 = 1;}; 3_17;
3_16; -; -; 3_18;
3_17; (send_ok(out3)); {send(&out3, one, mynumber3);}; 3_18;
3_18; -; {first_message3 = 0;}; 3_19;
3_19; (active3); -; 3_20;
3_19; (!active3); -; 3_24;
3_20; (neighborR3 > nr3 && neighborR3 > maximum3); -; 3_21;
3_20; (neighborR3 <= nr3 || neighborR3 <= maximum3); -; 3_23;
3_21; -; {maximum3 = neighborR3;}; 3_22;
3_22; (send_ok(out3)); {send(&out3, one, neighborR3);}; 3_2.
3_23; -; {active3 = 0;}; 3_2.
3_24; (send_ok(out3)); {send(&out3, two, nr3);}; 3_2.
3_25; (nr3 != mynumber3); -; 3_26;
3_25; (nr3 == mynumber3); -; 3_27;
3_26; -; -; 3_30;
3_27; -; -; 3_28;
3_28; -; {nr_leaders++;}; 3_29;
3_29; (nr_leaders == 1); a2_ok; 3_30;
3_29; (nr_leaders != 1); a2_violated; 3_30;
3_30; (know_winner3); -; 3_32.
3_30; (!know_winner3); -; 3_31;
3_31; (send_ok(out3)); {send(&out3, winner, nr3);}; 3_32.

4_1; -; -; 4_2.
4_2. (atomic_ok(active4, out4)); {atomic(&active4, &out4, mynumber4, &first_message4);}; 4_2.
4_2. (recv_ok(in4, one)); {recv(&in4, &nr4);}; 4_3;
4_2. (recv_ok(in4, two)); {recv(&in4, &nr4);}; 4_15;
4_2. (recv_ok(in4, winner)); {recv(&in4, &nr4);}; 4_25;
4_3; (first_message4 && !active4); -; 4_4;
4_3; (!first_message4 || active4); -; 4_6;
4_4; -; {active4 = 1;}; 4_5;
4_4; -; -; 4_6;
4_5; (send_ok(out4)); {send(&out4, one, mynumber4);}; 4_6;
4_6; -; {first_message4 = 0;}; 4_7;
4_7; (active4); -; 4_8;
4_7; (!active4); -; 4_14;
4_8; (nr4 != maximum4); -; 4_9;
4_8; (nr4 == maximum4); -; 4_11;
4_9; (send_ok(out4)); {send(&out4, two, nr4);}; 4_10;
4_10; -; {neighborR4 = nr4;}; 4_2.
4_11; (nr4 == N); a1_ok; 4_12;
4_11; (nr4 != N); a1_violated; 4_12;
4_12; -; {know_winner4 = 1;}; 4_13;
4_13; (send_ok(out4)); {send(&out4, winner, nr4);}; 4_2.
4_14; (send_ok(out4)); {send(&out4, two, nr4);}; 4_2.
4_15; (first_message4 && !active4); -; 4_16;
4_15; (!first_message4 || active4); -; 4_19;
4_16; -; {active4 = 1;}; 4_17;
4_16; -; -; 4_18;
4_17; (send_ok(out4)); {send(&out4, one, mynumber4);}; 4_18;
4_18; -; {first_message4 = 0;}; 4_19;
4_19; (active4); -; 4_20;
4_19; (!active4); -; 4_24;
4_20; (neighborR4 > nr4 && neighborR4 > maximum4); -; 4_21;
4_20; (neighborR4 <= nr4 || neighborR4 <= maximum4); -; 4_23;
4_21; -; {maximum4 = neighborR4;}; 4_22;
4_22; (send_ok(out4)); {send(&out4, one, neighborR4);}; 4_2.
4_23; -; {active4 = 0;}; 4_2.
4_24; (send_ok(out4)); {send(&out4, two, nr4);}; 4_2.
4_25; (nr4 != mynumber4); -; 4_26;
4_25; (nr4 == mynumber4); -; 4_27;
4_26; -; -; 4_30;
4_27; -; -; 4_28;
4_28; -; {nr_leaders++;}; 4_29;
4_29; (nr_leaders == 1); a2_ok; 4_30;
4_29; (nr_leaders != 1); a2_violated; 4_30;
4_30; (know_winner4); -; 4_32.
4_30; (!know_winner4); -; 4_31;
4_31; (send_ok(out4)); {send(&out4, winner, nr4);}; 4_32.

5_1; -; -; 5_2.
5_2. (atomic_ok(active5, out5)); {atomic(&active5, &out5, mynumber5, &first_message5);}; 5_2.
5_2. (recv_ok(in5, one)); {recv(&in5, &nr5);}; 5_3;
5_2. (recv_ok(in5, two)); {recv(&in5, &nr5);}; 5_15;
5_2. (recv_ok(in5, winner)); {recv(&in5, &nr5);}; 5_25;
5_3; (first_message5 && !active5); -; 5_4;
5_3; (!first_message5 || active5); -; 5_6;
5_4; -; {active5 = 1;}; 5_5;
5_4; -; -; 5_6;
5_5; (send_ok(out5)); {send(&out5, one, mynumber5);}; 5_6;
5_6; -; {first_message5 = 0;}; 5_7;
5_7; (active5); -; 5_8;
5_7; (!active5); -; 5_14;
5_8; (nr5 != maximum5); -; 5_9;
5_8; (nr5 == maximum5); -; 5_11;
5_9; (send_ok(out5)); {send(&out5, two, nr5);}; 5_10;
5_10; -; {neighborR5 = nr5;}; 5_2.
5_11; (nr5 == N); a1_ok; 5_12;
5_11; (nr5 != N); a1_violated; 5_12;
5_12; -; {know_winner5 = 1;}; 5_13;
5_13; (send_ok(out5)); {send(&out5, winner, nr5);}; 5_2.
5_14; (send_ok(out5)); {send(&out5, two, nr5);}; 5_2.
5_15; (first_message5 && !active5); -; 5_16;
5_15; (!first_message5 || active5); -; 5_19;
5_16; -; {active5 = 1;}; 5_17;
5_16; -; -; 5_18;
5_17; (send_ok(out5)); {send(&out5, one, mynumber5);}; 5_18;
5_18; -; {first_message5 = 0;}; 5_19;
5_19; (active5); -; 5_20;
5_19; (!active5); -; 5_24;
5_20; (neighborR5 > nr5 && neighborR5 > maximum5); -; 5_21;
5_20; (neighborR5 <= nr5 || neighborR5 <= maximum5); -; 5_23;
5_21; -; {maximum5 = neighborR5;}; 5_22;
5_22; (send_ok(out5)); {send(&out5, one, neighborR5);}; 5_2.
5_23; -; {active5 = 0;}; 5_2.
5_24; (send_ok(out5)); {send(&out5, two, nr5);}; 5_2.
5_25; (nr5 != mynumber5); -; 5_26;
5_25; (nr5 == mynumber5); -; 5_27;
5_26; -; -; 5_30;
5_27; -; -; 5_28;
5_28; -; {nr_leaders++;}; 5_29;
5_29; (nr_leaders == 1); a2_ok; 5_30;
5_29; (nr_leaders != 1); a2_violated; 5_30;
5_30; (know_winner5); -; 5_32.
5_30; (!know_winner5); -; 5_31;
5_31; (send_ok(out5)); {send(&out5, winner, nr5);}; 5_32.

6_1; -; -; 6_2.
6_2. (atomic_ok(active6, out6)); {atomic(&active6, &out6, mynumber6, &first_message6);}; 6_2.
6_2. (recv_ok(in6, one)); {recv(&in6, &nr6);}; 6_3;
6_2. (recv_ok(in6, two)); {recv(&in6, &nr6);}; 6_15;
6_2. (recv_ok(in6, winner)); {recv(&in6, &nr6);}; 6_25;
6_3; (first_message6 && !active6); -; 6_4;
6_3; (!first_message6 || active6); -; 6_6;
6_4; -; {active6 = 1;}; 6_5;
6_4; -; -; 6_6;
6_5; (send_ok(out6)); {send(&out6, one, mynumber6);}; 6_6;
6_6; -; {first_message6 = 0;}; 6_7;
6_7; (active6); -; 6_8;
6_7; (!active6); -; 6_14;
6_8; (nr6 != maximum6); -; 6_9;
6_8; (nr6 == maximum6); -; 6_11;
6_9; (send_ok(out6)); {send(&out6, two, nr6);}; 6_10;
6_10; -; {neighborR6 = nr6;}; 6_2.
6_11; (nr6 == N); a1_ok; 6_12;
6_11; (nr6 != N); a1_violated; 6_12;
6_12; -; {know_winner6 = 1;}; 6_13;
6_13; (send_ok(out6)); {send(&out6, winner, nr6);}; 6_2.
6_14; (send_ok(out6)); {send(&out6, two, nr6);}; 6_2.
6_15; (first_message6 && !active6); -; 6_16;
6_15; (!first_message6 || active6); -; 6_19;
6_16; -; {active6 = 1;}; 6_17;
6_16; -; -; 6_18;
6_17; (send_ok(out6)); {send(&out6, one, mynumber6);}; 6_18;
6_18; -; {first_message6 = 0;}; 6_19;
6_19; (active6); -; 6_20;
6_19; (!active6); -; 6_24;
6_20; (neighborR6 > nr6 && neighborR6 > maximum6); -; 6_21;
6_20; (neighborR6 <= nr6 || neighborR6 <= maximum6); -; 6_23;
6_21; -; {maximum6 = neighborR6;}; 6_22;
6_22; (send_ok(out6)); {send(&out6, one, neighborR6);}; 6_2.
6_23; -; {active6 = 0;}; 6_2.
6_24; (send_ok(out6)); {send(&out6, two, nr6);}; 6_2.
6_25; (nr6 != mynumber6); -; 6_26;
6_25; (nr6 == mynumber6); -; 6_27;
6_26; -; -; 6_30;
6_27; -; -; 6_28;
6_28; -; {nr_leaders++;}; 6_29;
6_29; (nr_leaders == 1); a2_ok; 6_30;
6_29; (nr_leaders != 1); a2_violated; 6_30;
6_30; (know_winner6); -; 6_32.
6_30; (!know_winner6); -; 6_31;
6_31; (send_ok(out6)); {send(&out6, winner, nr6);}; 6_32.

7_1; -; -; 7_2.
7_2. (atomic_ok(active7, out7)); {atomic(&active7, &out7, mynumber7, &first_message7);}; 7_2.
7_2. (recv_ok(in7, one)); {recv(&in7, &nr7);}; 7_3;
7_2. (recv_ok(in7, two)); {recv(&in7, &nr7);}; 7_15;
7_2. (recv_ok(in7, winner)); {recv(&in7, &nr7);}; 7_25;
7_3; (first_message7 && !active7); -; 7_4;
7_3; (!first_message7 || active7); -; 7_6;
7_4; -; {active7 = 1;}; 7_5;
7_4; -; -; 7_6;
7_5; (send_ok(out7)); {send(&out7, one, mynumber7);}; 7_6;
7_6; -; {first_message7 = 0;}; 7_7;
7_7; (active7); -; 7_8;
7_7; (!active7); -; 7_14;
7_8; (nr7 != maximum7); -; 7_9;
7_8; (nr7 == maximum7); -; 7_11;
7_9; (send_ok(out7)); {send(&out7, two, nr7);}; 7_10;
7_10; -; {neighborR7 = nr7;}; 7_2.
7_11; (nr7 == N); a1_ok; 7_12;
7_11; (nr7 != N); a1_violated; 7_12;
7_12; -; {know_winner7 = 1;}; 7_13;
7_13; (send_ok(out7)); {send(&out7, winner, nr7);}; 7_2.
7_14; (send_ok(out7)); {send(&out7, two, nr7);}; 7_2.
7_15; (first_message7 && !active7); -; 7_16;
7_15; (!first_message7 || active7); -; 7_19;
7_16; -; {active7 = 1;}; 7_17;
7_16; -; -; 7_18;
7_17; (send_ok(out7)); {send(&out7, one, mynumber7);}; 7_18;
7_18; -; {first_message7 = 0;}; 7_19;
7_19; (active7); -; 7_20;
7_19; (!active7); -; 7_24;
7_20; (neighborR7 > nr7 && neighborR7 > maximum7); -; 7_21;
7_20; (neighborR7 <= nr7 || neighborR7 <= maximum7); -; 7_23;
7_21; -; {maximum7 = neighborR7;}; 7_22;
7_22; (send_ok(out7)); {send(&out7, one, neighborR7);}; 7_2.
7_23; -; {active7 = 0;}; 7_2.
7_24; (send_ok(out7)); {send(&out7, two, nr7);}; 7_2.
7_25; (nr7 != mynumber7); -; 7_26;
7_25; (nr7 == mynumber7); -; 7_27;
7_26; -; -; 7_30;
7_27; -; -; 7_28;
7_28; -; {nr_leaders++;}; 7_29;
7_29; (nr_leaders == 1); a2_ok; 7_30;
7_29; (nr_leaders != 1); a2_violated; 7_30;
7_30; (know_winner7); -; 7_32.
7_30; (!know_winner7); -; 7_31;
7_31; (send_ok(out7)); {send(&out7, winner, nr7);}; 7_32.

8_1; -; -; 8_2.
8_2. (atomic_ok(active8, out8)); {atomic(&active8, &out8, mynumber8, &first_message8);}; 8_2.
8_2. (recv_ok(in8, one)); {recv(&in8, &nr8);}; 8_3;
8_2. (recv_ok(in8, two)); {recv(&in8, &nr8);}; 8_15;
8_2. (recv_ok(in8, winner)); {recv(&in8, &nr8);}; 8_25;
8_3; (first_message8 && !active8); -; 8_4;
8_3; (!first_message8 || active8); -; 8_6;
8_4; -; {active8 = 1;}; 8_5;
8_4; -; -; 8_6;
8_5; (send_ok(out8)); {send(&out8, one, mynumber8);}; 8_6;
8_6; -; {first_message8 = 0;}; 8_7;
8_7; (active8); -; 8_8;
8_7; (!active8); -; 8_14;
8_8; (nr8 != maximum8); -; 8_9;
8_8; (nr8 == maximum8); -; 8_11;
8_9; (send_ok(out8)); {send(&out8, two, nr8);}; 8_10;
8_10; -; {neighborR8 = nr8;}; 8_2.
8_11; (nr8 == N); a1_ok; 8_12;
8_11; (nr8 != N); a1_violated; 8_12;
8_12; -; {know_winner8 = 1;}; 8_13;
8_13; (send_ok(out8)); {send(&out8, winner, nr8);}; 8_2.
8_14; (send_ok(out8)); {send(&out8, two, nr8);}; 8_2.
8_15; (first_message8 && !active8); -; 8_16;
8_15; (!first_message8 || active8); -; 8_19;
8_16; -; {active8 = 1;}; 8_17;
8_16; -; -; 8_18;
8_17; (send_ok(out8)); {send(&out8, one, mynumber8);}; 8_18;
8_18; -; {first_message8 = 0;}; 8_19;
8_19; (active8); -; 8_20;
8_19; (!active8); -; 8_24;
8_20; (neighborR8 > nr8 && neighborR8 > maximum8); -; 8_21;
8_20; (neighborR8 <= nr8 || neighborR8 <= maximum8); -; 8_23;
8_21; -; {maximum8 = neighborR8;}; 8_22;
8_22; (send_ok(out8)); {send(&out8, one, neighborR8);}; 8_2.
8_23; -; {active8 = 0;}; 8_2.
8_24; (send_ok(out8)); {send(&out8, two, nr8);}; 8_2.
8_25; (nr8 != mynumber8); -; 8_26;
8_25; (nr8 == mynumber8); -; 8_27;
8_26; -; -; 8_30;
8_27; -; -; 8_28;
8_28; -; {nr_leaders++;}; 8_29;
8_29; (nr_leaders == 1); a2_ok; 8_30;
8_29; (nr_leaders != 1); a2_violated; 8_30;
8_30; (know_winner8); -; 8_32.
8_30; (!know_winner8); -; 8_31;
8_31; (send_ok(out8)); {send(&out8, winner, nr8);}; 8_32.

9_1; -; -; 9_2.
9_2. (atomic_ok(active9, out9)); {atomic(&active9, &out9, mynumber9, &first_message9);}; 9_2.
9_2. (recv_ok(in9, one)); {recv(&in9, &nr9);}; 9_3;
9_2. (recv_ok(in9, two)); {recv(&in9, &nr9);}; 9_15;
9_2. (recv_ok(in9, winner)); {recv(&in9, &nr9);}; 9_25;
9_3; (first_message9 && !active9); -; 9_4;
9_3; (!first_message9 || active9); -; 9_6;
9_4; -; {active9 = 1;}; 9_5;
9_4; -; -; 9_6;
9_5; (send_ok(out9)); {send(&out9, one, mynumber9);}; 9_6;
9_6; -; {first_message9 = 0;}; 9_7;
9_7; (active9); -; 9_8;
9_7; (!active9); -; 9_14;
9_8; (nr9 != maximum9); -; 9_9;
9_8; (nr9 == maximum9); -; 9_11;
9_9; (send_ok(out9)); {send(&out9, two, nr9);}; 9_10;
9_10; -; {neighborR9 = nr9;}; 9_2.
9_11; (nr9 == N); a1_ok; 9_12;
9_11; (nr9 != N); a1_violated; 9_12;
9_12; -; {know_winner9 = 1;}; 9_13;
9_13; (send_ok(out9)); {send(&out9, winner, nr9);}; 9_2.
9_14; (send_ok(out9)); {send(&out9, two, nr9);}; 9_2.
9_15; (first_message9 && !active9); -; 9_16;
9_15; (!first_message9 || active9); -; 9_19;
9_16; -; {active9 = 1;}; 9_17;
9_16; -; -; 9_18;
9_17; (send_ok(out9)); {send(&out9, one, mynumber9);}; 9_18;
9_18; -; {first_message9 = 0;}; 9_19;
9_19; (active9); -; 9_20;
9_19; (!active9); -; 9_24;
9_20; (neighborR9 > nr9 && neighborR9 > maximum9); -; 9_21;
9_20; (neighborR9 <= nr9 || neighborR9 <= maximum9); -; 9_23;
9_21; -; {maximum9 = neighborR9;}; 9_22;
9_22; (send_ok(out9)); {send(&out9, one, neighborR9);}; 9_2.
9_23; -; {active9 = 0;}; 9_2.
9_24; (send_ok(out9)); {send(&out9, two, nr9);}; 9_2.
9_25; (nr9 != mynumber9); -; 9_26;
9_25; (nr9 == mynumber9); -; 9_27;
9_26; -; -; 9_30;
9_27; -; -; 9_28;
9_28; -; {nr_leaders++;}; 9_29;
9_29; (nr_leaders == 1); a2_ok; 9_30;
9_29; (nr_leaders != 1); a2_violated; 9_30;
9_30; (know_winner9); -; 9_32.
9_30; (!know_winner9); -; 9_31;
9_31; (send_ok(out9)); {send(&out9, winner, nr9);}; 9_32.

10_1; -; -; 10_2.
10_2. (atomic_ok(active10, out10)); {atomic(&active10, &out10, mynumber10, &first_message10);}; 10_2.
10_2. (recv_ok(in10, one)); {recv(&in10, &nr10);}; 10_3;
10_2. (recv_ok(in10, two)); {recv(&in10, &nr10);}; 10_15;
10_2. (recv_ok(in10, winner)); {recv(&in10, &nr10);}; 10_25;
10_3; (first_message10 && !active10); -; 10_4;
10_3; (!first_message10 || active10); -; 10_6;
10_4; -; {active10 = 1;}; 10_5;
10_4; -; -; 10_6;
10_5; (send_ok(out10)); {send(&out10, one, mynumber10);}; 10_6;
10_6; -; {first_message10 = 0;}; 10_7;
10_7; (active10); -; 10_8;
10_7; (!active10); -; 10_14;
10_8; (nr10 != maximum10); -; 10_9;
10_8; (nr10 == maximum10); -; 10_11;
10_9; (send_ok(out10)); {send(&out10, two, nr10);}; 10_10;
10_10; -; {neighborR10 = nr10;}; 10_2.
10_11; (nr10 == N); a1_ok; 10_12;
10_11; (nr10 != N); a1_violated; 10_12;
10_12; -; {know_winner10 = 1;}; 10_13;
10_13; (send_ok(out10)); {send(&out10, winner, nr10);}; 10_2.
10_14; (send_ok(out10)); {send(&out10, two, nr10);}; 10_2.
10_15; (first_message10 && !active10); -; 10_16;
10_15; (!first_message10 || active10); -; 10_19;
10_16; -; {active10 = 1;}; 10_17;
10_16; -; -; 10_18;
10_17; (send_ok(out10)); {send(&out10, one, mynumber10);}; 10_18;
10_18; -; {first_message10 = 0;}; 10_19;
10_19; (active10); -; 10_20;
10_19; (!active10); -; 10_24;
10_20; (neighborR10 > nr10 && neighborR10 > maximum10); -; 10_21;
10_20; (neighborR10 <= nr10 || neighborR10 <= maximum10); -; 10_23;
10_21; -; {maximum10 = neighborR10;}; 10_22;
10_22; (send_ok(out10)); {send(&out10, one, neighborR10);}; 10_2.
10_23; -; {active10 = 0;}; 10_2.
10_24; (send_ok(out10)); {send(&out10, two, nr10);}; 10_2.
10_25; (nr10 != mynumber10); -; 10_26;
10_25; (nr10 == mynumber10); -; 10_27;
10_26; -; -; 10_30;
10_27; -; -; 10_28;
10_28; -; {nr_leaders++;}; 10_29;
10_29; (nr_leaders == 1); a2_ok; 10_30;
10_29; (nr_leaders != 1); a2_violated; 10_30;
10_30; (know_winner10); -; 10_32.
10_30; (!know_winner10); -; 10_31;
10_31; (send_ok(out10)); {send(&out10, winner, nr10);}; 10_32.

n: T0_init. (! ((nr_leaders == 1))); -; =accept_S4.
n: T0_init. (1); -; T0_init.
n: =accept_S4. (! ((nr_leaders == 1))); -; =accept_S4.