This https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6 starts with an excellent description of how to model with state transitions in Electrum.
The point about asserting that everything else stays the same, is that Alloy will use any flexibility it is permitted to explore a model. This is good because we only specify what we care about. You might also check out this discussion which I found useful https://alloytools.discourse.group/t/facts-vs-assertions