Is it possible to catch TLC exceptions in TLA+?

[Anton Trunov]

Dear all,

Is it possible to catch TLC exception in TLA+?

E.g. I would imagine an overridden TLA+ expression “Catch” that could be used as follows:

Catch(DivisionByZero, expr1, expr2)

where
DivisionByZero is a particular kind of exception to handle (assuming there is a standard list of those);
expr1 is the main expression to evaluate;
expr2 is the expression to evaluate in case DivisionByZero is caught
(of course, if expr2 fails and there is no wrapping “Catch” expression then one gets an unexpected TLC exception)

The need for this comes up in a transpiler into TLA+ I’m working on.
Another option would be to model e.g. division as a partial operation and propagate the missing result,
but this would complicate the generated code.

Any suggestions on how this issue can be bypassed otherwise are more than welcome!

Best regards,
Anton Trunov

[Leslie Lamport]

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.

Leslie

[Markus Kuppe]

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/

[Anton Trunov]

Dear Leslie and Markus,

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

Best,
Anton

> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2a8546b0-ce43-dcf6-1602-0cb61e270f5c%40lemmster.de.