删除 Alloy 中的谓词关系

Question

我正在学习如何使用 Alloy，并且我编写了以下代码：

module test/SlotsAndFillers

sig Slot { content: one Filler}
sig Filler { slots: set Slot}

fact AllSlotsAreOwned {
    all s:Slot | some x:Filler | s in x.slots
}

fact ImproperParthoodSlots {
    all x:Filler | some y, z:Slot |  y in x.slots implies z in x.slots and x in z.content
}

fact SlotInheritance {
    all x, y : Filler, z, z' : Slot | x != y and z != z' and z in y.slots and x in z.content and z' in x.slots implies z' in y.slots
}

fact SingleOccupancy {
    all x:Slot, y:Filler  | x in y.slots implies one z:Filler | z in x.content
}

fact MutualOccupancyIsIdentity {
    all x, y: Filler, z, z': Slot | x != y and z != z' and
    z in y.slots and x in z.content and z' in x.slots and y in z'.content implies x = y
}

pred show() {}

run show

当我执行和显示模型时，除了关系 content 和 slots，模型还有新的关系，命名为 $show_x、$show_y 和 $show_z。通过测试，我了解到如果我在谓词中添加内容，这些关系就会存在。但是这段代码，show是空的，还有这些关系。所以我有两个问题：它们来自哪里以及如何删除它们？我知道我可以隐藏它们，但是模型看起来（几乎）都一样。所以我想探索只使用我的两个关系而不是新关系的不同模型。

请毫不犹豫地重新表述或重新命名此 post。

谢谢！

Answer 1

当您执行运行命令后跟一个谓词时，您实际上是在生成满足该谓词的实例。根据我的理解，当谓词被命名时，实例可视化工具会尝试突出显示实例的哪些元素满足谓词。在你的例子中，“一切”都符合这个空谓词，所以你的谓词名称随处可见。

一个简单的解决方法是不命名作为参数提供给运行命令的谓词：

module test/SlotsAndFillers

sig Slot { content: one Filler}
sig Filler { slots: set Slot}

fact AllSlotsAreOwned {
    all s:Slot | some x:Filler | s in x.slots
}

fact ImproperParthoodSlots {
    all x:Filler | some y, z:Slot |  y in x.slots implies z in x.slots and x in z.content
}

fact SlotInheritance {
    all x, y : Filler, z, z' : Slot | x != y and z != z' and z in y.slots and x in z.content and z' in x.slots implies z' in y.slots
}

fact SingleOccupancy {
    all x:Slot, y:Filler  | x in y.slots implies one z:Filler | z in x.content
}

fact MutualOccupancyIsIdentity {
    all x, y: Filler, z, z': Slot | x != y and z != z' and
    z in y.slots and x in z.content and z' in x.slots and y in z'.content implies x = y
}

run {}

编辑：

看来这个修复没有解决问题。实际上，事实中定义的量化变量仍然由实例查看器显示。摆脱它们的唯一选择（我能想到）是在主题菜单中手动禁用它们的表示。

（对于 $x、$y、$z 这 3 个关系，将“显示为弧”设置为关闭）

删除 Alloy 中的谓词关系

Remove predicate relations in Alloy

alloy