Refactor (simplify) TypeOK to use Sequences!Seq operator

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
microsoft · Sep 12, 2024 · cb9542e · cb9542e
1 parent b08724a
commit cb9542e
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
@@ -11,8 +11,7 @@ CONSTANT Servers, Terms, MaxLogLength
 VARIABLE cLogs
 
 TypeOK ==
-    /\ cLogs \in [Servers -> 
-        UNION {[1..l -> Terms] : l \in 0..MaxLogLength}]
+    cLogs \in [Servers -> Seq(Terms)]
 
 StartTerm == Min(Terms)