在 Alloy 中测试特定解决方案
Testing a specific solution in Alloy
我在我的 .als 文件中定义了一些约束，但是当我单击 执行 时，没有找到解决方案。我有一个特定的解决方案，我怀疑 "should" 可行，但显然由于一些只有 Alloy 可以发现的模糊原因而失败。
我想要的是将我提出的解决方案手动输入 Alloy Visualiser，然后让 Alloy 告诉我违反了哪些约束。这可能吗？
我要做的第一件事是 运行 Unsat Core 来强调不一致。然后，您可以通过将约束从事实转移到谓词来削弱模型；然后，您可以直接在求值器中求值谓词和函数。另请注意，Alloy 分析器可识别构造实例的公式并对其进行优化，例如，
形式的公式
r = a -> b + c -> d
然而，Alloy 不会让您只输入一个实例并对其进行评估。
我在我的 .als 文件中定义了一些约束，但是当我单击 执行 时，没有找到解决方案。我有一个特定的解决方案，我怀疑 "should" 可行，但显然由于一些只有 Alloy 可以发现的模糊原因而失败。
我想要的是将我提出的解决方案手动输入 Alloy Visualiser，然后让 Alloy 告诉我违反了哪些约束。这可能吗？
我要做的第一件事是 运行 Unsat Core 来强调不一致。然后，您可以通过将约束从事实转移到谓词来削弱模型；然后，您可以直接在求值器中求值谓词和函数。另请注意，Alloy 分析器可识别构造实例的公式并对其进行优化，例如，
形式的公式r = a -> b + c -> d
Alloy 不会让您只输入一个实例并对其进行评估。