statechart art

The business of boba

Four statecharts about running a boba shop, one for each kind of chart /statechart makes: a flat chart, a parent state, two regions at the same time, and a rule that breaks. Each one is a small TLA+ model checked by TLC, laid out by pele, and drawn by hand in pen and coloured pencil, by code.

The code, the models and the drawings are on GitHub: kevintngo/statechart-art

Pen and coloured pencil drawing titled An order, from the line to your hand. The statechart is drawn as paper order tickets pinned up with coloured pushpins and joined by red thread: in line; you order, to ordered; you pay, to paid. From paid, the barista starts if there are pearls, to being made, or money back if the pearls ran out, to refunded. From being made, your number is called, to ready. From ready, it is the wrong drink goes back to being made, and you pick it up leads to in your hand. Around the chart: three customers waiting in line, a cashier at a counter with a till showing 5.50 and coins, a barista shaking a drink beside a service bell and a finished cup, a jar of pearls labelled sold out with a coin on a shelf, and a person with short wavy black hair, a beige polo and an iced coffee on their head holding up a cup of boba milk tea. — I
An order
from the line to your hand
**A flat chart with a branch and a loop.** Each state is an order ticket pinned up, and each step is a red thread between the pins. The words for each step sit beside its thread.

Pen and coloured pencil drawing titled A day, at the shop, 7 am to 9 pm. The statechart is drawn as a shop front. Closed, getting ready and closing up are wooden signs. Open is the shop window under a striped awning, with quiet, busy and a rush as notes taped to the glass. At 7 am, closed goes to getting ready; tea and pearls ready leads into open, to quiet; people come in, to busy; school is out, to a rush; it calms down, back to quiet; at 9 pm, if quiet, to closing up; till counted, back to closed. Around the chart: a sunrise, a kettle and a pot of pearls on a stove on a shelf, a moon and stars, a mop in a bucket, a morning glory vine and a planter of flowers under the window. — II
A day
at the shop, 7 am to 9 pm
**A chart with a parent state.** Open is a parent state with three states inside, so it is drawn as the shop window: quiet, busy and a rush are notes taped to the glass, and the other states are wooden signs.

Pen and coloured pencil drawing titled Two at once, the barista and the pot. Under a menu board, the statechart shows two regions side by side inside a frame marked at the same time. The barista: barista free; an order comes in, unless cooking pearls, to making a drink; shaken and sealed, to calling a number; picked up, back to barista free. The pot: full of pearls; pearls run low, to running low; a new batch, when barista free, to cooking pearls; chewy again, back to full of pearls. Each condition is coloured like the region it names. Below, a barista shakes a drink behind the counter beside two finished cups and a pager, and a pot of pearls and a kettle sit on a stove. — III
Two at once
the barista and the pot
**Two regions, at the same time.** The barista and the pot each move on their own, side by side. A step that waits on the other region says so in brackets, coloured like the region it waits on.

Pen and coloured pencil drawing titled The pearl bug, TLC finds how old pearls get served. A card states the rule: never serve pearls more than 4 hours old. The statechart: just boiled; an hour passes, to chewy, where more hours pass; an hour passes, to getting firm; an hour passes, to too old, where a rush starts. From too old, thrown out leads to thrown out, and a new batch is boiled leads back to just boiled; but a cup is served in a rush leads to an old cup is served, which is stamped rule broken. The path TLC found, from just boiled through too old to the old cup, is traced in red. Around the chart: a ladybug, an hourglass, a magnifying glass over a cup of old pearls, a pot of pearls on a stove and a jar of old pearls. — IV
The pearl bug
TLC finds how old pearls get served
**A rule that breaks, and the path to it.** TLC finds a way to break the rule: in a rush, nobody checks how old the pearls are. The chart marks the state that breaks it, and the shortest path to it is traced in red.

How they were made

What TLC is

Each chart starts as a model in TLA+, a language for saying how something works one step at a time: where it starts, and which steps can come next. TLC is the program that checks a TLA+ model.

A test tries a few cases. TLC tries all of them. From the first state it takes every step that can happen, then every step after those, until it has seen every state the model can reach. In each state it checks the rules, such as "every drink being made has been paid for". If a rule can break, TLC finds the shortest list of steps that breaks it. That's the red path on the pearl bug: in a rush, nobody checks how old the pearls are.

Model it. A few lines of TLA+ say what can happen in the shop, and which rules must always hold.
Check it. /statechart runs TLC over every state the model can reach and checks each rule in each one. When a rule breaks, it finds the shortest path to the break.
Choose the words. A view says what the reader sees in each state and each step. It picks the kind of chart too: a word for a flat chart, a list for parent states, an object for regions.
Lay it out. pele lays out the Mermaid chart, measuring every word in the letters the drawing uses.
Draw it. A program draws pele's boxes and lines as things from a boba shop, tickets, signs, notes and cards, in a simulated pen and coloured pencils, and fills the space around them with the shop. Words sit on clean paper, and arrows stop short of what they point at. The last picture for each plate below puts pele's boxes and lines, in blue, over the finished drawing.

I An order

TLC reached 13 states and 17 steps.

Every drink being made, ready or handed over has been paid for. PaidForEveryDrink
A refunded order has its money back. RefundsGiveMoneyBack

---- MODULE Order ----
EXTENDS Naturals
VARIABLES order, paid, pearls, remakes

vars == <<order, paid, pearls, remakes>>

Init ==
  /\ order = "in line"
  /\ paid = FALSE
  /\ pearls = "plenty"
  /\ remakes = 0

YouOrder ==
  /\ order = "in line"
  /\ order' = "ordered"
  /\ UNCHANGED <<paid, pearls, remakes>>

YouPay ==
  /\ order = "ordered"
  /\ order' = "paid"
  /\ paid' = TRUE
  /\ UNCHANGED <<pearls, remakes>>

PearlsRunOut ==
  /\ pearls = "plenty"
  /\ order \in {"in line", "ordered", "paid"}
  /\ pearls' = "out"
  /\ UNCHANGED <<order, paid, remakes>>

BaristaStarts ==
  /\ order = "paid"
  /\ pearls = "plenty"
  /\ order' = "being made"
  /\ UNCHANGED <<paid, pearls, remakes>>

MoneyBack ==
  /\ order = "paid"
  /\ pearls = "out"
  /\ order' = "refunded"
  /\ paid' = FALSE
  /\ UNCHANGED <<pearls, remakes>>

NumberCalled ==
  /\ order = "being made"
  /\ order' = "ready"
  /\ UNCHANGED <<paid, pearls, remakes>>

WrongDrink ==
  /\ order = "ready"
  /\ remakes < 1
  /\ order' = "being made"
  /\ remakes' = remakes + 1
  /\ UNCHANGED <<paid, pearls>>

YouPickItUp ==
  /\ order = "ready"
  /\ order' = "in your hand"
  /\ UNCHANGED <<paid, pearls, remakes>>

Done ==
  /\ order \in {"in your hand", "refunded"}
  /\ UNCHANGED vars

Next ==
  \/ YouOrder \/ YouPay \/ PearlsRunOut \/ BaristaStarts \/ MoneyBack
  \/ NumberCalled \/ WrongDrink \/ YouPickItUp \/ Done

Spec == Init /\ [][Next]_vars

TypeOK ==
  /\ order \in {"in line", "ordered", "paid", "being made", "ready", "in your hand", "refunded"}
  /\ paid \in BOOLEAN
  /\ pearls \in {"plenty", "out"}
  /\ remakes \in 0..1

PaidForEveryDrink == order \in {"being made", "ready", "in your hand"} => paid
RefundsGiveMoneyBack == order = "refunded" => ~paid
NoDrinkWithoutPearls == order = "being made" => pearls = "plenty" \/ remakes > 0
====

1. The model, in TLA+

export const title = "an order of boba";

export const state = (v) => v.order;

const STEPS = {
  YouOrder: "you order",
  YouPay: "you pay",
  PearlsRunOut: "the pearls run out",
  BaristaStarts: "the barista starts [if there are pearls]",
  MoneyBack: "money back [if the pearls ran out]",
  NumberCalled: "your number is called",
  WrongDrink: "it's the wrong drink",
  YouPickItUp: "you pick it up",
  Done: "you drink it",
};

export const step = (action) => STEPS[action];

2. The view: the reader's words for each state and step

---
title: "an order of boba"
config:
  state:
    rankSpacing: 26
    nodeSpacing: 60
---
stateDiagram-v2
  s0: in line
  s1: ordered
  s2: paid
  s3: being made
  s4: ready
  s5: refunded
  s6: in your hand
  [*] --> s0
  s0 --> s1: you order
  s1 --> s2: you pay
  s2 --> s3: the barista starts [if there are pearls]
  s3 --> s4: your number is called
  s2 --> s5: money back [if the pearls ran out]
  s4 --> s3: it's the wrong drink
  s4 --> s6: you pick it up

3. The chart /statechart wrote, with a line of layout for pele

4. pele's plain layout, which the drawing follows

5. pele's boxes and lines, in blue, on the drawing

II A day

TLC reached 8 states and 9 steps.

The shop is open only once the tea is brewed and the pearls are boiled. OpenOnlyWhenReady
The shop closes up only when no one is inside. CloseOnlyWhenEmpty
The till is counted only after the floor is mopped. CountAfterMopping

---- MODULE Day ----
VARIABLES phase, teaReady, pearlsReady, crowd, mopped

vars == <<phase, teaReady, pearlsReady, crowd, mopped>>

Phases == {"closed", "brewing", "boiling", "quiet", "busy", "rush", "cleaning", "counting"}

Init ==
  /\ phase = "closed"
  /\ teaReady = FALSE
  /\ pearlsReady = FALSE
  /\ crowd = 0
  /\ mopped = FALSE

Unlock ==
  /\ phase = "closed"
  /\ phase' = "brewing"
  /\ UNCHANGED <<teaReady, pearlsReady, crowd, mopped>>

TeaSteeped ==
  /\ phase = "brewing"
  /\ phase' = "boiling"
  /\ teaReady' = TRUE
  /\ UNCHANGED <<pearlsReady, crowd, mopped>>

DoorsOpen ==
  /\ phase = "boiling"
  /\ phase' = "quiet"
  /\ pearlsReady' = TRUE
  /\ UNCHANGED <<teaReady, crowd, mopped>>

PeopleComeIn ==
  /\ phase = "quiet"
  /\ phase' = "busy"
  /\ crowd' = 1
  /\ UNCHANGED <<teaReady, pearlsReady, mopped>>

SchoolLetsOut ==
  /\ phase = "busy"
  /\ phase' = "rush"
  /\ crowd' = 2
  /\ UNCHANGED <<teaReady, pearlsReady, mopped>>

RushPasses ==
  /\ phase = "rush"
  /\ phase' = "quiet"
  /\ crowd' = 0
  /\ UNCHANGED <<teaReady, pearlsReady, mopped>>

DoorsClose ==
  /\ phase = "quiet"
  /\ crowd = 0
  /\ phase' = "cleaning"
  /\ UNCHANGED <<teaReady, pearlsReady, crowd, mopped>>

FloorMopped ==
  /\ phase = "cleaning"
  /\ phase' = "counting"
  /\ mopped' = TRUE
  /\ UNCHANGED <<teaReady, pearlsReady, crowd>>

TillAddsUp ==
  /\ phase = "counting"
  /\ phase' = "closed"
  /\ teaReady' = FALSE
  /\ pearlsReady' = FALSE
  /\ mopped' = FALSE
  /\ UNCHANGED crowd

Next ==
  \/ Unlock \/ TeaSteeped \/ DoorsOpen \/ PeopleComeIn \/ SchoolLetsOut
  \/ RushPasses \/ DoorsClose \/ FloorMopped \/ TillAddsUp

Spec == Init /\ [][Next]_vars

TypeOK ==
  /\ phase \in Phases
  /\ teaReady \in BOOLEAN
  /\ pearlsReady \in BOOLEAN
  /\ crowd \in {0, 1, 2}
  /\ mopped \in BOOLEAN

OpenOnlyWhenReady == phase \in {"quiet", "busy", "rush"} => teaReady /\ pearlsReady
CloseOnlyWhenEmpty == phase \in {"cleaning", "counting"} => crowd = 0
CountAfterMopping == phase = "counting" => mopped
====

1. The model, in TLA+

export const title = "a day at the shop";

const PATH = {
  closed: ["closed"],
  brewing: ["getting ready"],
  boiling: ["getting ready"],
  quiet: ["open", "quiet"],
  busy: ["open", "busy"],
  rush: ["open", "a rush"],
  cleaning: ["closing up"],
  counting: ["closing up"],
};

export const state = (v) => PATH[v.phase];

const STEPS = {
  Unlock: "7 am",
  TeaSteeped: "tea steeped",
  DoorsOpen: "tea and pearls ready",
  PeopleComeIn: "people come in",
  SchoolLetsOut: "school's out",
  RushPasses: "it calms down",
  DoorsClose: "9 pm [if quiet]",
  FloorMopped: "floor mopped",
  TillAddsUp: "till counted",
};

export const step = (action) => STEPS[action];

2. The view: the reader's words for each state and step

---
title: "a day at the shop"
config:
  state:
    rankSpacing: 26
    nodeSpacing: 34
---
stateDiagram-v2
  direction TB
  s0: closed
  s1: getting ready
  state "open" as s2 {
    direction TB
    s3: quiet
    s4: busy
    s5: a rush
  }
  s6: closing up
  [*] --> s0
  s0 --> s1: 7 am
  s1 --> s3: tea and pearls ready
  s3 --> s6: 9 pm [if quiet]
  s3 --> s4: people come in
  s4 --> s5: school's out
  s6 --> s0: till counted
  s5 --> s3: it calms down

3. The chart /statechart wrote, with a line of layout for pele

4. pele's plain layout, which the drawing follows

III Two at once

TLC reached 7 states and 11 steps.

The barista is never making a drink while a batch of pearls is cooking. NoDrinkWhileCooking

---- MODULE Counter ----
VARIABLES barista, pot

vars == <<barista, pot>>

Init ==
  /\ barista = "free"
  /\ pot = "full"

OrderComesIn ==
  /\ barista = "free"
  /\ pot # "cooking"
  /\ barista' = "making"
  /\ UNCHANGED pot

ShakenAndSealed ==
  /\ barista = "making"
  /\ barista' = "calling"
  /\ UNCHANGED pot

PickedUp ==
  /\ barista = "calling"
  /\ barista' = "free"
  /\ UNCHANGED pot

PearlsRunLow ==
  /\ pot = "full"
  /\ pot' = "low"
  /\ UNCHANGED barista

NewBatch ==
  /\ pot = "low"
  /\ barista = "free"
  /\ pot' = "cooking"
  /\ UNCHANGED barista

ChewyAgain ==
  /\ pot = "cooking"
  /\ pot' = "full"
  /\ UNCHANGED barista

Next == OrderComesIn \/ ShakenAndSealed \/ PickedUp \/ PearlsRunLow \/ NewBatch \/ ChewyAgain

Spec == Init /\ [][Next]_vars

TypeOK ==
  /\ barista \in {"free", "making", "calling"}
  /\ pot \in {"full", "low", "cooking"}

NoDrinkWhileCooking == barista # "free" => pot # "cooking"
====

1. The model, in TLA+

export const title = "behind the counter";

const BARISTA = { free: "barista free", making: "making a drink", calling: "calling a number" };
const POT = { full: "full of pearls", low: "running low", cooking: "cooking pearls" };

export const state = (v) => ({ "the barista": BARISTA[v.barista], "the pot": POT[v.pot] });

const STEPS = {
  OrderComesIn: "an order comes in",
  ShakenAndSealed: "shaken and sealed",
  PickedUp: "picked up",
  PearlsRunLow: "pearls run low",
  NewBatch: "a new batch",
  ChewyAgain: "chewy again",
};

export const step = (action) => STEPS[action];

2. The view: the reader's words for each state and step

---
title: "behind the counter"
config:
  state:
    rankSpacing: 24
    nodeSpacing: 30
---
stateDiagram-v2
  direction LR
  state "At the same time" as all {
    state "the barista" as r0 {
      s0: barista free
      s1: making a drink
      s2: calling a number
      [*] --> s0
      s0 --> s1: an order comes in [unless cooking pearls]
      s1 --> s2: shaken and sealed
      s2 --> s0: picked up
    }
    --
    state "the pot" as r1 {
      s3: full of pearls
      s4: running low
      s5: cooking pearls
      [*] --> s3
      s3 --> s4: pearls run low
      s4 --> s5: a new batch [when barista free]
      s5 --> s3: chewy again
    }
  }

3. The chart /statechart wrote, with a line of layout for pele

4. pele's plain layout, which the drawing follows

IV The pearl bug

TLC reached 36 states and 90 steps.

Pearls are never served more than 4 hours after boiling. It breaks. NeverServeOldPearls

The path TLC found

The shortest path has 6 steps:
0. just boiled
1. an hour passes: chewy
2. an hour passes: chewy
3. an hour passes: getting firm
4. an hour passes: too old
5. a rush starts: too old
6. a cup is served [in a rush]: an old cup is served

---- MODULE Bug ----
EXTENDS Naturals
VARIABLES age, batch, rush, served

vars == <<age, batch, rush, served>>

Init ==
  /\ age = 0
  /\ batch = "in the pot"
  /\ rush = FALSE
  /\ served = "nothing yet"

AnHourPasses ==
  /\ batch = "in the pot"
  /\ age < 4
  /\ age' = age + 1
  /\ UNCHANGED <<batch, rush, served>>

ServeACup ==
  /\ batch = "in the pot"
  /\ served # "an old cup"
  /\ (age < 4 \/ rush)
  /\ served' = IF age < 4 THEN "a fresh cup" ELSE "an old cup"
  /\ UNCHANGED <<age, batch, rush>>

RushStarts ==
  /\ ~rush
  /\ rush' = TRUE
  /\ UNCHANGED <<age, batch, served>>

RushEnds ==
  /\ rush
  /\ rush' = FALSE
  /\ UNCHANGED <<age, batch, served>>

ThrowOut ==
  /\ batch = "in the pot"
  /\ age = 4
  /\ batch' = "thrown out"
  /\ UNCHANGED <<age, rush, served>>

NewBatch ==
  /\ batch = "thrown out"
  /\ batch' = "in the pot"
  /\ age' = 0
  /\ UNCHANGED <<rush, served>>

Next == AnHourPasses \/ ServeACup \/ RushStarts \/ RushEnds \/ ThrowOut \/ NewBatch

Spec == Init /\ [][Next]_vars

TypeOK ==
  /\ age \in 0..4
  /\ batch \in {"in the pot", "thrown out"}
  /\ rush \in BOOLEAN
  /\ served \in {"nothing yet", "a fresh cup", "an old cup"}

NeverServeOldPearls == served # "an old cup"
====

1. The model, in TLA+

export const title = "the pearl bug";

const AGE = ["just boiled", "chewy", "chewy", "getting firm", "too old"];

export const state = (v) =>
  v.served === "an old cup" ? "an old cup is served"
  : v.batch === "thrown out" ? "thrown out"
  : AGE[v.age];

const STEPS = {
  AnHourPasses: "an hour passes",
  ServeACup: "a cup is served",
  RushStarts: "a rush starts",
  RushEnds: "the rush ends",
  ThrowOut: "thrown out",
  NewBatch: "a new batch is boiled",
};

export const step = (action, from, to) =>
  action === "ServeACup" && to.served === "an old cup" ? "a cup is served [in a rush]" : STEPS[action];

2. The view: the reader's words for each state and step

---
title: "the pearl bug"
config:
  state:
    rankSpacing: 26
    nodeSpacing: 40
---
stateDiagram-v2
  state "Legend" as legend {
    lg0: Breaks NeverServeOldPearls
    lg1: Path to the NeverServeOldPearls bug
  }
  class lg0 breaks
  class lg1 bugPath
  s0: just boiled
  s1: chewy
  s2: getting firm
  s3: too old
  s4: thrown out
  s5: an old cup is served
  [*] --> s0
  s0 --> s1: an hour passes
  s1 --> s1: an hour passes
  s1 --> s2: an hour passes
  s2 --> s3: an hour passes
  s3 --> s3: a rush starts
  s3 --> s4: thrown out
  s3 --> s5: a cup is served [in a rush]
  s4 --> s0: a new batch is boiled
  classDef breaks fill:#ffecee,stroke:#e72e3b,stroke-width:2.5px,color:#cd2834
  class s0 bugPath
  class s1 bugPath
  class s2 bugPath
  class s3 bugPath
  class s5 breaks
  class s5 bugPath

3. The chart /statechart wrote, with a line of layout for pele

4. pele's plain layout, which the drawing follows