示例中的訪問對象編號

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 + ... 

現在，由於排序上簽字的名字，這是有序的明確固定的，由合金中發現的車型確實會滿足您所需的性能。