Make meaning of AcquirableSessionTokens clearer #6
Conversation
simple-model/CosmosDB.tla
Outdated
| \* The "not a session token" session token. | ||
| \* The "not a session token" session token. It precedes all session tokens, | ||
| \* and should be used when no session token is known / available. | ||
| \* It is not a valid session token itself, but is usually compatible with them. |
There was a problem hiding this comment.
"usually"? Perhaps add, under what condition it is incompatible?
There was a problem hiding this comment.
I believe always, but I was being vague as a reflex because there may be some edge case (which would be a bug) where that isn't true. I'll just delete the word.
simple-model/CosmosDB.tla
Outdated
| \* updating a session token using this operator and the ones defined near it. | ||
| \* Assuming session-consistent reads and writes, | ||
| \* this operator describes the set of all session tokens that could be | ||
| \* acquired during the current action. |
There was a problem hiding this comment.
AcquirableSessionTokens is a state-level formula? Should "during the current action" be replaced with "in the current state"? Nitpicking: AcquirableSessionTokens also describes the set of all session independently of session-consistent reads and writes.
There was a problem hiding this comment.
Makes sense I think - I edited that a little bit to account for both things as I understand them.
|
@fhackett Thanks! |
Based on some discussion with @lemmy, this commit makes the meaning of
AcquirableSessionTokensclearer, since it was previously not well integrated with the rest of the spec.As a result two new properties check that the definition works as intended, and some changes and comments document a surprising behavior that came up.