Anton Trunov
unread,Jul 18, 2020, 1:37:42 PM7/18/20Sign in to reply to author
Sign in to forward
You do not have permission to delete messages in this group
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tla...@googlegroups.com
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