A newbie question about writing specs in TLA.
Below are two specs (ATR and ATR2) of a system with two boolean state components (a "lock" and a "beacon") and three "buttons": lock, unlock, toggleBeacon. The idea is that toggleBeacon is disabled when the system is locked; when the system is unlocked, toggleBeacon toggles the beacon state; locking the system also switches off the beacon.
ATR2 is almost identical to ATR except that toggleBeacon will additionally lock the system if the beacon was on (whereas, in ATR, toggleBeacon always leaves the system unlocked).
What I find unintuitive is that ATR2 *implements* ATR: TLC confirms that the ATR2 Spec implies the ATR Spec.
I can see why this is so: the ATR2 behaviours that transition from (beacon=TRUE,lock=FALSE) to (beacon=FALSE,LOCK=FALSE) area also allowed by ATR. Intuitively though, the *causes* are different; in ATR this can only be caused by pressing the lock button but in ATR2 it can also be caused by pressing the toggleBeacon button. My intuition is that ATR2 is not a "good" implementation of ATR, because its toggleBeacon button behaves differently.
It seems that I need either to adjust my intuitions about the meaning of "implements" or specify "user actions" (like pressing buttons) in some less abstract way. Or...? Any advice would be very welcome.
Seb
-------------------------------- MODULE ATR --------------------------------
VARIABLES locked, beacon
TypeOK == locked \in BOOLEAN /\ beacon \in BOOLEAN
Init == locked = TRUE /\ beacon = FALSE
unlock ==
/\ locked
/\ locked' = FALSE
/\ beacon' = FALSE
lock ==
/\ locked' = TRUE
/\ beacon' = FALSE
toggleBeacon ==
/\ ~locked
/\ beacon' = ~beacon
/\ UNCHANGED locked
Next == unlock \/ lock \/ toggleBeacon
Spec == Init /\ [][Next]_<<locked, beacon>>
=============================================================================
-------------------------------- MODULE ATR2 --------------------------------
VARIABLES locked, beacon
TypeOK == locked \in BOOLEAN /\ beacon \in BOOLEAN
Init == locked = TRUE /\ beacon = FALSE
unlock ==
/\ locked
/\ locked' = FALSE
/\ beacon' = FALSE
lock ==
/\ locked' = TRUE
/\ beacon' = FALSE
toggleBeacon ==
/\ ~locked
/\ beacon' = ~beacon
/\ locked' = beacon
Next == unlock \/ lock \/ toggleBeacon
Spec == Init /\ [][Next]_<<locked, beacon>>
ATR1 == INSTANCE ATR
THEOREM Spec => ATR1!Spec
=============================================================================