I have another question though. I started increasing the set and got the following error:
Attempted to apply the operator overridden by the Java method
public static tlc2.value.impl.IntValue tlc2.module.FiniteSets.Cardinality(tlc2.value.impl.Value),
but it produced the following error:
k=4 and n=112
The error occurred when TLC was evaluating the nested
expressions at the following positions:
….
I omitted the call stack but if I did not misread neither the message nor the call stack,
it is complaining about the Cardinatily(KSet). Is this expected?
Init ==
/\ KSet = kSubset(2, BigSet)
/\ Print(Cardinality(KSet), TRUE)
If I remove the TLC Print, it fails with a similar message but it does not show a stack trace:
k=4 and n=112
While working on the initial state:
/\ KSet = {{1,2}, … }
The error occurred when TLC was evaluating the nested
expressions at the following positions:
The error call stack is empty.
Is this expected?