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?
thanks
-ns