mcsta

Model:	wlan-large v.1 (PTA)
Parameter(s)	K = 2
Property:	E_or (exp-time)

mono mcsta/mcsta.exe wlan-large.jani --props E_or -E K=2 --relative-width -O out.txt Minimal --unsafe -S Memory --chainopt

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, '--chainopt' = use state chain compression during state space exploration, which tends to work well for PTA and unbounded properties.

Walltime:	39.66012096405029s
Return code:	0
Relative Error:	1.5434653739590166e-09

wlan-large.jani:model: info: wlan-large is an STA model.
wlan-large.jani: info: Need 16 bytes per state.
wlan-large.jani: info: Explored 2823492 states for K=2.

Peak memory usage: 817 MB
Analysis results for wlan-large.jani
Experiment K=2

+ State space exploration
  State size:  16 bytes
  States:      2823492
  Transitions: 5678944
  Branches:    5699564
  Rate:        276379 states/s
  Time:        10.6 s

+ Property E_or
  Value:  33692.4572892667
  Bounds: [33692.4572892667, infinity)
  Time:   27.9 s

  + Precomputations
    Min. prob. 0 states:          0
    Time for min. prob. 0 states: 3.7 s
    Min. prob. 1 states:          2823492
    Time for min. prob. 1 states: 0.2 s

  + Value iteration
    Final error: 8.47686459918393E-07
    Iterations:  194
    Time:        24.0 s