[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Is it possible to catch TLC exceptions in TLA+?
Dear Leslie and Markus,
Thank you for all the pointers! This has been very helpful.
> 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  might be another useful
> example. However, please don't take TLC's exceptions or their types as API.
>  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.