diff options
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 | 72 |
1 files changed, 72 insertions, 0 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 new file mode 100644 index 00000000..7dfc3161 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | |||
@@ -0,0 +1,72 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper | ||
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler | ||
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation | ||
6 | 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.MonitoredAlloySolution | ||
9 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated | ||
10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
16 | 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 | |||
21 | class AlloySolver extends LogicReasoner{ | ||
22 | |||
23 | new() { | ||
24 | AlloyLanguagePackage.eINSTANCE.eClass | ||
25 | val x = new AlloyLanguageStandaloneSetupGenerated | ||
26 | x.createInjectorAndDoEMFRegistration | ||
27 | } | ||
28 | |||
29 | val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes) | ||
30 | val AlloyHandler handler = new AlloyHandler | ||
31 | val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper | ||
32 | |||
33 | val fileName = "problem.als" | ||
34 | |||
35 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | ||
36 | if(configuration instanceof AlloySolverConfiguration) { | ||
37 | val transformationStart = System.currentTimeMillis | ||
38 | val result = forwardMapper.transformProblem(problem,configuration) | ||
39 | val alloyProblem = result.output | ||
40 | |||
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 | } | ||
63 | |||
64 | override getInterpretation(ModelResult modelResult) { | ||
65 | return new AlloyModelInterpretation( | ||
66 | new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, | ||
67 | (modelResult.representation as MonitoredAlloySolution).solution, | ||
68 | forwardMapper, | ||
69 | modelResult.trace as Logic2AlloyLanguageMapperTrace | ||
70 | ); | ||
71 | } | ||
72 | } \ No newline at end of file | ||