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、MIT Press、2012 年) を読むことをお勧めします。