hello, I've been reading the chapter on real-time in the Specifying Systems book. In there, real-time is represented by adding a variable now
, which is constrained in various ways, e.g. it must increase, can't exhibit zeno behavior, is weakly fair. However, now
itself is a variable beyond the control of the spec, it is presumably incremented by say a clock signal. However, it does seem to me that it conflicts with the stuttering invariance property of every TLA spec, in the sense that while the spec itself is technically stuttering invariant, once you tie now
to an external clock signal it seems that you would have to give up stuttering invariance or v.v. to retain stuttering invariance, now
cannot be tied to a fixed clock signal. Is that right, or am I misreading the example?