Error with CommunityModules (kSubset)

[Alfranio Correia]

Hi all,

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 at https://www.youtube.com/watch?v=w9t6JnmxV2E to install the extensions.
Thank you in advance for any suggestion on how to fix the problem.

Cheers.

This is my configuratiion:


*** System properties:
applicationXMI=org.eclipse.ui.workbench/LegacyIDE.e4xmi
ds.delayed.keepInstances=true
ds.delayed.keepInstances.default=true
eclipse.application=org.lamport.tla.toolbox.application
eclipse.buildId=1.7.1
eclipse.commands=-os
macosx
-ws
cocoa
-arch
x86_64
-showsplash
-launcher
/Applications/TLA+ Toolbox.app/Contents/MacOS/toolbox
-name
TLA+ Toolbox
--launcher.library
/Applications/TLA+ Toolbox.app/Contents/MacOS//../Eclipse/plugins/org.eclipse.equinox.launcher.cocoa.macosx.x86_64_1.1.1200.v20200508-1552/eclipse_1902.so
-startup
/Applications/TLA+ Toolbox.app/Contents/MacOS//../Eclipse/plugins/org.eclipse.equinox.launcher_1.5.700.v20200207-2156.jar
--launcher.overrideVmargs
-keyring
/Users/alcorrei/.eclipse_keyring
-vm
/Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.openjdk.macosx.x86_64_14.0.1.7/Contents/Home/bin/../lib/server/libjvm.dylib
eclipse.home.location=file:/Applications/TLA+ Toolbox.app/Contents/Eclipse/
eclipse.launcher=/Applications/TLA+ Toolbox.app/Contents/MacOS/toolbox
eclipse.launcher.name=TLA+ Toolbox
eclipse.p2.data.area=@config.dir/../p2/
eclipse.p2.profile=DefaultProfile
eclipse.product=org.lamport.tla.toolbox.product.standalone.product
eclipse.startTime=1619427088118
eclipse.stateSaveDelayInterval=30000
eclipse.vm=/Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.openjdk.macosx.x86_64_14.0.1.7/Contents/Home/bin/../lib/server/libjvm.dylib
eclipse.vmargs=-XX:+IgnoreUnrecognizedVMOptions
-Xmx1024m
-XX:+UseParallelGC
-Dorg.eclipse.equinox.http.jetty.http.port=10996
-Dosgi.splashPath=platform:/base/
-Dosgi.requiredJavaVersion=11.0
-Dosgi.instance.area.default=@user.home/.tlaplus/
-Dosgi.clean=true
-XstartOnFirstThread
-Dorg.eclipse.swt.internal.carbon.smallFonts
-Djava.class.path=/Applications/TLA+ Toolbox.app/Contents/MacOS//../Eclipse/plugins/org.eclipse.equinox.launcher_1.5.700.v20200207-2156.jar
equinox.init.uuid=true
file.encoding=UTF-8
file.separator=/
ftp.nonProxyHosts=local|*.local|169.254/16|*.169.254/16
gosh.args=--nointeractive
java.class.path=/Applications/TLA+ Toolbox.app/Contents/MacOS//../Eclipse/plugins/org.eclipse.equinox.launcher_1.5.700.v20200207-2156.jar
java.class.version=58.0
java.home=/Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.openjdk.macosx.x86_64_14.0.1.7/Contents/Home
java.io.tmpdir=/var/folders/hm/b2txfg_s03g9_pjwmr45k9y40000gn/T/
java.library.path=/Users/alcorrei/Library/Java/Extensions:/Library/Java/Extensions:/Network/Library/Java/Extensions:/System/Library/Java/Extensions:/usr/lib/java:.
java.runtime.name=OpenJDK Runtime Environment
java.runtime.version=14.0.1+7
java.specification.name=Java Platform API Specification
java.specification.vendor=Oracle Corporation
java.specification.version=14
java.vendor=AdoptOpenJDK
java.vendor.url=https://adoptopenjdk.net/
java.vendor.url.bug=https://github.com/AdoptOpenJDK/openjdk-support/issues
java.vendor.version=AdoptOpenJDK
java.version=14.0.1
java.version.date=2020-04-14
java.vm.compressedOopsMode=32-bit
java.vm.info=mixed mode, sharing
java.vm.name=OpenJDK 64-Bit Server VM
java.vm.specification.name=Java Virtual Machine Specification
java.vm.specification.vendor=Oracle Corporation
java.vm.specification.version=14
java.vm.vendor=AdoptOpenJDK
java.vm.version=14.0.1+7

…

org.osgi.framework.executionenvironment=OSGi/Minimum-1.0, OSGi/Minimum-1.1, OSGi/Minimum-1.2, JavaSE/compact1-1.8, JavaSE/compact2-1.8, JavaSE/compact3-1.8, JRE-1.1, J2SE-1.2, J2SE-1.3, J2SE-1.4, J2SE-1.5, JavaSE-1.6, JavaSE-1.7, JavaSE-1.8, JavaSE-9, JavaSE-10, JavaSE-11, JavaSE-12, JavaSE-13, JavaSE-14
org.osgi.framework.language=en
org.osgi.framework.os.name=MacOSX
org.osgi.framework.os.version=10.16.0
org.osgi.framework.processor=x86-64

…

os.arch=x86_64
os.name=Mac OS X
os.version=10.16

…

[Markus Kuppe]

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/

[Alfranio Correia]

Hi Markus,

Thank you for the quick reply. I will try that.

Cheers.

> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5f25dcab-73b6-42a6-7f48-4642541dce7f%40lemmster.de.

[Alfranio Correia]

Hi Markus,

> On 26 Apr 2021, at 18:01, Alfranio Correia <alfr...@hotmail.com> 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.

[Markus Kuppe]

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

[Alfranio Correia]

Hi Markus,

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+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ed236730-bbe1-862b-4e15-59d3bbce9ea8%40lemmster.de.