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.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | 467 |
1 files changed, 467 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend new file mode 100644 index 00000000..23b9027f --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | |||
@@ -0,0 +1,467 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumericOperator | ||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
51 | import java.util.Collections | ||
52 | import java.util.HashMap | ||
53 | import java.util.List | ||
54 | import java.util.Map | ||
55 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
56 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
57 | import org.eclipse.xtend.lib.annotations.Accessors | ||
58 | |||
59 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
60 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation | ||
61 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | ||
62 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation | ||
63 | import java.util.Collection | ||
64 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | ||
65 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | ||
66 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct | ||
67 | |||
68 | class Logic2AlloyLanguageMapper { | ||
69 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
70 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
71 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | ||
72 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this) | ||
73 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this) | ||
74 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_RelationMapper relationMapper = new Logic2AlloyLanguageMapper_RelationMapper(this) | ||
75 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_Containment containmentMapper = new Logic2AlloyLanguageMapper_Containment(this) | ||
76 | |||
77 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | ||
78 | this.typeMapper = typeMapper | ||
79 | } | ||
80 | |||
81 | public def TracedOutput<ALSDocument,Logic2AlloyLanguageMapperTrace> transformProblem(LogicProblem problem, AlloySolverConfiguration config) { | ||
82 | val logicLanguage = createALSSignatureBody => [ | ||
83 | it.multiplicity = ALSMultiplicity.ONE | ||
84 | it.declarations += | ||
85 | createALSSignatureDeclaration => [ | ||
86 | it.name = support.toID(#["util", "language"]) ] | ||
87 | ] | ||
88 | |||
89 | val specification = createALSDocument=>[ | ||
90 | it.signatureBodies+=logicLanguage | ||
91 | ] | ||
92 | val trace = new Logic2AlloyLanguageMapperTrace => [ | ||
93 | it.specification = specification | ||
94 | it.logicLanguage = logicLanguage.declarations.head | ||
95 | it.logicLanguageBody = logicLanguage | ||
96 | |||
97 | it.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem)) | ||
98 | ] | ||
99 | |||
100 | typeMapper.transformTypes(problem.types,problem.elements,this,trace) | ||
101 | |||
102 | trace.constantDefinitions = problem.collectConstantDefinitions | ||
103 | trace.functionDefinitions = problem.collectFunctionDefinitions | ||
104 | trace.relationDefinitions = problem.collectRelationDefinitions | ||
105 | |||
106 | problem.constants.forEach[this.constantMapper.transformConstant(it,trace)] | ||
107 | problem.functions.forEach[this.functionMapper.transformFunction(it, trace)] | ||
108 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] | ||
109 | |||
110 | problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstantDefinitionSpecification(it,trace)] | ||
111 | problem.functions.filter(FunctionDefinition).forEach[this.functionMapper.transformFunctionDefinitionSpecification(it,trace)] | ||
112 | problem.relations.filter(RelationDefinition).forEach[this.relationMapper.transformRelationDefinitionSpecification(it,trace)] | ||
113 | |||
114 | val containment = problem.getContainmentHierarchies.head | ||
115 | if(containment !== null) { | ||
116 | this.containmentMapper.transformContainmentHierarchy(containment,trace) | ||
117 | } | ||
118 | |||
119 | //////////////////// | ||
120 | // Collect EMF-specific assertions | ||
121 | //////////////////// | ||
122 | val assertion2InverseRelation = problem.annotations.collectAnnotations(InverseRelationAssertion) | ||
123 | val assertion2UpperMultiplicityAssertion = problem.annotations.collectAnnotations(UpperMultiplicityAssertion) | ||
124 | val assertion2LowerMultiplicityAssertion = problem.annotations.collectAnnotations(LowerMultiplicityAssertion) | ||
125 | |||
126 | //////////////////// | ||
127 | // Transform Assertions | ||
128 | //////////////////// | ||
129 | for(assertion : problem.assertions) { | ||
130 | if(assertion2InverseRelation.containsKey(assertion)) { | ||
131 | transformInverseAssertion(assertion.lookup(assertion2InverseRelation),trace) | ||
132 | } else if(assertion2UpperMultiplicityAssertion.containsKey(assertion)) { | ||
133 | transformUpperMultiplicityAssertion(assertion.lookup(assertion2UpperMultiplicityAssertion),trace) | ||
134 | } else if(assertion2LowerMultiplicityAssertion.containsKey(assertion)) { | ||
135 | transformLowerMultiplicityAssertion(assertion.lookup(assertion2LowerMultiplicityAssertion),trace) | ||
136 | } else { | ||
137 | transformAssertion(assertion,trace) | ||
138 | } | ||
139 | } | ||
140 | |||
141 | transformRunCommand(specification, trace, config) | ||
142 | |||
143 | return new TracedOutput(specification,trace) | ||
144 | } | ||
145 | |||
146 | def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
147 | val a = assertion.inverseA | ||
148 | val b = assertion.inverseB | ||
149 | if(a instanceof RelationDeclaration && b instanceof RelationDeclaration && | ||
150 | !trace.relationDefinitions.containsKey(a) && !trace.relationDefinitions.containsKey(b)) | ||
151 | { | ||
152 | val fact = createALSFactDeclaration => [ | ||
153 | it.name = support.toID(assertion.target.name) | ||
154 | it.term = createALSEquals => [ | ||
155 | it.leftOperand = relationMapper.transformRelationReference(a as RelationDeclaration, trace) | ||
156 | it.rightOperand = createALSInverseRelation => [it.operand = relationMapper.transformRelationReference(b as RelationDeclaration, trace) ] | ||
157 | ] | ||
158 | ] | ||
159 | trace.specification.factDeclarations += fact | ||
160 | } else { | ||
161 | return transformAssertion(assertion.target,trace) | ||
162 | } | ||
163 | } | ||
164 | |||
165 | def transformUpperMultiplicityAssertion(UpperMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
166 | val x = assertion.relation | ||
167 | if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) { | ||
168 | val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) | ||
169 | val type = relation.type | ||
170 | |||
171 | if(type instanceof ALSDirectProduct) { | ||
172 | type.rightMultiplicit = type.rightMultiplicit.addUpper | ||
173 | } else { | ||
174 | relation.multiplicity = relation.multiplicity.addUpper | ||
175 | } | ||
176 | |||
177 | if(assertion.upper === 1) { | ||
178 | return true | ||
179 | } else { | ||
180 | return transformAssertion(assertion.target,trace) | ||
181 | } | ||
182 | |||
183 | } else { | ||
184 | return transformAssertion(assertion.target,trace) | ||
185 | } | ||
186 | } | ||
187 | |||
188 | def transformLowerMultiplicityAssertion(LowerMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
189 | val x = assertion.relation | ||
190 | if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) { | ||
191 | val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) | ||
192 | val type = relation.type | ||
193 | |||
194 | if(type instanceof ALSDirectProduct) { | ||
195 | type.rightMultiplicit = type.rightMultiplicit.addLower | ||
196 | } else { | ||
197 | relation.multiplicity = relation.multiplicity.addLower | ||
198 | } | ||
199 | |||
200 | if(assertion.lower === 1) { | ||
201 | return true | ||
202 | } else { | ||
203 | return transformAssertion(assertion.target,trace) | ||
204 | } | ||
205 | |||
206 | } else { | ||
207 | return transformAssertion(assertion.target,trace) | ||
208 | } | ||
209 | } | ||
210 | |||
211 | private def addLower(ALSMultiplicity multiplicity) { | ||
212 | if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { | ||
213 | return ALSMultiplicity::SOME | ||
214 | } else if(multiplicity === ALSMultiplicity::LONE) { | ||
215 | return ALSMultiplicity::ONE | ||
216 | } else { | ||
217 | throw new IllegalArgumentException('''Lower multiplicity is already set!''') | ||
218 | } | ||
219 | } | ||
220 | private def addUpper(ALSMultiplicity multiplicity) { | ||
221 | if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { | ||
222 | return ALSMultiplicity::LONE | ||
223 | } else if(multiplicity === ALSMultiplicity::SOME) { | ||
224 | return ALSMultiplicity::ONE | ||
225 | } else { | ||
226 | throw new IllegalArgumentException('''Upper multiplicity is already set!''') | ||
227 | } | ||
228 | } | ||
229 | |||
230 | private def <T extends AssertionAnnotation> collectAnnotations(Collection<? extends Annotation> collection, Class<T> annotationKind) { | ||
231 | val res = new HashMap | ||
232 | collection.filter(annotationKind).forEach[res.put(it.target,it)] | ||
233 | return res | ||
234 | } | ||
235 | |||
236 | private def collectConstantDefinitions(LogicProblem problem) { | ||
237 | val res = new HashMap | ||
238 | problem.constants.filter(ConstantDefinition).filter[it.defines!==null].forEach[ | ||
239 | res.put(it.defines,it) | ||
240 | ] | ||
241 | return res | ||
242 | } | ||
243 | private def collectFunctionDefinitions(LogicProblem problem) { | ||
244 | val res = new HashMap | ||
245 | problem.functions.filter(FunctionDefinition).filter[it.defines!==null].forEach[ | ||
246 | res.put(it.defines,it) | ||
247 | ] | ||
248 | return res | ||
249 | } | ||
250 | private def collectRelationDefinitions(LogicProblem problem) { | ||
251 | val res = new HashMap | ||
252 | problem.relations.filter(RelationDefinition).filter[it.defines!==null].forEach[ | ||
253 | res.put(it.defines,it) | ||
254 | ] | ||
255 | return res | ||
256 | } | ||
257 | |||
258 | //////////////////// | ||
259 | // Type References | ||
260 | //////////////////// | ||
261 | def dispatch protected ALSTerm transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyLanguageMapperTrace trace) { | ||
262 | return createALSReference => [ it.referred = support.getBooleanType(trace) ] | ||
263 | } | ||
264 | def dispatch protected ALSTerm transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt } | ||
265 | def dispatch protected ALSTerm transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyLanguageMapperTrace trace) {throw new UnsupportedOperationException('''Real types are not supported in Alloy.''')} | ||
266 | def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { | ||
267 | val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) | ||
268 | return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) | ||
269 | } | ||
270 | |||
271 | ////////////// | ||
272 | // Scopes | ||
273 | ////////////// | ||
274 | |||
275 | def transformRunCommand(ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) { | ||
276 | specification.runCommand = createALSRunCommand => [ | ||
277 | it.typeScopes+= createALSSigScope => [ | ||
278 | it.type= typeMapper.getUndefinedSupertype(trace) | ||
279 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | ||
280 | //it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements) | ||
281 | ] | ||
282 | if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( | ||
283 | '''An integer scope have to be specified for Alloy!''') | ||
284 | it.typeScopes += createALSIntScope => [ | ||
285 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxIntScope) | ||
286 | ] | ||
287 | // for(definedScope : config.typeScopes.allDefinedScope) { | ||
288 | // it.typeScopes += createALSSigScope => [ | ||
289 | // it.type = definedScope.type.lookup(trace.type2ALSType) | ||
290 | // it.number = definedScope.upperLimit | ||
291 | // it.exactly = (definedScope.upperLimit == definedScope.lowerLimit) | ||
292 | // ] | ||
293 | // } | ||
294 | ] | ||
295 | } | ||
296 | |||
297 | |||
298 | ////////////// | ||
299 | // Assertions + Terms | ||
300 | ////////////// | ||
301 | |||
302 | def protected transformAssertion(Assertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
303 | val res = createALSFactDeclaration => [ | ||
304 | it.name = support.toID(assertion.name) | ||
305 | it.term = assertion.value.transformTerm(trace,Collections.EMPTY_MAP) | ||
306 | ] | ||
307 | trace.specification.factDeclarations += res | ||
308 | } | ||
309 | |||
310 | def dispatch protected ALSTerm transformTerm(BoolLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
311 | var ALSEnumLiteral ref; | ||
312 | if(literal.value==true) {ref = support.getBooleanTrue(trace)} | ||
313 | else {ref = support.getBooleanFalse(trace)} | ||
314 | val refFinal = ref | ||
315 | |||
316 | return support.booleanToLogicValue((createALSReference => [referred = refFinal]),trace) | ||
317 | } | ||
318 | def dispatch protected ALSTerm transformTerm(RealLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
319 | throw new UnsupportedOperationException("RealLiteral is not supported") | ||
320 | } | ||
321 | def dispatch protected ALSTerm transformTerm(IntLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
322 | if(literal.value>=0) { createALSNumberLiteral => [value = literal.value]} | ||
323 | else {createALSUnaryMinus => [it.operand = createALSNumberLiteral => [value = literal.value] ] } | ||
324 | } | ||
325 | |||
326 | def dispatch protected ALSTerm transformTerm(Not not, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
327 | createALSNot=>[operand = not.operand.transformTerm(trace,variables)] } | ||
328 | def dispatch protected ALSTerm transformTerm(And and, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
329 | support.unfoldAnd(and.operands.map[transformTerm(trace,variables)]) } | ||
330 | def dispatch protected ALSTerm transformTerm(Or or, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
331 | support.unfoldOr(or.operands.map[transformTerm(trace,variables)],trace) } | ||
332 | def dispatch protected ALSTerm transformTerm(Impl impl, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
333 | createALSImpl => [leftOperand = impl.leftOperand.transformTerm(trace,variables) rightOperand = impl.rightOperand.transformTerm(trace,variables)] } | ||
334 | def dispatch protected ALSTerm transformTerm(Iff iff, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
335 | createALSIff => [leftOperand = iff.leftOperand.transformTerm(trace,variables) rightOperand = iff.rightOperand.transformTerm(trace,variables)] } | ||
336 | def dispatch protected ALSTerm transformTerm(MoreThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
337 | createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } | ||
338 | def dispatch protected ALSTerm transformTerm(LessThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
339 | createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } | ||
340 | def dispatch protected ALSTerm transformTerm(MoreOrEqualThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
341 | createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } | ||
342 | def dispatch protected ALSTerm transformTerm(LessOrEqualThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
343 | createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } | ||
344 | def dispatch protected ALSTerm transformTerm(Equals equals, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
345 | createALSEquals => [leftOperand = equals.leftOperand.transformTerm(trace,variables) rightOperand = equals.rightOperand.transformTerm(trace,variables)] } | ||
346 | def dispatch protected ALSTerm transformTerm(Distinct distinct, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
347 | support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } | ||
348 | |||
349 | def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
350 | createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] } | ||
351 | def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
352 | createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] } | ||
353 | def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
354 | createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] } | ||
355 | def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
356 | createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] } | ||
357 | def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
358 | createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] } | ||
359 | |||
360 | def dispatch protected ALSTerm transformTerm(Forall forall, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
361 | support.createQuantifiedExpression(this,forall,ALSMultiplicity.ALL,trace,variables) } | ||
362 | def dispatch protected ALSTerm transformTerm(Exists exists, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
363 | support.createQuantifiedExpression(this,exists,ALSMultiplicity.SOME,trace,variables) } | ||
364 | |||
365 | def dispatch protected ALSTerm transformTerm(InstanceOf instanceOf, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
366 | return createALSSubset => [ | ||
367 | it.leftOperand = instanceOf.value.transformTerm(trace,variables) | ||
368 | it.rightOperand = instanceOf.range.transformTypeReference(trace) | ||
369 | ] | ||
370 | } | ||
371 | |||
372 | def dispatch protected ALSTerm transformTerm(SymbolicValue symbolicValue, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
373 | symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } | ||
374 | |||
375 | def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
376 | typeMapper.transformReference(referred,trace)} | ||
377 | def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
378 | if(trace.constantDefinitions.containsKey(constant)) { | ||
379 | return this.transformSymbolicReference(constant.lookup(trace.constantDefinitions),parameterSubstitutions,trace,variables) | ||
380 | } else { | ||
381 | val res = createALSJoin=> [ | ||
382 | leftOperand = createALSReference => [ referred = trace.logicLanguage ] | ||
383 | rightOperand = createALSReference => [ referred = constant.lookup(trace.constantDeclaration2LanguageField) ] | ||
384 | ] | ||
385 | return support.postprocessResultOfSymbolicReference(constant.type,res,trace) | ||
386 | } | ||
387 | } | ||
388 | def dispatch protected ALSTerm transformSymbolicReference(ConstantDefinition constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
389 | val res = createALSFunctionCall => [ | ||
390 | it.referredDefinition = constant.lookup(trace.constantDefinition2Function) | ||
391 | ] | ||
392 | return support.postprocessResultOfSymbolicReference(constant.type,res,trace) | ||
393 | } | ||
394 | def dispatch protected ALSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
395 | val res = createALSReference => [referred = variable.lookup(variables)] | ||
396 | return support.postprocessResultOfSymbolicReference(variable.range,res,trace) | ||
397 | } | ||
398 | def dispatch protected ALSTerm transformSymbolicReference(FunctionDeclaration function, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
399 | if(trace.functionDefinitions.containsKey(function)) { | ||
400 | return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) | ||
401 | } else { | ||
402 | if(functionMapper.transformedToHostedField(function,trace)) { | ||
403 | val param = parameterSubstitutions.get(0).transformTerm(trace,variables) | ||
404 | val res = createALSJoin => [ | ||
405 | leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace) | ||
406 | rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)] | ||
407 | ] | ||
408 | return support.postprocessResultOfSymbolicReference(function.range,res,trace) | ||
409 | } else { | ||
410 | val functionExpression = createALSJoin=>[ | ||
411 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
412 | rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)] | ||
413 | ] | ||
414 | val res = support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables) | ||
415 | return support.postprocessResultOfSymbolicReference(function.range,res,trace) | ||
416 | } | ||
417 | } | ||
418 | } | ||
419 | def dispatch protected ALSTerm transformSymbolicReference(FunctionDefinition function, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
420 | val result = createALSFunctionCall => [ | ||
421 | it.referredDefinition = function.lookup(trace.functionDefinition2Function) | ||
422 | it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] | ||
423 | ] | ||
424 | return support.postprocessResultOfSymbolicReference(function.range,result,trace) | ||
425 | } | ||
426 | |||
427 | def dispatch protected ALSTerm transformSymbolicReference(RelationDeclaration relation, List<Term> parameterSubstitutions, | ||
428 | Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
429 | if(trace.relationDefinitions.containsKey(relation)) { | ||
430 | this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),parameterSubstitutions,trace,variables) | ||
431 | } else { | ||
432 | if(relationMapper.transformToHostedField(relation,trace)) { | ||
433 | val alsRelation = relation.lookup(trace.relationDeclaration2Field) | ||
434 | // R(a,b) => | ||
435 | // b in a.R | ||
436 | return createALSSubset => [ | ||
437 | it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace,variables) | ||
438 | it.rightOperand = createALSJoin => [ | ||
439 | it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace,variables) | ||
440 | it.rightOperand = createALSReference => [ it.referred = alsRelation ] | ||
441 | ] | ||
442 | ] | ||
443 | } else { | ||
444 | val target = createALSJoin => [ | ||
445 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
446 | rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]] | ||
447 | val source = support.unfoldTermDirectProduct(this,parameterSubstitutions,trace,variables) | ||
448 | |||
449 | return createALSSubset => [ | ||
450 | leftOperand = source | ||
451 | rightOperand = target | ||
452 | ] | ||
453 | } | ||
454 | } | ||
455 | } | ||
456 | |||
457 | |||
458 | |||
459 | def dispatch protected ALSTerm transformSymbolicReference(RelationDefinition relation, List<Term> parameterSubstitutions, | ||
460 | Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) | ||
461 | { | ||
462 | return createALSFunctionCall => [ | ||
463 | it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) | ||
464 | it.params += parameterSubstitutions.map[p | p.transformTerm(trace,variables)] | ||
465 | ] | ||
466 | } | ||
467 | } \ No newline at end of file | ||