diff --git a/jastadd-mquat-solver-ilp/src/main/java/de/tudresden/inf/st/mquat/solving/ilp/ILPExternalSolver.java b/jastadd-mquat-solver-ilp/src/main/java/de/tudresden/inf/st/mquat/solving/ilp/ILPExternalSolver.java index 03385221053416aa341d16c794f42131b57161e4..851e0789566b49a2ef87768363058717cac5e2d3 100644 --- a/jastadd-mquat-solver-ilp/src/main/java/de/tudresden/inf/st/mquat/solving/ilp/ILPExternalSolver.java +++ b/jastadd-mquat-solver-ilp/src/main/java/de/tudresden/inf/st/mquat/solving/ilp/ILPExternalSolver.java @@ -73,6 +73,7 @@ public class ILPExternalSolver extends AbstractILPSolver { protected double solve0(Root model, StopWatch watch, List<IlpVariable> variablesSetToOne) throws SolvingException { // Create temporary files + StopWatch writeOut = StopWatch.start(); try { lp = Files.createTempFile("ilp", null); // solution = Files.createTempFile("solution", null); @@ -88,12 +89,15 @@ public class ILPExternalSolver extends AbstractILPSolver { lp, StandardOpenOption.CREATE, StandardOpenOption.TRUNCATE_EXISTING)) { writer.write(output.toString()); } catch (IOException e) { cleanup(watch); throw new SolvingException("Could not write to lp file", e); } + long secondsNeededToWriteOut = writeOut.time(TimeUnit.SECONDS); + // take twice the time to have buffer to write out solution afterwards + long newTimeout = Math.min(1, timeoutInSeconds - 2 * secondsNeededToWriteOut); // start GLPK to solve the lp file just written, writing out the solution Process process; String command = "glpsol --lp " + lp.toAbsolutePath() + // " -w " + solution.toAbsolutePath() + - " --tmlim " + timeoutInSeconds + + " --tmlim " + newTimeout + " -o " + solutionReadable.toAbsolutePath(); logger.debug("Call: '{}'", command); try { @@ -101,22 +105,23 @@ public class ILPExternalSolver extends AbstractILPSolver { } catch (IOException e) { cleanup(watch); throw new SolvingException("Problem calling glpsol. Is it installed?", e); } boolean finishedInTime; try { - finishedInTime = process.waitFor(timeoutInSeconds, TimeUnit.SECONDS); + finishedInTime = process.waitFor(newTimeout, TimeUnit.SECONDS); } catch (InterruptedException e) { cleanup(watch); throw new SolvingException("Interrupted while waiting for result", e); } if (!finishedInTime) { - // solver already had a timeout, so wait at least 2 seconds longer to let it write a solution file + // solver already had a timeout, so wait some seconds longer to let it write a solution file this.timedOut = true; try { - process.waitFor(2, TimeUnit.SECONDS); + process.waitFor(10, TimeUnit.SECONDS); } catch (InterruptedException ignored) { } // then destroy the process process.destroyForcibly(); - if (!solutionReadable.toFile().exists()) { + if (!solutionReadable.toAbsolutePath().toFile().exists()) { cleanup(watch); - throw new SolvingException("Solving did not finish within " + timeoutValue + " " + timeoutUnit.toString()); + throw new SolvingException("Solving did not finish within " + timeoutValue + " " + timeoutUnit.toString() + + ", file at " + solutionReadable.toAbsolutePath() + " was not written."); } // if there is a solution file, move on and check its content }