mcsta

Model:	coupon v.1 (DTMC)
Parameter(s)	N = 9, DRAWS = 4, B = 5
Property:	exp_draws (exp-reward)

mono mcsta/mcsta.exe coupon.9-4.jani --props exp_draws -E B=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.

Walltime:	93.44874143600464s
Return code:	0
Relative Error:	1.8224477902489147e-06

coupon.9-4.jani:model: info: coupon.9-4 is a DTMC model.
coupon.9-4.jani: info: Need 14 bytes per state.
coupon.9-4.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
coupon.9-4.jani: info: Explored 21077063 states for B=5.

Peak memory usage: 3805 MB
Analysis results for coupon.9-4.jani
Experiment B=5

+ State space exploration
  State size:  14 bytes
  States:      21077063
  Transitions: 21077063
  Branches:    24429223
  Rate:        842914 states/s
  Time:        26.8 s

+ Property exp_draws
  Value:  6.74006020887122
  Bounds: [6.74006020887122, infinity)
  Time:   65.7 s

  + Precomputations
    Min. prob. 0 states:          0
    Time for min. prob. 0 states: 4.4 s
    Min. prob. 1 states:          21077063
    Time for min. prob. 1 states: 1.1 s

  + Value iteration
    Final error: 9.50156125645416E-07
    Iterations:  88
    Time:        60.2 s