PRISM

Benchmark
Model:zeroconf v.1 (MDP)
Parameter(s)N = 1000, K = 8, reset = False
Property:correct_max (prob-reach)
Invocation (specific)
./fix-syntax ./prism --javamaxmem 11g zeroconf.prism zeroconf.props --property correct_max -const N=1000,K=8,reset=false 
Use default settings
Execution
Walltime:194.60747957229614s
Return code:0
Relative Error:1.1108812419475163e-15
Log
PRISM
=====

Version: 4.4.dev
Date: Tue Dec 11 01:48:57 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g zeroconf.prism zeroconf.props --property correct_max -const 'N=1000,K=8,reset=false'

Parsing model file "zeroconf.prism"...

Parsing properties file "zeroconf.props"...

2 properties:
(1) "correct_max": Pmax=? [ F (l=4&ip=1) ]
(2) "correct_min": Pmin=? [ F (l=4&ip=1) ]

Type:        MDP
Modules:     environment host0 
Variables:   b_ip7 b_ip6 b_ip5 b_ip4 b_ip3 b_ip2 b_ip1 b_ip0 n n0 n1 b z ip_mess x y coll probes mess defend ip l 

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

Model checking: "correct_max": Pmax=? [ F (l=4&ip=1) ]
Model constants: reset=false,N=1000,K=8

Building model...
Model constants: reset=false,N=1000,K=8

Computing reachable states...

Reachability (BFS): 592 iterations in 68.34 seconds (average 0.115448, setup 0.00)

Time for model construction: 69.243 seconds.

Type:        MDP
States:      1870338 (1 initial)
Transitions: 4245554
Choices:     3443961

Transition matrix: 154038 nodes (6 terminal), 4245554 minterms, vars: 58r/58c/7nd

Prob0A: 131 iterations in 4.08 seconds (average 0.031137, setup 0.00)

Prob1E: 2127 iterations in 91.46 seconds (average 0.042999, setup 0.00)

yes = 171749, no = 611330, maybe = 1087259

Computing remaining probabilities...
Engine: Hybrid

Building hybrid MTBDD matrices... [nm=9, levels=58, nodes=272480] [12.5 MB]
Adding sparse bits... [levels=24-43, num=4846, compact=9/9] [8.0 MB]
Creating vector for yes... [dist=2, compact] [3.6 MB]
Allocating iteration vectors... [3 x 14.3 MB]
TOTAL: [66.8 MB]

Starting iterations...
Iteration 60: max relative diff=1.000000, 5.05 sec so far
Iteration 120: max relative diff=1.000000, 10.12 sec so far
Iteration 180: max relative diff=0.000983, 15.18 sec so far
Iteration 240: max relative diff=0.000056, 20.21 sec so far
Iteration 300: max relative diff=0.000010, 25.24 sec so far

Iterative method: 311 iterations in 28.71 seconds (average 0.084096, setup 2.56)

Value in the initial state: 4.801413635072425E-8

Time for model checking: 124.483 seconds.

Result: 4.801413635072425E-8 (value in the initial state)


Overall running time: 194.223 seconds.