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 ?
All the best,
Vahab