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