aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Oszkar Semerath <semerath@mit.bme.hu>2019-10-01 19:09:53 +0200
committerLibravatar Oszkar Semerath <semerath@mit.bme.hu>2019-10-01 19:09:53 +0200
commit2674956aeb76910420e89afa29ad2441b7b14f96 (patch)
tree504c6cdd85b8027f1d8fbae4939afe1bdfe9713f
parentAlloy upper multiplicity under-approximation with keyword bug fix (diff)
downloadVIATRA-Generator-2674956aeb76910420e89afa29ad2441b7b14f96.tar.gz
VIATRA-Generator-2674956aeb76910420e89afa29ad2441b7b14f96.tar.zst
VIATRA-Generator-2674956aeb76910420e89afa29ad2441b7b14f96.zip
handler refactor
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend23
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 ebbca624..9b4265b9 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 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder 1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2 2
3import com.google.common.util.concurrent.SimpleTimeLimiter
4import com.google.common.util.concurrent.UncheckedTimeoutException
5import edu.mit.csail.sdg.alloy4.A4Reporter 3import edu.mit.csail.sdg.alloy4.A4Reporter
6import edu.mit.csail.sdg.alloy4.Err 4import edu.mit.csail.sdg.alloy4.Err
7import edu.mit.csail.sdg.alloy4.ErrorWarning 5import edu.mit.csail.sdg.alloy4.ErrorWarning
@@ -23,7 +21,11 @@ import java.util.LinkedList
23import java.util.List 21import java.util.List
24import java.util.Map 22import java.util.Map
25import java.util.concurrent.Callable 23import java.util.concurrent.Callable
24import java.util.concurrent.ExecutionException
25import java.util.concurrent.ExecutorService
26import java.util.concurrent.Executors
26import java.util.concurrent.TimeUnit 27import java.util.concurrent.TimeUnit
28import java.util.concurrent.TimeoutException
27import org.eclipse.xtend.lib.annotations.Data 29import org.eclipse.xtend.lib.annotations.Data
28 30
29class AlloySolverException extends Exception{ 31class 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 }