The Day abstract machine, has one tick action.
Day is like an enumerated type in Pascal or Ada; its set of states is just the days of the week:
Day = ( ).