Storm.exact

Benchmark
Model:stream v.1 (MA)
Parameter(s)N = 1000
Property:exp_buffertime (exp-reward)
Invocation (exact)
/home/tq429871/storm/build/bin/storm --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ma/stream/stream.ma --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ma/stream/stream.csl exp_buffertime --constants N=1000 --exact --timemem
Sparse engine with exact model checking
Execution
Walltime:25.6359760761261s
Return code:0
Relative Error:1.1629814174600902e-29
Log
Storm 1.6.2

Date: Sat Sep  5 20:48:00 2020
Command line arguments: --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ma/stream/stream.ma --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/ma/stream/stream.csl exp_buffertime --constants N=1000 --exact --timemem
Current working directory: /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks

Time for model input parsing: 0.002s.

Time for model construction: 12.745s.

-------------------------------------------------------------- 
Model type: 	Markov Automaton (sparse)
States: 	1502501
Transitions: 	3001001
Choices: 	2002001
Markovian St.: 	1001001
Max. Rate.: 	8
Reward Models:  buffering
State Labels: 	3 labels
   * deadlock -> 0 item(s)
   * done -> 1 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Time for model preprocessing: 0.018s.

-------------------------------------------------------------- 
Model type: 	Markov Automaton (sparse)
States: 	1502501
Transitions: 	3001001
Choices: 	2002001
Markovian St.: 	1001001
Max. Rate.: 	8
Reward Models:  buffering
State Labels: 	3 labels
   * deadlock -> 0 item(s)
   * done -> 1 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "exp_buffertime": R[exp]{"buffering"}min=? [F "done"] ...
Result (for initial states): 4000296146463847098310864263634423914836767359338666081680434839202633176175944835603384754262910558987235871718746140024248987886727587484410249120643089020630884563738907513961936570219758813042355246319131762815388815989618440516494797219018946754993629191203712330205282342959267185327074343139033487340401390100903833079370568060213520613067377809755496713965444996024304117384475854000536382644863605857104782047725418570659881778080987601337412396108392474119605527990269896939414251339208175004932615431994404792059880640511653620458797873644746281859191934262699791320138884720183523420213125/448488552841505673528450469210032025008717852378396562686579194072564945856394653850257611842385261686892954937104477645877780844087130988838254436002598900543476520098876093752690543547812675279019246054935493143678185404868704546669207132970571695198847642805321870347439959396966061131000641492071612036500659800720541037509294862530914292581776470704800791862135257150476594266547973795942452669207838277325767258308678827571890789686926497076331599351180046564667803842147156402969070145377463213888204787436429748157612446950906462925450296030791504591545034378214229573507677553758534574800896 (approx. 8.919505573)
Time for model checking: 11.768s.

Performance statistics:
  * peak memory usage: 2472MB
  * CPU time: 24.414s
  * wallclock time: 25.415s