Web Based TLA+ Microwave
This is a locally hosted microwave simulator intended as an introduction to TLA+. It pairs a simple microwave interface with the state traces the model produces.
It is built with Spring Boot (Java) and Vaadin (also Java). The program starts from a terminal and runs in a browser. Development took two weeks from start to finish. Issues are tracked at https://github.com/EricSpencer00/interactive-microwave-tla/issues.
Two toggles change what the model does. Power button mode adds a further parameter to the state traces. Dangerous mode allows the microwave to operate while the door is open.
Violating the microwave's SAFE configuration is caught by the mock TLC checker, which reports that the sequence of actions produced an unsafe state. A real TLC checker explores all states and executions of the microwave and reports whether an unsafe state is reachable at all.
The interactive guide on the left holds a tutorial for the application, a short introduction to TLA+ syntax, and an explanation of the state traces.
---- MODULE Microwave ----
EXTENDS Integers, TLC
VARIABLES door, time, radiation
CONSTANTS OPEN, CLOSED, ON, OFF
Init ==
/\ door = CLOSED
/\ time = 0
/\ radiation = OFF
IncrementTime ==
/\ UNCHANGED <>
/\ time' = time + 3
Start ==
/\ time > 0
/\ door = CLOSED
/\ radiation' = ON
/\ UNCHANGED <>
Tick ==
/\ time > 0
/\ time' = time - 1
/\ UNCHANGED <>
/\ radiation' = IF time' = 0 THEN OFF ELSE radiation
Cancel ==
/\ time' = 0
/\ radiation' = OFF
/\ UNCHANGED <>
CloseDoor ==
/\ door = OPEN
/\ door' = CLOSED
/\ UNCHANGED <>
OpenDoor ==
/\ door = CLOSED
/\ door' = OPEN
/\ radiation' = OFF
/\ UNCHANGED <>
Next == IncrementTime \/ Start \/ Tick \/ Cancel \/ CloseDoor \/ OpenDoor
Safe == ~(radiation = ON /\ door = OPEN)
Spec == Init /\ [][Next]_<>
====
Once a .tla file and a .cfg file are defined, a TLC checker can be run against them, producing output of the kind shown below. This example comes from the interactive microwave, so it is not identical to the output of a real TLC run.
\* <Initial line 10, col 3 to line 13, col 36 of module Microwave>
STATE_1 ==
/\ door = "closed"
/\ timeRemaining = 0
/\ radiation = "off"
(* Power Button ENABLED *)
\* <TogglePower line 15, col 3 to line 18, col 36 of module Microwave>
STATE_3 ==
/\ door = "closed"
/\ timeRemaining = 0
/\ radiation = "off"
/\ power = "on"
\* <TogglePower line 15, col 3 to line 18, col 36 of module Microwave>
STATE_4 ==
/\ door = "closed"
/\ timeRemaining = 0
/\ radiation = "off"
/\ power = "off"
\* <Cancel line 35, col 3 to line 38, col 36 of module Microwave>
STATE_5 ==
/\ door = "closed"
/\ timeRemaining = 0
/\ radiation = "off"
/\ power = "off"
\* <OpenDoor line 40, col 3 to line 43, col 36 of module Microwave>
STATE_6 ==
/\ door = "open"
/\ timeRemaining = 0
/\ radiation = "off"
/\ power = "off"
\* <CloseDoor line 45, col 3 to line 48, col 36 of module Microwave>
STATE_7 ==
/\ door = "closed"
/\ timeRemaining = 0
/\ radiation = "off"
/\ power = "off"
\* IncrementTime Violation Attempt - Power is OFF
\* <TogglePower line 15, col 3 to line 18, col 36 of module Microwave>
STATE_9 ==
/\ door = "closed"
/\ timeRemaining = 0
/\ radiation = "off"
/\ power = "on"
\* <IncrementTime line 20, col 3 to line 23, col 36 of module Microwave>
STATE_10 ==
/\ door = "closed"
/\ timeRemaining = 3
/\ radiation = "off"
/\ power = "on"
\* <IncrementTime line 20, col 3 to line 23, col 36 of module Microwave>
STATE_11 ==
/\ door = "closed"
/\ timeRemaining = 6
/\ radiation = "off"
/\ power = "on"
\* <Start line 25, col 3 to line 28, col 36 of module Microwave>
STATE_12 ==
/\ door = "closed"
/\ timeRemaining = 6
/\ radiation = "on"
/\ power = "on"
\* <Tick line 30, col 3 to line 33, col 36 of module Microwave>
STATE_13 ==
/\ door = "closed"
/\ timeRemaining = 5
/\ radiation = "on"
/\ power = "on"
\* <Tick line 30, col 3 to line 33, col 36 of module Microwave>
STATE_14 ==
/\ door = "closed"
/\ timeRemaining = 4
/\ radiation = "on"
/\ power = "on"
\* <Tick line 30, col 3 to line 33, col 36 of module Microwave>
STATE_15 ==
/\ door = "closed"
/\ timeRemaining = 3
/\ radiation = "on"
/\ power = "on"
\* <Tick line 30, col 3 to line 33, col 36 of module Microwave>
STATE_16 ==
/\ door = "closed"
/\ timeRemaining = 2
/\ radiation = "on"
/\ power = "on"
\* <Tick line 30, col 3 to line 33, col 36 of module Microwave>
STATE_17 ==
/\ door = "closed"
/\ timeRemaining = 1
/\ radiation = "on"
/\ power = "on"
\* <Tick line 30, col 3 to line 33, col 36 of module Microwave>
STATE_18 ==
/\ door = "closed"
/\ timeRemaining = 0
/\ radiation = "off"
/\ power = "on"
(* Mode changed to DANGEROUS *)
(* Mode changed to SAFE *)
(* Power Button DISABLED *)
\* <Power Button Disabled line 50, col 3 to line 53, col 36 of module Microwave>
STATE_22 ==
/\ door = "closed"
/\ timeRemaining = 0
/\ radiation = "off"