CODEWITHSUNDEEP
alloy
Programmer
Programmer

Reputation: 6753

Predicate with arguments and predicate without arguments in alloy

I saw the following definition in a book:

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

where 

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

After playing with the Alloy analyzer, I realized this is the same as 

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

I was curious what is the advantage of specifying Book as an argument, and not use the second approach using quantifiers?

Upvotes: 2

Views: 750

Answers (1)

Aviad P.
Aviad P.

Reputation: 32629

Using or not using arguments to predicates is not an 'approach' it has different semantics. If you include some b in your predicate you can't use all b outside of it...

For example:

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

Upvotes: 1

Related Questions