在下面
sig building{ abv: Man -> Man } { all m:Man | Above(m,m.abv) }
以下是什么意思？它与签名定义有什么关系？这是签名的关系吗？
{ all m:Man | Above(m,m.abv) }
这被称为“附加事实”，意思是它必须保持相应信号的所有原子 . 因此，您的模型的等效事实将是
fact { all b: building | all m: Man | Above[m, m.(b.abv)] }
在附加的事实中，您可以使用 this 关键字来引用相应sig的当前原子，因此更清楚地编写附加事实的方法是显式写入 m.(this.abv) ，而不是依赖于 abv 被隐式扩展为 this.abv .
this
m.(this.abv)
abv
this.abv
1 回答
这被称为“附加事实”，意思是它必须保持相应信号的所有原子 . 因此，您的模型的等效事实将是
在附加的事实中，您可以使用
this关键字来引用相应sig的当前原子，因此更清楚地编写附加事实的方法是显式写入m.(this.abv)，而不是依赖于abv被隐式扩展为this.abv.