diff options
author | 2019-10-25 04:15:39 -0400 | |
---|---|---|
committer | 2019-10-25 04:15:39 -0400 | |
commit | 25a4b1b53add70e268c3083682f8a3508c618ec2 (patch) | |
tree | 6d46e62be49cfe6c5640e2e9af80aae90da6a212 /Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | |
parent | mid-measurement push (diff) | |
download | VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.gz VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.zst VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.zip |
VAMPIRE: post-submission push
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend')
-rw-r--r-- | Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | 263 |
1 files changed, 263 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/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..9e548ab6 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | |||
@@ -0,0 +1,263 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
13 | import java.util.ArrayList | ||
14 | import java.util.Collection | ||
15 | import java.util.HashMap | ||
16 | import java.util.List | ||
17 | |||
18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
19 | |||
20 | /** | ||
21 | * Each object is an element of an Object set, and types are subsets of the objects. | ||
22 | */ | ||
23 | class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyLanguageMapper_TypeMapper{ | ||
24 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
25 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
26 | |||
27 | new() { | ||
28 | // Initialize package | ||
29 | LogicproblemPackage.eINSTANCE.class | ||
30 | } | ||
31 | |||
32 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
33 | val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
34 | trace.typeMapperTrace = typeTrace | ||
35 | |||
36 | // 1. A global type for Objects is created | ||
37 | val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])] | ||
38 | val objectBody = createALSSignatureBody => [ | ||
39 | it.declarations += objectSig | ||
40 | it.abstract = true | ||
41 | ] | ||
42 | typeTrace.objectSupperClass = objectSig | ||
43 | trace.specification.signatureBodies += objectBody | ||
44 | |||
45 | // 2. Each type is mapped to a unique sig | ||
46 | for(type : types) { | ||
47 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)] | ||
48 | val body = createALSSignatureBody => [it.declarations += sig] | ||
49 | trace.specification.signatureBodies += body | ||
50 | typeTrace.type2ALSType.put(type,sig) | ||
51 | } | ||
52 | |||
53 | // 3. The elements of a defined type is mapped to singleton signatures | ||
54 | // 3.1 Collect the elements | ||
55 | val elementMatcher = TypeQueries.instance.getLowestCommonSupertypeOfAllOccuranceOfElement(trace.incqueryEngine) | ||
56 | val topmostType2Elements = new HashMap<ALSSignatureDeclaration,List<DefinedElement>> | ||
57 | for(element : elements) { | ||
58 | val topmostTypes = elementMatcher.getAllValuesOftype(element) | ||
59 | var ALSSignatureDeclaration selectedTopmostType; | ||
60 | if(topmostTypes.empty) { | ||
61 | selectedTopmostType = objectSig | ||
62 | } else{ | ||
63 | selectedTopmostType = topmostTypes.head.lookup(typeTrace.type2ALSType) | ||
64 | } | ||
65 | topmostType2Elements.putOrAddToList(selectedTopmostType,element) | ||
66 | } | ||
67 | |||
68 | // 4. For each topmost types several singleton classes are generated, which represents the elements. | ||
69 | // For the sake of clarity, common bodies are used. | ||
70 | for(topmostEntry : topmostType2Elements.entrySet) { | ||
71 | |||
72 | for(element : topmostEntry.value) { | ||
73 | val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] | ||
74 | typeTrace.definedElement2Declaration.put(element,signature) | ||
75 | } | ||
76 | |||
77 | val body = createALSSignatureBody => [ | ||
78 | it.multiplicity = ALSMultiplicity.ONE | ||
79 | it.declarations += topmostEntry.value.map[it.lookup(typeTrace.definedElement2Declaration)] | ||
80 | ] | ||
81 | |||
82 | val containerLogicType = topmostEntry.key | ||
83 | body.superset += containerLogicType | ||
84 | |||
85 | trace.specification.signatureBodies+=body | ||
86 | } | ||
87 | |||
88 | // 5.1 Each Defined Type is specified as the union of its elements | ||
89 | for(definedType : types.filter(TypeDefinition)) { | ||
90 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
91 | it.name = support.toIDMultiple("typedefinition",definedType.name) | ||
92 | it.term = createALSEquals => [ | ||
93 | it.leftOperand = createALSReference => [ it.referred = definedType.lookup(typeTrace.type2ALSType) ] | ||
94 | it.rightOperand = support.unfoldPlus(definedType.elements.map[e| | ||
95 | createALSReference => [it.referred = e.lookup(typeTrace.definedElement2Declaration)]]) | ||
96 | ] | ||
97 | ] | ||
98 | } | ||
99 | // 5.2 Each Defined Element is unique | ||
100 | for(definedType : types.filter(TypeDefinition)) { | ||
101 | val allElementsIncludingSubtypes = | ||
102 | definedType.<Type>transitiveClosureStar[it.subtypes].filter(TypeDefinition) | ||
103 | .map[elements].flatten.toSet.toList | ||
104 | if(allElementsIncludingSubtypes.size>=2) { | ||
105 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
106 | it.name = support.toIDMultiple("typeElementsUnique",definedType.name) | ||
107 | it.term = unfoldDistinctElements(allElementsIncludingSubtypes,trace) | ||
108 | ] | ||
109 | } | ||
110 | } | ||
111 | |||
112 | // 6. Each inheritance is modeled by subset operator 'in' | ||
113 | for(type : types) { | ||
114 | val sigBody = type.lookup(typeTrace.type2ALSType).eContainer as ALSSignatureBody | ||
115 | if(type.supertypes.empty) { | ||
116 | sigBody.superset += typeTrace.objectSupperClass | ||
117 | } else { | ||
118 | sigBody.superset += type.supertypes.map[lookup(typeTrace.type2ALSType)] | ||
119 | } | ||
120 | } | ||
121 | |||
122 | |||
123 | // 7. Each type is in the intersection of the supertypes | ||
124 | for(type : types.filter[it.supertypes.size>=2]) { | ||
125 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
126 | it.name = support.toIDMultiple("abstract",type.name) | ||
127 | it.term = createALSEquals => [ | ||
128 | it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] | ||
129 | it.rightOperand = support.unfoldIntersection(type.supertypes.map[e| | ||
130 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
131 | ] | ||
132 | ] | ||
133 | } | ||
134 | |||
135 | // 8. Each abstract type is equal to the union of the subtypes | ||
136 | for(type : types.filter[isIsAbstract]) { | ||
137 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
138 | it.name = support.toIDMultiple("abstract",type.name) | ||
139 | it.term = createALSEquals => [ | ||
140 | it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] | ||
141 | it.rightOperand = support.unfoldPlus(type.subtypes.map[e| | ||
142 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
143 | ] | ||
144 | ] | ||
145 | } | ||
146 | // 8.1 The object type is the union of the root types. | ||
147 | val rootTypes = types.filter[it.supertypes.empty].toList | ||
148 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
149 | it.name = support.toIDMultiple(#["ObjectTypeDefinition"]) | ||
150 | it.term = createALSEquals => [ | ||
151 | it.leftOperand = createALSReference => [ it.referred = typeTrace.objectSupperClass ] | ||
152 | it.rightOperand = support.unfoldPlus(rootTypes.map[e| | ||
153 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
154 | ] | ||
155 | ] | ||
156 | |||
157 | // 9. For each type X (including Object) | ||
158 | // only the common subtypes are in the intersection | ||
159 | // of the two subtype. | ||
160 | // 9.1. for the object | ||
161 | { | ||
162 | val rootTypeList = types.filter[it.supertypes.empty].toList | ||
163 | for(type1Index: 0..<rootTypeList.size) { | ||
164 | for(type2Index: 0..<type1Index) { | ||
165 | trace.specification.factDeclarations += | ||
166 | commonSubtypeOnlyInDiamonds(rootTypeList.get(type1Index),rootTypeList.get(type2Index),trace) | ||
167 | } | ||
168 | } | ||
169 | } | ||
170 | |||
171 | //9.3 for the subtypes of each objects | ||
172 | { | ||
173 | for(inScope : types) { | ||
174 | val subtypeList = inScope.subtypes//.toList | ||
175 | if(subtypeList.size>=2) { | ||
176 | for(type1Index: 0..<subtypeList.size) { | ||
177 | for(type2Index: 0..<type1Index) { | ||
178 | trace.specification.factDeclarations += | ||
179 | commonSubtypeOnlyInDiamonds(subtypeList.get(type1Index),subtypeList.get(type2Index),trace) | ||
180 | } | ||
181 | } | ||
182 | } | ||
183 | } | ||
184 | } | ||
185 | } | ||
186 | |||
187 | private def isEnumlikeType(Type type) { | ||
188 | if(type instanceof TypeDefinition) { | ||
189 | val elements = type.elements | ||
190 | return elements.forall[it.definedInType.size === 1 && it.definedInType.head === type] | ||
191 | } | ||
192 | return false | ||
193 | } | ||
194 | |||
195 | private def isEnumlikeElement(DefinedElement d) { | ||
196 | d.definedInType.size === 1 && d.definedInType.head.isEnumlikeType | ||
197 | } | ||
198 | |||
199 | def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) { | ||
200 | val res = trace.typeMapperTrace | ||
201 | if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes) { | ||
202 | return res | ||
203 | } else { | ||
204 | throw new IllegalArgumentException(''' | ||
205 | Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name», | ||
206 | but found «res.class.name»''') | ||
207 | } | ||
208 | } | ||
209 | |||
210 | def private commonSubtypeOnlyInDiamonds(Type t1, Type t2, Logic2AlloyLanguageMapperTrace trace) { | ||
211 | val topmostCommonSubtypes = TypeQueries.instance.getTopmostCommonSubtypes(trace.incqueryEngine) | ||
212 | val allTopmostCommon = topmostCommonSubtypes.getAllValuesOfcommon(t1,t2).toList | ||
213 | return createALSFactDeclaration => [ | ||
214 | it.name = support.toIDMultiple("common","types",t1.name,t2.name) | ||
215 | it.term = createALSEquals => [ | ||
216 | it.leftOperand = createALSIntersection => [ | ||
217 | it.leftOperand = createALSReference => [it.referred = t1.lookup(trace.typeTrace.type2ALSType)] | ||
218 | it.rightOperand = createALSReference => [it.referred = t2.lookup(trace.typeTrace.type2ALSType)] | ||
219 | ] | ||
220 | it.rightOperand = support.unfoldPlus(allTopmostCommon.map[t|createALSReference => [it.referred = t.lookup(trace.typeTrace.type2ALSType)]]) | ||
221 | ] | ||
222 | ] | ||
223 | } | ||
224 | |||
225 | def private unfoldDistinctElements( | ||
226 | List<DefinedElement> operands, | ||
227 | Logic2AlloyLanguageMapperTrace trace | ||
228 | ) { | ||
229 | if(operands.size == 1 || operands.size == 0) {support.unfoldTrueStatement(trace);} | ||
230 | else { | ||
231 | val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2) | ||
232 | for(i:0..<operands.size) { | ||
233 | for(j: i+1..<operands.size) { | ||
234 | notEquals+=createALSNotEquals=>[ | ||
235 | leftOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(i)) ] | ||
236 | rightOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(j)) ] | ||
237 | ] | ||
238 | } | ||
239 | } | ||
240 | return support.unfoldAnd(notEquals) | ||
241 | } | ||
242 | } | ||
243 | |||
244 | override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
245 | return #[trace.typeTrace.type2ALSType.get(referred)] | ||
246 | } | ||
247 | |||
248 | override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { | ||
249 | trace.typeTrace.objectSupperClass | ||
250 | } | ||
251 | |||
252 | override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { | ||
253 | createALSReference => [it.referred = referred.lookup(trace.typeTrace.definedElement2Declaration)] | ||
254 | } | ||
255 | |||
256 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { | ||
257 | if(undefinedScope == Integer.MAX_VALUE) return undefinedScope else return undefinedScope + trace.typeTrace.definedElement2Declaration.size | ||
258 | } | ||
259 | |||
260 | override getTypeInterpreter() { | ||
261 | return new AlloyModelInterpretation_TypeInterpretation_FilteredTypes | ||
262 | } | ||
263 | } \ No newline at end of file | ||