Eric Spencer

projects

 _____      _        ____
| ____|_ __(_) ___  / ___| _ __   ___ _ __   ___ ___ _ __
|  _| | '__| |/ __| \___ \| '_ \ / _ \ '_ \ / __/ _ \ '__|
| |___| |  | | (__   ___) | |_) |  __/ | | | (_|  __/ |
|_____|_|  |_|\___| |____/| .__/ \___|_| |_|\___\___|_|
                          |_|

← back to index

TLA+ Model of a Laptop

A formal TLA+ specification modeling a laptop's power states, battery, lid, thermals, and auto-suspend.

A small TLA+ spec in the same family as the walk-in oven and the interactive microwave. The microwave page is the gentler introduction for a reader new to TLA+. This one models a laptop: not a real laptop, but a small mechanical abstraction of one, with a power button, lid, charger, display, brightness, wifi, bluetooth, CPU mode, temperature, fan and sleep timer. The spec writes down everything that can change and the rules for how it changes, then asks TLC whether anything bad can happen.

The repo is at https://github.com/EricSpencer00/tla-laptop.

What's in the spec

The state is twelve variables plus a phase flag that flips between "user" and "tick". The phase split is a trick: user actions (pressing the power button, opening the lid, toggling wifi) fire only in the user phase, and ambient ticks (battery draining, temperature rising, the auto-suspend countdown) fire only in the tick phase. Without it the model can take a user action and a thermal tick in the same step, which makes counterexamples annoying to read.

Power has three states: off, on, suspend. The interlocks:

Closing the lid on a laptop that is on puts it into suspend and turns the display off.
Opening the lid on a suspend laptop wakes it back to on and the display comes back on. If power was already off, the lid does nothing to it.
Pressing the power button toggles between off and on, and moves suspend to on.
With the laptop on and the display off, the sleep timer counts up, and once it crosses SleepTimeout the AutoSuspend action fires.

Battery and thermals are the messy bits. TickBatteryAndTimer does the battery accounting: charge when plugged in (capped at BatteryMax), drain by DisplayDrain with the display on, IdleDrain with it off but the laptop on, SuspendDrain while suspended. ThermalTick raises temperature by 1 to 3 depending on CPU mode and lowers it by the fan speed, clamped at ThermalMax.

What it checks

Three invariants in laptop.cfg:

BatteryRange: battery stays inside 0..BatteryMax
TempRange: temperature never exceeds ThermalMax
FanRange: fan stays inside 0..FanMax

And one liveness property, left as an option in the config:


PROPERTY == <> (power = "on" /\ lid = "open" /\ display = "on")

That is, the laptop eventually ends up in the state of actually being used. It is a sanity check against a spec whose only reachable behavior is the lid staying shut forever.

Scope

This is a personal study spec, not class work and not part of any research. It follows the walk-in oven with more variables and a non-trivial ambient process (the battery and thermal dynamics) rather than safety interlocks alone. The repo carries two configs: laptop.cfg is the full one, and laptop_small.cfg cuts every constant down (BatteryMax = 4, MaxBrightness = 3, FanMax = 2) so that TLC finishes in reasonable time on a laptop modeling a laptop. The state space grows fast once brightness and fan speed are parameterized as integers.

An unreported counterexample is worth an issue. Catching an action that was left unconstrained is much of the point.