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.