moving typeOk

microsoft · Sep 2, 2024 · 6dbe828 · 6dbe828
1 parent 1d131f6
commit 6dbe828
Showing 1 changed file with 3 additions and 4 deletions.
diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
@@ -10,6 +10,9 @@ CONSTANT Servers, Terms, MaxLogLength, StartTerm
 \* Each log is append-only and the logs will never diverge.
 VARIABLE CLogs
 
+TypeOK ==
+    /\ CLogs \in [Servers -> 
+        UNION {[1..l -> Terms] : l \in 0..MaxLogLength}]
 
 InitialLogs == {
     <<>>,
@@ -43,10 +46,6 @@ Next ==
 
 AbsSpec == Init /\ [][Next]_CLogs
 
-TypeOK ==
-    /\ CLogs \in [Servers -> 
-        UNION {[1..l -> Terms] : l \in 0..MaxLogLength}]
-
 AppendOnlyProp ==
     [][\A i \in Servers : IsPrefix(CLogs[i], CLogs'[i])]_CLogs