我创建了一个测试图来尝试创建一个独立集。我知道独立集是一组没有连接的顶点，但我不知道如何在合金4.2中实现这一点。下面是我有： abstract sig Vertex {
e: set Vertex -- e is the edge relation
}
-- the test graph has vertices A, B, C, D, E, F
one sig A, B, C,
我想让Alloy实例化一组完全有序的节点，但似乎无法做到我想要的。这里是一个简单的例子： open util/ordering[S]
sig S {
rel : set S
}
pred show {}
run show for 4
我期待看到高达那些在链条，而是我看到4个节点是互不相干4个节点。杰克逊书第6.1.1节建议使用util/ordering来定义这样的事情，
我学习合金，并试图使其找到两个二元关系r和s，从而s等于r传递闭包，并且使得s不等于r。我想我可以问合金通过执行这样做如下： sig V
{
r : V,
s : V
}
assert F { not (some (s-r) and s=^r) }
check F
现在合金4.2找不到一个反例，但一个简单的3要素的组成将是一个地方r = {(V0,V1), (V1,