hi Stephan, thanks as always for your insightful answer. My thinking was that since the spec doesn't admit any traces in which the lights don't change at least once every K s (based on my understanding of TLA semantics) I was hoping that the model checker would agree and say that the invariant was indeed satisfied. But instead it reported deadlock. I did see where the deadlock is coming from, and I suppose its a way of rejecting those bad traces, but was somewhat surprising. I like your solution to the problem using a kind of "lookahead" to prevent DoNothing when a bound is about to expire, but it appears to me a way of getting TLC to do the right thing. Please let me know if I'm still missing something key.On Sunday, October 10, 2021 at 2:19:32 AM UTC-7 Stephan Merz wrote:Not sure I understand your question: TLC *does* model check your spec, it just (correctly) signals a deadlock, since the non-clock variables may stutter according to DoNothing until the clock exceeds its bound, at which point no action is enabled anymore. If you intend to avoid this, DoNothing needs a stronger time bound, see attached module for a possible definition.Since the modified spec generates an unbounded state space, you'll need to add a state constraint to your model, such asclock <= MAX_TIMEHope this helps,Stephan