OutOfMemoryError when using alloy api for Java

Question

I have an Alloy model that, when running in Alloy tool (alloy4.2.jar), generates instances without any problems. But, when I use this same model as input to the Alloy api in Java in order to get all of these instances, one by one, an out of memory error is generated after a while (many instances are captured before the error appears).

The error occurs exactly in the if command located just after the try command (corresponding to JDolly.java:192 in the print stack trace further) in the code below:

@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;
    }

The print stack trace of this error is:

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)

I think the reason of this error can be the same as the one described in: CapacityExceededException when reading a very large instance using A4SolutionReader

Any suggestions in order to avoid this error?

What is your -Xms and -Xmx parameters? You try to increase this parameters for this application? — Slava Vedenin, Feb 10 '16 at 21:35
Are you using the same solver when you use the tool and when you call the API in your java code ? You might want to check the A4Option class — Loïc Gammaitoni, Feb 23 '16 at 11:03
Hi, Loic. Yes, the solver is the same. The difference is that the tool immediately tell us that instances are found. And we have to click next, next, next in order to find all of the instances . When the api is used, instances are also found (more than 600 thousands) and after this, the outofmemory error appears telling me that the solution is unsatisfiable. This is what i consider strange. Please, help me! — Tarciana, Feb 26 '16 at 16:05

score 0 · Answer 1 · answered Mar 01 '16 at 07:12

0

Solutions (i.e. instances of the A4Solution class) in Alloy are organized in a linked list fashion, meaning that a call to next will essentially compute the next solution based on the given one and put it into the list by chaining it to the current solution.

If you are generating a lot of solutions, while all of them are being stored, eventually the out of memory exception is bound to be thrown.

You should probably check that you are not retaining references to all the solutions (or just the first one) and thus preventing them being garbage collected.

answered Mar 01 '16 at 07:12

ivcha

463
5
15

This is not the case. I made a test to only get each A4Solution class (without doing any storage or manipulation) to see if the error would still happen, and, as soon as the A4Solution is generated, the error occurs. The point is that the object instance is already provided (A4Solution is generated) and printed in my program, but after this, the error occurs. I think the reason could be similar to the reason of the error described in Loïc's question in: [link](http://stackoverflow.com/questions/35703242/capacityexceededexception-when-reading-a-very-large-instance-using-a4solutionrea) – Tarciana Mar 21 '16 at 18:33
Can you point us to your tests that exhibit this? – ivcha Mar 21 '16 at 19:44
Hi @kaptoxic, thank you for the feedback. I edited the question by adding the code where the error occurs and the corresponding printstack trace. Thank you for the attention. – Tarciana Mar 22 '16 at 00:25
Can you extract a piece of test code that exhibits the issue? Something that we can try to run to see if we can get the bug. – ivcha Mar 22 '16 at 03:57
i did not make any specific test. The bug appears when i iterate over the instances (generated by the command CompUtil.parseEverything_fromFile(null, null,alloyTheory), which returns a module object passed as parameter in "TranslateAlloyToKodkod.execute_command(null, moduleObject.getAllReachableSigs(), moduleObject.getAllCommands().get(0), options);") through the loop "for (List cus : generator)", where generator represents an A4Solution through its CompilationUnits. – Tarciana Mar 28 '16 at 14:24
Please make a test (and post a link here) so that people can run it and debug it. Thanks. – ivcha Mar 28 '16 at 14:37

OutOfMemoryError when using alloy api for Java

1 Answers1