alloy - 了解合金中的输出

Question

无法理解合金代码的输出：

abstract sig Name{}
one sig N0, N1, N2 extends Name{}
abstract sig Book{}
one sig b0 extends Book { addr : Name -> Name}
abstract sig E{}
one sig e0 extends E{}
pred show(){
  some *(b0.addr)

}

run show

我很好奇输出是否包含（e0，e0）和（b0，b0）。我附上了分析仪的输出，但不知道如何解释它。这是否意味着 (e0,e0) 在解决方案中？

Answer 1

(e0, e0)“在解决方案中”是什么意思？我建议您阅读 Alloy 书（Software Abstractions，麻省理工学院出版社，2012 年）以了解所有基本概念。