diff options
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend')
-rw-r--r-- | Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend | 199 |
1 files changed, 199 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_RelationMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend new file mode 100644 index 00000000..d300a28b --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend | |||
@@ -0,0 +1,199 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
9 | import java.util.HashMap | ||
10 | |||
11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
13 | import java.util.List | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
15 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
16 | |||
17 | class Logic2AlloyLanguageMapper_RelationMapper { | ||
18 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
19 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
20 | val Logic2AlloyLanguageMapper base; | ||
21 | public new(Logic2AlloyLanguageMapper base) { | ||
22 | this.base = base | ||
23 | } | ||
24 | |||
25 | def dispatch public void transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
26 | if(!trace.relationDefinitions.containsKey(r)) { | ||
27 | if(r.transformToHostedField(trace)) { | ||
28 | transformRelationDeclarationToHostedField(r,trace) | ||
29 | } else { | ||
30 | transformRelationDeclarationToGlobalField(r,trace) | ||
31 | } | ||
32 | } | ||
33 | } | ||
34 | |||
35 | def public createRelationDeclaration(String name, List<TypeReference> paramTypes, Logic2AlloyLanguageMapperTrace trace) { | ||
36 | val field = createALSFieldDeclaration => [ | ||
37 | it.name = support.toID(name) | ||
38 | it.type = support.unfoldReferenceDirectProduct(base,paramTypes,trace) | ||
39 | ] | ||
40 | trace.logicLanguageBody.fields += field | ||
41 | return field | ||
42 | } | ||
43 | |||
44 | def protected transformToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
45 | val first = r.parameters.get(0) | ||
46 | if(r.parameters.size == 2) { | ||
47 | if(first instanceof ComplexTypeReference) { | ||
48 | val types = base.typeMapper.transformTypeReference(first.referred,base,trace) | ||
49 | if(types.size == 1) { | ||
50 | return true | ||
51 | } | ||
52 | } | ||
53 | } | ||
54 | return false | ||
55 | } | ||
56 | |||
57 | def protected transformRelationDeclarationToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
58 | val hostType = (r.parameters.head as ComplexTypeReference).referred | ||
59 | |||
60 | val targetBody = base.typeMapper.transformTypeReference(hostType,base,trace).get(0).eContainer as ALSSignatureBody | ||
61 | val field = createALSFieldDeclaration => [ | ||
62 | it.name = support.toID(r.getName) | ||
63 | it.multiplicity = ALSMultiplicity.SET | ||
64 | it.type = base.transformTypeReference(r.parameters.get(1),trace) | ||
65 | ] | ||
66 | targetBody.fields += field | ||
67 | trace.relationDeclaration2Field.put(r,field) | ||
68 | |||
69 | } | ||
70 | |||
71 | def protected transformRelationDeclarationToGlobalField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
72 | val field = createALSFieldDeclaration => [ | ||
73 | it.name = support.toID(r.name) | ||
74 | it.type = support.unfoldReferenceDirectProduct(base,r.parameters,trace) | ||
75 | ] | ||
76 | trace.logicLanguageBody.fields += field | ||
77 | trace.relationDeclaration2Global.put(r, field) | ||
78 | } | ||
79 | |||
80 | def dispatch public void transformRelation(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { | ||
81 | val res = createALSRelationDefinition => [ | ||
82 | name = support.toID(r.name) | ||
83 | // fill the variables later | ||
84 | // fill the expression later | ||
85 | ] | ||
86 | |||
87 | trace.relationDefinition2Predicate.put(r,res) | ||
88 | trace.specification.relationDefinitions+=res; | ||
89 | } | ||
90 | |||
91 | def protected void transformRelationDefinitionSpecification(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { | ||
92 | val predicate = r.lookup(trace.relationDefinition2Predicate) | ||
93 | if(predicate !== null) { | ||
94 | val variableMap = new HashMap | ||
95 | for(variable : r.variables) { | ||
96 | val v = createALSVariableDeclaration => [ | ||
97 | it.name = support.toID(variable.name) | ||
98 | it.range = base.transformTypeReference(variable.range,trace) | ||
99 | ] | ||
100 | predicate.variables+=v | ||
101 | variableMap.put(variable,v) | ||
102 | } | ||
103 | predicate.value = base.transformTerm(r.value,trace,variableMap) | ||
104 | } | ||
105 | } | ||
106 | |||
107 | def public transformRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { | ||
108 | if(relation.transformToHostedField(trace)) { | ||
109 | return createALSReference => [it.referred = relation.lookup(trace.relationDeclaration2Field) ] | ||
110 | } else { | ||
111 | return createALSJoin => [ | ||
112 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
113 | rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]] | ||
114 | } | ||
115 | } | ||
116 | |||
117 | def public getRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { | ||
118 | if(relation.transformToHostedField(trace)) { | ||
119 | return relation.lookup(trace.relationDeclaration2Field) | ||
120 | } else { | ||
121 | return relation.lookup(trace.relationDeclaration2Global) | ||
122 | } | ||
123 | } | ||
124 | |||
125 | public def dispatch void prepareTransitiveClosure(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { | ||
126 | // There is nothing to do, relation can be used in ^relation expressions | ||
127 | if(transformToHostedField(relation,trace)) { | ||
128 | trace.relationInTransitiveToHosterField.put(relation,relation.lookup(trace.relationDeclaration2Field)) | ||
129 | } else { | ||
130 | trace.relationInTransitiveToGlobalField.put(relation,relation.lookup(trace.relationDeclaration2Global)) | ||
131 | } | ||
132 | } | ||
133 | public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { | ||
134 | if(relation.parameters.size === 2) { | ||
135 | /** 1. Create a relation that can be used in ^relation expressions */ | ||
136 | val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace) | ||
137 | trace.relationInTransitiveToHosterField.put(relation,declaration) | ||
138 | /** 2. Add fact that the declaration corresponds to the definition */ | ||
139 | val fact = createALSFactDeclaration => [ | ||
140 | it.name = '''EqualsAsDeclaration «relation.name»''' | ||
141 | it.term = createALSQuantifiedEx => [ | ||
142 | val a = createALSVariableDeclaration => [ | ||
143 | it.name = "a" | ||
144 | it.range = base.transformTypeReference(relation.parameters.get(0),trace) | ||
145 | ] | ||
146 | val b = createALSVariableDeclaration => [ | ||
147 | it.name = "b" | ||
148 | it.range = base.transformTypeReference(relation.parameters.get(1),trace) | ||
149 | ] | ||
150 | it.variables += a | ||
151 | it.variables += b | ||
152 | it.type = ALSMultiplicity::ALL | ||
153 | it.expression = createALSIff => [ | ||
154 | it.leftOperand = createALSFunctionCall => [ | ||
155 | it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) | ||
156 | it.params += createALSReference => [ it.referred = a ] | ||
157 | it.params += createALSReference => [ it.referred = b ] | ||
158 | ] | ||
159 | it.rightOperand = createALSSubset => [ | ||
160 | it.leftOperand = createALSJoin => [ | ||
161 | it.leftOperand = createALSReference => [ referred = a ] | ||
162 | it.rightOperand = createALSReference => [ referred = b ] | ||
163 | ] | ||
164 | it.rightOperand = createALSJoin => [ | ||
165 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
166 | rightOperand = createALSReference => [ referred = declaration ] | ||
167 | ] | ||
168 | ] | ||
169 | ] | ||
170 | ] | ||
171 | ] | ||
172 | trace.specification.factDeclarations += fact | ||
173 | return | ||
174 | } else { | ||
175 | throw new AssertionError('''A non-binary relation "«relation.name»" is used in transitive clousure!''') | ||
176 | } | ||
177 | } | ||
178 | |||
179 | def public transformTransitiveRelationReference(Relation relation, ALSTerm source, ALSTerm target, Logic2AlloyLanguageMapperTrace trace) { | ||
180 | val alsTargetRelation = if(trace.relationInTransitiveToGlobalField.containsKey(relation)) { | ||
181 | createALSJoin => [ | ||
182 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
183 | rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] | ||
184 | ] | ||
185 | } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ | ||
186 | createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] | ||
187 | } else { | ||
188 | throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') | ||
189 | } | ||
190 | return createALSSubset => [ | ||
191 | it.leftOperand = createALSJoin => [ | ||
192 | it.leftOperand = source | ||
193 | it.rightOperand = target | ||
194 | ] | ||
195 | it.rightOperand = createAlSTransitiveClosure => [it.operand = alsTargetRelation] | ||
196 | |||
197 | ] | ||
198 | } | ||
199 | } \ No newline at end of file | ||