[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Re: Is it possible to catch TLC exceptions in TLA+?
On 19.07.20 08:48, Leslie Lamport wrote:
> It is possible to get TLC to override an operator's definition with Java
> code. To override definitions in a module name M, you have to create a
> Java class named M. For example, TLC does addition by overriding the
> definition of + in the Naturals module. Looking at the Java classes
> that implement the standard modules should indicate how you can write
> the necessary Java code to implement Catch. I don't remember where one
> puts the Java class file so TLC will do the overriding.
AssertError [1,2] of the CommunityModules  might be another useful
example. However, please don't take TLC's exceptions or their types as API.
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/2a8546b0-ce43-dcf6-1602-0cb61e270f5c%40lemmster.de.