alloy - 引数付き述語と引数なし述語の合金

Question

本で次の定義を見ました。

pred show(b: Book){
  some b.addr
}

どこ

abstract sig Name, Addr {}
sig Book { addr: Name lone -> lone Addr }

Alloyアナライザーで遊んだ後、これは

pred show(){
  some b:Book | some b.addr
}

Book を引数として指定し、量指定子を使用する 2 番目のアプローチを使用しないことの利点は何ですか?

Answer 1

述語に引数を使用するか使用しないかは「アプローチ」ではなく、セマンティクスが異なります。述語に含めるsome bと、それ以外では使用できませんall b...

例えば：

sig Addr {}

sig Book {
    addr: Addr
}

pred show {
    some b:Book | some b.addr
}

pred show'[b:Book] {
    some b.addr
}

check { show }

// These are not possible without an argument to show'
check { all b:Book | show'[b] }
check { some b:Book | show'[b] }
check { no b:Book | show'[b] }