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.
That is all that matters.
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.
The events that you call "causes" weren't modelled by your specification, since they aren't represented in the possible behaviours. Note you only consider declare variables "locked" and "beacon".
The bits of the spec that you associate such "causes" with, namely "toggleBeacon", are just identifiers for the corresponding actions they define. These are auxiliary definitions that allow you to write the temporal formula Next, and consequently the temporal formula Spec, in a modular fashion rather than as a long unreadable one-liner. But in the end all you have is a temporal formula Spec that is true of some behaviours and false of others. And that's your specification.