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

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

On Sunday, September 13, 2020 at 10:55:55 PM UTC-4, Willy Schultz wrote:

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