diff options
author | 2017-07-05 15:00:37 +0200 | |
---|---|---|
committer | 2017-07-05 15:00:37 +0200 | |
commit | 53cf6e18913a9f0c7717ff84eedd56941944367a (patch) | |
tree | 09534b4fb4c1b3cb6949a403b2c3f196a21d060b /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src | |
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')
3 files changed, 11 insertions, 10 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 d0c7d320..65539155 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 | |||
@@ -16,6 +16,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | |||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
19 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
20 | import java.util.List | ||
19 | 21 | ||
20 | class AlloySolver extends LogicReasoner{ | 22 | class AlloySolver extends LogicReasoner{ |
21 | 23 | ||
@@ -72,16 +74,16 @@ class AlloySolver extends LogicReasoner{ | |||
72 | } | 74 | } |
73 | 75 | ||
74 | override getInterpretations(ModelResult modelResult) { | 76 | override getInterpretations(ModelResult modelResult) { |
75 | val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] | 77 | //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] |
76 | val res = answers.map [ | 78 | val sols = modelResult.representation// as List<A4Solution> |
79 | //val res = answers.map | ||
80 | sols.map[ | ||
77 | new AlloyModelInterpretation( | 81 | new AlloyModelInterpretation( |
78 | new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, | 82 | new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, |
79 | it, | 83 | it as A4Solution, |
80 | forwardMapper, | 84 | forwardMapper, |
81 | modelResult.trace as Logic2AlloyLanguageMapperTrace | 85 | modelResult.trace as Logic2AlloyLanguageMapperTrace |
82 | ) | 86 | ) |
83 | ] | 87 | ] |
84 | |||
85 | return res | ||
86 | } | 88 | } |
87 | } \ No newline at end of file | 89 | } \ No newline at end of file |
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() { |