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

Re: [tlaplus] Error with CommunityModules (kSubset)



On 26.04.21 12:07, Alfranio Correia wrote:
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?


Can you please add your findings to https://github.com/tlaplus/tlaplus/issues/611 ?

Thanks,
Markus

--
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/ed236730-bbe1-862b-4e15-59d3bbce9ea8%40lemmster.de.