diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | 111 |
1 files changed, 93 insertions, 18 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 6bac4130..17220776 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 | |||
@@ -21,6 +21,11 @@ import org.eclipse.emf.common.CommonPlugin | |||
21 | import java.util.ArrayList | 21 | import java.util.ArrayList |
22 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | 22 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument |
23 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 23 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration |
24 | import com.google.common.util.concurrent.SimpleTimeLimiter | ||
25 | import java.util.concurrent.Callable | ||
26 | import java.util.concurrent.TimeUnit | ||
27 | import com.google.common.util.concurrent.UncheckedTimeoutException | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
24 | 29 | ||
25 | class AlloySolverException extends Exception{ | 30 | class AlloySolverException extends Exception{ |
26 | new(String s) { super(s) } | 31 | new(String s) { super(s) } |
@@ -34,9 +39,8 @@ class AlloySolverException extends Exception{ | |||
34 | List<String> warnings | 39 | List<String> warnings |
35 | List<String> debugs | 40 | List<String> debugs |
36 | long kodkodTime | 41 | long kodkodTime |
37 | long runtimeTime | 42 | val List<Pair<A4Solution, Long>> aswers |
38 | 43 | val boolean finishedBeforeTimeout | |
39 | A4Solution solution | ||
40 | } | 44 | } |
41 | 45 | ||
42 | class AlloyHandler { | 46 | class AlloyHandler { |
@@ -63,6 +67,7 @@ class AlloyHandler { | |||
63 | if(configuration.solver.externalSolver) { | 67 | if(configuration.solver.externalSolver) { |
64 | it.solverDirectory = configuration.solverPath | 68 | it.solverDirectory = configuration.solverPath |
65 | } | 69 | } |
70 | //it.inferPartialInstance | ||
66 | it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString | 71 | it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString |
67 | ] | 72 | ] |
68 | 73 | ||
@@ -70,8 +75,8 @@ class AlloyHandler { | |||
70 | var Command command = null; | 75 | var Command command = null; |
71 | var CompModule compModule = null | 76 | var CompModule compModule = null |
72 | 77 | ||
78 | // Start: Alloy -> Kodkod | ||
73 | val kodkodTransformStart = System.currentTimeMillis(); | 79 | val kodkodTransformStart = System.currentTimeMillis(); |
74 | |||
75 | try { | 80 | try { |
76 | if(configuration.writeToFile) { | 81 | if(configuration.writeToFile) { |
77 | compModule = CompUtil.parseEverything_fromFile(reporter,null,path) | 82 | compModule = CompUtil.parseEverything_fromFile(reporter,null,path) |
@@ -85,23 +90,26 @@ class AlloyHandler { | |||
85 | throw new AlloySolverException(e.message,warnings,e) | 90 | throw new AlloySolverException(e.message,warnings,e) |
86 | } | 91 | } |
87 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | 92 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart |
93 | // Finish: Alloy -> Kodkod | ||
88 | 94 | ||
89 | //Execute | 95 | val limiter = new SimpleTimeLimiter |
90 | var A4Solution answer = null; | 96 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration.solutionScope.numberOfRequiredSolution) |
91 | try { | 97 | var List<Pair<A4Solution, Long>> answers |
92 | answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | 98 | var boolean finished |
93 | }catch(Exception e) { | 99 | if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { |
94 | warnings +=e.message | 100 | answers = callable.call |
95 | } | 101 | finished = true |
96 | |||
97 | var long runtimeFromAnswer; | ||
98 | if(runtime.empty) { | ||
99 | runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish) | ||
100 | } else { | 102 | } else { |
101 | runtimeFromAnswer = runtime.head | 103 | try{ |
104 | answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) | ||
105 | finished = true | ||
106 | } catch (UncheckedTimeoutException e) { | ||
107 | answers = callable.partialAnswers | ||
108 | finished = false | ||
109 | } | ||
102 | } | 110 | } |
103 | 111 | ||
104 | return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer) | 112 | new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) |
105 | } | 113 | } |
106 | 114 | ||
107 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap | 115 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap |
@@ -138,6 +146,73 @@ class AlloyHandler { | |||
138 | } | 146 | } |
139 | } | 147 | } |
140 | 148 | ||
149 | class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | ||
150 | |||
151 | val List<String> warnings | ||
152 | val List<String> debugs | ||
153 | val A4Reporter reporter | ||
154 | val A4Options options | ||
155 | |||
156 | val Command command | ||
157 | val CompModule compModule | ||
158 | val int numberOfRequiredSolution | ||
159 | |||
160 | val List<Pair<A4Solution,Long>> answers = new LinkedList() | ||
161 | |||
162 | new(List<String> warnings, | ||
163 | List<String> debugs, | ||
164 | A4Reporter reporter, | ||
165 | A4Options options, | ||
166 | Command command, | ||
167 | CompModule compModule, | ||
168 | int numberOfRequiredSolution) | ||
169 | { | ||
170 | this.warnings = warnings | ||
171 | this.debugs = debugs | ||
172 | this.reporter = reporter | ||
173 | this.options = options | ||
174 | this.command = command | ||
175 | this.compModule = compModule | ||
176 | this.numberOfRequiredSolution = numberOfRequiredSolution | ||
177 | } | ||
178 | |||
179 | override call() throws Exception { | ||
180 | val startTime = System.currentTimeMillis | ||
181 | |||
182 | // Start: Execute | ||
183 | var A4Solution lastAnswer = null | ||
184 | try { | ||
185 | do{ | ||
186 | if(lastAnswer == null) { | ||
187 | lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | ||
188 | } else { | ||
189 | lastAnswer = lastAnswer.next | ||
190 | } | ||
191 | |||
192 | val runtime = System.currentTimeMillis -startTime | ||
193 | synchronized(this) { | ||
194 | answers += lastAnswer->runtime | ||
195 | } | ||
196 | println( answers.size ) | ||
197 | } while(lastAnswer.satisfiable != false && hasEnoughSolution(answers)) | ||
198 | |||
199 | }catch(Exception e) { | ||
200 | warnings +=e.message | ||
201 | } | ||
202 | // Finish: execute | ||
203 | return answers | ||
204 | } | ||
205 | |||
206 | def hasEnoughSolution(List<?> answers) { | ||
207 | if(numberOfRequiredSolution < 0) return false | ||
208 | else return answers.size < numberOfRequiredSolution | ||
209 | } | ||
210 | |||
211 | public def getPartialAnswers() { | ||
212 | return answers | ||
213 | } | ||
214 | } | ||
215 | |||
141 | @Data class SolverConfiguration { | 216 | @Data class SolverConfiguration { |
142 | AlloyBackendSolver backedSolver | 217 | AlloyBackendSolver backedSolver |
143 | String path | 218 | String path |