diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-07-02 23:34:27 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-07-02 23:34:27 +0200 |
commit | f00ce77fdc3a1417ddfd833f122b64ecef80d7d6 (patch) | |
tree | 2a26b61a43576f58ed4c35680bd47fa3c15df3d8 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | |
parent | Multiple model with interpretations (diff) | |
download | VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.tar.gz VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.tar.zst VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.zip |
Alloy implementation of multiple model generation
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | 85 |
1 files changed, 50 insertions, 35 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 7dfc3161..d0c7d320 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 | |||
@@ -3,8 +3,10 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper | 3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper |
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler | 4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler |
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation | 5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation |
6 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes | ||
6 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper | 7 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper |
7 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace | 8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace |
9 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes | ||
8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution | 10 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution |
9 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated | 11 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated |
10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage | 12 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage |
@@ -14,9 +16,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | |||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
16 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
17 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes | ||
18 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes | ||
19 | import org.eclipse.emf.common.util.URI | ||
20 | 19 | ||
21 | class AlloySolver extends LogicReasoner{ | 20 | class AlloySolver extends LogicReasoner{ |
22 | 21 | ||
@@ -33,40 +32,56 @@ class AlloySolver extends LogicReasoner{ | |||
33 | val fileName = "problem.als" | 32 | val fileName = "problem.als" |
34 | 33 | ||
35 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | 34 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { |
35 | val alloyConfig = configuration.asConfig | ||
36 | |||
37 | // Start: Logic -> Alloy mapping | ||
38 | val transformationStart = System.currentTimeMillis | ||
39 | val result = forwardMapper.transformProblem(problem,alloyConfig) | ||
40 | val alloyProblem = result.output | ||
41 | val forwardTrace = result.trace | ||
42 | |||
43 | var String fileURI = null; | ||
44 | var String alloyCode = null; | ||
45 | if(alloyConfig.writeToFile) { | ||
46 | fileURI = workspace.writeModel(alloyProblem,fileName).toFileString | ||
47 | } else { | ||
48 | alloyCode = workspace.writeModelToString(alloyProblem,fileName) | ||
49 | } | ||
50 | val transformationTime = System.currentTimeMillis - transformationStart | ||
51 | // Finish: Logic -> Alloy mapping | ||
52 | |||
53 | |||
54 | // Start: Solving Alloy problem | ||
55 | val solverStart = System.currentTimeMillis | ||
56 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode) | ||
57 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | ||
58 | val solverFinish = System.currentTimeMillis-solverStart | ||
59 | // Finish: Solving Alloy problem | ||
60 | |||
61 | if(alloyConfig.writeToFile) workspace.deactivateModel(fileName) | ||
62 | |||
63 | return logicResult | ||
64 | } | ||
65 | |||
66 | def asConfig(LogicSolverConfiguration configuration) { | ||
36 | if(configuration instanceof AlloySolverConfiguration) { | 67 | if(configuration instanceof AlloySolverConfiguration) { |
37 | val transformationStart = System.currentTimeMillis | 68 | return configuration |
38 | val result = forwardMapper.transformProblem(problem,configuration) | 69 | } else { |
39 | val alloyProblem = result.output | 70 | throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''') |
40 | 71 | } | |
41 | /*val x = alloyProblem.eAllContents.filter(ALSFunctionCall).filter[it.referredDefinition == null].toList | ||
42 | println(x)*/ | ||
43 | val forwardTrace = result.trace | ||
44 | |||
45 | var String fileURI = null; | ||
46 | var String alloyCode = null; | ||
47 | if(configuration.writeToFile) { | ||
48 | fileURI = workspace.writeModel(alloyProblem,fileName).toFileString | ||
49 | } else { | ||
50 | alloyCode = workspace.writeModelToString(alloyProblem,fileName) | ||
51 | } | ||
52 | |||
53 | //val alloyCode = workspace.readText(fileName) | ||
54 | //val FunctionWithTimeout<MonitoredAlloySolution> call = new FunctionWithTimeout[] | ||
55 | |||
56 | val transformationTime = System.currentTimeMillis - transformationStart | ||
57 | val result2 = handler.callSolver(alloyProblem,workspace,configuration,fileURI,alloyCode) | ||
58 | workspace.deactivateModel(fileName) | ||
59 | val logicResult = backwardMapper.transformOutput(problem,result2,forwardTrace,transformationTime) | ||
60 | return logicResult | ||
61 | } else throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''') | ||
62 | } | 72 | } |
63 | 73 | ||
64 | override getInterpretation(ModelResult modelResult) { | 74 | override getInterpretations(ModelResult modelResult) { |
65 | return new AlloyModelInterpretation( | 75 | val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] |
66 | new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, | 76 | val res = answers.map [ |
67 | (modelResult.representation as MonitoredAlloySolution).solution, | 77 | new AlloyModelInterpretation( |
68 | forwardMapper, | 78 | new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, |
69 | modelResult.trace as Logic2AlloyLanguageMapperTrace | 79 | it, |
70 | ); | 80 | forwardMapper, |
81 | modelResult.trace as Logic2AlloyLanguageMapperTrace | ||
82 | ) | ||
83 | ] | ||
84 | |||
85 | return res | ||
71 | } | 86 | } |
72 | } \ No newline at end of file | 87 | } \ No newline at end of file |