[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Real-time TLA+ and stuttering

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?


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/41a094cb-09ae-4adf-8c26-483dd3d95e36%40googlegroups.com.