mcsta

Benchmark
Model:crowds v.1 (DTMC)
Parameter(s)TotalRuns = 6, CrowdSize = 20
Property:positive (prob-reach)
Invocation (specific)
mono mcsta/mcsta.exe crowds.jani --props positive -E TotalRuns=6,CrowdSize=20 --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:58.81874489784241s
Return code:0
Relative Error:1.7427039735113588e-06
Log
crowds.jani:model: info: crowds is a DTMC model.
crowds.jani: info: Need 33 bytes per state.
crowds.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
crowds.jani: info: Explored 10291282 states for TotalRuns=6, CrowdSize=20.

Peak memory usage: 2977 MB
Analysis results for crowds.jani
Experiment TotalRuns=6, CrowdSize=20

+ State space exploration
  State size:  33 bytes
  States:      10291282
  Transitions: 10291282
  Branches:    37068802
  Rate:        376832 states/s
  Time:        28.7 s

+ Property positive
  Probability: 0.120476160929948
  Bounds:      [0.120476160929948, 1]
  Time:        29.1 s

  + Value iteration
    Final error: 8.7785422810086E-07
    Iterations:  63
    Time:        29.1 s