From 6d5812941b859e50d22d6655486f612a6e6681b3 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Tue, 14 May 2024 01:45:31 +0200 Subject: [PATCH] dec-pomdp sketch experiments --- experiments/grid-meet-2fsc-df-p.log | 170 +++++ experiments/grid-meet-2fsc-df.log | 149 ++++ experiments/grid-meet-2fsc-nat.log | 152 ++++ experiments/grid-meet-3fsc-df.log | 496 +++++++++++++ experiments/grid-meet-3fsc-nat.log | 664 ++++++++++++++++++ .../sketch.props | 6 + .../sketch.templ | 152 ++++ .../sketch.props | 6 + .../sketch.templ | 176 +++++ 9 files changed, 1971 insertions(+) create mode 100644 experiments/grid-meet-2fsc-df-p.log create mode 100644 experiments/grid-meet-2fsc-df.log create mode 100644 experiments/grid-meet-2fsc-nat.log create mode 100644 experiments/grid-meet-3fsc-df.log create mode 100644 experiments/grid-meet-3fsc-nat.log create mode 100644 models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount-native/sketch.props create mode 100644 models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount-native/sketch.templ create mode 100644 models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount-native/sketch.props create mode 100644 models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount-native/sketch.templ diff --git a/experiments/grid-meet-2fsc-df-p.log b/experiments/grid-meet-2fsc-df-p.log new file mode 100644 index 000000000..afbd761d9 --- /dev/null +++ b/experiments/grid-meet-2fsc-df-p.log @@ -0,0 +1,170 @@ +2024-05-13 21:18:44,982 - cli.py - This is Paynt version 0.1.0. +2024-05-13 21:18:44,982 - sketch.py - loading sketch from models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount/sketch.templ ... +2024-05-13 21:18:44,982 - sketch.py - assuming sketch in PRISM format... +2024-05-13 21:18:44,986 - prism_parser.py - PRISM model type: DTMC +2024-05-13 21:18:44,986 - prism_parser.py - processing hole definitions... +2024-05-13 21:18:44,987 - prism_parser.py - loading properties from models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount/sketch.props ... +2024-05-13 21:18:44,988 - prism_parser.py - found the following specification: optimality: R[exp]{"moves"}max=? [F "goal"] +2024-05-13 21:18:44,988 - jani.py - constructing JANI program... +2024-05-13 21:18:44,994 - jani.py - constructing the quotient... +2024-05-13 21:18:47,959 - jani.py - associating choices of the quotient with hole assignments... +2024-05-13 21:18:48,946 - sketch.py - sketch parsing OK +2024-05-13 21:18:48,946 - sketch.py - converting state rewards 'moves' to state-action rewards +2024-05-13 21:18:48,989 - sketch.py - constructed explicit quotient having 18432 states and 599040 actions +2024-05-13 21:18:48,989 - sketch.py - found the following specification optimality: R[exp]{"moves"}max=? [F "goal"] +2024-05-13 21:18:49,548 - synthesizer.py - synthesis initiated, design space: 1e7 +> progress 1.037%, elapsed 3 s, estimated 289 s, iters = {MDP: 122}, opt = -99.026 +> progress 1.596%, elapsed 6 s, estimated 376 s, iters = {MDP: 399}, opt = -87.955 +> progress 1.685%, elapsed 9 s, estimated 535 s, iters = {MDP: 583}, opt = -12.438 +> progress 2.197%, elapsed 12 s, estimated 560 s, iters = {MDP: 680}, opt = -12.418 +> progress 2.359%, elapsed 15 s, estimated 649 s, iters = {MDP: 765}, opt = -12.402 +> progress 2.406%, elapsed 18 s, estimated 761 s, iters = {MDP: 905}, opt = -11.455 +> progress 2.49%, elapsed 21 s, estimated 856 s, iters = {MDP: 1062}, opt = -11.455 +> progress 2.685%, elapsed 24 s, estimated 906 s, iters = {MDP: 1238}, opt = -11.142 +> progress 5.322%, elapsed 27 s, estimated 515 s, iters = {MDP: 1310}, opt = -11.142 +> progress 5.468%, elapsed 30 s, estimated 558 s, iters = {MDP: 1358}, opt = -11.142 +> progress 5.53%, elapsed 33 s, estimated 607 s, iters = {MDP: 1502}, opt = -11.142 +> progress 5.599%, elapsed 36 s, estimated 655 s, iters = {MDP: 1561}, opt = -11.142 +> progress 5.691%, elapsed 39 s, estimated 698 s, iters = {MDP: 1603}, opt = -11.142 +> progress 5.765%, elapsed 42 s, estimated 741 s, iters = {MDP: 1675}, opt = -11.142 +> progress 6.689%, elapsed 45 s, estimated 683 s, iters = {MDP: 1733}, opt = -11.142 +> progress 6.732%, elapsed 48 s, estimated 725 s, iters = {MDP: 1742}, opt = -11.142 +> progress 6.909%, elapsed 51 s, estimated 751 s, iters = {MDP: 1760}, opt = -11.142 +> progress 6.982%, elapsed 55 s, estimated 793 s, iters = {MDP: 1770}, opt = -11.142 +> progress 7.0%, elapsed 58 s, estimated 839 s, iters = {MDP: 1779}, opt = -11.142 +> progress 7.031%, elapsed 62 s, estimated 883 s, iters = {MDP: 1794}, opt = -11.142 +> progress 7.226%, elapsed 66 s, estimated 923 s, iters = {MDP: 1802}, opt = -11.142 +> progress 7.275%, elapsed 69 s, estimated 959 s, iters = {MDP: 1804}, opt = -11.142 +> progress 7.276%, elapsed 72 s, estimated 1001 s, iters = {MDP: 1871}, opt = -11.142 +> progress 7.283%, elapsed 75 s, estimated 1042 s, iters = {MDP: 1974}, opt = -11.142 +> progress 7.291%, elapsed 79 s, estimated 1084 s, iters = {MDP: 1999}, opt = -11.142 +> progress 7.296%, elapsed 82 s, estimated 1130 s, iters = {MDP: 2016}, opt = -11.142 +> progress 8.007%, elapsed 85 s, estimated 1068 s, iters = {MDP: 2050}, opt = -11.142 +> progress 8.056%, elapsed 88 s, estimated 1103 s, iters = {MDP: 2056}, opt = -11.142 +> progress 8.691%, elapsed 91 s, estimated 1058 s, iters = {MDP: 2074}, opt = -11.142 +> progress 10.937%, elapsed 95 s, estimated 868 s, iters = {MDP: 2096}, opt = -11.142 +> progress 11.962%, elapsed 98 s, estimated 820 s, iters = {MDP: 2112}, opt = -11.142 +> progress 12.011%, elapsed 101 s, estimated 843 s, iters = {MDP: 2134}, opt = -11.142 +> progress 12.792%, elapsed 104 s, estimated 815 s, iters = {MDP: 2173}, opt = -11.142 +> progress 12.976%, elapsed 107 s, estimated 827 s, iters = {MDP: 2230}, opt = -11.142 +> progress 13.281%, elapsed 110 s, estimated 833 s, iters = {MDP: 2278}, opt = -11.142 +> progress 13.305%, elapsed 113 s, estimated 856 s, iters = {MDP: 2289}, opt = -11.142 +> progress 13.427%, elapsed 117 s, estimated 872 s, iters = {MDP: 2293}, opt = -11.142 +> progress 13.439%, elapsed 120 s, estimated 894 s, iters = {MDP: 2332}, opt = -11.142 +> progress 13.476%, elapsed 123 s, estimated 915 s, iters = {MDP: 2343}, opt = -11.142 +> progress 13.479%, elapsed 126 s, estimated 938 s, iters = {MDP: 2354}, opt = -11.142 +> progress 13.488%, elapsed 129 s, estimated 963 s, iters = {MDP: 2374}, opt = -11.142 +> progress 13.497%, elapsed 133 s, estimated 986 s, iters = {MDP: 2387}, opt = -11.142 +> progress 13.519%, elapsed 136 s, estimated 1007 s, iters = {MDP: 2397}, opt = -11.142 +> progress 13.543%, elapsed 139 s, estimated 1029 s, iters = {MDP: 2408}, opt = -11.142 +> progress 13.598%, elapsed 142 s, estimated 1048 s, iters = {MDP: 2413}, opt = -11.142 +> progress 13.671%, elapsed 147 s, estimated 1075 s, iters = {MDP: 2417}, opt = -11.142 +> progress 13.671%, elapsed 150 s, estimated 1102 s, iters = {MDP: 2420}, opt = -11.142 +> progress 13.696%, elapsed 154 s, estimated 1127 s, iters = {MDP: 2490}, opt = -11.142 +> progress 13.714%, elapsed 157 s, estimated 1147 s, iters = {MDP: 2505}, opt = -11.142 +> progress 13.769%, elapsed 160 s, estimated 1167 s, iters = {MDP: 2538}, opt = -11.142 +> progress 13.867%, elapsed 163 s, estimated 1181 s, iters = {MDP: 2554}, opt = -11.142 +> progress 13.867%, elapsed 167 s, estimated 1209 s, iters = {MDP: 2557}, opt = -11.142 +> progress 13.876%, elapsed 170 s, estimated 1230 s, iters = {MDP: 2599}, opt = -11.142 +> progress 13.893%, elapsed 173 s, estimated 1250 s, iters = {MDP: 2620}, opt = -11.142 +> progress 13.916%, elapsed 177 s, estimated 1274 s, iters = {MDP: 2653}, opt = -11.142 +> progress 13.926%, elapsed 180 s, estimated 1297 s, iters = {MDP: 2688}, opt = -11.142 +> progress 13.945%, elapsed 183 s, estimated 1317 s, iters = {MDP: 2721}, opt = -11.142 +> progress 13.964%, elapsed 186 s, estimated 1338 s, iters = {MDP: 2741}, opt = -11.142 +> progress 14.206%, elapsed 190 s, estimated 1337 s, iters = {MDP: 2790}, opt = -11.142 +> progress 14.704%, elapsed 193 s, estimated 1313 s, iters = {MDP: 2846}, opt = -11.142 +> progress 14.965%, elapsed 196 s, estimated 1311 s, iters = {MDP: 2914}, opt = -11.142 +> progress 14.971%, elapsed 199 s, estimated 1331 s, iters = {MDP: 3015}, opt = -11.142 +> progress 15.478%, elapsed 202 s, estimated 1307 s, iters = {MDP: 3097}, opt = -11.142 +> progress 15.625%, elapsed 205 s, estimated 1317 s, iters = {MDP: 3174}, opt = -11.142 +> progress 15.637%, elapsed 208 s, estimated 1335 s, iters = {MDP: 3212}, opt = -11.142 +> progress 15.673%, elapsed 211 s, estimated 1352 s, iters = {MDP: 3246}, opt = -11.142 +> progress 16.21%, elapsed 215 s, estimated 1326 s, iters = {MDP: 3281}, opt = -11.142 +> progress 16.406%, elapsed 218 s, estimated 1331 s, iters = {MDP: 3299}, opt = -11.142 +> progress 16.412%, elapsed 221 s, estimated 1350 s, iters = {MDP: 3351}, opt = -11.142 +> progress 16.423%, elapsed 224 s, estimated 1368 s, iters = {MDP: 3405}, opt = -11.142 +> progress 16.43%, elapsed 227 s, estimated 1386 s, iters = {MDP: 3503}, opt = -11.142 +> progress 16.503%, elapsed 230 s, estimated 1398 s, iters = {MDP: 3548}, opt = -11.142 +> progress 16.525%, elapsed 233 s, estimated 1414 s, iters = {MDP: 3609}, opt = -11.142 +> progress 16.552%, elapsed 237 s, estimated 1432 s, iters = {MDP: 3649}, opt = -11.142 +> progress 16.589%, elapsed 240 s, estimated 1447 s, iters = {MDP: 3666}, opt = -11.142 +> progress 16.603%, elapsed 243 s, estimated 1464 s, iters = {MDP: 3694}, opt = -11.142 +> progress 16.656%, elapsed 246 s, estimated 1479 s, iters = {MDP: 3743}, opt = -11.142 +> progress 16.729%, elapsed 249 s, estimated 1492 s, iters = {MDP: 3759}, opt = -11.142 +> progress 16.774%, elapsed 252 s, estimated 1506 s, iters = {MDP: 3785}, opt = -11.142 +> progress 16.807%, elapsed 255 s, estimated 1521 s, iters = {MDP: 3845}, opt = -11.142 +> progress 16.87%, elapsed 258 s, estimated 1534 s, iters = {MDP: 3883}, opt = -11.142 +> progress 17.578%, elapsed 261 s, estimated 1489 s, iters = {MDP: 3906}, opt = -11.142 +> progress 17.626%, elapsed 265 s, estimated 1503 s, iters = {MDP: 3955}, opt = -11.142 +> progress 17.742%, elapsed 268 s, estimated 1511 s, iters = {MDP: 3973}, opt = -11.142 +> progress 17.788%, elapsed 271 s, estimated 1524 s, iters = {MDP: 3989}, opt = -11.142 +> progress 17.846%, elapsed 274 s, estimated 1536 s, iters = {MDP: 3999}, opt = -11.142 +> progress 19.143%, elapsed 277 s, estimated 1448 s, iters = {MDP: 4031}, opt = -10.265 +> progress 19.287%, elapsed 280 s, estimated 1453 s, iters = {MDP: 4114}, opt = -8.545 +> progress 19.531%, elapsed 283 s, estimated 1452 s, iters = {MDP: 4121}, opt = -8.545 +> progress 19.555%, elapsed 287 s, estimated 1468 s, iters = {MDP: 4159}, opt = -8.545 +> progress 19.677%, elapsed 290 s, estimated 1476 s, iters = {MDP: 4163}, opt = -8.545 +> progress 19.678%, elapsed 293 s, estimated 1492 s, iters = {MDP: 4182}, opt = -8.545 +> progress 19.689%, elapsed 296 s, estimated 1507 s, iters = {MDP: 4212}, opt = -8.545 +> progress 19.726%, elapsed 300 s, estimated 1521 s, iters = {MDP: 4218}, opt = -8.545 +> progress 19.73%, elapsed 303 s, estimated 1538 s, iters = {MDP: 4238}, opt = -8.545 +> progress 19.738%, elapsed 307 s, estimated 1555 s, iters = {MDP: 4277}, opt = -8.545 +> progress 19.921%, elapsed 310 s, estimated 1556 s, iters = {MDP: 4288}, opt = -8.545 +> progress 19.921%, elapsed 313 s, estimated 1572 s, iters = {MDP: 4290}, opt = -8.545 +> progress 19.946%, elapsed 316 s, estimated 1587 s, iters = {MDP: 4296}, opt = -8.545 +> progress 19.949%, elapsed 319 s, estimated 1603 s, iters = {MDP: 4393}, opt = -8.545 +> progress 19.958%, elapsed 323 s, estimated 1618 s, iters = {MDP: 4438}, opt = -8.545 +> progress 19.97%, elapsed 326 s, estimated 1635 s, iters = {MDP: 4471}, opt = -8.545 +> progress 19.979%, elapsed 329 s, estimated 1650 s, iters = {MDP: 4482}, opt = -8.545 +> progress 20.019%, elapsed 333 s, estimated 1663 s, iters = {MDP: 4488}, opt = -8.545 +> progress 20.03%, elapsed 336 s, estimated 1679 s, iters = {MDP: 4509}, opt = -8.545 +> progress 20.068%, elapsed 340 s, estimated 1694 s, iters = {MDP: 4515}, opt = -8.545 +> progress 20.117%, elapsed 344 s, estimated 1712 s, iters = {MDP: 4539}, opt = -8.545 +> progress 20.141%, elapsed 347 s, estimated 1726 s, iters = {MDP: 4548}, opt = -8.545 +> progress 21.875%, elapsed 351 s, estimated 1604 s, iters = {MDP: 4558}, opt = -8.545 +> progress 22.753%, elapsed 354 s, estimated 1557 s, iters = {MDP: 4564}, opt = -8.545 +> progress 22.875%, elapsed 357 s, estimated 1563 s, iters = {MDP: 4579}, opt = -8.545 +> progress 25.0%, elapsed 360 s, estimated 1442 s, iters = {MDP: 4606}, opt = -8.545 +> progress 37.5%, elapsed 363 s, estimated 970 s, iters = {MDP: 4619}, opt = -8.545 +> progress 43.832%, elapsed 366 s, estimated 837 s, iters = {MDP: 4690}, opt = -8.545 +> progress 50.0%, elapsed 370 s, estimated 740 s, iters = {MDP: 4773}, opt = -8.545 +> progress 59.472%, elapsed 374 s, estimated 629 s, iters = {MDP: 4782}, opt = -8.545 +> progress 59.521%, elapsed 377 s, estimated 634 s, iters = {MDP: 4786}, opt = -8.545 +> progress 59.533%, elapsed 381 s, estimated 640 s, iters = {MDP: 4807}, opt = -8.545 +> progress 59.545%, elapsed 384 s, estimated 645 s, iters = {MDP: 4817}, opt = -8.545 +> progress 59.546%, elapsed 387 s, estimated 650 s, iters = {MDP: 4824}, opt = -8.545 +> progress 60.156%, elapsed 390 s, estimated 649 s, iters = {MDP: 4835}, opt = -8.545 +> progress 94.531%, elapsed 393 s, estimated 416 s, iters = {MDP: 4845}, opt = -8.545 +> progress 94.531%, elapsed 397 s, estimated 420 s, iters = {MDP: 4852}, opt = -8.545 +> progress 94.543%, elapsed 400 s, estimated 423 s, iters = {MDP: 4872}, opt = -8.545 +> progress 94.554%, elapsed 403 s, estimated 427 s, iters = {MDP: 4901}, opt = -8.545 +> progress 94.592%, elapsed 407 s, estimated 430 s, iters = {MDP: 4906}, opt = -8.545 +> progress 94.597%, elapsed 410 s, estimated 433 s, iters = {MDP: 4916}, opt = -8.545 +> progress 94.604%, elapsed 413 s, estimated 437 s, iters = {MDP: 4929}, opt = -8.545 +> progress 94.612%, elapsed 416 s, estimated 440 s, iters = {MDP: 4948}, opt = -8.545 +> progress 94.622%, elapsed 420 s, estimated 444 s, iters = {MDP: 4963}, opt = -8.545 +> progress 94.731%, elapsed 423 s, estimated 447 s, iters = {MDP: 4982}, opt = -8.545 +> progress 94.754%, elapsed 426 s, estimated 450 s, iters = {MDP: 5003}, opt = -8.545 +> progress 94.836%, elapsed 429 s, estimated 453 s, iters = {MDP: 5017}, opt = -8.545 +> progress 94.921%, elapsed 433 s, estimated 456 s, iters = {MDP: 5027}, opt = -8.545 +> progress 94.921%, elapsed 437 s, estimated 460 s, iters = {MDP: 5030}, opt = -8.545 +> progress 94.946%, elapsed 440 s, estimated 463 s, iters = {MDP: 5068}, opt = -8.545 +> progress 94.95%, elapsed 443 s, estimated 466 s, iters = {MDP: 5083}, opt = -8.545 +> progress 94.958%, elapsed 446 s, estimated 470 s, iters = {MDP: 5094}, opt = -8.545 +> progress 94.967%, elapsed 450 s, estimated 473 s, iters = {MDP: 5107}, opt = -8.545 +> progress 94.976%, elapsed 453 s, estimated 477 s, iters = {MDP: 5121}, opt = -8.545 +> progress 95.117%, elapsed 456 s, estimated 480 s, iters = {MDP: 5127}, opt = -8.545 +2024-05-13 21:26:28,282 - synthesizer.py - synthesis finished, printing synthesized assignment below: +2024-05-13 21:26:28,282 - synthesizer.py - M1_0_1=1, M1_0_0=0, M1_1_1=1, M1_1_0=1, P1_0_1=2, P1_0_0=3, P1_1_1=2, P1_1_0=1, M2_0_1=1, M2_0_0=0, M2_1_1=1, M2_1_0=1, P2_0_1=4, P2_0_0=1, P2_1_1=4, P2_1_0=4 +2024-05-13 21:26:28,290 - synthesizer.py - double-checking specification satisfiability: : -8.544769337492935 +-------------------- +Synthesis summary: +optimality objective: R[exp]{"moves"}max=? [F "goal"] + +method: AR, synthesis time: 458.73 s +number of holes: 16, family size: 1e7, quotient: 18432 states / 599040 actions +explored: 100 % +MDP stats: avg MDP size: 3937, iterations: 5140 + +optimum: -8.544769 +-------------------- diff --git a/experiments/grid-meet-2fsc-df.log b/experiments/grid-meet-2fsc-df.log new file mode 100644 index 000000000..73e06014f --- /dev/null +++ b/experiments/grid-meet-2fsc-df.log @@ -0,0 +1,149 @@ +2024-05-13 20:55:08,753 - cli.py - This is Paynt version 0.1.0. +2024-05-13 20:55:08,753 - sketch.py - loading sketch from models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount/sketch.templ ... +2024-05-13 20:55:08,753 - sketch.py - assuming sketch in PRISM format... +2024-05-13 20:55:08,757 - prism_parser.py - PRISM model type: DTMC +2024-05-13 20:55:08,757 - prism_parser.py - processing hole definitions... +2024-05-13 20:55:08,757 - prism_parser.py - loading properties from models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount/sketch.props ... +2024-05-13 20:55:08,758 - prism_parser.py - found the following specification: optimality: R[exp]{"moves"}max=? [F "goal"] +2024-05-13 20:55:08,758 - jani.py - constructing JANI program... +2024-05-13 20:55:08,763 - jani.py - constructing the quotient... +2024-05-13 20:55:11,601 - jani.py - associating choices of the quotient with hole assignments... +2024-05-13 20:55:12,545 - sketch.py - sketch parsing OK +2024-05-13 20:55:12,545 - sketch.py - converting state rewards 'moves' to state-action rewards +2024-05-13 20:55:12,593 - sketch.py - constructed explicit quotient having 18432 states and 599040 actions +2024-05-13 20:55:12,593 - sketch.py - found the following specification optimality: R[exp]{"moves"}max=? [F "goal"] +2024-05-13 20:55:13,105 - synthesizer.py - synthesis initiated, design space: 1e7 +> progress 1.031%, elapsed 3 s, estimated 291 s, iters = {MDP: 121}, opt = -98.187 +> progress 1.595%, elapsed 6 s, estimated 376 s, iters = {MDP: 396}, opt = -87.496 +> progress 1.685%, elapsed 9 s, estimated 535 s, iters = {MDP: 599}, opt = -12.438 +> progress 2.197%, elapsed 12 s, estimated 547 s, iters = {MDP: 682}, opt = -12.417 +> progress 2.404%, elapsed 15 s, estimated 626 s, iters = {MDP: 794}, opt = -11.455 +> progress 2.416%, elapsed 18 s, estimated 749 s, iters = {MDP: 914}, opt = -11.455 +> progress 2.6%, elapsed 21 s, estimated 812 s, iters = {MDP: 1085}, opt = -11.141 +> progress 5.224%, elapsed 24 s, estimated 462 s, iters = {MDP: 1205}, opt = -11.141 +> progress 5.371%, elapsed 27 s, estimated 507 s, iters = {MDP: 1259}, opt = -11.141 +> progress 5.53%, elapsed 30 s, estimated 548 s, iters = {MDP: 1407}, opt = -11.141 +> progress 5.688%, elapsed 33 s, estimated 586 s, iters = {MDP: 1471}, opt = -11.141 +> progress 5.693%, elapsed 36 s, estimated 639 s, iters = {MDP: 1546}, opt = -11.141 +> progress 6.25%, elapsed 39 s, estimated 631 s, iters = {MDP: 1627}, opt = -11.141 +> progress 6.73%, elapsed 42 s, estimated 631 s, iters = {MDP: 1644}, opt = -11.141 +> progress 6.909%, elapsed 45 s, estimated 663 s, iters = {MDP: 1664}, opt = -11.141 +> progress 6.982%, elapsed 48 s, estimated 699 s, iters = {MDP: 1675}, opt = -11.141 +> progress 7.0%, elapsed 51 s, estimated 741 s, iters = {MDP: 1687}, opt = -11.141 +> progress 7.128%, elapsed 55 s, estimated 777 s, iters = {MDP: 1702}, opt = -11.141 +> progress 7.275%, elapsed 59 s, estimated 811 s, iters = {MDP: 1707}, opt = -11.141 +> progress 7.276%, elapsed 62 s, estimated 853 s, iters = {MDP: 1797}, opt = -11.141 +> progress 7.287%, elapsed 65 s, estimated 894 s, iters = {MDP: 1895}, opt = -11.141 +> progress 7.292%, elapsed 68 s, estimated 936 s, iters = {MDP: 1913}, opt = -11.141 +> progress 7.812%, elapsed 71 s, estimated 912 s, iters = {MDP: 1950}, opt = -11.141 +> progress 8.081%, elapsed 74 s, estimated 922 s, iters = {MDP: 1958}, opt = -11.141 +> progress 8.593%, elapsed 77 s, estimated 902 s, iters = {MDP: 1971}, opt = -11.141 +> progress 10.937%, elapsed 80 s, estimated 739 s, iters = {MDP: 1996}, opt = -11.141 +> progress 11.962%, elapsed 83 s, estimated 701 s, iters = {MDP: 2013}, opt = -11.141 +> progress 12.109%, elapsed 86 s, estimated 718 s, iters = {MDP: 2037}, opt = -11.141 +> progress 12.799%, elapsed 89 s, estimated 702 s, iters = {MDP: 2080}, opt = -11.141 +> progress 13.085%, elapsed 92 s, estimated 710 s, iters = {MDP: 2163}, opt = -11.141 +> progress 13.284%, elapsed 96 s, estimated 722 s, iters = {MDP: 2182}, opt = -11.141 +> progress 13.427%, elapsed 99 s, estimated 739 s, iters = {MDP: 2193}, opt = -11.141 +> progress 13.438%, elapsed 102 s, estimated 761 s, iters = {MDP: 2228}, opt = -11.141 +> progress 13.476%, elapsed 105 s, estimated 783 s, iters = {MDP: 2245}, opt = -11.141 +> progress 13.482%, elapsed 108 s, estimated 805 s, iters = {MDP: 2270}, opt = -11.141 +> progress 13.494%, elapsed 111 s, estimated 828 s, iters = {MDP: 2286}, opt = -11.141 +> progress 13.525%, elapsed 115 s, estimated 850 s, iters = {MDP: 2300}, opt = -11.141 +> progress 13.574%, elapsed 118 s, estimated 871 s, iters = {MDP: 2312}, opt = -11.141 +> progress 13.671%, elapsed 122 s, estimated 896 s, iters = {MDP: 2318}, opt = -11.141 +> progress 13.671%, elapsed 125 s, estimated 918 s, iters = {MDP: 2322}, opt = -11.141 +> progress 13.702%, elapsed 128 s, estimated 938 s, iters = {MDP: 2392}, opt = -11.141 +> progress 13.719%, elapsed 131 s, estimated 959 s, iters = {MDP: 2425}, opt = -11.141 +> progress 13.83%, elapsed 134 s, estimated 975 s, iters = {MDP: 2452}, opt = -11.141 +> progress 13.867%, elapsed 138 s, estimated 999 s, iters = {MDP: 2458}, opt = -11.141 +> progress 13.877%, elapsed 141 s, estimated 1020 s, iters = {MDP: 2503}, opt = -11.141 +> progress 13.897%, elapsed 144 s, estimated 1040 s, iters = {MDP: 2542}, opt = -11.141 +> progress 13.919%, elapsed 147 s, estimated 1060 s, iters = {MDP: 2570}, opt = -11.141 +> progress 13.94%, elapsed 151 s, estimated 1083 s, iters = {MDP: 2599}, opt = -11.141 +> progress 13.964%, elapsed 154 s, estimated 1105 s, iters = {MDP: 2642}, opt = -11.141 +> progress 14.257%, elapsed 157 s, estimated 1103 s, iters = {MDP: 2709}, opt = -11.141 +> progress 14.716%, elapsed 160 s, estimated 1089 s, iters = {MDP: 2771}, opt = -11.141 +> progress 14.969%, elapsed 163 s, estimated 1091 s, iters = {MDP: 2868}, opt = -11.141 +> progress 15.234%, elapsed 166 s, estimated 1092 s, iters = {MDP: 2969}, opt = -11.141 +> progress 15.496%, elapsed 169 s, estimated 1093 s, iters = {MDP: 3065}, opt = -11.141 +> progress 15.628%, elapsed 172 s, estimated 1103 s, iters = {MDP: 3105}, opt = -11.141 +> progress 15.661%, elapsed 175 s, estimated 1120 s, iters = {MDP: 3148}, opt = -11.141 +> progress 15.722%, elapsed 178 s, estimated 1135 s, iters = {MDP: 3191}, opt = -11.141 +> progress 16.241%, elapsed 181 s, estimated 1118 s, iters = {MDP: 3210}, opt = -11.141 +> progress 16.411%, elapsed 184 s, estimated 1125 s, iters = {MDP: 3252}, opt = -11.141 +> progress 16.424%, elapsed 187 s, estimated 1142 s, iters = {MDP: 3321}, opt = -11.141 +> progress 16.455%, elapsed 190 s, estimated 1159 s, iters = {MDP: 3430}, opt = -11.141 +> progress 16.522%, elapsed 193 s, estimated 1173 s, iters = {MDP: 3483}, opt = -11.141 +> progress 16.552%, elapsed 197 s, estimated 1190 s, iters = {MDP: 3561}, opt = -11.141 +> progress 16.589%, elapsed 200 s, estimated 1207 s, iters = {MDP: 3578}, opt = -11.141 +> progress 16.603%, elapsed 203 s, estimated 1224 s, iters = {MDP: 3612}, opt = -11.141 +> progress 16.674%, elapsed 206 s, estimated 1238 s, iters = {MDP: 3662}, opt = -11.141 +> progress 16.772%, elapsed 209 s, estimated 1249 s, iters = {MDP: 3684}, opt = -11.141 +> progress 16.798%, elapsed 212 s, estimated 1265 s, iters = {MDP: 3726}, opt = -11.141 +> progress 16.857%, elapsed 215 s, estimated 1279 s, iters = {MDP: 3788}, opt = -11.141 +> progress 17.59%, elapsed 218 s, estimated 1243 s, iters = {MDP: 3809}, opt = -11.141 +> progress 17.634%, elapsed 221 s, estimated 1257 s, iters = {MDP: 3848}, opt = -11.141 +> progress 17.678%, elapsed 224 s, estimated 1271 s, iters = {MDP: 3875}, opt = -11.141 +> progress 17.797%, elapsed 227 s, estimated 1279 s, iters = {MDP: 3891}, opt = -11.141 +> progress 18.75%, elapsed 230 s, estimated 1231 s, iters = {MDP: 3909}, opt = -11.141 +> progress 19.213%, elapsed 233 s, estimated 1217 s, iters = {MDP: 4008}, opt = -8.545 +> progress 19.531%, elapsed 237 s, estimated 1214 s, iters = {MDP: 4024}, opt = -8.545 +> progress 19.58%, elapsed 240 s, estimated 1227 s, iters = {MDP: 4063}, opt = -8.545 +> progress 19.677%, elapsed 243 s, estimated 1237 s, iters = {MDP: 4069}, opt = -8.545 +> progress 19.683%, elapsed 246 s, estimated 1253 s, iters = {MDP: 4114}, opt = -8.545 +> progress 19.726%, elapsed 249 s, estimated 1265 s, iters = {MDP: 4120}, opt = -8.545 +> progress 19.731%, elapsed 252 s, estimated 1281 s, iters = {MDP: 4142}, opt = -8.545 +> progress 19.744%, elapsed 256 s, estimated 1296 s, iters = {MDP: 4186}, opt = -8.545 +> progress 19.921%, elapsed 259 s, estimated 1301 s, iters = {MDP: 4192}, opt = -8.545 +> progress 19.946%, elapsed 262 s, estimated 1314 s, iters = {MDP: 4197}, opt = -8.545 +> progress 19.949%, elapsed 265 s, estimated 1329 s, iters = {MDP: 4294}, opt = -8.545 +> progress 19.959%, elapsed 268 s, estimated 1343 s, iters = {MDP: 4349}, opt = -8.545 +> progress 19.97%, elapsed 271 s, estimated 1359 s, iters = {MDP: 4375}, opt = -8.545 +> progress 20.019%, elapsed 275 s, estimated 1374 s, iters = {MDP: 4390}, opt = -8.545 +> progress 20.03%, elapsed 278 s, estimated 1389 s, iters = {MDP: 4412}, opt = -8.545 +> progress 20.069%, elapsed 281 s, estimated 1402 s, iters = {MDP: 4422}, opt = -8.545 +> progress 20.117%, elapsed 284 s, estimated 1415 s, iters = {MDP: 4442}, opt = -8.545 +> progress 20.153%, elapsed 288 s, estimated 1429 s, iters = {MDP: 4453}, opt = -8.545 +> progress 22.656%, elapsed 291 s, estimated 1286 s, iters = {MDP: 4464}, opt = -8.545 +> progress 22.851%, elapsed 294 s, estimated 1288 s, iters = {MDP: 4471}, opt = -8.545 +> progress 25.0%, elapsed 297 s, estimated 1190 s, iters = {MDP: 4508}, opt = -8.545 +> progress 28.125%, elapsed 300 s, estimated 1069 s, iters = {MDP: 4520}, opt = -8.545 +> progress 43.798%, elapsed 303 s, estimated 693 s, iters = {MDP: 4552}, opt = -8.545 +> progress 46.093%, elapsed 306 s, estimated 665 s, iters = {MDP: 4677}, opt = -8.545 +> progress 59.375%, elapsed 309 s, estimated 521 s, iters = {MDP: 4686}, opt = -8.545 +> progress 59.521%, elapsed 312 s, estimated 525 s, iters = {MDP: 4691}, opt = -8.545 +> progress 59.526%, elapsed 316 s, estimated 530 s, iters = {MDP: 4711}, opt = -8.545 +> progress 59.543%, elapsed 319 s, estimated 535 s, iters = {MDP: 4722}, opt = -8.545 +> progress 59.548%, elapsed 322 s, estimated 541 s, iters = {MDP: 4735}, opt = -8.545 +> progress 75.0%, elapsed 325 s, estimated 434 s, iters = {MDP: 4746}, opt = -8.545 +> progress 94.531%, elapsed 328 s, estimated 347 s, iters = {MDP: 4756}, opt = -8.545 +> progress 94.54%, elapsed 332 s, estimated 351 s, iters = {MDP: 4777}, opt = -8.545 +> progress 94.552%, elapsed 335 s, estimated 354 s, iters = {MDP: 4807}, opt = -8.545 +> progress 94.592%, elapsed 338 s, estimated 357 s, iters = {MDP: 4814}, opt = -8.545 +> progress 94.598%, elapsed 341 s, estimated 361 s, iters = {MDP: 4826}, opt = -8.545 +> progress 94.61%, elapsed 344 s, estimated 364 s, iters = {MDP: 4847}, opt = -8.545 +> progress 94.618%, elapsed 347 s, estimated 367 s, iters = {MDP: 4867}, opt = -8.545 +> progress 94.726%, elapsed 350 s, estimated 370 s, iters = {MDP: 4885}, opt = -8.545 +> progress 94.757%, elapsed 353 s, estimated 373 s, iters = {MDP: 4912}, opt = -8.545 +> progress 94.873%, elapsed 356 s, estimated 376 s, iters = {MDP: 4926}, opt = -8.545 +> progress 94.921%, elapsed 360 s, estimated 379 s, iters = {MDP: 4935}, opt = -8.545 +> progress 94.928%, elapsed 363 s, estimated 382 s, iters = {MDP: 4969}, opt = -8.545 +> progress 94.949%, elapsed 366 s, estimated 386 s, iters = {MDP: 4989}, opt = -8.545 +> progress 94.958%, elapsed 369 s, estimated 389 s, iters = {MDP: 5001}, opt = -8.545 +> progress 94.97%, elapsed 372 s, estimated 392 s, iters = {MDP: 5016}, opt = -8.545 +> progress 94.995%, elapsed 376 s, estimated 395 s, iters = {MDP: 5031}, opt = -8.545 +2024-05-13 21:01:32,382 - synthesizer.py - synthesis finished, printing synthesized assignment below: +2024-05-13 21:01:32,382 - synthesizer.py - M1_0_1=1, M1_0_0=0, M1_1_1=1, M1_1_0=1, P1_0_1=2, P1_0_0=3, P1_1_1=2, P1_1_0=1, M2_0_1=1, M2_0_0=0, M2_1_1=1, M2_1_0=1, P2_0_1=4, P2_0_0=1, P2_1_1=4, P2_1_0=4 +2024-05-13 21:01:32,389 - synthesizer.py - double-checking specification satisfiability: : -8.54476716312559 +-------------------- +Synthesis summary: +optimality objective: R[exp]{"moves"}max=? [F "goal"] + +method: AR, synthesis time: 379.28 s +number of holes: 16, family size: 1e7, quotient: 18432 states / 599040 actions +explored: 100 % +MDP stats: avg MDP size: 4000, iterations: 5047 + +optimum: -8.544767 +-------------------- diff --git a/experiments/grid-meet-2fsc-nat.log b/experiments/grid-meet-2fsc-nat.log new file mode 100644 index 000000000..0b28fd518 --- /dev/null +++ b/experiments/grid-meet-2fsc-nat.log @@ -0,0 +1,152 @@ +2024-05-13 21:17:25,837 - cli.py - This is Paynt version 0.1.0. +2024-05-13 21:17:25,837 - sketch.py - loading sketch from models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount-native/sketch.templ ... +2024-05-13 21:17:25,837 - sketch.py - assuming sketch in PRISM format... +2024-05-13 21:17:25,841 - prism_parser.py - PRISM model type: DTMC +2024-05-13 21:17:25,842 - prism_parser.py - processing hole definitions... +2024-05-13 21:17:25,842 - prism_parser.py - loading properties from models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount-native/sketch.props ... +2024-05-13 21:17:25,843 - prism_parser.py - found the following specification: optimality: R[exp]{"moves"}max=? [C{99/100}] +2024-05-13 21:17:25,843 - jani.py - constructing JANI program... +2024-05-13 21:17:25,848 - jani.py - constructing the quotient... +2024-05-13 21:17:27,258 - jani.py - associating choices of the quotient with hole assignments... +2024-05-13 21:17:28,125 - sketch.py - sketch parsing OK +2024-05-13 21:17:28,125 - sketch.py - converting state rewards 'moves' to state-action rewards +2024-05-13 21:17:28,162 - sketch.py - constructed explicit quotient having 9216 states and 577728 actions +2024-05-13 21:17:28,162 - sketch.py - found the following specification optimality: R[exp]{"moves"}max=? [C{99/100}] +2024-05-13 21:17:28,617 - synthesizer.py - synthesis initiated, design space: 1e7 +> progress 1.57%, elapsed 3 s, estimated 191 s, iters = {MDP: 197}, opt = -89.991 +> progress 1.641%, elapsed 6 s, estimated 366 s, iters = {MDP: 522}, opt = -86.919 +> progress 1.727%, elapsed 9 s, estimated 526 s, iters = {MDP: 617}, opt = -11.553 +> progress 2.087%, elapsed 12 s, estimated 579 s, iters = {MDP: 675}, opt = -11.533 +> progress 2.417%, elapsed 15 s, estimated 625 s, iters = {MDP: 785}, opt = -10.561 +> progress 2.455%, elapsed 18 s, estimated 737 s, iters = {MDP: 952}, opt = -10.561 +> progress 2.558%, elapsed 21 s, estimated 825 s, iters = {MDP: 1081}, opt = -10.244 +> progress 5.175%, elapsed 24 s, estimated 470 s, iters = {MDP: 1153}, opt = -10.244 +> progress 5.273%, elapsed 27 s, estimated 521 s, iters = {MDP: 1191}, opt = -10.244 +> progress 5.542%, elapsed 30 s, estimated 551 s, iters = {MDP: 1334}, opt = -10.244 +> progress 5.59%, elapsed 33 s, estimated 601 s, iters = {MDP: 1425}, opt = -10.244 +> progress 5.764%, elapsed 36 s, estimated 636 s, iters = {MDP: 1472}, opt = -10.244 +> progress 5.798%, elapsed 39 s, estimated 685 s, iters = {MDP: 1518}, opt = -10.244 +> progress 7.91%, elapsed 43 s, estimated 551 s, iters = {MDP: 1528}, opt = -10.244 +> progress 8.154%, elapsed 47 s, estimated 581 s, iters = {MDP: 1533}, opt = -10.244 +> progress 8.203%, elapsed 51 s, estimated 628 s, iters = {MDP: 1536}, opt = -10.244 +> progress 8.251%, elapsed 55 s, estimated 670 s, iters = {MDP: 1538}, opt = -10.244 +> progress 8.252%, elapsed 58 s, estimated 706 s, iters = {MDP: 1552}, opt = -10.244 +> progress 8.258%, elapsed 61 s, estimated 742 s, iters = {MDP: 1657}, opt = -10.244 +> progress 8.267%, elapsed 64 s, estimated 784 s, iters = {MDP: 1695}, opt = -10.244 +> progress 8.269%, elapsed 68 s, estimated 824 s, iters = {MDP: 1709}, opt = -10.244 +> progress 8.398%, elapsed 73 s, estimated 870 s, iters = {MDP: 1739}, opt = -10.244 +> progress 8.886%, elapsed 77 s, estimated 867 s, iters = {MDP: 1747}, opt = -10.244 +> progress 10.156%, elapsed 82 s, estimated 808 s, iters = {MDP: 1754}, opt = -10.244 +> progress 10.205%, elapsed 86 s, estimated 843 s, iters = {MDP: 1761}, opt = -10.244 +> progress 10.223%, elapsed 89 s, estimated 872 s, iters = {MDP: 1769}, opt = -10.244 +> progress 10.253%, elapsed 92 s, estimated 901 s, iters = {MDP: 1772}, opt = -10.244 +> progress 10.351%, elapsed 96 s, estimated 930 s, iters = {MDP: 1779}, opt = -10.244 +> progress 10.4%, elapsed 99 s, estimated 958 s, iters = {MDP: 1786}, opt = -10.244 +> progress 10.449%, elapsed 102 s, estimated 985 s, iters = {MDP: 1795}, opt = -10.244 +> progress 10.449%, elapsed 106 s, estimated 1019 s, iters = {MDP: 1798}, opt = -10.244 +> progress 10.485%, elapsed 109 s, estimated 1048 s, iters = {MDP: 1808}, opt = -10.244 +> progress 10.486%, elapsed 113 s, estimated 1077 s, iters = {MDP: 1814}, opt = -10.244 +> progress 10.522%, elapsed 117 s, estimated 1113 s, iters = {MDP: 1825}, opt = -10.244 +> progress 10.523%, elapsed 120 s, estimated 1143 s, iters = {MDP: 1829}, opt = -10.244 +> progress 10.535%, elapsed 123 s, estimated 1171 s, iters = {MDP: 1838}, opt = -10.244 +> progress 11.328%, elapsed 127 s, estimated 1124 s, iters = {MDP: 1856}, opt = -10.244 +> progress 11.45%, elapsed 130 s, estimated 1140 s, iters = {MDP: 1866}, opt = -10.244 +> progress 11.621%, elapsed 133 s, estimated 1150 s, iters = {MDP: 1880}, opt = -10.244 +> progress 11.718%, elapsed 136 s, estimated 1166 s, iters = {MDP: 1888}, opt = -10.244 +> progress 12.5%, elapsed 139 s, estimated 1118 s, iters = {MDP: 1913}, opt = -10.244 +> progress 12.951%, elapsed 142 s, estimated 1103 s, iters = {MDP: 1991}, opt = -7.621 +> progress 13.281%, elapsed 145 s, estimated 1099 s, iters = {MDP: 2019}, opt = -7.621 +> progress 13.281%, elapsed 149 s, estimated 1125 s, iters = {MDP: 2023}, opt = -7.621 +> progress 13.305%, elapsed 153 s, estimated 1150 s, iters = {MDP: 2058}, opt = -7.621 +> progress 13.427%, elapsed 157 s, estimated 1170 s, iters = {MDP: 2062}, opt = -7.621 +> progress 13.427%, elapsed 160 s, estimated 1193 s, iters = {MDP: 2067}, opt = -7.621 +> progress 13.432%, elapsed 163 s, estimated 1215 s, iters = {MDP: 2101}, opt = -7.621 +> progress 13.452%, elapsed 166 s, estimated 1238 s, iters = {MDP: 2111}, opt = -7.621 +> progress 13.476%, elapsed 169 s, estimated 1259 s, iters = {MDP: 2116}, opt = -7.621 +> progress 13.479%, elapsed 172 s, estimated 1281 s, iters = {MDP: 2134}, opt = -7.621 +> progress 13.482%, elapsed 175 s, estimated 1303 s, iters = {MDP: 2140}, opt = -7.621 +> progress 13.5%, elapsed 179 s, estimated 1332 s, iters = {MDP: 2179}, opt = -7.621 +> progress 13.671%, elapsed 183 s, estimated 1340 s, iters = {MDP: 2184}, opt = -7.621 +> progress 13.671%, elapsed 186 s, estimated 1364 s, iters = {MDP: 2186}, opt = -7.621 +> progress 13.696%, elapsed 189 s, estimated 1384 s, iters = {MDP: 2193}, opt = -7.621 +> progress 13.698%, elapsed 192 s, estimated 1407 s, iters = {MDP: 2251}, opt = -7.621 +> progress 13.7%, elapsed 195 s, estimated 1430 s, iters = {MDP: 2300}, opt = -7.621 +> progress 13.708%, elapsed 199 s, estimated 1452 s, iters = {MDP: 2337}, opt = -7.621 +> progress 13.72%, elapsed 202 s, estimated 1475 s, iters = {MDP: 2370}, opt = -7.621 +> progress 13.726%, elapsed 205 s, estimated 1498 s, iters = {MDP: 2373}, opt = -7.621 +> progress 13.729%, elapsed 208 s, estimated 1521 s, iters = {MDP: 2383}, opt = -7.621 +> progress 13.745%, elapsed 212 s, estimated 1542 s, iters = {MDP: 2389}, opt = -7.621 +> progress 13.775%, elapsed 215 s, estimated 1564 s, iters = {MDP: 2393}, opt = -7.621 +> progress 13.778%, elapsed 218 s, estimated 1587 s, iters = {MDP: 2407}, opt = -7.621 +> progress 13.793%, elapsed 221 s, estimated 1609 s, iters = {MDP: 2413}, opt = -7.621 +> progress 13.824%, elapsed 225 s, estimated 1630 s, iters = {MDP: 2417}, opt = -7.621 +> progress 13.827%, elapsed 228 s, estimated 1652 s, iters = {MDP: 2431}, opt = -7.621 +> progress 13.842%, elapsed 231 s, estimated 1674 s, iters = {MDP: 2437}, opt = -7.621 +> progress 13.867%, elapsed 235 s, estimated 1697 s, iters = {MDP: 2440}, opt = -7.621 +> progress 13.894%, elapsed 238 s, estimated 1717 s, iters = {MDP: 2444}, opt = -7.621 +> progress 13.906%, elapsed 241 s, estimated 1738 s, iters = {MDP: 2453}, opt = -7.621 +> progress 15.625%, elapsed 244 s, estimated 1567 s, iters = {MDP: 2460}, opt = -7.621 +> progress 16.503%, elapsed 249 s, estimated 1510 s, iters = {MDP: 2468}, opt = -7.621 +> progress 16.606%, elapsed 252 s, estimated 1519 s, iters = {MDP: 2478}, opt = -7.621 +> progress 16.796%, elapsed 255 s, estimated 1520 s, iters = {MDP: 2506}, opt = -7.621 +> progress 20.336%, elapsed 258 s, estimated 1271 s, iters = {MDP: 2518}, opt = -7.621 +> progress 20.41%, elapsed 262 s, estimated 1287 s, iters = {MDP: 2532}, opt = -7.621 +> progress 20.458%, elapsed 266 s, estimated 1302 s, iters = {MDP: 2534}, opt = -7.621 +> progress 20.458%, elapsed 269 s, estimated 1319 s, iters = {MDP: 2537}, opt = -7.621 +> progress 20.465%, elapsed 273 s, estimated 1335 s, iters = {MDP: 2552}, opt = -7.621 +> progress 20.507%, elapsed 277 s, estimated 1352 s, iters = {MDP: 2558}, opt = -7.621 +> progress 20.727%, elapsed 280 s, estimated 1352 s, iters = {MDP: 2568}, opt = -7.621 +> progress 20.922%, elapsed 283 s, estimated 1354 s, iters = {MDP: 2579}, opt = -7.621 +> progress 25.0%, elapsed 286 s, estimated 1146 s, iters = {MDP: 2586}, opt = -7.621 +> progress 37.5%, elapsed 289 s, estimated 772 s, iters = {MDP: 2602}, opt = -7.621 +> progress 37.55%, elapsed 292 s, estimated 779 s, iters = {MDP: 2641}, opt = -7.621 +> progress 37.554%, elapsed 296 s, estimated 788 s, iters = {MDP: 2654}, opt = -7.621 +> progress 37.89%, elapsed 299 s, estimated 789 s, iters = {MDP: 2733}, opt = -7.621 +> progress 62.695%, elapsed 303 s, estimated 484 s, iters = {MDP: 2747}, opt = -7.621 +> progress 62.744%, elapsed 307 s, estimated 490 s, iters = {MDP: 2750}, opt = -7.621 +> progress 62.744%, elapsed 310 s, estimated 495 s, iters = {MDP: 2755}, opt = -7.621 +> progress 62.756%, elapsed 314 s, estimated 500 s, iters = {MDP: 2772}, opt = -7.621 +> progress 62.765%, elapsed 317 s, estimated 505 s, iters = {MDP: 2779}, opt = -7.621 +> progress 62.768%, elapsed 321 s, estimated 511 s, iters = {MDP: 2784}, opt = -7.621 +> progress 62.771%, elapsed 324 s, estimated 516 s, iters = {MDP: 2803}, opt = -7.621 +> progress 62.89%, elapsed 327 s, estimated 521 s, iters = {MDP: 2807}, opt = -7.621 +> progress 81.25%, elapsed 330 s, estimated 407 s, iters = {MDP: 2817}, opt = -7.621 +> progress 81.5%, elapsed 334 s, estimated 409 s, iters = {MDP: 2853}, opt = -7.621 +> progress 81.857%, elapsed 337 s, estimated 411 s, iters = {MDP: 2913}, opt = -7.621 +> progress 82.861%, elapsed 341 s, estimated 411 s, iters = {MDP: 2957}, opt = -7.621 +> progress 82.885%, elapsed 344 s, estimated 415 s, iters = {MDP: 2961}, opt = -7.621 +> progress 82.893%, elapsed 347 s, estimated 419 s, iters = {MDP: 2978}, opt = -7.621 +> progress 83.203%, elapsed 350 s, estimated 421 s, iters = {MDP: 2985}, opt = -7.621 +> progress 83.251%, elapsed 353 s, estimated 424 s, iters = {MDP: 3007}, opt = -7.621 +> progress 83.306%, elapsed 356 s, estimated 428 s, iters = {MDP: 3025}, opt = -7.621 +> progress 83.593%, elapsed 359 s, estimated 430 s, iters = {MDP: 3050}, opt = -7.621 +> progress 83.715%, elapsed 363 s, estimated 433 s, iters = {MDP: 3071}, opt = -7.621 +> progress 83.715%, elapsed 366 s, estimated 437 s, iters = {MDP: 3076}, opt = -7.621 +> progress 83.728%, elapsed 369 s, estimated 441 s, iters = {MDP: 3086}, opt = -7.621 +> progress 83.729%, elapsed 372 s, estimated 445 s, iters = {MDP: 3098}, opt = -7.621 +> progress 83.813%, elapsed 376 s, estimated 448 s, iters = {MDP: 3107}, opt = -7.621 +> progress 83.825%, elapsed 379 s, estimated 452 s, iters = {MDP: 3120}, opt = -7.621 +> progress 83.903%, elapsed 382 s, estimated 455 s, iters = {MDP: 3135}, opt = -7.621 +> progress 93.945%, elapsed 385 s, estimated 410 s, iters = {MDP: 3151}, opt = -7.621 +> progress 93.969%, elapsed 388 s, estimated 413 s, iters = {MDP: 3174}, opt = -7.621 +> progress 94.042%, elapsed 392 s, estimated 416 s, iters = {MDP: 3190}, opt = -7.621 +> progress 94.049%, elapsed 395 s, estimated 420 s, iters = {MDP: 3202}, opt = -7.621 +> progress 94.091%, elapsed 398 s, estimated 423 s, iters = {MDP: 3207}, opt = -7.621 +> progress 94.573%, elapsed 401 s, estimated 424 s, iters = {MDP: 3218}, opt = -7.621 +> progress 94.677%, elapsed 404 s, estimated 427 s, iters = {MDP: 3236}, opt = -7.621 +> progress 95.019%, elapsed 407 s, estimated 429 s, iters = {MDP: 3255}, opt = -7.621 +> progress 95.117%, elapsed 410 s, estimated 431 s, iters = {MDP: 3273}, opt = -7.621 +2024-05-13 21:24:19,964 - synthesizer.py - synthesis finished, printing synthesized assignment below: +2024-05-13 21:24:19,964 - synthesizer.py - M1_0_1=1, M1_0_0=0, M1_1_1=1, M1_1_0=1, P1_0_1=2, P1_0_0=3, P1_1_1=2, P1_1_0=1, M2_0_1=1, M2_0_0=0, M2_1_1=1, M2_1_0=1, P2_0_1=4, P2_0_0=1, P2_1_1=4, P2_1_0=4 +2024-05-13 21:24:19,971 - synthesizer.py - double-checking specification satisfiability: : -7.620974109662922 +-------------------- +Synthesis summary: +optimality objective: R[exp]{"moves"}max=? [C{99/100}] + +method: AR, synthesis time: 411.35 s +number of holes: 16, family size: 1e7, quotient: 9216 states / 577728 actions +explored: 100 % +MDP stats: avg MDP size: 2036, iterations: 3276 + +optimum: -7.620974 +-------------------- diff --git a/experiments/grid-meet-3fsc-df.log b/experiments/grid-meet-3fsc-df.log new file mode 100644 index 000000000..15b73e538 --- /dev/null +++ b/experiments/grid-meet-3fsc-df.log @@ -0,0 +1,496 @@ +2024-05-13 21:49:13,793 - cli.py - This is Paynt version 0.1.0. +2024-05-13 21:49:13,793 - sketch.py - loading sketch from models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount/sketch.templ ... +2024-05-13 21:49:13,793 - sketch.py - assuming sketch in PRISM format... +2024-05-13 21:49:13,798 - prism_parser.py - PRISM model type: DTMC +2024-05-13 21:49:13,798 - prism_parser.py - processing hole definitions... +2024-05-13 21:49:13,799 - prism_parser.py - loading properties from models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount/sketch.props ... +2024-05-13 21:49:13,800 - prism_parser.py - found the following specification: optimality: R[exp]{"moves"}max=? [F "goal"] +2024-05-13 21:49:13,800 - jani.py - constructing JANI program... +2024-05-13 21:49:13,808 - jani.py - constructing the quotient... +2024-05-13 21:49:28,977 - jani.py - associating choices of the quotient with hole assignments... +2024-05-13 21:49:33,583 - sketch.py - sketch parsing OK +2024-05-13 21:49:33,583 - sketch.py - converting state rewards 'moves' to state-action rewards +2024-05-13 21:49:33,764 - sketch.py - constructed explicit quotient having 41472 states and 3006720 actions +2024-05-13 21:49:33,764 - sketch.py - found the following specification optimality: R[exp]{"moves"}max=? [F "goal"] +2024-05-13 21:49:36,919 - synthesizer.py - optimality threshold set to -8.545 +2024-05-13 21:49:36,920 - synthesizer.py - synthesis initiated, design space: 1e12 +> progress 0.0%, elapsed 3 s, estimated 3512957 s (40 days), iters = {MDP: 2}, opt = -8.545 +> progress 0.0%, elapsed 8 s, estimated 8216833 s (95 days), iters = {MDP: 4}, opt = -8.545 +> progress 4.166%, elapsed 11 s, estimated 278 s, iters = {MDP: 6}, opt = -8.545 +> progress 4.166%, elapsed 15 s, estimated 375 s, iters = {MDP: 8}, opt = -8.545 +> progress 4.166%, elapsed 19 s, estimated 459 s, iters = {MDP: 11}, opt = -8.545 +> progress 4.167%, elapsed 22 s, estimated 533 s, iters = {MDP: 19}, opt = -8.545 +> progress 4.168%, elapsed 26 s, estimated 626 s, iters = {MDP: 31}, opt = -8.545 +> progress 4.168%, elapsed 30 s, estimated 727 s, iters = {MDP: 40}, opt = -8.545 +> progress 4.169%, elapsed 33 s, estimated 805 s, iters = {MDP: 52}, opt = -8.545 +> progress 4.171%, elapsed 36 s, estimated 879 s, iters = {MDP: 62}, opt = -8.545 +> progress 4.173%, elapsed 41 s, estimated 985 s, iters = {MDP: 67}, opt = -8.545 +> progress 4.174%, elapsed 44 s, estimated 1059 s, iters = {MDP: 69}, opt = -8.545 +> progress 4.174%, elapsed 48 s, estimated 1154 s, iters = {MDP: 72}, opt = -8.545 +> progress 4.174%, elapsed 52 s, estimated 1246 s, iters = {MDP: 75}, opt = -8.545 +> progress 4.174%, elapsed 55 s, estimated 1330 s, iters = {MDP: 81}, opt = -8.545 +> progress 4.174%, elapsed 59 s, estimated 1413 s, iters = {MDP: 83}, opt = -8.545 +> progress 4.174%, elapsed 62 s, estimated 1503 s, iters = {MDP: 85}, opt = -8.545 +> progress 4.174%, elapsed 66 s, estimated 1588 s, iters = {MDP: 91}, opt = -8.545 +> progress 4.174%, elapsed 70 s, estimated 1696 s, iters = {MDP: 98}, opt = -8.545 +> progress 4.175%, elapsed 74 s, estimated 1788 s, iters = {MDP: 105}, opt = -8.545 +> progress 4.175%, elapsed 77 s, estimated 1863 s, iters = {MDP: 109}, opt = -8.545 +> progress 4.175%, elapsed 82 s, estimated 1971 s, iters = {MDP: 114}, opt = -8.545 +> progress 4.175%, elapsed 86 s, estimated 2059 s, iters = {MDP: 116}, opt = -8.545 +> progress 4.175%, elapsed 89 s, estimated 2140 s, iters = {MDP: 122}, opt = -8.545 +> progress 4.175%, elapsed 93 s, estimated 2239 s, iters = {MDP: 129}, opt = -8.545 +> progress 4.175%, elapsed 97 s, estimated 2324 s, iters = {MDP: 136}, opt = -8.545 +> progress 4.175%, elapsed 100 s, estimated 2399 s, iters = {MDP: 141}, opt = -8.545 +> progress 4.175%, elapsed 104 s, estimated 2492 s, iters = {MDP: 145}, opt = -8.545 +> progress 4.175%, elapsed 107 s, estimated 2577 s, iters = {MDP: 147}, opt = -8.545 +> progress 4.175%, elapsed 111 s, estimated 2662 s, iters = {MDP: 149}, opt = -8.545 +> progress 4.175%, elapsed 114 s, estimated 2735 s, iters = {MDP: 156}, opt = -8.545 +> progress 4.175%, elapsed 117 s, estimated 2822 s, iters = {MDP: 162}, opt = -8.545 +> progress 4.175%, elapsed 120 s, estimated 2896 s, iters = {MDP: 169}, opt = -8.545 +> progress 4.175%, elapsed 124 s, estimated 2979 s, iters = {MDP: 176}, opt = -8.545 +> progress 4.175%, elapsed 128 s, estimated 3079 s, iters = {MDP: 179}, opt = -8.545 +> progress 4.175%, elapsed 132 s, estimated 3171 s, iters = {MDP: 182}, opt = -8.545 +> progress 4.175%, elapsed 136 s, estimated 3259 s, iters = {MDP: 185}, opt = -8.545 +> progress 4.175%, elapsed 139 s, estimated 3333 s, iters = {MDP: 195}, opt = -8.545 +> progress 4.175%, elapsed 142 s, estimated 3407 s, iters = {MDP: 200}, opt = -8.545 +> progress 4.175%, elapsed 145 s, estimated 3492 s, iters = {MDP: 207}, opt = -8.545 +> progress 4.175%, elapsed 150 s, estimated 3595 s, iters = {MDP: 215}, opt = -8.545 +> progress 4.175%, elapsed 153 s, estimated 3679 s, iters = {MDP: 218}, opt = -8.545 +> progress 4.175%, elapsed 157 s, estimated 3769 s, iters = {MDP: 222}, opt = -8.545 +> progress 4.175%, elapsed 161 s, estimated 3861 s, iters = {MDP: 228}, opt = -8.545 +> progress 4.175%, elapsed 164 s, estimated 3945 s, iters = {MDP: 230}, opt = -8.545 +> progress 4.175%, elapsed 168 s, estimated 4033 s, iters = {MDP: 233}, opt = -8.545 +> progress 4.175%, elapsed 171 s, estimated 4105 s, iters = {MDP: 243}, opt = -8.545 +> progress 4.175%, elapsed 174 s, estimated 4178 s, iters = {MDP: 249}, opt = -8.545 +> progress 4.175%, elapsed 178 s, estimated 4264 s, iters = {MDP: 255}, opt = -8.545 +> progress 4.175%, elapsed 181 s, estimated 4337 s, iters = {MDP: 262}, opt = -8.545 +> progress 4.175%, elapsed 185 s, estimated 4431 s, iters = {MDP: 265}, opt = -8.545 +> progress 4.175%, elapsed 188 s, estimated 4510 s, iters = {MDP: 269}, opt = -8.545 +> progress 4.175%, elapsed 191 s, estimated 4586 s, iters = {MDP: 274}, opt = -8.545 +> progress 4.175%, elapsed 195 s, estimated 4687 s, iters = {MDP: 277}, opt = -8.545 +> progress 4.175%, elapsed 199 s, estimated 4783 s, iters = {MDP: 280}, opt = -8.545 +> progress 4.175%, elapsed 203 s, estimated 4876 s, iters = {MDP: 283}, opt = -8.545 +> progress 4.175%, elapsed 206 s, estimated 4953 s, iters = {MDP: 288}, opt = -8.545 +> progress 4.175%, elapsed 210 s, estimated 5030 s, iters = {MDP: 290}, opt = -8.545 +> progress 4.175%, elapsed 214 s, estimated 5125 s, iters = {MDP: 292}, opt = -8.545 +> progress 4.175%, elapsed 217 s, estimated 5209 s, iters = {MDP: 295}, opt = -8.545 +> progress 4.176%, elapsed 221 s, estimated 5303 s, iters = {MDP: 298}, opt = -8.545 +> progress 4.176%, elapsed 224 s, estimated 5378 s, iters = {MDP: 304}, opt = -8.545 +> progress 4.176%, elapsed 227 s, estimated 5457 s, iters = {MDP: 306}, opt = -8.545 +> progress 4.176%, elapsed 231 s, estimated 5551 s, iters = {MDP: 308}, opt = -8.545 +> progress 4.176%, elapsed 235 s, estimated 5639 s, iters = {MDP: 311}, opt = -8.545 +> progress 4.176%, elapsed 239 s, estimated 5734 s, iters = {MDP: 314}, opt = -8.545 +> progress 4.177%, elapsed 242 s, estimated 5815 s, iters = {MDP: 320}, opt = -8.545 +> progress 4.177%, elapsed 247 s, estimated 5915 s, iters = {MDP: 322}, opt = -8.545 +> progress 4.178%, elapsed 251 s, estimated 6018 s, iters = {MDP: 324}, opt = -8.545 +> progress 4.178%, elapsed 254 s, estimated 6097 s, iters = {MDP: 326}, opt = -8.545 +> progress 4.178%, elapsed 257 s, estimated 6170 s, iters = {MDP: 345}, opt = -8.545 +> progress 4.178%, elapsed 260 s, estimated 6246 s, iters = {MDP: 367}, opt = -8.545 +> progress 4.178%, elapsed 265 s, estimated 6356 s, iters = {MDP: 370}, opt = -8.545 +> progress 4.178%, elapsed 269 s, estimated 6445 s, iters = {MDP: 373}, opt = -8.545 +> progress 4.178%, elapsed 272 s, estimated 6525 s, iters = {MDP: 380}, opt = -8.545 +> progress 4.178%, elapsed 275 s, estimated 6603 s, iters = {MDP: 384}, opt = -8.545 +> progress 4.178%, elapsed 279 s, estimated 6691 s, iters = {MDP: 387}, opt = -8.545 +> progress 4.178%, elapsed 283 s, estimated 6781 s, iters = {MDP: 393}, opt = -8.545 +> progress 4.178%, elapsed 287 s, estimated 6882 s, iters = {MDP: 397}, opt = -8.545 +> progress 4.178%, elapsed 292 s, estimated 6994 s, iters = {MDP: 399}, opt = -8.545 +> progress 4.178%, elapsed 295 s, estimated 7067 s, iters = {MDP: 402}, opt = -8.545 +> progress 4.178%, elapsed 299 s, estimated 7161 s, iters = {MDP: 407}, opt = -8.545 +> progress 4.178%, elapsed 302 s, estimated 7240 s (2 hours), iters = {MDP: 409}, opt = -8.545 +> progress 4.178%, elapsed 305 s, estimated 7317 s (2 hours), iters = {MDP: 415}, opt = -8.545 +> progress 4.178%, elapsed 309 s, estimated 7415 s (2 hours), iters = {MDP: 418}, opt = -8.545 +> progress 4.178%, elapsed 312 s, estimated 7488 s (2 hours), iters = {MDP: 423}, opt = -8.545 +> progress 4.178%, elapsed 316 s, estimated 7586 s (2 hours), iters = {MDP: 427}, opt = -8.545 +> progress 4.178%, elapsed 320 s, estimated 7664 s (2 hours), iters = {MDP: 429}, opt = -8.545 +> progress 4.178%, elapsed 323 s, estimated 7736 s (2 hours), iters = {MDP: 434}, opt = -8.545 +> progress 4.178%, elapsed 327 s, estimated 7833 s (2 hours), iters = {MDP: 438}, opt = -8.545 +> progress 4.178%, elapsed 330 s, estimated 7912 s (2 hours), iters = {MDP: 444}, opt = -8.545 +> progress 4.178%, elapsed 334 s, estimated 8005 s (2 hours), iters = {MDP: 447}, opt = -8.545 +> progress 4.178%, elapsed 337 s, estimated 8083 s (2 hours), iters = {MDP: 449}, opt = -8.545 +> progress 4.178%, elapsed 340 s, estimated 8159 s (2 hours), iters = {MDP: 455}, opt = -8.545 +> progress 4.178%, elapsed 344 s, estimated 8251 s (2 hours), iters = {MDP: 458}, opt = -8.545 +> progress 4.178%, elapsed 348 s, estimated 8329 s (2 hours), iters = {MDP: 464}, opt = -8.545 +> progress 4.178%, elapsed 351 s, estimated 8423 s (2 hours), iters = {MDP: 467}, opt = -8.545 +> progress 4.178%, elapsed 357 s, estimated 8554 s (2 hours), iters = {MDP: 469}, opt = -8.545 +> progress 4.178%, elapsed 360 s, estimated 8633 s (2 hours), iters = {MDP: 471}, opt = -8.545 +> progress 4.178%, elapsed 363 s, estimated 8706 s (2 hours), iters = {MDP: 481}, opt = -8.545 +> progress 4.178%, elapsed 366 s, estimated 8781 s (2 hours), iters = {MDP: 491}, opt = -8.545 +> progress 4.178%, elapsed 370 s, estimated 8855 s (2 hours), iters = {MDP: 495}, opt = -8.545 +> progress 4.178%, elapsed 373 s, estimated 8940 s (2 hours), iters = {MDP: 509}, opt = -8.545 +> progress 4.178%, elapsed 376 s, estimated 9019 s (2 hours), iters = {MDP: 517}, opt = -8.545 +> progress 4.178%, elapsed 380 s, estimated 9094 s (2 hours), iters = {MDP: 530}, opt = -8.545 +> progress 4.178%, elapsed 383 s, estimated 9169 s (2 hours), iters = {MDP: 536}, opt = -8.545 +> progress 4.178%, elapsed 386 s, estimated 9243 s (2 hours), iters = {MDP: 542}, opt = -8.545 +> progress 4.178%, elapsed 390 s, estimated 9334 s (2 hours), iters = {MDP: 546}, opt = -8.545 +> progress 4.178%, elapsed 393 s, estimated 9424 s (2 hours), iters = {MDP: 552}, opt = -8.545 +> progress 4.178%, elapsed 397 s, estimated 9510 s (2 hours), iters = {MDP: 555}, opt = -8.545 +> progress 4.178%, elapsed 400 s, estimated 9589 s (2 hours), iters = {MDP: 557}, opt = -8.545 +> progress 4.178%, elapsed 404 s, estimated 9680 s (2 hours), iters = {MDP: 567}, opt = -8.545 +> progress 4.178%, elapsed 407 s, estimated 9758 s (2 hours), iters = {MDP: 572}, opt = -8.545 +> progress 4.178%, elapsed 411 s, estimated 9841 s (2 hours), iters = {MDP: 580}, opt = -8.545 +> progress 4.178%, elapsed 414 s, estimated 9923 s (2 hours), iters = {MDP: 590}, opt = -8.545 +> progress 4.178%, elapsed 418 s, estimated 10007 s (2 hours), iters = {MDP: 594}, opt = -8.545 +> progress 4.178%, elapsed 421 s, estimated 10086 s (2 hours), iters = {MDP: 603}, opt = -8.545 +> progress 4.178%, elapsed 425 s, estimated 10188 s (2 hours), iters = {MDP: 605}, opt = -8.545 +> progress 4.178%, elapsed 428 s, estimated 10261 s (2 hours), iters = {MDP: 610}, opt = -8.545 +> progress 4.178%, elapsed 431 s, estimated 10333 s (2 hours), iters = {MDP: 617}, opt = -8.545 +> progress 4.178%, elapsed 435 s, estimated 10433 s (2 hours), iters = {MDP: 623}, opt = -8.545 +> progress 4.178%, elapsed 439 s, estimated 10515 s (2 hours), iters = {MDP: 633}, opt = -8.545 +> progress 4.178%, elapsed 442 s, estimated 10592 s (2 hours), iters = {MDP: 643}, opt = -8.545 +> progress 4.178%, elapsed 446 s, estimated 10682 s (2 hours), iters = {MDP: 646}, opt = -8.545 +> progress 4.178%, elapsed 450 s, estimated 10776 s (2 hours), iters = {MDP: 649}, opt = -8.545 +> progress 4.178%, elapsed 453 s, estimated 10848 s (3 hours), iters = {MDP: 651}, opt = -8.545 +> progress 4.178%, elapsed 456 s, estimated 10930 s (3 hours), iters = {MDP: 659}, opt = -8.545 +> progress 4.178%, elapsed 461 s, estimated 11038 s (3 hours), iters = {MDP: 663}, opt = -8.545 +> progress 4.178%, elapsed 464 s, estimated 11113 s (3 hours), iters = {MDP: 668}, opt = -8.545 +> progress 4.178%, elapsed 468 s, estimated 11220 s (3 hours), iters = {MDP: 675}, opt = -8.545 +> progress 4.178%, elapsed 471 s, estimated 11292 s (3 hours), iters = {MDP: 680}, opt = -8.545 +> progress 4.178%, elapsed 475 s, estimated 11367 s (3 hours), iters = {MDP: 690}, opt = -8.545 +> progress 4.178%, elapsed 478 s, estimated 11444 s (3 hours), iters = {MDP: 693}, opt = -8.545 +> progress 4.178%, elapsed 482 s, estimated 11539 s (3 hours), iters = {MDP: 701}, opt = -8.545 +> progress 4.178%, elapsed 486 s, estimated 11642 s (3 hours), iters = {MDP: 704}, opt = -8.545 +> progress 4.178%, elapsed 489 s, estimated 11719 s (3 hours), iters = {MDP: 714}, opt = -8.545 +> progress 4.178%, elapsed 492 s, estimated 11792 s (3 hours), iters = {MDP: 720}, opt = -8.545 +> progress 4.178%, elapsed 496 s, estimated 11876 s (3 hours), iters = {MDP: 725}, opt = -8.545 +> progress 4.178%, elapsed 499 s, estimated 11959 s (3 hours), iters = {MDP: 728}, opt = -8.545 +> progress 4.178%, elapsed 502 s, estimated 12034 s (3 hours), iters = {MDP: 739}, opt = -8.545 +> progress 4.178%, elapsed 505 s, estimated 12108 s (3 hours), iters = {MDP: 744}, opt = -8.545 +> progress 4.178%, elapsed 510 s, estimated 12212 s (3 hours), iters = {MDP: 750}, opt = -8.545 +> progress 4.178%, elapsed 514 s, estimated 12314 s (3 hours), iters = {MDP: 752}, opt = -8.545 +> progress 4.178%, elapsed 517 s, estimated 12389 s (3 hours), iters = {MDP: 758}, opt = -8.545 +> progress 4.178%, elapsed 520 s, estimated 12462 s (3 hours), iters = {MDP: 766}, opt = -8.545 +> progress 4.178%, elapsed 524 s, estimated 12546 s (3 hours), iters = {MDP: 770}, opt = -8.545 +> progress 4.178%, elapsed 527 s, estimated 12624 s (3 hours), iters = {MDP: 780}, opt = -8.545 +> progress 4.178%, elapsed 530 s, estimated 12697 s (3 hours), iters = {MDP: 790}, opt = -8.545 +> progress 4.178%, elapsed 534 s, estimated 12785 s (3 hours), iters = {MDP: 793}, opt = -8.545 +> progress 4.178%, elapsed 538 s, estimated 12878 s (3 hours), iters = {MDP: 796}, opt = -8.545 +> progress 4.178%, elapsed 542 s, estimated 12982 s (3 hours), iters = {MDP: 799}, opt = -8.545 +> progress 4.178%, elapsed 545 s, estimated 13062 s (3 hours), iters = {MDP: 807}, opt = -8.545 +> progress 4.178%, elapsed 548 s, estimated 13136 s (3 hours), iters = {MDP: 810}, opt = -8.545 +> progress 4.178%, elapsed 552 s, estimated 13218 s (3 hours), iters = {MDP: 816}, opt = -8.545 +> progress 4.178%, elapsed 556 s, estimated 13323 s (3 hours), iters = {MDP: 822}, opt = -8.545 +> progress 4.178%, elapsed 561 s, estimated 13429 s (3 hours), iters = {MDP: 824}, opt = -8.545 +> progress 4.178%, elapsed 564 s, estimated 13504 s (3 hours), iters = {MDP: 831}, opt = -8.545 +> progress 4.178%, elapsed 567 s, estimated 13584 s (3 hours), iters = {MDP: 837}, opt = -8.545 +> progress 4.178%, elapsed 570 s, estimated 13660 s (3 hours), iters = {MDP: 844}, opt = -8.545 +> progress 4.178%, elapsed 574 s, estimated 13739 s (3 hours), iters = {MDP: 849}, opt = -8.545 +> progress 4.178%, elapsed 577 s, estimated 13811 s (3 hours), iters = {MDP: 856}, opt = -8.545 +> progress 4.178%, elapsed 580 s, estimated 13892 s (3 hours), iters = {MDP: 869}, opt = -8.545 +> progress 4.178%, elapsed 583 s, estimated 13966 s (3 hours), iters = {MDP: 876}, opt = -8.545 +> progress 4.178%, elapsed 588 s, estimated 14085 s (3 hours), iters = {MDP: 880}, opt = -8.545 +> progress 4.178%, elapsed 592 s, estimated 14167 s (3 hours), iters = {MDP: 883}, opt = -8.545 +> progress 4.178%, elapsed 596 s, estimated 14281 s (3 hours), iters = {MDP: 886}, opt = -8.545 +> progress 4.178%, elapsed 600 s, estimated 14363 s (3 hours), iters = {MDP: 893}, opt = -8.545 +> progress 4.178%, elapsed 603 s, estimated 14439 s (4 hours), iters = {MDP: 898}, opt = -8.545 +> progress 4.178%, elapsed 606 s, estimated 14514 s (4 hours), iters = {MDP: 904}, opt = -8.545 +> progress 4.178%, elapsed 609 s, estimated 14596 s (4 hours), iters = {MDP: 908}, opt = -8.545 +> progress 4.178%, elapsed 613 s, estimated 14670 s (4 hours), iters = {MDP: 915}, opt = -8.545 +> progress 4.178%, elapsed 617 s, estimated 14778 s (4 hours), iters = {MDP: 917}, opt = -8.545 +> progress 4.178%, elapsed 620 s, estimated 14852 s (4 hours), iters = {MDP: 923}, opt = -8.545 +> progress 4.178%, elapsed 623 s, estimated 14925 s (4 hours), iters = {MDP: 927}, opt = -8.545 +> progress 4.178%, elapsed 626 s, estimated 14998 s (4 hours), iters = {MDP: 932}, opt = -8.545 +> progress 4.178%, elapsed 630 s, estimated 15086 s (4 hours), iters = {MDP: 939}, opt = -8.545 +> progress 4.178%, elapsed 634 s, estimated 15193 s (4 hours), iters = {MDP: 947}, opt = -8.545 +> progress 4.178%, elapsed 638 s, estimated 15271 s (4 hours), iters = {MDP: 950}, opt = -8.545 +> progress 4.178%, elapsed 641 s, estimated 15343 s (4 hours), iters = {MDP: 952}, opt = -8.545 +> progress 4.178%, elapsed 644 s, estimated 15423 s (4 hours), iters = {MDP: 956}, opt = -8.545 +> progress 4.178%, elapsed 647 s, estimated 15497 s (4 hours), iters = {MDP: 962}, opt = -8.545 +> progress 4.178%, elapsed 651 s, estimated 15588 s (4 hours), iters = {MDP: 966}, opt = -8.545 +> progress 4.178%, elapsed 654 s, estimated 15661 s (4 hours), iters = {MDP: 974}, opt = -8.545 +> progress 4.178%, elapsed 657 s, estimated 15744 s (4 hours), iters = {MDP: 982}, opt = -8.545 +> progress 4.178%, elapsed 661 s, estimated 15833 s (4 hours), iters = {MDP: 990}, opt = -8.545 +> progress 4.178%, elapsed 665 s, estimated 15916 s (4 hours), iters = {MDP: 998}, opt = -8.545 +> progress 4.178%, elapsed 668 s, estimated 15989 s (4 hours), iters = {MDP: 1004}, opt = -8.545 +> progress 4.178%, elapsed 672 s, estimated 16081 s (4 hours), iters = {MDP: 1010}, opt = -8.545 +> progress 4.178%, elapsed 675 s, estimated 16159 s (4 hours), iters = {MDP: 1012}, opt = -8.545 +> progress 4.178%, elapsed 679 s, estimated 16259 s (4 hours), iters = {MDP: 1020}, opt = -8.545 +> progress 4.178%, elapsed 682 s, estimated 16341 s (4 hours), iters = {MDP: 1026}, opt = -8.545 +> progress 4.178%, elapsed 686 s, estimated 16425 s (4 hours), iters = {MDP: 1033}, opt = -8.545 +> progress 4.178%, elapsed 689 s, estimated 16498 s (4 hours), iters = {MDP: 1038}, opt = -8.545 +> progress 4.178%, elapsed 692 s, estimated 16575 s (4 hours), iters = {MDP: 1041}, opt = -8.545 +> progress 4.178%, elapsed 695 s, estimated 16648 s (4 hours), iters = {MDP: 1043}, opt = -8.545 +> progress 4.178%, elapsed 698 s, estimated 16724 s (4 hours), iters = {MDP: 1047}, opt = -8.545 +> progress 4.178%, elapsed 702 s, estimated 16800 s (4 hours), iters = {MDP: 1054}, opt = -8.545 +> progress 4.178%, elapsed 705 s, estimated 16881 s (4 hours), iters = {MDP: 1057}, opt = -8.545 +> progress 4.178%, elapsed 708 s, estimated 16965 s (4 hours), iters = {MDP: 1065}, opt = -8.545 +> progress 4.178%, elapsed 712 s, estimated 17050 s (4 hours), iters = {MDP: 1073}, opt = -8.545 +> progress 4.178%, elapsed 715 s, estimated 17125 s (4 hours), iters = {MDP: 1081}, opt = -8.545 +> progress 4.178%, elapsed 719 s, estimated 17211 s (4 hours), iters = {MDP: 1089}, opt = -8.545 +> progress 4.178%, elapsed 722 s, estimated 17299 s (4 hours), iters = {MDP: 1096}, opt = -8.545 +> progress 4.178%, elapsed 726 s, estimated 17378 s (4 hours), iters = {MDP: 1101}, opt = -8.545 +> progress 4.178%, elapsed 729 s, estimated 17457 s (4 hours), iters = {MDP: 1103}, opt = -8.545 +> progress 4.178%, elapsed 733 s, estimated 17557 s (4 hours), iters = {MDP: 1111}, opt = -8.545 +> progress 4.178%, elapsed 736 s, estimated 17633 s (4 hours), iters = {MDP: 1117}, opt = -8.545 +> progress 4.178%, elapsed 740 s, estimated 17720 s (4 hours), iters = {MDP: 1124}, opt = -8.545 +> progress 4.178%, elapsed 745 s, estimated 17840 s (4 hours), iters = {MDP: 1132}, opt = -8.545 +> progress 4.178%, elapsed 748 s, estimated 17922 s (4 hours), iters = {MDP: 1135}, opt = -8.545 +> progress 4.178%, elapsed 753 s, estimated 18034 s (5 hours), iters = {MDP: 1138}, opt = -8.545 +> progress 4.178%, elapsed 756 s, estimated 18114 s (5 hours), iters = {MDP: 1144}, opt = -8.545 +> progress 4.178%, elapsed 760 s, estimated 18201 s (5 hours), iters = {MDP: 1150}, opt = -8.545 +> progress 4.178%, elapsed 763 s, estimated 18275 s (5 hours), iters = {MDP: 1158}, opt = -8.545 +> progress 4.178%, elapsed 766 s, estimated 18352 s (5 hours), iters = {MDP: 1166}, opt = -8.545 +> progress 4.178%, elapsed 769 s, estimated 18425 s (5 hours), iters = {MDP: 1173}, opt = -8.545 +> progress 4.178%, elapsed 773 s, estimated 18505 s (5 hours), iters = {MDP: 1181}, opt = -8.545 +> progress 4.178%, elapsed 776 s, estimated 18584 s (5 hours), iters = {MDP: 1185}, opt = -8.545 +> progress 4.178%, elapsed 779 s, estimated 18659 s (5 hours), iters = {MDP: 1194}, opt = -8.545 +> progress 4.18%, elapsed 785 s, estimated 18781 s (5 hours), iters = {MDP: 1197}, opt = -8.545 +> progress 4.18%, elapsed 788 s, estimated 18860 s (5 hours), iters = {MDP: 1198}, opt = -8.545 +> progress 4.18%, elapsed 791 s, estimated 18937 s (5 hours), iters = {MDP: 1200}, opt = -8.545 +> progress 4.18%, elapsed 796 s, estimated 19052 s (5 hours), iters = {MDP: 1206}, opt = -8.545 +> progress 4.18%, elapsed 801 s, estimated 19166 s (5 hours), iters = {MDP: 1214}, opt = -8.545 +> progress 4.18%, elapsed 805 s, estimated 19270 s (5 hours), iters = {MDP: 1216}, opt = -8.545 +> progress 4.18%, elapsed 809 s, estimated 19355 s (5 hours), iters = {MDP: 1218}, opt = -8.545 +> progress 4.18%, elapsed 813 s, estimated 19467 s (5 hours), iters = {MDP: 1226}, opt = -8.545 +> progress 4.18%, elapsed 818 s, estimated 19579 s (5 hours), iters = {MDP: 1228}, opt = -8.545 +> progress 4.18%, elapsed 821 s, estimated 19654 s (5 hours), iters = {MDP: 1231}, opt = -8.545 +> progress 4.18%, elapsed 824 s, estimated 19733 s (5 hours), iters = {MDP: 1248}, opt = -8.545 +> progress 4.18%, elapsed 828 s, estimated 19806 s (5 hours), iters = {MDP: 1279}, opt = -8.545 +> progress 4.18%, elapsed 831 s, estimated 19881 s (5 hours), iters = {MDP: 1301}, opt = -8.545 +> progress 4.18%, elapsed 835 s, estimated 19992 s (5 hours), iters = {MDP: 1319}, opt = -8.545 +> progress 4.18%, elapsed 839 s, estimated 20069 s (5 hours), iters = {MDP: 1321}, opt = -8.545 +> progress 4.18%, elapsed 842 s, estimated 20151 s (5 hours), iters = {MDP: 1326}, opt = -8.545 +> progress 4.18%, elapsed 845 s, estimated 20228 s (5 hours), iters = {MDP: 1330}, opt = -8.545 +> progress 4.18%, elapsed 848 s, estimated 20308 s (5 hours), iters = {MDP: 1345}, opt = -8.545 +> progress 4.18%, elapsed 852 s, estimated 20392 s (5 hours), iters = {MDP: 1349}, opt = -8.545 +> progress 4.18%, elapsed 855 s, estimated 20467 s (5 hours), iters = {MDP: 1354}, opt = -8.545 +> progress 4.18%, elapsed 859 s, estimated 20549 s (5 hours), iters = {MDP: 1360}, opt = -8.545 +> progress 4.18%, elapsed 862 s, estimated 20622 s (5 hours), iters = {MDP: 1364}, opt = -8.545 +> progress 4.18%, elapsed 866 s, estimated 20725 s (5 hours), iters = {MDP: 1369}, opt = -8.545 +> progress 4.18%, elapsed 869 s, estimated 20798 s (5 hours), iters = {MDP: 1382}, opt = -8.545 +> progress 4.18%, elapsed 872 s, estimated 20874 s (5 hours), iters = {MDP: 1397}, opt = -8.545 +> progress 4.18%, elapsed 875 s, estimated 20947 s (5 hours), iters = {MDP: 1414}, opt = -8.545 +> progress 4.18%, elapsed 878 s, estimated 21019 s (5 hours), iters = {MDP: 1429}, opt = -8.545 +> progress 4.18%, elapsed 881 s, estimated 21092 s (5 hours), iters = {MDP: 1435}, opt = -8.545 +> progress 4.18%, elapsed 885 s, estimated 21170 s (5 hours), iters = {MDP: 1448}, opt = -8.545 +> progress 4.18%, elapsed 888 s, estimated 21253 s (5 hours), iters = {MDP: 1461}, opt = -8.545 +> progress 4.18%, elapsed 891 s, estimated 21334 s (5 hours), iters = {MDP: 1464}, opt = -8.545 +> progress 4.18%, elapsed 895 s, estimated 21420 s (5 hours), iters = {MDP: 1466}, opt = -8.545 +> progress 4.18%, elapsed 898 s, estimated 21501 s (5 hours), iters = {MDP: 1468}, opt = -8.545 +> progress 4.18%, elapsed 902 s, estimated 21581 s (5 hours), iters = {MDP: 1472}, opt = -8.545 +> progress 4.18%, elapsed 905 s, estimated 21655 s (6 hours), iters = {MDP: 1477}, opt = -8.545 +> progress 4.18%, elapsed 908 s, estimated 21737 s (6 hours), iters = {MDP: 1486}, opt = -8.545 +> progress 4.18%, elapsed 912 s, estimated 21821 s (6 hours), iters = {MDP: 1491}, opt = -8.545 +> progress 4.18%, elapsed 915 s, estimated 21896 s (6 hours), iters = {MDP: 1495}, opt = -8.545 +> progress 4.18%, elapsed 918 s, estimated 21971 s (6 hours), iters = {MDP: 1511}, opt = -8.545 +> progress 4.18%, elapsed 921 s, estimated 22048 s (6 hours), iters = {MDP: 1533}, opt = -8.545 +> progress 4.18%, elapsed 925 s, estimated 22133 s (6 hours), iters = {MDP: 1544}, opt = -8.545 +> progress 4.18%, elapsed 928 s, estimated 22209 s (6 hours), iters = {MDP: 1552}, opt = -8.545 +> progress 4.18%, elapsed 931 s, estimated 22283 s (6 hours), iters = {MDP: 1565}, opt = -8.545 +> progress 4.18%, elapsed 934 s, estimated 22360 s (6 hours), iters = {MDP: 1568}, opt = -8.545 +> progress 4.18%, elapsed 938 s, estimated 22460 s (6 hours), iters = {MDP: 1570}, opt = -8.545 +> progress 4.18%, elapsed 943 s, estimated 22567 s (6 hours), iters = {MDP: 1572}, opt = -8.545 +> progress 4.18%, elapsed 947 s, estimated 22662 s (6 hours), iters = {MDP: 1574}, opt = -8.545 +> progress 4.18%, elapsed 951 s, estimated 22756 s (6 hours), iters = {MDP: 1587}, opt = -8.545 +> progress 4.18%, elapsed 954 s, estimated 22829 s (6 hours), iters = {MDP: 1592}, opt = -8.545 +> progress 4.18%, elapsed 958 s, estimated 22916 s (6 hours), iters = {MDP: 1598}, opt = -8.545 +> progress 4.18%, elapsed 961 s, estimated 22990 s (6 hours), iters = {MDP: 1605}, opt = -8.545 +> progress 4.18%, elapsed 964 s, estimated 23070 s (6 hours), iters = {MDP: 1613}, opt = -8.545 +> progress 4.18%, elapsed 968 s, estimated 23169 s (6 hours), iters = {MDP: 1622}, opt = -8.545 +> progress 4.18%, elapsed 971 s, estimated 23243 s (6 hours), iters = {MDP: 1624}, opt = -8.545 +> progress 4.18%, elapsed 975 s, estimated 23323 s (6 hours), iters = {MDP: 1636}, opt = -8.545 +> progress 4.18%, elapsed 979 s, estimated 23431 s (6 hours), iters = {MDP: 1641}, opt = -8.545 +> progress 4.18%, elapsed 983 s, estimated 23513 s (6 hours), iters = {MDP: 1648}, opt = -8.545 +> progress 4.18%, elapsed 987 s, estimated 23614 s (6 hours), iters = {MDP: 1656}, opt = -8.545 +> progress 4.18%, elapsed 991 s, estimated 23727 s (6 hours), iters = {MDP: 1659}, opt = -8.545 +> progress 4.18%, elapsed 996 s, estimated 23824 s (6 hours), iters = {MDP: 1661}, opt = -8.545 +> progress 4.18%, elapsed 999 s, estimated 23902 s (6 hours), iters = {MDP: 1664}, opt = -8.545 +> progress 4.18%, elapsed 1002 s, estimated 23975 s (6 hours), iters = {MDP: 1671}, opt = -8.545 +> progress 4.18%, elapsed 1005 s, estimated 24062 s (6 hours), iters = {MDP: 1680}, opt = -8.545 +> progress 4.18%, elapsed 1010 s, estimated 24162 s (6 hours), iters = {MDP: 1683}, opt = -8.545 +> progress 4.18%, elapsed 1014 s, estimated 24267 s (6 hours), iters = {MDP: 1691}, opt = -8.545 +> progress 4.18%, elapsed 1017 s, estimated 24348 s (6 hours), iters = {MDP: 1697}, opt = -8.545 +> progress 4.18%, elapsed 1021 s, estimated 24432 s (6 hours), iters = {MDP: 1703}, opt = -8.545 +> progress 4.18%, elapsed 1024 s, estimated 24504 s (6 hours), iters = {MDP: 1706}, opt = -8.545 +> progress 4.18%, elapsed 1028 s, estimated 24611 s (6 hours), iters = {MDP: 1722}, opt = -8.545 +> progress 4.18%, elapsed 1032 s, estimated 24703 s (6 hours), iters = {MDP: 1725}, opt = -8.545 +> progress 4.18%, elapsed 1035 s, estimated 24777 s (6 hours), iters = {MDP: 1733}, opt = -8.545 +> progress 4.18%, elapsed 1039 s, estimated 24862 s (6 hours), iters = {MDP: 1737}, opt = -8.545 +> progress 4.18%, elapsed 1042 s, estimated 24943 s (6 hours), iters = {MDP: 1740}, opt = -8.545 +> progress 4.18%, elapsed 1045 s, estimated 25016 s (6 hours), iters = {MDP: 1746}, opt = -8.545 +> progress 4.18%, elapsed 1050 s, estimated 25126 s (6 hours), iters = {MDP: 1752}, opt = -8.545 +> progress 4.18%, elapsed 1053 s, estimated 25208 s (7 hours), iters = {MDP: 1754}, opt = -8.545 +> progress 4.18%, elapsed 1057 s, estimated 25291 s (7 hours), iters = {MDP: 1761}, opt = -8.545 +> progress 4.18%, elapsed 1060 s, estimated 25374 s (7 hours), iters = {MDP: 1765}, opt = -8.545 +> progress 4.18%, elapsed 1064 s, estimated 25453 s (7 hours), iters = {MDP: 1774}, opt = -8.545 +> progress 4.18%, elapsed 1067 s, estimated 25539 s (7 hours), iters = {MDP: 1777}, opt = -8.545 +> progress 4.18%, elapsed 1071 s, estimated 25624 s (7 hours), iters = {MDP: 1779}, opt = -8.545 +> progress 4.18%, elapsed 1074 s, estimated 25710 s (7 hours), iters = {MDP: 1786}, opt = -8.545 +> progress 4.18%, elapsed 1078 s, estimated 25786 s (7 hours), iters = {MDP: 1791}, opt = -8.545 +> progress 4.18%, elapsed 1081 s, estimated 25859 s (7 hours), iters = {MDP: 1796}, opt = -8.545 +> progress 4.18%, elapsed 1084 s, estimated 25938 s (7 hours), iters = {MDP: 1800}, opt = -8.545 +> progress 4.18%, elapsed 1088 s, estimated 26028 s (7 hours), iters = {MDP: 1803}, opt = -8.545 +> progress 4.18%, elapsed 1091 s, estimated 26103 s (7 hours), iters = {MDP: 1807}, opt = -8.545 +> progress 4.18%, elapsed 1095 s, estimated 26212 s (7 hours), iters = {MDP: 1816}, opt = -8.545 +> progress 4.18%, elapsed 1101 s, estimated 26336 s (7 hours), iters = {MDP: 1818}, opt = -8.545 +> progress 4.18%, elapsed 1104 s, estimated 26424 s (7 hours), iters = {MDP: 1820}, opt = -8.545 +> progress 4.18%, elapsed 1112 s, estimated 26601 s (7 hours), iters = {MDP: 1822}, opt = -8.545 +> progress 4.18%, elapsed 1115 s, estimated 26693 s (7 hours), iters = {MDP: 1830}, opt = -8.545 +> progress 4.18%, elapsed 1119 s, estimated 26780 s (7 hours), iters = {MDP: 1839}, opt = -8.545 +> progress 4.18%, elapsed 1122 s, estimated 26859 s (7 hours), iters = {MDP: 1841}, opt = -8.545 +> progress 4.18%, elapsed 1127 s, estimated 26956 s (7 hours), iters = {MDP: 1849}, opt = -8.545 +> progress 4.18%, elapsed 1130 s, estimated 27034 s (7 hours), iters = {MDP: 1855}, opt = -8.545 +> progress 4.18%, elapsed 1133 s, estimated 27116 s (7 hours), iters = {MDP: 1861}, opt = -8.545 +> progress 4.18%, elapsed 1137 s, estimated 27196 s (7 hours), iters = {MDP: 1865}, opt = -8.545 +> progress 4.18%, elapsed 1141 s, estimated 27292 s (7 hours), iters = {MDP: 1880}, opt = -8.545 +> progress 4.18%, elapsed 1145 s, estimated 27389 s (7 hours), iters = {MDP: 1883}, opt = -8.545 +> progress 4.18%, elapsed 1148 s, estimated 27464 s (7 hours), iters = {MDP: 1891}, opt = -8.545 +> progress 4.18%, elapsed 1151 s, estimated 27547 s (7 hours), iters = {MDP: 1895}, opt = -8.545 +> progress 4.18%, elapsed 1155 s, estimated 27628 s (7 hours), iters = {MDP: 1898}, opt = -8.545 +> progress 4.18%, elapsed 1158 s, estimated 27702 s (7 hours), iters = {MDP: 1904}, opt = -8.545 +> progress 4.18%, elapsed 1163 s, estimated 27821 s (7 hours), iters = {MDP: 1910}, opt = -8.545 +> progress 4.18%, elapsed 1166 s, estimated 27905 s (7 hours), iters = {MDP: 1912}, opt = -8.545 +> progress 4.18%, elapsed 1170 s, estimated 27986 s (7 hours), iters = {MDP: 1919}, opt = -8.545 +> progress 4.18%, elapsed 1173 s, estimated 28067 s (7 hours), iters = {MDP: 1923}, opt = -8.545 +> progress 4.18%, elapsed 1176 s, estimated 28147 s (7 hours), iters = {MDP: 1932}, opt = -8.545 +> progress 4.18%, elapsed 1180 s, estimated 28231 s (7 hours), iters = {MDP: 1935}, opt = -8.545 +> progress 4.18%, elapsed 1183 s, estimated 28313 s (7 hours), iters = {MDP: 1937}, opt = -8.545 +> progress 4.18%, elapsed 1187 s, estimated 28395 s (7 hours), iters = {MDP: 1944}, opt = -8.545 +> progress 4.18%, elapsed 1190 s, estimated 28467 s (7 hours), iters = {MDP: 1949}, opt = -8.545 +> progress 4.18%, elapsed 1193 s, estimated 28539 s (7 hours), iters = {MDP: 1954}, opt = -8.545 +> progress 4.18%, elapsed 1196 s, estimated 28619 s (7 hours), iters = {MDP: 1958}, opt = -8.545 +> progress 4.18%, elapsed 1200 s, estimated 28708 s (7 hours), iters = {MDP: 1961}, opt = -8.545 +> progress 4.18%, elapsed 1203 s, estimated 28790 s (7 hours), iters = {MDP: 1966}, opt = -8.545 +> progress 4.18%, elapsed 1207 s, estimated 28889 s (8 hours), iters = {MDP: 1974}, opt = -8.545 +> progress 4.18%, elapsed 1212 s, estimated 29011 s (8 hours), iters = {MDP: 1976}, opt = -8.545 +> progress 4.18%, elapsed 1216 s, estimated 29086 s (8 hours), iters = {MDP: 1983}, opt = -8.545 +> progress 4.18%, elapsed 1219 s, estimated 29173 s (8 hours), iters = {MDP: 1988}, opt = -8.545 +> progress 4.18%, elapsed 1222 s, estimated 29248 s (8 hours), iters = {MDP: 1994}, opt = -8.545 +> progress 4.18%, elapsed 1225 s, estimated 29321 s (8 hours), iters = {MDP: 2000}, opt = -8.545 +> progress 4.181%, elapsed 1229 s, estimated 29403 s (8 hours), iters = {MDP: 2003}, opt = -8.545 +> progress 4.181%, elapsed 1232 s, estimated 29485 s (8 hours), iters = {MDP: 2008}, opt = -8.545 +> progress 4.181%, elapsed 1237 s, estimated 29587 s (8 hours), iters = {MDP: 2014}, opt = -8.545 +> progress 4.181%, elapsed 1241 s, estimated 29693 s (8 hours), iters = {MDP: 2021}, opt = -8.545 +> progress 4.181%, elapsed 1245 s, estimated 29793 s (8 hours), iters = {MDP: 2024}, opt = -8.545 +> progress 4.181%, elapsed 1249 s, estimated 29889 s (8 hours), iters = {MDP: 2027}, opt = -8.545 +> progress 4.181%, elapsed 1252 s, estimated 29964 s (8 hours), iters = {MDP: 2029}, opt = -8.545 +> progress 4.181%, elapsed 1255 s, estimated 30038 s (8 hours), iters = {MDP: 2032}, opt = -8.545 +> progress 4.181%, elapsed 1259 s, estimated 30113 s (8 hours), iters = {MDP: 2043}, opt = -8.545 +> progress 4.181%, elapsed 1262 s, estimated 30192 s (8 hours), iters = {MDP: 2048}, opt = -8.545 +> progress 4.181%, elapsed 1265 s, estimated 30267 s (8 hours), iters = {MDP: 2051}, opt = -8.545 +> progress 4.181%, elapsed 1268 s, estimated 30350 s (8 hours), iters = {MDP: 2056}, opt = -8.545 +> progress 4.181%, elapsed 1272 s, estimated 30443 s (8 hours), iters = {MDP: 2061}, opt = -8.545 +> progress 4.181%, elapsed 1277 s, estimated 30547 s (8 hours), iters = {MDP: 2064}, opt = -8.545 +> progress 4.181%, elapsed 1280 s, estimated 30619 s (8 hours), iters = {MDP: 2066}, opt = -8.545 +> progress 4.181%, elapsed 1283 s, estimated 30703 s (8 hours), iters = {MDP: 2071}, opt = -8.545 +> progress 4.181%, elapsed 1288 s, estimated 30827 s (8 hours), iters = {MDP: 2077}, opt = -8.545 +> progress 4.181%, elapsed 1291 s, estimated 30900 s (8 hours), iters = {MDP: 2078}, opt = -8.545 +> progress 4.181%, elapsed 1295 s, estimated 30977 s (8 hours), iters = {MDP: 2080}, opt = -8.545 +> progress 4.181%, elapsed 1298 s, estimated 31054 s (8 hours), iters = {MDP: 2097}, opt = -8.545 +> progress 4.181%, elapsed 1301 s, estimated 31125 s (8 hours), iters = {MDP: 2108}, opt = -8.545 +> progress 4.181%, elapsed 1304 s, estimated 31209 s (8 hours), iters = {MDP: 2119}, opt = -8.545 +> progress 4.181%, elapsed 1308 s, estimated 31284 s (8 hours), iters = {MDP: 2121}, opt = -8.545 +> progress 4.181%, elapsed 1311 s, estimated 31362 s (8 hours), iters = {MDP: 2126}, opt = -8.545 +> progress 4.181%, elapsed 1314 s, estimated 31434 s (8 hours), iters = {MDP: 2133}, opt = -8.545 +> progress 4.181%, elapsed 1317 s, estimated 31511 s (8 hours), iters = {MDP: 2141}, opt = -8.545 +> progress 4.181%, elapsed 1320 s, estimated 31592 s (8 hours), iters = {MDP: 2146}, opt = -8.545 +> progress 4.181%, elapsed 1324 s, estimated 31676 s (8 hours), iters = {MDP: 2153}, opt = -8.545 +> progress 4.181%, elapsed 1328 s, estimated 31764 s (8 hours), iters = {MDP: 2157}, opt = -8.545 +> progress 4.181%, elapsed 1331 s, estimated 31837 s (8 hours), iters = {MDP: 2160}, opt = -8.545 +> progress 4.181%, elapsed 1335 s, estimated 31933 s (8 hours), iters = {MDP: 2165}, opt = -8.545 +> progress 4.181%, elapsed 1338 s, estimated 32005 s (8 hours), iters = {MDP: 2173}, opt = -8.545 +> progress 4.181%, elapsed 1341 s, estimated 32084 s (8 hours), iters = {MDP: 2184}, opt = -8.545 +> progress 4.181%, elapsed 1344 s, estimated 32162 s (8 hours), iters = {MDP: 2191}, opt = -8.545 +> progress 4.181%, elapsed 1348 s, estimated 32243 s (8 hours), iters = {MDP: 2199}, opt = -8.545 +> progress 4.181%, elapsed 1352 s, estimated 32351 s (8 hours), iters = {MDP: 2203}, opt = -8.545 +> progress 4.181%, elapsed 1356 s, estimated 32450 s (9 hours), iters = {MDP: 2205}, opt = -8.545 +> progress 4.181%, elapsed 1359 s, estimated 32525 s (9 hours), iters = {MDP: 2222}, opt = -8.545 +> progress 4.181%, elapsed 1363 s, estimated 32612 s (9 hours), iters = {MDP: 2243}, opt = -8.545 +> progress 4.181%, elapsed 1366 s, estimated 32692 s (9 hours), iters = {MDP: 2259}, opt = -8.545 +> progress 4.181%, elapsed 1370 s, estimated 32771 s (9 hours), iters = {MDP: 2262}, opt = -8.545 +> progress 4.181%, elapsed 1373 s, estimated 32843 s (9 hours), iters = {MDP: 2267}, opt = -8.545 +> progress 4.181%, elapsed 1376 s, estimated 32918 s (9 hours), iters = {MDP: 2270}, opt = -8.545 +> progress 4.181%, elapsed 1379 s, estimated 32992 s (9 hours), iters = {MDP: 2281}, opt = -8.545 +> progress 4.181%, elapsed 1382 s, estimated 33067 s (9 hours), iters = {MDP: 2294}, opt = -8.545 +> progress 4.181%, elapsed 1386 s, estimated 33153 s (9 hours), iters = {MDP: 2298}, opt = -8.545 +> progress 4.181%, elapsed 1389 s, estimated 33226 s (9 hours), iters = {MDP: 2302}, opt = -8.545 +> progress 4.181%, elapsed 1393 s, estimated 33321 s (9 hours), iters = {MDP: 2306}, opt = -8.545 +> progress 4.181%, elapsed 1396 s, estimated 33395 s (9 hours), iters = {MDP: 2320}, opt = -8.545 +> progress 4.181%, elapsed 1399 s, estimated 33468 s (9 hours), iters = {MDP: 2337}, opt = -8.545 +> progress 4.181%, elapsed 1402 s, estimated 33548 s (9 hours), iters = {MDP: 2354}, opt = -8.545 +> progress 4.181%, elapsed 1406 s, estimated 33626 s (9 hours), iters = {MDP: 2369}, opt = -8.545 +> progress 4.181%, elapsed 1409 s, estimated 33700 s (9 hours), iters = {MDP: 2388}, opt = -8.545 +> progress 4.181%, elapsed 1412 s, estimated 33777 s (9 hours), iters = {MDP: 2410}, opt = -8.545 +> progress 4.181%, elapsed 1415 s, estimated 33853 s (9 hours), iters = {MDP: 2429}, opt = -8.545 +> progress 4.181%, elapsed 1418 s, estimated 33928 s (9 hours), iters = {MDP: 2448}, opt = -8.545 +> progress 4.181%, elapsed 1422 s, estimated 34019 s (9 hours), iters = {MDP: 2460}, opt = -8.545 +> progress 4.181%, elapsed 1425 s, estimated 34103 s (9 hours), iters = {MDP: 2464}, opt = -8.545 +> progress 4.181%, elapsed 1429 s, estimated 34182 s (9 hours), iters = {MDP: 2470}, opt = -8.545 +> progress 4.181%, elapsed 1432 s, estimated 34254 s (9 hours), iters = {MDP: 2485}, opt = -8.545 +> progress 4.181%, elapsed 1435 s, estimated 34338 s (9 hours), iters = {MDP: 2488}, opt = -8.545 +> progress 4.181%, elapsed 1440 s, estimated 34456 s (9 hours), iters = {MDP: 2490}, opt = -8.545 +> progress 4.181%, elapsed 1444 s, estimated 34551 s (9 hours), iters = {MDP: 2492}, opt = -8.545 +> progress 4.181%, elapsed 1448 s, estimated 34644 s (9 hours), iters = {MDP: 2505}, opt = -8.545 +> progress 4.181%, elapsed 1451 s, estimated 34717 s (9 hours), iters = {MDP: 2508}, opt = -8.545 +> progress 4.181%, elapsed 1455 s, estimated 34817 s (9 hours), iters = {MDP: 2521}, opt = -8.545 +> progress 4.181%, elapsed 1459 s, estimated 34904 s (9 hours), iters = {MDP: 2523}, opt = -8.545 +> progress 4.181%, elapsed 1464 s, estimated 35020 s (9 hours), iters = {MDP: 2526}, opt = -8.545 +> progress 4.181%, elapsed 1467 s, estimated 35102 s (9 hours), iters = {MDP: 2528}, opt = -8.545 +> progress 4.181%, elapsed 1471 s, estimated 35191 s (9 hours), iters = {MDP: 2536}, opt = -8.545 +> progress 4.181%, elapsed 1474 s, estimated 35273 s (9 hours), iters = {MDP: 2545}, opt = -8.545 +> progress 4.181%, elapsed 1478 s, estimated 35361 s (9 hours), iters = {MDP: 2548}, opt = -8.545 +> progress 4.181%, elapsed 1481 s, estimated 35441 s (9 hours), iters = {MDP: 2550}, opt = -8.545 +> progress 4.181%, elapsed 1485 s, estimated 35529 s (9 hours), iters = {MDP: 2558}, opt = -8.545 +> progress 4.181%, elapsed 1489 s, estimated 35614 s (9 hours), iters = {MDP: 2561}, opt = -8.545 +> progress 4.181%, elapsed 1492 s, estimated 35688 s (9 hours), iters = {MDP: 2573}, opt = -8.545 +> progress 4.181%, elapsed 1495 s, estimated 35762 s (9 hours), iters = {MDP: 2585}, opt = -8.545 +> progress 4.181%, elapsed 1499 s, estimated 35855 s (9 hours), iters = {MDP: 2598}, opt = -8.545 +> progress 4.181%, elapsed 1502 s, estimated 35936 s (9 hours), iters = {MDP: 2601}, opt = -8.545 +> progress 4.181%, elapsed 1506 s, estimated 36037 s (10 hours), iters = {MDP: 2603}, opt = -8.545 +> progress 4.181%, elapsed 1510 s, estimated 36117 s (10 hours), iters = {MDP: 2605}, opt = -8.545 +> progress 4.181%, elapsed 1513 s, estimated 36204 s (10 hours), iters = {MDP: 2613}, opt = -8.545 +> progress 4.181%, elapsed 1516 s, estimated 36279 s (10 hours), iters = {MDP: 2621}, opt = -8.545 +> progress 4.181%, elapsed 1521 s, estimated 36383 s (10 hours), iters = {MDP: 2625}, opt = -8.545 +> progress 4.181%, elapsed 1524 s, estimated 36462 s (10 hours), iters = {MDP: 2627}, opt = -8.545 +> progress 4.181%, elapsed 1528 s, estimated 36554 s (10 hours), iters = {MDP: 2635}, opt = -8.545 +> progress 4.181%, elapsed 1531 s, estimated 36627 s (10 hours), iters = {MDP: 2638}, opt = -8.545 +> progress 4.181%, elapsed 1534 s, estimated 36700 s (10 hours), iters = {MDP: 2651}, opt = -8.545 +> progress 4.181%, elapsed 1537 s, estimated 36775 s (10 hours), iters = {MDP: 2662}, opt = -8.545 +> progress 4.181%, elapsed 1541 s, estimated 36869 s (10 hours), iters = {MDP: 2675}, opt = -8.545 +> progress 4.181%, elapsed 1544 s, estimated 36947 s (10 hours), iters = {MDP: 2678}, opt = -8.545 +> progress 4.181%, elapsed 1549 s, estimated 37053 s (10 hours), iters = {MDP: 2680}, opt = -8.545 +> progress 4.181%, elapsed 1552 s, estimated 37135 s (10 hours), iters = {MDP: 2687}, opt = -8.545 +> progress 4.181%, elapsed 1555 s, estimated 37210 s (10 hours), iters = {MDP: 2689}, opt = -8.545 +> progress 4.181%, elapsed 1559 s, estimated 37296 s (10 hours), iters = {MDP: 2692}, opt = -8.545 +> progress 4.181%, elapsed 1562 s, estimated 37373 s (10 hours), iters = {MDP: 2695}, opt = -8.545 +> progress 4.181%, elapsed 1566 s, estimated 37462 s (10 hours), iters = {MDP: 2698}, opt = -8.545 +> progress 4.181%, elapsed 1569 s, estimated 37534 s (10 hours), iters = {MDP: 2710}, opt = -8.545 +> progress 4.181%, elapsed 1572 s, estimated 37615 s (10 hours), iters = {MDP: 2721}, opt = -8.545 +> progress 4.181%, elapsed 1576 s, estimated 37701 s (10 hours), iters = {MDP: 2724}, opt = -8.545 +> progress 4.181%, elapsed 1579 s, estimated 37777 s (10 hours), iters = {MDP: 2727}, opt = -8.545 +> progress 4.181%, elapsed 1582 s, estimated 37852 s (10 hours), iters = {MDP: 2728}, opt = -8.545 +> progress 4.181%, elapsed 1587 s, estimated 37964 s (10 hours), iters = {MDP: 2730}, opt = -8.545 +> progress 4.181%, elapsed 1591 s, estimated 38051 s (10 hours), iters = {MDP: 2732}, opt = -8.545 +> progress 4.181%, elapsed 1594 s, estimated 38124 s (10 hours), iters = {MDP: 2734}, opt = -8.545 +> progress 4.181%, elapsed 1597 s, estimated 38199 s (10 hours), iters = {MDP: 2745}, opt = -8.545 +> progress 4.181%, elapsed 1601 s, estimated 38296 s (10 hours), iters = {MDP: 2749}, opt = -8.545 +> progress 4.181%, elapsed 1605 s, estimated 38401 s (10 hours), iters = {MDP: 2755}, opt = -8.545 +> progress 4.181%, elapsed 1608 s, estimated 38474 s (10 hours), iters = {MDP: 2757}, opt = -8.545 +> progress 4.181%, elapsed 1611 s, estimated 38547 s (10 hours), iters = {MDP: 2765}, opt = -8.545 +> progress 4.181%, elapsed 1615 s, estimated 38620 s (10 hours), iters = {MDP: 2779}, opt = -8.545 +> progress 4.181%, elapsed 1618 s, estimated 38700 s (10 hours), iters = {MDP: 2796}, opt = -8.545 +> progress 4.181%, elapsed 1621 s, estimated 38776 s (10 hours), iters = {MDP: 2802}, opt = -8.545 +> progress 4.181%, elapsed 1625 s, estimated 38863 s (10 hours), iters = {MDP: 2813}, opt = -8.545 +> progress 4.181%, elapsed 1629 s, estimated 38960 s (10 hours), iters = {MDP: 2816}, opt = -8.545 +> progress 4.181%, elapsed 1633 s, estimated 39073 s (10 hours), iters = {MDP: 2819}, opt = -8.545 +> progress 4.181%, elapsed 1637 s, estimated 39158 s (10 hours), iters = {MDP: 2821}, opt = -8.545 +> progress 4.181%, elapsed 1641 s, estimated 39260 s (10 hours), iters = {MDP: 2823}, opt = -8.545 +> progress 4.181%, elapsed 1644 s, estimated 39334 s (10 hours), iters = {MDP: 2833}, opt = -8.545 +> progress 4.181%, elapsed 1648 s, estimated 39412 s (10 hours), iters = {MDP: 2842}, opt = -8.545 +> progress 4.181%, elapsed 1651 s, estimated 39491 s (10 hours), iters = {MDP: 2850}, opt = -8.545 +> progress 4.181%, elapsed 1654 s, estimated 39564 s (10 hours), iters = {MDP: 2854}, opt = -8.545 +> progress 4.181%, elapsed 1659 s, estimated 39676 s (11 hours), iters = {MDP: 2864}, opt = -8.545 +> progress 4.181%, elapsed 1662 s, estimated 39763 s (11 hours), iters = {MDP: 2866}, opt = -8.545 +> progress 4.181%, elapsed 1667 s, estimated 39874 s (11 hours), iters = {MDP: 2868}, opt = -8.545 +> progress 4.181%, elapsed 1671 s, estimated 39968 s (11 hours), iters = {MDP: 2870}, opt = -8.545 +> progress 4.181%, elapsed 1676 s, estimated 40078 s (11 hours), iters = {MDP: 2872}, opt = -8.545 +> progress 4.181%, elapsed 1680 s, estimated 40196 s (11 hours), iters = {MDP: 2874}, opt = -8.545 +> progress 4.181%, elapsed 1684 s, estimated 40271 s (11 hours), iters = {MDP: 2877}, opt = -8.545 +> progress 4.181%, elapsed 1687 s, estimated 40345 s (11 hours), iters = {MDP: 2881}, opt = -8.545 +> progress 4.181%, elapsed 1690 s, estimated 40424 s (11 hours), iters = {MDP: 2883}, opt = -8.545 +> progress 4.181%, elapsed 1693 s, estimated 40496 s (11 hours), iters = {MDP: 2888}, opt = -8.545 +> progress 4.181%, elapsed 1696 s, estimated 40568 s (11 hours), iters = {MDP: 2912}, opt = -8.545 +> progress 4.181%, elapsed 1699 s, estimated 40648 s (11 hours), iters = {MDP: 2919}, opt = -8.545 +> progress 4.181%, elapsed 1703 s, estimated 40724 s (11 hours), iters = {MDP: 2926}, opt = -8.545 +> progress 4.181%, elapsed 1706 s, estimated 40808 s (11 hours), iters = {MDP: 2933}, opt = -8.545 +> progress 4.181%, elapsed 1709 s, estimated 40881 s (11 hours), iters = {MDP: 2935}, opt = -8.545 +> progress 4.181%, elapsed 1714 s, estimated 41004 s (11 hours), iters = {MDP: 2938}, opt = -8.545 diff --git a/experiments/grid-meet-3fsc-nat.log b/experiments/grid-meet-3fsc-nat.log new file mode 100644 index 000000000..bfebfcb15 --- /dev/null +++ b/experiments/grid-meet-3fsc-nat.log @@ -0,0 +1,664 @@ +2024-05-13 21:52:36,995 - cli.py - This is Paynt version 0.1.0. +2024-05-13 21:52:36,996 - sketch.py - loading sketch from models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount-native/sketch.templ ... +2024-05-13 21:52:36,996 - sketch.py - assuming sketch in PRISM format... +2024-05-13 21:52:37,002 - prism_parser.py - PRISM model type: DTMC +2024-05-13 21:52:37,002 - prism_parser.py - processing hole definitions... +2024-05-13 21:52:37,003 - prism_parser.py - loading properties from models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount-native/sketch.props ... +2024-05-13 21:52:37,004 - prism_parser.py - found the following specification: optimality: R[exp]{"moves"}max=? [C{99/100}] +2024-05-13 21:52:37,004 - jani.py - constructing JANI program... +2024-05-13 21:52:37,012 - jani.py - constructing the quotient... +2024-05-13 21:52:44,935 - jani.py - associating choices of the quotient with hole assignments... +2024-05-13 21:52:49,874 - sketch.py - sketch parsing OK +2024-05-13 21:52:49,874 - sketch.py - converting state rewards 'moves' to state-action rewards +2024-05-13 21:52:50,063 - sketch.py - constructed explicit quotient having 20736 states and 2924208 actions +2024-05-13 21:52:50,063 - sketch.py - found the following specification optimality: R[exp]{"moves"}max=? [C{99/100}] +2024-05-13 21:52:52,713 - synthesizer.py - optimality threshold set to -7.621 +2024-05-13 21:52:52,713 - synthesizer.py - synthesis initiated, design space: 1e12 +> progress 0.0%, elapsed 4 s, estimated 4192011 s (48 days), iters = {MDP: 3}, opt = -7.621 +> progress 0.0%, elapsed 7 s, estimated 7275155 s (84 days), iters = {MDP: 5}, opt = -7.621 +> progress 0.26%, elapsed 10 s, estimated 3978 s, iters = {MDP: 12}, opt = -7.621 +> progress 0.26%, elapsed 13 s, estimated 5317 s, iters = {MDP: 19}, opt = -7.621 +> progress 0.26%, elapsed 17 s, estimated 6810 s, iters = {MDP: 25}, opt = -7.621 +> progress 0.26%, elapsed 20 s, estimated 7995 s (2 hours), iters = {MDP: 33}, opt = -7.621 +> progress 0.26%, elapsed 23 s, estimated 9205 s (2 hours), iters = {MDP: 51}, opt = -7.621 +> progress 0.26%, elapsed 27 s, estimated 10375 s (2 hours), iters = {MDP: 64}, opt = -7.621 +> progress 0.26%, elapsed 30 s, estimated 11540 s (3 hours), iters = {MDP: 78}, opt = -7.621 +> progress 0.26%, elapsed 33 s, estimated 12705 s (3 hours), iters = {MDP: 108}, opt = -7.621 +> progress 0.26%, elapsed 36 s, estimated 13927 s (3 hours), iters = {MDP: 138}, opt = -7.621 +> progress 0.26%, elapsed 39 s, estimated 15100 s (4 hours), iters = {MDP: 160}, opt = -7.525 +> progress 0.26%, elapsed 42 s, estimated 16273 s (4 hours), iters = {MDP: 188}, opt = -7.525 +> progress 0.26%, elapsed 45 s, estimated 17484 s (4 hours), iters = {MDP: 195}, opt = -7.525 +> progress 0.26%, elapsed 49 s, estimated 18829 s (5 hours), iters = {MDP: 201}, opt = -7.525 +> progress 0.26%, elapsed 52 s, estimated 20176 s (5 hours), iters = {MDP: 207}, opt = -7.525 +> progress 0.26%, elapsed 55 s, estimated 21383 s (5 hours), iters = {MDP: 217}, opt = -7.525 +> progress 0.26%, elapsed 58 s, estimated 22569 s (6 hours), iters = {MDP: 238}, opt = -7.525 +> progress 0.26%, elapsed 62 s, estimated 23791 s (6 hours), iters = {MDP: 250}, opt = -7.525 +> progress 0.26%, elapsed 65 s, estimated 24970 s (6 hours), iters = {MDP: 263}, opt = -7.525 +> progress 0.26%, elapsed 68 s, estimated 26136 s (7 hours), iters = {MDP: 295}, opt = -7.525 +> progress 0.26%, elapsed 71 s, estimated 27299 s (7 hours), iters = {MDP: 328}, opt = -7.525 +> progress 0.26%, elapsed 74 s, estimated 28452 s (7 hours), iters = {MDP: 365}, opt = -7.525 +> progress 0.26%, elapsed 77 s, estimated 29624 s (8 hours), iters = {MDP: 403}, opt = -7.525 +> progress 0.26%, elapsed 80 s, estimated 30779 s (8 hours), iters = {MDP: 417}, opt = -7.525 +> progress 0.26%, elapsed 83 s, estimated 31957 s (8 hours), iters = {MDP: 435}, opt = -7.525 +> progress 0.26%, elapsed 86 s, estimated 33121 s (9 hours), iters = {MDP: 442}, opt = -7.525 +> progress 0.26%, elapsed 89 s, estimated 34275 s (9 hours), iters = {MDP: 457}, opt = -7.525 +> progress 0.26%, elapsed 92 s, estimated 35437 s (9 hours), iters = {MDP: 481}, opt = -7.525 +> progress 0.26%, elapsed 95 s, estimated 36603 s (10 hours), iters = {MDP: 512}, opt = -7.525 +> progress 0.26%, elapsed 98 s, estimated 37778 s (10 hours), iters = {MDP: 545}, opt = -7.525 +> progress 0.26%, elapsed 101 s, estimated 38936 s (10 hours), iters = {MDP: 586}, opt = -7.525 +> progress 0.26%, elapsed 104 s, estimated 40087 s (11 hours), iters = {MDP: 626}, opt = -7.525 +> progress 0.26%, elapsed 107 s, estimated 41254 s (11 hours), iters = {MDP: 659}, opt = -7.525 +> progress 0.261%, elapsed 110 s, estimated 42422 s (11 hours), iters = {MDP: 672}, opt = -7.525 +> progress 0.261%, elapsed 114 s, estimated 43722 s (12 hours), iters = {MDP: 680}, opt = -7.525 +> progress 0.261%, elapsed 117 s, estimated 44915 s (12 hours), iters = {MDP: 706}, opt = -7.525 +> progress 0.261%, elapsed 120 s, estimated 46166 s (12 hours), iters = {MDP: 720}, opt = -7.525 +> progress 0.261%, elapsed 123 s, estimated 47347 s (13 hours), iters = {MDP: 732}, opt = -7.525 +> progress 0.261%, elapsed 126 s, estimated 48536 s (13 hours), iters = {MDP: 750}, opt = -7.525 +> progress 0.261%, elapsed 129 s, estimated 49694 s (13 hours), iters = {MDP: 760}, opt = -7.525 +> progress 0.261%, elapsed 132 s, estimated 50851 s (14 hours), iters = {MDP: 770}, opt = -7.525 +> progress 0.261%, elapsed 135 s, estimated 52014 s (14 hours), iters = {MDP: 794}, opt = -7.525 +> progress 0.261%, elapsed 139 s, estimated 53241 s (14 hours), iters = {MDP: 812}, opt = -7.525 +> progress 0.261%, elapsed 142 s, estimated 54399 s (15 hours), iters = {MDP: 827}, opt = -7.525 +> progress 0.261%, elapsed 145 s, estimated 55586 s (15 hours), iters = {MDP: 840}, opt = -7.525 +> progress 0.265%, elapsed 148 s, estimated 55899 s (15 hours), iters = {MDP: 856}, opt = -7.525 +> progress 0.265%, elapsed 151 s, estimated 57053 s (15 hours), iters = {MDP: 888}, opt = -7.525 +> progress 0.265%, elapsed 154 s, estimated 58242 s (16 hours), iters = {MDP: 898}, opt = -7.525 +> progress 0.265%, elapsed 157 s, estimated 59359 s (16 hours), iters = {MDP: 918}, opt = -7.525 +> progress 0.265%, elapsed 160 s, estimated 60482 s (16 hours), iters = {MDP: 951}, opt = -7.525 +> progress 0.265%, elapsed 164 s, estimated 62012 s (17 hours), iters = {MDP: 968}, opt = -7.525 +> progress 0.266%, elapsed 169 s, estimated 63597 s (17 hours), iters = {MDP: 972}, opt = -7.525 +> progress 0.266%, elapsed 172 s, estimated 64904 s (18 hours), iters = {MDP: 979}, opt = -7.525 +> progress 0.266%, elapsed 176 s, estimated 66256 s (18 hours), iters = {MDP: 983}, opt = -7.525 +> progress 0.266%, elapsed 180 s, estimated 67673 s (18 hours), iters = {MDP: 988}, opt = -7.525 +> progress 0.266%, elapsed 183 s, estimated 68870 s (19 hours), iters = {MDP: 997}, opt = -7.525 +> progress 0.266%, elapsed 186 s, estimated 70033 s (19 hours), iters = {MDP: 1010}, opt = -7.525 +> progress 0.266%, elapsed 189 s, estimated 71217 s (19 hours), iters = {MDP: 1017}, opt = -7.525 +> progress 0.266%, elapsed 193 s, estimated 72446 s (20 hours), iters = {MDP: 1026}, opt = -7.525 +> progress 0.266%, elapsed 196 s, estimated 73674 s (20 hours), iters = {MDP: 1038}, opt = -7.525 +> progress 0.266%, elapsed 199 s, estimated 74842 s (20 hours), iters = {MDP: 1046}, opt = -7.525 +> progress 0.266%, elapsed 202 s, estimated 76093 s (21 hours), iters = {MDP: 1051}, opt = -7.525 +> progress 0.266%, elapsed 205 s, estimated 77279 s (21 hours), iters = {MDP: 1068}, opt = -7.525 +> progress 0.266%, elapsed 209 s, estimated 78425 s (21 hours), iters = {MDP: 1090}, opt = -7.525 +> progress 0.266%, elapsed 212 s, estimated 79523 s (22 hours), iters = {MDP: 1107}, opt = -7.525 +> progress 0.266%, elapsed 215 s, estimated 80657 s (22 hours), iters = {MDP: 1126}, opt = -7.525 +> progress 0.266%, elapsed 218 s, estimated 81831 s (22 hours), iters = {MDP: 1138}, opt = -7.525 +> progress 0.268%, elapsed 221 s, estimated 82722 s (22 hours), iters = {MDP: 1146}, opt = -7.525 +> progress 0.27%, elapsed 224 s, estimated 83312 s (23 hours), iters = {MDP: 1152}, opt = -7.525 +> progress 0.27%, elapsed 228 s, estimated 84435 s (23 hours), iters = {MDP: 1171}, opt = -7.525 +> progress 0.27%, elapsed 231 s, estimated 85611 s (23 hours), iters = {MDP: 1185}, opt = -7.525 +> progress 0.27%, elapsed 234 s, estimated 86726 s (24 hours), iters = {MDP: 1202}, opt = -7.525 +> progress 0.27%, elapsed 237 s, estimated 87848 s (24 hours), iters = {MDP: 1231}, opt = -7.525 +> progress 0.27%, elapsed 240 s, estimated 88973 s (24 hours), iters = {MDP: 1269}, opt = -7.525 +> progress 0.27%, elapsed 243 s, estimated 90288 s (25 hours), iters = {MDP: 1282}, opt = -7.525 +> progress 0.27%, elapsed 246 s, estimated 91411 s (25 hours), iters = {MDP: 1290}, opt = -7.525 +> progress 0.27%, elapsed 250 s, estimated 92626 s (25 hours), iters = {MDP: 1306}, opt = -7.525 +> progress 0.27%, elapsed 253 s, estimated 93696 s (26 hours), iters = {MDP: 1318}, opt = -7.525 +> progress 0.27%, elapsed 256 s, estimated 94927 s (26 hours), iters = {MDP: 1324}, opt = -7.525 +> progress 0.27%, elapsed 260 s, estimated 96251 s (26 hours), iters = {MDP: 1330}, opt = -7.525 +> progress 0.27%, elapsed 263 s, estimated 97456 s (27 hours), iters = {MDP: 1340}, opt = -7.525 +> progress 0.27%, elapsed 266 s, estimated 98702 s (27 hours), iters = {MDP: 1350}, opt = -7.525 +> progress 0.27%, elapsed 271 s, estimated 100227 s (27 hours), iters = {MDP: 1364}, opt = -7.525 +> progress 0.27%, elapsed 274 s, estimated 101451 s (28 hours), iters = {MDP: 1370}, opt = -7.525 +> progress 0.27%, elapsed 277 s, estimated 102586 s (28 hours), iters = {MDP: 1386}, opt = -7.525 +> progress 0.27%, elapsed 280 s, estimated 103822 s (28 hours), iters = {MDP: 1394}, opt = -7.525 +> progress 0.27%, elapsed 283 s, estimated 104932 s (29 hours), iters = {MDP: 1398}, opt = -7.525 +> progress 0.27%, elapsed 287 s, estimated 106171 s (29 hours), iters = {MDP: 1410}, opt = -7.525 +> progress 0.27%, elapsed 290 s, estimated 107428 s (29 hours), iters = {MDP: 1420}, opt = -7.525 +> progress 0.27%, elapsed 293 s, estimated 108688 s (30 hours), iters = {MDP: 1426}, opt = -7.525 +> progress 0.27%, elapsed 297 s, estimated 109837 s (30 hours), iters = {MDP: 1442}, opt = -7.525 +> progress 0.27%, elapsed 300 s, estimated 110962 s (30 hours), iters = {MDP: 1460}, opt = -7.525 +> progress 0.27%, elapsed 303 s, estimated 112105 s (31 hours), iters = {MDP: 1488}, opt = -7.525 +> progress 0.27%, elapsed 306 s, estimated 113341 s (31 hours), iters = {MDP: 1493}, opt = -7.525 +> progress 0.27%, elapsed 310 s, estimated 114639 s (31 hours), iters = {MDP: 1500}, opt = -7.525 +> progress 0.27%, elapsed 313 s, estimated 115782 s (32 hours), iters = {MDP: 1536}, opt = -7.525 +> progress 0.27%, elapsed 316 s, estimated 116900 s (32 hours), iters = {MDP: 1553}, opt = -7.525 +> progress 0.27%, elapsed 319 s, estimated 118050 s (32 hours), iters = {MDP: 1578}, opt = -7.525 +> progress 0.27%, elapsed 322 s, estimated 119171 s (33 hours), iters = {MDP: 1613}, opt = -7.525 +> progress 0.27%, elapsed 325 s, estimated 120325 s (33 hours), iters = {MDP: 1634}, opt = -7.525 +> progress 0.27%, elapsed 328 s, estimated 121512 s (33 hours), iters = {MDP: 1660}, opt = -7.525 +> progress 0.27%, elapsed 331 s, estimated 122628 s (34 hours), iters = {MDP: 1695}, opt = -7.525 +> progress 0.27%, elapsed 334 s, estimated 123769 s (34 hours), iters = {MDP: 1716}, opt = -7.525 +> progress 0.27%, elapsed 337 s, estimated 124926 s (34 hours), iters = {MDP: 1743}, opt = -7.525 +> progress 0.27%, elapsed 340 s, estimated 126050 s (35 hours), iters = {MDP: 1771}, opt = -7.525 +> progress 0.27%, elapsed 344 s, estimated 127221 s (35 hours), iters = {MDP: 1805}, opt = -7.525 +> progress 0.27%, elapsed 347 s, estimated 128394 s (35 hours), iters = {MDP: 1826}, opt = -7.525 +> progress 0.27%, elapsed 350 s, estimated 129505 s (35 hours), iters = {MDP: 1852}, opt = -7.525 +> progress 0.27%, elapsed 353 s, estimated 130547 s (36 hours), iters = {MDP: 1887}, opt = -7.525 +> progress 0.27%, elapsed 356 s, estimated 131671 s (36 hours), iters = {MDP: 1899}, opt = -7.525 +> progress 0.27%, elapsed 359 s, estimated 132818 s (36 hours), iters = {MDP: 1913}, opt = -7.525 +> progress 0.27%, elapsed 363 s, estimated 134011 s (37 hours), iters = {MDP: 1936}, opt = -7.525 +> progress 0.27%, elapsed 366 s, estimated 135136 s (37 hours), iters = {MDP: 1945}, opt = -7.525 +> progress 0.27%, elapsed 369 s, estimated 136262 s (37 hours), iters = {MDP: 1973}, opt = -7.525 +> progress 0.27%, elapsed 372 s, estimated 137373 s (38 hours), iters = {MDP: 1987}, opt = -7.525 +> progress 0.27%, elapsed 375 s, estimated 138498 s (38 hours), iters = {MDP: 1999}, opt = -7.525 +> progress 0.27%, elapsed 378 s, estimated 139828 s (38 hours), iters = {MDP: 2025}, opt = -7.525 +> progress 0.27%, elapsed 381 s, estimated 140963 s (39 hours), iters = {MDP: 2035}, opt = -7.525 +> progress 0.27%, elapsed 385 s, estimated 142209 s (39 hours), iters = {MDP: 2052}, opt = -7.525 +> progress 0.27%, elapsed 388 s, estimated 143358 s (39 hours), iters = {MDP: 2069}, opt = -7.525 +> progress 0.27%, elapsed 391 s, estimated 144497 s (40 hours), iters = {MDP: 2080}, opt = -7.525 +> progress 0.27%, elapsed 394 s, estimated 145657 s (40 hours), iters = {MDP: 2098}, opt = -7.525 +> progress 0.27%, elapsed 397 s, estimated 146841 s (40 hours), iters = {MDP: 2109}, opt = -7.525 +> progress 0.27%, elapsed 400 s, estimated 147961 s (41 hours), iters = {MDP: 2123}, opt = -7.525 +> progress 0.27%, elapsed 404 s, estimated 149126 s (41 hours), iters = {MDP: 2133}, opt = -7.525 +> progress 0.27%, elapsed 407 s, estimated 150237 s (41 hours), iters = {MDP: 2142}, opt = -7.525 +> progress 0.27%, elapsed 410 s, estimated 151397 s (42 hours), iters = {MDP: 2151}, opt = -7.525 +> progress 0.27%, elapsed 413 s, estimated 152610 s (42 hours), iters = {MDP: 2161}, opt = -7.525 +> progress 0.52%, elapsed 417 s, estimated 80189 s (22 hours), iters = {MDP: 2173}, opt = -7.525 +> progress 0.564%, elapsed 420 s, estimated 74555 s (20 hours), iters = {MDP: 2176}, opt = -7.525 +> progress 0.567%, elapsed 432 s, estimated 76141 s (21 hours), iters = {MDP: 2178}, opt = -7.525 +> progress 0.567%, elapsed 442 s, estimated 77991 s (21 hours), iters = {MDP: 2179}, opt = -7.525 +> progress 0.567%, elapsed 451 s, estimated 79552 s (22 hours), iters = {MDP: 2180}, opt = -7.525 +> progress 0.568%, elapsed 456 s, estimated 80431 s (22 hours), iters = {MDP: 2181}, opt = -7.525 +> progress 0.568%, elapsed 462 s, estimated 81383 s (22 hours), iters = {MDP: 2182}, opt = -7.525 +> progress 0.568%, elapsed 466 s, estimated 82067 s (22 hours), iters = {MDP: 2183}, opt = -7.525 +> progress 0.568%, elapsed 469 s, estimated 82654 s (22 hours), iters = {MDP: 2184}, opt = -7.525 +> progress 0.568%, elapsed 474 s, estimated 83570 s (23 hours), iters = {MDP: 2186}, opt = -7.525 +> progress 0.568%, elapsed 477 s, estimated 84100 s (23 hours), iters = {MDP: 2205}, opt = -7.525 +> progress 0.568%, elapsed 480 s, estimated 84639 s (23 hours), iters = {MDP: 2218}, opt = -7.525 +> progress 0.568%, elapsed 484 s, estimated 85289 s (23 hours), iters = {MDP: 2228}, opt = -7.525 +> progress 0.568%, elapsed 488 s, estimated 85963 s (23 hours), iters = {MDP: 2232}, opt = -7.525 +> progress 0.568%, elapsed 492 s, estimated 86624 s (24 hours), iters = {MDP: 2234}, opt = -7.525 +> progress 0.568%, elapsed 495 s, estimated 87157 s (24 hours), iters = {MDP: 2254}, opt = -7.525 +> progress 0.568%, elapsed 498 s, estimated 87737 s (24 hours), iters = {MDP: 2258}, opt = -7.525 +> progress 0.568%, elapsed 502 s, estimated 88487 s (24 hours), iters = {MDP: 2260}, opt = -7.525 +> progress 0.568%, elapsed 505 s, estimated 89022 s (24 hours), iters = {MDP: 2271}, opt = -7.525 +> progress 0.568%, elapsed 509 s, estimated 89756 s (24 hours), iters = {MDP: 2285}, opt = -7.525 +> progress 0.568%, elapsed 514 s, estimated 90598 s (25 hours), iters = {MDP: 2287}, opt = -7.525 +> progress 0.568%, elapsed 518 s, estimated 91271 s (25 hours), iters = {MDP: 2290}, opt = -7.525 +> progress 0.568%, elapsed 521 s, estimated 91809 s (25 hours), iters = {MDP: 2303}, opt = -7.525 +> progress 0.568%, elapsed 525 s, estimated 92542 s (25 hours), iters = {MDP: 2311}, opt = -7.525 +> progress 0.568%, elapsed 529 s, estimated 93144 s (25 hours), iters = {MDP: 2313}, opt = -7.525 +> progress 0.568%, elapsed 532 s, estimated 93782 s (26 hours), iters = {MDP: 2315}, opt = -7.525 +> progress 0.568%, elapsed 535 s, estimated 94328 s (26 hours), iters = {MDP: 2327}, opt = -7.525 +> progress 0.568%, elapsed 540 s, estimated 95168 s (26 hours), iters = {MDP: 2339}, opt = -7.525 +> progress 0.568%, elapsed 545 s, estimated 95924 s (26 hours), iters = {MDP: 2343}, opt = -7.525 +> progress 0.568%, elapsed 550 s, estimated 96854 s (26 hours), iters = {MDP: 2345}, opt = -7.525 +> progress 0.568%, elapsed 554 s, estimated 97533 s (27 hours), iters = {MDP: 2365}, opt = -7.525 +> progress 0.568%, elapsed 557 s, estimated 98084 s (27 hours), iters = {MDP: 2367}, opt = -7.525 +> progress 0.568%, elapsed 562 s, estimated 99058 s (27 hours), iters = {MDP: 2369}, opt = -7.525 +> progress 0.568%, elapsed 566 s, estimated 99779 s (27 hours), iters = {MDP: 2371}, opt = -7.525 +> progress 0.568%, elapsed 569 s, estimated 100313 s (27 hours), iters = {MDP: 2406}, opt = -7.525 +> progress 0.568%, elapsed 573 s, estimated 100852 s (28 hours), iters = {MDP: 2429}, opt = -7.525 +> progress 0.568%, elapsed 576 s, estimated 101393 s (28 hours), iters = {MDP: 2435}, opt = -7.525 +> progress 0.568%, elapsed 579 s, estimated 101930 s (28 hours), iters = {MDP: 2448}, opt = -7.525 +> progress 0.568%, elapsed 582 s, estimated 102558 s (28 hours), iters = {MDP: 2454}, opt = -7.525 +> progress 0.568%, elapsed 589 s, estimated 103691 s (28 hours), iters = {MDP: 2457}, opt = -7.525 +> progress 0.568%, elapsed 592 s, estimated 104230 s (28 hours), iters = {MDP: 2458}, opt = -7.525 +> progress 0.568%, elapsed 595 s, estimated 104760 s (29 hours), iters = {MDP: 2493}, opt = -7.525 +> progress 0.568%, elapsed 599 s, estimated 105528 s (29 hours), iters = {MDP: 2530}, opt = -7.525 +> progress 0.568%, elapsed 603 s, estimated 106255 s (29 hours), iters = {MDP: 2533}, opt = -7.525 +> progress 0.568%, elapsed 608 s, estimated 106987 s (29 hours), iters = {MDP: 2534}, opt = -7.525 +> progress 0.568%, elapsed 612 s, estimated 107740 s (29 hours), iters = {MDP: 2535}, opt = -7.525 +> progress 0.568%, elapsed 620 s, estimated 109123 s (30 hours), iters = {MDP: 2536}, opt = -7.525 +> progress 0.568%, elapsed 627 s, estimated 110440 s (30 hours), iters = {MDP: 2537}, opt = -7.525 +> progress 0.568%, elapsed 633 s, estimated 111380 s (30 hours), iters = {MDP: 2538}, opt = -7.525 +> progress 0.568%, elapsed 639 s, estimated 112433 s (31 hours), iters = {MDP: 2539}, opt = -7.525 +> progress 0.568%, elapsed 644 s, estimated 113312 s (31 hours), iters = {MDP: 2540}, opt = -7.525 +> progress 0.568%, elapsed 648 s, estimated 114068 s (31 hours), iters = {MDP: 2541}, opt = -7.525 +> progress 0.568%, elapsed 651 s, estimated 114627 s (31 hours), iters = {MDP: 2544}, opt = -7.525 +> progress 0.568%, elapsed 655 s, estimated 115243 s (32 hours), iters = {MDP: 2553}, opt = -7.525 +> progress 0.568%, elapsed 658 s, estimated 115797 s (32 hours), iters = {MDP: 2567}, opt = -7.525 +> progress 0.568%, elapsed 661 s, estimated 116380 s (32 hours), iters = {MDP: 2578}, opt = -7.525 +> progress 0.568%, elapsed 665 s, estimated 117023 s (32 hours), iters = {MDP: 2590}, opt = -7.525 +> progress 0.568%, elapsed 668 s, estimated 117553 s (32 hours), iters = {MDP: 2599}, opt = -7.525 +> progress 0.568%, elapsed 671 s, estimated 118084 s (32 hours), iters = {MDP: 2606}, opt = -7.525 +> progress 0.568%, elapsed 674 s, estimated 118639 s (32 hours), iters = {MDP: 2612}, opt = -7.525 +> progress 0.568%, elapsed 677 s, estimated 119189 s (33 hours), iters = {MDP: 2630}, opt = -7.525 +> progress 0.568%, elapsed 681 s, estimated 119848 s (33 hours), iters = {MDP: 2646}, opt = -7.525 +> progress 0.568%, elapsed 684 s, estimated 120390 s (33 hours), iters = {MDP: 2654}, opt = -7.525 +> progress 0.568%, elapsed 687 s, estimated 120922 s (33 hours), iters = {MDP: 2663}, opt = -7.525 +> progress 0.568%, elapsed 690 s, estimated 121499 s (33 hours), iters = {MDP: 2678}, opt = -7.525 +> progress 0.568%, elapsed 694 s, estimated 122102 s (33 hours), iters = {MDP: 2683}, opt = -7.525 +> progress 0.568%, elapsed 698 s, estimated 122895 s (34 hours), iters = {MDP: 2690}, opt = -7.525 +> progress 0.568%, elapsed 703 s, estimated 123836 s (34 hours), iters = {MDP: 2693}, opt = -7.525 +> progress 0.568%, elapsed 708 s, estimated 124655 s (34 hours), iters = {MDP: 2694}, opt = -7.525 +> progress 0.568%, elapsed 712 s, estimated 125359 s (34 hours), iters = {MDP: 2695}, opt = -7.525 +> progress 0.568%, elapsed 715 s, estimated 125895 s (34 hours), iters = {MDP: 2699}, opt = -7.525 +> progress 0.568%, elapsed 719 s, estimated 126501 s (35 hours), iters = {MDP: 2707}, opt = -7.525 +> progress 0.568%, elapsed 722 s, estimated 127093 s (35 hours), iters = {MDP: 2721}, opt = -7.525 +> progress 0.568%, elapsed 725 s, estimated 127671 s (35 hours), iters = {MDP: 2732}, opt = -7.525 +> progress 0.568%, elapsed 729 s, estimated 128262 s (35 hours), iters = {MDP: 2744}, opt = -7.525 +> progress 0.568%, elapsed 732 s, estimated 128885 s (35 hours), iters = {MDP: 2754}, opt = -7.525 +> progress 0.568%, elapsed 736 s, estimated 129579 s (35 hours), iters = {MDP: 2762}, opt = -7.525 +> progress 0.568%, elapsed 739 s, estimated 130115 s (36 hours), iters = {MDP: 2779}, opt = -7.525 +> progress 0.568%, elapsed 742 s, estimated 130656 s (36 hours), iters = {MDP: 2793}, opt = -7.525 +> progress 0.568%, elapsed 746 s, estimated 131345 s (36 hours), iters = {MDP: 2807}, opt = -7.525 +> progress 0.568%, elapsed 750 s, estimated 131944 s (36 hours), iters = {MDP: 2815}, opt = -7.525 +> progress 0.568%, elapsed 753 s, estimated 132594 s (36 hours), iters = {MDP: 2832}, opt = -7.525 +> progress 0.568%, elapsed 757 s, estimated 133189 s (36 hours), iters = {MDP: 2837}, opt = -7.525 +> progress 0.568%, elapsed 761 s, estimated 133976 s (37 hours), iters = {MDP: 2844}, opt = -7.525 +> progress 0.568%, elapsed 766 s, estimated 134882 s (37 hours), iters = {MDP: 2847}, opt = -7.525 +> progress 0.568%, elapsed 771 s, estimated 135708 s (37 hours), iters = {MDP: 2848}, opt = -7.525 +> progress 0.568%, elapsed 775 s, estimated 136410 s (37 hours), iters = {MDP: 2849}, opt = -7.525 +> progress 0.568%, elapsed 778 s, estimated 136942 s (38 hours), iters = {MDP: 2854}, opt = -7.525 +> progress 0.568%, elapsed 781 s, estimated 137546 s (38 hours), iters = {MDP: 2861}, opt = -7.525 +> progress 0.568%, elapsed 785 s, estimated 138139 s (38 hours), iters = {MDP: 2875}, opt = -7.525 +> progress 0.568%, elapsed 788 s, estimated 138714 s (38 hours), iters = {MDP: 2886}, opt = -7.525 +> progress 0.568%, elapsed 791 s, estimated 139292 s (38 hours), iters = {MDP: 2898}, opt = -7.525 +> progress 0.568%, elapsed 795 s, estimated 139904 s (38 hours), iters = {MDP: 2908}, opt = -7.525 +> progress 0.568%, elapsed 799 s, estimated 140585 s (39 hours), iters = {MDP: 2916}, opt = -7.525 +> progress 0.568%, elapsed 802 s, estimated 141123 s (39 hours), iters = {MDP: 2933}, opt = -7.525 +> progress 0.568%, elapsed 805 s, estimated 141703 s (39 hours), iters = {MDP: 2947}, opt = -7.525 +> progress 0.568%, elapsed 808 s, estimated 142236 s (39 hours), iters = {MDP: 2959}, opt = -7.525 +> progress 0.568%, elapsed 811 s, estimated 142823 s (39 hours), iters = {MDP: 2964}, opt = -7.525 +> progress 0.568%, elapsed 815 s, estimated 143404 s (39 hours), iters = {MDP: 2978}, opt = -7.525 +> progress 0.568%, elapsed 818 s, estimated 144004 s (40 hours), iters = {MDP: 2988}, opt = -7.525 +> progress 0.568%, elapsed 822 s, estimated 144628 s (40 hours), iters = {MDP: 2993}, opt = -7.525 +> progress 0.568%, elapsed 825 s, estimated 145239 s (40 hours), iters = {MDP: 2998}, opt = -7.525 +> progress 0.568%, elapsed 831 s, estimated 146329 s (40 hours), iters = {MDP: 3000}, opt = -7.525 +> progress 0.568%, elapsed 835 s, estimated 147054 s (40 hours), iters = {MDP: 3001}, opt = -7.525 +> progress 0.568%, elapsed 839 s, estimated 147749 s (41 hours), iters = {MDP: 3002}, opt = -7.525 +> progress 0.568%, elapsed 842 s, estimated 148278 s (41 hours), iters = {MDP: 3017}, opt = -7.525 +> progress 0.568%, elapsed 845 s, estimated 148806 s (41 hours), iters = {MDP: 3036}, opt = -7.525 +> progress 0.568%, elapsed 849 s, estimated 149386 s (41 hours), iters = {MDP: 3048}, opt = -7.525 +> progress 0.568%, elapsed 852 s, estimated 149944 s (41 hours), iters = {MDP: 3057}, opt = -7.525 +> progress 0.568%, elapsed 855 s, estimated 150499 s (41 hours), iters = {MDP: 3066}, opt = -7.525 +> progress 0.568%, elapsed 858 s, estimated 151062 s (41 hours), iters = {MDP: 3075}, opt = -7.525 +> progress 0.568%, elapsed 861 s, estimated 151597 s (42 hours), iters = {MDP: 3094}, opt = -7.525 +> progress 0.568%, elapsed 867 s, estimated 152590 s (42 hours), iters = {MDP: 3110}, opt = -7.525 +> progress 0.568%, elapsed 870 s, estimated 153120 s (42 hours), iters = {MDP: 3111}, opt = -7.525 +> progress 0.568%, elapsed 875 s, estimated 154007 s (42 hours), iters = {MDP: 3116}, opt = -7.525 +> progress 0.568%, elapsed 878 s, estimated 154555 s (42 hours), iters = {MDP: 3117}, opt = -7.525 +> progress 0.568%, elapsed 881 s, estimated 155086 s (43 hours), iters = {MDP: 3120}, opt = -7.525 +> progress 0.568%, elapsed 886 s, estimated 155987 s (43 hours), iters = {MDP: 3122}, opt = -7.525 +> progress 0.568%, elapsed 890 s, estimated 156695 s (43 hours), iters = {MDP: 3123}, opt = -7.525 +> progress 0.568%, elapsed 893 s, estimated 157242 s (43 hours), iters = {MDP: 3126}, opt = -7.525 +> progress 0.568%, elapsed 897 s, estimated 157784 s (43 hours), iters = {MDP: 3134}, opt = -7.525 +> progress 0.568%, elapsed 900 s, estimated 158329 s (43 hours), iters = {MDP: 3145}, opt = -7.525 +> progress 0.568%, elapsed 903 s, estimated 158883 s (44 hours), iters = {MDP: 3156}, opt = -7.525 +> progress 0.568%, elapsed 906 s, estimated 159445 s (44 hours), iters = {MDP: 3170}, opt = -7.525 +> progress 0.568%, elapsed 909 s, estimated 160054 s (44 hours), iters = {MDP: 3179}, opt = -7.525 +> progress 0.568%, elapsed 914 s, estimated 160790 s (44 hours), iters = {MDP: 3187}, opt = -7.525 +> progress 0.568%, elapsed 917 s, estimated 161346 s (44 hours), iters = {MDP: 3191}, opt = -7.525 +> progress 0.568%, elapsed 920 s, estimated 161897 s (44 hours), iters = {MDP: 3210}, opt = -7.525 +> progress 0.568%, elapsed 923 s, estimated 162481 s (45 hours), iters = {MDP: 3222}, opt = -7.525 +> progress 0.568%, elapsed 927 s, estimated 163092 s (45 hours), iters = {MDP: 3235}, opt = -7.525 +> progress 0.568%, elapsed 930 s, estimated 163646 s (45 hours), iters = {MDP: 3242}, opt = -7.525 +> progress 0.568%, elapsed 933 s, estimated 164190 s (45 hours), iters = {MDP: 3256}, opt = -7.525 +> progress 0.568%, elapsed 937 s, estimated 164842 s (45 hours), iters = {MDP: 3264}, opt = -7.525 +> progress 0.568%, elapsed 940 s, estimated 165481 s (45 hours), iters = {MDP: 3269}, opt = -7.525 +> progress 0.568%, elapsed 943 s, estimated 166030 s (46 hours), iters = {MDP: 3274}, opt = -7.525 +> progress 0.568%, elapsed 948 s, estimated 166753 s (46 hours), iters = {MDP: 3275}, opt = -7.525 +> progress 0.568%, elapsed 953 s, estimated 167730 s (46 hours), iters = {MDP: 3276}, opt = -7.525 +> progress 0.568%, elapsed 958 s, estimated 168653 s (46 hours), iters = {MDP: 3277}, opt = -7.525 +> progress 0.568%, elapsed 964 s, estimated 169587 s (47 hours), iters = {MDP: 3278}, opt = -7.525 +> progress 0.568%, elapsed 968 s, estimated 170291 s (47 hours), iters = {MDP: 3279}, opt = -7.525 +> progress 0.568%, elapsed 971 s, estimated 170875 s (47 hours), iters = {MDP: 3280}, opt = -7.525 +> progress 0.568%, elapsed 975 s, estimated 171536 s (47 hours), iters = {MDP: 3282}, opt = -7.525 +> progress 0.568%, elapsed 978 s, estimated 172078 s (47 hours), iters = {MDP: 3289}, opt = -7.525 +> progress 0.568%, elapsed 981 s, estimated 172637 s (47 hours), iters = {MDP: 3302}, opt = -7.525 +> progress 0.568%, elapsed 984 s, estimated 173226 s (2 days), iters = {MDP: 3311}, opt = -7.525 +> progress 0.568%, elapsed 988 s, estimated 173796 s (2 days), iters = {MDP: 3316}, opt = -7.525 +> progress 0.568%, elapsed 991 s, estimated 174396 s (2 days), iters = {MDP: 3324}, opt = -7.525 +> progress 0.568%, elapsed 995 s, estimated 175087 s (2 days), iters = {MDP: 3326}, opt = -7.525 +> progress 0.568%, elapsed 998 s, estimated 175699 s (2 days), iters = {MDP: 3328}, opt = -7.525 +> progress 0.568%, elapsed 1002 s, estimated 176368 s (2 days), iters = {MDP: 3330}, opt = -7.525 +> progress 0.568%, elapsed 1005 s, estimated 176903 s (2 days), iters = {MDP: 3337}, opt = -7.525 +> progress 0.568%, elapsed 1008 s, estimated 177454 s (2 days), iters = {MDP: 3350}, opt = -7.525 +> progress 0.568%, elapsed 1012 s, estimated 178054 s (2 days), iters = {MDP: 3359}, opt = -7.525 +> progress 0.568%, elapsed 1015 s, estimated 178599 s (2 days), iters = {MDP: 3364}, opt = -7.525 +> progress 0.568%, elapsed 1018 s, estimated 179181 s (2 days), iters = {MDP: 3372}, opt = -7.525 +> progress 0.568%, elapsed 1022 s, estimated 179887 s (2 days), iters = {MDP: 3375}, opt = -7.525 +> progress 0.568%, elapsed 1026 s, estimated 180521 s (2 days), iters = {MDP: 3376}, opt = -7.525 +> progress 0.568%, elapsed 1029 s, estimated 181053 s (2 days), iters = {MDP: 3377}, opt = -7.525 +> progress 0.568%, elapsed 1035 s, estimated 182049 s (2 days), iters = {MDP: 3382}, opt = -7.525 +> progress 0.568%, elapsed 1038 s, estimated 182676 s (2 days), iters = {MDP: 3383}, opt = -7.525 +> progress 0.568%, elapsed 1042 s, estimated 183388 s (2 days), iters = {MDP: 3384}, opt = -7.525 +> progress 0.568%, elapsed 1048 s, estimated 184321 s (2 days), iters = {MDP: 3385}, opt = -7.525 +> progress 0.568%, elapsed 1052 s, estimated 185013 s (2 days), iters = {MDP: 3386}, opt = -7.525 +> progress 0.568%, elapsed 1055 s, estimated 185623 s (2 days), iters = {MDP: 3387}, opt = -7.525 +> progress 0.568%, elapsed 1059 s, estimated 186255 s (2 days), iters = {MDP: 3389}, opt = -7.525 +> progress 0.568%, elapsed 1062 s, estimated 186836 s (2 days), iters = {MDP: 3397}, opt = -7.525 +> progress 0.568%, elapsed 1065 s, estimated 187388 s (2 days), iters = {MDP: 3410}, opt = -7.525 +> progress 0.568%, elapsed 1068 s, estimated 187939 s (2 days), iters = {MDP: 3419}, opt = -7.525 +> progress 0.568%, elapsed 1071 s, estimated 188499 s (2 days), iters = {MDP: 3426}, opt = -7.525 +> progress 0.568%, elapsed 1075 s, estimated 189133 s (2 days), iters = {MDP: 3432}, opt = -7.525 +> progress 0.568%, elapsed 1081 s, estimated 190209 s (2 days), iters = {MDP: 3435}, opt = -7.525 +> progress 0.568%, elapsed 1085 s, estimated 190903 s (2 days), iters = {MDP: 3437}, opt = -7.525 +> progress 0.568%, elapsed 1088 s, estimated 191492 s (2 days), iters = {MDP: 3445}, opt = -7.525 +> progress 0.568%, elapsed 1091 s, estimated 192024 s (2 days), iters = {MDP: 3458}, opt = -7.525 +> progress 0.568%, elapsed 1095 s, estimated 192576 s (2 days), iters = {MDP: 3466}, opt = -7.525 +> progress 0.568%, elapsed 1098 s, estimated 193124 s (2 days), iters = {MDP: 3472}, opt = -7.525 +> progress 0.568%, elapsed 1102 s, estimated 193812 s (2 days), iters = {MDP: 3480}, opt = -7.525 +> progress 0.568%, elapsed 1108 s, estimated 194945 s (2 days), iters = {MDP: 3483}, opt = -7.525 +> progress 0.568%, elapsed 1111 s, estimated 195505 s (2 days), iters = {MDP: 3484}, opt = -7.525 +> progress 0.568%, elapsed 1117 s, estimated 196504 s (2 days), iters = {MDP: 3489}, opt = -7.525 +> progress 0.568%, elapsed 1121 s, estimated 197138 s (2 days), iters = {MDP: 3490}, opt = -7.525 +> progress 0.568%, elapsed 1125 s, estimated 197846 s (2 days), iters = {MDP: 3491}, opt = -7.525 +> progress 0.569%, elapsed 1130 s, estimated 198678 s (2 days), iters = {MDP: 3492}, opt = -7.525 +> progress 0.569%, elapsed 1139 s, estimated 200301 s (2 days), iters = {MDP: 3493}, opt = -7.525 +> progress 0.569%, elapsed 1146 s, estimated 201539 s (2 days), iters = {MDP: 3494}, opt = -7.525 +> progress 0.569%, elapsed 1151 s, estimated 202301 s (2 days), iters = {MDP: 3495}, opt = -7.525 +> progress 0.569%, elapsed 1154 s, estimated 202832 s (2 days), iters = {MDP: 3497}, opt = -7.525 +> progress 0.569%, elapsed 1157 s, estimated 203359 s (2 days), iters = {MDP: 3518}, opt = -7.525 +> progress 0.569%, elapsed 1160 s, estimated 203913 s (2 days), iters = {MDP: 3548}, opt = -7.525 +> progress 0.569%, elapsed 1164 s, estimated 204585 s (2 days), iters = {MDP: 3562}, opt = -7.525 +> progress 0.569%, elapsed 1167 s, estimated 205206 s (2 days), iters = {MDP: 3576}, opt = -7.525 +> progress 0.569%, elapsed 1172 s, estimated 206103 s (2 days), iters = {MDP: 3579}, opt = -7.525 +> progress 0.569%, elapsed 1177 s, estimated 206813 s (2 days), iters = {MDP: 3581}, opt = -7.525 +> progress 0.569%, elapsed 1180 s, estimated 207396 s (2 days), iters = {MDP: 3587}, opt = -7.525 +> progress 0.569%, elapsed 1183 s, estimated 208006 s (2 days), iters = {MDP: 3594}, opt = -7.525 +> progress 0.569%, elapsed 1186 s, estimated 208545 s (2 days), iters = {MDP: 3609}, opt = -7.525 +> progress 0.569%, elapsed 1189 s, estimated 209081 s (2 days), iters = {MDP: 3621}, opt = -7.525 +> progress 0.569%, elapsed 1193 s, estimated 209633 s (2 days), iters = {MDP: 3630}, opt = -7.525 +> progress 0.569%, elapsed 1196 s, estimated 210170 s (2 days), iters = {MDP: 3639}, opt = -7.525 +> progress 0.569%, elapsed 1200 s, estimated 210875 s (2 days), iters = {MDP: 3647}, opt = -7.525 +> progress 0.569%, elapsed 1203 s, estimated 211433 s (2 days), iters = {MDP: 3664}, opt = -7.525 +> progress 0.569%, elapsed 1206 s, estimated 212003 s (2 days), iters = {MDP: 3678}, opt = -7.525 +> progress 0.569%, elapsed 1210 s, estimated 212692 s (2 days), iters = {MDP: 3692}, opt = -7.525 +> progress 0.569%, elapsed 1213 s, estimated 213248 s (2 days), iters = {MDP: 3699}, opt = -7.525 +> progress 0.569%, elapsed 1217 s, estimated 213841 s (2 days), iters = {MDP: 3714}, opt = -7.525 +> progress 0.569%, elapsed 1220 s, estimated 214408 s (2 days), iters = {MDP: 3721}, opt = -7.525 +> progress 0.569%, elapsed 1223 s, estimated 215035 s (2 days), iters = {MDP: 3726}, opt = -7.525 +> progress 0.569%, elapsed 1226 s, estimated 215590 s (2 days), iters = {MDP: 3733}, opt = -7.525 +> progress 0.569%, elapsed 1230 s, estimated 216173 s (2 days), iters = {MDP: 3741}, opt = -7.525 +> progress 0.569%, elapsed 1233 s, estimated 216743 s (2 days), iters = {MDP: 3754}, opt = -7.525 +> progress 0.569%, elapsed 1236 s, estimated 217292 s (2 days), iters = {MDP: 3763}, opt = -7.525 +> progress 0.569%, elapsed 1239 s, estimated 217853 s (2 days), iters = {MDP: 3770}, opt = -7.525 +> progress 0.569%, elapsed 1243 s, estimated 218543 s (2 days), iters = {MDP: 3775}, opt = -7.525 +> progress 0.569%, elapsed 1248 s, estimated 219347 s (2 days), iters = {MDP: 3777}, opt = -7.525 +> progress 0.569%, elapsed 1253 s, estimated 220200 s (2 days), iters = {MDP: 3778}, opt = -7.525 +> progress 0.569%, elapsed 1257 s, estimated 220897 s (2 days), iters = {MDP: 3779}, opt = -7.525 +> progress 0.569%, elapsed 1261 s, estimated 221608 s (2 days), iters = {MDP: 3780}, opt = -7.525 +> progress 0.569%, elapsed 1265 s, estimated 222343 s (2 days), iters = {MDP: 3781}, opt = -7.525 +> progress 0.569%, elapsed 1269 s, estimated 223059 s (2 days), iters = {MDP: 3782}, opt = -7.525 +> progress 0.569%, elapsed 1273 s, estimated 223668 s (2 days), iters = {MDP: 3786}, opt = -7.525 +> progress 0.569%, elapsed 1278 s, estimated 224445 s (2 days), iters = {MDP: 3794}, opt = -7.525 +> progress 0.57%, elapsed 1288 s, estimated 225972 s (2 days), iters = {MDP: 3797}, opt = -7.525 +> progress 0.57%, elapsed 1295 s, estimated 227245 s (2 days), iters = {MDP: 3798}, opt = -7.525 +> progress 0.57%, elapsed 1300 s, estimated 227974 s (2 days), iters = {MDP: 3799}, opt = -7.525 +> progress 0.57%, elapsed 1303 s, estimated 228644 s (2 days), iters = {MDP: 3802}, opt = -7.525 +> progress 0.57%, elapsed 1307 s, estimated 229180 s (2 days), iters = {MDP: 3837}, opt = -7.525 +> progress 0.57%, elapsed 1310 s, estimated 229826 s (2 days), iters = {MDP: 3861}, opt = -7.525 +> progress 0.57%, elapsed 1314 s, estimated 230412 s (2 days), iters = {MDP: 3868}, opt = -7.525 +> progress 0.57%, elapsed 1317 s, estimated 231048 s (2 days), iters = {MDP: 3881}, opt = -7.525 +> progress 0.57%, elapsed 1320 s, estimated 231600 s (2 days), iters = {MDP: 3883}, opt = -7.525 +> progress 0.57%, elapsed 1324 s, estimated 232259 s (2 days), iters = {MDP: 3885}, opt = -7.525 +> progress 0.57%, elapsed 1327 s, estimated 232804 s (2 days), iters = {MDP: 3887}, opt = -7.525 +> progress 0.57%, elapsed 1331 s, estimated 233421 s (2 days), iters = {MDP: 3893}, opt = -7.525 +> progress 0.57%, elapsed 1334 s, estimated 234053 s (2 days), iters = {MDP: 3900}, opt = -7.525 +> progress 0.57%, elapsed 1338 s, estimated 234594 s (2 days), iters = {MDP: 3915}, opt = -7.525 +> progress 0.57%, elapsed 1341 s, estimated 235158 s (2 days), iters = {MDP: 3928}, opt = -7.525 +> progress 0.57%, elapsed 1344 s, estimated 235688 s (2 days), iters = {MDP: 3936}, opt = -7.525 +> progress 0.57%, elapsed 1347 s, estimated 236285 s (2 days), iters = {MDP: 3946}, opt = -7.525 +> progress 0.57%, elapsed 1351 s, estimated 236932 s (2 days), iters = {MDP: 3953}, opt = -7.525 +> progress 0.57%, elapsed 1354 s, estimated 237472 s (2 days), iters = {MDP: 3969}, opt = -7.525 +> progress 0.57%, elapsed 1357 s, estimated 238088 s (2 days), iters = {MDP: 3984}, opt = -7.525 +> progress 0.57%, elapsed 1361 s, estimated 238776 s (2 days), iters = {MDP: 3998}, opt = -7.525 +> progress 0.57%, elapsed 1364 s, estimated 239325 s (2 days), iters = {MDP: 4005}, opt = -7.525 +> progress 0.57%, elapsed 1368 s, estimated 239852 s (2 days), iters = {MDP: 4019}, opt = -7.525 +> progress 0.57%, elapsed 1371 s, estimated 240500 s (2 days), iters = {MDP: 4027}, opt = -7.525 +> progress 0.57%, elapsed 1375 s, estimated 241129 s (2 days), iters = {MDP: 4032}, opt = -7.525 +> progress 0.57%, elapsed 1378 s, estimated 241671 s (2 days), iters = {MDP: 4040}, opt = -7.525 +> progress 0.57%, elapsed 1381 s, estimated 242226 s (2 days), iters = {MDP: 4053}, opt = -7.525 +> progress 0.57%, elapsed 1384 s, estimated 242800 s (2 days), iters = {MDP: 4058}, opt = -7.525 +> progress 0.57%, elapsed 1388 s, estimated 243376 s (2 days), iters = {MDP: 4066}, opt = -7.525 +> progress 0.57%, elapsed 1391 s, estimated 243988 s (2 days), iters = {MDP: 4075}, opt = -7.525 +> progress 0.57%, elapsed 1394 s, estimated 244554 s (2 days), iters = {MDP: 4082}, opt = -7.525 +> progress 0.57%, elapsed 1398 s, estimated 245131 s (2 days), iters = {MDP: 4096}, opt = -7.525 +> progress 0.57%, elapsed 1401 s, estimated 245695 s (2 days), iters = {MDP: 4103}, opt = -7.525 +> progress 0.57%, elapsed 1404 s, estimated 246300 s (2 days), iters = {MDP: 4111}, opt = -7.525 +> progress 0.57%, elapsed 1408 s, estimated 246978 s (2 days), iters = {MDP: 4119}, opt = -7.525 +> progress 0.57%, elapsed 1414 s, estimated 247993 s (2 days), iters = {MDP: 4121}, opt = -7.525 +> progress 0.57%, elapsed 1418 s, estimated 248640 s (2 days), iters = {MDP: 4122}, opt = -7.525 +> progress 0.57%, elapsed 1421 s, estimated 249241 s (2 days), iters = {MDP: 4123}, opt = -7.525 +> progress 0.57%, elapsed 1425 s, estimated 249858 s (2 days), iters = {MDP: 4124}, opt = -7.525 +> progress 0.57%, elapsed 1428 s, estimated 250472 s (2 days), iters = {MDP: 4125}, opt = -7.525 +> progress 0.57%, elapsed 1432 s, estimated 251017 s (2 days), iters = {MDP: 4132}, opt = -7.525 +> progress 0.57%, elapsed 1437 s, estimated 252038 s (2 days), iters = {MDP: 4134}, opt = -7.525 +> progress 0.57%, elapsed 1442 s, estimated 252747 s (2 days), iters = {MDP: 4135}, opt = -7.525 +> progress 0.57%, elapsed 1446 s, estimated 253482 s (2 days), iters = {MDP: 4136}, opt = -7.525 +> progress 0.57%, elapsed 1450 s, estimated 254191 s (2 days), iters = {MDP: 4137}, opt = -7.525 +> progress 0.57%, elapsed 1454 s, estimated 254860 s (2 days), iters = {MDP: 4138}, opt = -7.525 +> progress 0.578%, elapsed 1467 s, estimated 253580 s (2 days), iters = {MDP: 4142}, opt = -7.525 +> progress 0.578%, elapsed 1479 s, estimated 255708 s (2 days), iters = {MDP: 4144}, opt = -7.525 +> progress 0.578%, elapsed 1488 s, estimated 257140 s (2 days), iters = {MDP: 4145}, opt = -7.525 +> progress 0.578%, elapsed 1494 s, estimated 258250 s (2 days), iters = {MDP: 4146}, opt = -7.525 +> progress 0.578%, elapsed 1498 s, estimated 259021 s (2 days), iters = {MDP: 4147}, opt = -7.525 +> progress 0.578%, elapsed 1502 s, estimated 259602 s (3 days), iters = {MDP: 4149}, opt = -7.525 +> progress 0.578%, elapsed 1506 s, estimated 260335 s (3 days), iters = {MDP: 4151}, opt = -7.525 +> progress 0.578%, elapsed 1510 s, estimated 261013 s (3 days), iters = {MDP: 4153}, opt = -7.525 +> progress 0.578%, elapsed 1515 s, estimated 261894 s (3 days), iters = {MDP: 4156}, opt = -7.525 +> progress 0.578%, elapsed 1535 s, estimated 265355 s (3 days), iters = {MDP: 4161}, opt = -7.525 +> progress 0.578%, elapsed 1538 s, estimated 265904 s (3 days), iters = {MDP: 4173}, opt = -7.525 +> progress 0.578%, elapsed 1542 s, estimated 266522 s (3 days), iters = {MDP: 4179}, opt = -7.525 +> progress 0.578%, elapsed 1545 s, estimated 267051 s (3 days), iters = {MDP: 4195}, opt = -7.525 +> progress 0.578%, elapsed 1549 s, estimated 267667 s (3 days), iters = {MDP: 4205}, opt = -7.525 +> progress 0.578%, elapsed 1552 s, estimated 268294 s (3 days), iters = {MDP: 4210}, opt = -7.525 +> progress 0.578%, elapsed 1556 s, estimated 268889 s (3 days), iters = {MDP: 4225}, opt = -7.525 +> progress 0.578%, elapsed 1560 s, estimated 269616 s (3 days), iters = {MDP: 4235}, opt = -7.525 +> progress 0.578%, elapsed 1563 s, estimated 270196 s (3 days), iters = {MDP: 4242}, opt = -7.525 +> progress 0.578%, elapsed 1567 s, estimated 270757 s (3 days), iters = {MDP: 4256}, opt = -7.525 +> progress 0.578%, elapsed 1570 s, estimated 271390 s (3 days), iters = {MDP: 4260}, opt = -7.525 +> progress 0.578%, elapsed 1574 s, estimated 272009 s (3 days), iters = {MDP: 4277}, opt = -7.525 +> progress 0.578%, elapsed 1577 s, estimated 272608 s (3 days), iters = {MDP: 4287}, opt = -7.525 +> progress 0.578%, elapsed 1580 s, estimated 273133 s (3 days), iters = {MDP: 4291}, opt = -7.525 +> progress 0.578%, elapsed 1583 s, estimated 273682 s (3 days), iters = {MDP: 4307}, opt = -7.525 +> progress 0.578%, elapsed 1587 s, estimated 274323 s (3 days), iters = {MDP: 4315}, opt = -7.525 +> progress 0.578%, elapsed 1590 s, estimated 274863 s (3 days), iters = {MDP: 4321}, opt = -7.525 +> progress 0.578%, elapsed 1593 s, estimated 275385 s (3 days), iters = {MDP: 4328}, opt = -7.525 +> progress 0.578%, elapsed 1596 s, estimated 275916 s (3 days), iters = {MDP: 4333}, opt = -7.525 +> progress 0.578%, elapsed 1599 s, estimated 276446 s (3 days), iters = {MDP: 4338}, opt = -7.525 +> progress 0.578%, elapsed 1603 s, estimated 276999 s (3 days), iters = {MDP: 4343}, opt = -7.525 +> progress 0.578%, elapsed 1606 s, estimated 277538 s (3 days), iters = {MDP: 4351}, opt = -7.525 +> progress 0.578%, elapsed 1609 s, estimated 278065 s (3 days), iters = {MDP: 4356}, opt = -7.525 +> progress 0.578%, elapsed 1612 s, estimated 278671 s (3 days), iters = {MDP: 4362}, opt = -7.525 +> progress 0.578%, elapsed 1616 s, estimated 279241 s (3 days), iters = {MDP: 4365}, opt = -7.525 +> progress 0.578%, elapsed 1621 s, estimated 280198 s (3 days), iters = {MDP: 4367}, opt = -7.525 +> progress 0.578%, elapsed 1625 s, estimated 280807 s (3 days), iters = {MDP: 4368}, opt = -7.525 +> progress 0.578%, elapsed 1628 s, estimated 281401 s (3 days), iters = {MDP: 4369}, opt = -7.525 +> progress 0.578%, elapsed 1632 s, estimated 282009 s (3 days), iters = {MDP: 4370}, opt = -7.525 +> progress 0.578%, elapsed 1636 s, estimated 282612 s (3 days), iters = {MDP: 4371}, opt = -7.525 +> progress 0.579%, elapsed 1640 s, estimated 283297 s (3 days), iters = {MDP: 4372}, opt = -7.525 +> progress 0.579%, elapsed 1646 s, estimated 284251 s (3 days), iters = {MDP: 4373}, opt = -7.525 +> progress 0.579%, elapsed 1652 s, estimated 285181 s (3 days), iters = {MDP: 4374}, opt = -7.525 +> progress 0.579%, elapsed 1660 s, estimated 286541 s (3 days), iters = {MDP: 4375}, opt = -7.525 +> progress 0.579%, elapsed 1666 s, estimated 287582 s (3 days), iters = {MDP: 4376}, opt = -7.525 +> progress 0.579%, elapsed 1670 s, estimated 288188 s (3 days), iters = {MDP: 4377}, opt = -7.525 +> progress 0.579%, elapsed 1675 s, estimated 288967 s (3 days), iters = {MDP: 4380}, opt = -7.525 +> progress 0.579%, elapsed 1678 s, estimated 289572 s (3 days), iters = {MDP: 4382}, opt = -7.525 +> progress 0.579%, elapsed 1681 s, estimated 290128 s (3 days), iters = {MDP: 4384}, opt = -7.525 +> progress 0.579%, elapsed 1684 s, estimated 290662 s (3 days), iters = {MDP: 4387}, opt = -7.525 +> progress 0.579%, elapsed 1687 s, estimated 291198 s (3 days), iters = {MDP: 4395}, opt = -7.525 +> progress 0.579%, elapsed 1691 s, estimated 291778 s (3 days), iters = {MDP: 4404}, opt = -7.525 +> progress 0.579%, elapsed 1695 s, estimated 292426 s (3 days), iters = {MDP: 4412}, opt = -7.525 +> progress 0.579%, elapsed 1698 s, estimated 293052 s (3 days), iters = {MDP: 4421}, opt = -7.525 +> progress 0.579%, elapsed 1701 s, estimated 293595 s (3 days), iters = {MDP: 4435}, opt = -7.525 +> progress 0.579%, elapsed 1705 s, estimated 294181 s (3 days), iters = {MDP: 4440}, opt = -7.525 +> progress 0.579%, elapsed 1708 s, estimated 294750 s (3 days), iters = {MDP: 4451}, opt = -7.525 +> progress 0.579%, elapsed 1712 s, estimated 295364 s (3 days), iters = {MDP: 4456}, opt = -7.525 +> progress 0.579%, elapsed 1715 s, estimated 295902 s (3 days), iters = {MDP: 4467}, opt = -7.525 +> progress 0.579%, elapsed 1719 s, estimated 296607 s (3 days), iters = {MDP: 4473}, opt = -7.525 +> progress 0.579%, elapsed 1722 s, estimated 297181 s (3 days), iters = {MDP: 4479}, opt = -7.525 +> progress 0.579%, elapsed 1725 s, estimated 297707 s (3 days), iters = {MDP: 4488}, opt = -7.525 +> progress 0.579%, elapsed 1728 s, estimated 298239 s (3 days), iters = {MDP: 4495}, opt = -7.525 +> progress 0.579%, elapsed 1732 s, estimated 298807 s (3 days), iters = {MDP: 4501}, opt = -7.525 +> progress 0.579%, elapsed 1735 s, estimated 299425 s (3 days), iters = {MDP: 4510}, opt = -7.525 +> progress 0.579%, elapsed 1738 s, estimated 299954 s (3 days), iters = {MDP: 4524}, opt = -7.525 +> progress 0.579%, elapsed 1742 s, estimated 300522 s (3 days), iters = {MDP: 4529}, opt = -7.525 +> progress 0.579%, elapsed 1745 s, estimated 301141 s (3 days), iters = {MDP: 4540}, opt = -7.525 +> progress 0.579%, elapsed 1749 s, estimated 301772 s (3 days), iters = {MDP: 4546}, opt = -7.525 +> progress 0.579%, elapsed 1752 s, estimated 302359 s (3 days), iters = {MDP: 4557}, opt = -7.525 +> progress 0.579%, elapsed 1756 s, estimated 303019 s (3 days), iters = {MDP: 4562}, opt = -7.525 +> progress 0.579%, elapsed 1759 s, estimated 303580 s (3 days), iters = {MDP: 4567}, opt = -7.525 +> progress 0.579%, elapsed 1763 s, estimated 304167 s (3 days), iters = {MDP: 4579}, opt = -7.525 +> progress 0.579%, elapsed 1766 s, estimated 304723 s (3 days), iters = {MDP: 4587}, opt = -7.525 +> progress 0.579%, elapsed 1769 s, estimated 305265 s (3 days), iters = {MDP: 4598}, opt = -7.525 +> progress 0.579%, elapsed 1772 s, estimated 305822 s (3 days), iters = {MDP: 4605}, opt = -7.525 +> progress 0.579%, elapsed 1776 s, estimated 306425 s (3 days), iters = {MDP: 4614}, opt = -7.525 +> progress 0.579%, elapsed 1779 s, estimated 307034 s (3 days), iters = {MDP: 4620}, opt = -7.525 +> progress 0.579%, elapsed 1782 s, estimated 307560 s (3 days), iters = {MDP: 4629}, opt = -7.525 +> progress 0.579%, elapsed 1786 s, estimated 308126 s (3 days), iters = {MDP: 4634}, opt = -7.525 +> progress 0.579%, elapsed 1789 s, estimated 308713 s (3 days), iters = {MDP: 4646}, opt = -7.525 +> progress 0.579%, elapsed 1792 s, estimated 309286 s (3 days), iters = {MDP: 4654}, opt = -7.525 +> progress 0.579%, elapsed 1796 s, estimated 309837 s (3 days), iters = {MDP: 4665}, opt = -7.525 +> progress 0.579%, elapsed 1799 s, estimated 310408 s (3 days), iters = {MDP: 4672}, opt = -7.525 +> progress 0.579%, elapsed 1802 s, estimated 311006 s (3 days), iters = {MDP: 4681}, opt = -7.525 +> progress 0.579%, elapsed 1805 s, estimated 311548 s (3 days), iters = {MDP: 4686}, opt = -7.525 +> progress 0.579%, elapsed 1809 s, estimated 312098 s (3 days), iters = {MDP: 4695}, opt = -7.525 +> progress 0.579%, elapsed 1812 s, estimated 312733 s (3 days), iters = {MDP: 4699}, opt = -7.525 +> progress 0.579%, elapsed 1816 s, estimated 313292 s (3 days), iters = {MDP: 4709}, opt = -7.525 +> progress 0.579%, elapsed 1819 s, estimated 313887 s (3 days), iters = {MDP: 4718}, opt = -7.525 +> progress 0.579%, elapsed 1822 s, estimated 314426 s (3 days), iters = {MDP: 4729}, opt = -7.525 +> progress 0.579%, elapsed 1825 s, estimated 314956 s (3 days), iters = {MDP: 4736}, opt = -7.525 +> progress 0.579%, elapsed 1829 s, estimated 315563 s (3 days), iters = {MDP: 4743}, opt = -7.525 +> progress 0.579%, elapsed 1832 s, estimated 316102 s (3 days), iters = {MDP: 4752}, opt = -7.525 +> progress 0.579%, elapsed 1835 s, estimated 316652 s (3 days), iters = {MDP: 4759}, opt = -7.525 +> progress 0.579%, elapsed 1839 s, estimated 317247 s (3 days), iters = {MDP: 4766}, opt = -7.525 +> progress 0.579%, elapsed 1842 s, estimated 317841 s (3 days), iters = {MDP: 4776}, opt = -7.525 +> progress 0.579%, elapsed 1845 s, estimated 318446 s (3 days), iters = {MDP: 4785}, opt = -7.525 +> progress 0.579%, elapsed 1849 s, estimated 318986 s (3 days), iters = {MDP: 4796}, opt = -7.525 +> progress 0.579%, elapsed 1852 s, estimated 319524 s (3 days), iters = {MDP: 4803}, opt = -7.525 +> progress 0.579%, elapsed 1855 s, estimated 320048 s (3 days), iters = {MDP: 4809}, opt = -7.525 +> progress 0.579%, elapsed 1858 s, estimated 320595 s (3 days), iters = {MDP: 4818}, opt = -7.525 +> progress 0.579%, elapsed 1861 s, estimated 321122 s (3 days), iters = {MDP: 4823}, opt = -7.525 +> progress 0.579%, elapsed 1864 s, estimated 321670 s (3 days), iters = {MDP: 4832}, opt = -7.525 +> progress 0.579%, elapsed 1868 s, estimated 322336 s (3 days), iters = {MDP: 4835}, opt = -7.525 +> progress 0.579%, elapsed 1872 s, estimated 322998 s (3 days), iters = {MDP: 4836}, opt = -7.525 +> progress 0.579%, elapsed 1875 s, estimated 323530 s (3 days), iters = {MDP: 4837}, opt = -7.525 +> progress 0.579%, elapsed 1878 s, estimated 324060 s (3 days), iters = {MDP: 4838}, opt = -7.525 +> progress 0.579%, elapsed 1882 s, estimated 324614 s (3 days), iters = {MDP: 4839}, opt = -7.525 +> progress 0.579%, elapsed 1885 s, estimated 325177 s (3 days), iters = {MDP: 4840}, opt = -7.525 +> progress 0.579%, elapsed 1889 s, estimated 325916 s (3 days), iters = {MDP: 4844}, opt = -7.525 +> progress 0.579%, elapsed 1894 s, estimated 326711 s (3 days), iters = {MDP: 4850}, opt = -7.525 +> progress 0.579%, elapsed 1899 s, estimated 327564 s (3 days), iters = {MDP: 4852}, opt = -7.525 +> progress 0.579%, elapsed 1903 s, estimated 328220 s (3 days), iters = {MDP: 4853}, opt = -7.525 +> progress 0.58%, elapsed 1909 s, estimated 329122 s (3 days), iters = {MDP: 4854}, opt = -7.525 +> progress 0.58%, elapsed 1915 s, estimated 329965 s (3 days), iters = {MDP: 4855}, opt = -7.525 +> progress 0.58%, elapsed 1923 s, estimated 331285 s (3 days), iters = {MDP: 4856}, opt = -7.525 +> progress 0.58%, elapsed 1930 s, estimated 332536 s (3 days), iters = {MDP: 4857}, opt = -7.525 +> progress 0.58%, elapsed 1934 s, estimated 333242 s (3 days), iters = {MDP: 4858}, opt = -7.525 +> progress 0.58%, elapsed 1939 s, estimated 334009 s (3 days), iters = {MDP: 4859}, opt = -7.525 +> progress 0.58%, elapsed 1942 s, estimated 334544 s (3 days), iters = {MDP: 4860}, opt = -7.525 +> progress 0.58%, elapsed 1947 s, estimated 335394 s (3 days), iters = {MDP: 4862}, opt = -7.525 +> progress 0.58%, elapsed 1950 s, estimated 335912 s (3 days), iters = {MDP: 4893}, opt = -7.525 +> progress 0.58%, elapsed 1953 s, estimated 336512 s (3 days), iters = {MDP: 4908}, opt = -7.525 +> progress 0.58%, elapsed 1957 s, estimated 337144 s (3 days), iters = {MDP: 4915}, opt = -7.525 +> progress 0.58%, elapsed 1960 s, estimated 337707 s (3 days), iters = {MDP: 4921}, opt = -7.525 +> progress 0.58%, elapsed 1963 s, estimated 338230 s (3 days), iters = {MDP: 4932}, opt = -7.525 +> progress 0.58%, elapsed 1967 s, estimated 338841 s (3 days), iters = {MDP: 4947}, opt = -7.525 +> progress 0.58%, elapsed 1970 s, estimated 339455 s (3 days), iters = {MDP: 4951}, opt = -7.525 +> progress 0.58%, elapsed 1974 s, estimated 340147 s (3 days), iters = {MDP: 4957}, opt = -7.525 +> progress 0.58%, elapsed 1977 s, estimated 340682 s (3 days), iters = {MDP: 4985}, opt = -7.525 +> progress 0.58%, elapsed 1981 s, estimated 341219 s (3 days), iters = {MDP: 4998}, opt = -7.525 +> progress 0.58%, elapsed 1985 s, estimated 342031 s (3 days), iters = {MDP: 5006}, opt = -7.525 +> progress 0.58%, elapsed 1988 s, estimated 342574 s (3 days), iters = {MDP: 5008}, opt = -7.525 +> progress 0.58%, elapsed 1992 s, estimated 343127 s (3 days), iters = {MDP: 5038}, opt = -7.525 +> progress 0.58%, elapsed 1995 s, estimated 343685 s (3 days), iters = {MDP: 5054}, opt = -7.525 +> progress 0.58%, elapsed 1998 s, estimated 344273 s (3 days), iters = {MDP: 5056}, opt = -7.525 +> progress 0.58%, elapsed 2002 s, estimated 344965 s (3 days), iters = {MDP: 5058}, opt = -7.525 +> progress 0.58%, elapsed 2006 s, estimated 345567 s (3 days), iters = {MDP: 5062}, opt = -7.525 +> progress 0.58%, elapsed 2009 s, estimated 346142 s (4 days), iters = {MDP: 5081}, opt = -7.525 +> progress 0.58%, elapsed 2013 s, estimated 346728 s (4 days), iters = {MDP: 5083}, opt = -7.525 +> progress 0.58%, elapsed 2017 s, estimated 347457 s (4 days), iters = {MDP: 5085}, opt = -7.525 +> progress 0.58%, elapsed 2020 s, estimated 347981 s (4 days), iters = {MDP: 5106}, opt = -7.525 +> progress 0.58%, elapsed 2023 s, estimated 348502 s (4 days), iters = {MDP: 5121}, opt = -7.525 +> progress 0.58%, elapsed 2028 s, estimated 349314 s (4 days), iters = {MDP: 5133}, opt = -7.525 +> progress 0.58%, elapsed 2032 s, estimated 350026 s (4 days), iters = {MDP: 5137}, opt = -7.525 +> progress 0.58%, elapsed 2037 s, estimated 350854 s (4 days), iters = {MDP: 5139}, opt = -7.525 +> progress 0.58%, elapsed 2040 s, estimated 351375 s (4 days), iters = {MDP: 5171}, opt = -7.525 +> progress 0.58%, elapsed 2043 s, estimated 351999 s (4 days), iters = {MDP: 5183}, opt = -7.525 +> progress 0.58%, elapsed 2047 s, estimated 352682 s (4 days), iters = {MDP: 5185}, opt = -7.525 +> progress 0.58%, elapsed 2050 s, estimated 353205 s (4 days), iters = {MDP: 5186}, opt = -7.525 +> progress 0.58%, elapsed 2054 s, estimated 353851 s (4 days), iters = {MDP: 5187}, opt = -7.525 +> progress 0.58%, elapsed 2061 s, estimated 355094 s (4 days), iters = {MDP: 5188}, opt = -7.525 +> progress 0.58%, elapsed 2068 s, estimated 356212 s (4 days), iters = {MDP: 5189}, opt = -7.525 +> progress 0.58%, elapsed 2073 s, estimated 357062 s (4 days), iters = {MDP: 5190}, opt = -7.525 +> progress 0.58%, elapsed 2076 s, estimated 357679 s (4 days), iters = {MDP: 5193}, opt = -7.525 +> progress 0.58%, elapsed 2080 s, estimated 358227 s (4 days), iters = {MDP: 5201}, opt = -7.525 +> progress 0.58%, elapsed 2083 s, estimated 358774 s (4 days), iters = {MDP: 5207}, opt = -7.525 +> progress 0.58%, elapsed 2086 s, estimated 359313 s (4 days), iters = {MDP: 5222}, opt = -7.525 +> progress 0.58%, elapsed 2089 s, estimated 359835 s (4 days), iters = {MDP: 5237}, opt = -7.525 +> progress 0.58%, elapsed 2092 s, estimated 360359 s (4 days), iters = {MDP: 5242}, opt = -7.525 +> progress 0.58%, elapsed 2095 s, estimated 360896 s (4 days), iters = {MDP: 5252}, opt = -7.525 +> progress 0.58%, elapsed 2098 s, estimated 361468 s (4 days), iters = {MDP: 5258}, opt = -7.525 +> progress 0.58%, elapsed 2102 s, estimated 362000 s (4 days), iters = {MDP: 5275}, opt = -7.525 +> progress 0.58%, elapsed 2105 s, estimated 362549 s (4 days), iters = {MDP: 5289}, opt = -7.525 +> progress 0.58%, elapsed 2108 s, estimated 363072 s (4 days), iters = {MDP: 5300}, opt = -7.525 +> progress 0.58%, elapsed 2111 s, estimated 363600 s (4 days), iters = {MDP: 5307}, opt = -7.525 +> progress 0.58%, elapsed 2114 s, estimated 364170 s (4 days), iters = {MDP: 5320}, opt = -7.525 +> progress 0.58%, elapsed 2117 s, estimated 364696 s (4 days), iters = {MDP: 5331}, opt = -7.525 +> progress 0.58%, elapsed 2120 s, estimated 365259 s (4 days), iters = {MDP: 5336}, opt = -7.525 +> progress 0.58%, elapsed 2124 s, estimated 365807 s (4 days), iters = {MDP: 5342}, opt = -7.525 +> progress 0.58%, elapsed 2127 s, estimated 366428 s (4 days), iters = {MDP: 5344}, opt = -7.525 +> progress 0.58%, elapsed 2130 s, estimated 366968 s (4 days), iters = {MDP: 5346}, opt = -7.525 +> progress 0.58%, elapsed 2134 s, estimated 367551 s (4 days), iters = {MDP: 5348}, opt = -7.525 +> progress 0.58%, elapsed 2141 s, estimated 368732 s (4 days), iters = {MDP: 5350}, opt = -7.525 +> progress 0.58%, elapsed 2146 s, estimated 369610 s (4 days), iters = {MDP: 5351}, opt = -7.525 +> progress 0.58%, elapsed 2151 s, estimated 370450 s (4 days), iters = {MDP: 5352}, opt = -7.525 +> progress 0.58%, elapsed 2155 s, estimated 371235 s (4 days), iters = {MDP: 5353}, opt = -7.525 +> progress 0.58%, elapsed 2158 s, estimated 371756 s (4 days), iters = {MDP: 5356}, opt = -7.525 +> progress 0.58%, elapsed 2162 s, estimated 372326 s (4 days), iters = {MDP: 5370}, opt = -7.525 +> progress 0.58%, elapsed 2165 s, estimated 372861 s (4 days), iters = {MDP: 5392}, opt = -7.525 +> progress 0.58%, elapsed 2168 s, estimated 373449 s (4 days), iters = {MDP: 5408}, opt = -7.525 +> progress 0.58%, elapsed 2171 s, estimated 374027 s (4 days), iters = {MDP: 5425}, opt = -7.525 +> progress 0.58%, elapsed 2175 s, estimated 374654 s (4 days), iters = {MDP: 5442}, opt = -7.525 +> progress 0.58%, elapsed 2178 s, estimated 375190 s (4 days), iters = {MDP: 5445}, opt = -7.525 +> progress 0.58%, elapsed 2183 s, estimated 376097 s (4 days), iters = {MDP: 5448}, opt = -7.525 +> progress 0.58%, elapsed 2186 s, estimated 376622 s (4 days), iters = {MDP: 5455}, opt = -7.525 +> progress 0.58%, elapsed 2190 s, estimated 377182 s (4 days), iters = {MDP: 5457}, opt = -7.525 +> progress 0.58%, elapsed 2194 s, estimated 377864 s (4 days), iters = {MDP: 5459}, opt = -7.525 +> progress 0.58%, elapsed 2198 s, estimated 378607 s (4 days), iters = {MDP: 5462}, opt = -7.525 +> progress 0.58%, elapsed 2202 s, estimated 379337 s (4 days), iters = {MDP: 5465}, opt = -7.525 +> progress 0.58%, elapsed 2206 s, estimated 379991 s (4 days), iters = {MDP: 5475}, opt = -7.525 +> progress 0.58%, elapsed 2209 s, estimated 380577 s (4 days), iters = {MDP: 5488}, opt = -7.525 +> progress 0.58%, elapsed 2213 s, estimated 381147 s (4 days), iters = {MDP: 5500}, opt = -7.525 +> progress 0.58%, elapsed 2216 s, estimated 381710 s (4 days), iters = {MDP: 5504}, opt = -7.525 +> progress 0.58%, elapsed 2220 s, estimated 382318 s (4 days), iters = {MDP: 5513}, opt = -7.525 +> progress 0.58%, elapsed 2223 s, estimated 382967 s (4 days), iters = {MDP: 5516}, opt = -7.525 +> progress 0.58%, elapsed 2227 s, estimated 383568 s (4 days), iters = {MDP: 5521}, opt = -7.525 +> progress 0.58%, elapsed 2230 s, estimated 384094 s (4 days), iters = {MDP: 5524}, opt = -7.525 +> progress 0.58%, elapsed 2234 s, estimated 384859 s (4 days), iters = {MDP: 5537}, opt = -7.525 +> progress 0.58%, elapsed 2241 s, estimated 386001 s (4 days), iters = {MDP: 5540}, opt = -7.525 +> progress 0.58%, elapsed 2245 s, estimated 386643 s (4 days), iters = {MDP: 5541}, opt = -7.525 +> progress 0.58%, elapsed 2248 s, estimated 387201 s (4 days), iters = {MDP: 5545}, opt = -7.525 +> progress 0.58%, elapsed 2251 s, estimated 387785 s (4 days), iters = {MDP: 5549}, opt = -7.525 +> progress 0.58%, elapsed 2255 s, estimated 388452 s (4 days), iters = {MDP: 5551}, opt = -7.525 +> progress 0.58%, elapsed 2259 s, estimated 389094 s (4 days), iters = {MDP: 5552}, opt = -7.525 +> progress 0.58%, elapsed 2262 s, estimated 389704 s (4 days), iters = {MDP: 5556}, opt = -7.525 +> progress 0.58%, elapsed 2266 s, estimated 390354 s (4 days), iters = {MDP: 5562}, opt = -7.525 +> progress 0.58%, elapsed 2270 s, estimated 390923 s (4 days), iters = {MDP: 5564}, opt = -7.525 +> progress 0.58%, elapsed 2276 s, estimated 392009 s (4 days), iters = {MDP: 5569}, opt = -7.525 +> progress 0.58%, elapsed 2279 s, estimated 392582 s (4 days), iters = {MDP: 5570}, opt = -7.525 +> progress 0.58%, elapsed 2283 s, estimated 393224 s (4 days), iters = {MDP: 5572}, opt = -7.525 +> progress 0.58%, elapsed 2286 s, estimated 393758 s (4 days), iters = {MDP: 5579}, opt = -7.525 +> progress 0.58%, elapsed 2289 s, estimated 394295 s (4 days), iters = {MDP: 5592}, opt = -7.525 +> progress 0.58%, elapsed 2292 s, estimated 394868 s (4 days), iters = {MDP: 5601}, opt = -7.525 +> progress 0.58%, elapsed 2296 s, estimated 395423 s (4 days), iters = {MDP: 5607}, opt = -7.525 +> progress 0.58%, elapsed 2299 s, estimated 396070 s (4 days), iters = {MDP: 5615}, opt = -7.525 +> progress 0.58%, elapsed 2305 s, estimated 397008 s (4 days), iters = {MDP: 5617}, opt = -7.525 +> progress 0.58%, elapsed 2308 s, estimated 397549 s (4 days), iters = {MDP: 5618}, opt = -7.525 +> progress 0.58%, elapsed 2312 s, estimated 398139 s (4 days), iters = {MDP: 5619}, opt = -7.525 +> progress 0.58%, elapsed 2315 s, estimated 398748 s (4 days), iters = {MDP: 5620}, opt = -7.525 +> progress 0.58%, elapsed 2320 s, estimated 399636 s (4 days), iters = {MDP: 5622}, opt = -7.525 +> progress 0.58%, elapsed 2325 s, estimated 400521 s (4 days), iters = {MDP: 5624}, opt = -7.525 +> progress 0.58%, elapsed 2330 s, estimated 401324 s (4 days), iters = {MDP: 5627}, opt = -7.525 +> progress 0.58%, elapsed 2333 s, estimated 401901 s (4 days), iters = {MDP: 5628}, opt = -7.525 +> progress 0.58%, elapsed 2337 s, estimated 402524 s (4 days), iters = {MDP: 5630}, opt = -7.525 +> progress 0.58%, elapsed 2341 s, estimated 403129 s (4 days), iters = {MDP: 5638}, opt = -7.525 +> progress 0.58%, elapsed 2344 s, estimated 403679 s (4 days), iters = {MDP: 5651}, opt = -7.525 +> progress 0.58%, elapsed 2347 s, estimated 404264 s (4 days), iters = {MDP: 5660}, opt = -7.525 +> progress 0.58%, elapsed 2350 s, estimated 404792 s (4 days), iters = {MDP: 5666}, opt = -7.525 +> progress 0.58%, elapsed 2354 s, estimated 405365 s (4 days), iters = {MDP: 5673}, opt = -7.525 +> progress 0.58%, elapsed 2359 s, estimated 406306 s (4 days), iters = {MDP: 5675}, opt = -7.525 +> progress 0.58%, elapsed 2362 s, estimated 406855 s (4 days), iters = {MDP: 5676}, opt = -7.525 +> progress 0.58%, elapsed 2366 s, estimated 407429 s (4 days), iters = {MDP: 5677}, opt = -7.525 +> progress 0.58%, elapsed 2369 s, estimated 407996 s (4 days), iters = {MDP: 5678}, opt = -7.525 +> progress 0.58%, elapsed 2374 s, estimated 408916 s (4 days), iters = {MDP: 5680}, opt = -7.525 +> progress 0.58%, elapsed 2380 s, estimated 409842 s (4 days), iters = {MDP: 5682}, opt = -7.525 +> progress 0.58%, elapsed 2384 s, estimated 410624 s (4 days), iters = {MDP: 5685}, opt = -7.525 +> progress 0.58%, elapsed 2392 s, estimated 411869 s (4 days), iters = {MDP: 5686}, opt = -7.525 +> progress 0.58%, elapsed 2397 s, estimated 412865 s (4 days), iters = {MDP: 5687}, opt = -7.525 +> progress 0.58%, elapsed 2401 s, estimated 413416 s (4 days), iters = {MDP: 5688}, opt = -7.525 +> progress 0.58%, elapsed 2404 s, estimated 414012 s (4 days), iters = {MDP: 5691}, opt = -7.525 +> progress 0.58%, elapsed 2407 s, estimated 414535 s (4 days), iters = {MDP: 5719}, opt = -7.525 +> progress 0.58%, elapsed 2410 s, estimated 415056 s (4 days), iters = {MDP: 5742}, opt = -7.525 +> progress 0.58%, elapsed 2414 s, estimated 415629 s (4 days), iters = {MDP: 5759}, opt = -7.525 +> progress 0.58%, elapsed 2417 s, estimated 416150 s (4 days), iters = {MDP: 5772}, opt = -7.525 +> progress 0.58%, elapsed 2420 s, estimated 416704 s (4 days), iters = {MDP: 5776}, opt = -7.525 +> progress 0.58%, elapsed 2423 s, estimated 417310 s (4 days), iters = {MDP: 5778}, opt = -7.525 +> progress 0.58%, elapsed 2427 s, estimated 417887 s (4 days), iters = {MDP: 5780}, opt = -7.525 +> progress 0.58%, elapsed 2430 s, estimated 418515 s (4 days), iters = {MDP: 5783}, opt = -7.525 +> progress 0.58%, elapsed 2434 s, estimated 419065 s (4 days), iters = {MDP: 5796}, opt = -7.525 +> progress 0.58%, elapsed 2437 s, estimated 419582 s (4 days), iters = {MDP: 5815}, opt = -7.525 +> progress 0.58%, elapsed 2440 s, estimated 420110 s (4 days), iters = {MDP: 5833}, opt = -7.525 diff --git a/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount-native/sketch.props b/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount-native/sketch.props new file mode 100644 index 000000000..bbcfca504 --- /dev/null +++ b/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount-native/sketch.props @@ -0,0 +1,6 @@ +R{"moves"}max=? [C{0.99}] + +//R{"steps"}min=? [F "goal"] + + +//Pmax=? [F "goal"] \ No newline at end of file diff --git a/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount-native/sketch.templ b/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount-native/sketch.templ new file mode 100644 index 000000000..9ddde212b --- /dev/null +++ b/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount-native/sketch.templ @@ -0,0 +1,152 @@ + +dtmc + +// 7 | x x x x x x x x +// 6 | x x x +// 5 | x x A x x x x +// 4 | x x x x x x x +// 3 | x x x x x x +// 2 | x x x x x A x +// 1 | x x x x x +// 0 | x x x x x +// y _________________ +// x 0 1 2 3 4 5 6 7 + + +// agent1 can go in this direction +formula u1 = ya1<7 & !(xa1=3 & ya1=2) & !(ya1=5 & xa1>3); +formula r1 = xa1<7 & !(xa1=4 & ya1<4) & !(xa1=2 & (ya1>2 & ya1<7)); +formula d1 = ya1>0 & !(ya1=2 & xa1<2) & !(ya1=7 & xa1>2) & !(ya1=4 & xa1=5); +formula l1 = xa1>0 & !(xa1=2 & ya1<2) & !(xa1=6 & ya1<4) & !(xa1=4 & (ya1>2 & ya1<6)); + +// updates of coordinates (if possible) +formula y1u = u1 ? (ya1+1) : ya1; +formula x1r = r1 ? (xa1+1) : xa1; +formula y1d = d1 ? (ya1-1) : ya1; +formula x1l = l1 ? (xa1-1) : xa1; + + +// agent2 can go in this direction +formula u2 = ya2<7 & !(xa2=3 & ya2=2) & !(ya2=5 & xa2>3); +formula r2 = xa2<7 & !(xa2=4 & ya2<4) & !(xa2=2 & (ya2>2 & ya2<7)); +formula d2 = ya2>0 & !(ya2=2 & xa2<2) & !(ya2=7 & xa2>2) & !(ya2=4 & xa2=5); +formula l2 = xa2>0 & !(xa2=2 & ya2<2) & !(xa2=6 & ya2<4) & !(xa2=4 & (ya2>2 & ya2<6)); + +// updates of coordinates (if possible) +formula y2u = u2 ? (ya2+1) : ya2; +formula x2r = r2 ? (xa2+1) : xa2; +formula y2d = d2 ? (ya2-1) : ya2; +formula x2l = l2 ? (xa2-1) : xa2; + + +const double sl=0.1; + +// agent 1 holes +hole int M1_0_1 in {0,1}; +hole int M1_0_0 in {0,1}; +hole int M1_1_1 in {0,1}; +hole int M1_1_0 in {0,1}; +hole int P1_0_1 in {1,2,3,4}; +hole int P1_0_0 in {1,2,3,4}; +hole int P1_1_1 in {1,2,3,4}; +hole int P1_1_0 in {1,2,3,4}; + +// agent 2 holes +hole int M2_0_1 in {0,1}; +hole int M2_0_0 in {0,1}; +hole int M2_1_1 in {0,1}; +hole int M2_1_0 in {0,1}; +hole int P2_0_1 in {1,2,3,4}; +hole int P2_0_0 in {1,2,3,4}; +hole int P2_1_1 in {1,2,3,4}; +hole int P2_1_0 in {1,2,3,4}; + +module strategy1 + mem : [0..1] init 0; + + [move] !meet & mem=0 & r1 -> (mem'=M1_0_1); + [move] !meet & mem=0 & !r1 -> (mem'=M1_0_0); + [move] !meet & mem=1 & r1 -> (mem'=M1_1_1); + [move] !meet & mem=1 & !r1 -> (mem'=M1_1_0); + + [move] meet -> true; +endmodule + +module grid1 + + xa1 : [0..7] init 2; // agent1 x coordinate + ya1 : [0..7] init 5; // agent1 y coordinate + + + [move] !meet & mem=0 & r1 & P1_0_1=1 -> 1-sl: (ya1'=y1u) + sl: true; + [move] !meet & mem=0 & r1 & P1_0_1=2 -> 1-sl: (xa1'=x1r) + sl: true; + [move] !meet & mem=0 & r1 & P1_0_1=3 -> 1-sl: (ya1'=y1d) + sl: true; + [move] !meet & mem=0 & r1 & P1_0_1=4 -> 1-sl: (xa1'=x1l) + sl: true; + + [move] !meet & mem=0 & !r1 & P1_0_0=1 -> 1-sl: (ya1'=y1u) + sl: true; + [move] !meet & mem=0 & !r1 & P1_0_0=2 -> 1-sl: (xa1'=x1r) + sl: true; + [move] !meet & mem=0 & !r1 & P1_0_0=3 -> 1-sl: (ya1'=y1d) + sl: true; + [move] !meet & mem=0 & !r1 & P1_0_0=4 -> 1-sl: (xa1'=x1l) + sl: true; + + [move] !meet & mem=1 & r1 & P1_1_1=1 -> 1-sl: (ya1'=y1u) + sl: true; + [move] !meet & mem=1 & r1 & P1_1_1=2 -> 1-sl: (xa1'=x1r) + sl: true; + [move] !meet & mem=1 & r1 & P1_1_1=3 -> 1-sl: (ya1'=y1d) + sl: true; + [move] !meet & mem=1 & r1 & P1_1_1=4 -> 1-sl: (xa1'=x1l) + sl: true; + + [move] !meet & mem=1 & !r1 & P1_1_0=1 -> 1-sl: (ya1'=y1u) + sl: true; + [move] !meet & mem=1 & !r1 & P1_1_0=2 -> 1-sl: (xa1'=x1r) + sl: true; + [move] !meet & mem=1 & !r1 & P1_1_0=3 -> 1-sl: (ya1'=y1d) + sl: true; + [move] !meet & mem=1 & !r1 & P1_1_0=4 -> 1-sl: (xa1'=x1l) + sl: true; + + [move] meet -> true; +endmodule + + +module strategy2 + mem2 : [0..1] init 0; + + [move] !meet & mem2=0 & l2 -> (mem2'=M2_0_1); + [move] !meet & mem2=0 & !l2 -> (mem2'=M2_0_0); + [move] !meet & mem2=1 & l2 -> (mem2'=M2_1_1); + [move] !meet & mem2=1 & !l2 -> (mem2'=M2_1_0); + + [move] meet -> true; +endmodule + + +module grid2 + + xa2 : [0..7] init 6; // agent2 x coordinate + ya2 : [0..7] init 2; // agent2 y coordinate + + [move] !meet & mem2=0 & l2 & P2_0_1=1 -> 1-sl: (ya2'=y2u) + sl: true; + [move] !meet & mem2=0 & l2 & P2_0_1=2 -> 1-sl: (xa2'=x2r) + sl: true; + [move] !meet & mem2=0 & l2 & P2_0_1=3 -> 1-sl: (ya2'=y2d) + sl: true; + [move] !meet & mem2=0 & l2 & P2_0_1=4 -> 1-sl: (xa2'=x2l) + sl: true; + + [move] !meet & mem2=0 & !l2 & P2_0_0=1 -> 1-sl: (ya2'=y2u) + sl: true; + [move] !meet & mem2=0 & !l2 & P2_0_0=2 -> 1-sl: (xa2'=x2r) + sl: true; + [move] !meet & mem2=0 & !l2 & P2_0_0=3 -> 1-sl: (ya2'=y2d) + sl: true; + [move] !meet & mem2=0 & !l2 & P2_0_0=4 -> 1-sl: (xa2'=x2l) + sl: true; + + [move] !meet & mem2=1 & l2 & P2_1_1=1 -> 1-sl: (ya2'=y2u) + sl: true; + [move] !meet & mem2=1 & l2 & P2_1_1=2 -> 1-sl: (xa2'=x2r) + sl: true; + [move] !meet & mem2=1 & l2 & P2_1_1=3 -> 1-sl: (ya2'=y2d) + sl: true; + [move] !meet & mem2=1 & l2 & P2_1_1=4 -> 1-sl: (xa2'=x2l) + sl: true; + + [move] !meet & mem2=1 & !l2 & P2_1_0=1 -> 1-sl: (ya2'=y2u) + sl: true; + [move] !meet & mem2=1 & !l2 & P2_1_0=2 -> 1-sl: (xa2'=x2r) + sl: true; + [move] !meet & mem2=1 & !l2 & P2_1_0=3 -> 1-sl: (ya2'=y2d) + sl: true; + [move] !meet & mem2=1 & !l2 & P2_1_0=4 -> 1-sl: (xa2'=x2l) + sl: true; + + [move] meet -> true; +endmodule + +// reward +rewards "moves" + !meet : -1; +endrewards + +formula meet = (xa1=xa2) & (ya1=ya2); + + diff --git a/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount-native/sketch.props b/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount-native/sketch.props new file mode 100644 index 000000000..bbcfca504 --- /dev/null +++ b/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount-native/sketch.props @@ -0,0 +1,6 @@ +R{"moves"}max=? [C{0.99}] + +//R{"steps"}min=? [F "goal"] + + +//Pmax=? [F "goal"] \ No newline at end of file diff --git a/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount-native/sketch.templ b/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount-native/sketch.templ new file mode 100644 index 000000000..cc30fb820 --- /dev/null +++ b/models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount-native/sketch.templ @@ -0,0 +1,176 @@ + +dtmc + +// 7 | x x x x x x x x +// 6 | x x x +// 5 | x x A x x x x +// 4 | x x x x x x x +// 3 | x x x x x x +// 2 | x x x x x A x +// 1 | x x x x x +// 0 | x x x x x +// y _________________ +// x 0 1 2 3 4 5 6 7 + + +// agent1 can go in this direction +formula u1 = ya1<7 & !(xa1=3 & ya1=2) & !(ya1=5 & xa1>3); +formula r1 = xa1<7 & !(xa1=4 & ya1<4) & !(xa1=2 & (ya1>2 & ya1<7)); +formula d1 = ya1>0 & !(ya1=2 & xa1<2) & !(ya1=7 & xa1>2) & !(ya1=4 & xa1=5); +formula l1 = xa1>0 & !(xa1=2 & ya1<2) & !(xa1=6 & ya1<4) & !(xa1=4 & (ya1>2 & ya1<6)); + +// updates of coordinates (if possible) +formula y1u = u1 ? (ya1+1) : ya1; +formula x1r = r1 ? (xa1+1) : xa1; +formula y1d = d1 ? (ya1-1) : ya1; +formula x1l = l1 ? (xa1-1) : xa1; + + +// agent2 can go in this direction +formula u2 = ya2<7 & !(xa2=3 & ya2=2) & !(ya2=5 & xa2>3); +formula r2 = xa2<7 & !(xa2=4 & ya2<4) & !(xa2=2 & (ya2>2 & ya2<7)); +formula d2 = ya2>0 & !(ya2=2 & xa2<2) & !(ya2=7 & xa2>2) & !(ya2=4 & xa2=5); +formula l2 = xa2>0 & !(xa2=2 & ya2<2) & !(xa2=6 & ya2<4) & !(xa2=4 & (ya2>2 & ya2<6)); + +// updates of coordinates (if possible) +formula y2u = u2 ? (ya2+1) : ya2; +formula x2r = r2 ? (xa2+1) : xa2; +formula y2d = d2 ? (ya2-1) : ya2; +formula x2l = l2 ? (xa2-1) : xa2; + + +const double sl=0.1; + +// agent 1 holes +hole int M1_0_1 in {0,1,2}; +hole int M1_0_0 in {0,1,2}; +hole int M1_1_1 in {0,1,2}; +hole int M1_1_0 in {0,1,2}; +hole int M1_2_0 in {0,1,2}; +hole int M1_2_1 in {0,1,2}; +hole int P1_0_1 in {1,2,3,4}; +hole int P1_0_0 in {1,2,3,4}; +hole int P1_1_1 in {1,2,3,4}; +hole int P1_1_0 in {1,2,3,4}; +hole int P1_2_1 in {1,2,3,4}; +hole int P1_2_0 in {1,2,3,4}; + +// agent 2 holes +hole int M2_0_1 in {0,1,2}; +hole int M2_0_0 in {0,1,2}; +hole int M2_1_1 in {0,1,2}; +hole int M2_1_0 in {0,1,2}; +hole int M2_2_1 in {0,1,2}; +hole int M2_2_0 in {0,1,2}; +hole int P2_0_1 in {1,2,3,4}; +hole int P2_0_0 in {1,2,3,4}; +hole int P2_1_1 in {1,2,3,4}; +hole int P2_1_0 in {1,2,3,4}; +hole int P2_2_1 in {1,2,3,4}; +hole int P2_2_0 in {1,2,3,4}; + +module strategy1 + mem : [0..2] init 0; + + [move] !meet & mem=0 & r1 -> (mem'=M1_0_1); + [move] !meet & mem=0 & !r1 -> (mem'=M1_0_0); + [move] !meet & mem=1 & r1 -> (mem'=M1_1_1); + [move] !meet & mem=1 & !r1 -> (mem'=M1_1_0); + [move] !meet & mem=2 & r1 -> (mem'=M1_2_1); + [move] !meet & mem=2 & !r1 -> (mem'=M1_2_0); +endmodule + +module grid1 + + xa1 : [0..7] init 2; // agent1 x coordinate + ya1 : [0..7] init 5; // agent1 y coordinate + + + [move] !meet & mem=0 & r1 & P1_0_1=1 -> 1-sl: (ya1'=y1u) + sl: true; + [move] !meet & mem=0 & r1 & P1_0_1=2 -> 1-sl: (xa1'=x1r) + sl: true; + [move] !meet & mem=0 & r1 & P1_0_1=3 -> 1-sl: (ya1'=y1d) + sl: true; + [move] !meet & mem=0 & r1 & P1_0_1=4 -> 1-sl: (xa1'=x1l) + sl: true; + + [move] !meet & mem=0 & !r1 & P1_0_0=1 -> 1-sl: (ya1'=y1u) + sl: true; + [move] !meet & mem=0 & !r1 & P1_0_0=2 -> 1-sl: (xa1'=x1r) + sl: true; + [move] !meet & mem=0 & !r1 & P1_0_0=3 -> 1-sl: (ya1'=y1d) + sl: true; + [move] !meet & mem=0 & !r1 & P1_0_0=4 -> 1-sl: (xa1'=x1l) + sl: true; + + [move] !meet & mem=1 & r1 & P1_1_1=1 -> 1-sl: (ya1'=y1u) + sl: true; + [move] !meet & mem=1 & r1 & P1_1_1=2 -> 1-sl: (xa1'=x1r) + sl: true; + [move] !meet & mem=1 & r1 & P1_1_1=3 -> 1-sl: (ya1'=y1d) + sl: true; + [move] !meet & mem=1 & r1 & P1_1_1=4 -> 1-sl: (xa1'=x1l) + sl: true; + + [move] !meet & mem=1 & !r1 & P1_1_0=1 -> 1-sl: (ya1'=y1u) + sl: true; + [move] !meet & mem=1 & !r1 & P1_1_0=2 -> 1-sl: (xa1'=x1r) + sl: true; + [move] !meet & mem=1 & !r1 & P1_1_0=3 -> 1-sl: (ya1'=y1d) + sl: true; + [move] !meet & mem=1 & !r1 & P1_1_0=4 -> 1-sl: (xa1'=x1l) + sl: true; + + [move] !meet & mem=2 & r1 & P1_2_1=1 -> 1-sl: (ya1'=y1u) + sl: true; + [move] !meet & mem=2 & r1 & P1_2_1=2 -> 1-sl: (xa1'=x1r) + sl: true; + [move] !meet & mem=2 & r1 & P1_2_1=3 -> 1-sl: (ya1'=y1d) + sl: true; + [move] !meet & mem=2 & r1 & P1_2_1=4 -> 1-sl: (xa1'=x1l) + sl: true; + + [move] !meet & mem=2 & !r1 & P1_2_0=1 -> 1-sl: (ya1'=y1u) + sl: true; + [move] !meet & mem=2 & !r1 & P1_2_0=2 -> 1-sl: (xa1'=x1r) + sl: true; + [move] !meet & mem=2 & !r1 & P1_2_0=3 -> 1-sl: (ya1'=y1d) + sl: true; + [move] !meet & mem=2 & !r1 & P1_2_0=4 -> 1-sl: (xa1'=x1l) + sl: true; + +endmodule + + +module strategy2 + mem2 : [0..2] init 0; + + [move] !meet & mem2=0 & l2 -> (mem2'=M2_0_1); + [move] !meet & mem2=0 & !l2 -> (mem2'=M2_0_0); + [move] !meet & mem2=1 & l2 -> (mem2'=M2_1_1); + [move] !meet & mem2=1 & !l2 -> (mem2'=M2_1_0); + [move] !meet & mem2=2 & l2 -> (mem2'=M2_2_1); + [move] !meet & mem2=2 & !l2 -> (mem2'=M2_2_0); +endmodule + + +module grid2 + + xa2 : [0..7] init 6; // agent2 x coordinate + ya2 : [0..7] init 2; // agent2 y coordinate + + [move] !meet & mem2=0 & l2 & P2_0_1=1 -> 1-sl: (ya2'=y2u) + sl: true; + [move] !meet & mem2=0 & l2 & P2_0_1=2 -> 1-sl: (xa2'=x2r) + sl: true; + [move] !meet & mem2=0 & l2 & P2_0_1=3 -> 1-sl: (ya2'=y2d) + sl: true; + [move] !meet & mem2=0 & l2 & P2_0_1=4 -> 1-sl: (xa2'=x2l) + sl: true; + + [move] !meet & mem2=0 & !l2 & P2_0_0=1 -> 1-sl: (ya2'=y2u) + sl: true; + [move] !meet & mem2=0 & !l2 & P2_0_0=2 -> 1-sl: (xa2'=x2r) + sl: true; + [move] !meet & mem2=0 & !l2 & P2_0_0=3 -> 1-sl: (ya2'=y2d) + sl: true; + [move] !meet & mem2=0 & !l2 & P2_0_0=4 -> 1-sl: (xa2'=x2l) + sl: true; + + [move] !meet & mem2=1 & l2 & P2_1_1=1 -> 1-sl: (ya2'=y2u) + sl: true; + [move] !meet & mem2=1 & l2 & P2_1_1=2 -> 1-sl: (xa2'=x2r) + sl: true; + [move] !meet & mem2=1 & l2 & P2_1_1=3 -> 1-sl: (ya2'=y2d) + sl: true; + [move] !meet & mem2=1 & l2 & P2_1_1=4 -> 1-sl: (xa2'=x2l) + sl: true; + + [move] !meet & mem2=1 & !l2 & P2_1_0=1 -> 1-sl: (ya2'=y2u) + sl: true; + [move] !meet & mem2=1 & !l2 & P2_1_0=2 -> 1-sl: (xa2'=x2r) + sl: true; + [move] !meet & mem2=1 & !l2 & P2_1_0=3 -> 1-sl: (ya2'=y2d) + sl: true; + [move] !meet & mem2=1 & !l2 & P2_1_0=4 -> 1-sl: (xa2'=x2l) + sl: true; + + [move] !meet & mem2=2 & l2 & P2_2_1=1 -> 1-sl: (ya2'=y2u) + sl: true; + [move] !meet & mem2=2 & l2 & P2_2_1=2 -> 1-sl: (xa2'=x2r) + sl: true; + [move] !meet & mem2=2 & l2 & P2_2_1=3 -> 1-sl: (ya2'=y2d) + sl: true; + [move] !meet & mem2=2 & l2 & P2_2_1=4 -> 1-sl: (xa2'=x2l) + sl: true; + + [move] !meet & mem2=2 & !l2 & P2_2_0=1 -> 1-sl: (ya2'=y2u) + sl: true; + [move] !meet & mem2=2 & !l2 & P2_2_0=2 -> 1-sl: (xa2'=x2r) + sl: true; + [move] !meet & mem2=2 & !l2 & P2_2_0=3 -> 1-sl: (ya2'=y2d) + sl: true; + [move] !meet & mem2=2 & !l2 & P2_2_0=4 -> 1-sl: (xa2'=x2l) + sl: true; +endmodule + + +// reward +rewards "moves" + !meet : -1; +endrewards + +formula meet = (xa1=xa2) & (ya1=ya2);