LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
4 29 4: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0
5 36 5: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0
7 43 7: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0
10 50 10: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0
12 57 12: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 1, 2, 13, 24, 26, 27, 28 using the following ranking functions, which are bounded by −25.

18: 0
17: 0
0: 0
1: 0
3: 0
4: 0
5: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 0
2: 0
18: −7
17: −8
0: −9
1: −10
3: −11
4: −11
5: −11
6: −11
7: −11
8: −11
9: −11
10: −11
11: −11
12: −11
13: −11
14: −11
15: −11
16: −11
4_var_snapshot: −11
4*: −11
5_var_snapshot: −11
5*: −11
7_var_snapshot: −11
7*: −11
10_var_snapshot: −11
10*: −11
12_var_snapshot: −11
12*: −11
2: −23

3 Location Addition

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

4* 32 4: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

4 Location Addition

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

4 30 4_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

5 Location Addition

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

5* 39 5: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

6 Location Addition

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

5 37 5_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

7 Location Addition

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

7* 46 7: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

8 Location Addition

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

7 44 7_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

9 Location Addition

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

10* 53 10: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

10 Location Addition

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

10 51 10_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

11 Location Addition

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

12* 60 12: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

12 Location Addition

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

12 58 12_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0sxn_post + sxn_post ≤ 0sxn_postsxn_post ≤ 0sxn_0 + sxn_0 ≤ 0sxn_0sxn_0 ≤ 0shn_post + shn_post ≤ 0shn_postshn_post ≤ 0shn_0 + shn_0 ≤ 0shn_0shn_0 ≤ 0sgn_post + sgn_post ≤ 0sgn_postsgn_post ≤ 0sgn_0 + sgn_0 ≤ 0sgn_0sgn_0 ≤ 0sgd_post + sgd_post ≤ 0sgd_postsgd_post ≤ 0sgd_0 + sgd_0 ≤ 0sgd_0sgd_0 ≤ 0sd_post + sd_post ≤ 0sd_postsd_post ≤ 0sd_0 + sd_0 ≤ 0sd_0sd_0 ≤ 0qt2_post + qt2_post ≤ 0qt2_postqt2_post ≤ 0qt2_0 + qt2_0 ≤ 0qt2_0qt2_0 ≤ 0qt1_post + qt1_post ≤ 0qt1_postqt1_post ≤ 0qt1_0 + qt1_0 ≤ 0qt1_0qt1_0 ≤ 0qq_post + qq_post ≤ 0qq_postqq_post ≤ 0qq_0 + qq_0 ≤ 0qq_0qq_0 ≤ 0pt2_post + pt2_post ≤ 0pt2_postpt2_post ≤ 0pt2_0 + pt2_0 ≤ 0pt2_0pt2_0 ≤ 0pt1_post + pt1_post ≤ 0pt1_postpt1_post ≤ 0pt1_0 + pt1_0 ≤ 0pt1_0pt1_0 ≤ 0pp_post + pp_post ≤ 0pp_postpp_post ≤ 0pp_0 + pp_0 ≤ 0pp_0pp_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0m2_post + m2_post ≤ 0m2_postm2_post ≤ 0m2_0 + m2_0 ≤ 0m2_0m2_0 ≤ 0m1_post + m1_post ≤ 0m1_postm1_post ≤ 0m1_0 + m1_0 ≤ 0m1_0m1_0 ≤ 0k_post + k_post ≤ 0k_postk_post ≤ 0k_0 + k_0 ≤ 0k_0k_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0

13 SCC Decomposition

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

13.1 SCC Subproblem 1/1

Here we consider the SCC { 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 4_var_snapshot, 4*, 5_var_snapshot, 5*, 7_var_snapshot, 7*, 10_var_snapshot, 10*, 12_var_snapshot, 12* }.

13.1.1 Transition Removal

We remove transition 25 using the following ranking functions, which are bounded by −1.

3: −16 − 19⋅m_0 + 19⋅n_0
4: 1 − 19⋅m_0 + 19⋅n_0
5: −16 − 19⋅m_0 + 19⋅n_0
6: −19⋅m_0 + 19⋅n_0
7: −10 − 19⋅m_0 + 19⋅n_0
8: −10 − 19⋅m_0 + 19⋅n_0
9: −15 − 19⋅m_0 + 19⋅n_0
10: −15 − 19⋅m_0 + 19⋅n_0
11: −14 − 19⋅m_0 + 19⋅n_0
12: −12 − 19⋅m_0 + 19⋅n_0
13: −12 − 19⋅m_0 + 19⋅n_0
14: −13 − 19⋅m_0 + 19⋅n_0
15: −11 − 19⋅m_0 + 19⋅n_0
16: −10 − 19⋅m_0 + 19⋅n_0
4_var_snapshot: 1 − 19⋅m_0 + 19⋅n_0
4*: 2 − 19⋅m_0 + 19⋅n_0
5_var_snapshot: −16 − 19⋅m_0 + 19⋅n_0
5*: −16 − 19⋅m_0 + 19⋅n_0
7_var_snapshot: −10 − 19⋅m_0 + 19⋅n_0
7*: −10 − 19⋅m_0 + 19⋅n_0
10_var_snapshot: −15 − 19⋅m_0 + 19⋅n_0
10*: −15 − 19⋅m_0 + 19⋅n_0
12_var_snapshot: −12 − 19⋅m_0 + 19⋅n_0
12*: −12 − 19⋅m_0 + 19⋅n_0

13.1.2 Transition Removal

We remove transitions 7, 9, 11, 12, 14, 16, 19, 20, 21 using the following ranking functions, which are bounded by −5.

3: −8⋅j_0 + 3⋅k_0 − 3⋅m_0
4: 1 − 8⋅j_0 + 3⋅k_0 − 3⋅m_post
5: 2 − 8⋅j_0 + 3⋅k_0 − 3⋅m_0
6: −1 − 8⋅j_0 + 3⋅k_0 − 3⋅m_post
7: 2
8: 2
9: −4
10: −4
11: −3
12: −1
13: −1
14: −2
15: 0
16: 1
4_var_snapshot: −8⋅j_0 + 3⋅k_0 − 3⋅m_post
4*: 2 − 8⋅j_0 + 3⋅k_0 − 3⋅m_post
5_var_snapshot: 1 − 8⋅j_0 + 3⋅k_0 − 3⋅m_0
5*: 3 − 8⋅j_0 + 3⋅k_0 − 3⋅m_0
7_var_snapshot: 2
7*: 2
10_var_snapshot: −4
10*: −4
12_var_snapshot: −1
12*: −1

13.1.3 Transition Removal

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

3: −1 − j_0 + 3⋅k_0 + m2_0
4: −3 − j_0 + 3⋅k_0 + m2_0
5: 1 − j_0 + 3⋅k_0 + m2_0
6: −5 − j_0 + 3⋅k_0 + m2_0
7: 1 − 4⋅j_0 + 4⋅m_0
8: −1 − 4⋅j_0 + 4⋅m_0
9: −2 − 3⋅j_0 + 3⋅m_0
10: −3⋅j_0 + 3⋅m_0
11: 0
12: −3⋅j_0 + 3⋅m_0
13: −2 − 3⋅j_0 + 3⋅m_0
14: 0
15: 0
16: 0
4_var_snapshot: −4 − j_0 + 3⋅k_0 + m2_0
4*: −2 − j_0 + 3⋅k_0 + m2_0
5_var_snapshot: j_0 + 3⋅k_0 + m2_0
5*: 2 − j_0 + 3⋅k_0 + m2_0
7_var_snapshot: −4⋅j_0 + 4⋅m_0
7*: 2 − 4⋅j_0 + 4⋅m_0
10_var_snapshot: −1 − 3⋅j_0 + 3⋅m_0
10*: 1 − 3⋅j_0 + 3⋅m_0
12_var_snapshot: −1 − 3⋅j_0 + 3⋅m_0
12*: 1 − 3⋅j_0 + 3⋅m_0

13.1.4 Transition Removal

We remove transitions 44, 46, 6, 18 using the following ranking functions, which are bounded by −2.

3: −1 − 4⋅j_0 + 4⋅m2_0
4: −3 − 4⋅j_0 + 4⋅m2_0
5: 1 − 4⋅j_0 + 4⋅m2_0
6: −5 − 4⋅j_0 + 4⋅m2_0
7: 0
8: −2
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 1
4_var_snapshot: −4 − 4⋅j_0 + 4⋅m2_0
4*: −2 − 4⋅j_0 + 4⋅m2_0
5_var_snapshot: −4⋅j_0 + 4⋅m2_0
5*: 2 − 4⋅j_0 + 4⋅m2_0
7_var_snapshot: −1
7*: 1
10_var_snapshot: 0
10*: 0
12_var_snapshot: 0
12*: 0

13.1.5 Transition Removal

We remove transition 15 using the following ranking functions, which are bounded by −1.

3: −1 − 2⋅j_0 + k_0 + 2⋅m2_0
4: −3 − 2⋅j_0 + k_0 + 2⋅m2_0
5: −2⋅j_0 + k_0 + 2⋅m2_0
6: −5 − 2⋅j_0 + k_0 + 2⋅m2_0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 1 − 2⋅j_0 + 2⋅m_0
13: −2⋅j_0 + 2⋅m_0
14: 0
15: 0
16: 0
4_var_snapshot: −4 − 2⋅j_0 + k_0 + 2⋅m2_0
4*: −2 − 2⋅j_0 + k_0 + 2⋅m2_0
5_var_snapshot: −2⋅j_0 + k_0 + 2⋅m2_0
5*: 1 − 2⋅j_0 + k_0 + 2⋅m2_0
7_var_snapshot: 0
7*: 0
10_var_snapshot: 0
10*: 0
12_var_snapshot: −2⋅j_0 + 2⋅m_0
12*: 1 − 2⋅j_0 + 2⋅m_0

13.1.6 Transition Removal

We remove transitions 58, 60, 8, 10 using the following ranking functions, which are bounded by −3.

3: −1 − 3⋅j_0 + 3⋅m2_0
4: −3 − 3⋅j_0 + 3⋅m2_0
5: 1 − 3⋅j_0 + 3⋅m2_0
6: −5 − 3⋅j_0 + 3⋅m2_0
7: 0
8: 0
9: −2 − 3⋅j_0 + 3⋅m_0
10: −1 − 3⋅j_0 + 3⋅m_0
11: 0
12: 0
13: −2
14: 0
15: 0
16: 0
4_var_snapshot: −4 − 3⋅j_0 + 3⋅m2_0
4*: −2 − 3⋅j_0 + 3⋅m2_0
5_var_snapshot: −3⋅j_0 + 3⋅m2_0
5*: 2 − 3⋅j_0 + 3⋅m2_0
7_var_snapshot: 0
7*: 0
10_var_snapshot: −2 − 3⋅j_0 + 3⋅m_0
10*: −3⋅j_0 + 3⋅m_0
12_var_snapshot: −1
12*: 1

13.1.7 Transition Removal

We remove transitions 51, 53, 17 using the following ranking functions, which are bounded by −2.

3: −1 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
4: −3 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
5: 1 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
6: −5 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
7: 0
8: 0
9: −2
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 0
4_var_snapshot: −4 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
4*: −2 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
5_var_snapshot: −2⋅j_0 + 2⋅k_0 + 2⋅m2_0
5*: 2 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
7_var_snapshot: 0
7*: 0
10_var_snapshot: −1
10*: 1
12_var_snapshot: 0
12*: 0

13.1.8 Transition Removal

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

3: −1 − 4⋅j_0 + 4⋅m2_0
4: −3 − 4⋅j_0 + 4⋅m2_0
5: 1 − 4⋅j_0 + 4⋅m2_0
6: −5 − 4⋅j_0 + 4⋅m2_0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 0
4_var_snapshot: −4 − 4⋅j_0 + 4⋅m2_0
4*: −2 − 4⋅j_0 + 4⋅m2_0
5_var_snapshot: −4⋅j_0 + 4⋅m2_0
5*: 2 − 4⋅j_0 + 4⋅m2_0
7_var_snapshot: 0
7*: 0
10_var_snapshot: 0
10*: 0
12_var_snapshot: 0
12*: 0

13.1.9 Transition Removal

We remove transitions 30, 32, 37, 39, 3, 5, 23 using the following ranking functions, which are bounded by −5.

3: −1
4: −3
5: 1
6: −5
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 0
4_var_snapshot: −4
4*: −2
5_var_snapshot: 0
5*: 2
7_var_snapshot: 0
7*: 0
10_var_snapshot: 0
10*: 0
12_var_snapshot: 0
12*: 0

13.1.10 Splitting Cut-Point Transitions

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

13.1.10.1 Cut-Point Subproblem 1/5

Here we consider cut-point transition 29.

13.1.10.1.1 Splitting Cut-Point Transitions

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

13.1.10.2 Cut-Point Subproblem 2/5

Here we consider cut-point transition 36.

13.1.10.2.1 Splitting Cut-Point Transitions

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

13.1.10.3 Cut-Point Subproblem 3/5

Here we consider cut-point transition 43.

13.1.10.3.1 Splitting Cut-Point Transitions

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

13.1.10.4 Cut-Point Subproblem 4/5

Here we consider cut-point transition 50.

13.1.10.4.1 Splitting Cut-Point Transitions

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

13.1.10.5 Cut-Point Subproblem 5/5

Here we consider cut-point transition 57.

13.1.10.5.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert