mcsta

Benchmark
Model:crowds v.1 (DTMC)
Parameter(s)TotalRuns = 6, CrowdSize = 20
Property:positive (prob-reach)
Invocation (default)
mono mcsta/mcsta.exe crowds.jani --props positive -E TotalRuns=6,CrowdSize=20 --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:77.97724723815918s
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: 1542 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:        276313 states/s
  Time:        45.2 s

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

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