diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-07-05 16:31:32 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-07-05 16:31:32 +0200 |
commit | adce403870ea34f79cf2c59b88cdb5b2dcb438a8 (patch) | |
tree | 64a4aeedb53d642c1a60c498be26213b41547497 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend | |
parent | Adding multiple model generation support for the alloy solver. (diff) | |
download | VIATRA-Generator-adce403870ea34f79cf2c59b88cdb5b2dcb438a8.tar.gz VIATRA-Generator-adce403870ea34f79cf2c59b88cdb5b2dcb438a8.tar.zst VIATRA-Generator-adce403870ea34f79cf2c59b88cdb5b2dcb438a8.zip |
Support for generationg multiple difference models by VIATRA-Solver
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend | 73 |
1 files changed, 67 insertions, 6 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend index b2a7e3f5..56c3c852 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend | |||
@@ -1,16 +1,68 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | ||
13 | import java.util.HashMap | ||
14 | import java.util.List | ||
15 | import java.util.Map | ||
16 | import org.eclipse.emf.ecore.EObject | ||
17 | |||
18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink | ||
8 | 21 | ||
9 | class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | 22 | class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ |
23 | val PartialInterpretation partialInterpretation | ||
24 | val Map<EObject, EObject> trace; | ||
25 | val Map<TypeDeclaration,PartialTypeInterpratation> type2Interpretation | ||
26 | val Map<RelationDeclaration,PartialRelationInterpretation> relation2Interpretation | ||
27 | val Map<DefinedElement,DefinedElement> elementBackwardTrace | ||
10 | 28 | ||
29 | new(PartialInterpretation partialInterpretation, Map<EObject, EObject> forwardMap) { | ||
30 | this.partialInterpretation = partialInterpretation | ||
31 | this.trace = forwardMap | ||
32 | this.type2Interpretation = initTypes(partialInterpretation.partialtypeinterpratation) | ||
33 | this.relation2Interpretation = initRelations(partialInterpretation.partialrelationinterpretation) | ||
34 | this.elementBackwardTrace = initElementBackwardTrace(trace) | ||
35 | } | ||
36 | |||
37 | def initTypes(List<PartialTypeInterpratation> types) { | ||
38 | types.toMap[it.interpretationOf] | ||
39 | } | ||
40 | def initRelations(List<PartialRelationInterpretation> relations) { | ||
41 | relations.toMap[it.interpretationOf] | ||
42 | } | ||
43 | def initElementBackwardTrace(Map<EObject, EObject> trace) { | ||
44 | val entryBackwardMap = new HashMap | ||
45 | for(entry: trace.entrySet) { | ||
46 | if(entry.key instanceof DefinedElement) { | ||
47 | entryBackwardMap.put(entry.value as DefinedElement, entry.key as DefinedElement) | ||
48 | } | ||
49 | } | ||
50 | return entryBackwardMap | ||
51 | } | ||
11 | 52 | ||
12 | override getElements(Type type) { | 53 | override getElements(Type type) { |
13 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 54 | val t1 = type.lookup(trace) as TypeDeclaration |
55 | val t2 = t1.lookup(this.type2Interpretation) | ||
56 | return t2.elements.map[it.elementLookupBackward] | ||
57 | } | ||
58 | |||
59 | def elementLookupForward(DefinedElement e) { | ||
60 | if(this.trace.containsKey(e)) return e.lookup(trace) as DefinedElement | ||
61 | else return e; | ||
62 | } | ||
63 | def elementLookupBackward(DefinedElement e) { | ||
64 | if(this.elementBackwardTrace.containsKey(e)) return e.lookup(this.elementBackwardTrace) | ||
65 | else return e; | ||
14 | } | 66 | } |
15 | 67 | ||
16 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | 68 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { |
@@ -18,13 +70,22 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | |||
18 | } | 70 | } |
19 | 71 | ||
20 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | 72 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { |
21 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 73 | if(parameterSubstitution.size == 2) { |
74 | val param1 = (parameterSubstitution.get(0) as DefinedElement).elementLookupForward | ||
75 | val param2 = (parameterSubstitution.get(1) as DefinedElement).elementLookupForward | ||
76 | val r1 = relation.lookup(trace) as RelationDeclaration | ||
77 | val r2 = r1.lookup(this.relation2Interpretation) | ||
78 | val links = r2.relationlinks.filter(BinaryElementRelationLink) | ||
79 | val existLink = links.exists[it.param1 == param1 && it.param2 == param2] | ||
80 | //println(existLink) | ||
81 | return existLink | ||
82 | } else throw new UnsupportedOperationException | ||
22 | } | 83 | } |
23 | 84 | ||
24 | override getInterpretation(ConstantDeclaration constant) { | 85 | override getInterpretation(ConstantDeclaration constant) { |
25 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 86 | throw new UnsupportedOperationException("TODO: auto-generated method stub") |
26 | } | 87 | } |
27 | 88 | ||
28 | override getMinimalInteger() { 0 } | 89 | override getMinimalInteger() {0} |
29 | override getMaximalInteger() {0 } | 90 | override getMaximalInteger() {0} |
30 | } \ No newline at end of file | 91 | } \ No newline at end of file |