Edit: looks like they're talking about this: https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2B What I describe below is not related. -

Edit: looks like they're talking about this: https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2B What I describe below is not related. ---- Not the OP, but here's a stab at it... In state machines commonly used in embedded C code, each state is represented either by a function or by a struct that contains a function pointer. The state machine calls the current state function in a loop or whenever relevant events happen, and that function returns a pointer to the next state, calculated based on inputs. If there is no state transition, then the function returns NULL or returns its own state.