diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner')
5 files changed, 182 insertions, 59 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend index 65539155..b9723d18 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | |||
@@ -1,13 +1,13 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner | 1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner |
2 | 2 | ||
3 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper | 4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper |
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler | 5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler |
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation | 6 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation |
6 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes | 7 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes |
7 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper | 8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper |
8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace | 9 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace |
9 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes | 10 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal |
10 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution | ||
11 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated | 11 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated |
12 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage | 12 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
@@ -16,8 +16,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | |||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
19 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
20 | import java.util.List | ||
21 | 19 | ||
22 | class AlloySolver extends LogicReasoner{ | 20 | class AlloySolver extends LogicReasoner{ |
23 | 21 | ||
@@ -27,7 +25,7 @@ class AlloySolver extends LogicReasoner{ | |||
27 | x.createInjectorAndDoEMFRegistration | 25 | x.createInjectorAndDoEMFRegistration |
28 | } | 26 | } |
29 | 27 | ||
30 | val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes) | 28 | val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal) |
31 | val AlloyHandler handler = new AlloyHandler | 29 | val AlloyHandler handler = new AlloyHandler |
32 | val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper | 30 | val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper |
33 | 31 | ||
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) |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend index 22f49c98..9a16ddf2 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend | |||
@@ -17,6 +17,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | |||
17 | import java.util.HashMap | 17 | import java.util.HashMap |
18 | import java.util.Map | 18 | import java.util.Map |
19 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 19 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
20 | 21 | ||
21 | interface Logic2AlloyLanguageMapper_TypeMapperTrace {} | 22 | interface Logic2AlloyLanguageMapper_TypeMapperTrace {} |
22 | 23 | ||
@@ -39,11 +40,17 @@ class Logic2AlloyLanguageMapperTrace { | |||
39 | public val Map<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2LanguageField = new HashMap | 40 | public val Map<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2LanguageField = new HashMap |
40 | public val Map<FunctionDefinition,ALSFunctionDefinition> functionDefinition2Function = new HashMap | 41 | public val Map<FunctionDefinition,ALSFunctionDefinition> functionDefinition2Function = new HashMap |
41 | 42 | ||
42 | public val Map<RelationDeclaration,ALSFieldDeclaration> relationDeclaration2Global = new HashMap | 43 | public val Map<RelationDeclaration, ALSFieldDeclaration> relationDeclaration2Global = new HashMap |
43 | public val Map<RelationDeclaration, ALSFieldDeclaration> relationDeclaration2Field = new HashMap | 44 | public val Map<RelationDeclaration, ALSFieldDeclaration> relationDeclaration2Field = new HashMap |
44 | public val Map<RelationDefinition,ALSRelationDefinition> relationDefinition2Predicate = new HashMap | 45 | public val Map<RelationDefinition,ALSRelationDefinition> relationDefinition2Predicate = new HashMap |
45 | 46 | ||
47 | public val Map<RelationDeclaration, ALSFieldDeclaration> transitiveClosureTarget2Global = new HashMap | ||
48 | public val Map<RelationDeclaration, ALSFieldDeclaration> transitiveClosureTarget2Field = new HashMap | ||
49 | |||
46 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | 50 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions |
47 | public var Map<FunctionDeclaration, FunctionDefinition> functionDefinitions | 51 | public var Map<FunctionDeclaration, FunctionDefinition> functionDefinitions |
48 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | 52 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions |
53 | |||
54 | public var Map<Relation, ALSFieldDeclaration> relationInTransitiveToGlobalField = new HashMap | ||
55 | public var Map<Relation, ALSFieldDeclaration> relationInTransitiveToHosterField = new HashMap | ||
49 | } \ No newline at end of file | 56 | } \ No newline at end of file |
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 |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend index 4d7b50e8..92ac27df 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend | |||
@@ -30,58 +30,62 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L | |||
30 | } | 30 | } |
31 | 31 | ||
32 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | 32 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { |
33 | if(types.exists[hasDefinedSupertype]) { | 33 | val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal |
34 | throw new UnsupportedOperationException('''Defined supertype is not supported by this type mapping!''') | 34 | trace.typeMapperTrace = typeTrace |
35 | } else { | 35 | |
36 | 36 | // 1. A global type for Objects is created | |
37 | val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal | 37 | val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])] |
38 | trace.typeMapperTrace = typeTrace | 38 | val objectBody = createALSSignatureBody => [ |
39 | it.declarations += objectSig | ||
40 | it.abstract = true | ||
41 | ] | ||
42 | typeTrace.objectSupperClass = objectSig | ||
43 | trace.specification.signatureBodies += objectBody | ||
44 | |||
45 | // 2. Each type is mapped to a unique sig | ||
46 | for(type : types) { | ||
47 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)] | ||
48 | val body = createALSSignatureBody => [it.declarations += sig] | ||
49 | body.abstract = type.isIsAbstract || (type instanceof TypeDefinition) | ||
39 | 50 | ||
40 | // 1. A global type for Objects is created | 51 | trace.specification.signatureBodies += body |
41 | val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])] | 52 | typeTrace.type2ALSType.put(type,sig) |
42 | val objectBody = createALSSignatureBody => [ | ||
43 | it.declarations += objectSig | ||
44 | it.abstract = true | ||
45 | ] | ||
46 | typeTrace.objectSupperClass = objectSig | ||
47 | trace.specification.signatureBodies += objectBody | ||
48 | 53 | ||
49 | // 2. Each type is mapped to a unique sig | 54 | typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)]) |
50 | for(type : types) { | 55 | } |
51 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)] | 56 | |
52 | val body = createALSSignatureBody => [it.declarations += sig] | 57 | for(element : elements) { |
53 | body.abstract = type.isIsAbstract || (type instanceof TypeDefinition) | 58 | val mostSpecificTypes = element.definedInType.filter[it.subtypes.empty] |
54 | 59 | if(mostSpecificTypes.size== 1) { | |
55 | trace.specification.signatureBodies += body | 60 | val mostSpecificSubtype = mostSpecificTypes.head |
56 | typeTrace.type2ALSType.put(type,sig) | 61 | val elementContainer = createALSSignatureBody => [ |
57 | 62 | it.multiplicity = ALSMultiplicity::ONE | |
58 | if(type instanceof TypeDefinition) { | 63 | it.supertype =typeTrace.type2ALSType.get(mostSpecificSubtype) |
59 | val elementContainer = createALSSignatureBody => [it.multiplicity = ALSMultiplicity::ONE it.supertype = sig] | 64 | ] |
60 | for(element : type.elements) { | 65 | val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] |
61 | val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] | 66 | elementContainer.declarations += signature |
62 | elementContainer.declarations += signature | 67 | typeTrace.definedElement2Declaration.put(element,signature) |
63 | 68 | trace.specification.signatureBodies += elementContainer | |
64 | } | 69 | } else { |
65 | trace.specification.signatureBodies += elementContainer | 70 | throw new UnsupportedOperationException |
66 | } | ||
67 | |||
68 | typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)]) | ||
69 | } | 71 | } |
70 | 72 | } | |
71 | // 6. Each inheritance is modeled by extend keyword | 73 | |
72 | for(type : types) { | 74 | // 6. Each inheritance is modeled by extend keyword |
73 | if(type.supertypes.size == 1) { | 75 | for(type : types) { |
74 | val alsType = typeTrace.type2ALSType.get(type.supertypes.head) | 76 | if(type.supertypes.size == 0) { |
75 | (type.eContainer as ALSSignatureBody).supertype = alsType | 77 | (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = typeTrace.objectSupperClass |
76 | } else if(type.supertypes.size > 1){ | 78 | }if(type.supertypes.size == 1) { |
77 | val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head) | 79 | val alsType = typeTrace.type2ALSType.get(type.supertypes.head) |
78 | (type.eContainer as ALSSignatureBody).supertype = alsMainType | 80 | (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsType |
79 | for(otherType : type.supertypes.filter[it != alsMainType]) { | 81 | |
80 | typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(otherType)) | 82 | } else if(type.supertypes.size > 1){ |
81 | } | 83 | val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head) |
84 | (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsMainType | ||
85 | for(otherType : type.supertypes.filter[it != alsMainType]) { | ||
86 | typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(type)) | ||
82 | } | 87 | } |
83 | } | 88 | } |
84 | |||
85 | } | 89 | } |
86 | } | 90 | } |
87 | 91 | ||
@@ -114,7 +118,8 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L | |||
114 | } | 118 | } |
115 | 119 | ||
116 | override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { | 120 | override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { |
117 | createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(referred)] | 121 | val r = trace.typeTrace.definedElement2Declaration.get(referred) |
122 | return createALSReference => [it.referred =r] | ||
118 | } | 123 | } |
119 | 124 | ||
120 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { | 125 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { |