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

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

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

-- 
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/BA74CF48-7A38-491D-BEE4-1F53D474476D%40gmail.com.