blob: 9148424c35d1cd52786bb687486e19438b001c8a (
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
67
68
69
70
71
72
73
74
75
|
package hu.bme.mit.inf.dslreasoner.logic.model.builder.consistencychecker
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
import org.eclipse.viatra.query.runtime.emf.EMFScope
import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
import hu.bme.mit.inf.dslreasoner.logic.model.patterns.TypeSystemIsInconsistentMatcher
import hu.bme.mit.inf.dslreasoner.logic.model.patterns.ElementNotDefinedInSupertypeMatcher
import hu.bme.mit.inf.dslreasoner.logic.model.patterns.ElementWithNoPossibleDynamicTypeMatcher
import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher
class TypeConsistencyChecker extends LogicReasoner{
val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE
new() {
LogicproblemPackage.eINSTANCE.class
}
override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
val statistics = createStatistics => [
it.transformationTime = 0
it.solverMemory = -1
]
val start = System.currentTimeMillis
val queryEngine = ViatraQueryEngine.on(new EMFScope(problem))
val typeSystemInconsistencyMatcher = TypeSystemIsInconsistentMatcher.on(queryEngine)
val elementNotDefinedInSupertype = ElementNotDefinedInSupertypeMatcher.on(queryEngine)
val elementWithNoPossibleDynamicType = ElementWithNoPossibleDynamicTypeMatcher.on(queryEngine)
val possibleDynamicType = PossibleDynamicTypeMatcher.on(queryEngine)
val hasErrorPatternMatch = typeSystemInconsistencyMatcher.hasMatch(problem)
statistics.solverTime = (System.currentTimeMillis - start) as int
val possibleDynamicTypeStatisticEntry = problem.elements.map[e|
'''«e.name»: [«possibleDynamicType.getAllValuesOfdynamic(problem,e).map[it.name].join(", ")»]'''
].join("\n")
if(hasErrorPatternMatch) {
return createInconsistencyResult =>[
it.problem = problem
it.statistics = statistics
it.statistics.entries += createStringStatisticEntry => [
it.name = "possibleDynamicType"
it.value = possibleDynamicTypeStatisticEntry
]
it.statistics.entries += createStringStatisticEntry => [
it.name = "elementNotDefinedInSupertype"
it.value=elementNotDefinedInSupertype.allValuesOfelement.map[it.name].join(", ")
]
it.statistics.entries += createStringStatisticEntry => [
it.name = "elementWithNoPossibleDynamicType"
it.value=elementWithNoPossibleDynamicType.allValuesOfelement.map[it.name].join(", ")
]
]
} else {
return createUndecidableResult =>
[it.problem = problem it.statistics = statistics]
}
}
override getInterpretations(ModelResult modelResult) {
throw new UnsupportedOperationException('''This solver is unable to create interpretations!''')
}
}
|
