BLUF: I have a predicate which takes as arguments an instance of a signature and a set of instances of the same signature. Upon generating instances of the model, I'd like to pass instances of the signature to the predicate, but am at a loss for how to pass a set of instances, if it is even possible.
Alloy's Evaluator does not appear to be well-documented, unless I've missed it. I have Daniel Jackson's book, have done the tutuorial, and found various other resources online, but no one really seems to address how to use the Evaluator.
I've tried notation like:
myPred[instance$0,set(instance$1,instance$2)]
and
myPred[instance$0,set[instance$1,instance$2]]
and
myPred[instance$0,(instance$1,instance$2)]
and
myPred[instance$0,[instance$1,instance$2]]
The Evaluator doesn't like any of them. Is it possible to pass a set of instances? If so, how do I do it? Thanks for the help!
So, in usual fashion for me, almost as soon as I asked the question, I realized the answer (or at least a way to do what I wanted to). I simply used the union operator "+" to pass the set.
myPred[instance$0, instance$1 + instance$2]
Sorry for the inconvenience, but maybe this will help someone else!