Re: [tlaplus] Error with CommunityModules (kSubset)

[Alfranio Correia <alfranio@xxxxxxxxxxx>]

Hi Markus,

> On 26 Apr 2021, at 18:01, Alfranio Correia <alfranio@xxxxxxxxxxx> wrote:
> 
> Hi Markus,
> 
> Thank you for the quick reply. I will try that.
> 


It worked. Thank you.

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?

Cheers. 


> Cheers.
> 
>> On 26 Apr 2021, at 17:51, Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:
>> 
>> 
>> On 26.04.21 08:36, Alfranio Correia wrote:
>>> I am getting the following error when I use the kSubset imported from the community modules:
>>> kSubset(2, {1, 2, 3}) in “Evaluate Constant Expression”
>>> TLC threw an unexpected exception.
>>> This was probably caused by an error in the spec or model.
>>> See the User Output or TLC Console for clues to what happened.
>>> The exception was a java.lang.NoClassDefFoundError
>>> : tlc2/value/impl/KSubsetValue
>>> I followed the instructions available athttps://www.youtube.com/watch?v=w9t6JnmxV2E  to install the extensions.
>>> Thank you in advance for any suggestion on how to fix the problem.
>> 
>> 
>> Hi Alfranio,
>> 
>> the kSubset Java module override specifically requires a recent TLC nightly build.  The most up-to-date Toolbox nightly [1] comes with a compatible version of the CommunityModules ("CommunityModules-deps.jar" is part of the Toolbox zip file).
>> 
>> Note that you have to update the TLA+ library path to point to the Toolbox's "CommunityModules-deps.jar".
>> 
>> Markus
>> 
>> [1] http://nightly.tlapl.us/products/
>> 
> 
> 
> 
> 
>> -- 
>> 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/5f25dcab-73b6-42a6-7f48-4642541dce7f%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/PA4PR03MB731259A81BEB868E4A29778CDF429%40PA4PR03MB7312.eurprd03.prod.outlook.com.