The ReadConsistencyOK operator is inconsistent with the comments. The…

… comments do not explain the relationship between read and write consistencies, but the operator defines specific constraints based on the write consistency level.
Azure · Dec 5, 2023 · c926399 · c926399
1 parent 0e25985
commit c926399
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/simple-model/CosmosDB.tla b/simple-model/CosmosDB.tla
@@ -248,9 +248,12 @@ WriteCanSucceed(token) ==
         /\ token.epoch = epoch
         /\ token.checkpoint <= commitIndex)
 
-\* This predicate indicates whether a read consistency if
+\* This predicate indicates whether a read consistency is
 \* valid, given a particular configured write consistency.
-\* 
+\* A read consistency is valid if it is not stronger than
+\* the configured write consistency.  In other words, the
+\* write consistency level defines the upper bound for the
+\* strongest read consistency level that can be used.
 ReadConsistencyOK(level) ==
     CASE WriteConsistencyLevel = StrongConsistency ->
             TRUE