Storm

Benchmark
Model:bluetooth v.1 (DTMC)
Parameter(s)mrec = 1
Property:time (exp-reward)
Invocation (specific)
~/storm/build/bin/storm --prism bluetooth.prism --prop bluetooth.props time --constants mrec=1 --engine dd --ddlib sylvan --sylvan:maxmem 9000
Dd engine with sylvan. Memory limit for sylvan set to 0.75*available memory.
Execution
Walltime:10.97769284248352s
Return code:0
Relative Error:0.0
Log
Storm 1.3.1 (dev)

Date: Wed Dec 12 17:51:28 2018
Command line arguments: --prism bluetooth.prism --prop bluetooth.props time --constants mrec=1 --engine dd --ddlib sylvan '--sylvan:maxmem' 9000
Current working directory: /home/qcomp

Time for model input parsing: 0.017s.

Time for model construction: 9.903s.

-------------------------------------------------------------- 
Model type: 	DTMC (symbolic)
States: 	3411945339 (4393 nodes)
Transitions: 	5035263739 (14727 nodes)
Reward Models:  time
Variables: 	rows: 13 meta variables (52 DD variables), columns: 13 meta variables (52 DD variables)
Labels: 	2
   * deadlock -> 0 state(s) (1 nodes)
   * init -> 536870912 state(s) (27 nodes)
-------------------------------------------------------------- 

Model checking property "time": R[exp]=? [F (rec = 1)] ...
Result (for initial states): 8229
Time for model checking: 0.431s.