alloy - 合金中带参数的谓词和不带参数的谓词

Question

我在一本书中看到了以下定义：

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

在哪里

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

在玩过合金分析仪后，我意识到这和

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

我很好奇将 Book 指定为参数有什么好处，而不是使用量词的第二种方法？

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] }