1

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

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

4

1 回答 1

1

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

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

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

于 2020-02-29T17:37:56.403 回答