mcsta

Benchmark
Model:dpm v.2 (MA)
Parameter(s)N = 6, C = 6, TIME_BOUND = 5
Property:PminQueue1Full (prob-reach)
Invocation (default)
mono mcsta/mcsta.exe dpm.jani --props PminQueue1Full -E N=6,C=6,TIME_BOUND=5 --relative-width -O out.txt Minimal
Default settings: '--relative-width' = use relative error for sound methods, '-O out.txt Minimal' = write the property results into file out.txt with minimal formatting (will be read by get_result).
Execution
Walltime:44.57836890220642s
Return code:0
Relative Error:5.89911528660037e-08
Log
dpm.jani:model: info: dpm is an MA model.
dpm.jani: info: Need 15 bytes per state.
dpm.jani: info: Explored 9191028 states for N=6, C=6, TIME_BOUND=5.0.

Peak memory usage: 1015 MB
Analysis results for dpm.jani
Experiment N=6, C=6, TIME_BOUND=5.0

+ State space exploration
  State size:  15 bytes
  States:      9191028
  Transitions: 10604874
  Branches:    17865498
  Rate:        325058 states/s
  Time:        33.4 s

+ Property PminQueue1Full
  Probability: 0.0269661062565416
  Bounds:      [0.0269661062565416, 1]
  Time:        8.2 s

  + Value iteration
    Final error: 4.60882551363535E-07
    Iterations:  21
    Time:        7.9 s