【发布时间】：2016-02-10 21:33:15
【问题描述】：
我有一个合金模型，当它在合金工具 (alloy4.2.jar) 中运行时，可以毫无问题地生成实例。但是，当我使用相同的模型作为 Java 中 Alloy api 的输入以获取所有这些实例时，一段时间后会生成内存不足错误（在错误出现之前捕获了许多实例）。
错误恰好发生在下面代码中位于 try 命令之后的 if 命令中（进一步对应于打印堆栈跟踪中的 JDolly.java:192）：
@Override
public boolean hasNext() {
// primeira vez
if (firstTime) initializeAlloyAnalyzer();
if (currentAns.satisfiable() && firstTime) {
firstTime = false;
return true;
}
if (maximumPrograms > 0 && maximumPrograms == currentProgram) return false;
boolean result = true;
try {
if (!currentAns.next().satisfiable() || currentAns.equals(currentAns.next())){
result = false;
System.out.println("TARCIANA -- non satisfiable, linha 194");
} else {
currentAns = currentAns.next();
}
} catch (Err e) {
result = false;
e.printStackTrace();
}
return result;
}
此错误的打印堆栈跟踪是：
Exception in thread "main" java.lang.OutOfMemoryError: GC overhead limit exceeded
at kodkod.util.collections.IdentityHashSet.<init>(IdentityHashSet.java:162)
at kodkod.util.nodes.AnnotatedNode$SharingDetector.sharedNodes(AnnotatedNode.java:278)
at kodkod.util.nodes.AnnotatedNode.<init>(AnnotatedNode.java:92)
at kodkod.util.nodes.AnnotatedNode.annotate(AnnotatedNode.java:114)
at kodkod.engine.fol2sat.Translator.evaluate(Translator.java:104)
at kodkod.engine.Evaluator.evaluate(Evaluator.java:117)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.rename(A4Solution.java:844)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.rename(A4Solution.java:841)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.rename(A4Solution.java:824)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.<init>(A4Solution.java:330)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.next(A4Solution.java:1031)
at ejdolly.JDolly.hasNext(JDolly.java:192)
at org.testorrery.ForLoopIterator.hasNext(ForLoopIterator.java:40)
at refactoringTest.RefactoringTest.runTests(RefactoringTest.java:141)
at refactoringTest.MainRunner.main(MainRunner.java:83)
我认为这个错误的原因可能与以下描述的相同： CapacityExceededException when reading a very large instance using A4SolutionReader
有什么建议可以避免这个错误吗？
【问题讨论】：
-
你的 -Xms 和 -Xmx 参数是什么？您尝试为此应用增加此参数吗？
-
您在使用该工具和在 java 代码中调用 API 时是否使用相同的求解器？您可能需要检查 A4Option 类
-
嗨，洛伊克。是的，求解器是相同的。不同之处在于该工具会立即告诉我们找到了实例。我们必须单击下一步，下一步，下一步才能找到所有实例。使用 api 时，也会找到实例（超过 60 万个），然后出现内存不足错误，告诉我解决方案无法满足。这是我认为奇怪的。请帮帮我！
标签： java api out-of-memory alloy