TLA+ Microwave Model
March 26, 2026 ยท View on GitHub
This example models a very basic microwave oven with very simple state:
- door open or closed
- radiation on or off
- time remaining in seconds between zero and some maximum
The model has various actions:
- opening/closing the door
- starting/canceling the heater (magnetron)
- incrementing/counting down time
These typically correspond to buttons and other affordances in the appliance's user interface or internal events.
Typing
TLA+ does not support static typing, but we can define a (dynamic) invariant TypeOK that constrains which variable can take on which values.
Safety
Checking the intial model succeeds, but...
What does it actually mean for the microwave to be safe?
Typically, we wouldn't want it to be heating when the door is open.
So let's define a DoorSafety invariant accordingly.
Now the initial model fails, and we need to fix it so it satisfies the invariant!
- stage 1: turn off when opening door
- stage 2: don't allow turning on when door is open
Liveness
Is this notion of safety enough?
How do we know it won't accidentally keep running, overheat, and catch on fire?
We need some kind of HeatLiveness property.
This detects whether the model could go into stuttering, i.e., staying in the same state without getting closer to finishing.
We need to enable weak fairness (WF) to break this stutter-invariance! (See also www.hillelwayne.com/post/fairness.)
We can explore other temporal properties, e.g., RunsUntilDoneOrInterrupted.
Checking the model in various configurations
We have created separate configuration files reflecting the various possible model configuration settings.
| Configuration | Result | Description |
|---|---|---|
| Microwave.cfg | success | unsafe, unchecked |
| Microwave_1_Checked.cfg | safety failure | unsafe, checked |
| Microwave_2_PartiallySafe.cfg | safety failure | still unsafe, checked |
| Microwave_3_Safe.cfg | success | safe and checked |
| Microwave_4_Stuttering.cfg | liveness failure | stuttering |
| Microwave_5_Live.cfg | success | weak fairness |
To check the model in any configuration other than the default (Microwave.cfg), you need to specify the corresponding .cfg file as an option either interactively or on the command-line.
When using the TLA extension in Visual Studio Code, you can run the TLA+ model checker interactively:
- right-click on
Microwave.tla - Check Model with TLC
At this point, a dialog appears where you can add an option to choose the desired configuration, e.g.,
-config Microwave_1_Checked.cfg
In the same environment, you can also run TLC on the command line as follows:
java -jar ~/.vscode/extensions/tlaplus.vscode-ide-*/tools/tla2tools.jar -config Microwave_2_PartiallySafe.cfg Microwave.tla
Related publications
We have included this example in various formal methods education papers and presentations: