合金奇怪的行为？答案

【问题标题】：Alloy weird behavior?合金奇怪的行为？
【发布时间】：2017-08-29 23:02:15
【问题描述】：

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$0, S$1}
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$0, S$1}
this/S1={S$1}
this/S2={S$0}

来自评估者，

(1) S1.(S2 -> 1) 评估为 {}

(2) none = S1.(S2 -> 1) 评估为真

(3) -1 1) 计算结果为真 // 为什么整数小于比空集？

(4) -1

(5) 0 1) 评估为真

(6) 0 >= S1.(S2->1) 计算结果为真

(7) 0 = S1.(S2->1) 评估为假 // 给定 (5) (6)，看起来 S1.(S2->1) 计算结果为 0，但不是。

(8) 0 = 没有评估为假

(9) 0

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

【问题讨论】：

标签： alloy

【解决方案1】：

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

(2) none 评估为空集，因此给定 (1) none = S1.(S2->1) 是有意义的

(3) 没有类型错误，因为-1 的类型是int，S1.(S2->1) 的类型是S.(S->int)，即int。问题只是为什么-1 小于某些计算结果为空集的整数类型表达式。首先，表达式-1 < S1.(S2->1) 必须评估为某些东西（即，不能像在编程语言中那样抛出异常）。此外，这是一个布尔表达式，因此它必须计算为true 或false。因此，Alloy 所做的，为了评估 < 运算符，它必须将两边都转换为单个（标量）整数，即使两边实际上都是整数集（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)的解释相同

【讨论】：