Make meaning of AcquirableSessionTokens clearer (#6)

* Make meaning of AcquirableSessionTokens clearer
* Improve phrasing of CosmosDB.tla comments

simple-model/CosmosDB.tla

@@ -77,7 +77,10 @@ SessionTokens == [
     epoch: Epochs
 ]
 
-\* 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 compatible with them.
+\*
 \* It is not a member of SessionTokens because it has an epoch of 0,
 \* which is special-cased such that it is valid at all epochs.
 \* A read or write operation can be given this token, and that
@@ -194,13 +197,18 @@ TypesOK ==
     /\ epoch \in Epochs
     /\ WriteConsistencyLevel \in ConsistencyLevels
 
-\* This operator can be used to generate a
-\* fresh session token. Combined with session-consistent reads and writes,
-\* the expectation is that one could model a client holding and progressively
-\* 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 state, independent of session-consistent
+\* reads and writes.
+\*
+\* Note that the range of possible checkpoints is very broad: if the newest
+\* write to a key is very old, the current spec will consider the returned
+\* token's checkpoint to point to that oldest index, even if 
+\* the checkpoint is older than readIndex.
 AcquirableSessionTokens == [
     epoch: {epoch},
-    checkpoint: readIndex..Len(log)
+    checkpoint: 0..(Len(log) + 1) \* +1 to account for incomplete writes
 ]
 
 \* Whether the database's current state accepts writes.

simple-model/CosmosDBProps.tla

@@ -433,6 +433,19 @@ SessionTokenWhenValid ==
             /\ token.epoch = epoch \/ token = NoSessionToken
             => SessionConsistencyRead(token, key) # {}
 
+SessionTokenAlwaysAcquirableRead ==
+    ReadConsistencyOK(SessionConsistency)
+    =>
+    \A key \in Keys :
+        { UpdateTokenFromRead(NoSessionToken, read)
+          : read \in SessionConsistencyRead(NoSessionToken, key) }
+        \subseteq AcquirableSessionTokens
+
+SessionTokenAlwaysAcquirableWrite ==
+    WriteConsistencyLevel = SessionConsistency
+    =>
+    WriteInitToken \in AcquirableSessionTokens
+
 \* ConsistentPrefix
 \* https://docs.microsoft.com/en-us/azure/cosmos-db/consistency-levels#consistent-prefix-consistency
 \* Note: consistent prefix does not seem to be observable

simple-model/MCCosmosDBProps.cfg

@@ -35,6 +35,9 @@ INVARIANT
     BoundedStalenessReadsFollowReadIndex
     BoundedStalenessIsBounded
 
+    SessionTokenAlwaysAcquirableRead
+    SessionTokenAlwaysAcquirableWrite
+
     \* very slow:
     SessionConsistencyReadsMonotonicPerTokenSequence
     SessionConsistencyReadsFollowReadIndex

simple-model/MCCosmosDBProps.tla

@@ -8,7 +8,7 @@ CheckpointsImpl == LogIndicesImpl \cup {0}
 EpochsImpl == 1..3
 
 SpecificStateSpace ==
-    /\ Len(log) < Max(LogIndicesImpl)
+    /\ Len(log) < (Max(LogIndicesImpl) - 1)
     /\ epoch < Max(EpochsImpl)
 
 StalenessBoundImpl == 2