Storm.exact

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

Date: Sat Sep  5 20:49:49 2020
Command line arguments: --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/dtmc/nand/nand.prism --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/dtmc/nand/nand.props reliable --constants 'N=40,K=4' --exact --timemem
Current working directory: /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks

Time for model input parsing: 0.003s.

Time for model construction: 26.437s.

-------------------------------------------------------------- 
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: 40.333s.

Performance statistics:
  * peak memory usage: 4573MB
  * CPU time: 65.000s
  * wallclock time: 67.181s