This is the second part of the TLA+ series. For your convenience you can find other parts in the table of contents in Part 1 — TLA+ to ILP Part 1 — Reducing problem
Let’s now carry on with adding more invariants. Tutorial says to reorder the operations, so let’s first update the db and then send the message. Now we get the following output:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 |
Infeasibility row 'c4673': 0 = 1. Presolve time = 0.00 sec. (2.08 ticks) Root node processing (before b&c): Real time = 0.02 sec. (3.10 ticks) Parallel b&c, 8 threads: Real time = 0.00 sec. (0.00 ticks) Sync time (average) = 0.00 sec. Wait time (average) = 0.00 sec. ------------ Total (root+branch&cut) = 0.02 sec. (3.10 ticks) ILOG.CPLEX.CpxException: CPLEX Error 1217: No solution exists. at ILOG.CPLEX.CplexI.CALL(Int32 status) at ILOG.CPLEX.CplexI.GetXcache() at ILOG.CPLEX.Cplex.GetValue(INumExpr expr) at CplexMilpManager.Implementation.CplexMilpSolver.GetValue(IVariable variable) in C:\Users\afish\Desktop\milpmanager\CplexMilpSolver\Implementation\CplexMilpSolver.cs:line 160 at IlpPlayground.Program415798633.Start() at IlpPlayground.Env415798633.Start() |
Great, it took 0.02 second to show that the invariant holds. Let’s now do it for 3 messages and at most 3 processing attempts:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 |
Tried aggregator 4 times. MIP Presolve eliminated 54625 rows and 31499 columns. MIP Presolve modified 181700 coefficients. Aggregator did 45594 substitutions. Reduced MIP has 93725 rows, 47083 columns, and 249598 nonzeros. Reduced MIP has 46912 binaries, 171 generals, 0 SOSs, and 0 indicators. Presolve time = 1.23 sec. (600.55 ticks) Probing fixed 14146 vars, tightened 199 bounds. Probing changed sense of 57 constraints. Probing time = 17.13 sec. (1432.87 ticks) Cover probing fixed 0 vars, tightened 2535 bounds. Tried aggregator 3 times. MIP Presolve eliminated 70194 rows and 34054 columns. MIP Presolve modified 3224 coefficients. Aggregator did 2272 substitutions. Reduced MIP has 21259 rows, 10757 columns, and 63444 nonzeros. Reduced MIP has 10620 binaries, 137 generals, 0 SOSs, and 0 indicators. Presolve time = 0.59 sec. (231.37 ticks) Probing fixed 24 vars, tightened 0 bounds. Probing time = 0.22 sec. (45.46 ticks) Cover probing fixed 0 vars, tightened 1 bounds. Tried aggregator 2 times. MIP Presolve eliminated 155 rows and 76 columns. MIP Presolve modified 142 coefficients. Aggregator did 5 substitutions. Reduced MIP has 21099 rows, 10676 columns, and 62945 nonzeros. Reduced MIP has 10540 binaries, 136 generals, 0 SOSs, and 0 indicators. Presolve time = 0.23 sec. (95.63 ticks) Probing time = 0.08 sec. (13.65 ticks) Cover probing fixed 0 vars, tightened 1 bounds. Clique table members: 45984. Tightened 1 constraints. MIP emphasis: balance optimality and feasibility. MIP search method: dynamic search. Parallel mode: deterministic, using up to 8 threads. Root relaxation solution time = 1.11 sec. (961.52 ticks) Nodes Cuts/ Node Left Objective IInf Best Integer Best Bound ItCnt Gap 0 0 0.0000 5881 0.0000 1352 0 0 0.0000 3727 Cuts: 5374 6451 0 0 0.0000 4197 Cuts: 5035 11423 0 0 0.0000 4325 Cuts: 1023 13349 0 2 0.0000 4253 0.0000 13356 Elapsed time = 114.24 sec. (21523.30 ticks, tree = 0.01 MB, solutions = 0) 1 3 0.0000 2780 0.0000 16381 2 4 0.0000 2843 0.0000 17428 3 5 0.0000 3457 0.0000 18627 5 7 0.0000 2934 0.0000 21893 6 8 0.0000 2319 0.0000 23101 7 9 0.0000 3013 0.0000 25401 9 11 0.0000 2989 0.0000 28566 13 15 0.0000 2920 0.0000 31356 14 16 0.0000 2617 0.0000 37043 15 17 0.0000 2912 0.0000 46732 Elapsed time = 151.31 sec. (32512.06 ticks, tree = 0.62 MB, solutions = 0) 20 22 0.0000 3517 0.0000 81581 24 26 0.0000 2902 0.0000 88579 26 28 0.0000 3059 0.0000 93950 33 35 0.0000 3015 0.0000 103587 40 42 0.0000 3063 0.0000 114475 58 60 0.0000 2399 0.0000 125358 114 116 0.0000 3082 0.0000 152685 116 118 0.0000 3189 0.0000 161093 226 228 0.0000 3024 0.0000 240262 233 235 0.0000 3373 0.0000 254295 Elapsed time = 237.67 sec. (47212.18 ticks, tree = 2.07 MB, solutions = 0) 241 243 0.0000 3360 0.0000 270376 264 266 0.0000 3985 0.0000 296067 333 335 0.0000 4311 0.0000 330386 350 352 0.0000 3411 0.0000 338396 388 390 0.0000 4369 0.0000 352083 429 427 0.0000 3566 0.0000 364863 500 488 0.0000 3588 0.0000 388167 582 533 0.0000 2617 0.0000 420887 609 560 0.0000 3532 0.0000 445335 617 568 0.0000 3525 0.0000 452259 Elapsed time = 324.52 sec. (60798.93 ticks, tree = 52.37 MB, solutions = 0) 625 576 0.0000 3681 0.0000 459968 719 639 0.0000 3013 0.0000 502774 760 643 infeasible 0.0000 523214 767 640 infeasible 0.0000 537231 779 644 0.0000 2605 0.0000 554928 801 658 infeasible 0.0000 569934 808 661 infeasible 0.0000 579213 809 660 infeasible 0.0000 583339 835 676 infeasible 0.0000 628043 843 676 0.0000 3136 0.0000 638649 Elapsed time = 444.45 sec. (76815.67 ticks, tree = 85.60 MB, solutions = 0) 867 682 0.0000 3764 0.0000 669511 901 704 0.0000 3766 0.0000 709631 903 704 infeasible 0.0000 715957 915 710 0.0000 3162 0.0000 740255 917 708 infeasible 0.0000 749940 923 712 0.0000 3709 0.0000 761042 943 724 0.0000 3539 0.0000 783652 959 728 0.0000 3137 0.0000 798467 967 732 0.0000 3823 0.0000 804908 975 738 0.0000 4172 0.0000 815605 Elapsed time = 567.24 sec. (93862.15 ticks, tree = 93.52 MB, solutions = 0) 983 742 infeasible 0.0000 823977 999 746 0.0000 3371 0.0000 839661 1087 780 0.0000 2492 0.0000 902650 1119 797 0.0000 2777 0.0000 910464 1199 828 0.0000 4473 0.0000 925206 1247 837 0.0000 4138 0.0000 936822 1259 841 0.0000 1225 0.0000 940666 1315 850 0.0000 3219 0.0000 954899 1351 864 0.0000 4491 0.0000 966487 2173 937 infeasible 0.0000 1112720 Elapsed time = 673.52 sec. (108488.76 ticks, tree = 110.30 MB, solutions = 0) 2189 925 0.0000 1676 0.0000 1120865 2209 911 0.0000 579 0.0000 1136585 2245 885 0.0000 1784 0.0000 1160077 2253 885 0.0000 1849 0.0000 1168468 2261 883 0.0000 1390 0.0000 1173587 2297 859 0.0000 2847 0.0000 1202406 2318 862 0.0000 3319 0.0000 1230963 2338 868 0.0000 3796 0.0000 1247768 2354 884 0.0000 4336 0.0000 1255653 2370 898 0.0000 3772 0.0000 1263712 Elapsed time = 765.36 sec. (121444.90 ticks, tree = 90.82 MB, solutions = 0) 2458 937 0.0000 3417 0.0000 1291990 2465 938 0.0000 3515 0.0000 1292597 2497 947 0.0000 3714 0.0000 1301926 2529 961 0.0000 4121 0.0000 1310923 2728 998 0.0000 4528 0.0000 1359838 2947 1042 infeasible 0.0000 1421286 2955 1040 0.0000 2800 0.0000 1428789 2971 1040 infeasible 0.0000 1441818 2996 1055 0.0000 2774 0.0000 1461750 3011 1062 0.0000 663 0.0000 1471650 Elapsed time = 861.75 sec. (134254.97 ticks, tree = 121.30 MB, solutions = 0) 3032 1061 0.0000 4411 0.0000 1480281 3056 1063 0.0000 634 0.0000 1493358 3092 1077 0.0000 2755 0.0000 1508073 3143 1082 0.0000 2846 0.0000 1525295 3370 1085 0.0000 3626 0.0000 1603979 3386 1097 0.0000 3260 0.0000 1612883 3394 1103 0.0000 4976 0.0000 1617681 3402 1109 0.0000 4590 0.0000 1625703 3434 1127 0.0000 4192 0.0000 1642722 3458 1135 0.0000 3135 0.0000 1651700 Elapsed time = 955.80 sec. (147901.18 ticks, tree = 119.13 MB, solutions = 0) 3482 1145 0.0000 4132 0.0000 1666318 3490 1149 infeasible 0.0000 1671301 3522 1162 0.0000 3943 0.0000 1687495 3557 1157 0.0000 3739 0.0000 1698383 3878 1217 infeasible 0.0000 1793730 3879 1218 0.0000 4304 0.0000 1797563 3887 1214 0.0000 4112 0.0000 1810387 3895 1212 0.0000 3086 0.0000 1817630 3911 1214 infeasible 0.0000 1843753 3951 1230 infeasible 0.0000 1894774 Elapsed time = 1086.38 sec. (164678.85 ticks, tree = 138.75 MB, solutions = 0) 3984 1239 0.0000 3560 0.0000 1936581 4012 1243 0.0000 4185 0.0000 1978109 4036 1249 infeasible 0.0000 2008723 4084 1273 0.0000 2249 0.0000 2058914 4291 1339 0.0000 3954 0.0000 2160985 4451 1382 0.0000 1876 0.0000 2221480 4523 1399 0.0000 3779 0.0000 2243829 4643 1402 0.0000 3522 0.0000 2279823 5128 1475 infeasible 0.0000 2447189 5160 1457 0.0000 3772 0.0000 2483614 Elapsed time = 1361.44 sec. (209060.48 ticks, tree = 168.45 MB, solutions = 0) 5196 1459 0.0000 1136 0.0000 2517097 5227 1448 infeasible 0.0000 2548302 5275 1434 0.0000 4369 0.0000 2595818 5334 1457 0.0000 3442 0.0000 2654614 5374 1481 0.0000 4063 0.0000 2677172 5438 1504 0.0000 3184 0.0000 2715195 5630 1540 0.0000 2624 0.0000 2782860 5810 1580 0.0000 3521 0.0000 2877911 5976 1617 0.0000 4363 0.0000 2950026 6000 1635 0.0000 3808 0.0000 2981426 Elapsed time = 1643.06 sec. (254703.32 ticks, tree = 178.88 MB, solutions = 0) 6017 1646 0.0000 3429 0.0000 2998492 6041 1657 0.0000 3951 0.0000 3013795 6105 1681 0.0000 4355 0.0000 3044837 6472 1723 infeasible 0.0000 3284304 6501 1716 0.0000 3153 0.0000 3323608 6510 1723 0.0000 4787 0.0000 3346200 6533 1732 0.0000 4333 0.0000 3392812 6581 1762 0.0000 1784 0.0000 3452511 6627 1758 infeasible 0.0000 3508445 6655 1758 0.0000 4502 0.0000 3556108 Elapsed time = 1934.77 sec. (300419.53 ticks, tree = 185.01 MB, solutions = 0) 6673 1760 0.0000 3929 0.0000 3576293 6716 1777 0.0000 4649 0.0000 3622724 6738 1775 0.0000 4594 0.0000 3664192 6756 1777 0.0000 3895 0.0000 3707356 6780 1781 0.0000 4029 0.0000 3741195 6820 1779 infeasible 0.0000 3788602 6925 1802 0.0000 3864 0.0000 3921387 6986 1846 0.0000 5462 0.0000 3959989 7042 1862 0.0000 4057 0.0000 4000839 7122 1900 0.0000 3414 0.0000 4050704 Elapsed time = 2272.58 sec. (349766.51 ticks, tree = 196.05 MB, solutions = 0) 7178 1934 0.0000 3980 0.0000 4094289 7210 1950 0.0000 4365 0.0000 4118547 7367 2016 0.0000 4163 0.0000 4209261 7545 2086 0.0000 1570 -0.0000 4328399 7549 2089 0.0000 930 -0.0000 4335294 7564 2097 0.0000 2319 -0.0000 4368329 7594 2116 0.0000 1753 -0.0000 4428410 7603 2120 0.0000 1992 -0.0000 4499536 7639 2113 0.0000 2665 -0.0000 4567231 7760 1876 0.0000 3345 -0.0000 4650533 Elapsed time = 2584.36 sec. (418550.38 ticks, tree = 503.71 MB, solutions = 0) 7787 1778 infeasible -0.0000 4683492 7842 1626 0.0000 1482 -0.0000 4751846 7892 1516 0.0000 3149 -0.0000 4796067 7908 1479 0.0000 1445 -0.0000 4815710 7973 1275 0.0000 2715 -0.0000 4894447 8009 1199 0.0000 1522 -0.0000 4933489 8031 1145 0.0000 3088 -0.0000 4970651 8070 1081 0.0000 3651 -0.0000 5020954 8105 994 infeasible -0.0000 5064629 8121 957 infeasible -0.0000 5090673 Elapsed time = 2814.31 sec. (465587.14 ticks, tree = 218.87 MB, solutions = 0) 8150 917 0.0000 1817 -0.0000 5144677 8171 914 0.0000 2797 -0.0000 5173548 8203 863 infeasible -0.0000 5220060 8222 828 infeasible -0.0000 5252533 8255 774 0.0000 3762 -0.0000 5302317 8286 760 infeasible -0.0000 5336306 8315 722 0.0000 2793 -0.0000 5391932 8348 677 0.0000 3488 -0.0000 5441044 8377 647 0.0000 2029 -0.0000 5483059 8407 624 0.0000 2980 -0.0000 5519130 Elapsed time = 3060.86 sec. (512468.98 ticks, tree = 109.89 MB, solutions = 0) 8433 621 0.0000 3164 -0.0000 5562393 8456 594 infeasible -0.0000 5591068 8486 570 infeasible -0.0000 5637889 8513 555 0.0000 2542 -0.0000 5672283 8532 541 0.0000 2665 -0.0000 5700080 8564 509 0.0000 2708 -0.0000 5744187 8612 476 infeasible -0.0000 5812616 8629 460 infeasible -0.0000 5842067 8658 443 infeasible -0.0000 5897253 8674 431 infeasible -0.0000 5928058 Elapsed time = 3293.72 sec. (556670.87 ticks, tree = 50.01 MB, solutions = 0) 8690 417 0.0000 3761 -0.0000 5972047 8709 401 infeasible -0.0000 6025153 8726 385 0.0000 2293 -0.0000 6058443 8749 373 0.0000 2586 -0.0000 6084516 8795 341 0.0000 3357 -0.0000 6152100 8815 332 0.0000 3504 -0.0000 6181099 8839 314 infeasible -0.0000 6214294 8855 287 infeasible -0.0000 6239941 8888 275 0.0000 2871 -0.0000 6305306 8919 276 0.0000 2899 -0.0000 6345940 Elapsed time = 3544.33 sec. (603579.54 ticks, tree = 7.73 MB, solutions = 0) 8940 273 0.0000 3927 -0.0000 6382370 8963 270 0.0000 3880 -0.0000 6426954 8979 262 0.0000 3622 -0.0000 6457588 9002 259 infeasible -0.0000 6510739 9038 261 0.0000 3811 -0.0000 6575786 9054 267 0.0000 3360 -0.0000 6602310 9078 261 0.0000 3308 -0.0000 6640545 9100 257 0.0000 4100 -0.0000 6680438 9136 255 0.0000 4015 -0.0000 6733972 9160 253 0.0000 5122 -0.0000 6768716 Elapsed time = 3833.42 sec. (654232.38 ticks, tree = 7.51 MB, solutions = 0) 9196 241 infeasible -0.0000 6830570 9212 247 0.0000 3278 -0.0000 6868366 9237 252 infeasible -0.0000 6905455 9267 248 0.0000 3337 -0.0000 6949754 9285 244 infeasible -0.0000 6982328 9299 240 infeasible -0.0000 7007355 9339 246 0.0000 3457 -0.0000 7077818 9366 237 0.0000 3578 -0.0000 7131351 9379 240 0.0000 3621 -0.0000 7153049 9411 236 0.0000 3911 -0.0000 7197569 Elapsed time = 4127.74 sec. (697815.97 ticks, tree = 6.99 MB, solutions = 0) 9443 232 infeasible -0.0000 7255603 9459 222 infeasible -0.0000 7280744 9483 222 infeasible -0.0000 7320997 9507 222 infeasible -0.0000 7354601 9539 224 0.0000 3142 -0.0000 7395162 9575 232 0.0000 3356 -0.0000 7442675 9603 228 0.0000 3102 -0.0000 7484229 9633 224 0.0000 2556 -0.0000 7521632 9655 216 0.0000 3543 -0.0000 7558645 9681 204 0.0000 2819 -0.0000 7601679 Elapsed time = 4396.64 sec. (745122.95 ticks, tree = 6.22 MB, solutions = 0) 9709 200 0.0000 2874 -0.0000 7658008 9726 199 infeasible -0.0000 7683572 9743 192 0.0000 3106 -0.0000 7712638 9767 184 infeasible -0.0000 7748852 9799 180 infeasible -0.0000 7789378 9845 174 0.0000 3479 -0.0000 7857047 9868 169 infeasible -0.0000 7887777 9887 162 infeasible -0.0000 7914802 9908 155 0.0000 2762 -0.0000 7952261 9925 154 infeasible -0.0000 7978558 Elapsed time = 4668.92 sec. (789344.83 ticks, tree = 3.98 MB, solutions = 0) 9959 146 0.0000 3402 -0.0000 8022705 9999 136 0.0000 3421 -0.0000 8095320 10020 125 infeasible -0.0000 8132497 10036 115 infeasible -0.0000 8167324 10068 103 0.0000 4263 -0.0000 8215880 10092 97 infeasible -0.0000 8250282 10151 78 infeasible -0.0000 8327404 10167 78 infeasible -0.0000 8357192 10191 68 infeasible -0.0000 8387293 10215 52 infeasible -0.0000 8421111 Elapsed time = 4933.30 sec. (836114.41 ticks, tree = 0.30 MB, solutions = 0) 10240 41 infeasible -0.0000 8461178 10261 28 0.0000 3434 -0.0000 8492217 10285 24 0.0000 3244 -0.0000 8522078 10322 7 infeasible -0.0000 8557419 GUB cover cuts applied: 46 Clique cuts applied: 94 Cover cuts applied: 2012 Implied bound cuts applied: 2216 Flow cuts applied: 1 Mixed integer rounding cuts applied: 269 Zero-half cuts applied: 215 Gomory fractional cuts applied: 4 Root node processing (before b&c): Real time = 113.80 sec. (21386.31 ticks) Parallel b&c, 8 threads: Real time = 4895.06 sec. (834168.80 ticks) Sync time (average) = 312.55 sec. Wait time (average) = 0.01 sec. ------------ Total (root+branch&cut) = 5008.86 sec. (855555.11 ticks) ILOG.CPLEX.CpxException: CPLEX Error 1217: No solution exists. at ILOG.CPLEX.CplexI.CALL(Int32 status) at ILOG.CPLEX.CplexI.GetXcache() at ILOG.CPLEX.Cplex.GetValue(INumExpr expr) at CplexMilpManager.Implementation.CplexMilpSolver.GetValue(IVariable variable) in C:\Users\afish\Desktop\milpmanager\CplexMilpSolver\Implementation\CplexMilpSolver.cs:line 160 at IlpPlayground.Program1159526820.Start() at IlpPlayground.Env1159526820.Start() |
5000 seconds, that’s almost 85 minutes to prove that the invariant holds. The same takes around 2 seconds for TLA+.