leader_election.13UniqueNodes.progress.dve

%own modifications: all max values unique, progress only for active nodes

channel ch_0_in, ch_0_out;
channel ch_1_in, ch_1_out;
channel ch_2_in, ch_2_out;
channel ch_3_in, ch_3_out;
channel ch_4_in, ch_4_out;
channel ch_5_in, ch_5_out;
channel ch_6_in, ch_6_out;
channel ch_7_in, ch_7_out;
channel ch_8_in, ch_8_out;
channel ch_9_in, ch_9_out;
channel ch_10_in, ch_10_out;
channel ch_11_in, ch_11_out;
channel ch_12_in, ch_12_out;

byte nr_leaders;

process Node_0 {
byte max=24, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_1_in!(1*30+24); },
 wait -> got_msg { sync ch_0_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
%progress:
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_1_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_1_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_1_in!(0*30+number); effect know = 1; },
%progress:
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_1_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_1_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 24; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 24;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_1_in!(0*30+number); };
}

process Node_1 {
byte max=14, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_2_in!(1*30+14); },
 wait -> got_msg { sync ch_1_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_2_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_2_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_2_in!(0*30+number); effect know = 1; },
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_2_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_2_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 14; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 14;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_2_in!(0*30+number); };
}

process Node_2 {
byte max=6, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_3_in!(1*30+6); },
 wait -> got_msg { sync ch_2_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_3_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_3_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_3_in!(0*30+number); effect know = 1; },
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_3_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_3_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 6; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 6;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_3_in!(0*30+number); };
}

process Node_3 {
byte max=0, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_4_in!(1*30+0); },
 wait -> got_msg { sync ch_3_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_4_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_4_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_4_in!(0*30+number); effect know = 1; },
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_4_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_4_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 0; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 0;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_4_in!(0*30+number); };
}

process Node_4 {
byte max=23, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_5_in!(1*30+23); },
 wait -> got_msg { sync ch_4_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_5_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_5_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_5_in!(0*30+number); effect know = 1; },
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_5_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_5_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 23; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 23;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_5_in!(0*30+number); };
}

process Node_5 {
byte max=21, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_6_in!(1*30+21); },
 wait -> got_msg { sync ch_5_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_6_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_6_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_6_in!(0*30+number); effect know = 1; },
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_6_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_6_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 21; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 21;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_6_in!(0*30+number); };
}

process Node_6 {
byte max=1, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_7_in!(1*30+1); },
 wait -> got_msg { sync ch_6_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_7_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_7_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_7_in!(0*30+number); effect know = 1; },
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_7_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_7_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 1; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 1;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_7_in!(0*30+number); };
}

process Node_7 {
byte max=3, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_8_in!(1*30+3); },
 wait -> got_msg { sync ch_7_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_8_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_8_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_8_in!(0*30+number); effect know = 1; },
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_8_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_8_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 3; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 3;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_8_in!(0*30+number); };
}

process Node_8 {
byte max=10, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_9_in!(1*30+10); },
 wait -> got_msg { sync ch_8_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
%progress:
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_9_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_9_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_9_in!(0*30+number); effect know = 1; },
%progress:
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_9_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_9_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 10; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 10;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_9_in!(0*30+number); };
}

process Node_9 {
byte max=22, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_10_in!(1*30+22); },
 wait -> got_msg { sync ch_9_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
%progress:
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_10_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_10_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_10_in!(0*30+number); effect know = 1; },
%progress:
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_10_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_10_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 22; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 22;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_10_in!(0*30+number); };
}

process Node_10 {
byte max=5, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_11_in!(1*30+5); },
 wait -> got_msg { sync ch_10_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
%progress:
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_11_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_11_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_11_in!(0*30+number); effect know = 1; },
%progress:
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_11_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_11_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 5; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 5;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_11_in!(0*30+number); };
}

process Node_11 {
byte max=12, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_12_in!(1*30+12); },
 wait -> got_msg { sync ch_11_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
%progress:
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_12_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_12_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_12_in!(0*30+number); effect know = 1; },
%progress:
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_12_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_12_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 12; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 12;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_12_in!(0*30+number); };
}

process Node_12 {
byte max=13, number, neigh;
byte know=0, active=1;
state start, wait, got_msg, q1, q1a, q1n, q2, q2a, q2n, qw, qwcheck;
init start;
trans
 start -> wait { sync ch_13_in!(1*30+13); },
 wait -> got_msg { sync ch_12_out?number; },
 got_msg -> q1 { guard number/30 == 1; effect number = number%30; },
 got_msg -> q2 { guard number/30 == 2; effect number = number%30; },
 got_msg -> qwcheck { guard number/30 == 0; effect number = number%30; },
%progress:
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_13_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_13_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_13_in!(0*30+number); effect know = 1; },
%progress:
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_13_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_13_in!(1*30+neigh); effect max = neigh; },
 q2a -> wait { guard not (neigh > number && neigh > max); effect active = 0; },
 qwcheck -> qw { guard number == 13; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 13;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_13_in!(0*30+number); };
}

%template:
%process channel_ch_L {
%byte buf[!!!2*X];
%byte buf_act = 0;
%state q;
%init q;
%trans
% q -> q { guard not(buf_act == !!!2*X); sync ch_!!!L_in?buf[buf_act]; effect buf_act = buf_act+1; },
% q -> q { guard not(buf_act == 0); sync ch_!!!L_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = buf[26], buf[26] = buf[27], buf[27] = buf[28], buf[28] = buf[29], buf[!!!2*X-1] = 0, buf_act = buf_act -1;};
%}
%

process channel_ch_0 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_0_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_0_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_1 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_1_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_1_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_2 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_2_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_2_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_3 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_3_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_3_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_4 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_4_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_4_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_5 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_5_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_5_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_6 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_6_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_6_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_7 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_7_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_7_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_8 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_8_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_8_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_9 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_9_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_9_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_10 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_10_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_10_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_11 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_11_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_11_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process channel_ch_12 {
byte buf[26];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 26); sync ch_12_in?buf[buf_act]; effect buf_act = buf_act+1; },
 q -> q { guard not(buf_act == 0); sync ch_12_out!buf[0]; effect buf[0] = buf[1], buf[1] = buf[2], buf[2] = buf[3], buf[3] = buf[4], buf[4] = buf[5], buf[5] = buf[6], buf[6] = buf[7], buf[7] = buf[8], buf[8] = buf[9], buf[9] = buf[10], buf[10] = buf[11], buf[11] = buf[12], buf[12] = buf[13], buf[13] = buf[14], buf[14] = buf[15], buf[15] = buf[16], buf[16] = buf[17], buf[17] = buf[18], buf[18] = buf[19], buf[19] = buf[20], buf[20] = buf[21], buf[21] = buf[22], buf[22] = buf[23], buf[23] = buf[24], buf[24] = buf[25], buf[25] = 0, buf_act = buf_act -1;};
}

process LTL_property {
state q1, q2;
init q1;
accept q2;
trans
q1 -> q2 { guard not (Node_0.wait && Node_0.active) && not (Node_1.wait && Node_1.active) && not (Node_2.wait && Node_2.active) && not (Node_3.wait && Node_3.active) && not (Node_4.wait && Node_4.active) && not (Node_5.wait && Node_5.active) && not (Node_6.wait&& Node_6.active) && not (Node_7.wait && Node_7.active) && not (Node_8.wait && Node_8.active) && not (Node_9.wait && Node_9.active) && not (Node_10.wait && Node_10.active) && not (Node_11.wait && Node_11.active) && not (Node_12.wait && Node_12.active); },
q1 -> q1 {},
q2 -> q2 { guard not (Node_0.wait && Node_0.active) && not (Node_1.wait && Node_1.active) && not (Node_2.wait && Node_2.active) && not (Node_3.wait && Node_3.active) && not (Node_4.wait && Node_4.active) && not (Node_5.wait && Node_5.active) && not (Node_6.wait&& Node_6.active) && not (Node_7.wait && Node_7.active) && not (Node_8.wait && Node_8.active) && not (Node_9.wait && Node_9.active) && not (Node_10.wait && Node_10.active) && not (Node_11.wait && Node_11.active) && not (Node_12.wait && Node_12.active); };
}
system async property LTL_property;