alloy - 删除合金中的谓词关系

Question

我正在学习如何使用合金，我已经编写了这个代码：

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和slot之外，模型还有新的关系，名为$show_x、$show_y和$show_z。通过测试，我了解到如果我在谓词中添加内容，就会存在这些关系。但是对于这段代码，show是空的，仍然存在这些关系。所以我有两个问题：它们来自哪里以及如何删除它们？我知道我可以隐藏它们，但是模型看起来都（几乎）相同。所以我想探索只使用我的两个关系而不是新关系的不同模型。

不要犹豫，重新制定或重新命名这篇文章。

谢谢！

标签： alloy

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 {}

编辑：

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

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