量化集合中一定数量的元素答案

【问题标题】：Quantifying a certain number of elements in a set量化集合中一定数量的元素
【发布时间】：2014-12-13 22:27:55
【问题描述】：

所以我有一个将集合作为参数的谓词，所以我可以这样做：

all disj t1, t2, t3: set Thing | predicate[t1+t2+t3]

我想知道是否可以通过指定集合的大小来做到这一点，比如

all ts: set of 4 Thing | predicate[ts]

我最终想做的是找到谓词有效的最小整数。这有可能吗？

【问题讨论】：

标签： alloy

【解决方案1】：

通常不鼓励高阶量化，因为据我了解，合金分析仪无法始终处理它们。（它使用 skolemization 来摆脱它们，但并不总是适用）

因此，我将您的模型简化如下：

sig Thing{
}

run predicate for exactly 4 Thing

在 pred predicate 中直接评估您对完整的事物集感兴趣的属性（限制为恰好包含 4 个原子）。例如Thing.field= ....

顺便说一句，我不认为all disj t1, t2, t3: set Thing | predicate[t1+t2+t3] 正在做你期望它做的事情。实际上，t1 t2 和 t3 都是 Thing 的集合，具有不相交集的属性。因此 t1+t2+t3 不一定会产生一组 3 个事物。

【讨论】：

【解决方案2】：

不知道你想在这里实现什么，但直接表达了你的要求

all ts: set of 4 Thing | predicate[ts] -- not Alloy

会

all ts: set Thing | #ts = 4 implies predicate[ts]

【讨论】：