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.