[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Automatically checking for different model constants
- From: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>
- Date: Tue, 19 Apr 2022 11:13:02 -0700
- Ironport-data: A9a23:NrgUSa95Ii+UxDUOjXRADrUDB3uTJUtcMsCJ2f8bNWPcYEJGY0x3n GdMCGrVM/2Ja2unLdx/O4m//BsPsJHUm4dmHQBuqiBEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvylYAL9EngZqTVMEU/Nsjo+3b9h6mJUqYLhWVnV5 Yqj+5e31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Z0 NpGv4W/R18SO4KVpMYYUgJnImJ0BPgTkFPHCSDXXc27ykTHdz7zxqwrAhxoe4If/elzDCdF8 vlwxDIlNEjSwbLrhuvhGq8x2KzPL+GzVG8bkm1kxCndEO1lS5bIaY7q1+d37BsAr+l0N9DuV 5U+SxNKQy3tTEBsC31KIboxm+CngnTwaTpFsEnTrq0yi4TW5Fcri+i8bICJEjCMbcFQjhqJm zr6xXX0Jks8Jua7xh2rsVv504cjmguiAN5IfFGizdZmgUaY23cIIAESXB2+uuP8i0ikWtsZK koO+yNoo7JayaCwZtz0Xhn9v3vd+xBBBZxfFOo17AzLwa3Ri+qEOoQaZiZOY9Y/u8FufjkFj 2OrmtLyOg0suoTAHBpx6YyohT+1PCEUK0oLaikFURYJ7rHfTGcb3kKnojFLQP7dszHlJd3j6 2vV83Vm1t3/meZOhvrrpwmW6965jsGRFlZd2+nBYo6yAupEiGONYoWp7R3E6K8FItvHCFaGu 3cAlo6V6+Vm4XCxeM6lH7tl8FKBva7t3NjgbbhHQ8lJG9OFpiTLQGyoyGsiTHqFy+5dEdMTX GfduBlK+LhYN2awYKl8buqZUpp3lfK7RYW1C6iMNrKih6SdkifXrEmCgmbAjwjQfLQEzMnTx L/AIZ38Ui1KYUiZ5GPuHbZMjdfHORzSNUuKHcyhp/hW+bWZY3GRRN843KimP4gEAFe/iFyNq 753bpPUoz0GCbGWSnSJrOY7cA9SRVBmVcGeg5EGK4arf1s2cEl/UaO56e16IORNwf8F/tokC 1n4BSe0PnKh1S2bQehLA1g4AI7SsWFX9CtlZn19YQz1gxDOo++Htc8iSnf+RpF/nMQL8BK+Z 6BtlxyoDqsdRzLZ1S4aaJWh/oVueA7y21CBOC2qZDUwZZl9XxeP8djhJ1O9+C4LByuxlM0/v 7zxhliAGMFcGVtvXJTMdfai71KtpnxByuh8aE3Ff4tIc0L2/Yk2diH816dlI8wFJRjZ6CGd0 gKaXUURqeXX+tZn9NTMgLuYop3vH+YnRhhWGGzS7LCXMyjG/zP/kNEaD7vSJWjQDTqm9r+ja ONZy+DHHMcGxFsa4ZBhF7tLzL4l44e9rbFtyAk5Tm7AaE6mC+89L3SLhJIdtqBEyrJDgwauX lOT/d1WZeeANM//SQBDKw0iYeCO2usThyHJq/8yJRyitiNw+bOGV2RUPgWN2XwGd+Iub916z LdzotMS5iy+lgEuboSMgBdS+jneNXcHSagm6swXDYK32AomzlZOPc7VBiPsusrdbtxNNgw1J 2bRivecwbtbwUXGfjw4En2UhbhRgpEHuRZryl4eJgTWxoCU2KdvhBABoy4qSgl1zwlc174hM GZcMUAod76F+C1lhZQeUm39SQVAHwGk/FfswV8FyD/QQ0WyCDyfKWQ8PfqKrk8e9G1YczdB+ 6yA0yPgWDDjc8yyhXRiCBI49ay8FIUvtRDEg92tBM+fHpM3STXihaCqaGUSrAb/GoU6g0ie/ btm++N5aKvaMy8MovxrUNLDjutOFx3UdnZfRfxB/b8SGT2Ocj+F3zXTeVu6fdlAJqCX/EK0V 55nKs5VC0Xs1DqStitJQukDObhphOVv690FdbfmY2UBtvyQtD10qNXM8iHmgHIwBM5zm902M ILbej+PTj6KiX1PlzOfpcVIIDDjM9wNZQm5w+XstetUSdQMt+ZjdUx02byx5i3HPAxi9hOSn QXCe66GkLA4mNo0x9PhQvdZGgG5CdLvT+DUogq9hNJDMIHUOsDUugJJ91TqMmy651fKtwibS FhMjDL24K8BlLM/UmSchJzYUqcUu4O9W+1YNs+xJ35f9cdHtAkA/DNbk11U67QQ+D+e2iVjb wS/b8S0eNEPXMpF3ztebC02/9M1FfHsdqm5zc+ih63kN/XeuDAr6Puo8njmaWxUbCgVI4a4A Qjx0xprCha0s6wUbCI56zpa71OU7bMttWbKtzE8iNVAMlSVvw==
- Ironport-hdrordr: A9a23:zfDDH6gIxYSsAKiIGneLLaQGcXBQXngji2hC6mlwRA09TyXGra ze5MjzhCWY+U8ssS8b86HnBEDgewKiyXcR2+Ys1NiZLXnbUQeTXf1fBM7Zskjd88OXzJ8d6U 9PG5IORuEYTmIKx/oT2WGDYpkdKaC8geCVbVK09QYncegVUdAV0+4JMHfkLqQsfngPOXNRLv P1jbsi1kHQBEj7dv7LfEXtHdKz1OEj8qiWKCLuKCRH1ODkt0LY1FeVKWnr4v/eOwk/pIvKMl Kkr+U63MueW0HR8G6R64Ye1eU0pDPtoeEzcvBleqMuW0LRY8+TFeYRPIGqjXQOuemqrHwqnN PPrxplH8M2xWjWYnjdm2qh5zXd
- Ironport-sdr: Ri3HJ7PBxTw/QI6WGeVk9LrprwXMXnWE7wNPu0P4Ytfr1XWtTO/nB2HaLqP6KdqQRridKOq9h5 GUE5jqLRpze7RFC35608fOFpRmq0F4jZg/kVjIu5O0Djk5TE9hFJydDedl2k8dgWx9xavEWddC 1dfhapLPVgtq1h/j6nlhQlBfR141KknHXlZ8qx6uazC6mC4O+KFzn6HKhmnImGq955FUqcuoop +Hw+GIED8n+pynPGTIeMT7Gdn39NccxP7dQN8p9Al1IpM6d9bwqq2Q083d54DqJoL7bR68TeGq HXjnchpJOkin9hYmtBT5lnl/
- References: <a7afa6ff-ef8e-408a-a05a-d2ed637dd567n@googlegroups.com>
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.