LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 17 0: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0
3 24 3: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0
4 31 4: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0
8 38 8: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 7, 13, 15, 16 using the following ranking functions, which are bounded by −21.

12: 0
11: 0
0: 0
1: 0
4: 0
5: 0
2: 0
3: 0
6: 0
7: 0
8: 0
9: 0
10: 0
12: −6
11: −7
0: −8
1: −8
4: −8
5: −8
0_var_snapshot: −8
0*: −8
4_var_snapshot: −8
4*: −8
2: −11
3: −11
6: −11
7: −11
8: −11
9: −11
3_var_snapshot: −11
3*: −11
8_var_snapshot: −11
8*: −11
10: −14
Hints:
18 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
25 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
32 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
39 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
2 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
8 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
9 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
10 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
11 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
14 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
7 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
13 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
15 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
16 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

3 Location Addition

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

0* 20 0: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

4 Location Addition

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

0 18 0_var_snapshot: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

5 Location Addition

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

3* 27 3: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

6 Location Addition

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

3 25 3_var_snapshot: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

7 Location Addition

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

4* 34 4: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

8 Location Addition

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

4 32 4_var_snapshot: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

9 Location Addition

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

8* 41 8: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

10 Location Addition

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

8 39 8_var_snapshot: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_0 ≤ 0___const_1500_0 + ___const_1500_0 ≤ 0___const_1500_0___const_1500_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0___const_1000_0 + ___const_1000_0 ≤ 0___const_1000_0___const_1000_0 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

11 SCC Decomposition

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

11.1 SCC Subproblem 1/2

Here we consider the SCC { 2, 3, 6, 7, 8, 9, 3_var_snapshot, 3*, 8_var_snapshot, 8* }.

11.1.1 Transition Removal

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

2: −3⋅Outer9_0 + 3⋅___const_10_0
3: −3⋅Outer9_0 + 3⋅___const_10_0
6: −3⋅Outer9_0 + 3⋅___const_10_0
7: −3⋅Outer9_0 + 3⋅___const_10_0
8: 2 − 3⋅Outer9_0 + 3⋅___const_10_0
9: 1 − 3⋅Outer9_0 + 3⋅___const_10_0
3_var_snapshot: −3⋅Outer9_0 + 3⋅___const_10_0
3*: −3⋅Outer9_0 + 3⋅___const_10_0
8_var_snapshot: 2 − 3⋅Outer9_0 + 3⋅___const_10_0
8*: 2 − 3⋅Outer9_0 + 3⋅___const_10_0
Hints:
25 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
27 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
39 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
41 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
5 lexWeak[ [0, 0, 0, 0, 3, 0, 3, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
8 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
9 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
10 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

11.1.2 Transition Removal

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

2: −2 − 5⋅Inner10_0 + 5⋅___const_10_0
3: 1 − 5⋅Inner10_0 + 5⋅___const_10_0
6: −2 − 5⋅Inner10_0 + 5⋅___const_10_0
7: −1 − 5⋅Inner10_0 + 5⋅___const_10_0
8: −3 − 5⋅Inner10_0 + 5⋅___const_10_0
9: −4 − 5⋅Inner10_0 + 5⋅___const_10_0
3_var_snapshot: −5⋅Inner10_0 + 5⋅___const_10_0
3*: 2 − 5⋅Inner10_0 + 5⋅___const_10_0
8_var_snapshot: −4 − 5⋅Inner10_0 + 5⋅___const_10_0
8*: −2 − 5⋅Inner10_0 + 5⋅___const_10_0
Hints:
25 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ]
27 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ]
39 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ]
41 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ]
1 lexWeak[ [0, 0, 0, 5, 0, 5, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ]
4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ]
5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ]
6 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] , [5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
9 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ]
10 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ]

11.1.3 Transition Removal

We remove transitions 25, 27, 39, 41, 3, 4, 5, 9, 10 using the following ranking functions, which are bounded by −5.

2: 3
3: 1
6: 4
7: −1
8: −3
9: −5
3_var_snapshot: 0
3*: 2
8_var_snapshot: −4
8*: −2
Hints:
25 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
27 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
39 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
41 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
3 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
4 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
5 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
9 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
10 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

11.1.4 Transition Removal

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

2: 1
3: 0
6: 0
7: 0
8: 0
9: 0
3_var_snapshot: 0
3*: 0
8_var_snapshot: 0
8*: 0
Hints:
1 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

11.1.5 Splitting Cut-Point Transitions

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

11.1.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 24.

11.1.5.1.1 Splitting Cut-Point Transitions

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

11.1.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 38.

11.1.5.2.1 Splitting Cut-Point Transitions

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

11.2 SCC Subproblem 2/2

Here we consider the SCC { 0, 1, 4, 5, 0_var_snapshot, 0*, 4_var_snapshot, 4* }.

11.2.1 Transition Removal

We remove transition 14 using the following ranking functions, which are bounded by 7.

0: 1 − 8⋅OuterIndex6_0 + 8⋅___const_10_0
1: −8⋅OuterIndex6_0 + 8⋅___const_10_0
4: −5 − 8⋅OuterIndex6_0 + 8⋅___const_10_0
5: −5 − 8⋅OuterIndex6_0 + 8⋅___const_10_0
0_var_snapshot: −8⋅OuterIndex6_0 + 8⋅___const_10_0
0*: 2 − 8⋅OuterIndex6_0 + 8⋅___const_10_0
4_var_snapshot: −5 − 8⋅OuterIndex6_0 + 8⋅___const_10_0
4*: −5 − 8⋅OuterIndex6_0 + 8⋅___const_10_0
Hints:
18 lexWeak[ [0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
20 lexWeak[ [0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
32 lexWeak[ [0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
34 lexWeak[ [0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
0 lexWeak[ [0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
2 lexWeak[ [0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
11 lexWeak[ [0, 0, 0, 0, 8, 0, 8, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
14 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

11.2.2 Transition Removal

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

0: −2 − 4⋅InnerIndex7_0 + 4⋅___const_10_0
1: −4 − 4⋅InnerIndex7_0 + 4⋅___const_10_0
4: 2 − 4⋅InnerIndex7_0 + 4⋅___const_10_0
5: −4⋅InnerIndex7_0 + 4⋅___const_10_0
0_var_snapshot: −3 − 4⋅InnerIndex7_0 + 4⋅___const_10_0
0*: −1 − 4⋅InnerIndex7_0 + 4⋅___const_10_0
4_var_snapshot: 1 − 4⋅InnerIndex7_0 + 4⋅___const_10_0
4*: 3 − 4⋅InnerIndex7_0 + 4⋅___const_10_0
Hints:
18 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ]
20 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ]
32 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ]
34 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ]
0 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ]
2 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ]
11 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ]
12 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 4, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

11.2.3 Transition Removal

We remove transitions 18, 20, 32, 34, 0, 2, 11 using the following ranking functions, which are bounded by −4.

0: −2
1: −4
4: 2
5: 0
0_var_snapshot: −3
0*: −1
4_var_snapshot: 1
4*: 3
Hints:
18 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
20 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
32 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
34 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
0 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
2 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
11 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

11.2.4 Splitting Cut-Point Transitions

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

11.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 17.

11.2.4.1.1 Splitting Cut-Point Transitions

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

11.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 31.

11.2.4.2.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert