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

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

On Saturday, July 18, 2020 at 10:37:42 AM UTC-7, Anton Trunov wrote:

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