MACHINE WaterDispenser VARIABLES empty INVARIANT empty : BOOL INITIALISATION empty := FALSE OPERATIONS give = PRE empty = FALSE THEN CHOICE skip OR /* Last drink. */ empty := TRUE END END ; refill = PRE empty = TRUE THEN empty := FALSE END END