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

[tlaplus] Automatically checking for different model constants

Hi everyone,

I am into learning TLA+ and implemented a well-known Cosumer and Producer problem. 

When I test for deadlock model didn't get find any for the set of model constants I provided.
But when we discuss with my advisor, found out a deadlock for a specific set of constant values(e.g 1 producer, 2 consumer with buffer size of 1). My question is,

Is there any way of automatically checking for different values of model constants ? How can I truly find out that model is deadlock free for all kind of model constants ?

Link to the specification : https://gist.github.com/vjabrayilov/aa446420ea5bfb3c6147a80d5223149f

All the best,

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/a7afa6ff-ef8e-408a-a05a-d2ed637dd567n%40googlegroups.com.