Scaling Up Logico-Numerical Strategy Iteration
Tested max-strategy improvement algorithms:
GS'07: for each boolean state and each template row: test non-visited strategies
GM'11: for each boolean state and each template row: test all non-visited strategies at once
n: for each template row: test strategies for all boolean states at once by naive model enumeration
g: for each template row: test strategies for all boolean states at once by model generalisation
m: for each template row: test strategies for all boolean states at once by two-layered model enumeration generalisation
s: test strategies for all boolean states and all template rows at once by model enumeration
n: for each template row: test strategies for all boolean states at once by model enumeration and retesting successful models
Comparison between Max-Strategy Iteration and Widening-Based Techniques
Examples
| | state vars | input vars | CFG | max-strategy iteration | std.analysis | abs.accel. |
| template | bool. | num. | bool. | num. | locs | arcs | GS'07 | GM'11 | g | s | (wid.delay=2,desc.=2) | (wid.delay=2,desc.=2) |
| Traffic 1 | BOX | 6 | 6 | 0 | 0 | 18 | 61 | 2.160 | 2.104 | 2.328 | 2.164 | 1.224 | 0.428 |
| Traffic 2 | ZONE | 6 | 8 | 0 | 0 | 18 | 151 | 121.756 | 114.387 | 108.047 | 96.978 | 3.492 | 2.856 |
| Traffic 3 | ZONE | 8 | 8 | 1 | 0 | 50 | 619 | 674.062 | 640.220 | 356.93 | 328.93 | 22.077 | 19.170 |
| Thermostat 1 | BOX | 4 | 3 | 0 | 2 | 6 | 15 | 0.360 | 0.320 | 0.284 | 0.264 | 0.820 | 0.852 |
| Thermostat 2 | BOX | 6 | 5 | 0 | 4 | 18 | 145 | 16.801 | 15.109 | 3.440 | 3.228 | 26.626 | 30.398 |
| Thermostat 3 | BOX | 8 | 7 | 0 | 6 | 66 | 1357 | 720.205 | 715.353 | 66.520 | 61.880 | 674.182 | 907.889 |
| Window 1 | OCT | 9 | 5 | 5 | 0 | 21 | 120 | 109.283 | 102.318 | 70.740 | 73.433 | 4.568 | 4.696 |
| Window 2 | OCT | 11 | 5 | 6 | 0 | 45 | 452 | 393.901 | 371.511 | 189.096 | 286.318 | 18.573 | 23.493 |
| Window 3 | OCT | 13 | 5 | 7 | 0 | 81 | 1388 | 1412.444 | 1220.348 | 241.669 | 697.368 | 70.176 | 93.510 |
| Drugpump 1 | INT | 4 | 10 | 4 | 1 | 6 | 231 | 92.602 | 90.318 | 6.052 | 4.553 | 209.963 | 119.655 |
| Drugpump 2 | INT | 7 | 12 | 8 | 1 | 34 | 11201 | o.o.mem. | o.o.mem. | 149.463 | 95.457 | >1800 | >1800 |
| Drugpump 3 | INT | 10 | 14 | 8 | 1 | 146 | 112561 | o.o.mem. | o.o.mem. | 1019.348 | o.o.mem. | >1800 | >1800 |
Comparison between Various Variants of the Max-Strategy-Improvement Algorithm
Examples
| state vars | input vars | CFG | octagonal templates | box templates |
| bool. | num. | bool. | num. | locs | arcs | GS'07 | GM'11 | n | g | m | s | t | GS'07 | GM'11 | n | g | m | s | t |
| simple loop 1 | 3 | 2 | 0 | 0 | 4 | 9 | 0.164 | 0.128 | 0.112 | 0.116 | 0.148 | 0.108 | 0.120 | 0.100 | 0.104 | 0.088 | 0.080 | 0.092 | 0.080 | 0.092 |
| simple loop 2 | 4 | 2 | 1 | 0 | 6 | 24 | 0.368 | 0.280 | 0.116 | 0.104 | 0.136 | 0.136 | 0.124 | 0.204 | 0.196 | 0.084 | 0.072 | 0.092 | 0.072 | 0.088 |
| simple loop 3 | 5 | 2 | 2 | 0 | 10 | 72 | 1.044 | 0.776 | 0.144 | 0.140 | 0.176 | 0.144 | 0.176 | 0.588 | 0.456 | 0.112 | 0.088 | 0.108 | 0.112 | 0.132 |
| simple loop 4 | 6 | 2 | 3 | 0 | 18 | 240 | 3.456 | 2.560 | 0.232 | 0.112 | 0.160 | 0.236 | 0.260 | 2.064 | 1.452 | 0.244 | 0.080 | 0.116 | 0.220 | 0.244 |
| simple loop 5 | 7 | 2 | 4 | 0 | 34 | 864 | 13.377 | 9.353 | 0.596 | 0.120 | 0.184 | 0.552 | 0.628 | 7.952 | 5.632 | 0.776 | 0.096 | 0.152 | 0.636 | 0.680 |
| simple loop 6 | 8 | 2 | 5 | 0 | 66 | 3264 | 49.835 | 36.642 | 2.328 | 0.112 | 0.248 | 1.728 | 1.988 | 32.830 | 21.585 | 3.456 | 0.088 | 0.196 | 2.160 | 2.536 |
| simple loop 7 | 9 | 2 | 6 | 0 | 130 | 12672 | 222.642 | 177.515 | 11.161 | 0.124 | 0.376 | 6.872 | 7.904 | 143.901 | 101.278 | 19.105 | 0.080 | 0.316 | 8.041 | 10.925 |
| simple loop 8 | 10 | 2 | 7 | 0 | 258 | 49920 | >300 | >300 | 71.676 | 0.132 | 0.672 | 27.194 | 32.134 | >300 | >300 | 135.036 | 0.100 | 0.620 | 37.418 | 49.831 |
| simple loop 9 | 11 | 2 | 8 | 0 | ? | ? | >300 | >300 | >300 | 0.124 | 0.712 | >300 | >300 | >300 | >300 | >300 | 0.092 | 1.436 | >300 | >300 |
| simple loop 10 | 12 | 2 | 9 | 0 | ? | ? | >300 | >300 | >300 | 0.132 | 4.448 | >300 | >300 | >300 | >300 | >300 | 0.100 | 4.048 | >300 | >300 |
| simple loop 11 | 13 | 2 | 10 | 0 | ? | ? | >300 | >300 | >300 | 0.140 | 15.153 | >300 | >300 | >300 | >300 | >300 | 0.116 | 12.297 | >300 | >300 |
| simple loop 12 | 14 | 2 | 11 | 0 | ? | ? | >300 | >300 | >300 | 0.160 | 63.560 | >300 | >300 | >300 | >300 | >300 | 0.152 | 49.615 | >300 | >300 |
| simple loop 13 | 15 | 2 | 12 | 0 | ? | ? | >300 | >300 | >300 | 0.208 | >300 | >300 | >300 | >300 | >300 | >300 | 0.212 | 259.248 | >300 | >300 |
| simple loop 14 | 16 | 2 | 13 | 0 | ? | ? | >300 | >300 | >300 | 0.308 | >300 | >300 | >300 | >300 | >300 | >300 | 0.360 | >300 | >300 | >300 |
| simple loop 15 | 17 | 2 | 14 | 0 | ? | ? | >300 | >300 | >300 | 0.568 | >300 | >300 | >300 | >300 | >300 | >300 | 0.788 | >300 | >300 | >300 |
| simple loop 16 | 18 | 2 | 15 | 0 | ? | ? | >300 | >300 | >300 | 1.204 | >300 | >300 | >300 | >300 | >300 | >300 | 2.416 | >300 | >300 | >300 |
| nested loop 1 1 | 4 | 3 | 0 | 0 | 5 | 21 | 1.812 | 1.344 | 0.908 | 0.936 | 1.308 | 0.968 | 0.952 | 0.432 | 0.320 | 0.180 | 0.156 | 0.216 | 0.164 | 0.172 |
| nested loop 1 2 | 5 | 3 | 1 | 0 | 8 | 52 | 4.408 | 3.484 | 0.976 | 0.952 | 1.312 | 1.028 | 1.000 | 1.084 | 0.732 | 0.180 | 0.164 | 0.216 | 0.176 | 0.180 |
| nested loop 1 3 | 6 | 3 | 2 | 0 | 14 | 144 | 12.633 | 9.625 | 1.184 | 0.956 | 1.364 | 1.252 | 1.184 | 3.068 | 2.072 | 0.236 | 0.180 | 0.224 | 0.228 | 0.228 |
| nested loop 1 4 | 7 | 3 | 3 | 0 | 26 | 448 | 39.166 | 30.970 | 1.868 | 0.960 | 1.404 | 1.864 | 1.824 | 9.969 | 6.796 | 0.412 | 0.176 | 0.244 | 0.384 | 0.400 |
| nested loop 1 5 | 8 | 3 | 4 | 0 | 50 | 1536 | 133.004 | 107.539 | 4.708 | 0.964 | 1.500 | 3.788 | 3.820 | 34.910 | 24.126 | 1.080 | 0.172 | 0.272 | 0.916 | 0.996 |
| nested loop 1 6 | 9 | 3 | 5 | 0 | 98 | 5632 | >300 | >300 | 18.189 | 0.952 | 1.732 | 11.005 | 11.581 | 139.845 | 100.022 | 4.148 | 0.180 | 0.356 | 3.072 | 3.256 |
| nested loop 1 7 | 10 | 3 | 6 | 0 | 194 | 21504 | >300 | >300 | 105.175 | 0.972 | 2.228 | 41.491 | 43.471 | >300 | >300 | 18.701 | 0.184 | 0.512 | 11.501 | 12.901 |
| nested loop 1 8 | 11 | 3 | 7 | 0 | 386 | 82560 | >300 | >300 | >300 | 0.984 | 3.436 | 165.058 | 186.376 | >300 | >300 | 109.187 | 0.184 | 0.868 | 49.507 | 56.464 |
| nested loop 1 9 | 12 | 3 | 8 | 0 | ? | ? | >300 | >300 | >300 | 0.992 | 6.896 | >300 | >300 | >300 | >300 | >300 | 0.196 | 1.944 | >300 | >300 |
| nested loop 1 10 | 13 | 3 | 9 | 0 | ? | ? | >300 | >300 | >300 | 0.988 | 17.233 | >300 | >300 | >300 | >300 | >300 | 0.216 | 5.116 | >300 | >300 |
| nested loop 1 11 | 14 | 3 | 10 | 0 | ? | ? | >300 | >300 | >300 | 1.020 | 52.719 | >300 | >300 | >300 | >300 | >300 | 0.236 | 15.757 | >300 | >300 |
| nested loop 1 12 | 15 | 3 | 11 | 0 | ? | ? | >300 | >300 | >300 | 1.056 | 223.750 | >300 | >300 | >300 | >300 | >300 | 0.264 | 64.388 | >300 | >300 |
| nested loop 1 13 | 16 | 3 | 12 | 0 | ? | ? | >300 | >300 | >300 | 1.148 | >300 | >300 | >300 | >300 | >300 | >300 | 0.344 | >300 | >300 | >300 |
| nested loop 1 14 | 17 | 3 | 13 | 0 | ? | ? | >300 | >300 | >300 | 1.364 | >300 | >300 | >300 | >300 | >300 | >300 | 0.560 | >300 | >300 | >300
|
| nested loop 1 15 | 18 | 3 | 14 | 0 | ? | ? | >300 | >300 | >300 | 1.888 | >300 | >300 | >300 | >300 | >300 | >300 | 1.028 | >300 | >300 | >300 |
| nested loop 1 16 | 19 | 3 | 15 | 0 | ? | ? | >300 | >300 | >300 | 4.116 | >300 | >300 | >300 | >300 | >300 | >300 | 2.748 | >300 | >300 | >300 |
| nested loop 2 1 | 4 | 4 | 0 | 0 | 6 | 43 | 13.933 | 11.841 | 8.109 | 8.645 | 10.653 | 8.553 | 8.201 | 2.012 | 1.484 | 0.360 | 0.352 | 0.496 | 0.344 | 0.364 |
| nested loop 2 2 | 5 | 4 | 1 | 0 | 10 | 100 | 34.130 | 30.194 | 8.509 | 8.501 | 10.613 | 8.993 | 8.449 | 4.720 | 3.596 | 0.376 | 0.364 | 0.488 | 0.380 | 0.400 |
| nested loop 2 3 | 6 | 4 | 2 | 0 | 18 | 256 | 91.426 | 80.149 | 9.445 | 8.461 | 10.737 | 9.777 | 9.049 | 12.841 | 9.837 | 0.484 | 0.392 | 0.496 | 0.476 | 0.488 |
| nested loop 2 4 | 7 | 4 | 3 | 0 | 34 | 736 | >300 | 249.816 | 11.833 | 8.537 | 10.817 | 11.773 | 10.753 | 38.374 | 29.478 | 0.816 | 0.364 | 0.532 | 0.768 | 0.824 |
| nested loop 2 5 | 8 | 4 | 4 | 0 | 66 | 2368 | >300 | >300 | 21.937 | 8.417 | 11.213 | 18.181 | 16.673 | 127.716 | 103.662 | 2.180 | 0.375 | 0.616 | 1.836 | 1.952 |
| nested loop 2 6 | 9 | 4 | 5 | 0 | 130 | 8320 | >300 | >300 | 70.052 | 8.533 | 11.789 | 40.675 | 38.322 | >300 | >300 | 8.089 | 0.376 | 0.712 | 5.916 | 6.280 |
| nested loop 2 7 | 10 | 4 | 6 | 0 | 258 | 30976 | >300 | >300 | >300 | 8.461 | 13.081 | 129.668 | 128.584 | >300 | >300 | 38.654 | 0.404 | 0.984 | 22.409 | 24.626 |
| nested loop 2 8 | 11 | 4 | 7 | 0 | 514 | 115328 | >300 | >300 | >300 | 8.545 | 16.105 | >300 | >300 | >300 | >300 | 258.096 | 0.396 | 1.628 | 97.883 | 108.387 |
| nested loop 2 9 | 12 | 4 | 8 | 0 | ? | ? | >300 | >300 | >300 | 8.545 | 24.650 | >300 | >300 | >300 | >300 | >300 | 0.412 | 3.348 | >300 | >300 |
| nested loop 2 10 | 13 | 4 | 9 | 0 | ? | ? | >300 | >300 | >300 | 8.605 | 49.371 | >300 | >300 | >300 | >300 | >300 | 0.420 | 9.101 | >300 | >300 |
| nested loop 2 11 | 14 | 4 | 10 | 0 | ? | ? | >300 | >300 | >300 | 8.629 | 135.972 | >300 | >300 | >300 | >300 | >300 | 0.444 | 27.014 | >300 | >300 |
| nested loop 2 12 | 15 | 4 | 11 | 0 | ? | ? | >300 | >300 | >300 | 8.709 | >300 | >300 | >300 | >300 | >300 | >300 | 0.492 | 108.011 | >300 | >300 |
| nested loop 2 13 | 16 | 4 | 12 | 0 | ? | ? | >300 | >300 | >300 | 8.765 | >300 | >300 | >300 | >300 | >300 | >300 | 0.616 | >300 | >300 | >300 |
| nested loop 2 14 | 17 | 4 | 13 | 0 | ? | ? | >300 | >300 | >300 | 9.129 | >300 | >300 | >300 | >300 | >300 | >300 | 0.888 | >300 | >300 | >300 |
| nested loop 2 15 | 18 | 4 | 14 | 0 | ? | ? | >300 | >300 | >300 | 9.885 | >300 | >300 | >300 | >300 | >300 | >300 | 1.596 | >300 | >300 | >300 |
| nested loop 2 16 | 19 | 4 | 15 | 0 | ? | ? | >300 | >300 | >300 | 12.721 | >300 | >300 | >300 | >300 | >300 | >300 | 3.972 | >300 | >300 | >300 |