Java overflow when using RandomSubset to check inductive invariance

[Willy Schultz]

I am using the RandomSubset operator of the Randomization module to check inductive invariance as described in [1], but I am running into issues when my set of type correct states gets, apparently, too big for TLC. Here is the TLC error I encounter:

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 \in 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

[Willy Schultz]

Github issue filed: https://github.com/tlaplus/tlaplus/issues/503