mcsta

Model:	crowds v.1 (DTMC)
Parameter(s)	TotalRuns = 5, CrowdSize = 20
Property:	positive (prob-reach)

mono mcsta/mcsta.exe crowds.jani --props positive -E TotalRuns=5,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).

Walltime:	16.67981743812561s
Return code:	0
Relative Error:	1.663419856058807e-06

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 2018094 states for TotalRuns=5, CrowdSize=20.

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

+ State space exploration
  State size:  33 bytes
  States:      2018094
  Transitions: 2018094
  Branches:    7224834
  Rate:        294827 states/s
  Time:        8.4 s

+ Property positive
  Probability: 0.0860689112675363
  Bounds:      [0.0860689112675363, 1]
  Time:        6.2 s

  + Value iteration
    Final error: 9.36872388860927E-07
    Iterations:  58
    Time:        5.2 s