PRISM

Benchmark
Model:bluetooth v.1 (DTMC)
Parameter(s)mrec = 1
Property:time (exp-reward)
Invocation (default)
./fix-syntax ./prism --javamaxmem 11g bluetooth.prism bluetooth.props --property time -const mrec=1
Default settings.
Execution
Walltime:13.64305830001831s
Return code:0
Relative Error:0.0
Log
PRISM
=====

Version: 4.4.dev
Date: Mon Dec 10 19:53:54 CET 2018
Hostname: qcomp2019
Memory limits: cudd=1g, java(heap)=1g
Command line: prism --javamaxmem 11g bluetooth.prism bluetooth.props --property time -const mrec=1

Parsing model file "bluetooth.prism"...

Parsing properties file "bluetooth.props"...

1 property:
(1) "time": filter(max, R=? [ F rec=mrec ], "init")

Type:        DTMC
Modules:     receiver1 frequency1 sender_frequency replies 
Variables:   y1 receiver freq1 train1 z1 f1 t1 send freq train c rep rec 

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

Model checking: "time": filter(max, R=? [ F rec=mrec ], "init")
Model constants: mrec=1

Building model...
Model constants: mrec=1

Computing reachable states...

Reachability (BFS): 50 iterations in 0.16 seconds (average 0.003160, setup 0.00)

Time for model construction: 11.904 seconds.

Type:        DTMC
States:      3411945339 (536870912 initial)
Transitions: 5035263739

Transition matrix: 14727 nodes (4 terminal), 5035263739 minterms, vars: 52r/52c

Warning: Switching to MTBDD engine, as number of states is too large for Hybrid engine.

Prob0: 49 iterations in 0.25 seconds (average 0.005143, setup 0.00)

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

goal = 1636000575, inf = 0, maybe = 1775944764

Computing remaining rewards...
Engine: MTBDD

Iteration matrix MTBDD... [nodes=11441] [223.5 Kb]
Diagonals MTBDD... [nodes=4425] [86.4 Kb]

Starting iterations...

Jacobi: 47 iterations in 0.55 seconds (average 0.011553, setup 0.01)

Maximum value over states satisfying filter: 8229.0

There are 32768 states with (approximately) this value.
The first 10 states are displayed below. To view them all, enable verbose mode or use a print filter.
4479:(0,0,0,0,1,1,0,1,2,0,3,128,0)
4735:(0,0,0,0,1,1,0,1,2,0,5,128,0)
4991:(0,0,0,0,1,1,0,1,2,0,7,128,0)
5247:(0,0,0,0,1,1,0,1,2,0,9,128,0)
5503:(0,0,0,0,1,1,0,1,2,0,11,128,0)
5759:(0,0,0,0,1,1,0,1,2,0,13,128,0)
6015:(0,0,0,0,1,1,0,1,2,0,15,128,0)
6271:(0,0,0,0,1,1,0,1,2,1,1,128,0)
233777:(0,0,0,0,2,1,0,1,2,0,3,128,0)
234033:(0,0,0,0,2,1,0,1,2,0,5,128,0)

Time for model checking: 0.847 seconds.

Result: 8229.0 (maximum value over states satisfying filter)


Overall running time: 13.346 seconds.

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

Note: There was 1 warning during computation.