合金：是否可以检索使至少一个约束为假的“实例”

Question

我一直以相同的方式使用 Alloy：要么为给定的一组约束（= 模型）查找实例（解决方案），要么检查可以表示为断言的模型的特定属性（检查在为了搜索反例）。但是，有一个新要求引起了我的两个问题：

1. 是否可以检索不满足合金模型中包含的约束的变量的所有关系分配？这意味着我想收集所有不是给定合金模型解决方案的示例。
2. 如果是：我该怎么做？

非常感谢您！

Answer 1

如果pred 是您模型的一组约束，那么run {!pred} 将找到所有违反这些约束的实例。