CODEWITHSUNDEEP
alloy
Kaiyuan Wang
Kaiyuan Wang

Reputation: 59

Alloy pred/fun parameter constraint

The following Alloy predicate p has a parameter t declared as a singleton of type S. Invoke run p gives the correct result because the predicate body states that t may contain two different elements s and s'. However, in the second run command, a set of two disjoint elements of type S is passed into predicate p and this command gives an instance. Why is it the case?

sig S {}

pred p(t: one S) {
  some s, s': t | s != s'
}

r1: run p -- no instance found

r2: run { -- instance found
  some disj s0, s1: S {
    S = s0 + s1
    p[S]
  }
}

Upvotes: 0

Views: 165

Answers (1)

Daniel Jackson
Daniel Jackson

Reputation: 2768

See https://stackoverflow.com/a/43002442/1547046. Same issue, I think.

BTW, there's a nice research problem here. Can you define a coherent semantics for argument declarations that would be better (that is, simpler, unsurprising, and well defined in all contexts)?

Upvotes: 3

Related Questions