合金中的总排序

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语句中没有提到实例化排序（所以分析器必须猜测哪个关系是排序）。