On Saturday, July 18, 2020 at 10:37:42 AM UTC-7, Anton Trunov wrote:
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)
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!