NoClassDefFoundError `: tlc2/value/impl/KSubsetValue` in Toolbox 1.7.1 CommunityModules.jar

[carl-reverb]

I'm unable to run Model checking when I include the CommunityModules.jar file.

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

java --version
openjdk 11.0.13 2021-10-19
OpenJDK Runtime Environment Temurin-11.0.13+8 (build 11.0.13+8)
OpenJDK 64-Bit Server VM Temurin-11.0.13+8 (build 11.0.13+8, mixed mode)

I'm also unclear on whether I should have the CommunityModules.jar, the CommunityModules-deps.jar, or both. Attempting to include any versioned module displays an error: {0} is not a valid library path location

[lemmy]

Unfortunately, this issue will only be fixed with the next Toolbox release. :-( In the meantime, can you copy&paste the operators, assuming you don't care about Java module overrides? If you want the module overrides, it is easiest to switch to a Toolbox nightly build. Lastly, you can grab a CommunityModules release from before I screwed up, assuming it already has what you are after.

Duplicate: https://github.com/tlaplus/CommunityModules/issues/22

[carl-reverb]

Ok, I saw that other issue but I didn't realize from the comments that it was the same as this one. Thank you for explaining. I'll copy the operators I need, I learn something too from doing so.

[melhindi]

I can confirm that the error is gone when using the latest (pre-release) build: https://github.com/tlaplus/tlaplus/releases/tag/v1.8.0#latest-tla-files