mcsta

Benchmark
Model:dpm v.2 (MA)
Parameter(s)N = 6, C = 6, TIME_BOUND = 5
Property:PminQueue1Full (prob-reach)
Invocation (specific)
mono mcsta/mcsta.exe dpm.jani --props PminQueue1Full -E N=6,C=6,TIME_BOUND=5 --relative-width -O out.txt Minimal --unsafe -S Memory
Settings specific for this benchmark: '--unsafe' = compile model without bounds and assignment checks, '-S Memory' = store all data in memory since the model is small.
Execution
Walltime:31.898333072662354s
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: 2049 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:        414365 states/s
  Time:        23.1 s

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

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