On Tuesday, April 19, 2022 at 9:13:12 PM UTC+3 Markus Alexander Kuppe wrote:
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
> On Apr 19, 2022, at 7:03 AM, Vahab Jabrayilov <vaha...@xxxxxxxxx> wrote:
>
> 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
>
>
> --
> 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...@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a7afa6ff-ef8e-408a-a05a-d2ed637dd567n%40googlegroups.com.