Constraint state-space with a state constraint instead of with a "har…

…d-coded" counter in the behavior part of the specification. [Refactor]
Azure · Mar 6, 2022 · 7e22649 · 7e22649
1 parent 15101fc
commit 7e22649
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 26 deletions.
diff --git a/.github/MCcosmos_client.tla b/.github/MCcosmos_client.tla
@@ -32,9 +32,10 @@ mcStrong ==
 --------------------------- CONFIG MCcosmos_client --------------------------
 SPECIFICATION Spec
 \* Add statements after this line.
+CONSTRAINT 
+    MaxNumOp
 CONSTANT
-MaxNumOp = 3
-K = 1
+    K = 1
 CONSTANT
     NumRegions <- mcNumRegions
     NumWriteRegions <- mcNumWriteRegions

diff --git a/general-model/cosmos_client.tla b/general-model/cosmos_client.tla
@@ -24,11 +24,6 @@ CONSTANT NumClientsPerRegion
 
 ASSUME NumClientsPerRegion \in Nat
 
-(***************************************************************************)
-(* MaxNumOp max number of operations from client                           *)
-(***************************************************************************)
-CONSTANT MaxNumOp
-
 (***************************************************************************)
 (* Consistency level                                                       *)
 (* (1) strong (Linearizability)                                            *)
@@ -57,9 +52,9 @@ Clients == Regions \X (1..NumClientsPerRegion)
 Bound ==
     CASE Consistency = "Strong" -> 1
         [] Consistency = "Bounded_staleness" -> K
-        [] Consistency = "Session" -> MaxNumOp
-        [] Consistency = "Consistent_prefix" -> MaxNumOp
-        [] Consistency = "Eventual" -> MaxNumOp
+        [] Consistency = "Session" -> 100 \* effectively infinite.
+        [] Consistency = "Consistent_prefix" -> 100
+        [] Consistency = "Eventual" -> 100
 
 (***************************************************************************)
 (* All possible operations in history                                      *)
@@ -150,12 +145,10 @@ Operations == [type: {"write"}, data: Nat, region: WriteRegions, client: Clients
     (* -------------------------------------------------------------- *)
     fair process (client \in Clients)
     variable session_token = 0;
-    numOp = 0;
     {
         client_actions:
-        while(numOp < MaxNumOp)
+        while(TRUE)
         {
-            numOp := numOp + 1;
             either
             {
                 write:
@@ -193,9 +186,9 @@ RemoveDuplicates(es) == RemDupRec(es, {})
 
 Last(s) == s[Len(s)]
 
-VARIABLES session_token, numOp
+VARIABLE session_token
 
-vars == << History, Data, Database, value, pc, session_token, numOp >>
+vars == << History, Data, Database, value, pc, session_token >>
 
 ProcSet == (Clients) \cup {<<0, 0>>}
 
@@ -206,17 +199,12 @@ Init == (* Global variables *)
         /\ value = 0
         (* Process client *)
         /\ session_token = [self \in Clients |-> 0]
-        /\ numOp = [self \in Clients |-> 0]
         /\ pc = [self \in ProcSet |-> CASE self \in Clients -> "client_actions"
                                         [] self = <<0, 0>> -> "database_action"]
 
 client_actions(self) == /\ pc[self] = "client_actions"
-                        /\ IF numOp[self] < MaxNumOp
-                              THEN /\ numOp' = [numOp EXCEPT ![self] = numOp[self] + 1]
-                                   /\ \/ /\ pc' = [pc EXCEPT ![self] = "write"]
-                                      \/ /\ pc' = [pc EXCEPT ![self] = "read"]
-                              ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
-                                   /\ numOp' = numOp
+                        /\ \/ /\ pc' = [pc EXCEPT ![self] = "write"]
+                           \/ /\ pc' = [pc EXCEPT ![self] = "read"]
                         /\ UNCHANGED << History, Data, Database, value, 
                                         session_token >>
 
@@ -232,7 +220,6 @@ write(self) == /\ pc[self] = "write"
                                                  client |-> self])
                     /\ session_token' = [session_token EXCEPT ![self] = value']
                /\ pc' = [pc EXCEPT ![self] = "client_actions"]
-               /\ numOp' = numOp
 
 read(self) == /\ pc[self] = "read"
               /\ Consistency /= "Session" \/ Data[self[1]] >= session_token[self]
@@ -243,7 +230,7 @@ read(self) == /\ pc[self] = "read"
                                            client |-> self])
               /\ session_token' = [session_token EXCEPT ![self] = Data[self[1]]]
               /\ pc' = [pc EXCEPT ![self] = "client_actions"]
-              /\ UNCHANGED << Data, Database, value, numOp >>
+              /\ UNCHANGED << Data, Database, value >>
 
 client(self) == client_actions(self) \/ write(self) \/ read(self)
 
@@ -256,7 +243,7 @@ database_action == /\ pc[<<0, 0>>] = "database_action"
                                 ELSE /\ TRUE
                                      /\ Data' = Data
                    /\ pc' = [pc EXCEPT ![<<0, 0>>] = "database_action"]
-                   /\ UNCHANGED << History, value, session_token, numOp >>
+                   /\ UNCHANGED << History, value, session_token >>
 
 CosmosDB == database_action
 
@@ -269,7 +256,6 @@ Spec == /\ Init /\ [][Next]_vars
 
 \* END TRANSLATION
 
-
 -----------------------------------------------------------------------------
 
 (* enable these invariants in model checker *)
@@ -348,5 +334,10 @@ Invariant == /\ TypeOK
 
 Liveness == <>[] (\A i, j \in Regions : Database[i] = Database[j])
 
+-----------------------------------------------------------------------------
+(* Constraint the states-space to be finite for model-checking. *)
+MaxNumOp ==
+    Len(History) < 7
+
 =============================================================================
 \* Authored by Cosmos DB