diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | 36 |
1 files changed, 30 insertions, 6 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java index 0105d985..4fef6448 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | |||
@@ -42,8 +42,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
42 | private Map<Object, String> varMap; | 42 | private Map<Object, String> varMap; |
43 | private Map<String, String> curVar2Decl; | 43 | private Map<String, String> curVar2Decl; |
44 | 44 | ||
45 | private final int TIMEOUT_DOCKER = 5; | 45 | private final int TIMEOUT_DOCKER = 5000; |
46 | private final int TIMEOUT_LOCAL = 2; | 46 | private final int TIMEOUT_LOCAL = 20000; |
47 | 47 | ||
48 | public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { | 48 | public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { |
49 | this.useDocker = useDocker; | 49 | this.useDocker = useDocker; |
@@ -68,14 +68,26 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
68 | } | 68 | } |
69 | 69 | ||
70 | private Process runProcess(List<String> cmd, int timeout) throws IOException, InterruptedException { | 70 | private Process runProcess(List<String> cmd, int timeout) throws IOException, InterruptedException { |
71 | String s = String.join(" ", cmd); | 71 | // String s = String.join(" ", cmd); |
72 | Process p = Runtime.getRuntime().exec(s); | 72 | // Process p = Runtime.getRuntime().exec(s); |
73 | Process p = (new ProcessBuilder(cmd)).start(); | ||
73 | // p.waitFor(); | 74 | // p.waitFor(); |
74 | //TODO timeout if needed | 75 | //TODO timeout if needed |
75 | if (!p.waitFor(timeout, TimeUnit.SECONDS)) { | 76 | long startTime = System.nanoTime(); |
77 | if (!p.waitFor(timeout, TimeUnit.MILLISECONDS)) { | ||
76 | p.destroy(); | 78 | p.destroy(); |
79 | if (p.isAlive()) { | ||
80 | p.destroyForcibly(); | ||
81 | if (p.isAlive()) { | ||
82 | //Platform-specific but fine for now | ||
83 | Runtime.getRuntime().exec("killall -9 dreal").waitFor(); | ||
84 | if (p.isAlive()) System.out.println("dreal process not closed"); | ||
85 | } | ||
86 | } | ||
77 | return null; | 87 | return null; |
78 | } | 88 | } |
89 | double duration = (double) (System.nanoTime() - startTime) / 1000000000; | ||
90 | System.out.println("Dur = " + duration + " : "); | ||
79 | return p; | 91 | return p; |
80 | } | 92 | } |
81 | 93 | ||
@@ -371,18 +383,30 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
371 | if (outputProcess != null) { | 383 | if (outputProcess != null) { |
372 | outputs = getProcessOutput(outputProcess); | 384 | outputs = getProcessOutput(outputProcess); |
373 | result = getDrealResult(outputProcess.exitValue(), outputs); | 385 | result = getDrealResult(outputProcess.exitValue(), outputs); |
386 | // } else { | ||
387 | // System.err.print("Timeout, RETRYING..."); | ||
388 | // if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false); | ||
389 | // else outputProcess = callDrealLocal(numProbContent, false); | ||
390 | // if (outputProcess != null) { | ||
391 | // outputs = getProcessOutput(outputProcess); | ||
392 | // result = getDrealResult(outputProcess.exitValue(), outputs); | ||
393 | // System.out.println("pass"); | ||
394 | // } else { | ||
395 | // System.out.println("fail"); | ||
396 | // } | ||
374 | } | 397 | } |
375 | endSolvingProblem = System.nanoTime()-startSolvingProblem; | 398 | endSolvingProblem = System.nanoTime()-startSolvingProblem; |
376 | 399 | ||
377 | //DEBUG - Print things | 400 | //DEBUG - Print things |
378 | if (outputProcess == null) { | 401 | if (outputProcess == null) { |
402 | |||
379 | System.err.println("TIMEOUT"); | 403 | System.err.println("TIMEOUT"); |
380 | // printOutput(numProbContent); | 404 | // printOutput(numProbContent); |
381 | } | 405 | } |
382 | 406 | ||
383 | // printOutput(numProbContent); | 407 | // printOutput(numProbContent); |
384 | // if (outputs != null) printOutput(outputs.get(0)); | 408 | // if (outputs != null) printOutput(outputs.get(0)); |
385 | // System.out.println(result); | 409 | System.out.println(result); |
386 | // END DEBUG | 410 | // END DEBUG |
387 | 411 | ||
388 | return result; | 412 | return result; |