Most programming languages do not support something like Day as a built-in type. But fortunately, they usually support integers. So I'm going to represent the Day machine in terms of integers modulo-7.
Mod7Counter = (
).
My Mod7Counter concrete machine has a single action, inc, which is defined in the obvious way. I've intentionally defined Mod7Counter's set of states to be the set of integers rather than just the integers between 0 and 6, inclusive. (What are the reachable states of Mod7Counter?)