PRISM
=====
Version: 4.4.dev
Date: Mon Dec 10 20:33:35 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g nand.prism nand.props --property reliable -const 'N=60,K=4'
Parsing model file "nand.prism"...
Parsing properties file "nand.props"...
1 property:
(1) "reliable": P=? [ F s=4&z/N<0.1 ]
Type: DTMC
Modules: multiplex
Variables: u c s z zx zy x y
---------------------------------------------------------------------
Model checking: "reliable": P=? [ F s=4&z/N<0.1 ]
Model constants: N=60,K=4
Building model...
Model constants: N=60,K=4
Computing reachable states...
Reachability (BFS): 2162 iterations in 12.26 seconds (average 0.005672, setup 0.00)
Time for model construction: 12.75 seconds.
Type: DTMC
States: 18826082 (1 initial)
Transitions: 29772212
Transition matrix: 97452 nodes (1103 terminal), 29772212 minterms, vars: 33r/33c
Prob0: 2162 iterations in 10.62 seconds (average 0.004914, setup 0.00)
Prob1: 1945 iterations in 9.96 seconds (average 0.005123, setup 0.00)
yes = 547, no = 1757695, maybe = 17067840
Computing remaining probabilities...
Engine: Hybrid
Building hybrid MTBDD matrix... [levels=33, nodes=136740] [6.3 MB]
Adding explicit sparse matrices... [levels=14, num=365, compact] [769.2 KB]
Creating vector for diagonals... [dist=1, compact] [35.9 MB]
Creating vector for RHS... [dist=2, compact] [35.9 MB]
Allocating iteration vectors... [2 x 143.6 MB]
TOTAL: [366.1 MB]
Starting iterations...
Iteration 21: max relative diff=1.000000, 5.09 sec so far
Iteration 42: max relative diff=1.000000, 10.19 sec so far
Iteration 63: max relative diff=1.000000, 15.27 sec so far
Iteration 84: max relative diff=1.000000, 20.34 sec so far
Iteration 105: max relative diff=1.000000, 25.49 sec so far
Iteration 126: max relative diff=1.000000, 30.57 sec so far
Iteration 147: max relative diff=1.000000, 35.63 sec so far
Iteration 168: max relative diff=1.000000, 40.70 sec so far
Iteration 189: max relative diff=1.000000, 45.81 sec so far
Iteration 210: max relative diff=1.000000, 50.92 sec so far
Iteration 231: max relative diff=1.000000, 56.00 sec so far
Iteration 252: max relative diff=1.000000, 61.09 sec so far
Iteration 273: max relative diff=1.000000, 66.20 sec so far
Iteration 294: max relative diff=1.000000, 71.32 sec so far
Iteration 315: max relative diff=1.000000, 76.39 sec so far
Iteration 336: max relative diff=1.000000, 81.47 sec so far
Iteration 357: max relative diff=1.000000, 86.53 sec so far
Iteration 378: max relative diff=1.000000, 91.60 sec so far
Iteration 399: max relative diff=1.000000, 96.68 sec so far
Iteration 420: max relative diff=1.000000, 101.74 sec so far
Iteration 441: max relative diff=1.000000, 106.82 sec so far
Iteration 462: max relative diff=1.000000, 111.89 sec so far
Iteration 483: max relative diff=1.000000, 116.94 sec so far
Iteration 504: max relative diff=1.000000, 122.01 sec so far
Iteration 525: max relative diff=1.000000, 127.07 sec so far
Iteration 546: max relative diff=1.000000, 132.14 sec so far
Iteration 567: max relative diff=1.000000, 137.21 sec so far
Iteration 588: max relative diff=1.000000, 142.28 sec so far
Iteration 609: max relative diff=1.000000, 147.36 sec so far
Iteration 630: max relative diff=1.000000, 152.44 sec so far
Iteration 651: max relative diff=1.000000, 157.52 sec so far
Iteration 672: max relative diff=1.000000, 162.59 sec so far
Iteration 693: max relative diff=1.000000, 167.66 sec so far
Iteration 714: max relative diff=1.000000, 172.78 sec so far
Iteration 735: max relative diff=1.000000, 177.85 sec so far
Iteration 756: max relative diff=1.000000, 182.92 sec so far
Iteration 777: max relative diff=1.000000, 187.99 sec so far
Iteration 798: max relative diff=1.000000, 193.06 sec so far
Iteration 819: max relative diff=1.000000, 198.13 sec so far
Iteration 840: max relative diff=1.000000, 203.20 sec so far
Iteration 861: max relative diff=1.000000, 208.27 sec so far
Iteration 882: max relative diff=1.000000, 213.34 sec so far
Iteration 903: max relative diff=1.000000, 218.41 sec so far
Iteration 924: max relative diff=1.000000, 223.48 sec so far
Iteration 945: max relative diff=1.000000, 228.55 sec so far
Iteration 966: max relative diff=1.000000, 233.61 sec so far
Iteration 987: max relative diff=1.000000, 238.68 sec so far
Iteration 1008: max relative diff=1.000000, 243.75 sec so far
Iteration 1029: max relative diff=1.000000, 248.83 sec so far
Iteration 1050: max relative diff=1.000000, 253.91 sec so far
Iteration 1071: max relative diff=1.000000, 259.00 sec so far
Iteration 1092: max relative diff=1.000000, 264.11 sec so far
Iteration 1113: max relative diff=1.000000, 269.20 sec so far
Iteration 1134: max relative diff=1.000000, 274.30 sec so far
Iteration 1155: max relative diff=1.000000, 279.42 sec so far
Iteration 1176: max relative diff=1.000000, 284.51 sec so far
Iteration 1197: max relative diff=1.000000, 289.58 sec so far
Iteration 1218: max relative diff=1.000000, 294.75 sec so far
Iteration 1239: max relative diff=1.000000, 299.85 sec so far
Iteration 1260: max relative diff=1.000000, 304.97 sec so far
Iteration 1281: max relative diff=1.000000, 310.09 sec so far
Iteration 1302: max relative diff=1.000000, 315.22 sec so far
Iteration 1323: max relative diff=1.000000, 320.32 sec so far
Iteration 1344: max relative diff=1.000000, 325.46 sec so far
Iteration 1365: max relative diff=1.000000, 330.58 sec so far
Iteration 1386: max relative diff=1.000000, 335.71 sec so far
Iteration 1407: max relative diff=1.000000, 340.81 sec so far
Iteration 1428: max relative diff=1.000000, 345.90 sec so far
Iteration 1449: max relative diff=1.000000, 351.05 sec so far
Iteration 1470: max relative diff=1.000000, 356.16 sec so far
Iteration 1491: max relative diff=1.000000, 361.28 sec so far
Iteration 1512: max relative diff=1.000000, 366.42 sec so far
Iteration 1533: max relative diff=1.000000, 371.50 sec so far
Iteration 1554: max relative diff=1.000000, 376.58 sec so far
Iteration 1575: max relative diff=1.000000, 381.65 sec so far
Iteration 1596: max relative diff=1.000000, 386.73 sec so far
Iteration 1617: max relative diff=1.000000, 391.82 sec so far
Iteration 1638: max relative diff=1.000000, 396.91 sec so far
Iteration 1659: max relative diff=1.000000, 401.99 sec so far
Iteration 1680: max relative diff=1.000000, 407.10 sec so far
Iteration 1701: max relative diff=1.000000, 412.20 sec so far
Iteration 1722: max relative diff=1.000000, 417.27 sec so far
Iteration 1743: max relative diff=1.000000, 422.37 sec so far
Iteration 1764: max relative diff=1.000000, 427.45 sec so far
Iteration 1785: max relative diff=1.000000, 432.56 sec so far
Iteration 1806: max relative diff=1.000000, 437.65 sec so far
Iteration 1827: max relative diff=1.000000, 442.75 sec so far
Iteration 1848: max relative diff=1.000000, 447.83 sec so far
Iteration 1869: max relative diff=1.000000, 452.92 sec so far
Iteration 1890: max relative diff=1.000000, 458.00 sec so far
Iteration 1911: max relative diff=1.000000, 463.10 sec so far
Iteration 1932: max relative diff=1.000000, 468.19 sec so far
Iteration 1953: max relative diff=1.000000, 473.30 sec so far
Iteration 1974: max relative diff=1.000000, 478.37 sec so far
Iteration 1995: max relative diff=1.000000, 483.44 sec so far
Iteration 2016: max relative diff=1.000000, 488.58 sec so far
Iteration 2037: max relative diff=1.000000, 493.68 sec so far
Iteration 2058: max relative diff=1.000000, 498.77 sec so far
Iteration 2079: max relative diff=1.000000, 503.85 sec so far
Iteration 2100: max relative diff=1.000000, 508.98 sec so far
Iteration 2121: max relative diff=1.000000, 514.08 sec so far
Iteration 2142: max relative diff=0.712139, 519.16 sec so far
Jacobi: 2161 iterations in 531.46 seconds (average 0.242366, setup 7.71)
Value in the initial state: 0.6867214589192238
Time for model checking: 553.143 seconds.
Result: 0.6867214589192238 (value in the initial state)
Overall running time: 566.316 seconds.