LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
1 29 1: 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
3 36 3: 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
11 50 11: 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
15 57 15: 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, 4, 5, 6, 13, 23, 25, 28 using the following ranking functions, which are bounded by −25.

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

3 Location Addition

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

1* 32 1: 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.

1 30 1_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.

3* 39 3: 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.

3 37 3_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.

11* 53 11: 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.

11 51 11_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.

15* 60 15: 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.

15 58 15_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 { 1, 2, 3, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 17, 1_var_snapshot, 1*, 3_var_snapshot, 3*, 7_var_snapshot, 7*, 11_var_snapshot, 11*, 15_var_snapshot, 15* }.

13.1.1 Transition Removal

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

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

13.1.2 Transition Removal

We remove transitions 30, 32, 1, 7, 10, 11, 12, 14, 17, 18, 19, 20, 21, 27 using the following ranking functions, which are bounded by −11.

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

13.1.3 Transition Removal

We remove transitions 8, 15 using the following ranking functions, which are bounded by −4.

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

13.1.4 Transition Removal

We remove transitions 44, 46, 9, 16, 22 using the following ranking functions, which are bounded by −2.

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

13.1.5 Transition Removal

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

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

13.1.6 Transition Removal

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

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

13.1.7 Transition Removal

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

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

13.1.8 Transition Removal

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

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

13.1.9 Transition Removal

We remove transitions 37, 39, 3 using the following ranking functions, which are bounded by −1.

1: 0
2: −1
3: 1
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
17: 0
1_var_snapshot: 0
1*: 0
3_var_snapshot: 0
3*: 2
7_var_snapshot: 0
7*: 0
11_var_snapshot: 0
11*: 0
15_var_snapshot: 0
15*: 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