首页 文章

合金 - 找不到不满的核心

提问于
浏览 次
1

我有一个“No instance found”Alloy文件，并想调试它 . 文档说要去选项并选择SAT Solver>不满核心 . 然而，我没有看到，只有SAT4J .

我正在运行最新的Alloy 4.2，刚下载 . 当我运行时，有一条关于不支持JNI的说明 . 如果我需要下载不同的配置以查看不满核心，请告诉我该怎么做 . 否则，我该如何调试Alloy文件？

enter image description here

那是最新的稳定 . 我也尝试了最新的实验，并得到了相似（不完全相同）的结果 . 但请注意此警告：

Alloy Analyzer 4.2_2015-02-22 (build date: 2015-02-22 18:21 EST)

Warning: JNI-based SAT solver does not work on this platform.
This is okay, since you can still use SAT4J as the solver.
For more information, please visit http://alloy.mit.edu/alloy4/
.

Warning: Alloy4 defaults to SAT4J since it is pure Java and very reliable.
For faster performance, go to Options menu and try another solver like MiniSat.
If these native solvers fail on your computer, remember to change back to SAT4J.
alloy

1 回答

  • 0

    你只看到SAT4J？只是一个完整性检查：你点击选项菜单，然后在读取Solver：SAT4J的行上，对吧？

    当你这样做时，你应该得到一个带有SAT求解器列表的子菜单;在我的系统上，它看起来像这样：

    Screen shot of Alloy 4.2 Options / Solve menu

    我希望这有帮助 . 如果没有，我希望接下来要问的是构建About Alloy对话框的内容 . （为了比较：刚刚给出的屏幕截图是由2014-05-16的版本制作的 . ）

    [后记]

    啊 . 对 . 您的经验清楚地表明the documentation中的评论意味着什么：

    默认情况下，选择纯Java解算器“SAT4J”，因为它在每个平台和操作系统上运行 . 如果您需要更快的性能，可以尝试使用MiniSat或ZChaff等原生解算器 .

    我从那里（现在）推断，除了SAT4J之外的解算器并不是所有（或者可能是其中任何一个）纯Java，而是需要本机接口（即用其他语言编写的代码的接口） . 如果JNI在您的平台上不起作用，正如您的警告消息所示，SAT4J可能是唯一可用的解算器 .

    也许开发团队的某个人可以发表评论 .

    因此，如果您无法切换到Unsat Core作为查找模型没有实例的原因的方法，那么您将被抛回其他方法 .

    一种方法很明显（虽然有点乏味）：通过模型中的约束集进行二元搜索 .

    如果你知道我的意思，并且想不出更好的方法，那么这么久又好运 .

    如果您知道我的意思并且可以想到更好的方法，请告诉我们其他人它是什么 .

    如果你不喜欢编程珍珠 . 也许 . ）这是一种方法 .

    • 以当前状态备份模型 . 当你开始怀疑这个或那个微小的细节是否已经改变时，你将需要它 .

    • 将所有命名事实更改为命名谓词 . （如果证明有必要，也可以将所有签名事实，甚至其他约束更改为命名谓词 . 我只能在没有其他选择的情况下执行此操作，因为它需要重写更多的模型而不是我想要的 . ）

    • 创建一个新谓词，并将所有命名谓词进行AND运算 . 在下面我将称之为 AllTogetherNow . 它会有类似的形式

    pred AllTogetherNow {
  P1
  P2
  P3
  ...
  Pn
}

    此时，您的模型应该包含签名（带或不带签名事实）和命名谓词，没有事实 .

    • 检查以确保在 AllTogetherNow 不为真时可以实例化模型 .

    如果无法实例化，并且您仍然具有签名事实，则返回步骤2并将其中的部分或全部因素考虑在内 . 修改 AllTogetherNow 以包含新的因子约束 .

    如果它可以具有任何签名事实，则返回到步骤2并分解签名中基数约束中隐含的约束 . 修改 AllTogetherNow 以包含新的因子约束 .

    • 检查 AllTogetherNow 是否可以实例化 .

    如果它可以被实例化，那么原始模型和现在之间的某些东西已经发生了变化 . 改变的是原始模型中的错误 .

    • 注释掉目前生活在 AllTogetherNow 中的一半谓词，通过狡猾或随机选择 .

    • 检查 AllTogetherNow 是否可以实例化 .

    如果它不能，则 AllTogetherNow 中当前存在的谓词的某个子集包含矛盾 . 返回步骤6以注释掉更多谓词 .

    如果现在可以实例化 AllTogetherNow ，那么您刚刚注释掉的谓词的某个子集就是模型无法像最初编写的那样实例化的原因 . 继续第8步 .

    • 取消注释当前在 AllTogetherNow 中注释掉的一半约束，随机选择或通过狡猾选择 . 返回第7步 .

    我的经验是通过步骤6-8的一些循环通常有助于集中我的注意力，我可以最终看出矛盾所在 . 初始草案模型的主要复杂性并不仅限于单一的矛盾，（2）矛盾可能源于单独无害的谓词的不愉快组合，以及（3）可能有多种方法来构建矛盾的组合（谓词，A，B，C和D都很好; A与B或C一起致命......） .

    可能出现的一个心理困难是，矛盾不是出现在模型的一部分，而是在一个人知道任何解决方法，除了告诉自己任何意外的矛盾自然有趣，值得花时间 . 有时我能够说服自己 .

    回复于

相关问题