订购一套是什么意思？

Question

当用集合调用排序模块时，所有这些函数突然在集合上可用：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]

firstreturn是什么意思？ last return 是什么意思？ first.next return 是什么？

让我们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.) 中提供的函数使集合被排序出现。但那是一种错觉，它只是放在场景之上的一个视图。事实上，该集合没有顺序。

我的理解正确吗？您还有什么要补充的吗？

Answer 1

造成这种差异的原因有两个词：对称性破缺。简而言之，Alloy 想要避免 returning 同构实例（与标签重命名相同的实例）。

这样想：

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

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

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

然而，您的最终理解是正确的，因为使用排序不会改变它所使用的签名的本质（定义一组原子），而是提供用于定义键入元素排序的函数通过上述签名。

Answer 2

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

What does it mean to order a set?