使用合金可视化投影

Question

我有一个看起来像这样的合金模型：

open util/ordering[Time] as timeOrder

sig Time {
    database: one Database
}

sig Database {}
{
    #Database>1
    some database.this
}

pred show {}

run show

我想使用合金分析仪来查看每次系统的状态。我假设如果我在“时间”上进行投影，那么我将能够看到这一点。但是，如果我随着时间的推移进行投影，当我查看 Time0 时，它会显示与其他时间关联的数据库。

具体来说，我有一个看起来像这样的跟踪：

如果我随着时间的推移进行投影，我会假设 Time0 只会显示 Database1，而 Time1 只会显示 Database0。但是，当我对 Time 进行投影并查看 Time0 时，它同时显示了 Database0 和 Database1。它确实用 (database) 注释 Database1，但我真正想要的是它只在此视图中显示 Database1。

显然，投影并没有达到我的预期。为什么不？有什么方法可以查看与我正在投影的元素相关联的元素吗？

Answer 1

在签名上的投影减少了绘制关系的数量，但不会隐藏断开的原子。

这可以通过自定义可视化主题来实现：

• 取消选中 sig Database 的属性“显示”
• 检查集合database的“显示”属性（二元关系database成为投影下的集合）

此外，如果您愿意，还可以取消选中“显示为标签”属性以避免节点上的标签 (database)。