mcsta

Model:	embedded v.1 (CTMC)
Parameter(s)	MAX_COUNT = 8, T = 12
Property:	up_time (exp-reward)

mono mcsta/mcsta.exe embedded.jani --props up_time -E MAX_COUNT=8,T=12 --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:	15.354386568069458s
Return code:	0
Note(s):	The tool result '469626175533571/1000000000000' is tagged as incorrect. The reference result is '477.5523735836194490059111033' (approx. 477.55237358361944) which means a relative error of '0.016597547177012558' which is larger than the goal precision '0.001'.
Relative Error:	0.016597547177012558

embedded.jani:model: info: embedded is a CTMC model.
embedded.jani: info: Need 15 bytes per state.
embedded.jani: info: Explored 5820 states for MAX_COUNT=8, T=12.0.

Peak memory usage: 49 MB
Analysis results for embedded.jani
Experiment MAX_COUNT=8, T=12.0

+ State space exploration
  State size:  15 bytes
  States:      5820
  Transitions: 5820
  Branches:    16788
  Rate:        105818 states/s
  Time:        0.1 s

+ Property up_time
  Value:  469.626175533571
  Bounds: [469.626175533571, infinity)
  Time:   14.4 s

  + Precomputations
    Min. prob. 0 states:          0
    Time for min. prob. 0 states: 0.0 s
    Min. prob. 1 states:          5820
    Time for min. prob. 1 states: 0.0 s

  + Value iteration
    Final error: 9.99979663798136E-07
    Iterations:  79047
    Time:        14.4 s