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

Re: [tlaplus] Automatically checking for different model constants

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

-- 
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/3B8EA050-FE46-4F0E-A57A-D5EC730C0D2D%40lemmster.de.