leader_election.10.progress.dve

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;
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; },
 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; },
 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=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; },
 qwcheck -> qw { guard number != 21;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_7_in!(0*30+number); };
}
process Node_7 {
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; },
 qwcheck -> qw { guard number != 23;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_8_in!(0*30+number); };
}
process Node_8 {
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; },
 qwcheck -> qw { guard number != 0;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_9_in!(0*30+number); };
}
process Node_9 {
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_0_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_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 == 6; effect nr_leaders = nr_leaders+1; },
 qwcheck -> qw { guard number != 6;},
 qw -> wait { guard know; },
 qw -> wait { guard know==0; sync ch_0_in!(0*30+number); };
}
process channel_ch_0 {
byte buf[20];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 20); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_1 {
byte buf[20];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 20); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_2 {
byte buf[20];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 20); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_3 {
byte buf[20];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 20); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_4 {
byte buf[20];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 20); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_5 {
byte buf[20];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 20); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_6 {
byte buf[20];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 20); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_7 {
byte buf[20];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 20); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_8 {
byte buf[20];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 20); 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] = 0, buf_act = buf_act -1;};
}
process channel_ch_9 {
byte buf[20];
byte buf_act = 0;
state q;
init q;
trans
 q -> q { guard not(buf_act == 20); 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] = 0, buf_act = buf_act -1;};
}
process LTL_property {
state q1, q2;
init q1;
accept q2;
trans
q1 -> q2 { guard not (Node_0.wait) && not (Node_1.wait) && not (Node_2.wait) && not (Node_3.wait) && not (Node_4.wait) && not (Node_5.wait) && not (Node_6.wait) && not (Node_7.wait) && not (Node_8.wait) && not (Node_9.wait); },
q1 -> q1 {},
q2 -> q2 { guard not (Node_0.wait) && not (Node_1.wait) && not (Node_2.wait) && not (Node_3.wait) && not (Node_4.wait) && not (Node_5.wait) && not (Node_6.wait) && not (Node_7.wait) && not (Node_8.wait) && not (Node_9.wait); };
}
system async property LTL_property;