diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend | 92 |
1 files changed, 90 insertions, 2 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend index 9dd4da2f..0762efce 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend | |||
@@ -9,6 +9,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | |||
9 | import java.util.HashMap | 9 | import java.util.HashMap |
10 | 10 | ||
11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 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 | ||
12 | 16 | ||
13 | class Logic2AlloyLanguageMapper_RelationMapper { | 17 | class Logic2AlloyLanguageMapper_RelationMapper { |
14 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 18 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
@@ -18,7 +22,7 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
18 | this.base = base | 22 | this.base = base |
19 | } | 23 | } |
20 | 24 | ||
21 | def dispatch protected void transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | 25 | def dispatch public void transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { |
22 | if(!trace.relationDefinitions.containsKey(r)) { | 26 | if(!trace.relationDefinitions.containsKey(r)) { |
23 | if(r.transformToHostedField(trace)) { | 27 | if(r.transformToHostedField(trace)) { |
24 | transformRelationDeclarationToHostedField(r,trace) | 28 | transformRelationDeclarationToHostedField(r,trace) |
@@ -28,6 +32,15 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
28 | } | 32 | } |
29 | } | 33 | } |
30 | 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 | |||
31 | def protected transformToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | 44 | def protected transformToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { |
32 | val first = r.parameters.get(0) | 45 | val first = r.parameters.get(0) |
33 | if(r.parameters.size == 2) { | 46 | if(r.parameters.size == 2) { |
@@ -64,7 +77,7 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
64 | trace.relationDeclaration2Global.put(r, field) | 77 | trace.relationDeclaration2Global.put(r, field) |
65 | } | 78 | } |
66 | 79 | ||
67 | def dispatch protected void transformRelation(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { | 80 | def dispatch public void transformRelation(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { |
68 | val res = createALSRelationDefinition => [ | 81 | val res = createALSRelationDefinition => [ |
69 | name = support.toID(r.name) | 82 | name = support.toID(r.name) |
70 | // fill the variables later | 83 | // fill the variables later |
@@ -108,4 +121,79 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
108 | return relation.lookup(trace.relationDeclaration2Global) | 121 | return relation.lookup(trace.relationDeclaration2Global) |
109 | } | 122 | } |
110 | } | 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 | } | ||
111 | } \ No newline at end of file | 199 | } \ No newline at end of file |