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.
![](erlang_small.png)
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 |
![](prob_erlang_tiny.png)
![](scheduler_erlang_tiny.png)
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.