[tlaplus] Java overflow when using RandomSubset to check inductive invariance

Attempted to apply the operator overridden by the Java method

public static tlc2.value.impl.Value tlc2.module.Randomization.RandomSubset(tlc2.value.impl.Value,tlc2.value.impl.Value),

but it produced the following error:

Overflow when computing the number of elements in:

SUBSET [configOld: {{}, {n1}, {n2}, {n3}, {n1, n2}, {n1, n3}, {n2, n3}, {n1, n2, n3}}, configOldVersion: 0..2, configOldTerm: 0..2, configNew: {{}, {n1}, {n2}, {n3}, {n1, n2}, {n1, n3}, {n2, n3}, {n1, n2, n3}}, configNewVersion: 0..2, configNewTerm: 0..2]

Here are the relevant definitions from my spec:

SeqOf(set, n) == UNION {[1..m -> set] : m \in 0..n}

BoundedSeq(S, n) == SeqOf(S, n)

ReconfigsType == SUBSET [ configOld : SUBSET Server,

configOldVersion : Nat,

configOldTerm : Nat,

configNew : SUBSET Server,

configNewVersion : Nat,

configNewTerm : Nat]

TypeOKRandom ==

/\ currentTerm \in RandomSubset(4, [Server -> Nat])

/\ state \in RandomSubset(4, [Server -> {Secondary, Primary}])

/\ log \in RandomSubset(4, [Server -> Seq([term : Nat])])

/\ config \in RandomSubset(4, [Server -> SUBSET Server])

/\ configVersion \in RandomSubset(4, [Server -> Nat])

/\ configTerm \in RandomSubset(4, [Server -> Nat])

/\ immediatelyCommitted = {}

/\ elections = {}

/\ reconfigs = RandomSubset(3, ReconfigsType)

IInit == TypeOKRandom /\ IndInv

And I have the following model values and overrides:

Server <- {n1,n2,n3}

MaxLogLen <- 0

Nat <- 0..2

Seq(S) <- BoundedSeq(S, MaxLogLen)

IInit is the initial state predicate defined for TLC to check. From the stack trace produced I can confirm the error is occurring while evaluating the initial state predicate. From a quick glance at this assertion, it seems like 32 bits may be too small for that size value when the set of type correct states gets very big.

[1] https://lamport.azurewebsites.net/tla/inductive-invariant.pdf