Automatically checking for different model constants

[Vahab Jabrayilov]

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,

Vahab

[Markus Kuppe]

Hi Vahab,

chapter v06 [1] of my TLA+ tutorial shows how to do this for this very problem for safety checking. Chapter v30 [2] outlines in the light of liveness checking.

Markus

[1] https://github.com/lemmy/BlockingQueue/commit/e49a31a9c96fca5ad4ba1c8c419cd472a2857301
[2]
https://github.com/lemmy/BlockingQueue/commit/be16c92d5eba45a3be6f0ab508338637cb1f46e5

> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a7afa6ff-ef8e-408a-a05a-d2ed637dd567n%40googlegroups.com.

[Vahab Jabrayilov]

Thanks a lot Markus for your reply.