[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 [3] might be another useful
example.  However, please don't take TLC's exceptions or their types as API.


[3] https://github.com/tlaplus/CommunityModules/

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.