diff options
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend')
-rw-r--r-- | Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | 91 |
1 files changed, 91 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend new file mode 100644 index 00000000..9cfa7391 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | |||
@@ -0,0 +1,91 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper | ||
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler | ||
6 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation | ||
7 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper | ||
8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace | ||
9 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes | ||
10 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated | ||
11 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
19 | |||
20 | class AlloySolver extends LogicReasoner{ | ||
21 | |||
22 | new() { | ||
23 | AlloyLanguagePackage.eINSTANCE.eClass | ||
24 | val x = new AlloyLanguageStandaloneSetupGenerated | ||
25 | x.createInjectorAndDoEMFRegistration | ||
26 | } | ||
27 | |||
28 | val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes) | ||
29 | val AlloyHandler handler = new AlloyHandler | ||
30 | val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper | ||
31 | |||
32 | val fileName = "problem.als" | ||
33 | |||
34 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | ||
35 | val alloyConfig = configuration.asConfig | ||
36 | val writeFile = ( | ||
37 | configuration.documentationLevel===DocumentationLevel::NORMAL || | ||
38 | configuration.documentationLevel===DocumentationLevel::FULL) | ||
39 | |||
40 | // Start: Logic -> Alloy mapping | ||
41 | val transformationStart = System.currentTimeMillis | ||
42 | val result = forwardMapper.transformProblem(problem,alloyConfig) | ||
43 | val alloyProblem = result.output | ||
44 | val forwardTrace = result.trace | ||
45 | |||
46 | //var String fileURI = null; | ||
47 | var String alloyCode = workspace.writeModelToString(alloyProblem,fileName) | ||
48 | if(writeFile) { | ||
49 | workspace.writeModel(alloyProblem,fileName) | ||
50 | } | ||
51 | val transformationTime = System.currentTimeMillis - transformationStart | ||
52 | alloyConfig.progressMonitor.workedForwardTransformation | ||
53 | // Finish: Logic -> Alloy mapping | ||
54 | |||
55 | // Start: Solving Alloy problem | ||
56 | //val solverStart = System.currentTimeMillis | ||
57 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) | ||
58 | alloyConfig.progressMonitor.workedSearchFinished | ||
59 | |||
60 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | ||
61 | alloyConfig.progressMonitor.workedBackwardTransformationFinished | ||
62 | //val solverFinish = System.currentTimeMillis-solverStart | ||
63 | // Finish: Solving Alloy problem | ||
64 | |||
65 | //logicResult.statistics = | ||
66 | |||
67 | return logicResult | ||
68 | } | ||
69 | |||
70 | def asConfig(LogicSolverConfiguration configuration) { | ||
71 | if(configuration instanceof AlloySolverConfiguration) { | ||
72 | return configuration | ||
73 | } else { | ||
74 | throw new IllegalArgumentException('''The configuration has to be an «AlloySolverConfiguration.simpleName»!''') | ||
75 | } | ||
76 | } | ||
77 | |||
78 | override getInterpretations(ModelResult modelResult) { | ||
79 | //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] | ||
80 | val sols = modelResult.representation// as List<A4Solution> | ||
81 | //val res = answers.map | ||
82 | sols.map[ | ||
83 | new AlloyModelInterpretation( | ||
84 | forwardMapper.typeMapper.typeInterpreter, | ||
85 | it as A4Solution, | ||
86 | forwardMapper, | ||
87 | modelResult.trace as Logic2AlloyLanguageMapperTrace | ||
88 | ) | ||
89 | ] | ||
90 | } | ||
91 | } \ No newline at end of file | ||