Unfolding recursive operators

[konnov]

Unfold definitions of recursive operators by using an upper bound on the number of calls.

Consider the following TLA+ code:

RECURSIVE Sum(_)
Sum(S) ==
  IF S = {}
  THEN 0
  ELSE LET n = CHOOSE x \in S: TRUE IN
    n + Sum(S \ {n})

\* an upper bound on the number of unfoldings
Sum_unfold_count == 3

\* a failure expression to be used when the upper bound has been exceeded
Sum_unfold_fail ==
  CHOOSE x \in {}: TRUE \* the expression should be type-compatible

Test == Sum({3, 4})

As a result of rewriting, Test should be rewritten as:

Test == Sum3({3, 4})

Sum3(S3) ==
  IF S3 = {}
  THEN 0
  ELSE LET n3 = CHOOSE x3 \in S3: TRUE IN
    n3 + Sum2(S3 \in {n3})

Sum2(S2) ==
  IF S2 = {}
  THEN 0
  ELSE LET n2 = CHOOSE x2 \in S2: TRUE IN
    n2 + Sum1(S2 \in {n2})

Sum1(S1) ==
  IF S1 = {}
  THEN 0
  ELSE LET n1 = CHOOSE x1 \in S1: TRUE IN
    n1 + Sum0(S1 \in {n1})

Sum0(S0) == CHOOSE x \in {}: TRUE

[konnov]

The approach we take is documented in the manual. The implementation is quite unstable yet. It will be fixed in several days.

[Kukovec]

Addressed in #127.