LTS Termination Proof

by AProVE

Input

• Initial Location: f1_0_main_Load, f292_0_slide88_EQ', f196_0_create_LE, f234_0_slide88_FieldAccess, __init, f292_0_slide88_EQ
• Transitions: (pre-variables and post-variables)

  f1_0_main_Load	1	f234_0_slide88_FieldAccess:		x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x6 = _arg6 ∧ x7 = _arg7 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ x6 = _arg6P ∧ x7 = _arg7P ∧ −1 ≤ _x4 − 1 ∧ 1 ≤ _arg2 − 1 ∧ −1 ≤ _arg1P − 1 ∧ _arg2P ≤ _x5 − 1 ∧ −1 ≤ _x5 − 1 ∧ 0 ≤ _arg1 − 1
  f1_0_main_Load	2	f234_0_slide88_FieldAccess:		x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x6 ∧ x6 = _x7 ∧ x7 = _x8 ∧ x1 = _x9 ∧ x2 = _x11 ∧ x3 = _x12 ∧ x4 = _x13 ∧ x5 = _x14 ∧ x6 = _x15 ∧ x7 = _x16 ∧ −1 ≤ _x17 − 1 ∧ 1 ≤ _x1 − 1 ∧ _x11 ≤ 0 ∧ −1 ≤ _x9 − 1 ∧ 0 ≤ _x − 1
  f234_0_slide88_FieldAccess	3	f292_0_slide88_EQ:		x1 = _x18 ∧ x2 = _x19 ∧ x3 = _x20 ∧ x4 = _x21 ∧ x5 = _x22 ∧ x6 = _x23 ∧ x7 = _x24 ∧ x1 = _x25 ∧ x2 = _x26 ∧ x3 = _x27 ∧ x4 = _x28 ∧ x5 = _x29 ∧ x6 = _x30 ∧ x7 = _x31 ∧ _x19 = _x31 ∧ _x19 = _x30 ∧ 0 = _x29 ∧ _x19 = _x28 ∧ _x19 = _x27 ∧ 0 = _x26 ∧ _x18 = _x25 ∧ 0 ≤ _x19 − 1
  f292_0_slide88_EQ	4	f292_0_slide88_EQ':		x1 = _x32 ∧ x2 = _x33 ∧ x3 = _x34 ∧ x4 = _x35 ∧ x5 = _x36 ∧ x6 = _x37 ∧ x7 = _x38 ∧ x1 = _x39 ∧ x2 = _x42 ∧ x3 = _x43 ∧ x4 = _x44 ∧ x5 = _x45 ∧ x6 = _x46 ∧ x7 = _x47 ∧ 0 ≤ _x55 − 1 ∧ 0 ≤ _x35 − 1 ∧ 0 ≤ _x36 − 1 ∧ −1 ≤ _x37 − 1 ∧ _x37 ≤ _x33 − 1 ∧ _x37 ≤ _x56 − 1 ∧ _x37 ≤ _x34 − 1 ∧ _x38 ≤ _x55 − 1 ∧ −1 ≤ _x38 − 1 ∧ _x38 ≤ _x36 − 1 ∧ _x57 ≤ _x35 − 1 ∧ _x38 ≤ _x35 − 1 ∧ _x32 − 2⋅_x58 = 0 ∧ _x59 ≤ _x55 − 1 ∧ 0 ≤ _x56 − 1 ∧ 0 ≤ _x33 − 1 ∧ _x60 ≤ _x32 ∧ _x61 ≤ _x36 − 1 ∧ _x32 = _x39 ∧ _x33 = _x42 ∧ _x34 = _x43 ∧ _x35 = _x44 ∧ _x36 = _x45 ∧ _x37 = _x46 ∧ _x38 = _x47
  f292_0_slide88_EQ'	5	f292_0_slide88_EQ:		x1 = _x62 ∧ x2 = _x63 ∧ x3 = _x64 ∧ x4 = _x65 ∧ x5 = _x66 ∧ x6 = _x70 ∧ x7 = _x71 ∧ x1 = _x72 ∧ x2 = _x73 ∧ x3 = _x74 ∧ x4 = _x75 ∧ x5 = _x76 ∧ x6 = _x82 ∧ x7 = _x83 ∧ 0 ≤ _x84 − 1 ∧ 0 ≤ _x65 − 1 ∧ 0 ≤ _x66 − 1 ∧ −1 ≤ _x70 − 1 ∧ _x70 ≤ _x63 − 1 ∧ _x70 ≤ _x85 − 1 ∧ _x70 ≤ _x64 − 1 ∧ _x71 ≤ _x84 − 1 ∧ −1 ≤ _x71 − 1 ∧ _x71 ≤ _x66 − 1 ∧ _x75 ≤ _x65 − 1 ∧ _x71 ≤ _x65 − 1 ∧ _x62 − 2⋅_x86 = 0 ∧ _x83 ≤ _x84 − 1 ∧ 0 ≤ _x85 − 1 ∧ 0 ≤ _x63 − 1 ∧ _x76 ≤ _x66 − 1 ∧ _x72 ≤ _x62 ∧ 0 ≤ _x62 − 2⋅_x86 ∧ _x62 − 2⋅_x86 ≤ 1 ∧ _x62 − 2⋅_x72 ≤ 1 ∧ 0 ≤ _x62 − 2⋅_x72 ∧ _x64 = _x74 ∧ _x63 = _x82
  f292_0_slide88_EQ	6	f292_0_slide88_EQ':		x1 = _x87 ∧ x2 = _x88 ∧ x3 = _x89 ∧ x4 = _x90 ∧ x5 = _x91 ∧ x6 = _x92 ∧ x7 = _x95 ∧ x1 = _x96 ∧ x2 = _x97 ∧ x3 = _x98 ∧ x4 = _x99 ∧ x5 = _x100 ∧ x6 = _x101 ∧ x7 = _x102 ∧ −1 ≤ _x92 − 1 ∧ 0 ≤ _x89 − 1 ∧ _x92 ≤ _x88 − 1 ∧ _x92 ≤ _x103 − 1 ∧ _x92 ≤ _x89 − 1 ∧ _x95 ≤ _x103 − 1 ∧ −1 ≤ _x95 − 1 ∧ _x95 ≤ _x91 − 1 ∧ _x95 ≤ _x89 − 1 ∧ _x87 − 2⋅_x104 = 0 ∧ _x105 ≤ _x89 − 1 ∧ _x106 ≤ _x103 − 1 ∧ −1 ≤ _x103 − 1 ∧ _x107 ≤ _x87 ∧ _x89 = _x90 ∧ _x87 = _x96 ∧ _x88 = _x97 ∧ _x89 = _x98 ∧ _x89 = _x99 ∧ _x91 = _x100 ∧ _x92 = _x101 ∧ _x95 = _x102
  f292_0_slide88_EQ'	7	f292_0_slide88_EQ:		x1 = _x108 ∧ x2 = _x109 ∧ x3 = _x110 ∧ x4 = _x111 ∧ x5 = _x112 ∧ x6 = _x113 ∧ x7 = _x114 ∧ x1 = _x115 ∧ x2 = _x116 ∧ x3 = _x117 ∧ x4 = _x118 ∧ x5 = _x119 ∧ x6 = _x120 ∧ x7 = _x121 ∧ −1 ≤ _x113 − 1 ∧ 0 ≤ _x110 − 1 ∧ _x113 ≤ _x109 − 1 ∧ _x113 ≤ _x122 − 1 ∧ _x113 ≤ _x110 − 1 ∧ _x114 ≤ _x122 − 1 ∧ −1 ≤ _x114 − 1 ∧ _x114 ≤ _x112 − 1 ∧ _x114 ≤ _x110 − 1 ∧ _x108 − 2⋅_x123 = 0 ∧ _x118 ≤ _x110 − 1 ∧ _x119 ≤ _x122 − 1 ∧ _x115 ≤ _x108 ∧ −1 ≤ _x122 − 1 ∧ 0 ≤ _x108 − 2⋅_x123 ∧ _x108 − 2⋅_x123 ≤ 1 ∧ _x108 − 2⋅_x115 ≤ 1 ∧ 0 ≤ _x108 − 2⋅_x115 ∧ _x110 = _x111 ∧ 1 = _x116 ∧ 0 = _x120 ∧ _x119 = _x121
  f1_0_main_Load	8	f196_0_create_LE:		x1 = _x124 ∧ x2 = _x125 ∧ x3 = _x126 ∧ x4 = _x127 ∧ x5 = _x128 ∧ x6 = _x129 ∧ x7 = _x130 ∧ x1 = _x131 ∧ x2 = _x132 ∧ x3 = _x133 ∧ x4 = _x134 ∧ x5 = _x135 ∧ x6 = _x136 ∧ x7 = _x137 ∧ −1 ≤ _x138 − 1 ∧ 1 ≤ _x125 − 1 ∧ −1 ≤ _x139 − 1 ∧ 0 ≤ _x124 − 1 ∧ _x139 − 1 = _x131
  f196_0_create_LE	9	f196_0_create_LE:		x1 = _x140 ∧ x2 = _x141 ∧ x3 = _x142 ∧ x4 = _x143 ∧ x5 = _x144 ∧ x6 = _x145 ∧ x7 = _x146 ∧ x1 = _x147 ∧ x2 = _x148 ∧ x3 = _x149 ∧ x4 = _x150 ∧ x5 = _x151 ∧ x6 = _x152 ∧ x7 = _x153 ∧ _x140 − 1 = _x147 ∧ 0 ≤ _x140 − 1
  __init	10	f1_0_main_Load:		x1 = _x154 ∧ x2 = _x155 ∧ x3 = _x156 ∧ x4 = _x157 ∧ x5 = _x158 ∧ x6 = _x159 ∧ x7 = _x160 ∧ x1 = _x161 ∧ x2 = _x162 ∧ x3 = _x163 ∧ x4 = _x164 ∧ x5 = _x165 ∧ x6 = _x166 ∧ x7 = _x167 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 SCC Decomposition

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

2.1 SCC Subproblem 1/2

Here we consider the SCC { f196_0_create_LE }.

2.1.1 Transition Removal

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

2.1.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.2 SCC Subproblem 2/2

Here we consider the SCC { f292_0_slide88_EQ', f292_0_slide88_EQ }.

2.2.1 Transition Removal

We remove transitions 4, 5, 6, 7 using the following ranking functions, which are bounded by 0.

2.2.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

Tool configuration

AProVE

• version: AProVE Commit ID: unknown
• strategy: Statistics for single proof: 100.00 % (7 real / 0 unknown / 0 assumptions / 7 total proof steps)