Re: [tlaplus] Checking matrix multiplication correctness

["christin...@xxxxxxxxx" <christina.a.burge@xxxxxxxxx>]

Thanks! That fixed it :) I have one further (and very silly) question - how do I actually use the functions defined in the community modules, the toolbox doesn't recognise, for example Divides, from the DyadicRadtionals module. I have added an EXTENDS DyadicRationals to my spec, but this hasn't helped. Is it because Divides is "LOCAL"? But then how could you use it at all? I can't seem to find the answer anywhere else!

On Wednesday, January 10, 2024 at 1:36:00 AM UTC Markus Kuppe wrote:

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 <christin...@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/d7b9cde8-9573-4fe8-9bda-36bd9ca32289n%40googlegroups.com.