通过传递闭包以递归方式使用Alloy函数

Question

我在Alloy中做了一个模型来表示Java语言的一个子集。下面我们就这个模型的一些元素：

sig Method { 
    id : one MethodId, 
    param: lone Type, 
    return: one Type, 
    acc: lone Accessibility,  
    b: one Block 
} 

abstract sig Expression {} 
abstract sig StatementExpression extends Expression {} 

sig MethodInvocation extends StatementExpression{ 
    pExp: lone PrimaryExpression, 
    id_methodInvoked: one Method, 
    param: lone Type 
} 

sig Block { 
    statements: seq StatementExpression 
} 

pred noRecursiveMethodInvocationCall [] { 
    no m:Method | m in ^getMethodInvokedInsideBody[m] 
} 

fun getMethodInvokedInsideBody [m: Method] : Method { 
     (univ.(m.b.statements)).id_methodInvoked 
} 

的问题是块已经是StatementExpression在那个同样的方法递归调用，应避免在同一时间的序列。因此，我认为在上面的解决方案。

当我尝试生成相应的情况下，我得到以下错误类型：

. 
Name cannot be resolved; possible incorrect 
function/predicate call; perhaps you used () when you 
should have used [ ] 

This cannot be a correct call to fun 
genericLawsMetaModel/javametamodel_withfield_final/getMethodInvokedInsideBody. 
The parameters are 
m: 
{genericLawsMetaModel/javametamodel_withfield_final/Method} 
so the arguments cannot be empty. 

不过对于这个问题，我也试图改变定义谓词noRecursiveMethodInvocationCall（从而消除提到的功能）：

pred noRecursiveMethodInvocationCall [] { 
    no m:Method | m in ^((univ.(m.b.statements)).id_methodInvoked) 
} 

然而，出现了一种新型的错误：

^ can be used only with a binary relation. 
Instead, its possible type(s) are: 
{genericLawsMetaModel/javametamodel_withfield_final/Method} 

任何线索？我只是想避免递归调用相同的方法。 在此先感谢，

Answer 1

您滥用传递闭包运算符^。 后者仅适用于二元关系，而不适用于功能。

因此，我会将MethodInvokedInsideBody声明为Method的一个字段，并按照您的方式使用传递闭包。

希望它能帮助:)

编辑：

下面是如何传递闭包操作员可以使用才能达到你想要达到什么样的一个例子：

sig Method { 
    id : one MethodId, 
    param: lone Type, 
    return: one Type, 
    acc: lone Accessibility,  
    b: one Block 
    methodsInvokedInsideBody: set Method 
} 

pred noRecursiveMethodInvocationCall{ 
    no m:Method | m in m.^methodsInvokedInsideBody 
}