订购一套是什么意思？答案

【问题标题】：What does it mean to order a set?订购一套是什么意思？
【发布时间】：2018-02-11 21:57:09
【问题描述】：

当使用集合调用排序模块时，所有这些函数突然在集合上可用：first, last, next, prev, etc.

first returns the first atom.
last returns the last atom.
first.next returns the second atom.

等一下！

根据定义，集合是无序的。那么如何订购一套呢？

考虑这组颜色：

abstract sig Color {}
one sig red extends Color {}
one sig yellow extends Color {}
one sig green extends Color {}

订购这组颜色是什么意思？假设我们调用排序模块：

open util/ordering[Color]

first 返回什么？ last 返回什么？ first.next 返回什么？

让 Alloy 生成一些实例：

run {}

以下是生成的一些实例：

实例 #1

first returns: yellow
last returns: green
first.next returns: red

实例 #2

first returns: yellow
last returns: red
first.next returns: green

实例 #3

first returns: green
last returns: yellow
first.next returns: red

请注意，每个实例的顺序不同。

现在，让我们订购一个简单的签名：

open util/ordering[Time]
sig Time {}
run {}

只生成一个实例：

实例 #1

first returns: Time0
last returns: Time2
first.next returns: Time1

没有更多实例！

经验教训

然而，我认为真正的教训是排序模块 (first, last, next, etc.) 中提供的函数使得 看起来 集合是有序的。但那是一种错觉，它只是放在场景顶部的一个视图。事实上，这个集合没有顺序。

我的理解是否正确？你有什么要补充的吗？

【问题讨论】：

标签： alloy

【解决方案1】：

这种差异背后的原因在于两个词：对称性破坏。简而言之，Alloy 希望避免返回同构实例（与标签重命名相同的实例）。

这样想：

当您分析仅包含签名 one Time{} 的模型时，分析器将返回由原子 Time$0 组成的单个实例。标记此原子 Time$1、Time$2 或 CoolAtom 不会改变实例由单个 Time 类型的原子组成的事实。

在分析声明颜色为红色、黄色或绿色的模型时，分析器将返回 3 个实例，每个实例由不同的颜色组成。你为什么问？这是因为这些原子在语义上是不同的，因为它们没有相同的类型。

请注意，您绝不会创建一个枚举其原子的集合。您已将一组颜色定义为由几个集合（红色、绿色、黄色）组成，这些集合恰好都有一个元数。

然而，您的最终理解是正确的，因为使用排序不会改变它所使用的签名的本质（定义一组原子），而是提供用于定义由说签名。

【讨论】：

【解决方案2】：

当您在某个集合 S 上调用排序模块时，您只是在为每个实例添加一个排序，就好像您在集合 S 上显式包含同构关系一样。正如 Loic 所指出的，这样做比这样做更好的关键原因明确的是，您可以免费获得对称性破坏，从而获得更好的性能（以及更方便的原子编号）。当然，您不需要自己公理化排序。

【讨论】：