leader_election.12.dve

 // shoudl be >= 2*N
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;
byte nr_leaders;
process Node_0 {
// 0 my id, 1 next id, 24 my val
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; },
 
 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; },
 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; }, //I am the leader
 qwcheck -> qw { guard number != 24;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_1_in!(0*30+number); };
}
process Node_1 {
// 1 my id, 2 next id, 14 my val
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; }, //I am the leader
 qwcheck -> qw { guard number != 14;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_2_in!(0*30+number); };
}
process Node_2 {
// 2 my id, 3 next id, 6 my val
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; }, //I am the leader
 qwcheck -> qw { guard number != 6;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_3_in!(0*30+number); };
}
process Node_3 {
// 3 my id, 4 next id, 0 my val
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; }, //I am the leader
 qwcheck -> qw { guard number != 0;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_4_in!(0*30+number); };
}
process Node_4 {
// 4 my id, 5 next id, 23 my val
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; }, //I am the leader
 qwcheck -> qw { guard number != 23;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_5_in!(0*30+number); };
}
process Node_5 {
// 5 my id, 6 next id, 21 my val
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; }, //I am the leader
 qwcheck -> qw { guard number != 21;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_6_in!(0*30+number); };
}
process Node_6 {
// 6 my id, 7 next id, 21 my val
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_7_in!(1*30+21); },
 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 == 21; effect nr_leaders = nr_leaders+1; }, //I am the leader
 qwcheck -> qw { guard number != 21;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_7_in!(0*30+number); };
}
process Node_7 {
// 7 my id, 8 next id, 23 my val
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_8_in!(1*30+23); },
 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 == 23; effect nr_leaders = nr_leaders+1; }, //I am the leader
 qwcheck -> qw { guard number != 23;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_8_in!(0*30+number); };
}
process Node_8 {
// 8 my id, 9 next id, 0 my val
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_9_in!(1*30+0); },
 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; },
 
 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; },
 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 == 0; effect nr_leaders = nr_leaders+1; }, //I am the leader
 qwcheck -> qw { guard number != 0;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_9_in!(0*30+number); };
}
process Node_9 {
// 9 my id, 10 next id, 6 my val
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_10_in!(1*30+6); },
 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; },
 
 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; },
 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 == 6; effect nr_leaders = nr_leaders+1; }, //I am the leader
 qwcheck -> qw { guard number != 6;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_10_in!(0*30+number); };
}
process Node_10 {
// 10 my id, 11 next id, 14 my val
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_11_in!(1*30+14); },
 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; },
 
 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; },
 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 == 14; effect nr_leaders = nr_leaders+1; }, //I am the leader
 qwcheck -> qw { guard number != 14;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_11_in!(0*30+number); };
}
process Node_11 {
// 11 my id, 0 next id, 24 my val
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_0_in!(1*30+24); },
 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; },
 
 q1 -> q1a { guard active; },
 q1 -> q1n { guard active==0; },
 q1n -> wait { sync ch_0_in!(1*30+number); },
 q1a -> wait { guard number != max; sync ch_0_in!(2*30+number); effect neigh = number; },
 q1a -> wait { guard number == max; sync ch_0_in!(0*30+number); effect know = 1; },
 q2 -> q2a { guard active; },
 q2 -> q2n { guard active==0; },
 q2n -> wait { sync ch_0_in!(2*30+number); },
 q2a -> wait { guard neigh > number && neigh > max; sync ch_0_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; }, //I am the leader
 qwcheck -> qw { guard number != 24;}, 
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_0_in!(0*30+number); };
}
process channel_ch_0 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_1 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_2 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_3 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_4 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_5 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_6 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_7 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_8 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_9 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_10 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_11 {
byte buf[24];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 24); 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] = 0, buf_act = buf_act -1;};
}
system async;