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

[Anton Trunov <anton.a.trunov@xxxxxxxxx>]

Dear Leslie and Markus,

Thank you for all the pointers! This has been very helpful.

Best,
Anton

> On 19 Jul 2020, at 20:21, Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:
> 
> 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.

-- 
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/EFF96203-1642-4EA9-9E07-B061A0B32078%40gmail.com.