mcsta

Model:	coupon v.1 (DTMC)
Parameter(s)	N = 9, DRAWS = 4, B = 5
Property:	collect_all_bounded (prob-reach-reward-bounded)

mono mcsta/mcsta.exe coupon.9-4.jani --props collect_all_bounded -E B=5 --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:	65.62615275382996s
Return code:	0
Relative Error:	1.5301161470300262e-16

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.
coupon.9-4.jani: warning: Encountered a value greater than 1 during value iteration. The final result for property "collect_all_bounded" is likely affected by floating-point errors.

Peak memory usage: 2322 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:        719206 states/s
  Time:        36.4 s

+ Property collect_all_bounded
  Probability: 0.358510789821972
  Bounds:      [0.358510789821972, 1]
  CDF:         { (0, 0), ..., (2, 0), (3, 0.0286200660905159), (4, 0.16073553349926), (5, 0.358510789821972) }
  Time:        28.0 s

  + Value iteration
    Final error: 0
    Iterations:  35
    Time:        27.1 s