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