Programming recursive functions in alloy

Question

I am trying to construct a recursive function in Alloy. According to the grammar displayed on Daniel Jackson's book, this is possible. My function is:

fun auxiliaryToAvoidCyclicRecursion[idTarget:MethodId, m:Method]: Method{
    (m.b.id = idTarget) => {
        m
    } else (m.b.id != idTarget) => {
        (m.b = LiteralValue) => {
           m 
        } else {
           some mRet:Method, c:Class | mRet in c.methods && m.b.id = mRet.id => auxiliaryToAvoidCyclicRecursion[idTarget, mRet]
        }       
    }
}

But the solver claims about the call auxiliaryToAvoidCyclicRecursion[idTarget, mRet] saying that:

"This must be a formula expression.
Instead, it has the following possible type(s):
{this/Method}"

Answer 1

The problem is exactly what the error message says: the return type of your auxiliaryToAvoidCyclicRecursion function is Method, which you are trying to use in a boolean implication, where formula is expected (i.e., something of type Boolean). You'd get the same kind of error in any other statically typed language.

You could rewrite your function as a predicate to work around this problem:

pred auxiliaryToAvoidCyclicRecursion[idTarget:MethodId, m:Method, ans: Method] {
    (m.b.id = idTarget) => {
        ans = m
    } else (m.b.id != idTarget) => {
        (m.b = LiteralValue) => {
           ans = m 
        } else {
           some mRet:Method, c:Class {
             (mRet in c.methods && m.b.id = mRet.id) => 
                auxiliaryToAvoidCyclicRecursion[idTarget, mRet, ans]
           }
        }       
    }
}

This should not give you a compilation error, but to run it make sure you enable recursion (Options -> Recursion Depth). As you will see, the maximum recursion depth is 3, meaning that the Alloy Analyzer can unroll your recursive calls up to 3 times, regardless of the scope of your analysis. When that is not enough, you still have the option to rewrite your model such that the recursive predicate in question is modeled as a relation. Here is a simple example to illustrate that.

Linked list with a recursively defined function for computing the list length:

sig Node {
  next: lone Node
} {
  this !in this.^@next
}

fun len[n: Node]: Int {
  (no n.next) => 1 else plus[1, len[n.next]]
}

// instance found when recursion depth is set to 3
run { some n: Node | len[n] > 3 } for 5 but 4 Int

// can't find an instance because of too few recursion unrollings (3), 
// despite the scope being big enough
run { some n: Node | len[n] > 4 } for 5 but 4 Int

Now the same list where len is modeled as a relation (i.e., a field in Node)

sig Node {
  next: lone Node,
  len: one Int
} {
  this !in this.^@next
  (no this.@next) => this.@len = 1 else this.@len = plus[next.@len, 1]
}

// instance found
run { some n: Node | n.len > 4 } for 5 but 4 Int

Note that the latter approach, which doesn't use recursion (and therefore does not depend on the value of the "recursion depth" configuration option), can be (and typically is) significantly slower than the former.