理解複雜的簽名

Question

在下面

sig building{ 
    abv: Man -> Man 
} 
{ 
all m:Man | Above(m,m.abv) 
} 

什麼是下面的意思嗎？它與簽名定義有什麼關係？這是一個sig的關係嗎？

{ 
all m:Man | Above(m,m.abv) 
} 

Answer 1

這就是所謂的「附加事實」，其含義是它必須適用於對應sig的所有原子。因此，對於你的模型等效其實是

fact { 
    all b: building | 
    all m: Man | Above[m, m.(b.abv)] 
} 

在附加的事實，你可以使用this關鍵字來引用相應的SIG的當前原子，所以寫你的附加實際上是明確更明確的方式寫m.(this.abv)，而不是依靠abv被隱式擴展爲this.abv。