epmc - nand reliable 60-4

Log
running-epmc-revision bcbb8ed631893b5fa072e28d29126ca3ba5337e0
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property reliable
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 60472 60472
build-model-states-explored 200908 140435
build-model-states-explored 346221 145313
build-model-states-explored 502013 155793
build-model-states-explored 636314 134301
build-model-states-explored 789679 153365
build-model-states-explored 942189 152509
build-model-states-explored 1062360 120172
build-model-states-explored 1221832 159472
build-model-states-explored 1375651 153819
build-model-states-explored 1533180 157529
build-model-states-explored 1677701 144520
build-model-states-explored 1839254 161554
build-model-states-explored 1997313 158058
build-model-states-explored 2097152 99840
build-model-states-explored 2222518 125366
build-model-states-explored 2383023 160504
build-model-states-explored 2544158 161136
build-model-states-explored 2688968 144810
build-model-states-explored 2849457 160489
build-model-states-explored 3007511 158053
build-model-states-explored 3170269 162758
build-model-states-explored 3294771 124502
build-model-states-explored 3453044 158273
build-model-states-explored 3611206 158162
build-model-states-explored 3771437 160231
build-model-states-explored 3934696 163259
build-model-states-explored 4089963 155267
build-model-states-explored 4194304 104342
build-model-states-explored 4223550 29245
build-model-states-explored 4385846 162296
build-model-states-explored 4543281 157435
build-model-states-explored 4702343 159061
build-model-states-explored 4863534 161190
build-model-states-explored 5023148 159614
build-model-states-explored 5182504 159357
build-model-states-explored 5317413 134908
build-model-states-explored 5472692 155278
build-model-states-explored 5629444 156752
build-model-states-explored 5787298 157855
build-model-states-explored 5945207 157909
build-model-states-explored 6102502 157294
build-model-states-explored 6258260 155758
build-model-states-explored 6422351 164091
build-model-states-explored 6574224 151874
build-model-states-explored 6677504 103279
build-model-states-explored 6836667 159163
build-model-states-explored 6995923 159257
build-model-states-explored 7157285 161362
build-model-states-explored 7317679 160393
build-model-states-explored 7477417 159737
build-model-states-explored 7630503 153087
build-model-states-explored 7795059 164555
build-model-states-explored 7955036 159977
build-model-states-explored 8113512 158476
build-model-states-explored 8271995 158483
build-model-states-explored 8388608 116614
build-model-states-explored 8388608 0
build-model-states-explored 8388608 0
build-model-states-explored 8531499 142890
build-model-states-explored 8691514 160015
build-model-states-explored 8849257 157744
build-model-states-explored 9008717 159460
build-model-states-explored 9168776 160058
build-model-states-explored 9326652 157876
build-model-states-explored 9487488 160837
build-model-states-explored 9644823 157334
build-model-states-explored 9798906 154083
build-model-states-explored 9959384 160477
build-model-states-explored 10111942 152558
build-model-states-explored 10266730 154787
build-model-states-explored 10422875 156144
build-model-states-explored 10570447 147573
build-model-states-explored 10698489 128041
build-model-states-explored 10854823 156334
build-model-states-explored 11009765 154943
build-model-states-explored 11164081 154315
build-model-states-explored 11321423 157343
build-model-states-explored 11481857 160434
build-model-states-explored 11638342 156483
build-model-states-explored 11816462 178122
build-model-states-explored 11991499 175037
build-model-states-explored 12167161 175661
build-model-states-explored 12338349 171188
build-model-states-explored 12517337 178988
build-model-states-explored 12688320 170983
build-model-states-explored 12861690 173370
build-model-states-explored 13042577 180887
build-model-states-explored 13140555 97978
build-model-states-explored 13274486 133930
build-model-states-explored 13444109 169623
build-model-states-explored 13620209 176101
build-model-states-explored 13798771 178562
build-model-states-explored 13974454 175683
build-model-states-explored 14152087 177632
build-model-states-explored 14330692 178605
build-model-states-explored 14502692 172000
build-model-states-explored 14679483 176791
build-model-states-explored 14861299 181816
build-model-states-explored 15033766 172467
build-model-states-explored 15206170 172403
build-model-states-explored 15386314 180143
build-model-states-explored 15563188 176874
build-model-states-explored 15733041 169853
build-model-states-explored 15911342 178301
build-model-states-explored 16089503 178161
build-model-states-explored 16266878 177376
build-model-states-explored 16442558 175680
build-model-states-explored 16622017 179458
build-model-states-explored 16777216 155200
build-model-states-explored 16777216 0
build-model-states-explored 16777216 0
build-model-states-explored 16777216 0
build-model-states-explored 16777216 0
build-model-states-explored 16884080 106863
build-model-states-explored 17060135 176055
build-model-states-explored 17232249 172115
build-model-states-explored 17404666 172416
build-model-states-explored 17587470 182804
build-model-states-explored 17763051 175581
build-model-states-explored 17935077 172026
build-model-states-explored 18114986 179910
build-model-states-explored 18288737 173750
build-model-states-explored 18463094 174358
build-model-states-explored 18639165 176070
build-model-states-explored 18815557 176392
build-model-done 18826082 126
iterating
iterating-progress-unbounded 3 1.0 1
iterating-progress-unbounded 11 1.0 2
iterating-progress-unbounded 19 1.0 3
iterating-progress-unbounded 28 0.9999999995596799 4
iterating-progress-unbounded 36 0.9999999948956702 5
iterating-progress-unbounded 44 0.9999999728792586 6
iterating-progress-unbounded 52 0.999999902683124 7
iterating-progress-unbounded 60 0.999999725781042 8
iterating-progress-unbounded 68 0.9999993449001345 9
iterating-progress-unbounded 76 0.9999986124322358 10
iterating-progress-unbounded 84 0.9999973187283085 11
iterating-progress-unbounded 92 0.9999951806265993 12
iterating-progress-unbounded 101 0.9999895604197674 13
iterating-progress-unbounded 109 0.9999834933056793 14
iterating-progress-unbounded 117 0.9999748609239351 15
iterating-progress-unbounded 125 0.9999629260801226 16
iterating-progress-unbounded 133 0.9999468293003525 17
iterating-progress-unbounded 141 0.9999255836306689 18
iterating-progress-unbounded 149 0.9998980707059159 19
iterating-progress-unbounded 157 0.9998630380893541 20
iterating-progress-unbounded 165 0.9998190978655579 21
iterating-progress-unbounded 173 0.9997647264534882 22
iterating-progress-unbounded 181 0.999698265593764 23
iterating-progress-unbounded 190 0.9996179244537422 24
iterating-progress-unbounded 198 0.9995217827857854 25
iterating-progress-unbounded 206 0.9994077950677667 26
iterating-progress-unbounded 214 0.9992737955502329 27
iterating-progress-unbounded 222 0.9991175041314683 28
iterating-progress-unbounded 230 0.9989365329798184 29
iterating-progress-unbounded 238 0.9987283938218424 30
iterating-progress-unbounded 246 0.9975838529550849 31
iterating-progress-unbounded 254 0.9960732821429653 32
iterating-progress-unbounded 262 0.9941889129304883 33
iterating-progress-unbounded 270 0.9919254836255017 34
iterating-progress-unbounded 278 0.9892800088999637 35
iterating-progress-unbounded 286 0.9862515651362083 36
iterating-progress-unbounded 294 0.9828410905882023 37
iterating-progress-unbounded 302 0.9790511994780421 38
iterating-progress-unbounded 310 0.9748860091956166 39
iterating-progress-unbounded 318 0.9703509798146358 40
iterating-progress-unbounded 326 0.965452765181165 41
iterating-progress-unbounded 335 0.960199074871562 42
iterating-progress-unbounded 343 0.9545985463553762 43
iterating-progress-unbounded 351 0.9486606267354373 44
iterating-progress-unbounded 359 0.942395463472147 45
iterating-progress-unbounded 367 0.9358138035319664 46
iterating-progress-unbounded 375 0.928926900431368 47
iterating-progress-unbounded 383 0.9217464286771645 48
iterating-progress-unbounded 391 0.9142844051322329 49
iterating-progress-unbounded 399 0.9065531168622836 50
iterating-progress-unbounded 407 0.8985650550445587 51
iterating-progress-unbounded 415 0.8903328545432587 52
iterating-progress-unbounded 423 0.8818692387791437 53
iterating-progress-unbounded 431 0.8731869695422042 54
iterating-progress-unbounded 439 0.8642988014166191 55
iterating-progress-unbounded 447 0.8552174405064408 56
iterating-progress-unbounded 455 0.8459555071686619 57
iterating-progress-unbounded 463 0.8365255024775449 58
iterating-progress-unbounded 471 0.8269397781604064 59
iterating-progress-unbounded 479 0.8172105097604683 60
iterating-progress-unbounded 487 0.8170511491313984 61
iterating-progress-unbounded 495 0.8168792109611082 62
iterating-progress-unbounded 503 0.8166946779750736 63
iterating-progress-unbounded 511 0.8164975323751074 64
iterating-progress-unbounded 519 0.8162877558544314 65
iterating-progress-unbounded 527 0.8160653296130878 66
iterating-progress-unbounded 535 0.8158302343736823 67
iterating-progress-unbounded 543 0.8155824503974554 68
iterating-progress-unbounded 551 0.8153219575006774 69
iterating-progress-unbounded 559 0.8150487350713622 70
iterating-progress-unbounded 567 0.8147627620862931 71
iterating-progress-unbounded 575 0.8144640171283576 72
iterating-progress-unbounded 583 0.8141524784041853 73
iterating-progress-unbounded 591 0.8138281237620804 74
iterating-progress-unbounded 599 0.8134909307102479 75
iterating-progress-unbounded 607 0.8131408764353042 76
iterating-progress-unbounded 616 0.8127779378210657 77
iterating-progress-unbounded 624 0.8124020914676117 78
iterating-progress-unbounded 632 0.8120133137106134 79
iterating-progress-unbounded 639 0.8116115806409223 80
iterating-progress-unbounded 647 0.8111968681244126 81
iterating-progress-unbounded 655 0.8107691518220691 82
iterating-progress-unbounded 663 0.8103284072103151 83
iterating-progress-unbounded 671 0.8098746096015716 84
iterating-progress-unbounded 679 0.8094077341650425 85
iterating-progress-unbounded 688 0.8089277559477154 86
iterating-progress-unbounded 696 0.8084346498955737 87
iterating-progress-unbounded 703 0.8079283908750093 88
iterating-progress-unbounded 711 0.8074089536944308 89
iterating-progress-unbounded 719 0.8068763131260562 90
iterating-progress-unbounded 727 0.8055444178536709 91
iterating-progress-unbounded 735 0.8041643809604161 92
iterating-progress-unbounded 743 0.8027362068890609 93
iterating-progress-unbounded 751 0.801259913491408 94
iterating-progress-unbounded 759 0.7997355322961316 95
iterating-progress-unbounded 767 0.7981631087549211 96
iterating-progress-unbounded 776 0.7965427024670464 97
iterating-progress-unbounded 784 0.7948743873824821 98
iterating-progress-unbounded 792 0.7931582519837663 99
iterating-progress-unbounded 799 0.7913943994467872 100
iterating-progress-unbounded 807 0.7895829477807257 101
iterating-progress-unbounded 815 0.7877240299474013 102
iterating-progress-unbounded 823 0.7858177939602966 103
iterating-progress-unbounded 831 0.7838644029635544 104
iterating-progress-unbounded 839 0.781864035291264 105
iterating-progress-unbounded 847 0.7798168845073771 106
iterating-progress-unbounded 855 0.7777231594266019 107
iterating-progress-unbounded 863 0.7755830841166562 108
iterating-progress-unbounded 871 0.7733968978822618 109
iterating-progress-unbounded 879 0.771164855231289 110
iterating-progress-unbounded 887 0.7688872258234668 111
iterating-progress-unbounded 895 0.7665642944020901 112
iterating-progress-unbounded 903 0.7641963607091672 113
iterating-progress-unbounded 911 0.7617837393844591 114
iterating-progress-unbounded 919 0.7593267598488751 115
iterating-progress-unbounded 927 0.756825766172694 116
iterating-progress-unbounded 935 0.754281116929091 117
iterating-progress-unbounded 943 0.7516931850334532 118
iterating-progress-unbounded 951 0.7490623575689765 119
iterating-progress-unbounded 959 0.746389035599038 120
iterating-progress-unbounded 967 0.7463452289379023 121
iterating-progress-unbounded 975 0.7462979622227831 122
iterating-progress-unbounded 983 0.7462472300250964 123
iterating-progress-unbounded 991 0.7461930267105402 124
iterating-progress-unbounded 999 0.7461353464396442 125
iterating-progress-unbounded 1007 0.7460741831683387 126
iterating-progress-unbounded 1015 0.746009530648541 127
iterating-progress-unbounded 1023 0.745941382428759 128
iterating-progress-unbounded 1031 0.7458697318547132 129
iterating-progress-unbounded 1039 0.7457945720699765 130
iterating-progress-unbounded 1047 0.7457158960166329 131
iterating-progress-unbounded 1055 0.7456336964359547 132
iterating-progress-unbounded 1063 0.7455479658690982 133
iterating-progress-unbounded 1070 0.7454586966578192 134
iterating-progress-unbounded 1078 0.7453658809452066 135
iterating-progress-unbounded 1086 0.7452695106764375 136
iterating-progress-unbounded 1094 0.7451695775995505 137
iterating-progress-unbounded 1102 0.7450660732662391 138
iterating-progress-unbounded 1110 0.7449589890326667 139
iterating-progress-unbounded 1118 0.7448483160603002 140
iterating-progress-unbounded 1126 0.7447340453167666 141
iterating-progress-unbounded 1134 0.7446161675767282 142
iterating-progress-unbounded 1142 0.7444946734227814 143
iterating-progress-unbounded 1150 0.744369553246375 144
iterating-progress-unbounded 1158 0.7442407972487515 145
iterating-progress-unbounded 1166 0.7441083954419103 146
iterating-progress-unbounded 1174 0.7439723376495924 147
iterating-progress-unbounded 1182 0.7438326135082884 148
iterating-progress-unbounded 1190 0.743689212468269 149
iterating-progress-unbounded 1198 0.7435421237946384 150
iterating-progress-unbounded 1206 0.7431731729438688 151
iterating-progress-unbounded 1214 0.7427903170673772 152
iterating-progress-unbounded 1222 0.7423934750473488 153
iterating-progress-unbounded 1230 0.7419825649680214 154
iterating-progress-unbounded 1237 0.7415575041807144 155
iterating-progress-unbounded 1245 0.7411182093694834 156
iterating-progress-unbounded 1253 0.740664596617368 157
iterating-progress-unbounded 1261 0.7401965814732087 158
iterating-progress-unbounded 1269 0.739714079018998 159
iterating-progress-unbounded 1277 0.7392170039377409 160
iterating-progress-unbounded 1285 0.7387052705817878 161
iterating-progress-unbounded 1293 0.7381787930416077 162
iterating-progress-unbounded 1301 0.7376374852149726 163
iterating-progress-unbounded 1309 0.7370812608765122 164
iterating-progress-unbounded 1317 0.7365100337476075 165
iterating-progress-unbounded 1325 0.735923717566586 166
iterating-progress-unbounded 1333 0.7353222261591813 167
iterating-progress-unbounded 1341 0.734705473509219 168
iterating-progress-unbounded 1349 0.7340733738294921 169
iterating-progress-unbounded 1357 0.7334258416327852 170
iterating-progress-unbounded 1365 0.7327627918030083 171
iterating-progress-unbounded 1372 0.7324254212959421 172
iterating-progress-unbounded 1380 0.7317389364109652 173
iterating-progress-unbounded 1388 0.7310367231937058 174
iterating-progress-unbounded 1396 0.7303186983878358 175
iterating-progress-unbounded 1404 0.7295847794285312 176
iterating-progress-unbounded 1412 0.7288348845134814 177
iterating-progress-unbounded 1420 0.7280689326737432 178
iterating-progress-unbounded 1428 0.7272868438443917 179
iterating-progress-unbounded 1436 0.7264885389349303 180
iterating-progress-unbounded 1444 0.7260767968914178 181
iterating-progress-unbounded 1452 0.7260630439250847 182
iterating-progress-unbounded 1459 0.7260482429505218 183
iterating-progress-unbounded 1467 0.7260323918264852 184
iterating-progress-unbounded 1475 0.7260154883291758 185
iterating-progress-unbounded 1483 0.7259975301521417 186
iterating-progress-unbounded 1491 0.7259785149061757 187
iterating-progress-unbounded 1499 0.7259584401192125 188
iterating-progress-unbounded 1507 0.7259373032362229 189
iterating-progress-unbounded 1515 0.7259151016191056 190
iterating-progress-unbounded 1523 0.7258918325465777 191
iterating-progress-unbounded 1531 0.7258674932140625 192
iterating-progress-unbounded 1539 0.7258420807335746 193
iterating-progress-unbounded 1546 0.7258155921336045 194
iterating-progress-unbounded 1554 0.7257880243589995 195
iterating-progress-unbounded 1562 0.7257593742708439 196
iterating-progress-unbounded 1570 0.7257296386463358 197
iterating-progress-unbounded 1578 0.7256988141786637 198
iterating-progress-unbounded 1586 0.7256668974768794 199
iterating-progress-unbounded 1594 0.7256338850657706 200
iterating-progress-unbounded 1602 0.7255997733857299 201
iterating-progress-unbounded 1610 0.7255645587926234 202
iterating-progress-unbounded 1618 0.7255282375576575 203
iterating-progress-unbounded 1625 0.7254908058672425 204
iterating-progress-unbounded 1633 0.7254522598228561 205
iterating-progress-unbounded 1641 0.7254125954409043 206
iterating-progress-unbounded 1649 0.7253718086525809 207
iterating-progress-unbounded 1657 0.7253298953037255 208
iterating-progress-unbounded 1665 0.7252868511546795 209
iterating-progress-unbounded 1673 0.7252426718801412 210
iterating-progress-unbounded 1681 0.7251643748189535 211
iterating-progress-unbounded 1689 0.7250495211728318 212
iterating-progress-unbounded 1696 0.7249904379423928 213
iterating-progress-unbounded 1704 0.7248689333505669 214
iterating-progress-unbounded 1712 0.7247429435217866 215
iterating-progress-unbounded 1720 0.72461242641579 216
iterating-progress-unbounded 1728 0.724477339121669 217
iterating-progress-unbounded 1736 0.7243376378626363 218
iterating-progress-unbounded 1744 0.7241932780009912 219
iterating-progress-unbounded 1752 0.7240442140432894 220
iterating-progress-unbounded 1760 0.7238903996457255 221
iterating-progress-unbounded 1767 0.7237317876197387 222
iterating-progress-unbounded 1775 0.7235683299378446 223
iterating-progress-unbounded 1783 0.7233999777397074 224
iterating-progress-unbounded 1791 0.7232266813384554 225
iterating-progress-unbounded 1799 0.7230483902272484 226
iterating-progress-unbounded 1807 0.7228650530861085 227
iterating-progress-unbounded 1815 0.7226766177890149 228
iterating-progress-unbounded 1823 0.7224830314112772 229
iterating-progress-unbounded 1831 0.7222842402371895 230
iterating-progress-unbounded 1838 0.7220801897679743 231
iterating-progress-unbounded 1846 0.7218708247300235 232
iterating-progress-unbounded 1854 0.7216560890834421 233
iterating-progress-unbounded 1862 0.7214359260309021 234
iterating-progress-unbounded 1870 0.7212102780268124 235
iterating-progress-unbounded 1878 0.7209790867868109 236
iterating-progress-unbounded 1886 0.7207422932975862 237
iterating-progress-unbounded 1893 0.7204998378270322 238
iterating-progress-unbounded 1901 0.7202516599347427 239
iterating-progress-unbounded 1909 0.7199976984828513 240
iterating-progress-unbounded 1917 0.7197378916472209 241
iterating-progress-unbounded 1925 0.7197137946803001 242
iterating-progress-unbounded 1933 0.7196437324907152 243
iterating-progress-unbounded 1941 0.719538190868676 244
iterating-progress-unbounded 1949 0.7193959906297068 245
iterating-progress-unbounded 1956 0.7192259030406889 246
iterating-progress-unbounded 1964 0.7190075610593929 247
iterating-progress-unbounded 1972 0.7187471031023493 248
iterating-progress-unbounded 1980 0.7184419564140072 249
iterating-progress-unbounded 1988 0.7180891505016782 250
iterating-progress-unbounded 1996 0.7176852931401546 251
iterating-progress-unbounded 2004 0.7172265432169368 252
iterating-progress-unbounded 2012 0.716708580323139 253
iterating-progress-unbounded 2019 0.7161265710334557 254
iterating-progress-unbounded 2027 0.7154751318731072 255
iterating-progress-unbounded 2035 0.7147482890432034 256
iterating-progress-unbounded 2043 0.7139394350713879 257
iterating-progress-unbounded 2051 0.7130412826747399 258
iterating-progress-unbounded 2059 0.7120458162692682 259
iterating-progress-unbounded 2067 0.7109442417368863 260
iterating-progress-unbounded 2074 0.7099932022353419 261
iterating-progress-unbounded 2082 0.7086771879051186 262
iterating-progress-unbounded 2090 0.707225993835378 263
iterating-progress-unbounded 2098 0.7056274192377362 264
iterating-progress-unbounded 2106 0.7038682534982899 265
iterating-progress-unbounded 2114 0.7019342401596307 266
iterating-progress-unbounded 2122 0.6998100500761382 267
iterating-progress-unbounded 2130 0.6974792665015028 268
iterating-progress-unbounded 2137 0.6955561148891318 269
iterating-progress-unbounded 2145 0.6928182227515381 270
iterating-progress-unbounded 2153 0.689822814216666 271
iterating-progress-unbounded 2161 0.0 272
iterating-done 2162 272
model-checking-done 431
reliable: 0.6867214589192253
Model:	nand v.1 (DTMC)
Parameter(s)	N = 60, K = 4
Property:	reliable (prob-reach)
Walltime:	432.75370717048645s
Return code:	0
Relative Error:	7.572997465301528e-15