Re: [tlaplus] Re: Is it possible to catch TLC exceptions in TLA+?

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

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.

Markus

[1]
https://github.com/tlaplus/CommunityModules/blob/dfc75a91a0cb72bbc16a5295f8264d098d364550/modules/TLCExt.tla#L10-L25
[2]
https://github.com/tlaplus/CommunityModules/blob/dfc75a91a0cb72bbc16a5295f8264d098d364550/modules/tlc2/overrides/TLCExt.java#L59-L76
[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.