Home Articles

理解合金中复杂的特征

Asked
Viewed 1905 times
0

在下面

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

以下是什么意思?它与签名定义有什么关系?这是签名的关系吗?

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

1 Answer

  • 1

    这被称为“附加事实”,意思是它必须保持相应信号的所有原子 . 因此,您的模型的等效事实将是

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

    在附加的事实中,您可以使用 this 关键字来引用相应sig的当前原子,因此更清楚地编写附加事实的方法是显式写入 m.(this.abv) ,而不是依赖于 abv 被隐式扩展为 this.abv .

Related