LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: c1_post ≤ 0max_post ≤ 0n_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0
1: −1 + c1_post ≤ 01 − c1_post ≤ 0max_post ≤ 0n_post ≤ 0−1 + pos_post ≤ 01 − pos_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0−1 + c1_0 ≤ 01 − c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0−1 + pos_0 ≤ 01 − pos_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0c2_post ≤ 0c2_post ≤ 0−1 + c1_1 ≤ 01 − c1_1 ≤ 0−1 + c1_2 ≤ 01 − c1_2 ≤ 0−1 + c1_3 ≤ 01 − c1_3 ≤ 0c1_4 ≤ 0c1_4 ≤ 0c2_1 ≤ 0c2_1 ≤ 0−1 + c2_2 ≤ 01 − c2_2 ≤ 0−1 + c2_3 ≤ 01 − c2_3 ≤ 01 − m_1 ≤ 01 − m_2 ≤ 01 − m_3 ≤ 0pi_1 ≤ 01 − pi_2 ≤ 0−1 + wpos_1 ≤ 01 − wpos_1 ≤ 0wpos_2 ≤ 0wpos_2 ≤ 0−1 + wpos_3 ≤ 01 − wpos_3 ≤ 0wpos_4 ≤ 0wpos_4 ≤ 0−1 + wpos_5 ≤ 01 − wpos_5 ≤ 01 − z_1 ≤ 01 − z_2 ≤ 0c2_0 ≤ 0c2_0 ≤ 0
2: TRUE
3: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 4 0: z_post + z_post ≤ 0z_postz_post ≤ 0z_2 + z_2 ≤ 0z_2z_2 ≤ 0z_1 + z_1 ≤ 0z_1z_1 ≤ 0z_0 + z_0 ≤ 0z_0z_0 ≤ 0wpos_post + wpos_post ≤ 0wpos_postwpos_post ≤ 0wpos_5 + wpos_5 ≤ 0wpos_5wpos_5 ≤ 0wpos_4 + wpos_4 ≤ 0wpos_4wpos_4 ≤ 0wpos_3 + wpos_3 ≤ 0wpos_3wpos_3 ≤ 0wpos_2 + wpos_2 ≤ 0wpos_2wpos_2 ≤ 0wpos_1 + wpos_1 ≤ 0wpos_1wpos_1 ≤ 0wpos_0 + wpos_0 ≤ 0wpos_0wpos_0 ≤ 0seq_post + seq_post ≤ 0seq_postseq_post ≤ 0seq_0 + seq_0 ≤ 0seq_0seq_0 ≤ 0pos_post + pos_post ≤ 0pos_postpos_post ≤ 0pos_1 + pos_1 ≤ 0pos_1pos_1 ≤ 0pos_0 + pos_0 ≤ 0pos_0pos_0 ≤ 0pi_post + pi_post ≤ 0pi_postpi_post ≤ 0pi_2 + pi_2 ≤ 0pi_2pi_2 ≤ 0pi_1 + pi_1 ≤ 0pi_1pi_1 ≤ 0pi_0 + pi_0 ≤ 0pi_0pi_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0max_post + max_post ≤ 0max_postmax_post ≤ 0max_0 + max_0 ≤ 0max_0max_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_3 + m_3 ≤ 0m_3m_3 ≤ 0m_2 + m_2 ≤ 0m_2m_2 ≤ 0m_1 + m_1 ≤ 0m_1m_1 ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0c2_post + c2_post ≤ 0c2_postc2_post ≤ 0c2_3 + c2_3 ≤ 0c2_3c2_3 ≤ 0c2_2 + c2_2 ≤ 0c2_2c2_2 ≤ 0c2_1 + c2_1 ≤ 0c2_1c2_1 ≤ 0c2_0 + c2_0 ≤ 0c2_0c2_0 ≤ 0c1_post + c1_post ≤ 0c1_postc1_post ≤ 0c1_4 + c1_4 ≤ 0c1_4c1_4 ≤ 0c1_3 + c1_3 ≤ 0c1_3c1_3 ≤ 0c1_2 + c1_2 ≤ 0c1_2c1_2 ≤ 0c1_1 + c1_1 ≤ 0c1_1c1_1 ≤ 0c1_0 + c1_0 ≤ 0c1_0c1_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

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

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

4 Location Addition

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

0* 7 0: z_post + z_post ≤ 0z_postz_post ≤ 0z_2 + z_2 ≤ 0z_2z_2 ≤ 0z_1 + z_1 ≤ 0z_1z_1 ≤ 0z_0 + z_0 ≤ 0z_0z_0 ≤ 0wpos_post + wpos_post ≤ 0wpos_postwpos_post ≤ 0wpos_5 + wpos_5 ≤ 0wpos_5wpos_5 ≤ 0wpos_4 + wpos_4 ≤ 0wpos_4wpos_4 ≤ 0wpos_3 + wpos_3 ≤ 0wpos_3wpos_3 ≤ 0wpos_2 + wpos_2 ≤ 0wpos_2wpos_2 ≤ 0wpos_1 + wpos_1 ≤ 0wpos_1wpos_1 ≤ 0wpos_0 + wpos_0 ≤ 0wpos_0wpos_0 ≤ 0seq_post + seq_post ≤ 0seq_postseq_post ≤ 0seq_0 + seq_0 ≤ 0seq_0seq_0 ≤ 0pos_post + pos_post ≤ 0pos_postpos_post ≤ 0pos_1 + pos_1 ≤ 0pos_1pos_1 ≤ 0pos_0 + pos_0 ≤ 0pos_0pos_0 ≤ 0pi_post + pi_post ≤ 0pi_postpi_post ≤ 0pi_2 + pi_2 ≤ 0pi_2pi_2 ≤ 0pi_1 + pi_1 ≤ 0pi_1pi_1 ≤ 0pi_0 + pi_0 ≤ 0pi_0pi_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0max_post + max_post ≤ 0max_postmax_post ≤ 0max_0 + max_0 ≤ 0max_0max_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_3 + m_3 ≤ 0m_3m_3 ≤ 0m_2 + m_2 ≤ 0m_2m_2 ≤ 0m_1 + m_1 ≤ 0m_1m_1 ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0c2_post + c2_post ≤ 0c2_postc2_post ≤ 0c2_3 + c2_3 ≤ 0c2_3c2_3 ≤ 0c2_2 + c2_2 ≤ 0c2_2c2_2 ≤ 0c2_1 + c2_1 ≤ 0c2_1c2_1 ≤ 0c2_0 + c2_0 ≤ 0c2_0c2_0 ≤ 0c1_post + c1_post ≤ 0c1_postc1_post ≤ 0c1_4 + c1_4 ≤ 0c1_4c1_4 ≤ 0c1_3 + c1_3 ≤ 0c1_3c1_3 ≤ 0c1_2 + c1_2 ≤ 0c1_2c1_2 ≤ 0c1_1 + c1_1 ≤ 0c1_1c1_1 ≤ 0c1_0 + c1_0 ≤ 0c1_0c1_0 ≤ 0

5 Location Addition

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

0 5 0_var_snapshot: z_post + z_post ≤ 0z_postz_post ≤ 0z_2 + z_2 ≤ 0z_2z_2 ≤ 0z_1 + z_1 ≤ 0z_1z_1 ≤ 0z_0 + z_0 ≤ 0z_0z_0 ≤ 0wpos_post + wpos_post ≤ 0wpos_postwpos_post ≤ 0wpos_5 + wpos_5 ≤ 0wpos_5wpos_5 ≤ 0wpos_4 + wpos_4 ≤ 0wpos_4wpos_4 ≤ 0wpos_3 + wpos_3 ≤ 0wpos_3wpos_3 ≤ 0wpos_2 + wpos_2 ≤ 0wpos_2wpos_2 ≤ 0wpos_1 + wpos_1 ≤ 0wpos_1wpos_1 ≤ 0wpos_0 + wpos_0 ≤ 0wpos_0wpos_0 ≤ 0seq_post + seq_post ≤ 0seq_postseq_post ≤ 0seq_0 + seq_0 ≤ 0seq_0seq_0 ≤ 0pos_post + pos_post ≤ 0pos_postpos_post ≤ 0pos_1 + pos_1 ≤ 0pos_1pos_1 ≤ 0pos_0 + pos_0 ≤ 0pos_0pos_0 ≤ 0pi_post + pi_post ≤ 0pi_postpi_post ≤ 0pi_2 + pi_2 ≤ 0pi_2pi_2 ≤ 0pi_1 + pi_1 ≤ 0pi_1pi_1 ≤ 0pi_0 + pi_0 ≤ 0pi_0pi_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0max_post + max_post ≤ 0max_postmax_post ≤ 0max_0 + max_0 ≤ 0max_0max_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_3 + m_3 ≤ 0m_3m_3 ≤ 0m_2 + m_2 ≤ 0m_2m_2 ≤ 0m_1 + m_1 ≤ 0m_1m_1 ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0c2_post + c2_post ≤ 0c2_postc2_post ≤ 0c2_3 + c2_3 ≤ 0c2_3c2_3 ≤ 0c2_2 + c2_2 ≤ 0c2_2c2_2 ≤ 0c2_1 + c2_1 ≤ 0c2_1c2_1 ≤ 0c2_0 + c2_0 ≤ 0c2_0c2_0 ≤ 0c1_post + c1_post ≤ 0c1_postc1_post ≤ 0c1_4 + c1_4 ≤ 0c1_4c1_4 ≤ 0c1_3 + c1_3 ≤ 0c1_3c1_3 ≤ 0c1_2 + c1_2 ≤ 0c1_2c1_2 ≤ 0c1_1 + c1_1 ≤ 0c1_1c1_1 ≤ 0c1_0 + c1_0 ≤ 0c1_0c1_0 ≤ 0

6 SCC Decomposition

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

6.1 SCC Subproblem 1/1

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

6.1.1 Splitting Cut-Point Transitions

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

6.1.1.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 4.

6.1.1.1.1 Fresh Variable Addition

The new variable __snapshot_0_z_post is introduced. The transition formulas are extended as follows:

5: __snapshot_0_z_postz_postz_post__snapshot_0_z_post
7: __snapshot_0_z_post__snapshot_0_z_post__snapshot_0_z_post__snapshot_0_z_post
0: __snapshot_0_z_post__snapshot_0_z_post__snapshot_0_z_post__snapshot_0_z_post
1: __snapshot_0_z_post__snapshot_0_z_post__snapshot_0_z_post__snapshot_0_z_post

6.1.1.1.2 Fresh Variable Addition

The new variable __snapshot_0_z_2 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_z_2z_2z_2__snapshot_0_z_2
7: __snapshot_0_z_2__snapshot_0_z_2__snapshot_0_z_2__snapshot_0_z_2
0: __snapshot_0_z_2__snapshot_0_z_2__snapshot_0_z_2__snapshot_0_z_2
1: __snapshot_0_z_2__snapshot_0_z_2__snapshot_0_z_2__snapshot_0_z_2

6.1.1.1.3 Fresh Variable Addition

The new variable __snapshot_0_z_1 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_z_1z_1z_1__snapshot_0_z_1
7: __snapshot_0_z_1__snapshot_0_z_1__snapshot_0_z_1__snapshot_0_z_1
0: __snapshot_0_z_1__snapshot_0_z_1__snapshot_0_z_1__snapshot_0_z_1
1: __snapshot_0_z_1__snapshot_0_z_1__snapshot_0_z_1__snapshot_0_z_1

6.1.1.1.4 Fresh Variable Addition

The new variable __snapshot_0_z_0 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_z_0z_0z_0__snapshot_0_z_0
7: __snapshot_0_z_0__snapshot_0_z_0__snapshot_0_z_0__snapshot_0_z_0
0: __snapshot_0_z_0__snapshot_0_z_0__snapshot_0_z_0__snapshot_0_z_0
1: __snapshot_0_z_0__snapshot_0_z_0__snapshot_0_z_0__snapshot_0_z_0

6.1.1.1.5 Fresh Variable Addition

The new variable __snapshot_0_wpos_post is introduced. The transition formulas are extended as follows:

5: __snapshot_0_wpos_postwpos_postwpos_post__snapshot_0_wpos_post
7: __snapshot_0_wpos_post__snapshot_0_wpos_post__snapshot_0_wpos_post__snapshot_0_wpos_post
0: __snapshot_0_wpos_post__snapshot_0_wpos_post__snapshot_0_wpos_post__snapshot_0_wpos_post
1: __snapshot_0_wpos_post__snapshot_0_wpos_post__snapshot_0_wpos_post__snapshot_0_wpos_post

6.1.1.1.6 Fresh Variable Addition

The new variable __snapshot_0_wpos_5 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_wpos_5wpos_5wpos_5__snapshot_0_wpos_5
7: __snapshot_0_wpos_5__snapshot_0_wpos_5__snapshot_0_wpos_5__snapshot_0_wpos_5
0: __snapshot_0_wpos_5__snapshot_0_wpos_5__snapshot_0_wpos_5__snapshot_0_wpos_5
1: __snapshot_0_wpos_5__snapshot_0_wpos_5__snapshot_0_wpos_5__snapshot_0_wpos_5

6.1.1.1.7 Fresh Variable Addition

The new variable __snapshot_0_wpos_4 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_wpos_4wpos_4wpos_4__snapshot_0_wpos_4
7: __snapshot_0_wpos_4__snapshot_0_wpos_4__snapshot_0_wpos_4__snapshot_0_wpos_4
0: __snapshot_0_wpos_4__snapshot_0_wpos_4__snapshot_0_wpos_4__snapshot_0_wpos_4
1: __snapshot_0_wpos_4__snapshot_0_wpos_4__snapshot_0_wpos_4__snapshot_0_wpos_4

6.1.1.1.8 Fresh Variable Addition

The new variable __snapshot_0_wpos_3 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_wpos_3wpos_3wpos_3__snapshot_0_wpos_3
7: __snapshot_0_wpos_3__snapshot_0_wpos_3__snapshot_0_wpos_3__snapshot_0_wpos_3
0: __snapshot_0_wpos_3__snapshot_0_wpos_3__snapshot_0_wpos_3__snapshot_0_wpos_3
1: __snapshot_0_wpos_3__snapshot_0_wpos_3__snapshot_0_wpos_3__snapshot_0_wpos_3

6.1.1.1.9 Fresh Variable Addition

The new variable __snapshot_0_wpos_2 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_wpos_2wpos_2wpos_2__snapshot_0_wpos_2
7: __snapshot_0_wpos_2__snapshot_0_wpos_2__snapshot_0_wpos_2__snapshot_0_wpos_2
0: __snapshot_0_wpos_2__snapshot_0_wpos_2__snapshot_0_wpos_2__snapshot_0_wpos_2
1: __snapshot_0_wpos_2__snapshot_0_wpos_2__snapshot_0_wpos_2__snapshot_0_wpos_2

6.1.1.1.10 Fresh Variable Addition

The new variable __snapshot_0_wpos_1 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_wpos_1wpos_1wpos_1__snapshot_0_wpos_1
7: __snapshot_0_wpos_1__snapshot_0_wpos_1__snapshot_0_wpos_1__snapshot_0_wpos_1
0: __snapshot_0_wpos_1__snapshot_0_wpos_1__snapshot_0_wpos_1__snapshot_0_wpos_1
1: __snapshot_0_wpos_1__snapshot_0_wpos_1__snapshot_0_wpos_1__snapshot_0_wpos_1

6.1.1.1.11 Fresh Variable Addition

The new variable __snapshot_0_wpos_0 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_wpos_0wpos_0wpos_0__snapshot_0_wpos_0
7: __snapshot_0_wpos_0__snapshot_0_wpos_0__snapshot_0_wpos_0__snapshot_0_wpos_0
0: __snapshot_0_wpos_0__snapshot_0_wpos_0__snapshot_0_wpos_0__snapshot_0_wpos_0
1: __snapshot_0_wpos_0__snapshot_0_wpos_0__snapshot_0_wpos_0__snapshot_0_wpos_0

6.1.1.1.12 Fresh Variable Addition

The new variable __snapshot_0_seq_post is introduced. The transition formulas are extended as follows:

5: __snapshot_0_seq_postseq_postseq_post__snapshot_0_seq_post
7: __snapshot_0_seq_post__snapshot_0_seq_post__snapshot_0_seq_post__snapshot_0_seq_post
0: __snapshot_0_seq_post__snapshot_0_seq_post__snapshot_0_seq_post__snapshot_0_seq_post
1: __snapshot_0_seq_post__snapshot_0_seq_post__snapshot_0_seq_post__snapshot_0_seq_post

6.1.1.1.13 Fresh Variable Addition

The new variable __snapshot_0_seq_0 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_seq_0seq_0seq_0__snapshot_0_seq_0
7: __snapshot_0_seq_0__snapshot_0_seq_0__snapshot_0_seq_0__snapshot_0_seq_0
0: __snapshot_0_seq_0__snapshot_0_seq_0__snapshot_0_seq_0__snapshot_0_seq_0
1: __snapshot_0_seq_0__snapshot_0_seq_0__snapshot_0_seq_0__snapshot_0_seq_0

6.1.1.1.14 Fresh Variable Addition

The new variable __snapshot_0_pos_post is introduced. The transition formulas are extended as follows:

5: __snapshot_0_pos_postpos_postpos_post__snapshot_0_pos_post
7: __snapshot_0_pos_post__snapshot_0_pos_post__snapshot_0_pos_post__snapshot_0_pos_post
0: __snapshot_0_pos_post__snapshot_0_pos_post__snapshot_0_pos_post__snapshot_0_pos_post
1: __snapshot_0_pos_post__snapshot_0_pos_post__snapshot_0_pos_post__snapshot_0_pos_post

6.1.1.1.15 Fresh Variable Addition

The new variable __snapshot_0_pos_1 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_pos_1pos_1pos_1__snapshot_0_pos_1
7: __snapshot_0_pos_1__snapshot_0_pos_1__snapshot_0_pos_1__snapshot_0_pos_1
0: __snapshot_0_pos_1__snapshot_0_pos_1__snapshot_0_pos_1__snapshot_0_pos_1
1: __snapshot_0_pos_1__snapshot_0_pos_1__snapshot_0_pos_1__snapshot_0_pos_1

6.1.1.1.16 Fresh Variable Addition

The new variable __snapshot_0_pos_0 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_pos_0pos_0pos_0__snapshot_0_pos_0
7: __snapshot_0_pos_0__snapshot_0_pos_0__snapshot_0_pos_0__snapshot_0_pos_0
0: __snapshot_0_pos_0__snapshot_0_pos_0__snapshot_0_pos_0__snapshot_0_pos_0
1: __snapshot_0_pos_0__snapshot_0_pos_0__snapshot_0_pos_0__snapshot_0_pos_0

6.1.1.1.17 Fresh Variable Addition

The new variable __snapshot_0_pi_post is introduced. The transition formulas are extended as follows:

5: __snapshot_0_pi_postpi_postpi_post__snapshot_0_pi_post
7: __snapshot_0_pi_post__snapshot_0_pi_post__snapshot_0_pi_post__snapshot_0_pi_post
0: __snapshot_0_pi_post__snapshot_0_pi_post__snapshot_0_pi_post__snapshot_0_pi_post
1: __snapshot_0_pi_post__snapshot_0_pi_post__snapshot_0_pi_post__snapshot_0_pi_post

6.1.1.1.18 Fresh Variable Addition

The new variable __snapshot_0_pi_2 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_pi_2pi_2pi_2__snapshot_0_pi_2
7: __snapshot_0_pi_2__snapshot_0_pi_2__snapshot_0_pi_2__snapshot_0_pi_2
0: __snapshot_0_pi_2__snapshot_0_pi_2__snapshot_0_pi_2__snapshot_0_pi_2
1: __snapshot_0_pi_2__snapshot_0_pi_2__snapshot_0_pi_2__snapshot_0_pi_2

6.1.1.1.19 Fresh Variable Addition

The new variable __snapshot_0_pi_1 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_pi_1pi_1pi_1__snapshot_0_pi_1
7: __snapshot_0_pi_1__snapshot_0_pi_1__snapshot_0_pi_1__snapshot_0_pi_1
0: __snapshot_0_pi_1__snapshot_0_pi_1__snapshot_0_pi_1__snapshot_0_pi_1
1: __snapshot_0_pi_1__snapshot_0_pi_1__snapshot_0_pi_1__snapshot_0_pi_1

6.1.1.1.20 Fresh Variable Addition

The new variable __snapshot_0_pi_0 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_pi_0pi_0pi_0__snapshot_0_pi_0
7: __snapshot_0_pi_0__snapshot_0_pi_0__snapshot_0_pi_0__snapshot_0_pi_0
0: __snapshot_0_pi_0__snapshot_0_pi_0__snapshot_0_pi_0__snapshot_0_pi_0
1: __snapshot_0_pi_0__snapshot_0_pi_0__snapshot_0_pi_0__snapshot_0_pi_0

6.1.1.1.21 Fresh Variable Addition

The new variable __snapshot_0_n_post is introduced. The transition formulas are extended as follows:

5: __snapshot_0_n_postn_postn_post__snapshot_0_n_post
7: __snapshot_0_n_post__snapshot_0_n_post__snapshot_0_n_post__snapshot_0_n_post
0: __snapshot_0_n_post__snapshot_0_n_post__snapshot_0_n_post__snapshot_0_n_post
1: __snapshot_0_n_post__snapshot_0_n_post__snapshot_0_n_post__snapshot_0_n_post

6.1.1.1.22 Fresh Variable Addition

The new variable __snapshot_0_n_0 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_n_0n_0n_0__snapshot_0_n_0
7: __snapshot_0_n_0__snapshot_0_n_0__snapshot_0_n_0__snapshot_0_n_0
0: __snapshot_0_n_0__snapshot_0_n_0__snapshot_0_n_0__snapshot_0_n_0
1: __snapshot_0_n_0__snapshot_0_n_0__snapshot_0_n_0__snapshot_0_n_0

6.1.1.1.23 Fresh Variable Addition

The new variable __snapshot_0_max_post is introduced. The transition formulas are extended as follows:

5: __snapshot_0_max_postmax_postmax_post__snapshot_0_max_post
7: __snapshot_0_max_post__snapshot_0_max_post__snapshot_0_max_post__snapshot_0_max_post
0: __snapshot_0_max_post__snapshot_0_max_post__snapshot_0_max_post__snapshot_0_max_post
1: __snapshot_0_max_post__snapshot_0_max_post__snapshot_0_max_post__snapshot_0_max_post

6.1.1.1.24 Fresh Variable Addition

The new variable __snapshot_0_max_0 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_max_0max_0max_0__snapshot_0_max_0
7: __snapshot_0_max_0__snapshot_0_max_0__snapshot_0_max_0__snapshot_0_max_0
0: __snapshot_0_max_0__snapshot_0_max_0__snapshot_0_max_0__snapshot_0_max_0
1: __snapshot_0_max_0__snapshot_0_max_0__snapshot_0_max_0__snapshot_0_max_0

6.1.1.1.25 Fresh Variable Addition

The new variable __snapshot_0_m_post is introduced. The transition formulas are extended as follows:

5: __snapshot_0_m_postm_postm_post__snapshot_0_m_post
7: __snapshot_0_m_post__snapshot_0_m_post__snapshot_0_m_post__snapshot_0_m_post
0: __snapshot_0_m_post__snapshot_0_m_post__snapshot_0_m_post__snapshot_0_m_post
1: __snapshot_0_m_post__snapshot_0_m_post__snapshot_0_m_post__snapshot_0_m_post

6.1.1.1.26 Fresh Variable Addition

The new variable __snapshot_0_m_3 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_m_3m_3m_3__snapshot_0_m_3
7: __snapshot_0_m_3__snapshot_0_m_3__snapshot_0_m_3__snapshot_0_m_3
0: __snapshot_0_m_3__snapshot_0_m_3__snapshot_0_m_3__snapshot_0_m_3
1: __snapshot_0_m_3__snapshot_0_m_3__snapshot_0_m_3__snapshot_0_m_3

6.1.1.1.27 Fresh Variable Addition

The new variable __snapshot_0_m_2 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_m_2m_2m_2__snapshot_0_m_2
7: __snapshot_0_m_2__snapshot_0_m_2__snapshot_0_m_2__snapshot_0_m_2
0: __snapshot_0_m_2__snapshot_0_m_2__snapshot_0_m_2__snapshot_0_m_2
1: __snapshot_0_m_2__snapshot_0_m_2__snapshot_0_m_2__snapshot_0_m_2

6.1.1.1.28 Fresh Variable Addition

The new variable __snapshot_0_m_1 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_m_1m_1m_1__snapshot_0_m_1
7: __snapshot_0_m_1__snapshot_0_m_1__snapshot_0_m_1__snapshot_0_m_1
0: __snapshot_0_m_1__snapshot_0_m_1__snapshot_0_m_1__snapshot_0_m_1
1: __snapshot_0_m_1__snapshot_0_m_1__snapshot_0_m_1__snapshot_0_m_1

6.1.1.1.29 Fresh Variable Addition

The new variable __snapshot_0_m_0 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_m_0m_0m_0__snapshot_0_m_0
7: __snapshot_0_m_0__snapshot_0_m_0__snapshot_0_m_0__snapshot_0_m_0
0: __snapshot_0_m_0__snapshot_0_m_0__snapshot_0_m_0__snapshot_0_m_0
1: __snapshot_0_m_0__snapshot_0_m_0__snapshot_0_m_0__snapshot_0_m_0

6.1.1.1.30 Fresh Variable Addition

The new variable __snapshot_0_c2_post is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c2_postc2_postc2_post__snapshot_0_c2_post
7: __snapshot_0_c2_post__snapshot_0_c2_post__snapshot_0_c2_post__snapshot_0_c2_post
0: __snapshot_0_c2_post__snapshot_0_c2_post__snapshot_0_c2_post__snapshot_0_c2_post
1: __snapshot_0_c2_post__snapshot_0_c2_post__snapshot_0_c2_post__snapshot_0_c2_post

6.1.1.1.31 Fresh Variable Addition

The new variable __snapshot_0_c2_3 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c2_3c2_3c2_3__snapshot_0_c2_3
7: __snapshot_0_c2_3__snapshot_0_c2_3__snapshot_0_c2_3__snapshot_0_c2_3
0: __snapshot_0_c2_3__snapshot_0_c2_3__snapshot_0_c2_3__snapshot_0_c2_3
1: __snapshot_0_c2_3__snapshot_0_c2_3__snapshot_0_c2_3__snapshot_0_c2_3

6.1.1.1.32 Fresh Variable Addition

The new variable __snapshot_0_c2_2 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c2_2c2_2c2_2__snapshot_0_c2_2
7: __snapshot_0_c2_2__snapshot_0_c2_2__snapshot_0_c2_2__snapshot_0_c2_2
0: __snapshot_0_c2_2__snapshot_0_c2_2__snapshot_0_c2_2__snapshot_0_c2_2
1: __snapshot_0_c2_2__snapshot_0_c2_2__snapshot_0_c2_2__snapshot_0_c2_2

6.1.1.1.33 Fresh Variable Addition

The new variable __snapshot_0_c2_1 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c2_1c2_1c2_1__snapshot_0_c2_1
7: __snapshot_0_c2_1__snapshot_0_c2_1__snapshot_0_c2_1__snapshot_0_c2_1
0: __snapshot_0_c2_1__snapshot_0_c2_1__snapshot_0_c2_1__snapshot_0_c2_1
1: __snapshot_0_c2_1__snapshot_0_c2_1__snapshot_0_c2_1__snapshot_0_c2_1

6.1.1.1.34 Fresh Variable Addition

The new variable __snapshot_0_c2_0 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c2_0c2_0c2_0__snapshot_0_c2_0
7: __snapshot_0_c2_0__snapshot_0_c2_0__snapshot_0_c2_0__snapshot_0_c2_0
0: __snapshot_0_c2_0__snapshot_0_c2_0__snapshot_0_c2_0__snapshot_0_c2_0
1: __snapshot_0_c2_0__snapshot_0_c2_0__snapshot_0_c2_0__snapshot_0_c2_0

6.1.1.1.35 Fresh Variable Addition

The new variable __snapshot_0_c1_post is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c1_postc1_postc1_post__snapshot_0_c1_post
7: __snapshot_0_c1_post__snapshot_0_c1_post__snapshot_0_c1_post__snapshot_0_c1_post
0: __snapshot_0_c1_post__snapshot_0_c1_post__snapshot_0_c1_post__snapshot_0_c1_post
1: __snapshot_0_c1_post__snapshot_0_c1_post__snapshot_0_c1_post__snapshot_0_c1_post

6.1.1.1.36 Fresh Variable Addition

The new variable __snapshot_0_c1_4 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c1_4c1_4c1_4__snapshot_0_c1_4
7: __snapshot_0_c1_4__snapshot_0_c1_4__snapshot_0_c1_4__snapshot_0_c1_4
0: __snapshot_0_c1_4__snapshot_0_c1_4__snapshot_0_c1_4__snapshot_0_c1_4
1: __snapshot_0_c1_4__snapshot_0_c1_4__snapshot_0_c1_4__snapshot_0_c1_4

6.1.1.1.37 Fresh Variable Addition

The new variable __snapshot_0_c1_3 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c1_3c1_3c1_3__snapshot_0_c1_3
7: __snapshot_0_c1_3__snapshot_0_c1_3__snapshot_0_c1_3__snapshot_0_c1_3
0: __snapshot_0_c1_3__snapshot_0_c1_3__snapshot_0_c1_3__snapshot_0_c1_3
1: __snapshot_0_c1_3__snapshot_0_c1_3__snapshot_0_c1_3__snapshot_0_c1_3

6.1.1.1.38 Fresh Variable Addition

The new variable __snapshot_0_c1_2 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c1_2c1_2c1_2__snapshot_0_c1_2
7: __snapshot_0_c1_2__snapshot_0_c1_2__snapshot_0_c1_2__snapshot_0_c1_2
0: __snapshot_0_c1_2__snapshot_0_c1_2__snapshot_0_c1_2__snapshot_0_c1_2
1: __snapshot_0_c1_2__snapshot_0_c1_2__snapshot_0_c1_2__snapshot_0_c1_2

6.1.1.1.39 Fresh Variable Addition

The new variable __snapshot_0_c1_1 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c1_1c1_1c1_1__snapshot_0_c1_1
7: __snapshot_0_c1_1__snapshot_0_c1_1__snapshot_0_c1_1__snapshot_0_c1_1
0: __snapshot_0_c1_1__snapshot_0_c1_1__snapshot_0_c1_1__snapshot_0_c1_1
1: __snapshot_0_c1_1__snapshot_0_c1_1__snapshot_0_c1_1__snapshot_0_c1_1

6.1.1.1.40 Fresh Variable Addition

The new variable __snapshot_0_c1_0 is introduced. The transition formulas are extended as follows:

5: __snapshot_0_c1_0c1_0c1_0__snapshot_0_c1_0
7: __snapshot_0_c1_0__snapshot_0_c1_0__snapshot_0_c1_0__snapshot_0_c1_0
0: __snapshot_0_c1_0__snapshot_0_c1_0__snapshot_0_c1_0__snapshot_0_c1_0
1: __snapshot_0_c1_0__snapshot_0_c1_0__snapshot_0_c1_0__snapshot_0_c1_0

6.1.1.1.41 Invariant Updates

The following invariants are asserted.

0: c1_post ≤ 0c1_post + pi_0seq_0 ≤ 0max_0n_post ≤ 0c1_post ≤ 0max_post ≤ 0n_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0c1_post + pi_0seq_0 ≤ 0c1_postn_post ≤ 0max_0n_post ≤ 0c1_post ≤ 0max_post ≤ 0n_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0
1: c1_0 + c1_post + 2⋅c2_1 + m_1n_post ≤ 01 − c1_0 + c1_post + pi_0seq_0 ≤ 01 + pi_0seq_0 ≤ 0m_3n_post ≤ 0max_0n_post ≤ 0−1 + c1_post ≤ 01 − c1_post ≤ 0max_post ≤ 0n_post ≤ 0−1 + pos_post ≤ 01 − pos_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0−1 + c1_0 ≤ 01 − c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0−1 + pos_0 ≤ 01 − pos_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0c2_post ≤ 0c2_post ≤ 0−1 + c1_1 ≤ 01 − c1_1 ≤ 0−1 + c1_2 ≤ 01 − c1_2 ≤ 0−1 + c1_3 ≤ 01 − c1_3 ≤ 0c1_4 ≤ 0c1_4 ≤ 0c2_1 ≤ 0c2_1 ≤ 0−1 + c2_2 ≤ 01 − c2_2 ≤ 0−1 + c2_3 ≤ 01 − c2_3 ≤ 01 − m_1 ≤ 01 − m_2 ≤ 01 − m_3 ≤ 0pi_1 ≤ 01 − pi_2 ≤ 0−1 + wpos_1 ≤ 01 − wpos_1 ≤ 0wpos_2 ≤ 0wpos_2 ≤ 0−1 + wpos_3 ≤ 01 − wpos_3 ≤ 0wpos_4 ≤ 0wpos_4 ≤ 0−1 + wpos_5 ≤ 01 − wpos_5 ≤ 01 − z_1 ≤ 01 − z_2 ≤ 0c2_0 ≤ 0c2_0 ≤ 0
2: TRUE
3: TRUE
0: c1_post ≤ 0c1_post + pi_0seq_0 ≤ 0max_0n_post ≤ 0c1_post ≤ 0max_post ≤ 0n_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0−1 + __snapshot_0_c1_post__snapshot_0_n_post + __snapshot_0_pi_0 ≤ 01 + __snapshot_0_c1_post__snapshot_0_n_post + __snapshot_0_pi_0c1_post + n_postpi_0 ≤ 0−3 + c1_post + max_0n_post ≤ 0c1_post + pi_0seq_0 ≤ 0c1_postn_post ≤ 0max_0n_post ≤ 0c1_post ≤ 0max_post ≤ 0n_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0c1_post + pi_0seq_0 ≤ 0c1_postn_post ≤ 0max_0n_post ≤ 0c1_post ≤ 0max_post ≤ 0n_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0
1: −1 + __snapshot_0_c1_post__snapshot_0_n_post + __snapshot_0_pi_0 ≤ 02 − c1_0 + c1_post + m_1n_post ≤ 0−3 + 2⋅c1_4 + c1_post + max_0n_post ≤ 0__snapshot_0_c1_post__snapshot_0_n_post + __snapshot_0_pi_0 + n_postpi_0 ≤ 01 + pi_0seq_0 ≤ 0c1_post + pi_0seq_0 ≤ 0m_2n_post ≤ 0max_0n_post ≤ 0−1 + c1_post ≤ 01 − c1_post ≤ 0max_post ≤ 0n_post ≤ 0−1 + pos_post ≤ 01 − pos_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0−1 + c1_0 ≤ 01 − c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0−1 + pos_0 ≤ 01 − pos_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0c2_post ≤ 0c2_post ≤ 0−1 + c1_1 ≤ 01 − c1_1 ≤ 0−1 + c1_2 ≤ 01 − c1_2 ≤ 0−1 + c1_3 ≤ 01 − c1_3 ≤ 0c1_4 ≤ 0c1_4 ≤ 0c2_1 ≤ 0c2_1 ≤ 0−1 + c2_2 ≤ 01 − c2_2 ≤ 0−1 + c2_3 ≤ 01 − c2_3 ≤ 01 − m_1 ≤ 01 − m_2 ≤ 01 − m_3 ≤ 0pi_1 ≤ 01 − pi_2 ≤ 0−1 + wpos_1 ≤ 01 − wpos_1 ≤ 0wpos_2 ≤ 0wpos_2 ≤ 0−1 + wpos_3 ≤ 01 − wpos_3 ≤ 0wpos_4 ≤ 0wpos_4 ≤ 0−1 + wpos_5 ≤ 01 − wpos_5 ≤ 01 − z_1 ≤ 01 − z_2 ≤ 0c2_0 ≤ 0c2_0 ≤ 0
0_var_snapshot: __snapshot_0_c1_post__snapshot_0_n_post + __snapshot_0_pi_0 + n_postseq_0 ≤ 0__snapshot_0_c1_post__snapshot_0_n_post + __snapshot_0_pi_0pi_0 ≤ 0max_0n_post ≤ 0c1_post ≤ 0max_post ≤ 0n_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0
0*: −1 + __snapshot_0_c1_post__snapshot_0_n_post + __snapshot_0_pi_0 ≤ 01 + __snapshot_0_c1_post__snapshot_0_n_post + __snapshot_0_pi_0c1_post + n_postpi_0 ≤ 0−3 + c1_post + max_0n_post ≤ 02⋅c1_0 + c1_postn_post ≤ 0c1_post + pi_0seq_0 ≤ 0c1_postn_post ≤ 0max_0n_post ≤ 0c1_post ≤ 0max_post ≤ 0n_post ≤ 0wpos_post ≤ 0wpos_post ≤ 0z_post ≤ 0pos_1 ≤ 0pos_1 ≤ 0c1_0 ≤ 0max_0 ≤ 0n_0 ≤ 0wpos_0 ≤ 0wpos_0 ≤ 0z_0 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

6.1.1.1.42 Transition Removal

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

0: c1_post + n_postpi_0
1: __snapshot_0_c1_post + __snapshot_0_n_post__snapshot_0_pi_0
0_var_snapshot: __snapshot_0_c1_post + __snapshot_0_n_post__snapshot_0_pi_0
0*: __snapshot_0_c1_post + __snapshot_0_n_post__snapshot_0_pi_0

6.1.1.1.43 Transition Removal

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

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

6.1.1.1.44 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert