[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] About Enabled semantics
- From: Huailin <huailin@xxxxxxxxx>
- Date: Fri, 9 Jul 2021 16:42:56 -0700 (PDT)
- Ironport-hdrordr: A9a23:nc9bHKN8ZUCw68BcTxn155DYdb4zR+YMi2TDiHoddfUFSKalfp6V98jzjSWE7wr5K0tQ/+xoWZPwNE80kKQY3WB/B8bGYOCLggqVxeJZnP/fKl/baknDH4dmvM8OHZSWY+eAbmSS+PyKgjVQfexB/PC3tISTwcvOxXZkSg9nL4t66R1iNwqdGkpqACFbGJsQDvOnl7x6jgvlXU5SQtWwB3EDUeSGjcbMjojabRkPAANiwBWSjAmv9KXxH3Gjr14junJ0sPwfGSWsqX2w2kyQiYD39vbu7R6e031ioqqq9jMabPb8xfT9ZA+cxDpAL74RIoFq9ApF2N1Hrmxa5+Ukji1QQfib0UmhD12dsF/owU3twTwu43jtxRuRhmbiu9XwQHY/B9BajYxUfxPF4w541esMo55jziacrd5aHBnAlCPy65zBUAxrjFO9pT4nnfQIh3JSXIMCYPtarJAZ/klSDJAcdRiKmLzOlIJVfb3hDdNtACGnhlzizxRSKYaXLw4O9z+9Mzc/Uuz86UksoExE
I got a quick question about the semantics of Enabled of TLA+. Thanks for the clarification in advance.
As we know, the Enabled Predication is defined as:
s[Enabled A] = Exist t \Exist St: s[[A]]t.
For the action A, there exists a state t in the state space St, so that action A could be possible to get a chance(may not get the chance, though) to execute.
Then, my question is: When/after Enabled(A) is TRUE, when it could become false, or we say, why/when the state "t" will run away....? so that we can not match the s[[A]]t any more.
Can you give an example? t run away for a vacation, and then, after a while, come back...then Enabled(A) becomes TRUE again.
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/40e686f9-4176-474f-a7a0-77ef7c57b946n%40googlegroups.com.