合金分析儀：找出給定實例的模型

Question

我在想，是否可以爲給定實例生成模型規範。我的目標是檢查一個實例是否符合模型。

我發現一篇關於實例自動指定的文章。它被稱爲「使用實例編寫合金規格的自動化方法」（http://users.ece.utexas.edu/~khurshid/papers/2006/06isola-aDeryaft.pdf）。如果我沒有弄錯，這可能是一種檢查實例是否符合模型的方法。不幸的是，似乎沒有可用的下載實施。

你知道我該如何檢查給定的實例是否符合模型？

謝謝你的時間。

Answer 1

要檢查實例是否符合給定模型，可以通過編程方式檢查（使用Alloy api）實例的所有原子和元組都是通過模型的簽名和字段鍵入的，並且聲明所有事實在模型舉行的實例。

您所引用的論文描述了從給定實例生成新Alloy模型的方法。儘管有趣，但它與你試圖達到的目標無關，即檢查一個給定的實例是否符合已經存在的模型。