[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Automatically checking for different model constants
- From: Vahab Jabrayilov <vahabfuad@xxxxxxxxx>
- Date: Tue, 19 Apr 2022 07:03:58 -0700 (PDT)
- Ironport-data: A9a23:+OAUsao6ibWQDaAUJVMwx1aqSUZeBmK/YBIvgKrLsJaIsI4StFCzt garIBmEM/iPa2uhfo9zb4Xi90IAv5LVndNkTwNorC83Fn9GpePIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKicfHkZqTZMEE/Nszo68wICqtMu0IDR7z+l4 4uo+ZWDYQ79gVaYD0pNg069gEM31BjNkGhA1rAOTagjUIj2yhH5pLpGTU2AByOQrrt8RoZWd M6fpF2NxV41yj92Yj+TfhkXRWVRKlLaFVDmZnO7wMFOiDAazsA5+v5T2Pbx9S67hh3R9+2dx umhurTpESYmAJDvo90EeDt2Gh9ODPRPoaDIdC3XXcy7lyUqclPpyvRqSVg1ZMgWo7YnR25J8 vMcJXYGaRXra+CemurqDLkxwJ55do+ybNN3VnJIlVk1Cd46RZnbR7jRptVe1x0b3ZpiLdblW fc2QxBWTC+fRD9mH3guJbwBrsGNo1DXfDpfp1aYqrAw/nDIigd21dABNfKOIIfaFZoPxy50o ErY7WLJQRQjc+abzByG0lu+tPLAtnjCDdd6+LqQr6Y22jV/3Fc7BBwNXkagutGljkf4XslFb k0S4Csn66k07k2iCNfnNyBUu1aBtx8YHsNTSqg0sVHdjKXT5AmdCy4PSTsphMEaWNEeHGQL2 WG0vOjQHBdNnrSreUPE/+6LombnUcQKFlMqaSgBRAoDxtDspoAvkx7CJuqP9obl3rUZ/hmgk 1i3QDgCa6Y71pFUiv3qlbzTq3f9+ciTF19dChD/Bzr9tmtEiJiZi5tEAGU3AN5FJYedC0CC5 T0KwpjOqu8JCp6JmWqGR+Bl8FCVCxStb2O0bb1HRcFJG9GRF5iLIdA4DNZWeBYBDyr8UWW1C HI/QCsIjHOpAFOkbLVsf6W6ANkwwK7rGLzND66JNoAVMskhKVffpEmCgHJ8OUi9wCDAdolva f+mnTqEUB729Iw8nGHmGLxNuVPV7nlmnzKCGfgXMChLIZLHPCLPIVv0GFSJae894cu5TPb9o r5i2z+x40wHCIXWO3GJmaZKdABiBSVlWfje9pMPHsbeclsOMDxwVpf5nOJxE6Q7xfg9vrmTp RmVBBQHoGcTcFWCdW1mnFg9Ne+zNXu+xFpgVRER0aGAgiF9Otf+sP1CL/Pav9APrYRe8BK9d NFdE+3oPxiFYm6vF+01YcavoYp8Wg6sgA7SbSOpbCJmIcxvQAvG/tLrZAzy7DJIBS2y7JNsr 7ql3wLdYJwCWwUzXJ2NManwkQy87SoHheZ/f0rUOd0PKk/ix45ndn7qhfgtLsBQdBjOn2PI1 wufDRoCi/PKpos5rIvAiaye/tWmFuJ/GgxRGGyCteS6MizT/2yCx45cUbbQLWqNCj+soKj7P Ldb1fDxNvEDjW1miYskHuY517866vvuu6RekVZpEXDNWFKhVeFtL3yA6s9Q7/Efy7Jcvzy2b UKB4NxtP7uEZZH+G1kLKQt5N+mO2KhPyDnf5Pg4On/3/Ctm4L2DXRkANhWAknUDfrRyN4whz Og7v9MO8Eq0jR9zaoSKiSVd9mKtKH0cUvR37cpDW9C11Qd7mEtfZZH8CzPt5M3dYdt7NER3c CSfg7DPhugBy0fPLygzGHzK0bYPjJgCokoWnloLJlDMg9mcw/FujE0X/jMwQQBYiB5A1rsra GRsMkR0I4SI/itp1JcfBTHyQ1kZCU3L4FH1xnsIiHbdExuiWFvLITBvIu2K5k0Yrz9Rc2kJ+ LCD1FvjSivgeM2tjCI+VVQ7+67mRN116gqQl8egEMCIEIM9fCL+x6qnY2MHpli8XpNg2BCZ9 bYzpbgzdKvgKCQLqLc6AYSy2rMXRxSJK3ZFXOl6uqgOGDiEKj213DGPLWG3e99MdqyRqhbjV JIxK5IdTQm62QaPsisfWfwGLYhykaN7/9EFYL7qeTMLvrfD/DNlvIiMp3r+mHMzWIcp1sknL Z7JbHSNFWufgXYSkGjI68ZePXegJsUAbRX4wfvy6/gDDJkZsethfExugKG4uW6ZbFlu8x6O5 l+RYqbXy6l7yt0pkdK8QuNMAAK7Ld61X+ONqVjhv9NLZNLJEMHPqwJF9QW9bloOZeMcC4Zti LCAkN/rx0eZ7rw4ZGbUxsuaHK5T6MTuAedaP6ob9pWBcfduhSMt3/cCx4x8AZlAkdcY/8r+A gXhOJv2etkSVNNQgnZSbkCy1vrb57vfNs/dSeGV9pxgySTxFSTIK9So8XLmd2ZGbjROMJr7Y uMxk+j7/chW9eygGzddb8yLwPZEzJvLVqwheNn8uiOfE3GzxFiFv9MOUPbmBS7jUhG5LSox3 X4JqtUSuvh/VGEkAey1a7BPgyA=
- Ironport-hdrordr: A9a23:7jn536MaEyWdwcBcTjejsMiBIKoaSvp037BL7TEMdfUxSKb0qy nApoV86faZskdpZJnP8erwT5VpbxvnhOpICMoqTMSftDCPghrcEGga1/qV/9SCIVyCygbpvp 0QA5SWdueAdmSS1vyKkTVQeuxIqLL3ktHNuQ659QYScehEUc5dBmxCe3ym+yNNNXF77VtQLu v+2iOFnVSdkLYsAvhSthI+Lpr+ThHw9a4PkXU9dmEaAcC17ULMmdnHLyQ=
- Ironport-sdr: JMNRQbiq6pYWwI2Vfcm1YI3K7oxYO95o/WZJSIvIr1zhBizeGoZk0ZNiiERWYfvTken8P3YiGi grGE++y4Dq/LItCiO44DZR6upWHXZnoUamYezMqqHk/oK0qEFTnJ/CX1ilWYi7hL49UuI6LbtF IY6MIuvJEnbi964LwDtqm0Vexh8WDVdnlOaqiMkS3OSuisK0eSPOWBUPPmhuQoNMhwkSea1Nwm +XmAjMws10mxaD25ndHcW6WZvpf2/1GlmW57Z89yxwIAi+F2NlqZD26vVUZrXeErmqQ00T4cpR zyKi7iojSJXkd5oNn0ZpfbOC
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.