如何将一组实例传递给 Alloy Analyzer 的 Evaluator 中的函数或谓词？

Question

BLUF：我有一个谓词，它将一个签名实例和一组相同签名的实例作为参数。在生成模型的实例时，我想将签名的实例传递给谓词，但是如果可能的话，我不知道如何传递一组实例。

Alloy 的 Evaluator 似乎没有很好的记录，除非我错过了它。我有 Daniel Jackson 的书，完成了教程，并在网上找到了各种其他资源，但似乎没有人真正解决如何使用 Evaluator。

我试过这样的符号：

myPred[instance$0,set(instance$1,instance$2)] 和

myPred[instance$0,set[instance$1,instance$2]] 和

myPred[instance$0,(instance$1,instance$2)] 和

myPred[instance$0,[instance$1,instance$2]]

评估者不喜欢其中任何一个。是否可以传递一组实例？如果是这样，我该怎么做？感谢您的帮助！

Answer 1

因此，以我通常的方式，几乎在我提出问题的同时，我就意识到了答案（或者至少是一种做我想做的事情的方法）。我只是使用联合运算符“+”来传递集合。

myPred[instance$0, instance$1 + instance$2]

很抱歉给您带来不便，但也许这会对其他人有所帮助！