Update TwoPhase animated

will62794 · Apr 12, 2024 · 5ce2d70 · 5ce2d70
1 parent 4ff4d48
commit 5ce2d70
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/specs/TwoPhase_anim.tla b/specs/TwoPhase_anim.tla
@@ -217,19 +217,19 @@ c2 == Circle(20, 10, 3, [fill |-> "red"])
 \* ServerIdDomain == 1..Cardinality(Server)
 RMIdDomain == 1..2
 
-TMElem == Circle(40, 50, 6, [fill |-> IF tmState = "committed" THEN CommitColor ELSE IF tmState = "init" THEN "gray" ELSE AbortColor])
+TMElem == Circle(40, 85, 10, [fill |-> IF tmState = "committed" THEN CommitColor ELSE IF tmState = "init" THEN "gray" ELSE AbortColor])
 RMTextElems == 
     [i \in RMIdDomain |->
         Text(30 * i, 10, RMId[i], ("fill" :> "black" @@ "text-anchor" :> "middle"))
     ]
     \* <<Text(10, 10, "RM1", [fill |-> "black"]), Text(20, 10, "RM2", [fill |-> "black"]), Text(40, 50, "TM", [fill |-> "black"])>>
 TMTextElems == <<
     Text(50, 70, "TM", ("fill" :> "black" @@ "text-anchor" :> "middle")),
-    Text(50, 90, ToString(tmPrepared), ("fill" :> "black" @@ "text-anchor" :> "middle"))
+    Text(50, 110, ToString(tmPrepared), ("fill" :> "black" @@ "text-anchor" :> "middle"))
 >>
 TextElems == RMTextElems \o TMTextElems
 \* RM elements node circles with corresponding colors.
-RMElems == [i \in RMIdDomain |-> Circle(30 * i, 18, 6, 
+RMElems == [i \in RMIdDomain |-> Circle(30 * i, 25, 10, 
         [fill |-> 
             IF rmState[RMId[i]] = "prepared" 
                 THEN "blue"