CSL Model Checking by PRISM, log file ====================================== Property constants: K=0 b1 = 8915 states, b2 = 15150 states Diagonals vector: Embedded Markov chain: Prob1: 8 iterations in 0.03 seconds (average 0.003750, setup 0.00) yes = 24065, no = 0, maybe = 0 Warning: The filter {RafP=K} is satisfied by 8915 states. The result of model checking is for the first of these: 0:(0,0,1,0,0,3,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,3,true) Time for model checking: 2.764 seconds. Result: 1.0 Model checking: P=? [ (RafP=K) U (RafP>K) {RafP=K} ] Model constants: k=1 Property constants: K=1 b1 = 7195 states, b2 = 7955 states Diagonals vector: Embedded Markov chain: Prob1: 11 iterations in 0.04 seconds (average 0.003636, setup 0.00) Prob0: 3 iterations in 0.00 seconds (average 0.000000, setup 0.00) yes = 7955, no = 8915, maybe = 7195 Computing remaining probabilities... Building hybrid MTBDD matrix... [levels=67, nodes=480661] [11265.5 KB] Adding explicit sparse matrices... [levels=67, num=1, compact] [319.4 KB] Creating vector for diagonals... [dist=1, compact] [47.0 KB] Creating vector for RHS... [dist=2, compact] [47.0 KB] Allocating iteration vectors... [2 x 188.0 KB] TOTAL: [12055.0 KB] Starting iterations... Jacobi: 188 iterations in 367.38 seconds (average 0.003197, setup 366.78) Warning: The filter {RafP=K} is satisfied by 7195 states. The result of model checking is for the first of these: 1205:(0,0,1,1,1,2,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,3,true) Time for model checking: 371.564 seconds. Result: 0.7999410110827223 Model checking: P=? [ (RafP=K) U (RafP>K) {RafP=K} ] Model constants: k=1 Property constants: K=2 b1 = 4785 states, b2 = 3170 states Diagonals vector: Embedded Markov chain: Prob1: 8 iterations in 0.04 seconds (average 0.005000, setup 0.00) Prob0: 3 iterations in 0.01 seconds (average 0.003333, setup 0.00) yes = 3170, no = 16110, maybe = 4785 Computing remaining probabilities... Building hybrid MTBDD matrix... [levels=67, nodes=238881] [5598.8 KB] Adding explicit sparse matrices... [levels=67, num=1, compact] [206.2 KB] Creating vector for diagonals... [dist=1, compact] [47.0 KB] Creating vector for RHS... [dist=2, compact] [47.0 KB] Allocating iteration vectors... [2 x 188.0 KB] TOTAL: [6275.0 KB] Starting iterations... Jacobi: 129 iterations in 71.68 seconds (average 0.003574, setup 71.22) Warning: The filter {RafP=K} is satisfied by 4785 states. The result of model checking is for the first of these: 2410:(0,0,1,2,2,1,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,3,true) Time for model checking: 74.968 seconds. Result: 0.48449278218721503 Model checking: P=? [ (RafP=K) U (RafP>K) {RafP=K} ] Model constants: k=1 Property constants: K=3 b1 = 2480 states, b2 = 690 states Diagonals vector: Embedded Markov chain: Prob1: 8 iterations in 0.01 seconds (average 0.001250, setup 0.00) Prob0: 3 iterations in 0.01 seconds (average 0.003333, setup 0.00) yes = 690, no = 20895, maybe = 2480 Computing remaining probabilities... Building hybrid MTBDD matrix... [levels=67, nodes=175434] [4111.7 KB] Adding explicit sparse matrices... [levels=67, num=1, compact] [119.3 KB] Creating vector for diagonals... [dist=1, compact] [47.0 KB] Creating vector for RHS... [dist=2, compact] [47.0 KB] Allocating iteration vectors... [2 x 188.0 KB] TOTAL: [4701.1 KB] Starting iterations... Jacobi: 100 iterations in 34.41 seconds (average 0.003210, setup 34.09) Warning: The filter {RafP=K} is satisfied by 2480 states. The result of model checking is for the first of these: 3510:(0,0,1,3,3,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,3,true) Time for model checking: 35.941 seconds. Result: 0.07369095800612555 Model checking: P=? [ (RafP=K) U (RafP>K) {RafP=K} ] Model constants: k=1 Property constants: K=4 b1 = 690 states, b2 = 0 states Diagonals vector: Embedded Markov chain: yes = 0, no = 24065, maybe = 0 Warning: The filter {RafP=K} is satisfied by 690 states. The result of model checking is for the first of these: 8225:(0,1,0,4,3,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,3,true) Time for model checking: 0.992 seconds. Result: 0.0 Model constants: k=1 Building model... Computing reachable states... Reachability: 37 iterations in 0.32 seconds (average 0.008649, setup 0.00) Time for model construction: 1.182 seconds. States: 24065 (1 initial) Transitions: 206007 Rate matrix: 13693 nodes (30 terminal), 206007 minterms, vars: 67r/67c State rewards (0): 1122 nodes (5 terminal), 15150 minterms Model checking: P=? [ ((MEKPP=0) & (ERKPP=0)) U (RafP=K) {(MEKPP=0) & (ERKPP=0) & (RafP=0)} ] Model constants: k=1 Property constants: K=0 b1 = 10748 states, b2 = 8915 states Diagonals vector: Embedded Markov chain: Prob1: 37 iterations in 0.20 seconds (average 0.005405, setup 0.00) Prob0: 6 iterations in 0.01 seconds (average 0.001667, setup 0.00) yes = 8915, no = 8438, maybe = 6712 Computing remaining probabilities... Building hybrid MTBDD matrix... [levels=67, nodes=458675] [10750.2 KB] Adding explicit sparse matrices... [levels=67, num=1, compact] [279.3 KB] Creating vector for diagonals... [dist=1, compact] [47.0 KB] Creating vector for RHS... [dist=2, compact] [47.0 KB] Allocating iteration vectors... [2 x 188.0 KB] TOTAL: [11499.6 KB] Starting iterations... Jacobi: 329 iterations in 313.50 seconds (average 0.001644, setup 312.96) Warning: The filter {(MEKPP=0) & (ERKPP=0) & (RafP=0)} is satisfied by 4036 states. The result of model checking is for the first of these: 0:(0,0,1,0,0,3,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,3,true) Time for model checking: 317.166 seconds. Result: 1.0 Model checking: P=? [ ((MEKPP=0) & (ERKPP=0)) U (RafP=K) {(MEKPP=0) & (ERKPP=0) & (RafP=0)} ] Model constants: k=1 Property constants: K=1 b1 = 10748 states, b2 = 7195 states Diagonals vector: Embedded Markov chain: Prob1: 36 iterations in 0.18 seconds (average 0.005000, setup 0.00) Prob0: 4 iterations in 0.01 seconds (average 0.002500, setup 0.00) yes = 8245, no = 9346, maybe = 6474 Computing remaining probabilities... Building hybrid MTBDD matrix... [levels=67, nodes=396479] [9292.5 KB] Adding explicit sparse matrices... [levels=67, num=1, compact] [252.2 KB] Creating vector for diagonals... [dist=1, compact] [47.0 KB] Creating vector for RHS... [dist=2, compact] [47.0 KB] Allocating iteration vectors... [2 x 188.0 KB] TOTAL: [10014.8 KB] Starting iterations... Jacobi: 164 iterations in 206.45 seconds (average 0.001713, setup 206.17) Warning: The filter {(MEKPP=0) & (ERKPP=0) & (RafP=0)} is satisfied by 4036 states. The result of model checking is for the first of these: 0:(0,0,1,0,0,3,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,3,true) Time for model checking: 209.381 seconds. Result: 1.0 Model checking: P=? [ ((MEKPP=0) & (ERKPP=0)) U (RafP=K) {(MEKPP=0) & (ERKPP=0) & (RafP=0)} ] Model constants: k=1 Property constants: K=2 b1 = 10748 states, b2 = 4785 states Diagonals vector: Embedded Markov chain: Prob1: 40 iterations in 0.35 seconds (average 0.008750, setup 0.00) Prob0: 5 iterations in 0.01 seconds (average 0.002000, setup 0.00) yes = 4785, no = 10652, maybe = 8628 Computing remaining probabilities... Building hybrid MTBDD matrix... [levels=67, nodes=502308] [11772.8 KB] Adding explicit sparse matrices... [levels=67, num=1, compact] [332.4 KB] Creating vector for diagonals... [dist=1, compact] [47.0 KB] Creating vector for RHS... [dist=2, compact] [47.0 KB] Allocating iteration vectors... [2 x 188.0 KB] TOTAL: [12575.3 KB] Starting iterations... Jacobi: 509 iterations in 344.97 seconds (average 0.002458, setup 343.71) Warning: The filter {(MEKPP=0) & (ERKPP=0) & (RafP=0)} is satisfied by 4036 states. The result of model checking is for the first of these: 0:(0,0,1,0,0,3,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,3,true) Time for model checking: 347.419 seconds. Result: 0.9678639355066638 Model checking: P=? [ ((MEKPP=0) & (ERKPP=0)) U (RafP=K) {(MEKPP=0) & (ERKPP=0) & (RafP=0)} ] Model constants: k=1 Property constants: K=3 b1 = 10748 states, b2 = 2480 states Diagonals vector: Embedded Markov chain: Prob1: 44 iterations in 0.19 seconds (average 0.004318, setup 0.00) Prob0: 7 iterations in 0.02 seconds (average 0.002857, setup 0.00) yes = 2540, no = 11913, maybe = 9612 Computing remaining probabilities... Building hybrid MTBDD matrix... [levels=67, nodes=500232] [11724.2 KB] Adding explicit sparse matrices... [levels=67, num=1, compact] [368.0 KB] Creating vector for diagonals... [dist=1, compact] [47.0 KB] Creating vector for RHS... [dist=2, compact] [47.0 KB] Allocating iteration vectors... [2 x 188.0 KB] TOTAL: [12562.2 KB] Starting iterations... Jacobi: 863 iterations in 337.04 seconds (average 0.002379, setup 334.99) Warning: The filter {(MEKPP=0) & (ERKPP=0) & (RafP=0)} is satisfied by 4036 states. The result of model checking is for the first of these: 0:(0,0,1,0,0,3,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,3,true) Time for model checking: 342.052 seconds. Result: 0.7156993338640533 Model checking: P=? [ ((MEKPP=0) & (ERKPP=0)) U (RafP=K) {(MEKPP=0) & (ERKPP=0) & (RafP=0)} ] Model constants: k=1 Property constants: K=4 b1 = 10748 states, b2 = 690 states Diagonals vector: Embedded Markov chain: Prob1: 50 iterations in 0.21 seconds (average 0.004220, setup 0.00) Prob0: 9 iterations in 0.01 seconds (average 0.001111, setup 0.00) yes = 690, no = 12919, maybe = 10456 Computing remaining probabilities... Building hybrid MTBDD matrix... [levels=67, nodes=553736] [12978.2 KB] Adding explicit sparse matrices... [levels=67, num=1, compact] [398.7 KB] Creating vector for diagonals... [dist=1, compact] [47.0 KB] Creating vector for RHS... [dist=2, compact] [47.0 KB] Allocating iteration vectors... [2 x 188.0 KB] TOTAL: [13846.9 KB] Starting iterations... Jacobi: 1118 iterations in 423.80 seconds (average 0.002401, setup 421.12) Warning: The filter {(MEKPP=0) & (ERKPP=0) & (RafP=0)} is satisfied by 4036 states. The result of model checking is for the first of these: 0:(0,0,1,0,0,3,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,3,true) Time for model checking: 427.425 seconds. Result: 0.1892541640985339