合金 pred/fun 参数约束

Question

下面的合金谓词 p 有一个参数 t 声明为 S 类型的单例。调用 run p 给出正确的结果，因为谓词主体声明 t 可能包含两个不同的元素 s 和 s'。然而，在第二个run 命令中，一组S 类型的两个不相交元素被传递到谓词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。我认为同样的问题。

顺便说一句，这里有一个很好的研究问题。您能否为参数声明定义一个更好的连贯语义（即更简单、不出所料且在所有上下文中定义良好）？