Alloy 奇怪的行为？

Question

abstract sig S {}
one sig S1, S2 in S {}
fact {S1 != S2}
run {-1 < S1.(S2 -> 1)}

当我打开实例时，我得到了

integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7, S[=12=], S}
Int={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/S={S[=12=], S}
this/S1={S}
this/S2={S[=12=]}

来自评价者，

(1) S1.(S2 -> 1) evaluate to {}

(2) none = S1.(S2 -> 1) evaluate to true

(3) -1 < S1.(S2 -> 1) evaluate to true // Why is an integer less than an empty set?

(4) -1 < none gives type error // This looks good but give (3), why this gives type error?

(5) 0 <= S1.(S2->1) evaluate to true

(6) 0 >= S1.(S2->1) evaluate to true

(7) 0 = S1.(S2->1) evaluate to false // Given (5) (6), it seems S1.(S2->1) evaluate to 0, but it's not.

(8) 0 = none evaluate to false

(9) 0 <= none gives type error // (8) (9) seem to be interesting as "=" is not interpreted as integer comparison.

谁能解释为什么 (1) - (9) 会发生？有错误吗？

Answer 1

(1) 这应该是显而易见的原因：它是一个关系连接并且 S1 与 S2

不同

(2) none 求值为空集，因此给定 (1) none = S1.(S2->1)

是有道理的

(3) 那里没有类型错误，因为-1的类型是int，而S1.(S2->1)的类型是S.(S->int)也就是[=15] =].问题只是为什么 -1 小于某个求值为空集的整数类型表达式。首先，表达式 -1 < S1.(S2->1) 必须求值（即不能像在编程语言中那样抛出异常）。此外，这是一个布尔表达式，因此它的计算结果必须为 true 或 false。那么 Alloy 所做的，为了评估 < 运算符，它必须将两边都转换为单个（标量）整数，即使两边实际上都是整数集（一切都是 set/relation in Alloy)，它通过对每个集合中存在的所有原子求和来实现。所以 只是为了算术比较 , S1.(S2->1) 计算为 0.

(4) 现在应该清楚了，-1 < none确实是类型错误，因为左边的类型是int，右边的类型是none

(5), (6) 与 (3)

的解释相同

(7) 0 = S1.(S2->1) 为假，因为 = 总是集合比较，而不是整数比较。如果你尝试像 1 + 2 = 3 这样的东西，你会得到 false，因为集合 {1, 2} 不是 {3}。

(8) 同理，=是集合比较

(9) (4) 的解释相同

Alloy 奇怪的行为？

Alloy weird behavior?

alloy