diff options
author | 2017-10-13 13:32:46 +0200 | |
---|---|---|
committer | 2017-10-13 13:32:46 +0200 | |
commit | e9338be10e5453a7a026bbc16ddaa30abe9fa5be (patch) | |
tree | c33155d6110dc4cf2c99eda427cfb04ceff1511d /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu | |
parent | Visualisation for all models in a directory (diff) | |
download | VIATRA-Generator-e9338be10e5453a7a026bbc16ddaa30abe9fa5be.tar.gz VIATRA-Generator-e9338be10e5453a7a026bbc16ddaa30abe9fa5be.tar.zst VIATRA-Generator-e9338be10e5453a7a026bbc16ddaa30abe9fa5be.zip |
Refactoring of Alloy type mapping and interpretation.
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu')
4 files changed, 12 insertions, 135 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend index 53674ca3..abedf9e4 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend | |||
@@ -1,6 +1,7 @@ | |||
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.ast.Sig | ||
4 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | 5 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field |
5 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | 6 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation |
@@ -20,123 +21,6 @@ import java.util.Map | |||
20 | import java.util.Set | 21 | import java.util.Set |
21 | 22 | ||
22 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 23 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
23 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | ||
24 | import java.util.ArrayList | ||
25 | |||
26 | interface AlloyModelInterpretation_TypeInterpretation { | ||
27 | def void resolveUnknownAtoms( | ||
28 | Iterable<ExprVar> objectAtoms, | ||
29 | A4Solution solution, | ||
30 | Logic2AlloyLanguageMapperTrace forwardTrace, | ||
31 | Map<String, Sig> name2AlloySig, | ||
32 | Map<String, Field> name2AlloyField, | ||
33 | Map<String,DefinedElement> expression2DefinedElement, | ||
34 | Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) | ||
35 | } | ||
36 | |||
37 | class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{ | ||
38 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
39 | |||
40 | override resolveUnknownAtoms( | ||
41 | Iterable<ExprVar> objectAtoms, | ||
42 | A4Solution solution, | ||
43 | Logic2AlloyLanguageMapperTrace forwardTrace, | ||
44 | Map<String, Sig> name2AlloySig, | ||
45 | Map<String, Field> name2AlloyField, | ||
46 | Map<String,DefinedElement> expression2DefinedElement, | ||
47 | Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) | ||
48 | { | ||
49 | /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap() | ||
50 | val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/ | ||
51 | |||
52 | val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
53 | |||
54 | // 1. Evaluate the defined elements | ||
55 | for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) { | ||
56 | val name = definedElementMappingEntry.value.name | ||
57 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
58 | val elementsOfSingletonSignature = solution.eval(matchingSig) | ||
59 | if(elementsOfSingletonSignature.size != 1) { | ||
60 | throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''') | ||
61 | } else { | ||
62 | val expressionOfDefinedElement = elementsOfSingletonSignature.head.atom(0)// as ExprVar | ||
63 | expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key) | ||
64 | } | ||
65 | } | ||
66 | |||
67 | // 2. evaluate the signatures and create new elements if necessary | ||
68 | for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) { | ||
69 | val type = type2SingatureEntry.key | ||
70 | if(type instanceof TypeDeclaration) { | ||
71 | val name = type2SingatureEntry.value.name | ||
72 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
73 | val elementsOfSignature = solution.eval(matchingSig) | ||
74 | val elementList = new ArrayList(elementsOfSignature.size) | ||
75 | var newVariableIndex = 1; | ||
76 | for(elementOfSignature : elementsOfSignature) { | ||
77 | val expressionOfDefinedElement = elementOfSignature.atom(0) | ||
78 | if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) { | ||
79 | elementList += expressionOfDefinedElement.lookup(expression2DefinedElement) | ||
80 | } else { | ||
81 | val newElementName = '''newObject «newVariableIndex.toString»''' | ||
82 | val newRepresentation = createDefinedElement => [ | ||
83 | it.name = newElementName | ||
84 | ] | ||
85 | elementList += newRepresentation | ||
86 | expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation) | ||
87 | } | ||
88 | } | ||
89 | interpretationOfUndefinedType.put(type,elementList) | ||
90 | } | ||
91 | } | ||
92 | } | ||
93 | } | ||
94 | /* | ||
95 | class AlloyModelInterpretation_TypeInterpretation_Horizontal implements AlloyModelInterpretation_TypeInterpretation{ | ||
96 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
97 | |||
98 | override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String,DefinedElement> alloyAtom2LogicElement) { | ||
99 | val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap; | ||
100 | |||
101 | //TMP sig maps to identify alloy signatures by their names | ||
102 | val Map<String,Type> sigName2LogicType = | ||
103 | forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name] | ||
104 | //val Map<String,DefinedElement> elementNameNamel2DefinedElement = | ||
105 | // forwardTrace.definedElement2Declaration.keySet.toMap[x|forwardTrace.definedElement2Declaration.get(x).name] | ||
106 | |||
107 | // Fill the interpretation map with empty lists | ||
108 | forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x|interpretationOfUndefinedType.put(x,new LinkedList)] | ||
109 | |||
110 | // exporing individuals | ||
111 | for(atom: objectAtoms) { | ||
112 | val typeName = getName(atom.type) | ||
113 | //val atomName = atom.name | ||
114 | |||
115 | if(sigName2LogicType.containsKey(typeName)) { | ||
116 | val type = sigName2LogicType.get(typeName) | ||
117 | val elementsOfType = interpretationOfUndefinedType.get(type) | ||
118 | val element = createDefinedElement => [ | ||
119 | it.name += type.name | ||
120 | it.name += (elementsOfType.size+1).toString | ||
121 | ] | ||
122 | alloyAtom2LogicElement.put(atom.label,element) | ||
123 | elementsOfType+=element | ||
124 | } | ||
125 | else throw new UnsupportedOperationException('''Unknown atom: «atom»''') | ||
126 | } | ||
127 | |||
128 | return interpretationOfUndefinedType | ||
129 | } | ||
130 | |||
131 | def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) { | ||
132 | val name = type.toString | ||
133 | if(name.startsWith("{this/") && name.endsWith("}")) { | ||
134 | return type.toString.replaceFirst("\\{this\\/","").replace("}","") | ||
135 | } | ||
136 | else throw new IllegalArgumentException('''Unknown type format: "«name»"!''') | ||
137 | } | ||
138 | //def private getName(ExprVar atom) { atom.toString.split("\\$") } | ||
139 | }*/ | ||
140 | 24 | ||
141 | class AlloyModelInterpretation implements LogicModelInterpretation{ | 25 | class AlloyModelInterpretation implements LogicModelInterpretation{ |
142 | 26 | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend index 9927f1cc..49268b42 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend | |||
@@ -13,4 +13,6 @@ interface Logic2AlloyLanguageMapper_TypeMapper { | |||
13 | def ALSSignatureDeclaration getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) | 13 | def ALSSignatureDeclaration getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) |
14 | def int getUndefinedSupertypeScope(int undefinedScope,Logic2AlloyLanguageMapperTrace trace) | 14 | def int getUndefinedSupertypeScope(int undefinedScope,Logic2AlloyLanguageMapperTrace trace) |
15 | def ALSTerm transformReference(DefinedElement referred,Logic2AlloyLanguageMapperTrace trace) | 15 | def ALSTerm transformReference(DefinedElement referred,Logic2AlloyLanguageMapperTrace trace) |
16 | |||
17 | def AlloyModelInterpretation_TypeInterpretation getTypeInterpreter() | ||
16 | } | 18 | } |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend index ade9860b..3b2e3390 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | |||
@@ -18,13 +18,7 @@ import java.util.Map | |||
18 | 18 | ||
19 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 19 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
20 | 20 | ||
21 | class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | 21 | |
22 | implements Logic2AlloyLanguageMapper_TypeMapperTrace | ||
23 | { | ||
24 | public var ALSSignatureDeclaration objectSupperClass; | ||
25 | public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap; | ||
26 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap | ||
27 | } | ||
28 | /** | 22 | /** |
29 | * Each object is an element of an Object set, and types are subsets of the objects. | 23 | * Each object is an element of an Object set, and types are subsets of the objects. |
30 | */ | 24 | */ |
@@ -265,4 +259,7 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL | |||
265 | return undefinedScope + trace.typeTrace.definedElement2Declaration.size | 259 | return undefinedScope + trace.typeTrace.definedElement2Declaration.size |
266 | } | 260 | } |
267 | 261 | ||
262 | override getTypeInterpreter() { | ||
263 | return new AlloyModelInterpretation_TypeInterpretation_FilteredTypes | ||
264 | } | ||
268 | } \ No newline at end of file | 265 | } \ No newline at end of file |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend index 92ac27df..be840e30 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend | |||
@@ -2,24 +2,13 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | |||
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | 3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity |
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody | 4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody |
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | 5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
11 | import java.util.Collection | 10 | import java.util.Collection |
12 | import java.util.HashMap | ||
13 | import java.util.LinkedList | 11 | import java.util.LinkedList |
14 | import java.util.List | ||
15 | import java.util.Map | ||
16 | |||
17 | class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace { | ||
18 | public var ALSSignatureDeclaration objectSupperClass; | ||
19 | public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap; | ||
20 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap | ||
21 | public val Map<Type, List<ALSSignatureDeclaration>> typeSelection = new HashMap | ||
22 | } | ||
23 | 12 | ||
24 | class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{ | 13 | class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{ |
25 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 14 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
@@ -125,4 +114,9 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L | |||
125 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { | 114 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { |
126 | return undefinedScope + trace.typeTrace.definedElement2Declaration.size | 115 | return undefinedScope + trace.typeTrace.definedElement2Declaration.size |
127 | } | 116 | } |
117 | |||
118 | override getTypeInterpreter() { | ||
119 | return new AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal | ||
120 | } | ||
121 | |||
128 | } \ No newline at end of file | 122 | } \ No newline at end of file |