One thing that you can often get by moving the state machine a bit away from the source code as tends to be the case with these libraries is a definition that specifies I/O more concretely. In something like the Unity3D Tick() case, I/O is open-ended: All game state is available, and that state may itself impact when Tick() is called via various concerns of concurrency(timing, update order, etc.). When trying to apply a formal model it's usually a really bad sign to see a very broad "tick" or "update" callback dumped into execution - it leads towards hacky code that sets flags and uses frame boundaries to confirm events.

Game engines don't always have the best examples of these patterns, since games can so often get away with shoddy usage.