Open
Description
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
Metadata
Metadata
Assignees
Labels
No labels
Activity