LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
1 67 1: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
2 74 2: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
3 81 3: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
8 88 8: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
16 95 16: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
21 102 21: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
26 109 26: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
27 116 27: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
31 123 31: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
34 130 34: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
35 137 35: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
38 144 38: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
39 151 39: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 36, 42, 45, 50, 65, 66 using the following ranking functions, which are bounded by −41.

42: 0
41: 0
37: 0
38: 0
39: 0
40: 0
33: 0
35: 0
0: 0
1: 0
2: 0
3: 0
4: 0
5: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 0
17: 0
18: 0
19: 0
20: 0
21: 0
22: 0
23: 0
24: 0
26: 0
27: 0
28: 0
29: 0
30: 0
31: 0
32: 0
34: 0
36: 0
25: 0
42: −7
41: −8
37: −9
38: −9
39: −9
40: −9
38_var_snapshot: −9
38*: −9
39_var_snapshot: −9
39*: −9
33: −12
35: −12
35_var_snapshot: −12
35*: −12
1: −13
23: −13
27: −13
28: −13
31: −13
32: −13
0: −13
2: −13
3: −13
4: −13
5: −13
6: −13
7: −13
8: −13
9: −13
10: −13
11: −13
12: −13
13: −13
14: −13
15: −13
16: −13
17: −13
18: −13
19: −13
20: −13
21: −13
36: −13
22: −13
24: −13
26: −13
29: −13
30: −13
34: −13
1_var_snapshot: −13
1*: −13
2_var_snapshot: −13
2*: −13
3_var_snapshot: −13
3*: −13
8_var_snapshot: −13
8*: −13
16_var_snapshot: −13
16*: −13
21_var_snapshot: −13
21*: −13
26_var_snapshot: −13
26*: −13
27_var_snapshot: −13
27*: −13
31_var_snapshot: −13
31*: −13
34_var_snapshot: −13
34*: −13
25: −32

3 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

1* 70 1: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

4 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

1 68 1_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

5 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

2* 77 2: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

6 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

2 75 2_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

7 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

3* 84 3: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

8 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

3 82 3_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

9 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

8* 91 8: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

10 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

8 89 8_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

11 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

16* 98 16: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

12 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

16 96 16_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

13 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

21* 105 21: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

14 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

21 103 21_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

15 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

26* 112 26: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

16 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

26 110 26_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

17 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

27* 119 27: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

18 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

27 117 27_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

19 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

31* 126 31: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

20 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

31 124 31_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

21 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

34* 133 34: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

22 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

34 131 34_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

23 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

35* 140 35: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

24 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

35 138 35_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

25 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

38* 147 38: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

26 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

38 145 38_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

27 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

39* 154 39: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

28 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

39 152 39_var_snapshot: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0

29 SCC Decomposition

We consider subproblems for each of the 3 SCC(s) of the program graph.

29.1 SCC Subproblem 1/3

Here we consider the SCC { 1, 23, 27, 28, 31, 32, 0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 36, 22, 24, 26, 29, 30, 34, 1_var_snapshot, 1*, 2_var_snapshot, 2*, 3_var_snapshot, 3*, 8_var_snapshot, 8*, 16_var_snapshot, 16*, 21_var_snapshot, 21*, 26_var_snapshot, 26*, 27_var_snapshot, 27*, 31_var_snapshot, 31*, 34_var_snapshot, 34* }.

29.1.1 Splitting Cut-Point Transitions

We consider 10 subproblems corresponding to sets of cut-point transitions as follows.

29.1.1.1 Cut-Point Subproblem 1/10

Here we consider cut-point transition 67.

29.1.1.1.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0
1: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
22: 1 ≤ 0
23: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
25: TRUE
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
33: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
35: ip_0 + n_0 ≤ 0
36: 1 ≤ 0
37: TRUE
38: TRUE
39: TRUE
40: TRUE
41: TRUE
42: TRUE
1: 1 ≤ 0
23: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
36: 1 ≤ 0
22: FALSE
24: FALSE
26: FALSE
29: FALSE
30: FALSE
34: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: FALSE
8_var_snapshot: 1 ≤ 0
8*: 1 ≤ 0
16_var_snapshot: 1 ≤ 0
16*: 1 ≤ 0
21_var_snapshot: 1 ≤ 0
21*: 1 ≤ 0
26_var_snapshot: FALSE
26*: FALSE
27_var_snapshot: 1 ≤ 0
27*: 1 ≤ 0
31_var_snapshot: 1 ≤ 0
31*: 1 ≤ 0
34_var_snapshot: FALSE
34*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.1.1.2 Transition Removal

We remove transition 68 using the following ranking functions, which are bounded by −56.

1: −1
23: −2
27: −3
28: −4
31: −5
32: −6
0: −7
2: −8
4: −9
5: −10
6: −11
7: −12
8: −13
9: −14
10: −15
11: −16
12: −17
13: −18
14: −19
15: −20
16: −21
17: −22
18: −23
19: −24
20: −25
21: −26
36: −27
34: −28
1_var_snapshot: −29
1*: −30
2_var_snapshot: −31
2*: −32
3_var_snapshot: −33
8_var_snapshot: −34
16_var_snapshot: −35
16*: −36
21_var_snapshot: −37
21*: −38
27_var_snapshot: −39
27*: −40
31_var_snapshot: −41
31*: −42
34_var_snapshot: −43
30: −44
26*: −45
26: −46
26_var_snapshot: −47
29: −48
24: −49
22: −50
8*: −51
3*: −52
3: −53
34*: −54

29.1.1.1.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.1.1.2 Cut-Point Subproblem 2/10

Here we consider cut-point transition 74.

29.1.1.2.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0
1: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
22: 1 ≤ 0
23: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
25: TRUE
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
33: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
35: ip_0 + n_0 ≤ 0
36: 1 ≤ 0
37: TRUE
38: TRUE
39: TRUE
40: TRUE
41: TRUE
42: TRUE
1: 1 ≤ 0
23: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
36: 1 ≤ 0
22: FALSE
24: FALSE
26: FALSE
29: FALSE
30: FALSE
34: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: FALSE
8_var_snapshot: 1 ≤ 0
8*: 1 ≤ 0
16_var_snapshot: 1 ≤ 0
16*: 1 ≤ 0
21_var_snapshot: 1 ≤ 0
21*: 1 ≤ 0
26_var_snapshot: FALSE
26*: FALSE
27_var_snapshot: 1 ≤ 0
27*: 1 ≤ 0
31_var_snapshot: 1 ≤ 0
31*: 1 ≤ 0
34_var_snapshot: FALSE
34*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.1.2.2 Transition Removal

We remove transition 75 using the following ranking functions, which are bounded by −56.

1: −1
23: −2
27: −3
28: −4
31: −5
32: −6
0: −7
2: −8
4: −9
5: −10
6: −11
7: −12
8: −13
9: −14
10: −15
11: −16
12: −17
13: −18
14: −19
15: −20
16: −21
17: −22
18: −23
19: −24
20: −25
21: −26
36: −27
34: −28
1_var_snapshot: −29
1*: −30
2_var_snapshot: −31
2*: −32
3_var_snapshot: −33
8_var_snapshot: −34
16_var_snapshot: −35
16*: −36
21_var_snapshot: −37
21*: −38
27_var_snapshot: −39
27*: −40
31_var_snapshot: −41
31*: −42
34_var_snapshot: −43
30: −44
26*: −45
26: −46
26_var_snapshot: −47
29: −48
24: −49
22: −50
8*: −51
3*: −52
3: −53
34*: −54

29.1.1.2.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.1.1.3 Cut-Point Subproblem 3/10

Here we consider cut-point transition 81.

29.1.1.3.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0
1: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
22: 1 ≤ 0
23: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
25: TRUE
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
33: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
35: ip_0 + n_0 ≤ 0
36: 1 ≤ 0
37: TRUE
38: TRUE
39: TRUE
40: TRUE
41: TRUE
42: TRUE
1: 1 ≤ 0
23: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
36: 1 ≤ 0
22: FALSE
24: FALSE
26: FALSE
29: FALSE
30: FALSE
34: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: FALSE
8_var_snapshot: 1 ≤ 0
8*: 1 ≤ 0
16_var_snapshot: 1 ≤ 0
16*: 1 ≤ 0
21_var_snapshot: 1 ≤ 0
21*: 1 ≤ 0
26_var_snapshot: FALSE
26*: FALSE
27_var_snapshot: 1 ≤ 0
27*: 1 ≤ 0
31_var_snapshot: 1 ≤ 0
31*: 1 ≤ 0
34_var_snapshot: FALSE
34*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.1.3.2 Transition Removal

We remove transition 82 using the following ranking functions, which are bounded by −56.

1: −1
23: −2
27: −3
28: −4
31: −5
32: −6
0: −7
2: −8
4: −9
5: −10
6: −11
7: −12
8: −13
9: −14
10: −15
11: −16
12: −17
13: −18
14: −19
15: −20
16: −21
17: −22
18: −23
19: −24
20: −25
21: −26
36: −27
34: −28
1_var_snapshot: −29
1*: −30
2_var_snapshot: −31
2*: −32
3_var_snapshot: −33
8_var_snapshot: −34
16_var_snapshot: −35
16*: −36
21_var_snapshot: −37
21*: −38
27_var_snapshot: −39
27*: −40
31_var_snapshot: −41
31*: −42
34_var_snapshot: −43
30: −44
26*: −45
26: −46
26_var_snapshot: −47
29: −48
24: −49
22: −50
8*: −51
3*: −52
3: −53
34*: −54

29.1.1.3.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.1.1.4 Cut-Point Subproblem 4/10

Here we consider cut-point transition 88.

29.1.1.4.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0
1: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
22: 1 ≤ 0
23: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
25: TRUE
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
33: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
35: ip_0 + n_0 ≤ 0
36: 1 ≤ 0
37: TRUE
38: TRUE
39: TRUE
40: TRUE
41: TRUE
42: TRUE
1: 1 ≤ 0
23: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
36: 1 ≤ 0
22: FALSE
24: FALSE
26: FALSE
29: FALSE
30: FALSE
34: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: FALSE
8_var_snapshot: 1 ≤ 0
8*: 1 ≤ 0
16_var_snapshot: 1 ≤ 0
16*: 1 ≤ 0
21_var_snapshot: 1 ≤ 0
21*: 1 ≤ 0
26_var_snapshot: FALSE
26*: FALSE
27_var_snapshot: 1 ≤ 0
27*: 1 ≤ 0
31_var_snapshot: 1 ≤ 0
31*: 1 ≤ 0
34_var_snapshot: FALSE
34*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.1.4.2 Transition Removal

We remove transition 89 using the following ranking functions, which are bounded by −56.

1: −1
23: −2
27: −3
28: −4
31: −5
32: −6
0: −7
2: −8
4: −9
5: −10
6: −11
7: −12
8: −13
9: −14
10: −15
11: −16
12: −17
13: −18
14: −19
15: −20
16: −21
17: −22
18: −23
19: −24
20: −25
21: −26
36: −27
34: −28
1_var_snapshot: −29
1*: −30
2_var_snapshot: −31
2*: −32
3_var_snapshot: −33
8_var_snapshot: −34
16_var_snapshot: −35
16*: −36
21_var_snapshot: −37
21*: −38
27_var_snapshot: −39
27*: −40
31_var_snapshot: −41
31*: −42
34_var_snapshot: −43
30: −44
26*: −45
26: −46
26_var_snapshot: −47
29: −48
24: −49
22: −50
8*: −51
3*: −52
3: −53
34*: −54

29.1.1.4.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.1.1.5 Cut-Point Subproblem 5/10

Here we consider cut-point transition 95.

29.1.1.5.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0
1: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
22: 1 ≤ 0
23: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
25: TRUE
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
33: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
35: ip_0 + n_0 ≤ 0
36: 1 ≤ 0
37: TRUE
38: TRUE
39: TRUE
40: TRUE
41: TRUE
42: TRUE
1: 1 ≤ 0
23: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
36: 1 ≤ 0
22: FALSE
24: FALSE
26: FALSE
29: FALSE
30: FALSE
34: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: FALSE
8_var_snapshot: 1 ≤ 0
8*: 1 ≤ 0
16_var_snapshot: 1 ≤ 0
16*: 1 ≤ 0
21_var_snapshot: 1 ≤ 0
21*: 1 ≤ 0
26_var_snapshot: FALSE
26*: FALSE
27_var_snapshot: 1 ≤ 0
27*: 1 ≤ 0
31_var_snapshot: 1 ≤ 0
31*: 1 ≤ 0
34_var_snapshot: FALSE
34*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.1.5.2 Transition Removal

We remove transition 96 using the following ranking functions, which are bounded by −56.

1: −1
23: −2
27: −3
28: −4
31: −5
32: −6
0: −7
2: −8
4: −9
5: −10
6: −11
7: −12
8: −13
9: −14
10: −15
11: −16
12: −17
13: −18
14: −19
15: −20
16: −21
17: −22
18: −23
19: −24
20: −25
21: −26
36: −27
34: −28
1_var_snapshot: −29
1*: −30
2_var_snapshot: −31
2*: −32
3_var_snapshot: −33
8_var_snapshot: −34
16_var_snapshot: −35
16*: −36
21_var_snapshot: −37
21*: −38
27_var_snapshot: −39
27*: −40
31_var_snapshot: −41
31*: −42
34_var_snapshot: −43
30: −44
26*: −45
26: −46
26_var_snapshot: −47
29: −48
24: −49
22: −50
8*: −51
3*: −52
3: −53
34*: −54

29.1.1.5.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.1.1.6 Cut-Point Subproblem 6/10

Here we consider cut-point transition 102.

29.1.1.6.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0
1: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
22: 1 ≤ 0
23: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
25: TRUE
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
33: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
35: ip_0 + n_0 ≤ 0
36: 1 ≤ 0
37: TRUE
38: TRUE
39: TRUE
40: TRUE
41: TRUE
42: TRUE
1: 1 ≤ 0
23: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
36: 1 ≤ 0
22: FALSE
24: FALSE
26: FALSE
29: FALSE
30: FALSE
34: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: FALSE
8_var_snapshot: 1 ≤ 0
8*: 1 ≤ 0
16_var_snapshot: 1 ≤ 0
16*: 1 ≤ 0
21_var_snapshot: 1 ≤ 0
21*: 1 ≤ 0
26_var_snapshot: FALSE
26*: FALSE
27_var_snapshot: 1 ≤ 0
27*: 1 ≤ 0
31_var_snapshot: 1 ≤ 0
31*: 1 ≤ 0
34_var_snapshot: FALSE
34*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.1.6.2 Transition Removal

We remove transition 103 using the following ranking functions, which are bounded by −56.

1: −1
23: −2
27: −3
28: −4
31: −5
32: −6
0: −7
2: −8
4: −9
5: −10
6: −11
7: −12
8: −13
9: −14
10: −15
11: −16
12: −17
13: −18
14: −19
15: −20
16: −21
17: −22
18: −23
19: −24
20: −25
21: −26
36: −27
34: −28
1_var_snapshot: −29
1*: −30
2_var_snapshot: −31
2*: −32
3_var_snapshot: −33
8_var_snapshot: −34
16_var_snapshot: −35
16*: −36
21_var_snapshot: −37
21*: −38
27_var_snapshot: −39
27*: −40
31_var_snapshot: −41
31*: −42
34_var_snapshot: −43
30: −44
26*: −45
26: −46
26_var_snapshot: −47
29: −48
24: −49
22: −50
8*: −51
3*: −52
3: −53
34*: −54

29.1.1.6.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.1.1.7 Cut-Point Subproblem 7/10

Here we consider cut-point transition 109.

29.1.1.7.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0
1: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
22: 1 ≤ 0
23: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
25: TRUE
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
33: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
35: ip_0 + n_0 ≤ 0
36: 1 ≤ 0
37: TRUE
38: TRUE
39: TRUE
40: TRUE
41: TRUE
42: TRUE
1: 1 ≤ 0
23: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
36: 1 ≤ 0
22: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: FALSE
34: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: 1 ≤ 0
8_var_snapshot: 1 ≤ 0
8*: 1 ≤ 0
16_var_snapshot: 1 ≤ 0
16*: 1 ≤ 0
21_var_snapshot: 1 ≤ 0
21*: 1 ≤ 0
26_var_snapshot: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
26*: FALSE
27_var_snapshot: 1 ≤ 0
27*: 1 ≤ 0
31_var_snapshot: 1 ≤ 0
31*: 1 ≤ 0
34_var_snapshot: FALSE
34*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.1.7.2 Transition Removal

We remove transition 110 using the following ranking functions, which are bounded by −56.

1: −1
23: −2
27: −3
28: −4
31: −5
32: −6
0: −7
2: −8
3: −9
4: −10
5: −11
6: −12
7: −13
8: −14
9: −15
10: −16
11: −17
12: −18
13: −19
14: −20
15: −21
16: −22
17: −23
18: −24
19: −25
20: −26
21: −27
36: −28
34: −29
1_var_snapshot: −30
1*: −31
2_var_snapshot: −32
2*: −33
3_var_snapshot: −34
8_var_snapshot: −35
8*: −36
16_var_snapshot: −37
16*: −38
21_var_snapshot: −39
21*: −40
27_var_snapshot: −41
27*: −42
31_var_snapshot: −43
31*: −44
34_var_snapshot: −45
30: −46
26*: −47
26: −48
26_var_snapshot: −49
29: −50
24: −51
22: −52
3*: −53
34*: −54

29.1.1.7.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.1.1.8 Cut-Point Subproblem 8/10

Here we consider cut-point transition 116.

29.1.1.8.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0
1: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
22: 1 ≤ 0
23: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
25: TRUE
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
33: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
35: ip_0 + n_0 ≤ 0
36: 1 ≤ 0
37: TRUE
38: TRUE
39: TRUE
40: TRUE
41: TRUE
42: TRUE
1: 1 ≤ 0
23: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
36: 1 ≤ 0
22: FALSE
24: FALSE
26: FALSE
29: FALSE
30: FALSE
34: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: FALSE
8_var_snapshot: 1 ≤ 0
8*: 1 ≤ 0
16_var_snapshot: 1 ≤ 0
16*: 1 ≤ 0
21_var_snapshot: 1 ≤ 0
21*: 1 ≤ 0
26_var_snapshot: FALSE
26*: FALSE
27_var_snapshot: 1 ≤ 0
27*: 1 ≤ 0
31_var_snapshot: 1 ≤ 0
31*: 1 ≤ 0
34_var_snapshot: FALSE
34*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.1.8.2 Transition Removal

We remove transition 117 using the following ranking functions, which are bounded by −56.

1: −1
23: −2
27: −3
28: −4
31: −5
32: −6
0: −7
2: −8
4: −9
5: −10
6: −11
7: −12
8: −13
9: −14
10: −15
11: −16
12: −17
13: −18
14: −19
15: −20
16: −21
17: −22
18: −23
19: −24
20: −25
21: −26
36: −27
34: −28
1_var_snapshot: −29
1*: −30
2_var_snapshot: −31
2*: −32
3_var_snapshot: −33
8_var_snapshot: −34
16_var_snapshot: −35
16*: −36
21_var_snapshot: −37
21*: −38
27_var_snapshot: −39
27*: −40
31_var_snapshot: −41
31*: −42
34_var_snapshot: −43
30: −44
26*: −45
26: −46
26_var_snapshot: −47
29: −48
24: −49
22: −50
8*: −51
3*: −52
3: −53
34*: −54

29.1.1.8.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.1.1.9 Cut-Point Subproblem 9/10

Here we consider cut-point transition 123.

29.1.1.9.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0
1: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
22: 1 ≤ 0
23: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
25: TRUE
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
33: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
35: ip_0 + n_0 ≤ 0
36: 1 ≤ 0
37: TRUE
38: TRUE
39: TRUE
40: TRUE
41: TRUE
42: TRUE
1: 1 ≤ 0
23: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
36: 1 ≤ 0
22: FALSE
24: FALSE
26: FALSE
29: FALSE
30: FALSE
34: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: FALSE
8_var_snapshot: 1 ≤ 0
8*: 1 ≤ 0
16_var_snapshot: 1 ≤ 0
16*: 1 ≤ 0
21_var_snapshot: 1 ≤ 0
21*: 1 ≤ 0
26_var_snapshot: FALSE
26*: FALSE
27_var_snapshot: 1 ≤ 0
27*: 1 ≤ 0
31_var_snapshot: 1 ≤ 0
31*: 1 ≤ 0
34_var_snapshot: FALSE
34*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.1.9.2 Transition Removal

We remove transition 124 using the following ranking functions, which are bounded by −56.

1: −1
23: −2
27: −3
28: −4
31: −5
32: −6
0: −7
2: −8
4: −9
5: −10
6: −11
7: −12
8: −13
9: −14
10: −15
11: −16
12: −17
13: −18
14: −19
15: −20
16: −21
17: −22
18: −23
19: −24
20: −25
21: −26
36: −27
34: −28
1_var_snapshot: −29
1*: −30
2_var_snapshot: −31
2*: −32
3_var_snapshot: −33
8_var_snapshot: −34
16_var_snapshot: −35
16*: −36
21_var_snapshot: −37
21*: −38
27_var_snapshot: −39
27*: −40
31_var_snapshot: −41
31*: −42
34_var_snapshot: −43
30: −44
26*: −45
26: −46
26_var_snapshot: −47
29: −48
24: −49
22: −50
8*: −51
3*: −52
3: −53
34*: −54

29.1.1.9.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.1.1.10 Cut-Point Subproblem 10/10

Here we consider cut-point transition 130.

29.1.1.10.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0
1: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
22: 1 ≤ 0
23: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
25: TRUE
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
33: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
35: ip_0 + n_0 ≤ 0
36: 1 ≤ 0
37: TRUE
38: TRUE
39: TRUE
40: TRUE
41: TRUE
42: TRUE
1: 1 ≤ 0
23: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
31: 1 ≤ 0
32: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: 1 ≤ 0
7: 1 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
10: 1 ≤ 0
11: 1 ≤ 0
12: 1 ≤ 0
13: 1 ≤ 0
14: 1 ≤ 0
15: 1 ≤ 0
16: 1 ≤ 0
17: 1 ≤ 0
18: 1 ≤ 0
19: 1 ≤ 0
20: 1 ≤ 0
21: 1 ≤ 0
36: 1 ≤ 0
22: 1 ≤ 0
24: sm_0 ≤ 0sm_0 ≤ 0
26: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: ip_0 + n_0 ≤ 0
34: ip_0 + n_0 ≤ 0
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: 1 ≤ 0
8_var_snapshot: 1 ≤ 0
8*: 1 ≤ 0
16_var_snapshot: 1 ≤ 0
16*: 1 ≤ 0
21_var_snapshot: 1 ≤ 0
21*: 1 ≤ 0
26_var_snapshot: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
26*: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
27_var_snapshot: 1 ≤ 0
27*: 1 ≤ 0
31_var_snapshot: 1 ≤ 0
31*: 1 ≤ 0
34_var_snapshot: ip_0 + n_0 ≤ 0
34*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.1.10.2 Transition Removal

We remove transition 131 using the following ranking functions, which are bounded by −56.

1: −1
23: −2
27: −3
28: −4
31: −5
32: −6
0: −7
2: −8
3: −9
4: −10
5: −11
6: −12
7: −13
8: −14
9: −15
10: −16
11: −17
12: −18
13: −19
14: −20
15: −21
16: −22
17: −23
18: −24
19: −25
20: −26
21: −27
36: −28
34: −29
1_var_snapshot: −30
1*: −31
2_var_snapshot: −32
2*: −33
3_var_snapshot: −34
8_var_snapshot: −35
8*: −36
16_var_snapshot: −37
16*: −38
21_var_snapshot: −39
21*: −40
27_var_snapshot: −41
27*: −42
31_var_snapshot: −43
31*: −44
34_var_snapshot: −45
30: −46
26*: −47
26: −48
26_var_snapshot: −49
29: −50
24: −51
22: −52
3*: −53
34*: −54

29.1.1.10.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.2 SCC Subproblem 2/3

Here we consider the SCC { 33, 35, 35_var_snapshot, 35* }.

29.2.1 Transition Removal

We remove transition 46 using the following ranking functions, which are bounded by −2.

33: −1 − 4⋅ip_0 + 4⋅n_0
35: 1 − 4⋅ip_0 + 4⋅n_0
35_var_snapshot: −4⋅ip_0 + 4⋅n_0
35*: 2 − 4⋅ip_0 + 4⋅n_0

29.2.2 Transition Removal

We remove transitions 138, 140, 58 using the following ranking functions, which are bounded by −2.

33: −2
35: 0
35_var_snapshot: −1
35*: 1

29.2.3 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

29.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 137.

29.2.3.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.3 SCC Subproblem 3/3

Here we consider the SCC { 37, 38, 39, 40, 38_var_snapshot, 38*, 39_var_snapshot, 39* }.

29.3.1 Transition Removal

We remove transition 51 using the following ranking functions, which are bounded by 0.

37: −2⋅ip_0 + 2⋅n_0
38: 1 − 2⋅ip_0 + 2⋅n_0
39: −2⋅ip_0 + 2⋅n_0
40: 1 − 2⋅ip_0 + 2⋅n_0
38_var_snapshot: 1 − 2⋅ip_0 + 2⋅n_0
38*: 1 − 2⋅ip_0 + 2⋅n_0
39_var_snapshot: −2⋅ip_0 + 2⋅n_0
39*: −2⋅ip_0 + 2⋅n_0

29.3.2 Transition Removal

We remove transition 49 using the following ranking functions, which are bounded by −2.

37: −1 − 4⋅iq_0 + 4⋅n_0
38: −3 − 4⋅iq_0 + 4⋅n_0
39: 1 − 4⋅iq_0 + 4⋅n_0
40: −5 − 4⋅iq_0 + 4⋅n_0
38_var_snapshot: −4 − 4⋅iq_0 + 4⋅n_0
38*: −2 − 4⋅iq_0 + 4⋅n_0
39_var_snapshot: −4⋅iq_0 + 4⋅n_0
39*: 2 − 4⋅iq_0 + 4⋅n_0

29.3.3 Transition Removal

We remove transitions 145, 147, 152, 154, 48, 52, 55 using the following ranking functions, which are bounded by −5.

37: −1
38: −3
39: 1
40: −5
38_var_snapshot: −4
38*: −2
39_var_snapshot: 0
39*: 2

29.3.4 Splitting Cut-Point Transitions

We consider 2 subproblems corresponding to sets of cut-point transitions as follows.

29.3.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 144.

29.3.4.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

29.3.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 151.

29.3.4.2.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

Tool configuration

T2Cert