在合金中编程递归函数 [英] Programming recursive functions in alloy

问题描述

我正在尝试在 Alloy 中构建一个递归函数.根据丹尼尔杰克逊书中显示的语法，这是可能的.我的功能是:

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]
        }       
    }
}

但是求解器声称调用 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}"

推荐答案

问题正是错误信息所说的:你的auxiliaryToAvoidCyclicRecursion函数的返回类型是Method，您试图在布尔含义中使用它，其中需要公式(即布尔类型的东西).在任何其他静态类型语言中，您都会遇到相同类型的错误.

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]
           }
        }       
    }
}

这不应该给你一个编译错误，但要运行它，请确保启用递归(选项 -> 递归深度).正如您将看到的，最大递归深度为 3，这意味着 Alloy Analyzer 最多可以展开您的递归调用 3 次，而不管您的分析范围如何.如果这还不够，您仍然可以选择重写您的模型，以便将所讨论的递归谓词建模为关系.这是一个简单的例子来说明这一点.

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

现在相同的列表，其中 len 被建模为一个关系(即 Node 中的一个字段)

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.

这篇关于在合金中编程递归函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！