[tlaplus] Error with CommunityModules (kSubset)

[Alfranio Correia <alfranio@xxxxxxxxxxx>]

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

…

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