blob: 09b6759931ca9a8aaebce5dacbb38c994909707b (
plain) (
blame)
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
|
package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
class Alloy2LogicMapper {
val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
val models = monitoredAlloySolution.aswers.map[it.key].toList
if(!monitoredAlloySolution.finishedBeforeTimeout) {
return createInsuficientResourcesResult => [
it.problem = problem
it.representation += models
it.trace = trace
it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
]
} else {
if(models.last.satisfiable || requiredNumberOfSolution == -1) {
return createModelResult => [
it.problem = problem
it.representation += models
it.trace = trace
it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
]
} else {
return createInconsistencyResult => [
it.problem = problem
it.representation += models
it.trace = trace
it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
]
}
}
}
def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
createStatistics => [
it.transformationTime = transformationTime as int
for(solutionIndex : 0..<solution.aswers.size) {
val solutionTime = solution.aswers.get(solutionIndex).value
it.entries+= createIntStatisticEntry => [
it.name = '''Answer«solutionIndex»Time'''
it.value = solutionTime.intValue
]
}
it.entries+= createIntStatisticEntry => [
it.name = "Alloy2KodKodTransformationTime"
it.value = solution.kodkodTime as int
]
it.entries+= createIntStatisticEntry => [
it.name = "Alloy2KodKodTransformationTime"
it.value = solution.kodkodTime as int
]
it.entries+= createStringStatisticEntry => [
it.name = "warnings"
it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
]
]
}
def sum(Iterable<Long> ints) {
ints.reduce[p1, p2|p1+p2]
}
}
|
