CODEWITHSUNDEEP
alloy
thepandaatemyface
thepandaatemyface

Reputation: 5267

Quantifying a certain number of elements in a set

So i have a predicate that takes a set as an argument, and so I can do this:

all disj t1, t2, t3: set Thing | predicate[t1+t2+t3]

I was wondering if it was possible to do this by just specifying the size of the set, so something like

all ts: set of 4 Thing | predicate[ts]

What I eventually would like to do is find the minimal integer for which the predicate is valid. Is that in any way possible?

Upvotes: 1

Views: 622

Answers (2)

Daniel Jackson
Daniel Jackson

Reputation: 2768

Not sure what you're trying to achieve here, but a direct expression of what you seem to be asking for 

all ts: set of 4 Thing | predicate[ts] -- not Alloy

would be

all ts: set Thing | #ts = 4 implies predicate[ts]

Upvotes: 1

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

High order quantification is often discouraged as, to my understanding, the Alloy Analyzer can't always deal with them. (it uses skolemization to get rid of them, but those can't always be applied)

I would thus simplify your model as follows :

sig Thing{
}

run predicate for exactly 4 Thing

In the pred predicate evaluate the property your are interested in on the full set of Thing (constrained to contain exactly 4 atoms) directly.e.g. Thing.field= ....

Btw, I don't think that all disj t1, t2, t3: set Thing | predicate[t1+t2+t3] is doing what you expect it to do. Indeed, t1 t2 and t3 are all sets of Thing with the property that they are disjoint sets. t1+t2+t3 thus won't necessarily produce a set of 3 Things.

Upvotes: 3

Related Questions