diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-07-05 15:00:37 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-07-05 15:00:37 +0200 |
commit | 53cf6e18913a9f0c7717ff84eedd56941944367a (patch) | |
tree | 09534b4fb4c1b3cb6949a403b2c3f196a21d060b /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder | |
parent | Added a try-catch to detect if a query cannot be translated (because, (diff) | |
download | VIATRA-Generator-53cf6e18913a9f0c7717ff84eedd56941944367a.tar.gz VIATRA-Generator-53cf6e18913a9f0c7717ff84eedd56941944367a.tar.zst VIATRA-Generator-53cf6e18913a9f0c7717ff84eedd56941944367a.zip |
Adding multiple model generation support for the alloy solver.
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder')
2 files changed, 4 insertions, 5 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend index 7db9e0ea..2efd6b29 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | |||
@@ -9,7 +9,7 @@ class Alloy2LogicMapper { | |||
9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { | 9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { |
10 | val models = monitoredAlloySolution.aswers.map[it.key].toList | 10 | val models = monitoredAlloySolution.aswers.map[it.key].toList |
11 | 11 | ||
12 | if(monitoredAlloySolution.finishedBeforeTimeout) { | 12 | if(!monitoredAlloySolution.finishedBeforeTimeout) { |
13 | return createInsuficientResourcesResult => [ | 13 | return createInsuficientResourcesResult => [ |
14 | it.problem = problem | 14 | it.problem = problem |
15 | it.representation += models | 15 | it.representation += models |
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 17220776..c1f2ec4c 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 | |||
@@ -191,10 +191,9 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | |||
191 | 191 | ||
192 | val runtime = System.currentTimeMillis -startTime | 192 | val runtime = System.currentTimeMillis -startTime |
193 | synchronized(this) { | 193 | synchronized(this) { |
194 | answers += lastAnswer->runtime | 194 | answers += (lastAnswer->runtime) |
195 | } | 195 | } |
196 | println( answers.size ) | 196 | } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers)) |
197 | } while(lastAnswer.satisfiable != false && hasEnoughSolution(answers)) | ||
198 | 197 | ||
199 | }catch(Exception e) { | 198 | }catch(Exception e) { |
200 | warnings +=e.message | 199 | warnings +=e.message |
@@ -205,7 +204,7 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | |||
205 | 204 | ||
206 | def hasEnoughSolution(List<?> answers) { | 205 | def hasEnoughSolution(List<?> answers) { |
207 | if(numberOfRequiredSolution < 0) return false | 206 | if(numberOfRequiredSolution < 0) return false |
208 | else return answers.size < numberOfRequiredSolution | 207 | else return answers.size() == numberOfRequiredSolution |
209 | } | 208 | } |
210 | 209 | ||
211 | public def getPartialAnswers() { | 210 | public def getPartialAnswers() { |