Alloy Analyzer：为给定实例查找模型

Question

我想知道是否可以为给定实例生成模型规范。我的目标是检查实例是否符合模型。

我找到了一篇关于实例自动规范的论文。它被称为“使用实例编写合金规范的自动化方法”(http://users.ece.utexas.edu/~khurshid/papers/2006/06isola-aDeryaft.pdf)。如果我没记错的话，这可能是一种检查实例是否符合模型的方法。不幸的是，似乎没有可供下载的实现。

你知道我如何检查给定实例是否符合模型吗？

感谢您的宝贵时间。

Answer 1

要检查实例是否符合给定模型，您可以通过编程方式检查（使用 Alloy api）实例的所有原子和元组是否由模型的签名和字段键入，并且所有事实在模型保存在实例中。

您参考的论文描述了一种从给定实例生成新合金模型的方法。虽然很有趣，但它与您试图实现的目标无关，即检查给定实例是否符合现有模型。