|It sounds like you have unbounded queues: the producer can always append an item to some queue. In that case, the state space will be infinite and TLC will never finish. You can bound the number of states that TLC considers by imposing a state constraint (cf. tab "Spec Options", click on "Additional Spec Options" if that tab is not present), for example "Len(queue) <= 3" and gain confidence through incomplete verification. Add similar constraints for other potential sources of infinite state spaces, for example if you have a counter to number the products.|
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/9D9886EA-0C4A-47BF-80D1-EFB786CB5AF7%40gmail.com.