I played around with TLA+ a little. It is a model checker which focuses on state machines and time. If you care about data structures then Alloy should be more interesting. Since I work in embedded I deal with state machines a lot, so TLA+ fascinates me.
My first model was about two tasks interacting. The insight I got from the modelling was that shared variables need to be protected by mutexes. Thanks Captain Obvious.
My second model was about the state machine of a driver assistance function. For example, think about adaptive cruise control, which drives at a certain speed and automatically slows down if the driver before you does.
It can be off, active, or in a fault state. There is a separate temporary fault state because your sensors can be blind to due weather for a while or the seatbelt might not be closed. The normal fault state is permanent in the sense that something needs repair. At least usually, maybe it is just a bit-flip and repairs itself. The important part is that different notifications are shown to the driver although we do not model that here.
variables
seatbelt \in { "off" , "on", "unknown"},
sensors \in { "ok", "broken", "blind" },
brakes \in { "ok", "broken" };
macro environment()
begin
with x \in { "off" , "on"} do
seatbelt := x;
end with;
if brakes = "ok" then
with x \in { "ok", "broken" } do
brakes := x;
end with;
end if;
either
sensors := "broken";
or with x \in { "ok", "blind" } do
sensors := x;
end with;
end either;
end macro;
begin
Off:
environment();
if seatbelt = "unknown" \/ sensors = "broken" \/ brakes = "broken" then
goto Fault;
elsif seatbelt = "off" \/ sensors = "blind" then
goto TemporaryFault;
else
goto Active;
end if;
Active:
assert seatbelt = "on" /\ sensors = "ok" /\ brakes = "ok";
environment();
if seatbelt = "unknown" \/ sensors = "broken" \/ brakes = "broken" then
goto Fault;
elsif seatbelt = "off" \/ sensors = "blind" then
goto TemporaryFault;
else
goto Active;
end if;
TemporaryFault:
assert sensors = "blind" \/ seatbelt = "off";
environment();
if seatbelt = "on" /\ sensors = "ok" /\ brakes = "ok" then
goto Active;
elsif seatbelt = "unknown" \/ sensors = "broken" \/ brakes = "broken" then
goto Fault;
else
goto TemporaryFault;
end if;
Fault:
assert seatbelt = "unknown" \/ sensors = "broken" \/ brakes = "broken";
goto Off;
This little exercise found one error: The system transitioned to temporary fault due to blindness, then back to active when sensor became ok again. In the mean time the brakes were broken, so we should have transitioned to fault instead.
TLA+ works really was as an interactive system. The syntax and effort is reasonable. One obvious issue remains, it is left to me if the TLA+ model matches implementation and requirements. Still, the effort is so low that it makes sense to play with it once in a while. This is the easy way to call yourself a user of formal methods.
I can recommend the LearnTLA website. It contains everything you need for your first steps. Big thanks to Hillel Wayne who made TLA+ approachable.