对合金传递闭包的怀疑

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: set StatementExpression
}

pred noRecursiveMethodInvocationCall [] {
    all bl:Block | all mi, mi2: MethodInvocation | all m:Method |  
    bl in m.b && mi in bl.statements 
    && mi2 = mi.*(id_methodInvoked.b.statements)  =>  
    m != mi2.id_methodInvoked
}

问题是谓词 noRecursiveMethodInvocationCall 显然不起作用，因为生成的实例包含以递归方式调用的方法（甚至间接地，例如 m1 调用 m2，它调用 m3 又调用 m1）并且我想避免递归.

实例是通过另一个模型生成的，见下文：

open javametamodel_withfield_final

one sig BRight, CRight, BLeft, CLeft, Test extends Class{
}

one sig F extends Field{}

fact{
    BRight in CRight.extend
    BLeft in CLeft.extend
    F in BRight.fields
    F in CLeft.fields
    all c:{Class-BRight-CLeft} | F !in c.fields
}

pred law6RightToLeft[]{
    proviso[]
}

pred proviso [] {
   some BRight.extend   
   some BLeft.extend

   #(extend.BRight) > 2
   #(extend.BLeft) > 2

   no cfi:FieldAccess | ( cfi.pExp.id_cf in extend.BRight || cfi.pExp.id_cf in BRight || cfi.pExp.id_cf in extend.BLeft || cfi.pExp.id_cf in BLeft) && cfi.id_fieldInvoked=F
   some Method
}

run law6RightToLeft for 9 but 15 Id, 15 Type, 15 Class

请问有没有人知道问题出在哪里？

提前感谢您的关注，

---

后续查询

关于这个问题，建议的谓词解决了递归问题：

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

但是，它会导致与另一个谓词不一致（见下文），并且当两个谓词都存在时不会生成实例。

pred atLeastOneMethodInvocNonVoidMethods [] {
  all m:Method 
  | some mi:MethodInvocation 
  | mi in (m.b).statements
}

知道为什么不能使用两个谓词生成实例吗？

Answer 1

您可能会仔细查看情况

mi2 = mi.*(id_methodInvoked.b.statements)

这似乎是检查从mi 递归可达的所有语句的集合是否等于单个语句mi2。现在，除非我再次对多重性感到困惑，否则mi2 是一个标量，所以在任何情况下，所讨论的方法有一个包含多个方法调用语句的块，这个条件不会触发并且谓词将虚无缥缈。

将= 更改为in 可能是最简单的解决方法，但在这种情况下，我希望您不会得到任何非空实例，因为您正在使用* 并获得自反传递闭包，而不是^（正传递闭包）。

乍一看，条件似乎可以简化为类似

pred noRecursion {
  no m : Method 
  | m in m.^(b.statements.idMethodInvoked)
}

但也许我错过了一些东西。

---

后记：该问题的后续补充询问为什么在禁止递归与每个方法都包含至少一个方法调用的要求相结合时不会生成实例：

pred atLeastOneMethodInvocNonVoidMethods [] {
  all m:Method 
  | some mi:MethodInvocation 
  | mi in (m.b).statements
}

也许了解问题的最简单方法是想象构建一个调用图。图的节点是方法，图的弧是方法调用。如果方法 M1 的主体包含对方法 M2 的调用，则存在从节点 M1 到节点 M2 的弧。

如果我们根据图来解释这两个谓词，谓词noRecursiveMethodInvocationCall 意味着图是无环的。谓词atLeastOneMethodInvocNonVoidMethods 表示图中的每个节点都至少有一个出弧。

尝试使用单个方法 M。此方法必须包含方法调用，并且此方法调用必须调用 M（因为 Universe 中没有其他方法）。所以我们有一条从 M 到 M 的弧，图有一个循环。但是图形不允许有循环。所以我们不能创建一个同时满足两个谓词的单一方法宇宙。

使用两种方法重试，M1 和 M2。让 M1 呼叫 M2。现在，M2 叫什么？它不能在不循环的情况下调用 M1。它不能在不循环的情况下调用 M2。我们又失败了。

我刚才没时间查，但我想你会发现图论有一个基本定理，如果边数等于节点数，则图一定有圈.