Skip to content

Check Against Theory

Check a model against the queueing formulas, on a queue the formulas describe. A model that agrees is computing what it should. A model that differs has a defect to find.

Before You Start

Steps

Build a Queue the Formulas Describe

The M/M/1 and M/M/c formulas hold when the gaps between arrivals and the service times are exponential, every arrival joins one queue and waits until it is served, and nothing changes while the model runs. This shop has one packer, an order every 1.33 seconds on average (rate: 0.75) and a mean packing time of 1 second. Its utilisation is therefore 0.75 × 1 ÷ 1 = 0.75:

docs/snippets/yaml/check_against_theory.yaml:shop
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
simulation:
  sim_id: Shop
  factor: 0
  random_seed: 42
  warmup: 2000  # seconds left out of every measure, while the queue fills

arrivals:
  # An order every 1.33 s on average (rate 0.75) with one packer; RATE=1.5 with PACKERS=2
  orders:
    dist: exponential
    rate: ${RATE:-0.75}
    spawn: pack_order

services:
  packing: {dist: exponential, rate: 1}  # 1 second on average

resources:
  packers:
    current_cap: ${PACKERS:-1}
    max_cap: 4

tasks:
  pack_order:
    service: packing
    resource: packers
    payload: {event_type: order_packed}

run:
  until: 20000
docs/snippets/guides/check_against_theory_shop.py:shop
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
# An order every 1.33 s on average (rate 0.75) with one packer; RATE=1.5 with PACKERS=2
rate = float(os.environ.get("RATE", "0.75"))
packers = int(os.environ.get("PACKERS", "1"))

app = (
    # warmup: seconds left out of every measure, while the queue fills
    SimulationContext(sim_id="Shop", factor=0, random_seed=42, warmup=2000)
    .add_arrival("orders", dist="exponential", rate=rate, spawn="pack_order")
    .add_service("packing", dist="exponential", rate=1)  # 1 second on average
    .add_resource("packers", current_cap=packers, max_cap=4)
)


@app.task(service_id="packing", resource_id="packers")
def pack_order(task_id):
    return {"event_type": "order_packed"}

The low-level API has no analysis: explain and analyze read a blueprint or a builder file. Write the model as a builder file to check it.

The highlighted lines of the blueprint are the warm-up and the three numbers the formulas read: the arrival rate, the service rate and the number of packers. The warm-up leaves out the first 2,000 seconds, while the queue fills from empty. RATE and PACKERS set the second case below.

Work out the mean wait by hand first. For one packer it is ρ ÷ (1 − ρ) × the mean service time, where ρ is the utilisation. For several packers it is the Erlang C chance that every packer is busy, divided by (c ÷ the mean service time − the arrival rate):

docs/snippets/guides/check_against_theory.py:by-hand
1
2
3
4
5
6
7
8
load = rate * service  # packers' worth of work arriving each second
utilisation = load / packers
if packers == 1:
    return utilisation / (1 - utilisation) * service  # M/M/1
# M/M/c: Erlang C, the chance that every packer is busy, over (c / service - rate)
last = load**packers / math.factorial(packers) / (1 - utilisation)
busy = last / (sum(load**k / math.factorial(k) for k in range(packers)) + last)
return busy / (packers / service - rate)

With one packer at utilisation 0.75, the mean wait is 0.75 ÷ 0.25 × 1 = 3 seconds. With two packers and 1.5 orders a second, it is 1.286 seconds.

Verify It

desflow explain gives the same values from the blueprint, and --verify runs the model and compares. Each pair is a value from the formulas and the same measure from the runs. A pair differs by one of two rules:

  • With --replications 10, the model runs ten times. A pair differs when the formula's value lies outside the 95% interval of the runs and is more than 1 percent from their mean.
  • With one run, a pair differs when the two values are more than 10 percent apart.

The 1 percent matters when every run gives the same value, as with constant times. The interval then has a width of 0, and the last order still being packed at the end would count as a difference. This command runs ten replications. A builder file has no run.until, so its command gives the end of each run:

1
desflow explain check_against_theory.yaml --verify --replications 10

1
desflow explain check_against_theory_shop.py --verify --replications 10 --until 20000

The low-level API has no analysis: explain and analyze read a blueprint or a builder file. Write the model as a builder file to check it.

Both print the same tables, because they are the same model with the same seed:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
Shop
`-- orders (arrival, rate 0.75/s)
    `-- spawn -> pack_order (task, rate 0.75/s)
        +-- uses packers (resource)
        `-- next (share 1) -> exit
Resources
+--------------------------------------------------+
| resource |    λ | μ | c |    ρ | Wq | L | status |
|----------+------+---+---+------+----+---+--------|
| packers  | 0.75 | 1 | 1 | 0.75 |  3 | 3 | OK     |
+--------------------------------------------------+
packers by units
+---------------------+
| c |      ρ | status |
|---+--------+--------|
| 1 |   0.75 | OK     |
| 2 |  0.375 | OK     |
| 3 |   0.25 | OK     |
| 4 | 0.1875 | OK     |
+---------------------+
Bottleneck: packers
Hints for utilisation 0.85:
  packers with 1 unit: utilisation 0.75, at most 0.85
  packers with 1 unit: utilisation 0.85 at a request every 1.18 seconds (51 a minute, 0.85 a second)
Verify: 10 runs to 20000 s, seed 42
+---------------------------------------------------------------------+
| node       | measure      | analysis | measured |        ± | result |
|------------+--------------+----------+----------+----------+--------|
| packers    | utilization  |     0.75 |   0.7508 |  0.00624 | agrees |
| packers    | queue_length |     2.25 |     2.25 |    0.132 | agrees |
| pack_order | wait         |        3 |    2.994 |    0.163 | agrees |
| orders     | throughput   |     0.75 |   0.7514 | 0.004534 | agrees |
+---------------------------------------------------------------------+
--verify checks the implementation against the queueing analysis where it applies; it does not show that the model is close enough to the real system

Every measure agrees: the utilisation, the queue length Lq = λ × Wq, the mean wait of 3 seconds and the throughput. With two packers at the same utilisation, the wait comes from Erlang C:

1
PACKERS=2 RATE=1.5 desflow explain check_against_theory.yaml --verify --replications 10

1
2
# Twice the orders and two packers, checked against the formulas
PACKERS=2 RATE=1.5 desflow explain check_against_theory_shop.py --verify --replications 10 --until 20000

The low-level API has no analysis: explain and analyze read a blueprint or a builder file. Write the model as a builder file to check it.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
Verify: 10 runs to 20000 s, seed 42
+---------------------------------------------------------------------+
| node       | measure      | analysis | measured |        ± | result |
|------------+--------------+----------+----------+----------+--------|
| packers    | utilization  |     0.75 |    0.752 | 0.004173 | agrees |
| packers    | queue_length |    1.929 |    1.972 |  0.07398 | agrees |
| pack_order | wait         |    1.286 |    1.312 |  0.04669 | agrees |
| orders     | throughput   |      1.5 |    1.503 |  0.00529 | agrees |
+---------------------------------------------------------------------+
--verify checks the implementation against the queueing analysis where it applies; it does not show that the model is close enough to the real system

From Python, analyze(verify=True) runs the same check and returns it as explanation.verification. This function prints each pair:

docs/snippets/guides/check_against_theory.py:show
1
2
3
4
5
6
7
8
def show(explanation):
    """Prints each pair of the verification: the formula's value and the runs'."""
    for c in explanation.verification.comparisons:
        result = "differs" if c.differs else "agrees"
        print(
            f"{c.node} {c.measure}: analysis {c.analytical:.3f}, "
            f"runs {c.measured:.3f} ± {c.half_width:.3f}, {result}"
        )

Each form loads its model from its file and passes the result to show:

docs/snippets/guides/check_against_theory.py:verify
1
2
3
app = SimulationContext.from_yaml(BLUEPRINT)
explanation = app.analyze(verify=True, replications=10)  # until from run.until
show(explanation)
docs/snippets/guides/check_against_theory.py:verify-builder
1
2
3
app = load_context(SHOP.parent, SHOP.name)  # a new copy for each run needs a file
explanation = app.analyze(verify=True, until=20000, replications=10)
show(explanation)

The low-level API has no analysis: explain and analyze read a blueprint or a builder file. Write the model as a builder file to check it.

1
2
3
4
packers utilization: analysis 0.750, runs 0.751 ± 0.006, agrees
packers queue_length: analysis 2.250, runs 2.250 ± 0.132, agrees
pack_order wait: analysis 3.000, runs 2.994 ± 0.163, agrees
orders throughput: analysis 0.750, runs 0.751 ± 0.005, agrees

A context built in a script's own code refuses verify=True, because the runs need a new copy of the model, which only a file can give.

--json prints the same result as JSON, for a script or a CI job outside Python. Each comparison has node, measure, analytical, measured, half_width and differs. With jq -e, this command prints true and exits 0 when no pair differs, and exits 1 when one does:

1
2
# Exit with an error when any reading differs from its formula
desflow explain check_against_theory.yaml --verify --replications 10 --json | jq -e '[.verification.comparisons[] | select(.differs)] | length == 0'

The JSON shape is experimental through 1.x, as the Changelog says.

Check the Result

Every pair says agrees for the shop above. When one says differs, read it as follows.

Read a Difference

A pair that differs on a model the formulas describe points at the model: a wrong rate or unit, a task that holds its resource longer than its service, or a route that sends entities somewhere else.

Chance can also make a pair differ. A short run varies from one run to the next. With replications, each pair's 95% interval misses a correct value about 1 time in 20, so among many pairs one difference is expected now and then. Before looking for a defect, run the check again with more replications, a longer until or another seed.

Agreement shows the program computes what the model on paper says. It says nothing about whether the model is close enough to the real shop, which only a comparison with the shop's own records can show, as Checking a Model does.

When the Formulas Do Not Apply

explain estimates a wait only where a formula holds, and gives the reason where none does. Two packers whose packing always takes 1 second have no closed formula:

docs/snippets/yaml/check_against_theory_constant.yaml:unsupported
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
simulation:
  sim_id: Shop
  factor: 0

arrivals:
  orders: {dist: exponential, rate: 1.5, spawn: pack_order}

services:
  packing: {dist: constant, value: 1 s}

resources:
  packers: {current_cap: 2, max_cap: 4}

tasks:
  pack_order:
    service: packing
    resource: packers
    payload: {event_type: order_packed}

desflow explain check_against_theory_constant.yaml prints the same reason under Not estimated.

docs/snippets/guides/check_against_theory.py:unsupported
1
2
3
4
5
6
7
8
app = SimulationContext(sim_id="Shop", factor=0)
app.add_arrival("orders", dist="exponential", rate=1.5, spawn="pack_order")
app.add_service("packing", dist="constant", value=1)
app.add_resource("packers", current_cap=2, max_cap=4)
app.task("packing", "packers", name="pack_order")(lambda task_id: {})
packers = app.analyze().resources[0]
print(f"utilisation {packers.utilization}, status {packers.status}")
print(f"wait: {packers.wait_reason}")

The low-level API has no analysis: explain and analyze read a blueprint or a builder file. Write the model as a builder file to check it.

1
2
utilisation 0.75, status OK
wait: no closed formula for c > 1 with non-exponential times; run --verify to measure it

The utilisation is still known here, because it needs only the rates. The same rule applies to every model. The formulas hold in a plain network of queues: each task holds at most one resource, each queue serves first come, first served, and nothing blocks, removes, delays or reorders work. Anything else takes the formulas out of use, from the part of the model where it happens to the end of the flow:

  • a task's patience, balk, fail, keep, get, put, signal, subscribe, interrupt or on actions, preemption, or several resources held at once: that task and every task after it;
  • a wait other than a single request, such as a wait with two or more requests, or a request that a timeout of the same wait can end: that task and every task after it;
  • a resource's queue_limit, custom type or breakdowns: the tasks that use it and every task after them;
  • an unstable resource: every task after its tasks, though the resource itself keeps its utilisation and status;
  • a priority queue whose tasks have different priorities: its wait, and every task after its tasks;
  • a scenario step that changes a parameter, live ingress, or an add_process function: every arrival and every task;
  • a replayed arrival, a hand-written arrival loop or a next function: every rate they could change.

A task outside what the formulas cover has no rate, so each resource it uses has no utilisation, status or wait. Such a resource is not ranked as the bottleneck. When no resource has a utilisation, explain says that no bottleneck can be named, and why. Each unknown value is printed under Not estimated, with the first reason found.

One value is given but not compared. With one packer and gaps that are not exponential, such as constant or uniform gaps, Kingman's formula gives the wait only approximately, so explain shows it as an estimate. --verify marks that wait and the queue length not compared, because a correct model can differ from an approximation.

--verify still runs such a model and prints what it measures. It compares only the values the analysis gives. Every other row says not compared, with the reason, and a row whose measure did not happen in the run says no reading. The interval from replications is then the check, as the experiments of Checking a Model use it.

Full Files

The script reads the blueprint and the builder file from the repository, so run it in a clone:

1
2
3
4
# The script and the builder file are in docs/snippets/guides/, the blueprints in docs/snippets/yaml/
git clone https://github.com/jaehyeon-kim/desflow.git
cd desflow/docs/snippets/guides
python check_against_theory.py
Full files
docs/snippets/yaml/check_against_theory.yaml
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
# Check Against Theory: a shop the queueing formulas describe exactly. Gaps and
# packing times are exponential, one queue, no limits, nothing changes during the run.
# Check it with: desflow explain check_against_theory.yaml --verify --replications 10
simulation:
  sim_id: Shop
  factor: 0
  random_seed: 42
  warmup: 2000  # seconds left out of every measure, while the queue fills

arrivals:
  # An order every 1.33 s on average (rate 0.75) with one packer; RATE=1.5 with PACKERS=2
  orders:
    dist: exponential
    rate: ${RATE:-0.75}
    spawn: pack_order

services:
  packing: {dist: exponential, rate: 1}  # 1 second on average

resources:
  packers:
    current_cap: ${PACKERS:-1}
    max_cap: 4

tasks:
  pack_order:
    service: packing
    resource: packers
    payload: {event_type: order_packed}

run:
  until: 20000

egress:
  - type: Console
docs/snippets/yaml/check_against_theory_constant.yaml
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
# Check Against Theory: two packers whose packing always takes 1 second, which no
# closed formula describes.
# Check it with: desflow explain check_against_theory_constant.yaml
simulation:
  sim_id: Shop
  factor: 0

arrivals:
  orders: {dist: exponential, rate: 1.5, spawn: pack_order}

services:
  packing: {dist: constant, value: 1 s}

resources:
  packers: {current_cap: 2, max_cap: 4}

tasks:
  pack_order:
    service: packing
    resource: packers
    payload: {event_type: order_packed}

The script works out the waits by hand and verifies both the blueprint and the builder file:

docs/snippets/guides/check_against_theory.py
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
"""Check Against Theory: a shop the queueing formulas describe, checked against them.

check_against_theory.yaml, and check_against_theory_shop.py in the builder, are one
packer with exponential gaps and packing times. The script works out the wait by hand,
verifies each form against `explain`'s analysis from Python, and shows a shop the
formulas do not cover, with the reason.
"""

import math
from pathlib import Path

from desflow import SimulationContext, load_context

BLUEPRINT = Path(__file__).resolve().parents[1] / "yaml" / "check_against_theory.yaml"
SHOP = Path(__file__).resolve().parent / "check_against_theory_shop.py"


def by_hand(packers: int, rate: float, service: float = 1.0) -> float:
    """The mean wait in the queue from the M/M/1 and M/M/c formulas."""
    load = rate * service  # packers' worth of work arriving each second
    utilisation = load / packers
    if packers == 1:
        return utilisation / (1 - utilisation) * service  # M/M/1
    # M/M/c: Erlang C, the chance that every packer is busy, over (c / service - rate)
    last = load**packers / math.factorial(packers) / (1 - utilisation)
    busy = last / (sum(load**k / math.factorial(k) for k in range(packers)) + last)
    return busy / (packers / service - rate)


def show(explanation):
    """Prints each pair of the verification: the formula's value and the runs'."""
    for c in explanation.verification.comparisons:
        result = "differs" if c.differs else "agrees"
        print(
            f"{c.node} {c.measure}: analysis {c.analytical:.3f}, "
            f"runs {c.measured:.3f} ± {c.half_width:.3f}, {result}"
        )


def verify():
    """The blueprint's one packer, verified with 10 runs from Python."""
    app = SimulationContext.from_yaml(BLUEPRINT)
    explanation = app.analyze(verify=True, replications=10)  # until from run.until
    show(explanation)
    return explanation


def verify_builder():
    """The builder file's one packer, verified with 10 runs from Python."""
    app = load_context(SHOP.parent, SHOP.name)  # a new copy for each run needs a file
    explanation = app.analyze(verify=True, until=20000, replications=10)
    show(explanation)
    return explanation


def unsupported():
    """Two packers whose packing always takes 1 second: no formula for the wait."""
    app = SimulationContext(sim_id="Shop", factor=0)
    app.add_arrival("orders", dist="exponential", rate=1.5, spawn="pack_order")
    app.add_service("packing", dist="constant", value=1)
    app.add_resource("packers", current_cap=2, max_cap=4)
    app.task("packing", "packers", name="pack_order")(lambda task_id: {})
    packers = app.analyze().resources[0]
    print(f"utilisation {packers.utilization}, status {packers.status}")
    print(f"wait: {packers.wait_reason}")
    return packers


if __name__ == "__main__":
    print(f"one packer, an order every 1.33 s (rate 0.75): {by_hand(1, 0.75):.3f} s")
    print(f"two packers at 1.5 orders a second: {by_hand(2, 1.5):.3f} s")
    verify()
    verify_builder()
    unsupported()
docs/snippets/guides/check_against_theory_shop.py
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
"""Check Against Theory: the shop of check_against_theory.yaml as a builder file.

Check it with:
desflow explain check_against_theory_shop.py --verify --replications 10 --until 20000
"""

import os

from desflow import SimulationContext

# An order every 1.33 s on average (rate 0.75) with one packer; RATE=1.5 with PACKERS=2
rate = float(os.environ.get("RATE", "0.75"))
packers = int(os.environ.get("PACKERS", "1"))

app = (
    # warmup: seconds left out of every measure, while the queue fills
    SimulationContext(sim_id="Shop", factor=0, random_seed=42, warmup=2000)
    .add_arrival("orders", dist="exponential", rate=rate, spawn="pack_order")
    .add_service("packing", dist="exponential", rate=1)  # 1 second on average
    .add_resource("packers", current_cap=packers, max_cap=4)
)


@app.task(service_id="packing", resource_id="packers")
def pack_order(task_id):
    return {"event_type": "order_packed"}


if __name__ == "__main__":
    app.run(until=20000)

check_against_theory.py, in the YAML tab, verifies this file too, with verify_builder.

The low-level API has no analysis: explain and analyze read a blueprint or a builder file. Write the model as a builder file to check it.