[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Checking matrix multiplication correctness

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/


> 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.