diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla index b0855392f03d..3692a897bbce 100644 --- 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)