diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend index 0762efce..8de9688b 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 | |||
@@ -133,11 +133,11 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
133 | public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { | 133 | public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { |
134 | if(relation.parameters.size === 2) { | 134 | if(relation.parameters.size === 2) { |
135 | /** 1. Create a relation that can be used in ^relation expressions */ | 135 | /** 1. Create a relation that can be used in ^relation expressions */ |
136 | val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace) | 136 | val declaration = this.createRelationDeclaration(support.toID('''AsDeclaration «relation.name»'''),relation.parameters,trace) |
137 | trace.relationInTransitiveToHosterField.put(relation,declaration) | 137 | trace.relationInTransitiveToHosterField.put(relation,declaration) |
138 | /** 2. Add fact that the declaration corresponds to the definition */ | 138 | /** 2. Add fact that the declaration corresponds to the definition */ |
139 | val fact = createALSFactDeclaration => [ | 139 | val fact = createALSFactDeclaration => [ |
140 | it.name = '''EqualsAsDeclaration «relation.name»''' | 140 | it.name = support.toID('''EqualsAsDeclaration «relation.name»''') |
141 | it.term = createALSQuantifiedEx => [ | 141 | it.term = createALSQuantifiedEx => [ |
142 | val a = createALSVariableDeclaration => [ | 142 | val a = createALSVariableDeclaration => [ |
143 | it.name = "a" | 143 | it.name = "a" |
@@ -157,7 +157,7 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
157 | it.params += createALSReference => [ it.referred = b ] | 157 | it.params += createALSReference => [ it.referred = b ] |
158 | ] | 158 | ] |
159 | it.rightOperand = createALSSubset => [ | 159 | it.rightOperand = createALSSubset => [ |
160 | it.leftOperand = createALSJoin => [ | 160 | it.leftOperand = createALSDirectProduct => [ |
161 | it.leftOperand = createALSReference => [ referred = a ] | 161 | it.leftOperand = createALSReference => [ referred = a ] |
162 | it.rightOperand = createALSReference => [ referred = b ] | 162 | it.rightOperand = createALSReference => [ referred = b ] |
163 | ] | 163 | ] |
@@ -183,12 +183,15 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
183 | rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] | 183 | rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] |
184 | ] | 184 | ] |
185 | } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ | 185 | } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ |
186 | createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] | 186 | createALSJoin => [ |
187 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
188 | rightOperand = createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] | ||
189 | ] | ||
187 | } else { | 190 | } else { |
188 | throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') | 191 | throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') |
189 | } | 192 | } |
190 | return createALSSubset => [ | 193 | return createALSSubset => [ |
191 | it.leftOperand = createALSJoin => [ | 194 | it.leftOperand = createALSDirectProduct => [ |
192 | it.leftOperand = source | 195 | it.leftOperand = source |
193 | it.rightOperand = target | 196 | it.rightOperand = target |
194 | ] | 197 | ] |