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
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
6 81 6: 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
7 88 7: 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
15 95 15: 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
20 102 20: 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
22 109 22: 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
24 116 24: 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
29 123 29: 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
30 130 30: 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
33 137 33: 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
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
40 151 40: 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
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 32, 39, 47, 50, 51, 66 using the following ranking functions, which are bounded by −41.

42: 0
34: 0
5: 0
6: 0
7: 0
23: 0
24: 0
35: 0
0: 0
1: 0
2: 0
3: 0
4: 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
25: 0
26: 0
28: 0
29: 0
30: 0
31: 0
32: 0
33: 0
36: 0
37: 0
38: 0
39: 0
40: 0
41: 0
27: 0
42: −7
34: −8
5: −9
6: −9
7: −9
23: −9
6_var_snapshot: −9
6*: −9
7_var_snapshot: −9
7*: −9
24: −12
35: −12
24_var_snapshot: −12
24*: −12
1: −13
37: −13
38: −13
39: −13
40: −13
41: −13
0: −13
2: −13
3: −13
4: −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
22: −13
36: −13
25: −13
26: −13
28: −13
29: −13
30: −13
31: −13
32: −13
33: −13
1_var_snapshot: −13
1*: −13
2_var_snapshot: −13
2*: −13
15_var_snapshot: −13
15*: −13
20_var_snapshot: −13
20*: −13
22_var_snapshot: −13
22*: −13
29_var_snapshot: −13
29*: −13
30_var_snapshot: −13
30*: −13
33_var_snapshot: −13
33*: −13
38_var_snapshot: −13
38*: −13
40_var_snapshot: −13
40*: −13
27: −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

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

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

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

7 Location Addition

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

6* 84 6: 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

8 Location Addition

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

6 82 6_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

9 Location Addition

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

7* 91 7: 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

10 Location Addition

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

7 89 7_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

11 Location Addition

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

15* 98 15: 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

12 Location Addition

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

15 96 15_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

13 Location Addition

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

20* 105 20: 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

14 Location Addition

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

20 103 20_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

15 Location Addition

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

22* 112 22: 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

16 Location Addition

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

22 110 22_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

17 Location Addition

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

24* 119 24: 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

18 Location Addition

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

24 117 24_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

19 Location Addition

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

29* 126 29: 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

20 Location Addition

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

29 124 29_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

21 Location Addition

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

30* 133 30: 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

22 Location Addition

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

30 131 30_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

23 Location Addition

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

33* 140 33: 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

24 Location Addition

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

33 138 33_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

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

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

27 Location Addition

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

40* 154 40: 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

28 Location Addition

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

40 152 40_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

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, 37, 38, 39, 40, 41, 0, 2, 3, 4, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 36, 25, 26, 28, 29, 30, 31, 32, 33, 1_var_snapshot, 1*, 2_var_snapshot, 2*, 15_var_snapshot, 15*, 20_var_snapshot, 20*, 22_var_snapshot, 22*, 29_var_snapshot, 29*, 30_var_snapshot, 30*, 33_var_snapshot, 33*, 38_var_snapshot, 38*, 40_var_snapshot, 40* }.

29.1.1 Transition Removal

We remove transition 48 using the following ranking functions, which are bounded by −3696.

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

29.1.2 Splitting Cut-Point Transitions

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

29.1.2.1 Cut-Point Subproblem 1/10

Here we consider cut-point transition 67.

29.1.2.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: TRUE
6: TRUE
7: TRUE
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: TRUE
24: TRUE
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
27: TRUE
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: ip_0 + n_0 ≤ 0
33: ip_0 + n_0 ≤ 0
34: TRUE
35: TRUE
36: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
42: TRUE
1: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 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
36: 1 ≤ 0
25: FALSE
26: FALSE
28: 1 ≤ 0
29: FALSE
30: 1 ≤ 0
31: FALSE
32: FALSE
33: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
15_var_snapshot: 1 ≤ 0
15*: 1 ≤ 0
20_var_snapshot: 1 ≤ 0
20*: 1 ≤ 0
22_var_snapshot: 1 ≤ 0
22*: 1 ≤ 0
29_var_snapshot: FALSE
29*: 1 ≤ 0
30_var_snapshot: 1 ≤ 0
30*: FALSE
33_var_snapshot: FALSE
33*: 1 ≤ 0
38_var_snapshot: 1 ≤ 0
38*: 1 ≤ 0
40_var_snapshot: 1 ≤ 0
40*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.2.1.2 Transition Removal

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

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

29.1.2.1.3 Splitting Cut-Point Transitions

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

29.1.2.2 Cut-Point Subproblem 2/10

Here we consider cut-point transition 74.

29.1.2.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: TRUE
6: TRUE
7: TRUE
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: TRUE
24: TRUE
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
27: TRUE
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: ip_0 + n_0 ≤ 0
33: ip_0 + n_0 ≤ 0
34: TRUE
35: TRUE
36: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
42: TRUE
1: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 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
36: 1 ≤ 0
25: FALSE
26: FALSE
28: 1 ≤ 0
29: FALSE
30: 1 ≤ 0
31: FALSE
32: FALSE
33: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
15_var_snapshot: 1 ≤ 0
15*: 1 ≤ 0
20_var_snapshot: 1 ≤ 0
20*: 1 ≤ 0
22_var_snapshot: 1 ≤ 0
22*: 1 ≤ 0
29_var_snapshot: FALSE
29*: 1 ≤ 0
30_var_snapshot: 1 ≤ 0
30*: FALSE
33_var_snapshot: FALSE
33*: 1 ≤ 0
38_var_snapshot: 1 ≤ 0
38*: 1 ≤ 0
40_var_snapshot: 1 ≤ 0
40*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.2.2.2 Transition Removal

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

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

29.1.2.2.3 Splitting Cut-Point Transitions

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

29.1.2.3 Cut-Point Subproblem 3/10

Here we consider cut-point transition 95.

29.1.2.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: TRUE
6: TRUE
7: TRUE
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: TRUE
24: TRUE
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
27: TRUE
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: ip_0 + n_0 ≤ 0
33: ip_0 + n_0 ≤ 0
34: TRUE
35: TRUE
36: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
42: TRUE
1: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 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
36: 1 ≤ 0
25: FALSE
26: FALSE
28: 1 ≤ 0
29: FALSE
30: 1 ≤ 0
31: FALSE
32: FALSE
33: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
15_var_snapshot: 1 ≤ 0
15*: 1 ≤ 0
20_var_snapshot: 1 ≤ 0
20*: 1 ≤ 0
22_var_snapshot: 1 ≤ 0
22*: 1 ≤ 0
29_var_snapshot: FALSE
29*: 1 ≤ 0
30_var_snapshot: 1 ≤ 0
30*: FALSE
33_var_snapshot: FALSE
33*: 1 ≤ 0
38_var_snapshot: 1 ≤ 0
38*: 1 ≤ 0
40_var_snapshot: 1 ≤ 0
40*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.2.3.2 Transition Removal

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

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

29.1.2.3.3 Splitting Cut-Point Transitions

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

29.1.2.4 Cut-Point Subproblem 4/10

Here we consider cut-point transition 102.

29.1.2.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: TRUE
6: TRUE
7: TRUE
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: TRUE
24: TRUE
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
27: TRUE
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: ip_0 + n_0 ≤ 0
33: ip_0 + n_0 ≤ 0
34: TRUE
35: TRUE
36: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
42: TRUE
1: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 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
36: 1 ≤ 0
25: FALSE
26: FALSE
28: 1 ≤ 0
29: FALSE
30: 1 ≤ 0
31: FALSE
32: FALSE
33: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
15_var_snapshot: 1 ≤ 0
15*: 1 ≤ 0
20_var_snapshot: 1 ≤ 0
20*: 1 ≤ 0
22_var_snapshot: 1 ≤ 0
22*: 1 ≤ 0
29_var_snapshot: FALSE
29*: 1 ≤ 0
30_var_snapshot: 1 ≤ 0
30*: FALSE
33_var_snapshot: FALSE
33*: 1 ≤ 0
38_var_snapshot: 1 ≤ 0
38*: 1 ≤ 0
40_var_snapshot: 1 ≤ 0
40*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.2.4.2 Transition Removal

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

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

29.1.2.4.3 Splitting Cut-Point Transitions

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

29.1.2.5 Cut-Point Subproblem 5/10

Here we consider cut-point transition 109.

29.1.2.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: TRUE
6: TRUE
7: TRUE
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: TRUE
24: TRUE
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
27: TRUE
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: ip_0 + n_0 ≤ 0
33: ip_0 + n_0 ≤ 0
34: TRUE
35: TRUE
36: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
42: TRUE
1: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 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
36: 1 ≤ 0
25: FALSE
26: FALSE
28: 1 ≤ 0
29: FALSE
30: 1 ≤ 0
31: FALSE
32: FALSE
33: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
15_var_snapshot: 1 ≤ 0
15*: 1 ≤ 0
20_var_snapshot: 1 ≤ 0
20*: 1 ≤ 0
22_var_snapshot: 1 ≤ 0
22*: 1 ≤ 0
29_var_snapshot: FALSE
29*: 1 ≤ 0
30_var_snapshot: 1 ≤ 0
30*: FALSE
33_var_snapshot: FALSE
33*: 1 ≤ 0
38_var_snapshot: 1 ≤ 0
38*: 1 ≤ 0
40_var_snapshot: 1 ≤ 0
40*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.2.5.2 Transition Removal

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

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

29.1.2.5.3 Splitting Cut-Point Transitions

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

29.1.2.6 Cut-Point Subproblem 6/10

Here we consider cut-point transition 123.

29.1.2.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: TRUE
6: TRUE
7: TRUE
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: TRUE
24: TRUE
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
27: TRUE
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: ip_0 + n_0 ≤ 0
33: ip_0 + n_0 ≤ 0
34: TRUE
35: TRUE
36: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
42: TRUE
1: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 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
36: 1 ≤ 0
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: FALSE
33: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
15_var_snapshot: 1 ≤ 0
15*: 1 ≤ 0
20_var_snapshot: 1 ≤ 0
20*: 1 ≤ 0
22_var_snapshot: 1 ≤ 0
22*: 1 ≤ 0
29_var_snapshot: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
29*: 1 ≤ 0
30_var_snapshot: 1 ≤ 0
30*: 1 ≤ 0
33_var_snapshot: FALSE
33*: 1 ≤ 0
38_var_snapshot: 1 ≤ 0
38*: 1 ≤ 0
40_var_snapshot: 1 ≤ 0
40*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.2.6.2 Transition Removal

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

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

29.1.2.6.3 Splitting Cut-Point Transitions

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

29.1.2.7 Cut-Point Subproblem 7/10

Here we consider cut-point transition 130.

29.1.2.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: TRUE
6: TRUE
7: TRUE
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: TRUE
24: TRUE
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
27: TRUE
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: ip_0 + n_0 ≤ 0
33: ip_0 + n_0 ≤ 0
34: TRUE
35: TRUE
36: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
42: TRUE
1: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 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
36: 1 ≤ 0
25: FALSE
26: FALSE
28: 1 ≤ 0
29: FALSE
30: 1 ≤ 0
31: FALSE
32: FALSE
33: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
15_var_snapshot: 1 ≤ 0
15*: 1 ≤ 0
20_var_snapshot: 1 ≤ 0
20*: 1 ≤ 0
22_var_snapshot: 1 ≤ 0
22*: 1 ≤ 0
29_var_snapshot: FALSE
29*: 1 ≤ 0
30_var_snapshot: 1 ≤ 0
30*: FALSE
33_var_snapshot: FALSE
33*: 1 ≤ 0
38_var_snapshot: 1 ≤ 0
38*: 1 ≤ 0
40_var_snapshot: 1 ≤ 0
40*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.2.7.2 Transition Removal

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

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

29.1.2.7.3 Splitting Cut-Point Transitions

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

29.1.2.8 Cut-Point Subproblem 8/10

Here we consider cut-point transition 137.

29.1.2.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: TRUE
6: TRUE
7: TRUE
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: TRUE
24: TRUE
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
27: TRUE
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: ip_0 + n_0 ≤ 0
33: ip_0 + n_0 ≤ 0
34: TRUE
35: TRUE
36: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
42: TRUE
1: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 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
36: 1 ≤ 0
25: FALSE
26: FALSE
28: 1 ≤ 0
29: FALSE
30: 1 ≤ 0
31: FALSE
32: TRUE
33: TRUE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
15_var_snapshot: 1 ≤ 0
15*: 1 ≤ 0
20_var_snapshot: 1 ≤ 0
20*: 1 ≤ 0
22_var_snapshot: 1 ≤ 0
22*: 1 ≤ 0
29_var_snapshot: FALSE
29*: 1 ≤ 0
30_var_snapshot: 1 ≤ 0
30*: FALSE
33_var_snapshot: TRUE
33*: 1 ≤ 0
38_var_snapshot: 1 ≤ 0
38*: 1 ≤ 0
40_var_snapshot: 1 ≤ 0
40*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.2.8.2 Transition Removal

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

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

29.1.2.8.3 Splitting Cut-Point Transitions

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

29.1.2.9 Cut-Point Subproblem 9/10

Here we consider cut-point transition 144.

29.1.2.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: TRUE
6: TRUE
7: TRUE
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: TRUE
24: TRUE
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
27: TRUE
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: ip_0 + n_0 ≤ 0
33: ip_0 + n_0 ≤ 0
34: TRUE
35: TRUE
36: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
42: TRUE
1: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 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
36: 1 ≤ 0
25: FALSE
26: FALSE
28: 1 ≤ 0
29: FALSE
30: 1 ≤ 0
31: FALSE
32: FALSE
33: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
15_var_snapshot: 1 ≤ 0
15*: 1 ≤ 0
20_var_snapshot: 1 ≤ 0
20*: 1 ≤ 0
22_var_snapshot: 1 ≤ 0
22*: 1 ≤ 0
29_var_snapshot: FALSE
29*: 1 ≤ 0
30_var_snapshot: 1 ≤ 0
30*: FALSE
33_var_snapshot: FALSE
33*: 1 ≤ 0
38_var_snapshot: 1 ≤ 0
38*: 1 ≤ 0
40_var_snapshot: 1 ≤ 0
40*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.2.9.2 Transition Removal

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

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

29.1.2.9.3 Splitting Cut-Point Transitions

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

29.1.2.10 Cut-Point Subproblem 10/10

Here we consider cut-point transition 151.

29.1.2.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: TRUE
6: TRUE
7: TRUE
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: TRUE
24: TRUE
25: 1 ≤ 0
26: sm_0 ≤ 0sm_0 ≤ 0
27: TRUE
28: 1 ≤ 0
29: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
30: 1 ≤ 0
31: sm_0 ≤ 0ip_0 + n_0 ≤ 0sm_0 ≤ 0
32: ip_0 + n_0 ≤ 0
33: ip_0 + n_0 ≤ 0
34: TRUE
35: TRUE
36: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
42: TRUE
1: 1 ≤ 0
37: 1 ≤ 0
38: 1 ≤ 0
39: 1 ≤ 0
40: 1 ≤ 0
41: 1 ≤ 0
0: 1 ≤ 0
2: 1 ≤ 0
3: 1 ≤ 0
4: 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
36: 1 ≤ 0
25: FALSE
26: FALSE
28: 1 ≤ 0
29: FALSE
30: 1 ≤ 0
31: FALSE
32: FALSE
33: FALSE
1_var_snapshot: 1 ≤ 0
1*: 1 ≤ 0
2_var_snapshot: 1 ≤ 0
2*: 1 ≤ 0
15_var_snapshot: 1 ≤ 0
15*: 1 ≤ 0
20_var_snapshot: 1 ≤ 0
20*: 1 ≤ 0
22_var_snapshot: 1 ≤ 0
22*: 1 ≤ 0
29_var_snapshot: FALSE
29*: 1 ≤ 0
30_var_snapshot: 1 ≤ 0
30*: FALSE
33_var_snapshot: FALSE
33*: 1 ≤ 0
38_var_snapshot: 1 ≤ 0
38*: 1 ≤ 0
40_var_snapshot: 1 ≤ 0
40*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

29.1.2.10.2 Transition Removal

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

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

29.1.2.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 { 24, 35, 24_var_snapshot, 24* }.

29.2.1 Transition Removal

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

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

29.2.2 Transition Removal

We remove transitions 117, 119, 53 using the following ranking functions, which are bounded by −1.

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

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 116.

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 { 5, 6, 7, 23, 6_var_snapshot, 6*, 7_var_snapshot, 7* }.

29.3.1 Transition Removal

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

5: −2 − 5⋅ip_0 + 5⋅n_0
6: 1 − 5⋅ip_0 + 5⋅n_0
7: −2 − 5⋅ip_0 + 5⋅n_0
23: −1 − 5⋅ip_0 + 5⋅n_0
6_var_snapshot: −5⋅ip_0 + 5⋅n_0
6*: 2 − 5⋅ip_0 + 5⋅n_0
7_var_snapshot: −2 − 5⋅ip_0 + 5⋅n_0
7*: −2 − 5⋅ip_0 + 5⋅n_0

29.3.2 Transition Removal

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

5: −1 − 4⋅iq_0 + 4⋅n_0
6: −3 − 4⋅iq_0 + 4⋅n_0
7: 1 − 4⋅iq_0 + 4⋅n_0
23: −5 − 4⋅iq_0 + 4⋅n_0
6_var_snapshot: −4 − 4⋅iq_0 + 4⋅n_0
6*: −2 − 4⋅iq_0 + 4⋅n_0
7_var_snapshot: −4⋅iq_0 + 4⋅n_0
7*: 2 − 4⋅iq_0 + 4⋅n_0

29.3.3 Transition Removal

We remove transitions 82, 84, 89, 91, 5, 24, 40 using the following ranking functions, which are bounded by −5.

5: −1
6: −3
7: 1
23: −5
6_var_snapshot: −4
6*: −2
7_var_snapshot: 0
7*: 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 81.

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 88.

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