diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | 23 |
1 files changed, 17 insertions, 6 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend index 033ced04..ed2ef6b7 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | |||
@@ -1,7 +1,5 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | 1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder |
2 | 2 | ||
3 | import com.google.common.util.concurrent.SimpleTimeLimiter | ||
4 | import com.google.common.util.concurrent.UncheckedTimeoutException | ||
5 | import edu.mit.csail.sdg.alloy4.A4Reporter | 3 | import edu.mit.csail.sdg.alloy4.A4Reporter |
6 | import edu.mit.csail.sdg.alloy4.Err | 4 | import edu.mit.csail.sdg.alloy4.Err |
7 | import edu.mit.csail.sdg.alloy4.ErrorWarning | 5 | import edu.mit.csail.sdg.alloy4.ErrorWarning |
@@ -23,7 +21,11 @@ import java.util.LinkedList | |||
23 | import java.util.List | 21 | import java.util.List |
24 | import java.util.Map | 22 | import java.util.Map |
25 | import java.util.concurrent.Callable | 23 | import java.util.concurrent.Callable |
24 | import java.util.concurrent.ExecutionException | ||
25 | import java.util.concurrent.ExecutorService | ||
26 | import java.util.concurrent.Executors | ||
26 | import java.util.concurrent.TimeUnit | 27 | import java.util.concurrent.TimeUnit |
28 | import java.util.concurrent.TimeoutException | ||
27 | import org.eclipse.xtend.lib.annotations.Data | 29 | import org.eclipse.xtend.lib.annotations.Data |
28 | 30 | ||
29 | class AlloySolverException extends Exception{ | 31 | class AlloySolverException extends Exception{ |
@@ -46,7 +48,7 @@ class AlloyHandler { | |||
46 | 48 | ||
47 | //val fileName = "problem.als" | 49 | //val fileName = "problem.als" |
48 | 50 | ||
49 | public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { | 51 | def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { |
50 | 52 | ||
51 | //Prepare | 53 | //Prepare |
52 | val warnings = new LinkedList<String> | 54 | val warnings = new LinkedList<String> |
@@ -87,7 +89,6 @@ class AlloyHandler { | |||
87 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | 89 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart |
88 | // Finish: Alloy -> Kodkod | 90 | // Finish: Alloy -> Kodkod |
89 | 91 | ||
90 | val limiter = new SimpleTimeLimiter | ||
91 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) | 92 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) |
92 | var List<Pair<A4Solution, Long>> answers | 93 | var List<Pair<A4Solution, Long>> answers |
93 | var boolean finished | 94 | var boolean finished |
@@ -95,10 +96,20 @@ class AlloyHandler { | |||
95 | answers = callable.call | 96 | answers = callable.call |
96 | finished = true | 97 | finished = true |
97 | } else { | 98 | } else { |
99 | val ExecutorService executor = Executors.newCachedThreadPool(); | ||
100 | val future = executor.submit(callable) | ||
98 | try{ | 101 | try{ |
99 | answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) | 102 | answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS) |
100 | finished = true | 103 | finished = true |
101 | } catch (UncheckedTimeoutException e) { | 104 | } catch (TimeoutException ex) { |
105 | // handle the timeout | ||
106 | } catch (InterruptedException e) { | ||
107 | // handle the interrupts | ||
108 | } catch (ExecutionException e) { | ||
109 | // handle other exceptions | ||
110 | } finally { | ||
111 | future.cancel(true); | ||
112 | |||
102 | answers = callable.partialAnswers | 113 | answers = callable.partialAnswers |
103 | finished = false | 114 | finished = false |
104 | } | 115 | } |