PRISM

Benchmark
Model:egl v.1 (DTMC)
Parameter(s)N = 10, L = 8
Property:messagesB (exp-reward)
Invocation (default)
./fix-syntax ./prism --javamaxmem 11g egl.prism egl.props --property messagesB -const N=10,L=8
Default settings.
Execution
Walltime:1431.4919621944427s
Return code:0
Relative Error:1.0751316283480098e-16
Log
PRISM
=====

Version: 4.4.dev
Date: Mon Dec 10 19:57:44 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g egl.prism egl.props --property messagesB -const 'N=10,L=8'

Parsing model file "egl.prism"...

Parsing properties file "egl.props"...

4 properties:
(1) "messagesA": R{"messages_A_needs"}=? [ F phase=4 ]
(2) "messagesB": R{"messages_B_needs"}=? [ F phase=4 ]
(3) "unfairA": P=? [ F !"knowA"&"knowB" ]
(4) "unfairB": P=? [ F !"knowB"&"knowA" ]

Type:        DTMC
Modules:     counter partyA partyB 
Variables:   b n phase party b0 b20 b1 b21 b2 b22 b3 b23 b4 b24 b5 b25 b6 b26 b7 b27 b8 b28 b9 b29 b10 b30 b11 b31 b12 b32 b13 b33 b14 b34 b15 b35 b16 b36 b17 b37 b18 b38 b19 b39 a0 a20 a1 a21 a2 a22 a3 a23 a4 a24 a5 a25 a6 a26 a7 a27 a8 a28 a9 a29 a10 a30 a11 a31 a12 a32 a13 a33 a14 a34 a15 a35 a16 a36 a17 a37 a18 a38 a19 a39 

---------------------------------------------------------------------

Model checking: "messagesB": R{"messages_B_needs"}=? [ F phase=4 ]
Model constants: N=10,L=8

Building model...
Model constants: N=10,L=8

Warning: Guard for command 11 of module "partyA" is never satisfied.

Warning: Guard for command 12 of module "partyA" is never satisfied.

Warning: Guard for command 13 of module "partyA" is never satisfied.

Warning: Guard for command 14 of module "partyA" is never satisfied.

Warning: Guard for command 15 of module "partyA" is never satisfied.

Warning: Guard for command 16 of module "partyA" is never satisfied.

Warning: Guard for command 17 of module "partyA" is never satisfied.

Warning: Guard for command 18 of module "partyA" is never satisfied.

Warning: Guard for command 19 of module "partyA" is never satisfied.

Warning: Guard for command 20 of module "partyA" is never satisfied.

Warning: Guard for command 31 of module "partyA" is never satisfied.

Warning: Guard for command 32 of module "partyA" is never satisfied.

Warning: Guard for command 33 of module "partyA" is never satisfied.

Warning: Guard for command 34 of module "partyA" is never satisfied.

Warning: Guard for command 35 of module "partyA" is never satisfied.

Warning: Guard for command 36 of module "partyA" is never satisfied.

Warning: Guard for command 37 of module "partyA" is never satisfied.

Warning: Guard for command 38 of module "partyA" is never satisfied.

Warning: Guard for command 39 of module "partyA" is never satisfied.

Warning: Guard for command 40 of module "partyA" is never satisfied.

Warning: Guard for command 51 of module "partyA" is never satisfied.

Warning: Guard for command 52 of module "partyA" is never satisfied.

Warning: Guard for command 53 of module "partyA" is never satisfied.

Warning: Guard for command 54 of module "partyA" is never satisfied.

Warning: Guard for command 55 of module "partyA" is never satisfied.

Warning: Guard for command 56 of module "partyA" is never satisfied.

Warning: Guard for command 57 of module "partyA" is never satisfied.

Warning: Guard for command 58 of module "partyA" is never satisfied.

Warning: Guard for command 59 of module "partyA" is never satisfied.

Warning: Guard for command 60 of module "partyA" is never satisfied.

Warning: Guard for command 11 of module "partyB" is never satisfied.

Warning: Guard for command 12 of module "partyB" is never satisfied.

Warning: Guard for command 13 of module "partyB" is never satisfied.

Warning: Guard for command 14 of module "partyB" is never satisfied.

Warning: Guard for command 15 of module "partyB" is never satisfied.

Warning: Guard for command 16 of module "partyB" is never satisfied.

Warning: Guard for command 17 of module "partyB" is never satisfied.

Warning: Guard for command 18 of module "partyB" is never satisfied.

Warning: Guard for command 19 of module "partyB" is never satisfied.

Warning: Guard for command 20 of module "partyB" is never satisfied.

Warning: Guard for command 31 of module "partyB" is never satisfied.

Warning: Guard for command 32 of module "partyB" is never satisfied.

Warning: Guard for command 33 of module "partyB" is never satisfied.

Warning: Guard for command 34 of module "partyB" is never satisfied.

Warning: Guard for command 35 of module "partyB" is never satisfied.

Warning: Guard for command 36 of module "partyB" is never satisfied.

Warning: Guard for command 37 of module "partyB" is never satisfied.

Warning: Guard for command 38 of module "partyB" is never satisfied.

Warning: Guard for command 39 of module "partyB" is never satisfied.

Warning: Guard for command 40 of module "partyB" is never satisfied.

Warning: Guard for command 51 of module "partyB" is never satisfied.

Warning: Guard for command 52 of module "partyB" is never satisfied.

Warning: Guard for command 53 of module "partyB" is never satisfied.

Warning: Guard for command 54 of module "partyB" is never satisfied.

Warning: Guard for command 55 of module "partyB" is never satisfied.

Warning: Guard for command 56 of module "partyB" is never satisfied.

Warning: Guard for command 57 of module "partyB" is never satisfied.

Warning: Guard for command 58 of module "partyB" is never satisfied.

Warning: Guard for command 59 of module "partyB" is never satisfied.

Warning: Guard for command 60 of module "partyB" is never satisfied.

Computing reachable states...

Reachability (BFS): 341 iterations in 3.66 seconds (average 0.010742, setup 0.00)

Time for model construction: 4.566 seconds.

Type:        DTMC
States:      317718526 (1 initial)
Transitions: 318767101

Transition matrix: 120213 nodes (3 terminal), 318767101 minterms, vars: 331r/331c

Prob0: 341 iterations in 3.36 seconds (average 0.009859, setup 0.00)

Prob1: 1 iterations in 0.00 seconds (average 0.004000, setup 0.00)

goal = 1, inf = 0, maybe = 317718525

Computing remaining rewards...
Engine: Hybrid

Building hybrid MTBDD matrix... [levels=331, nodes=120215] [5.5 MB]
Adding explicit sparse matrices... [levels=240, num=196, compact] [856.5 KB]
Creating vector for diagonals... [dist=1, compact] [606.0 MB]
Creating vector for RHS... [dist=2, compact] [606.0 MB]
Allocating iteration vectors... [2 x 2.4 GB]
TOTAL: [5.9 GB]

Starting iterations...
Iteration 2: max relative diff=1.000000, 7.24 sec so far
Iteration 4: max relative diff=1.000000, 14.38 sec so far
Iteration 6: max relative diff=1.000000, 21.54 sec so far
Iteration 8: max relative diff=1.000000, 28.71 sec so far
Iteration 10: max relative diff=1.000000, 35.88 sec so far
Iteration 12: max relative diff=1.000000, 43.04 sec so far
Iteration 14: max relative diff=1.000000, 50.22 sec so far
Iteration 16: max relative diff=1.000000, 57.37 sec so far
Iteration 18: max relative diff=1.000000, 64.53 sec so far
Iteration 20: max relative diff=1.000000, 71.69 sec so far
Iteration 22: max relative diff=1.000000, 78.86 sec so far
Iteration 24: max relative diff=1.000000, 85.96 sec so far
Iteration 26: max relative diff=1.000000, 93.10 sec so far
Iteration 28: max relative diff=1.000000, 100.24 sec so far
Iteration 30: max relative diff=1.000000, 107.39 sec so far
Iteration 32: max relative diff=1.000000, 114.53 sec so far
Iteration 34: max relative diff=1.000000, 121.68 sec so far
Iteration 36: max relative diff=1.000000, 128.78 sec so far
Iteration 38: max relative diff=1.000000, 135.89 sec so far
Iteration 40: max relative diff=1.000000, 143.00 sec so far
Iteration 42: max relative diff=1.000000, 150.11 sec so far
Iteration 44: max relative diff=1.000000, 157.21 sec so far
Iteration 46: max relative diff=1.000000, 164.34 sec so far
Iteration 48: max relative diff=1.000000, 171.45 sec so far
Iteration 50: max relative diff=1.000000, 178.55 sec so far
Iteration 52: max relative diff=1.000000, 185.68 sec so far
Iteration 54: max relative diff=1.000000, 192.78 sec so far
Iteration 56: max relative diff=1.000000, 199.88 sec so far
Iteration 58: max relative diff=1.000000, 206.98 sec so far
Iteration 60: max relative diff=1.000000, 214.09 sec so far
Iteration 62: max relative diff=1.000000, 221.18 sec so far
Iteration 64: max relative diff=1.000000, 228.29 sec so far
Iteration 66: max relative diff=1.000000, 235.39 sec so far
Iteration 68: max relative diff=1.000000, 242.50 sec so far
Iteration 70: max relative diff=1.000000, 249.60 sec so far
Iteration 72: max relative diff=1.000000, 256.70 sec so far
Iteration 74: max relative diff=1.000000, 263.81 sec so far
Iteration 76: max relative diff=1.000000, 270.91 sec so far
Iteration 78: max relative diff=1.000000, 278.01 sec so far
Iteration 80: max relative diff=1.000000, 285.11 sec so far
Iteration 82: max relative diff=1.000000, 292.22 sec so far
Iteration 84: max relative diff=1.000000, 299.32 sec so far
Iteration 86: max relative diff=1.000000, 306.43 sec so far
Iteration 88: max relative diff=1.000000, 313.53 sec so far
Iteration 90: max relative diff=1.000000, 320.63 sec so far
Iteration 92: max relative diff=1.000000, 327.73 sec so far
Iteration 94: max relative diff=1.000000, 334.82 sec so far
Iteration 96: max relative diff=1.000000, 341.91 sec so far
Iteration 98: max relative diff=1.000000, 349.01 sec so far
Iteration 100: max relative diff=1.000000, 356.11 sec so far
Iteration 102: max relative diff=1.000000, 363.21 sec so far
Iteration 104: max relative diff=1.000000, 370.30 sec so far
Iteration 106: max relative diff=1.000000, 377.39 sec so far
Iteration 108: max relative diff=1.000000, 384.49 sec so far
Iteration 110: max relative diff=1.000000, 391.58 sec so far
Iteration 112: max relative diff=1.000000, 398.70 sec so far
Iteration 114: max relative diff=1.000000, 405.79 sec so far
Iteration 116: max relative diff=1.000000, 412.89 sec so far
Iteration 118: max relative diff=1.000000, 419.99 sec so far
Iteration 120: max relative diff=1.000000, 427.10 sec so far
Iteration 122: max relative diff=1.000000, 434.19 sec so far
Iteration 124: max relative diff=1.000000, 441.29 sec so far
Iteration 126: max relative diff=1.000000, 448.39 sec so far
Iteration 128: max relative diff=1.000000, 455.50 sec so far
Iteration 130: max relative diff=1.000000, 462.60 sec so far
Iteration 132: max relative diff=1.000000, 469.70 sec so far
Iteration 134: max relative diff=1.000000, 476.80 sec so far
Iteration 136: max relative diff=1.000000, 483.92 sec so far
Iteration 138: max relative diff=1.000000, 491.01 sec so far
Iteration 140: max relative diff=1.000000, 498.11 sec so far
Iteration 142: max relative diff=1.000000, 505.21 sec so far
Iteration 144: max relative diff=1.000000, 512.31 sec so far
Iteration 146: max relative diff=1.000000, 519.40 sec so far
Iteration 148: max relative diff=1.000000, 526.49 sec so far
Iteration 150: max relative diff=1.000000, 533.58 sec so far
Iteration 152: max relative diff=1.000000, 540.66 sec so far
Iteration 154: max relative diff=1.000000, 547.76 sec so far
Iteration 156: max relative diff=1.000000, 554.84 sec so far
Iteration 158: max relative diff=1.000000, 561.92 sec so far
Iteration 160: max relative diff=1.000000, 569.00 sec so far
Iteration 162: max relative diff=1.000000, 576.07 sec so far
Iteration 164: max relative diff=0.500000, 583.15 sec so far
Iteration 166: max relative diff=0.250000, 590.23 sec so far
Iteration 168: max relative diff=0.166667, 597.31 sec so far
Iteration 170: max relative diff=0.125000, 604.39 sec so far
Iteration 172: max relative diff=0.100000, 611.48 sec so far
Iteration 174: max relative diff=0.090909, 618.56 sec so far
Iteration 176: max relative diff=0.090909, 625.65 sec so far
Iteration 178: max relative diff=0.090909, 632.74 sec so far
Iteration 180: max relative diff=0.090909, 639.82 sec so far
Iteration 182: max relative diff=0.090909, 646.92 sec so far
Iteration 184: max relative diff=0.083333, 654.10 sec so far
Iteration 186: max relative diff=0.071429, 661.26 sec so far
Iteration 188: max relative diff=0.062500, 668.39 sec so far
Iteration 190: max relative diff=0.055556, 675.57 sec so far
Iteration 192: max relative diff=0.050000, 682.72 sec so far
Iteration 194: max relative diff=0.047619, 689.85 sec so far
Iteration 196: max relative diff=0.047619, 696.97 sec so far
Iteration 198: max relative diff=0.047619, 704.21 sec so far
Iteration 200: max relative diff=0.047619, 711.39 sec so far
Iteration 202: max relative diff=0.047619, 718.56 sec so far
Iteration 204: max relative diff=0.045455, 725.73 sec so far
Iteration 206: max relative diff=0.041667, 732.84 sec so far
Iteration 208: max relative diff=0.038462, 739.99 sec so far
Iteration 210: max relative diff=0.035714, 747.12 sec so far
Iteration 212: max relative diff=0.033333, 754.27 sec so far
Iteration 214: max relative diff=0.032258, 761.36 sec so far
Iteration 216: max relative diff=0.032258, 768.43 sec so far
Iteration 218: max relative diff=0.032258, 775.51 sec so far
Iteration 220: max relative diff=0.032258, 782.65 sec so far
Iteration 222: max relative diff=0.032258, 789.77 sec so far
Iteration 224: max relative diff=0.031250, 796.96 sec so far
Iteration 226: max relative diff=0.029412, 804.12 sec so far
Iteration 228: max relative diff=0.027778, 811.25 sec so far
Iteration 230: max relative diff=0.026316, 818.39 sec so far
Iteration 232: max relative diff=0.025000, 825.51 sec so far
Iteration 234: max relative diff=0.024390, 832.62 sec so far
Iteration 236: max relative diff=0.024390, 839.72 sec so far
Iteration 238: max relative diff=0.024390, 846.85 sec so far
Iteration 240: max relative diff=0.024390, 853.93 sec so far
Iteration 242: max relative diff=0.024390, 861.08 sec so far
Iteration 244: max relative diff=0.023810, 868.18 sec so far
Iteration 246: max relative diff=0.022727, 875.29 sec so far
Iteration 248: max relative diff=0.021739, 882.40 sec so far
Iteration 250: max relative diff=0.020833, 889.49 sec so far
Iteration 252: max relative diff=0.020000, 896.59 sec so far
Iteration 254: max relative diff=0.019608, 903.66 sec so far
Iteration 256: max relative diff=0.019608, 910.75 sec so far
Iteration 258: max relative diff=0.019608, 917.83 sec so far
Iteration 260: max relative diff=0.019608, 924.91 sec so far
Iteration 262: max relative diff=0.019608, 931.99 sec so far
Iteration 264: max relative diff=0.019231, 939.09 sec so far
Iteration 266: max relative diff=0.018519, 946.18 sec so far
Iteration 268: max relative diff=0.017857, 953.28 sec so far
Iteration 270: max relative diff=0.017241, 960.39 sec so far
Iteration 272: max relative diff=0.016667, 967.49 sec so far
Iteration 274: max relative diff=0.016393, 974.57 sec so far
Iteration 276: max relative diff=0.016393, 981.77 sec so far
Iteration 278: max relative diff=0.016393, 988.87 sec so far
Iteration 280: max relative diff=0.016393, 996.00 sec so far
Iteration 282: max relative diff=0.016393, 1003.08 sec so far
Iteration 284: max relative diff=0.016129, 1010.16 sec so far
Iteration 286: max relative diff=0.015625, 1017.30 sec so far
Iteration 288: max relative diff=0.015152, 1024.47 sec so far
Iteration 290: max relative diff=0.014706, 1031.58 sec so far
Iteration 292: max relative diff=0.014286, 1038.68 sec so far
Iteration 294: max relative diff=0.013761, 1045.76 sec so far
Iteration 296: max relative diff=0.012281, 1052.88 sec so far
Iteration 298: max relative diff=0.009410, 1059.99 sec so far
Iteration 300: max relative diff=0.005842, 1067.09 sec so far
Iteration 302: max relative diff=0.003011, 1074.25 sec so far
Iteration 304: max relative diff=0.001395, 1081.44 sec so far
Iteration 306: max relative diff=0.000620, 1088.66 sec so far
Iteration 308: max relative diff=0.000273, 1095.78 sec so far
Iteration 310: max relative diff=0.000240, 1102.93 sec so far

Jacobi: 311 iterations in 1417.05 seconds (average 3.557797, setup 310.57)

Value in the initial state: 4.069269180297852

Time for model checking: 1426.2 seconds.

Result: 4.069269180297852 (value in the initial state)


Overall running time: 1431.236 seconds.

---------------------------------------------------------------------

Note: There were 60 warnings during computation.