[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Simple Question - Safety and Liveness
- From: Victor Clayton Barnett <vcbarnett93@xxxxxxxxx>
- Date: Wed, 13 Jul 2022 07:40:11 -0700 (PDT)
- Ironport-data: A9a23:e9ceO6MXdfpC2kLvrR0/ksFynXyQoLVcMsEvi/4bfWQNrUpz1TEEn DBKUWvXb6mCMTP8LtglYYq1/UIF7MPWyIMyTnM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8kk/vgqoPUUIYoAAgoLeNfYHpn2EgLd9IR2NYy24DmWljV4 7senuWGULOb824sWo4rw/nbwP9flKyaVOQw4zTSzdgS1LPvvyF94KA3fcldHFOkKmVgJdNWc s6YpF2PEsw1yD92Yj+tuu6TnkTn2dc+NyDW4pZdc/DKbhSvOkXe345jXMfwZ3u7hB3QhMFO+ osdkqCValo4YbX9yKc/fBlhRnQW0a1uoNcrIFC6uM2XilTaKj7imqU+Sk4xOoIc96B8BmQmG f4wcmhcKEDewbvomPTiGrkEascLdKEHOKsDvnh4ySzCTvwgSrrocfuV1Plp5wYcvOpyM83uQ O4wTBVWQT7/QixrAG4/B5U5k+OliWP4biVD7lmSoMLb5kCPkVEpj+W8YLI5fPSwBuhfhEDfq 1v93HbBGw8DNPCw0jiapyfEaujnxHunAur+DoaQ+v9xi0CI3UQPDBRQUECh5Pi/kE+3HdNZM U0dvCQ0xZXe72SuR9j5GgSk+TuK505MHdVXFOI+5UeGza+8Dxul6nYsFyVQV+545OgKYB93x wCRroOqJxNviejAIZ6CzYu8oTS3MCkTCGYNYy4YUAcIi+UPRqlj3nojqf4zQMaIYs3J9SLYm G/V8XBv71kHpYtaiPXhpAGvbyeE/8CRFmYIChPrsnVJBz6Viaagbo2srEHHtLNOddbJCFaGu 3cAlo6V6+Vm4XCxeM6lH7ll8FKBvazt3NjgbbhHQ8lJG9OFpyDLQGyoyGsiTHqFy+5dEdMTX GfduBlK+LhYN2awYKl8buqZUpp3kva9TYq+B66IMbKih6SdkifXrEmCgmbAjwjQfLQEzMnTx L/ALJnwVydCYUiZ5GPuF79MuVPU+szO7TqLGcqTI+WP3r2Za3qYIYrpw3PfBt3VGJis8VW92 48HaaOikkwDOMWjPHW/2dNNfDgicChqbbir+pA/XrPScmJORjt9Y9ePmulJU9I+z8xoehLgo hlRrGcFkwSv7ZAGQC3RAk1ehETHBMcj8C9mbXxxZj5FGRELOO6S0UvWTLNvFZFPyQCp5acco yAtd5rSD/JRZC7A/jhBP5DxoJY7KkakggWBOyeqej8iZ4UmTAvMo4e2cgzq/SgILyy2qcpv8 +b7j1iEH8UOF1Z4EcLbSPOz1Fft73ITr+R/AhnTKd5JdUSwrYVncnSjjvI+L8wWBw/Ewz+Wi 1SfDRsC9LvCpoY09J/CgqXd99WlFO53H0x7GWjH7ObuZXOKoDb7mYIZCbSGZzHQUm/w6Z6OX +QNwqGuKuADkXZLr5F4TORmwKc40N3l+O1XwwFiK3PUNgj5B75lJE6G6slBrKh6wLFU5FmtU UWV99gGYLiENZq+Ql4cLQYodN6OzfUFhj7W4ahnKUn2/nYprrWAVkpWMhaWjzFFN/1+N4Z8m bUtv8sf6gqejBs2M4fW1XsNrDvScXFQAb86spw6AZPwjlZ5wF91Z5GBWDT954uCaokRP0Qnf m2Uia7Fi+gOz0bOaSBvR33E3O4YnIhX/R4TnA9EKFOOld7IwPQw2UQJozgwSw1UyDRB0v5ya jc3bRwrff3W8mc6ntVHUkCtBxpFWE+T9Hv3xgZbj2beVUSpCjHAITxvPeeW4H0f6H9WejQHr riUxHy7AWTvdcD1wixgVklipPjuQsZ26xXZ3cWuGc2KEtphPmq03vLwNTVR8kWkHMUqmUfcr vNr9utYZqr8OiodrLc8FpGBk78XTUncdmBFRPhg+oIPHH3dKWHpgmHVdB7ud5MfPeHO/G+5F 9dqepBFWSO42XvctTscH6MNf+J5kfJ1ttMOdqm3dDwGr6eHtWgu953K8TXmnykkRNJhlct7I YTUMD2YFXGIwmdQknfJsdIDIXeyetIeZQfx0e3pov8FEYkP7LNlfU0oiOfmunyUNE5+40vRs lqTN+nZyOttzYkqlIzpS/0RCwKxINL1deKJ7AHj7IgUPI2XaZ/D51EPt13qHwVKJr9NCd55o rKA7Yzs10TfsbdqDm3UlvFtzUWSCRlegQaWDi72EJWetS6LWcup+gdavm7hecwPn9Ra6c2qA QC/baNcsDLTt8h1nBVoh+p2Sn7xyJgbqo/voiSyq/mDEB8AyReBJ9SinZMsRX8ObTcGYvUSF Set08tDJblkQEBkCxgDCPVrDIV/PUf4H6AhcrUdcNVe4naA2ju/h1cpqfbsBfwnxJVJ/AYWL K8pniTDSSk=
- Ironport-hdrordr: A9a23:M4Ftma+uHv2urwdIhoFuk+BHI+orL9Y04lQ7vn2ZKCYlCPBw8v rF8cjzuiWE7Ar5NEtQ/uxp1sG7MAfhHbAc2/hlAV7gZniWhIOQRLsSn7cKugeQbBEWldQtrp uJxsNFeaPN5CZB/L/HCVKDYqkdKbC8mcjC9IXjJhFWPH1Xgo5bgDuRYTzranGeKjM2Y6bQ1f Knl6l6TvmbF0j/rP7WOpG0NNKz1OEjWKiGXfb3bCRXlTVmRAnJmdvHOind5A4XV3dkwLsp82 TJ1yz/oou5te2joyWsp1Pu0w==
- Ironport-sdr: MfvxMwoitXAEh4nEOkfXSteicmUkf9L1trbkdv+6ULiqHxbP8aqtT7h+uo8VDC58ZUq0lVVhxQ TH6zZivA3ao0i4Gvl/rsH3+hIJnAEoqiRN3ScjlAIbhdxrA7SXahAncpB+84ZWpc/RAeHEW4ey 2CCyw3DQoIM7Z6vwiFbUbjprO+hmbvbDsYwAzMDl6HE5vzIeSD+73Vwlh0NP4J2CMUr+mMFvvE Pm0/e/UN8dA7SD7aao9oTf1tv90tD7TJ/f7JeNzBjQmHqYS4+v8xCVBBjSPz4VNMfqkyPbQ0zP NbvucpZJV0qoqfg3SKNmC2dV
Hi, I am trying to learn TLA+ as a Computer Engineering undergrad. I am reading the safety and liveness document from the TLA+ website and am trying to understand the definition of:
<<A>>_v = A /\ (v' \= v)
and when it is enabled. When I first read the definition, it seems this would be ENABLED in a behaviour specified by a formula S when there is a step allowed by S that satisfies:
A /\ (v' \= v).
But then this example is provided:
However, WF_v(A) and SF_v(A) need not be fairness properties. For example, let S equal (x=0) /\ [][x’=x+1]_x,
let A equal x’=x+2
and let v equal x.
An <<x’=x+2>>_x step is possible in any reachable state of S , but no such step satisfies x’=x+1. (A reachable state of S is one that occurs in some behavior that satisfies S .) Hence, no finite sequence of states satisfying S can be extended to satisfy S as well as WF_v(A) or SF_v(A).
So in this case, he's saying that <<x’=x+2>>_x is enabled in any state of a behavior satisfying S because a <<x’=x+2>>_x step is 'possible' in any state of S, but it is not a fairness property essentially because it's not actually allowed within the confines of S. What does possible mean in this case?
Thank you,
Victor
--
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/befc81a6-d74d-4c08-ae5d-2fc6a18d53cbn%40googlegroups.com.