function - Alloy での述語の使用

Question

別の述語 (つまり、checkOverriding) から 2 つの述語 (たとえば、methodsWiThSameParameters と MethodsWiThSameReturn) を使用しようとしていますが、「実行するコマンドがありません」というエラーが表示されます。手がかりはありますか？関数も使用しようとしましたが、構文または関数がブール値を返さないため、成功しませんでした。

以前の質問でコメントしたように、これらは Alloy で指定された Java メタモデルの一部です。

pred checkOverriding[]{
//check accessibility of methods involved in overriding
  no c1, c2: Class {
    c1=c2.^extend
    some m1, m2:Method |
          m1 in c1.methods && m2 in c2.methods && m1.id = m2.id 
          && methodsWiThSameParameters[m1, m2] && methodsWiThSameReturn[m1, m2] && 
               ( (m1.acc = protected && (m2.acc = private_ || #(m2.acc) = 0 )) ||
                 (m1.acc = public && (m2.acc != public || #(m2.acc) = 0 )) ||
                 (#(m1.acc) = 0 && m2.acc != private_ )
               )
      }
    }

pred methodsWiThSameParameters [first,second:Method]{
    m1.param=m2.param || (#(m1.param)=0 && #(m2.param)=0)  
}
pred methodsWiThSameReturn [first, second:Method]{
    m1.return=m2.return || (#(m1.return)=0 && #(m2.return)=0) 
}

---

CM Sperberg-McQueen さん、ご回答ありがとうございます。しかし、私の質問は十分に明確ではなかったと思います。

私の述語、たとえば checkOverriding は、次のような事実から呼び出されています。

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

したがって、「実行するコマンドがありません」というエラーを理解していません。