Erlang(30,10) model
Introduction
This case studie will show the different options the tool offers. We use the IMC depicted below, where Erl(30,10) denotes a transition with an Erlang (k,n) distributed delay. This corresponds to k=30 consecutive Markovian transitions, each with rate n = 10. Thus, the time to move from s2 to goal state s3 is K/n = 3 with variance k/n^2 = 3/10.
The source of the IMC model can be found here: erlang3010.imc
Model
Time-Bounded Reachability
We have computed the minimum and maximum time-bounded reachability probability for time-bound z=7 with scheduler synthesis for maximum time-bounded reachability.
| minimum | maximum | |
|---|---|---|
| time interval: | [0,7] | [0,7] |
| error-bound: | 0.0001 | 0.0001 |
| probability: | 0.491991 | 0.982829 |
| computing time: | 3.62014 sec | 3.78784 sec |
Expected-Time and Expected-Steps
We have computed the minimum and maximum expected-time and expected-steps to reach the goal state s4 from initial state s0.
| expected-time | expected-steps | |
|---|---|---|
| minimum: | 2 | 2 |
| maximum: | 4 | 31 |
For all computations the computing time was between 11 and 12 seconds.