Move explicit bound of state-space to TLC's state constraint.

[Refactor]
Azure · Mar 18, 2022 · 502b1d6 · 502b1d6
1 parent 43691aa
commit 502b1d6
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 25 deletions.
diff --git a/.github/MCswscop.tla b/.github/MCswscop.tla
@@ -1,12 +1,12 @@
 ------------------------- MODULE MCswscop -------------------------
 EXTENDS swscop, IOUtils
 
+MaxNumOp ==
+    \A i \in Clients: op[i] < 5
+
 mcNumClients ==
     1
 
-mcMaxNumOp ==
-    5
-
 mcK ==
     2
 
@@ -45,8 +45,9 @@ SPECIFICATION Spec
 \* Add statements after this line.
 CHECK_DEADLOCK 
     FALSE
+CONSTRAINT
+    MaxNumOp
 CONSTANT
-    MaxNumOp <- mcMaxNumOp
     NumClients <- mcNumClients
     Consistency <- mcConsistency
     K <- mcK

diff --git a/.github/MCswscrw.tla b/.github/MCswscrw.tla
@@ -1,12 +1,12 @@
 ------------------------- MODULE MCswscrw -------------------------
 EXTENDS swscrw, IOUtils
 
+MaxNumOp ==
+    \A i \in Clients: op[i] < 5
+
 mcNumClients ==
     1
 
-mcMaxNumOp ==
-    5
-
 mcK ==
     2
 
@@ -45,8 +45,9 @@ SPECIFICATION Spec
 \* Add statements after this line.
 CHECK_DEADLOCK 
     FALSE
+CONSTRAINT
+    MaxNumOp
 CONSTANT
-    MaxNumOp <- mcMaxNumOp
     NumClients <- mcNumClients
     Consistency <- mcConsistency
     K <- mcK

diff --git a/scenario1/swscop.tla b/scenario1/swscop.tla
@@ -1,8 +1,8 @@
 -------------------------- MODULE swscop --------------------------
 EXTENDS Naturals, Integers, Sequences, FiniteSets
-CONSTANT NumClients, MaxNumOp, Consistency, K
+CONSTANT NumClients, Consistency, K
 ASSUME Consistency \in {"Eventual", "Consistent_Prefix", "Session", "Bounded_Staleness", "Strong"}
-ASSUME MaxNumOp<10 /\ NumClients=1
+ASSUME NumClients=1
 Cloud == 0
 Clients == 1..NumClients
 (* --algorithm swscop {
@@ -50,7 +50,7 @@ variables
     variables
         m = <<>>; op=0; chistory = <<0>>; ses=1; 
     {
-     CW: while(op<MaxNumOp) {             
+     CW: while(TRUE) {             
            op:=op+1; 
            send(Cloud, [type |-> "Write", dat |-> op, ses|->ses, orig |-> self]);
      CWA:  receive(m); \* Ack
@@ -145,12 +145,9 @@ cosmosdb(self) == D(self) \/ DW(self) \/ DE(self) \/ DP(self) \/ DS(self)
                      \/ DB(self) \/ DG(self)
 
 CW(self) == /\ pc[self] = "CW"
-            /\ IF op[self]<MaxNumOp
-                  THEN /\ op' = [op EXCEPT ![self] = op[self]+1]
-                       /\ chan' = [chan EXCEPT ![Cloud] = Append(chan[Cloud], ([type |-> "Write", dat |-> op'[self], ses|->ses[self], orig |-> self]))]
-                       /\ pc' = [pc EXCEPT ![self] = "CWA"]
-                  ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
-                       /\ UNCHANGED << chan, op >>
+            /\ op' = [op EXCEPT ![self] = op[self]+1]
+            /\ chan' = [chan EXCEPT ![Cloud] = Append(chan[Cloud], ([type |-> "Write", dat |-> op'[self], ses|->ses[self], orig |-> self]))]
+            /\ pc' = [pc EXCEPT ![self] = "CWA"]
             /\ UNCHANGED << Database, msg, m, chistory, ses >>
 
 CWA(self) == /\ pc[self] = "CWA"

diff --git a/scenario2/swscrw.tla b/scenario2/swscrw.tla
@@ -1,8 +1,8 @@
 -------------------------- MODULE swscrw --------------------------
 EXTENDS Naturals, Integers, Sequences, FiniteSets
-CONSTANT NumClients, MaxNumOp, Consistency, K
+CONSTANT NumClients, Consistency, K
 ASSUME Consistency \in {"Eventual", "Consistent_Prefix", "Session", "Bounded_Staleness", "Strong"}
-ASSUME MaxNumOp<10 /\ NumClients=1
+ASSUME NumClients=1
 Cloud == 0
 Clients == 1..NumClients
 (* --algorithm swscrw {
@@ -50,7 +50,7 @@ variables
     variables
         m = <<>>; op=0; v=0; chistory = <<0>>; ses=1; 
     {
-     CR: while(op<MaxNumOp) {
+     CR: while(TRUE) {
            send(Cloud, [type |-> Consistency, ses|->ses, orig |-> self]); \* read
      CRA:  receive(m);  \* Reply      
            chistory:= Append(chistory,m.dat);
@@ -147,11 +147,8 @@ cosmosdb(self) == D(self) \/ DW(self) \/ DE(self) \/ DP(self) \/ DS(self)
                      \/ DB(self) \/ DG(self)
 
 CR(self) == /\ pc[self] = "CR"
-            /\ IF op[self]<MaxNumOp
-                  THEN /\ chan' = [chan EXCEPT ![Cloud] = Append(chan[Cloud], ([type |-> Consistency, ses|->ses[self], orig |-> self]))]
-                       /\ pc' = [pc EXCEPT ![self] = "CRA"]
-                  ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
-                       /\ chan' = chan
+            /\ chan' = [chan EXCEPT ![Cloud] = Append(chan[Cloud], ([type |-> Consistency, ses|->ses[self], orig |-> self]))]
+            /\ pc' = [pc EXCEPT ![self] = "CRA"]
             /\ UNCHANGED << Database, msg, m, op, v, chistory, ses >>
 
 CRA(self) == /\ pc[self] = "CRA"