Re: [tlaplus] Error with CommunityModules (kSubset)

[Alfranio Correia <alfranio@xxxxxxxxxxx>]

Hi Markus,

> On 26 Apr 2021, at 21:04, Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:
> 
> 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 ?


Sure.

https://github.com/tlaplus/tlaplus/issues/611#issuecomment-827447532


Cheers.

> 
> 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.

-- 
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/PA4PR03MB731263625BFB71BD6DE5576BDF419%40PA4PR03MB7312.eurprd03.prod.outlook.com.