[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8dfe181c-c7ea-4302-a5a2-2eeb31559bbbo%40googlegroups.com.