LTS Termination Proof

by AProVE

Input

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

  f1_0_main_Load	1	f234_0_slide68_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_slide68_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_slide68_FieldAccess	3	f288_0_slide68_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
  f288_0_slide68_EQ	4	f288_0_slide68_EQ':		x1 = _x32 ∧ x2 = _x33 ∧ x3 = _x34 ∧ x4 = _x35 ∧ x5 = _x36 ∧ x6 = _x37 ∧ x7 = _x38 ∧ x1 = _x39 ∧ x2 = _x40 ∧ x3 = _x41 ∧ x4 = _x42 ∧ x5 = _x43 ∧ x6 = _x44 ∧ x7 = _x45 ∧ _x46 ≤ _x34 − 1 ∧ 0 ≤ _x34 − 1 ∧ _x47 ≤ _x37 − 1 ∧ −1 ≤ _x37 − 1 ∧ _x48 ≤ _x49 − 1 ∧ −1 ≤ _x47 − 1 ∧ _x47 ≤ _x48 − 1 ∧ −1 ≤ _x49 − 1 ∧ _x47 ≤ _x50 − 1 ∧ _x47 ≤ _x46 − 1 ∧ _x51 ≤ _x32 ∧ _x32 − 2⋅_x52 = 0 ∧ _x34 = _x35 ∧ _x37 = _x38 ∧ _x32 = _x39 ∧ _x33 = _x40 ∧ _x34 = _x41 ∧ _x34 = _x42 ∧ _x36 = _x43 ∧ _x37 = _x44 ∧ _x37 = _x45
  f288_0_slide68_EQ'	5	f288_0_slide68_EQ:		x1 = _x53 ∧ x2 = _x54 ∧ x3 = _x55 ∧ x4 = _x56 ∧ x5 = _x57 ∧ x6 = _x58 ∧ x7 = _x59 ∧ x1 = _x60 ∧ x2 = _x61 ∧ x3 = _x62 ∧ x4 = _x63 ∧ x5 = _x64 ∧ x6 = _x65 ∧ x7 = _x66 ∧ _x63 ≤ _x55 − 1 ∧ 0 ≤ _x55 − 1 ∧ _x67 ≤ _x58 − 1 ∧ −1 ≤ _x58 − 1 ∧ _x64 ≤ _x68 − 1 ∧ −1 ≤ _x67 − 1 ∧ _x67 ≤ _x64 − 1 ∧ −1 ≤ _x68 − 1 ∧ _x67 ≤ _x69 − 1 ∧ _x67 ≤ _x63 − 1 ∧ _x53 − 2⋅_x70 = 0 ∧ _x60 ≤ _x53 ∧ 0 ≤ _x53 − 2⋅_x70 ∧ _x53 − 2⋅_x70 ≤ 1 ∧ _x53 − 2⋅_x60 ≤ 1 ∧ 0 ≤ _x53 − 2⋅_x60 ∧ _x55 = _x56 ∧ _x58 = _x59 ∧ 1 = _x61 ∧ 0 = _x65 ∧ _x64 = _x66
  f288_0_slide68_EQ	6	f288_0_slide68_EQ':		x1 = _x71 ∧ x2 = _x72 ∧ x3 = _x73 ∧ x4 = _x74 ∧ x5 = _x75 ∧ x6 = _x76 ∧ x7 = _x77 ∧ x1 = _x78 ∧ x2 = _x79 ∧ x3 = _x80 ∧ x4 = _x81 ∧ x5 = _x82 ∧ x6 = _x83 ∧ x7 = _x84 ∧ 0 ≤ _x74 − 1 ∧ 0 ≤ _x75 − 1 ∧ −1 ≤ _x77 − 1 ∧ _x85 ≤ _x77 − 1 ∧ _x86 ≤ _x74 − 1 ∧ _x85 ≤ _x75 − 1 ∧ 0 ≤ _x72 − 1 ∧ _x71 − 2⋅_x87 = 1 ∧ −1 ≤ _x88 − 1 ∧ _x86 ≤ _x88 − 1 ∧ _x89 ≤ _x71 ∧ −1 ≤ _x86 − 1 ∧ _x90 ≤ _x86 ∧ 0 ≤ _x85 − 1 ∧ _x71 = _x78 ∧ _x72 = _x79 ∧ _x73 = _x80 ∧ _x74 = _x81 ∧ _x75 = _x82 ∧ _x76 = _x83 ∧ _x77 = _x84
  f288_0_slide68_EQ'	7	f288_0_slide68_EQ:		x1 = _x91 ∧ x2 = _x92 ∧ x3 = _x93 ∧ x4 = _x94 ∧ x5 = _x97 ∧ x6 = _x98 ∧ x7 = _x106 ∧ x1 = _x107 ∧ x2 = _x108 ∧ x3 = _x109 ∧ x4 = _x110 ∧ x5 = _x111 ∧ x6 = _x112 ∧ x7 = _x113 ∧ 0 ≤ _x94 − 1 ∧ 0 ≤ _x97 − 1 ∧ −1 ≤ _x106 − 1 ∧ _x111 ≤ _x106 − 1 ∧ _x114 ≤ _x94 − 1 ∧ _x111 ≤ _x97 − 1 ∧ 0 ≤ _x92 − 1 ∧ _x91 − 2⋅_x115 = 1 ∧ −1 ≤ _x116 − 1 ∧ _x114 ≤ _x116 − 1 ∧ _x107 ≤ _x91 ∧ −1 ≤ _x114 − 1 ∧ 0 ≤ _x111 − 1 ∧ _x110 ≤ _x114 ∧ 0 ≤ _x91 − 2⋅_x115 ∧ _x91 − 2⋅_x115 ≤ 1 ∧ _x91 − 2⋅_x107 ≤ 1 ∧ 0 ≤ _x91 − 2⋅_x107 ∧ 1 = _x108 ∧ 0 = _x112 ∧ _x111 = _x113
  f288_0_slide68_EQ	8	f288_0_slide68_EQ':		x1 = _x121 ∧ x2 = _x122 ∧ x3 = _x123 ∧ x4 = _x124 ∧ x5 = _x125 ∧ x6 = _x126 ∧ x7 = _x127 ∧ x1 = _x134 ∧ x2 = _x135 ∧ x3 = _x136 ∧ x4 = _x137 ∧ x5 = _x138 ∧ x6 = _x139 ∧ x7 = _x140 ∧ _x141 ≤ _x123 − 1 ∧ 0 ≤ _x123 − 1 ∧ _x141 ≤ _x126 − 1 ∧ −1 ≤ _x126 − 1 ∧ _x142 ≤ _x143 − 1 ∧ −1 ≤ _x143 − 1 ∧ _x121 − 2⋅_x144 = 1 ∧ 0 ≤ _x141 − 1 ∧ _x148 ≤ _x121 ∧ _x123 = _x124 ∧ _x126 = _x127 ∧ _x121 = _x134 ∧ _x122 = _x135 ∧ _x123 = _x136 ∧ _x123 = _x137 ∧ _x125 = _x138 ∧ _x126 = _x139 ∧ _x126 = _x140
  f288_0_slide68_EQ'	9	f288_0_slide68_EQ:		x1 = _x149 ∧ x2 = _x150 ∧ x3 = _x151 ∧ x4 = _x152 ∧ x5 = _x153 ∧ x6 = _x154 ∧ x7 = _x155 ∧ x1 = _x161 ∧ x2 = _x162 ∧ x3 = _x163 ∧ x4 = _x164 ∧ x5 = _x165 ∧ x6 = _x166 ∧ x7 = _x167 ∧ _x163 ≤ _x151 − 1 ∧ 0 ≤ _x151 − 1 ∧ _x163 ≤ _x154 − 1 ∧ −1 ≤ _x154 − 1 ∧ _x168 ≤ _x169 − 1 ∧ −1 ≤ _x169 − 1 ∧ _x149 − 2⋅_x171 = 1 ∧ _x161 ≤ _x149 ∧ 0 ≤ _x163 − 1 ∧ 0 ≤ _x149 − 2⋅_x171 ∧ _x149 − 2⋅_x171 ≤ 1 ∧ _x149 − 2⋅_x161 ≤ 1 ∧ 0 ≤ _x149 − 2⋅_x161 ∧ _x151 = _x152 ∧ _x154 = _x155 ∧ 0 = _x162 ∧ _x163 = _x164 ∧ 0 = _x165 ∧ _x163 = _x166 ∧ _x163 = _x167
  f288_0_slide68_EQ	10	f288_0_slide68_EQ':		x1 = _x174 ∧ x2 = _x175 ∧ x3 = _x176 ∧ x4 = _x177 ∧ x5 = _x178 ∧ x6 = _x179 ∧ x7 = _x180 ∧ x1 = _x190 ∧ x2 = _x191 ∧ x3 = _x192 ∧ x4 = _x193 ∧ x5 = _x194 ∧ x6 = _x195 ∧ x7 = _x196 ∧ 0 ≤ _x177 − 1 ∧ 0 ≤ _x178 − 1 ∧ −1 ≤ _x179 − 1 ∧ _x179 ≤ _x175 − 1 ∧ _x179 ≤ _x197 − 1 ∧ _x179 ≤ _x176 − 1 ∧ _x179 ≤ _x198 − 1 ∧ −1 ≤ _x180 − 1 ∧ _x199 ≤ _x180 − 1 ∧ _x199 ≤ _x200 − 1 ∧ _x201 ≤ _x177 − 1 ∧ −1 ≤ _x199 − 1 ∧ _x199 ≤ _x207 − 1 ∧ _x208 ≤ _x178 − 1 ∧ 0 ≤ _x175 − 1 ∧ _x199 ≤ _x201 − 1 ∧ _x199 ≤ _x208 − 1 ∧ _x209 ≤ _x174 ∧ _x174 − 2⋅_x210 = 0 ∧ _x174 = _x190 ∧ _x175 = _x191 ∧ _x176 = _x192 ∧ _x177 = _x193 ∧ _x178 = _x194 ∧ _x179 = _x195 ∧ _x180 = _x196
  f288_0_slide68_EQ'	11	f288_0_slide68_EQ:		x1 = _x211 ∧ x2 = _x212 ∧ x3 = _x213 ∧ x4 = _x222 ∧ x5 = _x223 ∧ x6 = _x224 ∧ x7 = _x225 ∧ x1 = _x226 ∧ x2 = _x227 ∧ x3 = _x228 ∧ x4 = _x229 ∧ x5 = _x230 ∧ x6 = _x231 ∧ x7 = _x232 ∧ 0 ≤ _x222 − 1 ∧ 0 ≤ _x223 − 1 ∧ −1 ≤ _x224 − 1 ∧ _x224 ≤ _x212 − 1 ∧ _x224 ≤ _x233 − 1 ∧ _x224 ≤ _x213 − 1 ∧ _x224 ≤ _x234 − 1 ∧ −1 ≤ _x225 − 1 ∧ _x238 ≤ _x225 − 1 ∧ _x238 ≤ _x232 − 1 ∧ _x229 ≤ _x222 − 1 ∧ −1 ≤ _x238 − 1 ∧ _x238 ≤ _x239 − 1 ∧ _x230 ≤ _x223 − 1 ∧ 0 ≤ _x212 − 1 ∧ _x238 ≤ _x229 − 1 ∧ _x238 ≤ _x230 − 1 ∧ _x211 − 2⋅_x240 = 0 ∧ _x226 ≤ _x211 ∧ 0 ≤ _x211 − 2⋅_x240 ∧ _x211 − 2⋅_x240 ≤ 1 ∧ _x211 − 2⋅_x226 ≤ 1 ∧ 0 ≤ _x211 − 2⋅_x226 ∧ _x213 = _x228 ∧ _x212 = _x231
  f288_0_slide68_EQ	12	f288_0_slide68_EQ':		x1 = _x241 ∧ x2 = _x242 ∧ x3 = _x243 ∧ x4 = _x244 ∧ x5 = _x252 ∧ x6 = _x253 ∧ x7 = _x254 ∧ x1 = _x255 ∧ x2 = _x256 ∧ x3 = _x257 ∧ x4 = _x258 ∧ x5 = _x259 ∧ x6 = _x260 ∧ x7 = _x261 ∧ 0 ≤ _x244 − 1 ∧ 0 ≤ _x252 − 1 ∧ −1 ≤ _x254 − 1 ∧ _x262 ≤ _x254 − 1 ∧ _x263 ≤ _x244 − 1 ∧ _x264 ≤ _x252 − 1 ∧ 0 ≤ _x242 − 1 ∧ _x241 − 2⋅_x265 = 1 ∧ −1 ≤ _x243 − 1 ∧ _x270 ≤ _x243 ∧ _x271 ≤ _x263 ∧ −1 ≤ _x263 − 1 ∧ _x272 ≤ _x264 ∧ 0 ≤ _x253 − 1 ∧ _x273 ≤ _x241 ∧ −1 ≤ _x264 − 1 ∧ 0 ≤ _x262 − 1 ∧ _x241 = _x255 ∧ _x242 = _x256 ∧ _x243 = _x257 ∧ _x244 = _x258 ∧ _x252 = _x259 ∧ _x253 = _x260 ∧ _x254 = _x261
  f288_0_slide68_EQ'	13	f288_0_slide68_EQ:		x1 = _x274 ∧ x2 = _x275 ∧ x3 = _x276 ∧ x4 = _x277 ∧ x5 = _x278 ∧ x6 = _x279 ∧ x7 = _x280 ∧ x1 = _x281 ∧ x2 = _x282 ∧ x3 = _x283 ∧ x4 = _x284 ∧ x5 = _x285 ∧ x6 = _x286 ∧ x7 = _x287 ∧ 0 ≤ _x277 − 1 ∧ 0 ≤ _x278 − 1 ∧ −1 ≤ _x280 − 1 ∧ _x287 ≤ _x280 − 1 ∧ _x288 ≤ _x277 − 1 ∧ _x289 ≤ _x278 − 1 ∧ 0 ≤ _x275 − 1 ∧ _x274 − 2⋅_x290 = 1 ∧ −1 ≤ _x276 − 1 ∧ _x283 ≤ _x276 ∧ _x284 ≤ _x288 ∧ −1 ≤ _x288 − 1 ∧ _x285 ≤ _x289 ∧ 0 ≤ _x279 − 1 ∧ _x281 ≤ _x274 ∧ 0 ≤ _x287 − 1 ∧ −1 ≤ _x289 − 1 ∧ 0 ≤ _x274 − 2⋅_x290 ∧ _x274 − 2⋅_x290 ≤ 1 ∧ _x274 − 2⋅_x281 ≤ 1 ∧ 0 ≤ _x274 − 2⋅_x281 ∧ _x279 = _x286
  f288_0_slide68_EQ	14	f288_0_slide68_EQ':		x1 = _x291 ∧ x2 = _x292 ∧ x3 = _x293 ∧ x4 = _x294 ∧ x5 = _x295 ∧ x6 = _x296 ∧ x7 = _x297 ∧ x1 = _x298 ∧ x2 = _x299 ∧ x3 = _x300 ∧ x4 = _x301 ∧ x5 = _x302 ∧ x6 = _x303 ∧ x7 = _x304 ∧ _x305 ≤ _x293 − 1 ∧ 0 ≤ _x293 − 1 ∧ _x306 ≤ _x296 − 1 ∧ −1 ≤ _x296 − 1 ∧ _x307 ≤ _x308 − 1 ∧ −1 ≤ _x308 − 1 ∧ _x291 − 2⋅_x309 = 1 ∧ _x310 ≤ _x291 ∧ −1 ≤ _x305 − 1 ∧ _x311 ≤ _x305 ∧ 0 ≤ _x306 − 1 ∧ _x293 = _x294 ∧ _x296 = _x297 ∧ _x291 = _x298 ∧ _x292 = _x299 ∧ _x293 = _x300 ∧ _x293 = _x301 ∧ _x295 = _x302 ∧ _x296 = _x303 ∧ _x296 = _x304
  f288_0_slide68_EQ'	15	f288_0_slide68_EQ:		x1 = _x312 ∧ x2 = _x313 ∧ x3 = _x314 ∧ x4 = _x315 ∧ x5 = _x316 ∧ x6 = _x317 ∧ x7 = _x318 ∧ x1 = _x319 ∧ x2 = _x320 ∧ x3 = _x321 ∧ x4 = _x322 ∧ x5 = _x323 ∧ x6 = _x324 ∧ x7 = _x325 ∧ _x326 ≤ _x314 − 1 ∧ 0 ≤ _x314 − 1 ∧ _x325 ≤ _x317 − 1 ∧ −1 ≤ _x317 − 1 ∧ _x327 ≤ _x328 − 1 ∧ −1 ≤ _x328 − 1 ∧ _x312 − 2⋅_x329 = 1 ∧ _x319 ≤ _x312 ∧ −1 ≤ _x326 − 1 ∧ 0 ≤ _x325 − 1 ∧ _x322 ≤ _x326 ∧ 0 ≤ _x312 − 2⋅_x329 ∧ _x312 − 2⋅_x329 ≤ 1 ∧ _x312 − 2⋅_x319 ≤ 1 ∧ 0 ≤ _x312 − 2⋅_x319 ∧ _x314 = _x315 ∧ _x317 = _x318
  f1_0_main_Load	16	f196_0_create_LE:		x1 = _x330 ∧ x2 = _x331 ∧ x3 = _x332 ∧ x4 = _x333 ∧ x5 = _x334 ∧ x6 = _x335 ∧ x7 = _x336 ∧ x1 = _x337 ∧ x2 = _x338 ∧ x3 = _x339 ∧ x4 = _x340 ∧ x5 = _x341 ∧ x6 = _x342 ∧ x7 = _x343 ∧ −1 ≤ _x344 − 1 ∧ 1 ≤ _x331 − 1 ∧ −1 ≤ _x345 − 1 ∧ 0 ≤ _x330 − 1 ∧ _x345 − 1 = _x337
  f196_0_create_LE	17	f196_0_create_LE:		x1 = _x346 ∧ x2 = _x347 ∧ x3 = _x348 ∧ x4 = _x349 ∧ x5 = _x350 ∧ x6 = _x351 ∧ x7 = _x352 ∧ x1 = _x353 ∧ x2 = _x354 ∧ x3 = _x355 ∧ x4 = _x356 ∧ x5 = _x357 ∧ x6 = _x358 ∧ x7 = _x359 ∧ _x346 − 1 = _x353 ∧ 0 ≤ _x346 − 1
  __init	18	f1_0_main_Load:		x1 = _x360 ∧ x2 = _x361 ∧ x3 = _x362 ∧ x4 = _x363 ∧ x5 = _x364 ∧ x6 = _x365 ∧ x7 = _x366 ∧ x1 = _x367 ∧ x2 = _x368 ∧ x3 = _x369 ∧ x4 = _x370 ∧ x5 = _x371 ∧ x6 = _x372 ∧ x7 = _x373 ∧ 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 17 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 { f288_0_slide68_EQ, f288_0_slide68_EQ' }.

2.2.1 Transition Removal

We remove transitions 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 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)