示例中的访问对象编号

Question

如果我只有一个sig A并想链接它的多个实例（例如通过后继关系），Alloy会随机为它们编号（A1，A2，A3，...）。

有没有办法告诉它，我希望这些按升序排列？

或者说A3必须在A1之后出现，但A2在A4之前或类似的约束之后。

Answer 1

如果你的目标是要在A征收总订单，那么我会建议使用util/ordering库：

open util/ordering[A] 

如果您使用此库，然后分析仪将尽最大努力，以保持在上升的A原子订单（根据在库中声明的next关系，即A$1.next将为A$2等）。此外，由于改善了对称性分析，分析效率更高。但是，您需要知道签名A将完全饱和，因为5 A的范围将与exactly 5 A相同。

Answer 2

在一般情况下，没有办法将sig实例的名称连接到您在模型中定义的任何关系（无论是“链接关系”还是“库”）。 （。从本质上讲，这是达合金的求解器可能无法预测实例化新名称）

一个选择，那也许可以在你的情况下工作，可能是声明多个SIGS，例如：

one sig A1, A2, A3, ... extends A {} 

与一个“链接关系”：

succ = A1 -> A2 + A2 -> A3 + ... 

现在，由于排序上签字的名字，这是有序的明确固定的，由合金中发现的车型确实会满足您所需的性能。