Re: [tlaplus] How to model check this "real-time" spec?

[ns <nedsri1988@xxxxxxxxx>]

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 as 

clock <= MAX_TIME

Hope this helps,

Stephan

-- 
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/6ffc80d4-e218-40cc-8f53-bca2c868dbb6n%40googlegroups.com.