Re: [tlaplus] Checking matrix multiplication correctness

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Unfortunately, the latest version of the CommunityModules is only compatible with the most recent version of TLC.  You will have to download a nightly build of the Toolbox from https://nightly.tlapl.us/products/

Markus

> On Jan 9, 2024, at 5:28 PM, christin...@xxxxxxxxx <christina.a.burge@xxxxxxxxx> wrote:
> 
> Thanks Andrew! I've added the most recent version of the community modules to my TLA+ Toolbox (and I'm using v 1.7.1 of the toolbox), and I get the error:
> 
> 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
> 
> What am I doing wrong?


-- 
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/30D2B8D1-41AF-4FCF-86C3-4B95D9207F98%40lemmster.de.