diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-09-27 17:40:00 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-09-27 17:40:00 +0200 |
commit | 53bfa0734fff9a70b992d6effde3a6cbac9ea946 (patch) | |
tree | 7c510f811144cfb0f8e50d083a1b87f28fbc7bdd /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | |
parent | String attributes are not mapped. (diff) | |
download | VIATRA-Generator-53bfa0734fff9a70b992d6effde3a6cbac9ea946.tar.gz VIATRA-Generator-53bfa0734fff9a70b992d6effde3a6cbac9ea946.tar.zst VIATRA-Generator-53bfa0734fff9a70b992d6effde3a6cbac9ea946.zip |
Transitive closure support for relation definitions in Alloy
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 | 31 |
1 files changed, 28 insertions, 3 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 index ee2f49ed..d6c62f54 100644 --- 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 | |||
@@ -64,6 +64,8 @@ import java.util.Collection | |||
64 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | 64 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion |
65 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | 65 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion |
66 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct | 66 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct |
67 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure | ||
68 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
67 | 69 | ||
68 | class Logic2AlloyLanguageMapper { | 70 | class Logic2AlloyLanguageMapper { |
69 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 71 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
@@ -102,10 +104,12 @@ class Logic2AlloyLanguageMapper { | |||
102 | trace.constantDefinitions = problem.collectConstantDefinitions | 104 | trace.constantDefinitions = problem.collectConstantDefinitions |
103 | trace.functionDefinitions = problem.collectFunctionDefinitions | 105 | trace.functionDefinitions = problem.collectFunctionDefinitions |
104 | trace.relationDefinitions = problem.collectRelationDefinitions | 106 | trace.relationDefinitions = problem.collectRelationDefinitions |
107 | val calledInTransitiveClosure = problem.collectTransitiveRelationCalls | ||
105 | 108 | ||
106 | problem.constants.forEach[this.constantMapper.transformConstant(it,trace)] | 109 | problem.constants.forEach[this.constantMapper.transformConstant(it, trace)] |
107 | problem.functions.forEach[this.functionMapper.transformFunction(it, trace)] | 110 | problem.functions.forEach[this.functionMapper.transformFunction(it, trace)] |
108 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] | 111 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] |
112 | calledInTransitiveClosure.forEach[this.relationMapper.prepareTransitiveClosure(it, trace)] | ||
109 | 113 | ||
110 | problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstantDefinitionSpecification(it,trace)] | 114 | problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstantDefinitionSpecification(it,trace)] |
111 | problem.functions.filter(FunctionDefinition).forEach[this.functionMapper.transformFunctionDefinitionSpecification(it,trace)] | 115 | problem.functions.filter(FunctionDefinition).forEach[this.functionMapper.transformFunctionDefinitionSpecification(it,trace)] |
@@ -143,6 +147,8 @@ class Logic2AlloyLanguageMapper { | |||
143 | return new TracedOutput(specification,trace) | 147 | return new TracedOutput(specification,trace) |
144 | } | 148 | } |
145 | 149 | ||
150 | |||
151 | |||
146 | def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | 152 | def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { |
147 | val a = assertion.inverseA | 153 | val a = assertion.inverseA |
148 | val b = assertion.inverseB | 154 | val b = assertion.inverseB |
@@ -213,15 +219,21 @@ class Logic2AlloyLanguageMapper { | |||
213 | return ALSMultiplicity::SOME | 219 | return ALSMultiplicity::SOME |
214 | } else if(multiplicity === ALSMultiplicity::LONE) { | 220 | } else if(multiplicity === ALSMultiplicity::LONE) { |
215 | return ALSMultiplicity::ONE | 221 | return ALSMultiplicity::ONE |
222 | } else if(multiplicity == ALSMultiplicity::ONE) { | ||
223 | return ALSMultiplicity::ONE | ||
216 | } else { | 224 | } else { |
217 | throw new IllegalArgumentException('''Lower multiplicity is already set!''') | 225 | throw new IllegalArgumentException('''Lower multiplicity is already set!''') |
218 | } | 226 | } |
219 | } | 227 | } |
220 | private def addUpper(ALSMultiplicity multiplicity) { | 228 | private def addUpper(ALSMultiplicity multiplicity) { |
221 | if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { | 229 | if(multiplicity === ALSMultiplicity::ALL) { |
230 | return ALSMultiplicity::LONE | ||
231 | } else if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { | ||
222 | return ALSMultiplicity::LONE | 232 | return ALSMultiplicity::LONE |
223 | } else if(multiplicity === ALSMultiplicity::SOME) { | 233 | } else if(multiplicity === ALSMultiplicity::SOME) { |
224 | return ALSMultiplicity::ONE | 234 | return ALSMultiplicity::ONE |
235 | } else if(multiplicity == ALSMultiplicity::ONE) { | ||
236 | return ALSMultiplicity::ONE | ||
225 | } else { | 237 | } else { |
226 | throw new IllegalArgumentException('''Upper multiplicity is already set!''') | 238 | throw new IllegalArgumentException('''Upper multiplicity is already set!''') |
227 | } | 239 | } |
@@ -254,6 +266,9 @@ class Logic2AlloyLanguageMapper { | |||
254 | ] | 266 | ] |
255 | return res | 267 | return res |
256 | } | 268 | } |
269 | private def collectTransitiveRelationCalls(LogicProblem problem) { | ||
270 | return problem.eAllContents.filter(TransitiveClosure).map[it.relation].toSet | ||
271 | } | ||
257 | 272 | ||
258 | //////////////////// | 273 | //////////////////// |
259 | // Type References | 274 | // Type References |
@@ -380,11 +395,21 @@ class Logic2AlloyLanguageMapper { | |||
380 | ] | 395 | ] |
381 | } | 396 | } |
382 | 397 | ||
398 | def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
399 | return this.relationMapper.transformTransitiveRelationReference( | ||
400 | tc.relation, | ||
401 | tc.leftOperand.transformTerm(trace,variables), | ||
402 | tc.rightOperand.transformTerm(trace,variables), | ||
403 | trace | ||
404 | ) | ||
405 | } | ||
406 | |||
383 | def dispatch protected ALSTerm transformTerm(SymbolicValue symbolicValue, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | 407 | def dispatch protected ALSTerm transformTerm(SymbolicValue symbolicValue, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { |
384 | symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } | 408 | symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } |
385 | 409 | ||
386 | def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | 410 | def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { |
387 | typeMapper.transformReference(referred,trace)} | 411 | typeMapper.transformReference(referred,trace) |
412 | } | ||
388 | def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | 413 | def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { |
389 | if(trace.constantDefinitions.containsKey(constant)) { | 414 | if(trace.constantDefinitions.containsKey(constant)) { |
390 | return this.transformSymbolicReference(constant.lookup(trace.constantDefinitions),parameterSubstitutions,trace,variables) | 415 | return this.transformSymbolicReference(constant.lookup(trace.constantDefinitions),parameterSubstitutions,trace,variables) |