合金predが/楽しいパラメータ制約

Question

以下合金述語pは、パラメータtはタイプS.起動run pのシングルトンとして宣言し、正しい結果が得られるので、Tは、2つの異なる要素sとs'を含んでいてもよい述語体状態。しかし、第2のrunコマンドでは、タイプSの2つの分離した要素のセットが述語pに渡され、このコマンドはインスタンスを与えます。それはなぜですか？

sig S {} 

pred p(t: one S) { 
    some s, s': t | s != s' 
} 

r1: run p -- no instance found 

r2: run { -- instance found 
    some disj s0, s1: S { 
    S = s0 + s1 
    p[S] 
    } 
} 

Answer 1

https://stackoverflow.com/a/43002442/1547046を参照してください。同じ問題だと思います

ところで、いい研究の問題があります。より良い（つまり、より簡単で、驚くべきことではなく、すべてのコンテキストで明確に定義されている）引数宣言のための一貫したセマンティクスを定義できますか？