LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: TRUE
1: TRUE
2: 10 − OuterIndex6_0 ≤ 0−1000 + StartTime2_post ≤ 01000 − StartTime2_post ≤ 0−1000 + StartTime2_0 ≤ 01000 − StartTime2_0 ≤ 0
3: 10 − OuterIndex6_0 ≤ 0−1000 + StartTime2_post ≤ 01000 − StartTime2_post ≤ 0−1000 + StartTime2_0 ≤ 01000 − StartTime2_0 ≤ 0
4: TRUE
5: TRUE
6: 10 − OuterIndex6_0 ≤ 0−1000 + StartTime2_post ≤ 01000 − StartTime2_post ≤ 0−1000 + StartTime2_0 ≤ 01000 − StartTime2_0 ≤ 0
7: 10 − OuterIndex6_0 ≤ 0−1000 + StartTime2_post ≤ 01000 − StartTime2_post ≤ 0−1000 + StartTime2_0 ≤ 01000 − StartTime2_0 ≤ 0
8: 10 − OuterIndex6_0 ≤ 0−1000 + StartTime2_post ≤ 01000 − StartTime2_post ≤ 0−1000 + StartTime2_0 ≤ 01000 − StartTime2_0 ≤ 0
9: 10 − OuterIndex6_0 ≤ 0−1000 + StartTime2_post ≤ 01000 − StartTime2_post ≤ 0−1000 + StartTime2_0 ≤ 01000 − StartTime2_0 ≤ 0
10: 10 − OuterIndex6_0 ≤ 0−1000 + StartTime2_post ≤ 01000 − StartTime2_post ≤ 010 − Outer9_0 ≤ 0−1000 + StartTime2_0 ≤ 01000 − StartTime2_0 ≤ 0−1500 + StopTime3_post ≤ 01500 − StopTime3_post ≤ 0−1500 + StopTime3_0 ≤ 01500 − StopTime3_0 ≤ 0
11: TRUE
12: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 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 ≤ 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 ≤ 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 ≤ 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 ≤ 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.

3 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

4 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 ≤ 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.

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 ≤ 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* 27 3: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_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.

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 ≤ 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* 34 4: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_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.

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 ≤ 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* 41 8: ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_RandomInteger15_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 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 ≤ 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

12 SCC Decomposition

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

12.1 SCC Subproblem 1/2

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

12.1.1 Transition Removal

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

2: −3001⋅Outer9_0
3: −3001⋅Outer9_0
6: −3001⋅Outer9_0
7: −3001⋅Outer9_0
8: −3001⋅Outer9_0 + 3⋅StartTime2_post
9: 1000 − 3001⋅Outer9_0
3_var_snapshot: −3001⋅Outer9_0
3*: −3001⋅Outer9_0
8_var_snapshot: −3001⋅Outer9_0 + 2⋅StartTime2_0
8*: −3001⋅Outer9_0 + 3⋅StartTime2_post

12.1.2 Transition Removal

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

2: −4002⋅Inner10_0StartTime2_0
3: −4002⋅Inner10_0 + 3⋅StartTime2_0
6: −4002⋅Inner10_0StartTime2_0 + StartTime2_post
7: −4002⋅Inner10_0 + StartTime2_post
8: −3000 − 4002⋅Inner10_0 + StartTime2_0 + StartTime2_post
9: 999 − 4002⋅Inner10_0 − 3⋅StartTime2_post
3_var_snapshot: 1000 − 4002⋅Inner10_0 + StartTime2_post
3*: 2001 − 4002⋅Inner10_0 + StartTime2_0
8_var_snapshot: −4002⋅Inner10_0 + StartTime2_0 − 3⋅StartTime2_post
8*: −1000 − 4002⋅Inner10_0 + StartTime2_post

12.1.3 Transition Removal

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

2: 3002
3: 3⋅StartTime2_0
6: 3003
7: StartTime2_0 + 2⋅StartTime2_post
8: −1000
9: −1 − 2⋅StartTime2_0
3_var_snapshot: 2⋅StartTime2_post
3*: 1 + 3⋅StartTime2_0
8_var_snapshot: −2⋅StartTime2_0
8*: 0

12.1.4 Splitting Cut-Point Transitions

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

12.1.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 24.

12.1.4.1.1 Splitting Cut-Point Transitions

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

12.1.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 38.

12.1.4.2.1 Splitting Cut-Point Transitions

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

12.2 SCC Subproblem 2/2

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

12.2.1 Transition Removal

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

0: 1 − 4⋅OuterIndex6_0
1: −4⋅OuterIndex6_0
4: −1 − 4⋅OuterIndex6_0
5: −1 − 4⋅OuterIndex6_0
0_var_snapshot: −4⋅OuterIndex6_0
0*: 2 − 4⋅OuterIndex6_0
4_var_snapshot: −1 − 4⋅OuterIndex6_0
4*: −1 − 4⋅OuterIndex6_0

12.2.2 Transition Removal

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

0: −11 − 4⋅InnerIndex7_0
1: −13 − 4⋅InnerIndex7_0
4: 2 − 4⋅InnerIndex7_0
5: −4⋅InnerIndex7_0
0_var_snapshot: −12 − 4⋅InnerIndex7_0
0*: −1 − 4⋅InnerIndex7_0
4_var_snapshot: 1 − 4⋅InnerIndex7_0
4*: 3 − 4⋅InnerIndex7_0

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

12.2.4 Splitting Cut-Point Transitions

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

12.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 17.

12.2.4.1.1 Splitting Cut-Point Transitions

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

12.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 31.

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