LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: TRUE
1: TRUE
2: TRUE
3: TRUE
4: 1 + ctr23_0 ≤ 0
5: TRUE
6: TRUE
7: TRUE
8: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
1 11 1: z521_post + z521_post ≤ 0z521_postz521_post ≤ 0z521_0 + z521_0 ≤ 0z521_0z521_0 ≤ 0z420_post + z420_post ≤ 0z420_postz420_post ≤ 0z420_2 + z420_2 ≤ 0z420_2z420_2 ≤ 0z420_1 + z420_1 ≤ 0z420_1z420_1 ≤ 0z420_0 + z420_0 ≤ 0z420_0z420_0 ≤ 0z319_post + z319_post ≤ 0z319_postz319_post ≤ 0z319_2 + z319_2 ≤ 0z319_2z319_2 ≤ 0z319_1 + z319_1 ≤ 0z319_1z319_1 ≤ 0z319_0 + z319_0 ≤ 0z319_0z319_0 ≤ 0z218_post + z218_post ≤ 0z218_postz218_post ≤ 0z218_1 + z218_1 ≤ 0z218_1z218_1 ≤ 0z218_0 + z218_0 ≤ 0z218_0z218_0 ≤ 0z117_post + z117_post ≤ 0z117_postz117_post ≤ 0z117_2 + z117_2 ≤ 0z117_2z117_2 ≤ 0z117_1 + z117_1 ≤ 0z117_1z117_1 ≤ 0z117_0 + z117_0 ≤ 0z117_0z117_0 ≤ 0tmp712_post + tmp712_post ≤ 0tmp712_posttmp712_post ≤ 0tmp712_1 + tmp712_1 ≤ 0tmp712_1tmp712_1 ≤ 0tmp712_0 + tmp712_0 ≤ 0tmp712_0tmp712_0 ≤ 0tmp611_post + tmp611_post ≤ 0tmp611_posttmp611_post ≤ 0tmp611_1 + tmp611_1 ≤ 0tmp611_1tmp611_1 ≤ 0tmp611_0 + tmp611_0 ≤ 0tmp611_0tmp611_0 ≤ 0tmp510_post + tmp510_post ≤ 0tmp510_posttmp510_post ≤ 0tmp510_1 + tmp510_1 ≤ 0tmp510_1tmp510_1 ≤ 0tmp510_0 + tmp510_0 ≤ 0tmp510_0tmp510_0 ≤ 0tmp49_post + tmp49_post ≤ 0tmp49_posttmp49_post ≤ 0tmp49_1 + tmp49_1 ≤ 0tmp49_1tmp49_1 ≤ 0tmp49_0 + tmp49_0 ≤ 0tmp49_0tmp49_0 ≤ 0tmp38_post + tmp38_post ≤ 0tmp38_posttmp38_post ≤ 0tmp38_0 + tmp38_0 ≤ 0tmp38_0tmp38_0 ≤ 0tmp27_post + tmp27_post ≤ 0tmp27_posttmp27_post ≤ 0tmp27_0 + tmp27_0 ≤ 0tmp27_0tmp27_0 ≤ 0tmp16_post + tmp16_post ≤ 0tmp16_posttmp16_post ≤ 0tmp16_0 + tmp16_0 ≤ 0tmp16_0tmp16_0 ≤ 0tmp1316_post + tmp1316_post ≤ 0tmp1316_posttmp1316_post ≤ 0tmp1316_0 + tmp1316_0 ≤ 0tmp1316_0tmp1316_0 ≤ 0tmp1215_post + tmp1215_post ≤ 0tmp1215_posttmp1215_post ≤ 0tmp1215_0 + tmp1215_0 ≤ 0tmp1215_0tmp1215_0 ≤ 0tmp1114_post + tmp1114_post ≤ 0tmp1114_posttmp1114_post ≤ 0tmp1114_0 + tmp1114_0 ≤ 0tmp1114_0tmp1114_0 ≤ 0tmp1013_post + tmp1013_post ≤ 0tmp1013_posttmp1013_post ≤ 0tmp1013_0 + tmp1013_0 ≤ 0tmp1013_0tmp1013_0 ≤ 0tmp05_post + tmp05_post ≤ 0tmp05_posttmp05_post ≤ 0tmp05_0 + tmp05_0 ≤ 0tmp05_0tmp05_0 ≤ 0seed_post + seed_post ≤ 0seed_postseed_post ≤ 0seed_0 + seed_0 ≤ 0seed_0seed_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0ctr23_post + ctr23_post ≤ 0ctr23_postctr23_post ≤ 0ctr23_0 + ctr23_0 ≤ 0ctr23_0ctr23_0 ≤ 0___const_7_0 + ___const_7_0 ≤ 0___const_7_0___const_7_0 ≤ 0___const_64_0 + ___const_64_0 ≤ 0___const_64_0___const_64_0 ≤ 0
2 18 2: z521_post + z521_post ≤ 0z521_postz521_post ≤ 0z521_0 + z521_0 ≤ 0z521_0z521_0 ≤ 0z420_post + z420_post ≤ 0z420_postz420_post ≤ 0z420_2 + z420_2 ≤ 0z420_2z420_2 ≤ 0z420_1 + z420_1 ≤ 0z420_1z420_1 ≤ 0z420_0 + z420_0 ≤ 0z420_0z420_0 ≤ 0z319_post + z319_post ≤ 0z319_postz319_post ≤ 0z319_2 + z319_2 ≤ 0z319_2z319_2 ≤ 0z319_1 + z319_1 ≤ 0z319_1z319_1 ≤ 0z319_0 + z319_0 ≤ 0z319_0z319_0 ≤ 0z218_post + z218_post ≤ 0z218_postz218_post ≤ 0z218_1 + z218_1 ≤ 0z218_1z218_1 ≤ 0z218_0 + z218_0 ≤ 0z218_0z218_0 ≤ 0z117_post + z117_post ≤ 0z117_postz117_post ≤ 0z117_2 + z117_2 ≤ 0z117_2z117_2 ≤ 0z117_1 + z117_1 ≤ 0z117_1z117_1 ≤ 0z117_0 + z117_0 ≤ 0z117_0z117_0 ≤ 0tmp712_post + tmp712_post ≤ 0tmp712_posttmp712_post ≤ 0tmp712_1 + tmp712_1 ≤ 0tmp712_1tmp712_1 ≤ 0tmp712_0 + tmp712_0 ≤ 0tmp712_0tmp712_0 ≤ 0tmp611_post + tmp611_post ≤ 0tmp611_posttmp611_post ≤ 0tmp611_1 + tmp611_1 ≤ 0tmp611_1tmp611_1 ≤ 0tmp611_0 + tmp611_0 ≤ 0tmp611_0tmp611_0 ≤ 0tmp510_post + tmp510_post ≤ 0tmp510_posttmp510_post ≤ 0tmp510_1 + tmp510_1 ≤ 0tmp510_1tmp510_1 ≤ 0tmp510_0 + tmp510_0 ≤ 0tmp510_0tmp510_0 ≤ 0tmp49_post + tmp49_post ≤ 0tmp49_posttmp49_post ≤ 0tmp49_1 + tmp49_1 ≤ 0tmp49_1tmp49_1 ≤ 0tmp49_0 + tmp49_0 ≤ 0tmp49_0tmp49_0 ≤ 0tmp38_post + tmp38_post ≤ 0tmp38_posttmp38_post ≤ 0tmp38_0 + tmp38_0 ≤ 0tmp38_0tmp38_0 ≤ 0tmp27_post + tmp27_post ≤ 0tmp27_posttmp27_post ≤ 0tmp27_0 + tmp27_0 ≤ 0tmp27_0tmp27_0 ≤ 0tmp16_post + tmp16_post ≤ 0tmp16_posttmp16_post ≤ 0tmp16_0 + tmp16_0 ≤ 0tmp16_0tmp16_0 ≤ 0tmp1316_post + tmp1316_post ≤ 0tmp1316_posttmp1316_post ≤ 0tmp1316_0 + tmp1316_0 ≤ 0tmp1316_0tmp1316_0 ≤ 0tmp1215_post + tmp1215_post ≤ 0tmp1215_posttmp1215_post ≤ 0tmp1215_0 + tmp1215_0 ≤ 0tmp1215_0tmp1215_0 ≤ 0tmp1114_post + tmp1114_post ≤ 0tmp1114_posttmp1114_post ≤ 0tmp1114_0 + tmp1114_0 ≤ 0tmp1114_0tmp1114_0 ≤ 0tmp1013_post + tmp1013_post ≤ 0tmp1013_posttmp1013_post ≤ 0tmp1013_0 + tmp1013_0 ≤ 0tmp1013_0tmp1013_0 ≤ 0tmp05_post + tmp05_post ≤ 0tmp05_posttmp05_post ≤ 0tmp05_0 + tmp05_0 ≤ 0tmp05_0tmp05_0 ≤ 0seed_post + seed_post ≤ 0seed_postseed_post ≤ 0seed_0 + seed_0 ≤ 0seed_0seed_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0ctr23_post + ctr23_post ≤ 0ctr23_postctr23_post ≤ 0ctr23_0 + ctr23_0 ≤ 0ctr23_0ctr23_0 ≤ 0___const_7_0 + ___const_7_0 ≤ 0___const_7_0___const_7_0 ≤ 0___const_64_0 + ___const_64_0 ≤ 0___const_64_0___const_64_0 ≤ 0
5 25 5: z521_post + z521_post ≤ 0z521_postz521_post ≤ 0z521_0 + z521_0 ≤ 0z521_0z521_0 ≤ 0z420_post + z420_post ≤ 0z420_postz420_post ≤ 0z420_2 + z420_2 ≤ 0z420_2z420_2 ≤ 0z420_1 + z420_1 ≤ 0z420_1z420_1 ≤ 0z420_0 + z420_0 ≤ 0z420_0z420_0 ≤ 0z319_post + z319_post ≤ 0z319_postz319_post ≤ 0z319_2 + z319_2 ≤ 0z319_2z319_2 ≤ 0z319_1 + z319_1 ≤ 0z319_1z319_1 ≤ 0z319_0 + z319_0 ≤ 0z319_0z319_0 ≤ 0z218_post + z218_post ≤ 0z218_postz218_post ≤ 0z218_1 + z218_1 ≤ 0z218_1z218_1 ≤ 0z218_0 + z218_0 ≤ 0z218_0z218_0 ≤ 0z117_post + z117_post ≤ 0z117_postz117_post ≤ 0z117_2 + z117_2 ≤ 0z117_2z117_2 ≤ 0z117_1 + z117_1 ≤ 0z117_1z117_1 ≤ 0z117_0 + z117_0 ≤ 0z117_0z117_0 ≤ 0tmp712_post + tmp712_post ≤ 0tmp712_posttmp712_post ≤ 0tmp712_1 + tmp712_1 ≤ 0tmp712_1tmp712_1 ≤ 0tmp712_0 + tmp712_0 ≤ 0tmp712_0tmp712_0 ≤ 0tmp611_post + tmp611_post ≤ 0tmp611_posttmp611_post ≤ 0tmp611_1 + tmp611_1 ≤ 0tmp611_1tmp611_1 ≤ 0tmp611_0 + tmp611_0 ≤ 0tmp611_0tmp611_0 ≤ 0tmp510_post + tmp510_post ≤ 0tmp510_posttmp510_post ≤ 0tmp510_1 + tmp510_1 ≤ 0tmp510_1tmp510_1 ≤ 0tmp510_0 + tmp510_0 ≤ 0tmp510_0tmp510_0 ≤ 0tmp49_post + tmp49_post ≤ 0tmp49_posttmp49_post ≤ 0tmp49_1 + tmp49_1 ≤ 0tmp49_1tmp49_1 ≤ 0tmp49_0 + tmp49_0 ≤ 0tmp49_0tmp49_0 ≤ 0tmp38_post + tmp38_post ≤ 0tmp38_posttmp38_post ≤ 0tmp38_0 + tmp38_0 ≤ 0tmp38_0tmp38_0 ≤ 0tmp27_post + tmp27_post ≤ 0tmp27_posttmp27_post ≤ 0tmp27_0 + tmp27_0 ≤ 0tmp27_0tmp27_0 ≤ 0tmp16_post + tmp16_post ≤ 0tmp16_posttmp16_post ≤ 0tmp16_0 + tmp16_0 ≤ 0tmp16_0tmp16_0 ≤ 0tmp1316_post + tmp1316_post ≤ 0tmp1316_posttmp1316_post ≤ 0tmp1316_0 + tmp1316_0 ≤ 0tmp1316_0tmp1316_0 ≤ 0tmp1215_post + tmp1215_post ≤ 0tmp1215_posttmp1215_post ≤ 0tmp1215_0 + tmp1215_0 ≤ 0tmp1215_0tmp1215_0 ≤ 0tmp1114_post + tmp1114_post ≤ 0tmp1114_posttmp1114_post ≤ 0tmp1114_0 + tmp1114_0 ≤ 0tmp1114_0tmp1114_0 ≤ 0tmp1013_post + tmp1013_post ≤ 0tmp1013_posttmp1013_post ≤ 0tmp1013_0 + tmp1013_0 ≤ 0tmp1013_0tmp1013_0 ≤ 0tmp05_post + tmp05_post ≤ 0tmp05_posttmp05_post ≤ 0tmp05_0 + tmp05_0 ≤ 0tmp05_0tmp05_0 ≤ 0seed_post + seed_post ≤ 0seed_postseed_post ≤ 0seed_0 + seed_0 ≤ 0seed_0seed_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0ctr23_post + ctr23_post ≤ 0ctr23_postctr23_post ≤ 0ctr23_0 + ctr23_0 ≤ 0ctr23_0ctr23_0 ≤ 0___const_7_0 + ___const_7_0 ≤ 0___const_7_0___const_7_0 ≤ 0___const_64_0 + ___const_64_0 ≤ 0___const_64_0___const_64_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 2, 7, 9, 10 using the following ranking functions, which are bounded by −21.

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

4 Location Addition

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

1* 14 1: z521_post + z521_post ≤ 0z521_postz521_post ≤ 0z521_0 + z521_0 ≤ 0z521_0z521_0 ≤ 0z420_post + z420_post ≤ 0z420_postz420_post ≤ 0z420_2 + z420_2 ≤ 0z420_2z420_2 ≤ 0z420_1 + z420_1 ≤ 0z420_1z420_1 ≤ 0z420_0 + z420_0 ≤ 0z420_0z420_0 ≤ 0z319_post + z319_post ≤ 0z319_postz319_post ≤ 0z319_2 + z319_2 ≤ 0z319_2z319_2 ≤ 0z319_1 + z319_1 ≤ 0z319_1z319_1 ≤ 0z319_0 + z319_0 ≤ 0z319_0z319_0 ≤ 0z218_post + z218_post ≤ 0z218_postz218_post ≤ 0z218_1 + z218_1 ≤ 0z218_1z218_1 ≤ 0z218_0 + z218_0 ≤ 0z218_0z218_0 ≤ 0z117_post + z117_post ≤ 0z117_postz117_post ≤ 0z117_2 + z117_2 ≤ 0z117_2z117_2 ≤ 0z117_1 + z117_1 ≤ 0z117_1z117_1 ≤ 0z117_0 + z117_0 ≤ 0z117_0z117_0 ≤ 0tmp712_post + tmp712_post ≤ 0tmp712_posttmp712_post ≤ 0tmp712_1 + tmp712_1 ≤ 0tmp712_1tmp712_1 ≤ 0tmp712_0 + tmp712_0 ≤ 0tmp712_0tmp712_0 ≤ 0tmp611_post + tmp611_post ≤ 0tmp611_posttmp611_post ≤ 0tmp611_1 + tmp611_1 ≤ 0tmp611_1tmp611_1 ≤ 0tmp611_0 + tmp611_0 ≤ 0tmp611_0tmp611_0 ≤ 0tmp510_post + tmp510_post ≤ 0tmp510_posttmp510_post ≤ 0tmp510_1 + tmp510_1 ≤ 0tmp510_1tmp510_1 ≤ 0tmp510_0 + tmp510_0 ≤ 0tmp510_0tmp510_0 ≤ 0tmp49_post + tmp49_post ≤ 0tmp49_posttmp49_post ≤ 0tmp49_1 + tmp49_1 ≤ 0tmp49_1tmp49_1 ≤ 0tmp49_0 + tmp49_0 ≤ 0tmp49_0tmp49_0 ≤ 0tmp38_post + tmp38_post ≤ 0tmp38_posttmp38_post ≤ 0tmp38_0 + tmp38_0 ≤ 0tmp38_0tmp38_0 ≤ 0tmp27_post + tmp27_post ≤ 0tmp27_posttmp27_post ≤ 0tmp27_0 + tmp27_0 ≤ 0tmp27_0tmp27_0 ≤ 0tmp16_post + tmp16_post ≤ 0tmp16_posttmp16_post ≤ 0tmp16_0 + tmp16_0 ≤ 0tmp16_0tmp16_0 ≤ 0tmp1316_post + tmp1316_post ≤ 0tmp1316_posttmp1316_post ≤ 0tmp1316_0 + tmp1316_0 ≤ 0tmp1316_0tmp1316_0 ≤ 0tmp1215_post + tmp1215_post ≤ 0tmp1215_posttmp1215_post ≤ 0tmp1215_0 + tmp1215_0 ≤ 0tmp1215_0tmp1215_0 ≤ 0tmp1114_post + tmp1114_post ≤ 0tmp1114_posttmp1114_post ≤ 0tmp1114_0 + tmp1114_0 ≤ 0tmp1114_0tmp1114_0 ≤ 0tmp1013_post + tmp1013_post ≤ 0tmp1013_posttmp1013_post ≤ 0tmp1013_0 + tmp1013_0 ≤ 0tmp1013_0tmp1013_0 ≤ 0tmp05_post + tmp05_post ≤ 0tmp05_posttmp05_post ≤ 0tmp05_0 + tmp05_0 ≤ 0tmp05_0tmp05_0 ≤ 0seed_post + seed_post ≤ 0seed_postseed_post ≤ 0seed_0 + seed_0 ≤ 0seed_0seed_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0ctr23_post + ctr23_post ≤ 0ctr23_postctr23_post ≤ 0ctr23_0 + ctr23_0 ≤ 0ctr23_0ctr23_0 ≤ 0___const_7_0 + ___const_7_0 ≤ 0___const_7_0___const_7_0 ≤ 0___const_64_0 + ___const_64_0 ≤ 0___const_64_0___const_64_0 ≤ 0

5 Location Addition

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

1 12 1_var_snapshot: z521_post + z521_post ≤ 0z521_postz521_post ≤ 0z521_0 + z521_0 ≤ 0z521_0z521_0 ≤ 0z420_post + z420_post ≤ 0z420_postz420_post ≤ 0z420_2 + z420_2 ≤ 0z420_2z420_2 ≤ 0z420_1 + z420_1 ≤ 0z420_1z420_1 ≤ 0z420_0 + z420_0 ≤ 0z420_0z420_0 ≤ 0z319_post + z319_post ≤ 0z319_postz319_post ≤ 0z319_2 + z319_2 ≤ 0z319_2z319_2 ≤ 0z319_1 + z319_1 ≤ 0z319_1z319_1 ≤ 0z319_0 + z319_0 ≤ 0z319_0z319_0 ≤ 0z218_post + z218_post ≤ 0z218_postz218_post ≤ 0z218_1 + z218_1 ≤ 0z218_1z218_1 ≤ 0z218_0 + z218_0 ≤ 0z218_0z218_0 ≤ 0z117_post + z117_post ≤ 0z117_postz117_post ≤ 0z117_2 + z117_2 ≤ 0z117_2z117_2 ≤ 0z117_1 + z117_1 ≤ 0z117_1z117_1 ≤ 0z117_0 + z117_0 ≤ 0z117_0z117_0 ≤ 0tmp712_post + tmp712_post ≤ 0tmp712_posttmp712_post ≤ 0tmp712_1 + tmp712_1 ≤ 0tmp712_1tmp712_1 ≤ 0tmp712_0 + tmp712_0 ≤ 0tmp712_0tmp712_0 ≤ 0tmp611_post + tmp611_post ≤ 0tmp611_posttmp611_post ≤ 0tmp611_1 + tmp611_1 ≤ 0tmp611_1tmp611_1 ≤ 0tmp611_0 + tmp611_0 ≤ 0tmp611_0tmp611_0 ≤ 0tmp510_post + tmp510_post ≤ 0tmp510_posttmp510_post ≤ 0tmp510_1 + tmp510_1 ≤ 0tmp510_1tmp510_1 ≤ 0tmp510_0 + tmp510_0 ≤ 0tmp510_0tmp510_0 ≤ 0tmp49_post + tmp49_post ≤ 0tmp49_posttmp49_post ≤ 0tmp49_1 + tmp49_1 ≤ 0tmp49_1tmp49_1 ≤ 0tmp49_0 + tmp49_0 ≤ 0tmp49_0tmp49_0 ≤ 0tmp38_post + tmp38_post ≤ 0tmp38_posttmp38_post ≤ 0tmp38_0 + tmp38_0 ≤ 0tmp38_0tmp38_0 ≤ 0tmp27_post + tmp27_post ≤ 0tmp27_posttmp27_post ≤ 0tmp27_0 + tmp27_0 ≤ 0tmp27_0tmp27_0 ≤ 0tmp16_post + tmp16_post ≤ 0tmp16_posttmp16_post ≤ 0tmp16_0 + tmp16_0 ≤ 0tmp16_0tmp16_0 ≤ 0tmp1316_post + tmp1316_post ≤ 0tmp1316_posttmp1316_post ≤ 0tmp1316_0 + tmp1316_0 ≤ 0tmp1316_0tmp1316_0 ≤ 0tmp1215_post + tmp1215_post ≤ 0tmp1215_posttmp1215_post ≤ 0tmp1215_0 + tmp1215_0 ≤ 0tmp1215_0tmp1215_0 ≤ 0tmp1114_post + tmp1114_post ≤ 0tmp1114_posttmp1114_post ≤ 0tmp1114_0 + tmp1114_0 ≤ 0tmp1114_0tmp1114_0 ≤ 0tmp1013_post + tmp1013_post ≤ 0tmp1013_posttmp1013_post ≤ 0tmp1013_0 + tmp1013_0 ≤ 0tmp1013_0tmp1013_0 ≤ 0tmp05_post + tmp05_post ≤ 0tmp05_posttmp05_post ≤ 0tmp05_0 + tmp05_0 ≤ 0tmp05_0tmp05_0 ≤ 0seed_post + seed_post ≤ 0seed_postseed_post ≤ 0seed_0 + seed_0 ≤ 0seed_0seed_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0ctr23_post + ctr23_post ≤ 0ctr23_postctr23_post ≤ 0ctr23_0 + ctr23_0 ≤ 0ctr23_0ctr23_0 ≤ 0___const_7_0 + ___const_7_0 ≤ 0___const_7_0___const_7_0 ≤ 0___const_64_0 + ___const_64_0 ≤ 0___const_64_0___const_64_0 ≤ 0

6 Location Addition

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

2* 21 2: z521_post + z521_post ≤ 0z521_postz521_post ≤ 0z521_0 + z521_0 ≤ 0z521_0z521_0 ≤ 0z420_post + z420_post ≤ 0z420_postz420_post ≤ 0z420_2 + z420_2 ≤ 0z420_2z420_2 ≤ 0z420_1 + z420_1 ≤ 0z420_1z420_1 ≤ 0z420_0 + z420_0 ≤ 0z420_0z420_0 ≤ 0z319_post + z319_post ≤ 0z319_postz319_post ≤ 0z319_2 + z319_2 ≤ 0z319_2z319_2 ≤ 0z319_1 + z319_1 ≤ 0z319_1z319_1 ≤ 0z319_0 + z319_0 ≤ 0z319_0z319_0 ≤ 0z218_post + z218_post ≤ 0z218_postz218_post ≤ 0z218_1 + z218_1 ≤ 0z218_1z218_1 ≤ 0z218_0 + z218_0 ≤ 0z218_0z218_0 ≤ 0z117_post + z117_post ≤ 0z117_postz117_post ≤ 0z117_2 + z117_2 ≤ 0z117_2z117_2 ≤ 0z117_1 + z117_1 ≤ 0z117_1z117_1 ≤ 0z117_0 + z117_0 ≤ 0z117_0z117_0 ≤ 0tmp712_post + tmp712_post ≤ 0tmp712_posttmp712_post ≤ 0tmp712_1 + tmp712_1 ≤ 0tmp712_1tmp712_1 ≤ 0tmp712_0 + tmp712_0 ≤ 0tmp712_0tmp712_0 ≤ 0tmp611_post + tmp611_post ≤ 0tmp611_posttmp611_post ≤ 0tmp611_1 + tmp611_1 ≤ 0tmp611_1tmp611_1 ≤ 0tmp611_0 + tmp611_0 ≤ 0tmp611_0tmp611_0 ≤ 0tmp510_post + tmp510_post ≤ 0tmp510_posttmp510_post ≤ 0tmp510_1 + tmp510_1 ≤ 0tmp510_1tmp510_1 ≤ 0tmp510_0 + tmp510_0 ≤ 0tmp510_0tmp510_0 ≤ 0tmp49_post + tmp49_post ≤ 0tmp49_posttmp49_post ≤ 0tmp49_1 + tmp49_1 ≤ 0tmp49_1tmp49_1 ≤ 0tmp49_0 + tmp49_0 ≤ 0tmp49_0tmp49_0 ≤ 0tmp38_post + tmp38_post ≤ 0tmp38_posttmp38_post ≤ 0tmp38_0 + tmp38_0 ≤ 0tmp38_0tmp38_0 ≤ 0tmp27_post + tmp27_post ≤ 0tmp27_posttmp27_post ≤ 0tmp27_0 + tmp27_0 ≤ 0tmp27_0tmp27_0 ≤ 0tmp16_post + tmp16_post ≤ 0tmp16_posttmp16_post ≤ 0tmp16_0 + tmp16_0 ≤ 0tmp16_0tmp16_0 ≤ 0tmp1316_post + tmp1316_post ≤ 0tmp1316_posttmp1316_post ≤ 0tmp1316_0 + tmp1316_0 ≤ 0tmp1316_0tmp1316_0 ≤ 0tmp1215_post + tmp1215_post ≤ 0tmp1215_posttmp1215_post ≤ 0tmp1215_0 + tmp1215_0 ≤ 0tmp1215_0tmp1215_0 ≤ 0tmp1114_post + tmp1114_post ≤ 0tmp1114_posttmp1114_post ≤ 0tmp1114_0 + tmp1114_0 ≤ 0tmp1114_0tmp1114_0 ≤ 0tmp1013_post + tmp1013_post ≤ 0tmp1013_posttmp1013_post ≤ 0tmp1013_0 + tmp1013_0 ≤ 0tmp1013_0tmp1013_0 ≤ 0tmp05_post + tmp05_post ≤ 0tmp05_posttmp05_post ≤ 0tmp05_0 + tmp05_0 ≤ 0tmp05_0tmp05_0 ≤ 0seed_post + seed_post ≤ 0seed_postseed_post ≤ 0seed_0 + seed_0 ≤ 0seed_0seed_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0ctr23_post + ctr23_post ≤ 0ctr23_postctr23_post ≤ 0ctr23_0 + ctr23_0 ≤ 0ctr23_0ctr23_0 ≤ 0___const_7_0 + ___const_7_0 ≤ 0___const_7_0___const_7_0 ≤ 0___const_64_0 + ___const_64_0 ≤ 0___const_64_0___const_64_0 ≤ 0

7 Location Addition

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

2 19 2_var_snapshot: z521_post + z521_post ≤ 0z521_postz521_post ≤ 0z521_0 + z521_0 ≤ 0z521_0z521_0 ≤ 0z420_post + z420_post ≤ 0z420_postz420_post ≤ 0z420_2 + z420_2 ≤ 0z420_2z420_2 ≤ 0z420_1 + z420_1 ≤ 0z420_1z420_1 ≤ 0z420_0 + z420_0 ≤ 0z420_0z420_0 ≤ 0z319_post + z319_post ≤ 0z319_postz319_post ≤ 0z319_2 + z319_2 ≤ 0z319_2z319_2 ≤ 0z319_1 + z319_1 ≤ 0z319_1z319_1 ≤ 0z319_0 + z319_0 ≤ 0z319_0z319_0 ≤ 0z218_post + z218_post ≤ 0z218_postz218_post ≤ 0z218_1 + z218_1 ≤ 0z218_1z218_1 ≤ 0z218_0 + z218_0 ≤ 0z218_0z218_0 ≤ 0z117_post + z117_post ≤ 0z117_postz117_post ≤ 0z117_2 + z117_2 ≤ 0z117_2z117_2 ≤ 0z117_1 + z117_1 ≤ 0z117_1z117_1 ≤ 0z117_0 + z117_0 ≤ 0z117_0z117_0 ≤ 0tmp712_post + tmp712_post ≤ 0tmp712_posttmp712_post ≤ 0tmp712_1 + tmp712_1 ≤ 0tmp712_1tmp712_1 ≤ 0tmp712_0 + tmp712_0 ≤ 0tmp712_0tmp712_0 ≤ 0tmp611_post + tmp611_post ≤ 0tmp611_posttmp611_post ≤ 0tmp611_1 + tmp611_1 ≤ 0tmp611_1tmp611_1 ≤ 0tmp611_0 + tmp611_0 ≤ 0tmp611_0tmp611_0 ≤ 0tmp510_post + tmp510_post ≤ 0tmp510_posttmp510_post ≤ 0tmp510_1 + tmp510_1 ≤ 0tmp510_1tmp510_1 ≤ 0tmp510_0 + tmp510_0 ≤ 0tmp510_0tmp510_0 ≤ 0tmp49_post + tmp49_post ≤ 0tmp49_posttmp49_post ≤ 0tmp49_1 + tmp49_1 ≤ 0tmp49_1tmp49_1 ≤ 0tmp49_0 + tmp49_0 ≤ 0tmp49_0tmp49_0 ≤ 0tmp38_post + tmp38_post ≤ 0tmp38_posttmp38_post ≤ 0tmp38_0 + tmp38_0 ≤ 0tmp38_0tmp38_0 ≤ 0tmp27_post + tmp27_post ≤ 0tmp27_posttmp27_post ≤ 0tmp27_0 + tmp27_0 ≤ 0tmp27_0tmp27_0 ≤ 0tmp16_post + tmp16_post ≤ 0tmp16_posttmp16_post ≤ 0tmp16_0 + tmp16_0 ≤ 0tmp16_0tmp16_0 ≤ 0tmp1316_post + tmp1316_post ≤ 0tmp1316_posttmp1316_post ≤ 0tmp1316_0 + tmp1316_0 ≤ 0tmp1316_0tmp1316_0 ≤ 0tmp1215_post + tmp1215_post ≤ 0tmp1215_posttmp1215_post ≤ 0tmp1215_0 + tmp1215_0 ≤ 0tmp1215_0tmp1215_0 ≤ 0tmp1114_post + tmp1114_post ≤ 0tmp1114_posttmp1114_post ≤ 0tmp1114_0 + tmp1114_0 ≤ 0tmp1114_0tmp1114_0 ≤ 0tmp1013_post + tmp1013_post ≤ 0tmp1013_posttmp1013_post ≤ 0tmp1013_0 + tmp1013_0 ≤ 0tmp1013_0tmp1013_0 ≤ 0tmp05_post + tmp05_post ≤ 0tmp05_posttmp05_post ≤ 0tmp05_0 + tmp05_0 ≤ 0tmp05_0tmp05_0 ≤ 0seed_post + seed_post ≤ 0seed_postseed_post ≤ 0seed_0 + seed_0 ≤ 0seed_0seed_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0ctr23_post + ctr23_post ≤ 0ctr23_postctr23_post ≤ 0ctr23_0 + ctr23_0 ≤ 0ctr23_0ctr23_0 ≤ 0___const_7_0 + ___const_7_0 ≤ 0___const_7_0___const_7_0 ≤ 0___const_64_0 + ___const_64_0 ≤ 0___const_64_0___const_64_0 ≤ 0

8 Location Addition

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

5* 28 5: z521_post + z521_post ≤ 0z521_postz521_post ≤ 0z521_0 + z521_0 ≤ 0z521_0z521_0 ≤ 0z420_post + z420_post ≤ 0z420_postz420_post ≤ 0z420_2 + z420_2 ≤ 0z420_2z420_2 ≤ 0z420_1 + z420_1 ≤ 0z420_1z420_1 ≤ 0z420_0 + z420_0 ≤ 0z420_0z420_0 ≤ 0z319_post + z319_post ≤ 0z319_postz319_post ≤ 0z319_2 + z319_2 ≤ 0z319_2z319_2 ≤ 0z319_1 + z319_1 ≤ 0z319_1z319_1 ≤ 0z319_0 + z319_0 ≤ 0z319_0z319_0 ≤ 0z218_post + z218_post ≤ 0z218_postz218_post ≤ 0z218_1 + z218_1 ≤ 0z218_1z218_1 ≤ 0z218_0 + z218_0 ≤ 0z218_0z218_0 ≤ 0z117_post + z117_post ≤ 0z117_postz117_post ≤ 0z117_2 + z117_2 ≤ 0z117_2z117_2 ≤ 0z117_1 + z117_1 ≤ 0z117_1z117_1 ≤ 0z117_0 + z117_0 ≤ 0z117_0z117_0 ≤ 0tmp712_post + tmp712_post ≤ 0tmp712_posttmp712_post ≤ 0tmp712_1 + tmp712_1 ≤ 0tmp712_1tmp712_1 ≤ 0tmp712_0 + tmp712_0 ≤ 0tmp712_0tmp712_0 ≤ 0tmp611_post + tmp611_post ≤ 0tmp611_posttmp611_post ≤ 0tmp611_1 + tmp611_1 ≤ 0tmp611_1tmp611_1 ≤ 0tmp611_0 + tmp611_0 ≤ 0tmp611_0tmp611_0 ≤ 0tmp510_post + tmp510_post ≤ 0tmp510_posttmp510_post ≤ 0tmp510_1 + tmp510_1 ≤ 0tmp510_1tmp510_1 ≤ 0tmp510_0 + tmp510_0 ≤ 0tmp510_0tmp510_0 ≤ 0tmp49_post + tmp49_post ≤ 0tmp49_posttmp49_post ≤ 0tmp49_1 + tmp49_1 ≤ 0tmp49_1tmp49_1 ≤ 0tmp49_0 + tmp49_0 ≤ 0tmp49_0tmp49_0 ≤ 0tmp38_post + tmp38_post ≤ 0tmp38_posttmp38_post ≤ 0tmp38_0 + tmp38_0 ≤ 0tmp38_0tmp38_0 ≤ 0tmp27_post + tmp27_post ≤ 0tmp27_posttmp27_post ≤ 0tmp27_0 + tmp27_0 ≤ 0tmp27_0tmp27_0 ≤ 0tmp16_post + tmp16_post ≤ 0tmp16_posttmp16_post ≤ 0tmp16_0 + tmp16_0 ≤ 0tmp16_0tmp16_0 ≤ 0tmp1316_post + tmp1316_post ≤ 0tmp1316_posttmp1316_post ≤ 0tmp1316_0 + tmp1316_0 ≤ 0tmp1316_0tmp1316_0 ≤ 0tmp1215_post + tmp1215_post ≤ 0tmp1215_posttmp1215_post ≤ 0tmp1215_0 + tmp1215_0 ≤ 0tmp1215_0tmp1215_0 ≤ 0tmp1114_post + tmp1114_post ≤ 0tmp1114_posttmp1114_post ≤ 0tmp1114_0 + tmp1114_0 ≤ 0tmp1114_0tmp1114_0 ≤ 0tmp1013_post + tmp1013_post ≤ 0tmp1013_posttmp1013_post ≤ 0tmp1013_0 + tmp1013_0 ≤ 0tmp1013_0tmp1013_0 ≤ 0tmp05_post + tmp05_post ≤ 0tmp05_posttmp05_post ≤ 0tmp05_0 + tmp05_0 ≤ 0tmp05_0tmp05_0 ≤ 0seed_post + seed_post ≤ 0seed_postseed_post ≤ 0seed_0 + seed_0 ≤ 0seed_0seed_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0ctr23_post + ctr23_post ≤ 0ctr23_postctr23_post ≤ 0ctr23_0 + ctr23_0 ≤ 0ctr23_0ctr23_0 ≤ 0___const_7_0 + ___const_7_0 ≤ 0___const_7_0___const_7_0 ≤ 0___const_64_0 + ___const_64_0 ≤ 0___const_64_0___const_64_0 ≤ 0

9 Location Addition

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

5 26 5_var_snapshot: z521_post + z521_post ≤ 0z521_postz521_post ≤ 0z521_0 + z521_0 ≤ 0z521_0z521_0 ≤ 0z420_post + z420_post ≤ 0z420_postz420_post ≤ 0z420_2 + z420_2 ≤ 0z420_2z420_2 ≤ 0z420_1 + z420_1 ≤ 0z420_1z420_1 ≤ 0z420_0 + z420_0 ≤ 0z420_0z420_0 ≤ 0z319_post + z319_post ≤ 0z319_postz319_post ≤ 0z319_2 + z319_2 ≤ 0z319_2z319_2 ≤ 0z319_1 + z319_1 ≤ 0z319_1z319_1 ≤ 0z319_0 + z319_0 ≤ 0z319_0z319_0 ≤ 0z218_post + z218_post ≤ 0z218_postz218_post ≤ 0z218_1 + z218_1 ≤ 0z218_1z218_1 ≤ 0z218_0 + z218_0 ≤ 0z218_0z218_0 ≤ 0z117_post + z117_post ≤ 0z117_postz117_post ≤ 0z117_2 + z117_2 ≤ 0z117_2z117_2 ≤ 0z117_1 + z117_1 ≤ 0z117_1z117_1 ≤ 0z117_0 + z117_0 ≤ 0z117_0z117_0 ≤ 0tmp712_post + tmp712_post ≤ 0tmp712_posttmp712_post ≤ 0tmp712_1 + tmp712_1 ≤ 0tmp712_1tmp712_1 ≤ 0tmp712_0 + tmp712_0 ≤ 0tmp712_0tmp712_0 ≤ 0tmp611_post + tmp611_post ≤ 0tmp611_posttmp611_post ≤ 0tmp611_1 + tmp611_1 ≤ 0tmp611_1tmp611_1 ≤ 0tmp611_0 + tmp611_0 ≤ 0tmp611_0tmp611_0 ≤ 0tmp510_post + tmp510_post ≤ 0tmp510_posttmp510_post ≤ 0tmp510_1 + tmp510_1 ≤ 0tmp510_1tmp510_1 ≤ 0tmp510_0 + tmp510_0 ≤ 0tmp510_0tmp510_0 ≤ 0tmp49_post + tmp49_post ≤ 0tmp49_posttmp49_post ≤ 0tmp49_1 + tmp49_1 ≤ 0tmp49_1tmp49_1 ≤ 0tmp49_0 + tmp49_0 ≤ 0tmp49_0tmp49_0 ≤ 0tmp38_post + tmp38_post ≤ 0tmp38_posttmp38_post ≤ 0tmp38_0 + tmp38_0 ≤ 0tmp38_0tmp38_0 ≤ 0tmp27_post + tmp27_post ≤ 0tmp27_posttmp27_post ≤ 0tmp27_0 + tmp27_0 ≤ 0tmp27_0tmp27_0 ≤ 0tmp16_post + tmp16_post ≤ 0tmp16_posttmp16_post ≤ 0tmp16_0 + tmp16_0 ≤ 0tmp16_0tmp16_0 ≤ 0tmp1316_post + tmp1316_post ≤ 0tmp1316_posttmp1316_post ≤ 0tmp1316_0 + tmp1316_0 ≤ 0tmp1316_0tmp1316_0 ≤ 0tmp1215_post + tmp1215_post ≤ 0tmp1215_posttmp1215_post ≤ 0tmp1215_0 + tmp1215_0 ≤ 0tmp1215_0tmp1215_0 ≤ 0tmp1114_post + tmp1114_post ≤ 0tmp1114_posttmp1114_post ≤ 0tmp1114_0 + tmp1114_0 ≤ 0tmp1114_0tmp1114_0 ≤ 0tmp1013_post + tmp1013_post ≤ 0tmp1013_posttmp1013_post ≤ 0tmp1013_0 + tmp1013_0 ≤ 0tmp1013_0tmp1013_0 ≤ 0tmp05_post + tmp05_post ≤ 0tmp05_posttmp05_post ≤ 0tmp05_0 + tmp05_0 ≤ 0tmp05_0tmp05_0 ≤ 0seed_post + seed_post ≤ 0seed_postseed_post ≤ 0seed_0 + seed_0 ≤ 0seed_0seed_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0ctr23_post + ctr23_post ≤ 0ctr23_postctr23_post ≤ 0ctr23_0 + ctr23_0 ≤ 0ctr23_0ctr23_0 ≤ 0___const_7_0 + ___const_7_0 ≤ 0___const_7_0___const_7_0 ≤ 0___const_64_0 + ___const_64_0 ≤ 0___const_64_0___const_64_0 ≤ 0

10 SCC Decomposition

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

10.1 SCC Subproblem 1/3

Here we consider the SCC { 3, 5, 5_var_snapshot, 5* }.

10.1.1 Transition Removal

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

3: −1 + 4⋅ctr23_0
5: 1 + 4⋅ctr23_0
5_var_snapshot: 4⋅ctr23_0
5*: 2 + 4⋅ctr23_0

10.1.2 Transition Removal

We remove transitions 26, 28, 6 using the following ranking functions, which are bounded by −3.

3: −3
5: −1
5_var_snapshot: −2
5*: 0

10.1.3 Splitting Cut-Point Transitions

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

10.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 25.

10.1.3.1.1 Splitting Cut-Point Transitions

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

10.2 SCC Subproblem 2/3

Here we consider the SCC { 1, 6, 1_var_snapshot, 1* }.

10.2.1 Transition Removal

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

1: 2 + 4⋅ctr23_0
6: 4⋅ctr23_0
1_var_snapshot: 1 + 4⋅ctr23_0
1*: 3 + 4⋅ctr23_0

10.2.2 Transition Removal

We remove transitions 12, 14, 5 using the following ranking functions, which are bounded by −3.

1: −1
6: −3
1_var_snapshot: −2
1*: 0

10.2.3 Splitting Cut-Point Transitions

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

10.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 11.

10.2.3.1.1 Splitting Cut-Point Transitions

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

10.3 SCC Subproblem 3/3

Here we consider the SCC { 0, 2, 2_var_snapshot, 2* }.

10.3.1 Transition Removal

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

0: −1 + 4⋅___const_64_0 − 4⋅i_0
2: 1 + 4⋅___const_64_0 − 4⋅i_0
2_var_snapshot: 4⋅___const_64_0 − 4⋅i_0
2*: 2 + 4⋅___const_64_0 − 4⋅i_0

10.3.2 Transition Removal

We remove transitions 19, 21, 4 using the following ranking functions, which are bounded by −1.

0: −1
2: 1
2_var_snapshot: 0
2*: 2

10.3.3 Splitting Cut-Point Transitions

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

10.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 18.

10.3.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert