【发布时间】：2017-05-25 13:34:31
【问题描述】：
以下合金型号：
sig A {}
run {all a : A | some r : A->A | a.r = a} for 3
run {some a : A | all r : A->A | a.r = a} for 3
Alloy 和 Alloy* 均失败。如果我使用普通 Alloy 运行这两个命令（具体来说，使用来自 http://alloy.mit.edu/alloy/download.html 的最新版本，版本 4.2_2015-02-22，构建日期 2015-02-22 18:21 EST），那么 first 命令工作正常，但 second 无法完成：
但是，如果我使用 Alloy* 运行这两个命令（具体来说，使用来自 http://alloy.mit.edu/alloy/hola/ 的 hola-0.2.jar），那么 first 命令无法进行 skolemize 并且 second em> 命令工作正常：
也许这里有某种错误？我认为这样的问题不应该发生在 Alloy* 中；事实上，Alloy* 论文指出它“允许高阶量词出现在任何地方”。
【问题讨论】：
-
有趣的是，如果我通过将
a : A更改为a : A->A使问题“更难”，那么 skolemization 成功！ -
尝试将 Skolem depth 设置为至少 1。SAT4J/Skolem depth=1 适用于您的模型。
-
约翰，这是我的比较输出。我正在运行您的模型复制/粘贴。会不会是 CEGIS 选项？我从来没有见过。执行“Run run$1 for 3” Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 205 vars。 30个初级变量。 316 条。 26 毫秒。找到实例。谓词是一致的。 26 毫秒。
-
John, Alloy Analyzer 4.2_2015-02-22（构建日期：2015-02-22 18:21 EST），它位于下载页面上的“实验版本”标签下。
-
@AttilaKaroly 我已经修改了我的问题的陈述——如果你有时间，你能再看看我编辑过的问题吗？非常感谢。
标签： alloy