TLA+ Example

kyle.tla

---- MODULE Kyle1 ----
(* Kyle has a rule that turns on his garage light for 10 minutes every time
   he opens his garage door.  Unfortunately, Kyle has to go into his garage
   frequently (in order to get the next exotic tool he urgently needs
   for a project).  Does his rule really do what he wants? *)
   
EXTENDS Naturals, Sequences

VARIABLES lts,     \* Light timers
          o,       \* Interal state for deciding whether to open the door
          lightOn  \* State of the light

Init == /\ lts = <<>> \* No timers initially.
        /\ o = 1
        /\ lightOn = FALSE

(* Expire removes timers that have expired. *)
Expire(ts) == SelectSeq(ts, LAMBDA t : t >= 0)

(* Tick decrements and expires timers. *)
Tick(ts) == Expire([ i \in DOMAIN ts |-> ts[i] - 1])

(* Firing reports if a timer is firing. *)
Firing(ts) == \E t \in DOMAIN ts : ts[t] = 0

(* This "Next" starts a new timer each time the door opens.  That
   behavior turns out to be bad. *)
BadNext == /\ o' \in 1..20 \* 1 in 20 chance that the door is opened.
           /\ IF o = 5 \* If door is opened ...
              THEN /\ lts' = Append(Tick(lts), 10)
                   /\ lightOn' = TRUE
              ELSE /\ lts' = Tick(lts)
                   /\ lightOn' = IF Firing(lts')
                                 THEN FALSE \* Timer turns the light off.
                                 ELSE lightOn

(* This "Next" resets the one and only timer each time the door opens,
   and that's the kind of behavior we think we want. *)
GoodNext == /\ o' \in 1..20 \* 1 in 20 chance that the door is opened.
            /\ IF o = 5 \* If door is opened ...
               THEN /\ lts' = <<10>> \* Reset the timer!
                    /\ lightOn' = TRUE
               ELSE /\ lts' = Tick(lts)
                    /\ lightOn' = IF Firing(lts')
                                  THEN FALSE
                                  ELSE lightOn
                                                               
(* We don't want to be surprised by the light turning off. *)
Surprised == /\ lightOn
             /\ Firing(lts)

====