Closed Kukovec closed 3 months ago
This PR introduces a TLA-to-TLA translation rule for translating RECURSIVE TLA+ operators into the Apalache-supported fragment, as well as a rule for dealing with mutual-recursion cycles in RECURSIVE TLA+ operator calls.
RECURSIVE
This PR introduces a TLA-to-TLA translation rule for translating
RECURSIVETLA+ operators into the Apalache-supported fragment, as well as a rule for dealing with mutual-recursion cycles inRECURSIVETLA+ operator calls.