Benchmark

Model: | coupon v.1 (DTMC) |

Parameter(s) | N = 9, DRAWS = 4, B = 5 |

Property: | collect_all_bounded (prob-reach-reward-bounded) |

Invocation (default)

mono mcsta/mcsta.exe coupon.9-4.jani --props collect_all_bounded -E B=5 --relative-width -O out.txt MinimalDefault 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: | 65.62615275382996s |

Return code: | 0 |

Relative Error: | 1.5301161470300262e-16 |

Log

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