I'm trying to set a created date on files.
Maybe this is what you meant by a test clock... what you could do is have each event that needs a timestamp increment an integer index variable t, and time[t] is the time of the event with the time index t. In your model you wouldn't need to have the "time", the actual wall clock time, you could just have t=1, t=2, etc. Then to show that a HEAD or GET returns the correct time the data was submitted, you could have the methods return t=2 as the created date, where the data was submitted in event 2, without having to model which particular time t=2 was.
It's interesting as it complicates testing; you can't execute that exact sequence to demonstrate that the store appears to have create consistency, or if you do, you'd better have some idea of what a good delay between the negative GET and the PUT should be. And it'd have to be a coded in delay, as the usual probe+sleep strategy doesn't work, as it just refreshes the entry in the cache.
A thought: you could add a "DELAY" event to your model; so that e.g. a "~GET DELAY PUT GET" would successfully get what was put; without having to model how long the delay was in wall clock time.