Real-time TLA+ and stuttering

81 views
Skip to first unread message

ns

unread,
Jan 27, 2020, 1:16:58 PM1/27/20
to tlaplus
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
Reply all
Reply to author
Forward
0 new messages