合金分析仪：量词和集合产品

Question

我在 Alloy 中遇到了以下问题。考虑尝试捕获甚至标记实体的玩具代码（V1 用于 State，V2 用于 ProductStateSet）：

enum State {s1, s2, s3, s4, s5, s6}
enum DummySet {b,c}

let  ProductStateSet = DummySet->State

pred evenV1 (state: State){
(state = s2) or (state=s4) or (state=s6)
}


pred evensetV1 (stateset: State)  {
all state: stateset | evenV1[state]
}

assert a2V1 {
evensetV1[(s2 + s4)]
}

pred evenV2 (state: ProductStateSet){
(state = b->s2) or (state=b->s4) or (state=b->s6)
}

assert a1V2  {
evenV2[b->s2]
}


pred evensetV2 (stateset: ProductStateSet)  {
all state: stateset | evenV2[state]
}

assert a2V2 {
evensetV2[ (b->s2) + (b->s4) ]
}

断言 a2V1 为真，但 a2V2 为假，而我本以为它们是相同的。为什么会这样，在处理集合产品时使用量词的正确方法是什么？

如果我将“evenset”更改为“some”而不是“all”，则使用 evensetV1 没有问题，但对于 evensetV2，我得到：

pred evensetV2 (stateset: ProductStateSet)  {
some state: stateset | evenV2[state]
}

assert a2V2 {
evensetV2[ (b->s2) + (b->s4) ]
}


Executing "Check a2V2"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   Generating CNF...
.
Analysis cannot be performed since it requires higher-order
quantification that could not be skolemized.

这个例子的另一个关于集合理解的问题：我可以写一个断言，比如：

assert a3V1{
#{state: State | evenV1[state]} > 2
}

有没有办法打印出set元素，也就是可以打印出下面的set吗？

{state: State | evenV1[state]}

谢谢！

Answer 1

关于你的第一个问题：

已编辑（第一个答案是错误的）

运行断言给出了 2 个反例。 一个是预期的，因为在 evenV2 谓词中没有考虑 none -> none。但另一个（见下文）对我来说没有意义。

我唯一合乎逻辑的解释是 evenSetV2 的量化变量“状态”在 evenV2 的参数中给出时被错误解释，即使它似乎有点牵强...

我认为，只要有可能，就应该避免量化，而更喜欢更直接的集合操作。如下实现谓词和断言可以解决问题（您甚至不再需要区分单例和集合方法）：

pred evenV2 ( state:  ProductStateSet){
DummySet.state in (s2+s4+s6)
}

assert a2V2 {
evenV2[ (b->s4)+ (b->s6)]
}

结束编辑

对于第二个问题，Alloy 评估员是您的朋友。