diff options
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend')
-rw-r--r-- | Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend new file mode 100644 index 00000000..09b67599 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | |||
@@ -0,0 +1,66 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
5 | |||
6 | class Alloy2LogicMapper { | ||
7 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | ||
8 | |||
9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { | ||
10 | val models = monitoredAlloySolution.aswers.map[it.key].toList | ||
11 | |||
12 | if(!monitoredAlloySolution.finishedBeforeTimeout) { | ||
13 | return createInsuficientResourcesResult => [ | ||
14 | it.problem = problem | ||
15 | it.representation += models | ||
16 | it.trace = trace | ||
17 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
18 | ] | ||
19 | } else { | ||
20 | if(models.last.satisfiable || requiredNumberOfSolution == -1) { | ||
21 | return createModelResult => [ | ||
22 | it.problem = problem | ||
23 | it.representation += models | ||
24 | it.trace = trace | ||
25 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
26 | ] | ||
27 | } else { | ||
28 | return createInconsistencyResult => [ | ||
29 | it.problem = problem | ||
30 | it.representation += models | ||
31 | it.trace = trace | ||
32 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
33 | ] | ||
34 | } | ||
35 | } | ||
36 | } | ||
37 | |||
38 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { | ||
39 | createStatistics => [ | ||
40 | it.transformationTime = transformationTime as int | ||
41 | for(solutionIndex : 0..<solution.aswers.size) { | ||
42 | val solutionTime = solution.aswers.get(solutionIndex).value | ||
43 | it.entries+= createIntStatisticEntry => [ | ||
44 | it.name = '''Answer«solutionIndex»Time''' | ||
45 | it.value = solutionTime.intValue | ||
46 | ] | ||
47 | } | ||
48 | it.entries+= createIntStatisticEntry => [ | ||
49 | it.name = "Alloy2KodKodTransformationTime" | ||
50 | it.value = solution.kodkodTime as int | ||
51 | ] | ||
52 | it.entries+= createIntStatisticEntry => [ | ||
53 | it.name = "Alloy2KodKodTransformationTime" | ||
54 | it.value = solution.kodkodTime as int | ||
55 | ] | ||
56 | it.entries+= createStringStatisticEntry => [ | ||
57 | it.name = "warnings" | ||
58 | it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]''' | ||
59 | ] | ||
60 | ] | ||
61 | } | ||
62 | |||
63 | def sum(Iterable<Long> ints) { | ||
64 | ints.reduce[p1, p2|p1+p2] | ||
65 | } | ||
66 | } \ No newline at end of file | ||