Declare the state set as an enum whose constants are the spec state names.

Answer

enum PodState { CONNECTED, LISTED, SENT, REJECTED, CLOSED } PodState state = PodState.CONNECTED; while (state != PodState.CLOSED) { state = step(state, in, out); }

The enum constants are copied verbatim from the specification, which is what lets a marker read the document and the code side by side. The loop condition is the terminal-state rule made executable: there is exactly one way out, so no path can leave the session hanging.