合金 - 计算其他原子使用的原子

Question

我试图注意到原子与其他原子的关系发生了变化。使用以下签名：

    sig Word, Definition{}

    sig Dictionary {
        def: Word -> lone Definition
    }

然后，我使用谓词来展示当您通过另一个 Dictionary 向 Dictionary 添加新关系时会发生什么，这与 Dictionary 相同，但多了一个关系。

    pred addRelation [d,d':Dictionary,w:Word,f:Definition] { 
        d'.word = d.word + w -> f 
    }

要查看第一个 Dictionary 使用的 Word 原子的数量是否增加，我只能使用以下方法显示发生这种情况的实例：

    #d'.def.Definition > #d.def.Definition

但是，有没有办法查看第二个Dictionary atom 使用的Definition atom 的数量是否增加了？我一直在 Alloy Evaluator 中使用反复试验来尝试为此找到一个值，但结果不足。

谢谢！

Answer 1

像这样？

sig Word, Definition{}

sig Dictionary {
    def: Word -> lone Definition
}

pred addRelation [d,d':Dictionary,w:Word,f:Definition] { 
    d'.def = d.def + w -> f 
    #d'.def[Word] > #d.def[Word]
}
run addRelation