Storm.exact

Benchmark
Model:nand v.1 (DTMC)
Parameter(s)N = 40, K = 4
Property:reliable (prob-reach)
Invocation (exact)
storm/build/bin/storm --prism qcomp/benchmarks/dtmc/nand/nand.prism --prop qcomp/benchmarks/dtmc/nand/nand.props reliable --constants N=40,K=4 --exact --timemem
Sparse engine with exact model checking
Execution
Walltime:65.58709979057312s
Return code:0
Relative Error:5.272906966032163e-29
Log
Storm 1.4.1 (dev)

Date: Fri Dec  6 09:44:58 2019
Command line arguments: --prism qcomp/benchmarks/dtmc/nand/nand.prism --prop qcomp/benchmarks/dtmc/nand/nand.props reliable --constants 'N=40,K=4' --exact --timemem
Current working directory: 

Time for model input parsing: 0.004s.

Time for model construction: 27.132s.

-------------------------------------------------------------- 
Model type: 	DTMC (sparse)
States: 	3999522
Transitions: 	6288542
Reward Models:  none
State Labels: 	3 labels
   * deadlock -> 0 item(s)
   * ((s = 4) & ((z / 40) < 1/10)) -> 4 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "reliable": P=? [F ((s = 4) & ((z / 40) < 1/10))] ...
Result (for initial states): 7073410276867630182036256400888394636401281117838496193329308323687125707403234304583554599059642891015434709050290014659339126304802694362252183431807177003633968280617618995071337263400451170114626733996748290675371799715662983419506318701718558795860406494115162261649890650251693555717374614594670943847433539070343259606254316245084716000896473482539769578265846578050874211797180613965882452295534277381831975275853494748435478879461635997848648515103809170427736893067597368369125722353133284605839381110231288435557905276235846112930375580391379431641001473203640322244029437131656432754007785810519373450767717313409320241381606121889757/11433026582770433444150841434946575983665790023011997239866893501124069401225141786043274075451132615716021287640033707692804831240670294973965820412638988355604337906057133982774690808247500425599746811586452854879494120350499663410752853418655568298801018707370085780279622235281919773885153915410742665432027264385939603794342761535883881589330478746513396975860783173588783333310428610837885469575737992226585096003257861714861056977505239452452401210690205384130399418976115047153237702913577842484321014952056001690525414886369612166053431447977273573548482850717467051993025961564853787422180175781250000000000000000000000000000000000000000 (approx. 0.6186822208)
Time for model checking: 38.039s.

Performance statistics:
  * peak memory usage: 4572MB
  * CPU time: 62.991s
  * wallclock time: 65.515s