Comment by seanhunter

> instead of thinking about how state transition you focus on what the program is allowed to perform

The state transition is what the program is or isn't allowed to perform. The state they're talking about in the invariant isn't the program state, it's the game state.