PRISM

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

Version: 4.4.dev
Date: Mon Dec 10 19:55:15 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=2'

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=2

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

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): 101 iterations in 0.14 seconds (average 0.001386, setup 0.00)

Time for model construction: 0.397 seconds.

Type:        DTMC
States:      66060286 (1 initial)
Transitions: 67108861

Transition matrix: 18729 nodes (3 terminal), 67108861 minterms, vars: 169r/169c

Prob0: 101 iterations in 0.13 seconds (average 0.001277, setup 0.00)

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

goal = 1, inf = 0, maybe = 66060285

Computing remaining rewards...
Engine: Hybrid

Building hybrid MTBDD matrix... [levels=169, nodes=18672] [875.2 KB]
Adding explicit sparse matrices... [levels=128, num=72, compact] [868.5 KB]
Creating vector for diagonals... [dist=1, compact] [126.0 MB]
Creating vector for RHS... [dist=2, compact] [126.0 MB]
Allocating iteration vectors... [2 x 504.0 MB]
TOTAL: [1.2 GB]

Starting iterations...
Iteration 7: max relative diff=1.000000, 5.20 sec so far
Iteration 14: max relative diff=1.000000, 10.38 sec so far
Iteration 21: max relative diff=1.000000, 15.59 sec so far
Iteration 28: max relative diff=1.000000, 20.78 sec so far
Iteration 35: max relative diff=1.000000, 25.91 sec so far
Iteration 42: max relative diff=1.000000, 31.03 sec so far
Iteration 49: max relative diff=0.142857, 36.15 sec so far
Iteration 56: max relative diff=0.046667, 41.28 sec so far
Iteration 63: max relative diff=0.002998, 46.40 sec so far
Iteration 70: max relative diff=0.000243, 51.51 sec so far

Jacobi: 71 iterations in 88.26 seconds (average 0.735789, setup 36.02)

Value in the initial state: 4.010732650756836

Time for model checking: 89.567 seconds.

Result: 4.010732650756836 (value in the initial state)


Overall running time: 90.41 seconds.

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

Note: There were 60 warnings during computation.