diff options
author | 2018-03-03 02:03:09 -0500 | |
---|---|---|
committer | 2018-03-03 02:03:09 -0500 | |
commit | d2478be3f7ad7ebfe60125aa555388fe79003fe2 (patch) | |
tree | 7d9e16adfdca5c356f21d595f08df28a150a8bb3 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit | |
parent | ViatraSolver reports progress and stops at cancel (diff) | |
download | VIATRA-Generator-d2478be3f7ad7ebfe60125aa555388fe79003fe2.tar.gz VIATRA-Generator-d2478be3f7ad7ebfe60125aa555388fe79003fe2.tar.zst VIATRA-Generator-d2478be3f7ad7ebfe60125aa555388fe79003fe2.zip |
Alloy solver report progress and does not call solver if cancelled
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit')
2 files changed, 26 insertions, 25 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend index 1658a5b8..e664b3b5 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | |||
@@ -49,12 +49,16 @@ class AlloySolver extends LogicReasoner{ | |||
49 | workspace.writeModel(alloyProblem,fileName) | 49 | workspace.writeModel(alloyProblem,fileName) |
50 | } | 50 | } |
51 | val transformationTime = System.currentTimeMillis - transformationStart | 51 | val transformationTime = System.currentTimeMillis - transformationStart |
52 | alloyConfig.progressMonitor.workedForwardTransformation | ||
52 | // Finish: Logic -> Alloy mapping | 53 | // Finish: Logic -> Alloy mapping |
53 | 54 | ||
54 | // Start: Solving Alloy problem | 55 | // Start: Solving Alloy problem |
55 | //val solverStart = System.currentTimeMillis | 56 | //val solverStart = System.currentTimeMillis |
56 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) | 57 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) |
58 | alloyConfig.progressMonitor.workedSearchFinished | ||
59 | |||
57 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | 60 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) |
61 | alloyConfig.progressMonitor.workedBackwardTransformationFinished | ||
58 | //val solverFinish = System.currentTimeMillis-solverStart | 62 | //val solverFinish = System.currentTimeMillis-solverStart |
59 | // Finish: Solving Alloy problem | 63 | // Finish: Solving Alloy problem |
60 | 64 | ||
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 51cc8c42..ebbca624 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 | |||
@@ -24,9 +24,7 @@ import java.util.List | |||
24 | import java.util.Map | 24 | import java.util.Map |
25 | import java.util.concurrent.Callable | 25 | import java.util.concurrent.Callable |
26 | import java.util.concurrent.TimeUnit | 26 | import java.util.concurrent.TimeUnit |
27 | import org.eclipse.emf.common.CommonPlugin | ||
28 | import org.eclipse.xtend.lib.annotations.Data | 27 | import org.eclipse.xtend.lib.annotations.Data |
29 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
30 | 28 | ||
31 | class AlloySolverException extends Exception{ | 29 | class AlloySolverException extends Exception{ |
32 | new(String s) { super(s) } | 30 | new(String s) { super(s) } |
@@ -49,12 +47,8 @@ class AlloyHandler { | |||
49 | //val fileName = "problem.als" | 47 | //val fileName = "problem.als" |
50 | 48 | ||
51 | public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { | 49 | public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { |
52 | val writeToFile = ( | ||
53 | configuration.documentationLevel===DocumentationLevel::NORMAL || | ||
54 | configuration.documentationLevel===DocumentationLevel::FULL) | ||
55 | 50 | ||
56 | //Prepare | 51 | //Prepare |
57 | |||
58 | val warnings = new LinkedList<String> | 52 | val warnings = new LinkedList<String> |
59 | val debugs = new LinkedList<String> | 53 | val debugs = new LinkedList<String> |
60 | val runtime = new ArrayList<Long> | 54 | val runtime = new ArrayList<Long> |
@@ -73,7 +67,7 @@ class AlloyHandler { | |||
73 | it.solverDirectory = configuration.solverPath | 67 | it.solverDirectory = configuration.solverPath |
74 | } | 68 | } |
75 | //it.inferPartialInstance | 69 | //it.inferPartialInstance |
76 | it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString | 70 | //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString |
77 | ] | 71 | ] |
78 | 72 | ||
79 | // Transform | 73 | // Transform |
@@ -94,7 +88,7 @@ class AlloyHandler { | |||
94 | // Finish: Alloy -> Kodkod | 88 | // Finish: Alloy -> Kodkod |
95 | 89 | ||
96 | val limiter = new SimpleTimeLimiter | 90 | val limiter = new SimpleTimeLimiter |
97 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration.solutionScope.numberOfRequiredSolution) | 91 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) |
98 | var List<Pair<A4Solution, Long>> answers | 92 | var List<Pair<A4Solution, Long>> answers |
99 | var boolean finished | 93 | var boolean finished |
100 | if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { | 94 | if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { |
@@ -156,7 +150,7 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | |||
156 | 150 | ||
157 | val Command command | 151 | val Command command |
158 | val CompModule compModule | 152 | val CompModule compModule |
159 | val int numberOfRequiredSolution | 153 | val AlloySolverConfiguration configuration |
160 | 154 | ||
161 | val List<Pair<A4Solution,Long>> answers = new LinkedList() | 155 | val List<Pair<A4Solution,Long>> answers = new LinkedList() |
162 | 156 | ||
@@ -166,7 +160,7 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | |||
166 | A4Options options, | 160 | A4Options options, |
167 | Command command, | 161 | Command command, |
168 | CompModule compModule, | 162 | CompModule compModule, |
169 | int numberOfRequiredSolution) | 163 | AlloySolverConfiguration configuration) |
170 | { | 164 | { |
171 | this.warnings = warnings | 165 | this.warnings = warnings |
172 | this.debugs = debugs | 166 | this.debugs = debugs |
@@ -174,7 +168,7 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | |||
174 | this.options = options | 168 | this.options = options |
175 | this.command = command | 169 | this.command = command |
176 | this.compModule = compModule | 170 | this.compModule = compModule |
177 | this.numberOfRequiredSolution = numberOfRequiredSolution | 171 | this.configuration = configuration |
178 | } | 172 | } |
179 | 173 | ||
180 | override call() throws Exception { | 174 | override call() throws Exception { |
@@ -183,19 +177,22 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | |||
183 | // Start: Execute | 177 | // Start: Execute |
184 | var A4Solution lastAnswer = null | 178 | var A4Solution lastAnswer = null |
185 | try { | 179 | try { |
186 | do{ | 180 | if(!configuration.progressMonitor.isCancelled) { |
187 | if(lastAnswer == null) { | 181 | do{ |
188 | lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | 182 | if(lastAnswer == null) { |
189 | } else { | 183 | lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) |
190 | lastAnswer = lastAnswer.next | 184 | } else { |
191 | } | 185 | lastAnswer = lastAnswer.next |
186 | } | ||
187 | configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) | ||
188 | |||
189 | val runtime = System.currentTimeMillis -startTime | ||
190 | synchronized(this) { | ||
191 | answers += (lastAnswer->runtime) | ||
192 | } | ||
193 | } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) | ||
192 | 194 | ||
193 | val runtime = System.currentTimeMillis -startTime | 195 | } |
194 | synchronized(this) { | ||
195 | answers += (lastAnswer->runtime) | ||
196 | } | ||
197 | } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers)) | ||
198 | |||
199 | }catch(Exception e) { | 196 | }catch(Exception e) { |
200 | warnings +=e.message | 197 | warnings +=e.message |
201 | } | 198 | } |
@@ -204,8 +201,8 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | |||
204 | } | 201 | } |
205 | 202 | ||
206 | def hasEnoughSolution(List<?> answers) { | 203 | def hasEnoughSolution(List<?> answers) { |
207 | if(numberOfRequiredSolution < 0) return false | 204 | if(configuration.solutionScope.numberOfRequiredSolution < 0) return false |
208 | else return answers.size() == numberOfRequiredSolution | 205 | else return answers.size() == configuration.solutionScope.numberOfRequiredSolution |
209 | } | 206 | } |
210 | 207 | ||
211 | public def getPartialAnswers() { | 208 | public def getPartialAnswers() { |