[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Number of possible behaviors and fairness
- From: jack malkovick <sillymouse333@xxxxxxxxx>
- Date: Tue, 1 Mar 2022 23:38:57 -0800 (PST)
- Ironport-data: A9a23:SI2DAKnVtG6pjkqZ4+pFIozo5gwkI0RdPkR7XQ2eYbSJt1+Wr1Gzt xIdXTuAM/qINzT9KNp3aNyz80JU68ODmoc1HVY9qnthRVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvykTres1hlZHWeIcg944f5Ys7N/09YAbeSRWVvX4 4up+5eHYjdJ5hYtWo4qw/LbwP9QlK+q0N8olgRWiSdj4TcyP1FMZH4uDfnZw0nQGuG4LcbmL wr394xVy0uCl/sb5nxJpZ6gGqECaua60QFjERO6UYD66vRJjnRaPqrWqJPwZG8P4whlkeydx /12lb2MSQERH5TrnblNQzhhKX8vIepZreqvzXiX6aR/zmXDenrohvJvVQQ4ZNxCvOlwBm5K+ LoTLzVlghKr3brnhuLmDLAy2YJ6fZOD0IA34hmMyRnFCf8+RY3YAK/M7vVz4WoapvBxIN/zT eA0V2QwVzXpRjJ2F3goMMlgscaAiX74fDlVp0iSuLIspWPUyWSd1ZC3a4uOIoDVHK25mG66+ V3i4CfFJC0+ap+b1WGk6nKdnvHQyHaTtIU6TeXkrJaGmma7ym0IAwANTnOnpfD/j1WkHtNZM U0dvCsot6k7skKxJuQRRDW9qX+A+xkdAp9eSrxgrg6KzaXQ7kCSAW1soiN9hMIOj+8XeTws7 n6wuNa0VSxOiYfLGG7a6eLBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zQMZZafWlSVnNL yC2QDsW3OpM0JZav0mv1RWW3GL2/8mhohsdv12PBgqYAhVFiJlJjrFEBHDe5PdEaYGYFxyP5 Sle3ceZ6+8KANeGkynlrAQx8FOBuKzt3N702wUH83wdG9KFpifLkWd4vGEWGauRGpxYEQIFm WeK0e+r2LddPWGxcYh8aJ+rBsIhwMDITIq5CKmJP4YWOsQpL2drGR2Cg2bAjwgBd2B8wckC1 WuzLK5A8F5GU/08lGPuLwvj+eZym3tjrY8seXwL503/jeD2iI+9RrACP1+DBt3VH4vVyDg5B +13Zpvi40wHDoXWO3CHmaZOcw1iBSVkXfje9pwGHsbec1EOMDxwV5f5nOJxE6Q7xP89vrmTr hmAtrpwkQWXaYvvdV7WOxiOqdrHAf5CkJ7MFXd0bAbwhiN6Ot7HAWV2X8JfQITLPddLlZZcJ 8Tpse3aahiWYjiYqTkbc7fnq4luKEaiiQ6UZnT3bz84cJptSBbO58f/OADo8XBWXCawsMI/p Zym1x/aEMpYHF05U5iJZaL91U61sFgchPl2AxnCLO5VdRi+64NtMSHw0qI6LphUexXOzzeXz SiMBhIcqbWfqoM56oibiqWNroPvGOx7RxIIE27e5LewFC/b4mvzmd8aALjUJWjQDTqm9r+ja ONZy+DHHMcGxFsa4ZBhF7tLzL4l44S9qrJfyDNiFiqZYlmuDIRmPSDaj8RCs6t6xohZtxGzb USB94QIIr6OIs7kTAccKQd8NbaD2PgYlyPo4OwxMVn94CMrrrOLXV8LYUuDjytSKLZ6KoQ42 fxns8kTslTthh0vO9eAryZV62XdfidbCv546M4XUN3xlw4m6lBeepiAWCX415eCNodXOU4wL z7I2afPiugOxkfGdHZvR3HB0fAH2cYLsRFOiVgDfhGHw4ufwPAw2xJV/HI8SQEMlkdL1Od6O 25KMUxpJPXRo2052pAbB238SRtcABC5+1DqzwdbnmPuSUT1BHfGK3cwOLrQ8U1IoWZdZSRm+ qqFwmLpDWTjcM3rgHtgXEdkr+DkH9N28QLGlc+9GNmdBNw/aDzsjaLtPjVY+ke6X5Nu3RSZ5 vRs5/t6cqbhNCQdi6I8DIae2LsKTw2cPypJRvQ4pPEFGmTVeTeT3zmSKhHhIZgUfKOUrkLoW dZzIs9vVgil0HrcpD4sA6NRcaR/m+Qk5YZfd77neTwPv7eF8ms7sI7M7jOswygkWdJzid17J YTWeDaPVGeXgDxbgWjQtI5YPmOgZcQfIxbh1vu+6uQDGp8O7LN2fUcp3ufmtnmZKlE7rRedv QeGYK6PiuI7mN4qkIzrHaFOQQ6zLIqrBuiP9QmytfVIbM/OYZiS7VJL8gG/MlQEJ6YVVvR2i a+J7Iz90nTDsetkSGvegZSAS/RE6MjasDC76S4rwKS2XBduWfMAJzMG8mG8bJtIyZZTv5j9A QS/b8S0eJgeXNI1KLi5rcRBO051Nkg1Rv6ISeCBQzCkBR8a3gjKI8mg6GfyK2pcc0fk/rXgX xTsta/GCs9w9exx6dxtOx2iK5B/J1DnVKQ8cMDprn+TCWzAbpZufFf9vUJI1AwnwUVo3Co3D Vwpi/Q+mNmPVHn08exk
- Ironport-hdrordr: A9a23:1vTSCqBgG9dDNyLlHekz55DYdb4zR+YMi2TDtnoBMyC9F/bz+v xG885rsSMc5AxhP03Jd7i7Sd29qV21z+8B3WBTB8bSYOHe0FHYXr2KlLGStAEIeBeOjdK0YM xbAtZD4aPLfCFHZJ3BkXaF+r8bqbHtgcKVbIHlvgtQpC5RBJ2IhD0JcjpzfHcGIjWvxPICZf mhDwl8yQZIu056UiwKbUN1LNQra+erqHoXCiR2eiLPITPv/FaVwY+/KQGR2lM1Uj9Ew7sutU jD1yLj4Lm72svLuiPh6w==
- Ironport-sdr: ObtRWwJG8OX1Xk0LEqQSdnZPQl5emKTIwQhk36UAV3S0A5MNye6zq/Y4vg7w3bX34DPtETOMHV XCo8+cgGuJbga7aDjjIlX4qLmxcNFSO8lRydswCOdu1s4XBOUytIXudDbzHnHy3WmDx6DXuIlg LbJxzAYY5dqB1feE91UYPK8kIqRRRsKn1zAT+obO9pvqWg944hdvWzUMjrZ1mdT/VQM98JON8r 3Ofeex5wj6PNpsEQbGKpNbOVn0jR89tlIQU25RhGbdTMeFO/uit1sgjZIZsp674WlDzYja99dF aMdY+Dt+Wto35kDmhuPwUv7p
Hello. Suppose we have a spec that allows A, B and C actions.Next == A \/ B \/ C
All are always enabled but we want for C to be executed at some point in all behaviors. It is my understanding that the Spec should be something like
Spec == Init /\ [][Next]_vars /\ WF_vars(Next) /\ WF_vars(C)
The question is, how could we limit the number of possible behaviors that is processed?
A level based state constraint would work, but I don't think we get a guarantee that C will execute if we "cut" the behavior by level. We basically need to limit the number, of A, B behaviors until the first C... It this possible?
--
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/db84cfb8-a73a-4c53-b4ac-58be20addc1dn%40googlegroups.com.