合金中的總排序

Question

我想讓Alloy實例化一組完全有序的節點，但似乎無法做到我想要的。這裏是一個簡單的例子：

open util/ordering[S] 

sig S { 
    rel : set S 
} 

pred show {} 

run show for 4 

我期待看到高達那些在鏈條，而是我看到4個節點是互不相干4個節點。傑克遜書第6.1.1節建議使用util/ordering來定義這樣的事情，但是我必須在這裏錯過一些東西。

Answer 1

庫模塊在S上提供了一個可以通過next和prev等函數訪問的排序關係（只需在utils文件夾中打開代碼即可查看）。如果您願意，也可以明確地訪問該排序關係（但最好使用函數）。

您定義的關係rel不受影響，並且不受打開庫模塊的限制。如果你仔細想想，rel被約束是沒有意義的，因爲在open語句中沒有提到實例化排序（所以分析器必須猜測哪個關係是排序）。