You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{< include ../../scripts/_reticulate-setup.md >}}
@@ -14,15 +14,15 @@ title: ❌ Mathematical proof of correctness
14
14
15
15
**Learning objectives:**
16
16
17
-
*TODO
17
+
*Understand why and how to verify a model using mathematical proof of correctness.
18
18
19
19
**Pre-reading:**
20
20
21
21
This page implements mathematical proof of correctness implemented on the [verification and validation page](verification_validation.qmd). It does so within a test ([tests](tests.qmd) page).
22
22
23
23
The test is run on the model from the [parallel processing](../output_analysis/parallel.qmd) page (likewise, also used on the [scenario and sensitivity analysis](../experiments/scenarios.qmd) page and [tests](tests.qmd) pages).
24
24
25
-
> *Entity generation → Entity processing → Initialisation bias → Performance measures → Replications → Length of warm-up → Number of replications → Parallel processing → Mathematical proof of correctness*
@@ -81,15 +82,9 @@ A mathematical model is a set of equations or formulas that describe how systems
81
82
82
83
Real-world systems are often too complex for neat equations (e.g., variable arrivals, different service rules or other complex features). In these cases, discrete-event simulation allows us to better mimic the system. However, if your simulation is simple enough - or if you start with a basic model to verify your code (and later build in complexity) - you can use mathematical proof of correctness.
83
84
84
-
The small example we've been building throughout this book is an instance of an **M/M/s queue model** (as is the nurse visit simulation example). For a reminder on what an M/M/s queue model is, see the section "*Find out more about M/M/s models*" on the [example conceptual models](../intro/examples.qmd) page. In the next section, we'll show how to verify our small example by comparing it to a mathematical model.
85
+
The small example we've been building throughout this book is an instance of an **M/M/s queue model** (as is the nurse visit simulation example). For a reminder on what an M/M/s queue model is, see the section "*Find out more about M/M/s models*" on the [example conceptual models](../intro/examples.qmd) page. In the following sections, we'll show how to verify our small example by comparing it to a mathematical model.
85
86
86
-
## How to verify the model against mathematical results
87
-
88
-
::: {.python-content}
89
-
90
-
<divclass="h3-tight"></div>
91
-
92
-
### Simulation code
87
+
## Simulation code
93
88
94
89
The model used is the same as that on the [parallel processing](../output_analysis/parallel.qmd) page - as also used on the [scenario and sensitivity analysis](../experiments/scenarios.qmd) and [tests](tests.qmd) pages.
95
90
@@ -98,7 +93,15 @@ The model used is the same as that on the [parallel processing](../output_analys
98
93
#| echo: false
99
94
```
100
95
101
-
### Mathematical M/M/s queue model
96
+
```{r}
97
+
#| file: "tests_resources/simulation.R"
98
+
#| echo: false
99
+
```
100
+
101
+
102
+
## Mathematical M/M/s queue model
103
+
104
+
::: {.python-content}
102
105
103
106
The class implementing a mathematical M/M/s queue model is explained line-by-line below.
104
107
@@ -238,7 +241,7 @@ class MMSQueue:
238
241
return 1 / (sum_part + server_term)
239
242
```
240
243
241
-
####Explaining `MMSQueue`
244
+
### Explaining `MMSQueue`
242
245
243
246
```{.python}
244
247
class MMSQueue:
@@ -426,7 +429,53 @@ First, we compute P0 which is the probability that the system is completely empt
426
429
"""
427
430
# Sum for n = 0 to s-1
428
431
sum_part = sum(
429
-
(self.lambda_over_mu**n) / math.factorial(n)
432
+
(self.lambda_over_mu**n) / math.factorial(n)# Validates a discrete event simulation of a healthcare M/M/S queue by
433
+
# comparing simulation results to analytical queueing theory.
434
+
#
435
+
# Metrics (using standard queueing theory notation):
436
+
# - ρ (rho): utilisation
437
+
# - Lq: mean queue length
438
+
# - W: mean time in system
439
+
# - Wq: mean waiting
440
+
#
441
+
# Results must match theory with a 15% tolerance (accomodates stochasticity).
442
+
# Tests are run across diverse parameter combinations and utilisation levels.
443
+
# System stability requires arrival rate < number_of_servers * service_rate.
444
+
445
+
446
+
#' Run simulation and return key performance indicators using standard queueing
447
+
#' theory notation.
448
+
#'
449
+
#' The warm-up period should be sufficiently long to allow the system to reach
# Get overall results, using queueing theory notation in column names
469
+
results <- run_results |>
470
+
summarise(
471
+
RO = mean(.data[["utilisation_nurse"]]),
472
+
Lq = mean(.data[["mean_queue_length_nurse"]]),
473
+
W = mean(.data[["mean_time_in_system"]]),
474
+
Wq = mean(.data[["mean_waiting_time_nurse"]])
475
+
)
476
+
results
477
+
}
478
+
430
479
for n in range(self.num_servers)
431
480
)
432
481
@@ -440,14 +489,53 @@ First, we compute P0 which is the probability that the system is completely empt
440
489
441
490
This method calculates P0, which is the probability that the system is completely empty - i.e., no customers are waiting and all servers are idle.
442
491
443
-
### Function to run the model
492
+
:::
493
+
494
+
::: {.r-content}
495
+
496
+
In R, there is a package [queueing](https://cran.r-project.org/web/packages/queueing/index.html) which makes this task super easy!
497
+
498
+
To create a theoretical M/M/s queue model, we first need to calculate lambda and mu based on our inter-arrival time and service times:
499
+
500
+
```{r}
501
+
# Example parameters
502
+
interarrival_time <- 5
503
+
service_length <- 5
504
+
servers <- 2
505
+
506
+
# Calculate lambda and mu
507
+
lambda <- 1L / interarrival_time
508
+
mu <- 1L / service_length
509
+
```
510
+
511
+
We can then use `queueing::NewInput.MMC()` to set-up an M/M/s (M/M/c) model. This function takes the arrival rate (`lambda`), service rate (`mu`) and the number of servers (`c`). There are two other parameters `n` and `method`, but we just specify the defaults here (0) (see [documentation](https://cran.r-project.org/web/packages/queueing/queueing.pdf) for more details).
512
+
513
+
```{r}
514
+
math_model <- queueing::NewInput.MMC(
515
+
lambda = lambda, mu = mu, c = servers, n = 0L, method = 0L
516
+
)
517
+
math_model
518
+
```
519
+
520
+
We then provide this model to `queueing::QueueingModel()`, which builds the model and returns the relevant calculations.
This function simply runs our simulation model and returns the relevant metrics, renamed to use queueing theory notation.
446
532
447
533
We could have included this code as part of the test function below - but have just made it in a separate function to keep that test function a little simpler.
448
534
449
535
Our short illustrative parameters (30 minute warm-up, 40 minute data collection, 5 replications) are very unstable, so we have increased them to get more reliable results for the comparison in this test.
Our test function uses `patrick` to run several different test cases.
721
+
722
+
For each of these, it compares the results from the simulation model (from `run_simulation_model()`) with the results from the mathematical model from `queueing`, and checks they are reasonably similar.
0 commit comments