diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-08-31 18:13:33 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-08-31 18:13:33 +0200 |
commit | a9d71084f532dd866572c04da42507d917dcb79f (patch) | |
tree | 08c2561a6a12cc5c064b576422f2b2fd95e90d97 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy | |
parent | Merge remote-tracking branch 'origin/master' into kris (diff) | |
parent | Type Interpretation for Alloy with Inheritance+Horizontal mapping (diff) | |
download | VIATRA-Generator-a9d71084f532dd866572c04da42507d917dcb79f.tar.gz VIATRA-Generator-a9d71084f532dd866572c04da42507d917dcb79f.tar.zst VIATRA-Generator-a9d71084f532dd866572c04da42507d917dcb79f.zip |
Merge remote-tracking branch 'origin/master' into kris
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy')
1 files changed, 58 insertions, 5 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend index 8019c6b5..ac75b2a1 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend | |||
@@ -1,20 +1,73 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | 1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder |
2 | 2 | ||
3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar | 3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar |
4 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
5 | import java.util.Map | ||
6 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | 4 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig |
7 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | 5 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field |
6 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
10 | import java.util.ArrayList | ||
10 | import java.util.List | 11 | import java.util.List |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | 12 | import java.util.Map |
13 | |||
14 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
12 | 15 | ||
13 | class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{ | 16 | class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{ |
14 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | 17 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE |
15 | 18 | ||
16 | override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, A4Solution solution, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String, Sig> name2AlloySig, Map<String, Field> name2AlloyField, Map<String, DefinedElement> expression2DefinedElement, Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) { | 19 | override resolveUnknownAtoms( |
17 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 20 | Iterable<ExprVar> objectAtoms, |
21 | A4Solution solution, | ||
22 | Logic2AlloyLanguageMapperTrace forwardTrace, | ||
23 | Map<String, Sig> name2AlloySig, | ||
24 | Map<String, Field> name2AlloyField, | ||
25 | Map<String,DefinedElement> expression2DefinedElement, | ||
26 | Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) | ||
27 | { | ||
28 | /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap() | ||
29 | val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/ | ||
30 | |||
31 | val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal | ||
32 | |||
33 | // 1. Evaluate the defined elements | ||
34 | for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) { | ||
35 | val name = definedElementMappingEntry.value.name | ||
36 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
37 | val elementsOfSingletonSignature = solution.eval(matchingSig) | ||
38 | if(elementsOfSingletonSignature.size != 1) { | ||
39 | throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''') | ||
40 | } else { | ||
41 | val expressionOfDefinedElement = elementsOfSingletonSignature.head.atom(0)// as ExprVar | ||
42 | expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key) | ||
43 | } | ||
44 | } | ||
45 | |||
46 | // 2. evaluate the signatures and create new elements if necessary | ||
47 | for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) { | ||
48 | val type = type2SingatureEntry.key | ||
49 | if(type instanceof TypeDeclaration) { | ||
50 | val name = type2SingatureEntry.value.name | ||
51 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
52 | val elementsOfSignature = solution.eval(matchingSig) | ||
53 | val elementList = new ArrayList(elementsOfSignature.size) | ||
54 | var newVariableIndex = 1; | ||
55 | for(elementOfSignature : elementsOfSignature) { | ||
56 | val expressionOfDefinedElement = elementOfSignature.atom(0) | ||
57 | if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) { | ||
58 | elementList += expressionOfDefinedElement.lookup(expression2DefinedElement) | ||
59 | } else { | ||
60 | val newElementName = '''newObject «newVariableIndex.toString»''' | ||
61 | val newRepresentation = createDefinedElement => [ | ||
62 | it.name = newElementName | ||
63 | ] | ||
64 | elementList += newRepresentation | ||
65 | expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation) | ||
66 | } | ||
67 | } | ||
68 | interpretationOfUndefinedType.put(type,elementList) | ||
69 | } | ||
70 | } | ||
18 | } | 71 | } |
19 | 72 | ||
20 | } \ No newline at end of file | 73 | } \ No newline at end of file |