diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder')
2 files changed, 43 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/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend index abedf9e4..95216835 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend | |||
@@ -177,6 +177,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
177 | else if(label == this.logicBooleanTrue) return true | 177 | else if(label == this.logicBooleanTrue) return true |
178 | else if(label == this.logicBooleanFalse) return false | 178 | else if(label == this.logicBooleanFalse) return false |
179 | else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement) | 179 | else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement) |
180 | else if(label.isString) return parseString(label) | ||
180 | else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''') | 181 | else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''') |
181 | } | 182 | } |
182 | def private isNumber(String s) { | 183 | def private isNumber(String s) { |
@@ -187,6 +188,12 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
187 | return false | 188 | return false |
188 | } | 189 | } |
189 | } | 190 | } |
191 | def private isString(String label) { | ||
192 | label.startsWith("\"") && label.endsWith("\"") | ||
193 | } | ||
194 | def private parseString(String label) { | ||
195 | label.substring(1,label.length-1) | ||
196 | } | ||
190 | 197 | ||
191 | override getAllIntegersInStructure() { | 198 | override getAllIntegersInStructure() { |
192 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 199 | throw new UnsupportedOperationException("TODO: auto-generated method stub") |
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 4ecebb62..1076019f 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 | |||
@@ -66,6 +66,9 @@ import org.eclipse.xtend.lib.annotations.Accessors | |||
66 | 66 | ||
67 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 67 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
68 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt | 68 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt |
69 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference | ||
70 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral | ||
71 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSStringLiteral | ||
69 | 72 | ||
70 | class Logic2AlloyLanguageMapper { | 73 | class Logic2AlloyLanguageMapper { |
71 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 74 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
@@ -295,7 +298,8 @@ class Logic2AlloyLanguageMapper { | |||
295 | return createALSReference => [ it.referred = support.getBooleanType(trace) ] | 298 | return createALSReference => [ it.referred = support.getBooleanType(trace) ] |
296 | } | 299 | } |
297 | def dispatch protected ALSTerm transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt } | 300 | def dispatch protected ALSTerm transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt } |
298 | def dispatch protected ALSTerm transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyLanguageMapperTrace trace) {throw new UnsupportedOperationException('''Real types are not supported in Alloy.''')} | 301 | def dispatch protected ALSTerm transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt } |
302 | def dispatch protected ALSTerm transformTypeReference(StringTypeReference stringTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSString } | ||
299 | def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { | 303 | def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { |
300 | val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) | 304 | val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) |
301 | return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) | 305 | return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) |
@@ -305,7 +309,22 @@ class Logic2AlloyLanguageMapper { | |||
305 | // Scopes | 309 | // Scopes |
306 | ////////////// | 310 | ////////////// |
307 | 311 | ||
308 | def transformRunCommand(ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) { | 312 | def transformRunCommand(ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) |
313 | { | ||
314 | val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size | ||
315 | |||
316 | // add fact to ensure the existence of all literals in the scope | ||
317 | if(!config.typeScopes.knownStrings.empty) { | ||
318 | specification.factDeclarations += createALSFactDeclaration => [ | ||
319 | it.name = "EnsureAllStrings" | ||
320 | val List<? extends ALSTerm> equals = config.typeScopes.knownStrings.map[x|createALSEquals => [ | ||
321 | it.leftOperand =createALSStringLiteral => [it.value = x] | ||
322 | it.rightOperand =createALSStringLiteral => [it.value = x] | ||
323 | ]].toList | ||
324 | it.term = support.unfoldAnd(equals) | ||
325 | ] | ||
326 | } | ||
327 | |||
309 | specification.runCommand = createALSRunCommand => [ | 328 | specification.runCommand = createALSRunCommand => [ |
310 | it.typeScopes+= createALSSigScope => [ | 329 | it.typeScopes+= createALSSigScope => [ |
311 | it.type= typeMapper.getUndefinedSupertype(trace) | 330 | it.type= typeMapper.getUndefinedSupertype(trace) |
@@ -336,10 +355,18 @@ class Logic2AlloyLanguageMapper { | |||
336 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | 355 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { |
337 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | 356 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 |
338 | } | 357 | } |
339 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope) | 358 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 |
340 | } | 359 | } |
341 | ] | 360 | ] |
342 | } | 361 | } |
362 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | ||
363 | throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') | ||
364 | } else { | ||
365 | if(config.typeScopes.maxNewStrings != 0) { | ||
366 | it.typeScopes += createALSStringScope => [it.number = config.typeScopes.maxNewStrings - knownStringNumber] | ||
367 | } | ||
368 | } | ||
369 | |||
343 | // for(definedScope : config.typeScopes.allDefinedScope) { | 370 | // for(definedScope : config.typeScopes.allDefinedScope) { |
344 | // it.typeScopes += createALSSigScope => [ | 371 | // it.typeScopes += createALSSigScope => [ |
345 | // it.type = definedScope.type.lookup(trace.type2ALSType) | 372 | // it.type = definedScope.type.lookup(trace.type2ALSType) |
@@ -350,7 +377,6 @@ class Logic2AlloyLanguageMapper { | |||
350 | ] | 377 | ] |
351 | } | 378 | } |
352 | 379 | ||
353 | |||
354 | ////////////// | 380 | ////////////// |
355 | // Assertions + Terms | 381 | // Assertions + Terms |
356 | ////////////// | 382 | ////////////// |
@@ -372,12 +398,17 @@ class Logic2AlloyLanguageMapper { | |||
372 | return support.booleanToLogicValue((createALSReference => [referred = refFinal]),trace) | 398 | return support.booleanToLogicValue((createALSReference => [referred = refFinal]),trace) |
373 | } | 399 | } |
374 | def dispatch protected ALSTerm transformTerm(RealLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | 400 | def dispatch protected ALSTerm transformTerm(RealLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { |
375 | throw new UnsupportedOperationException("RealLiteral is not supported") | 401 | val v = literal.value.intValue |
402 | if(v>=0) { createALSNumberLiteral => [value = v]} | ||
403 | else {createALSUnaryMinus => [it.operand = createALSNumberLiteral => [value = v] ] } | ||
376 | } | 404 | } |
377 | def dispatch protected ALSTerm transformTerm(IntLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | 405 | def dispatch protected ALSTerm transformTerm(IntLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { |
378 | if(literal.value>=0) { createALSNumberLiteral => [value = literal.value]} | 406 | if(literal.value>=0) { createALSNumberLiteral => [value = literal.value]} |
379 | else {createALSUnaryMinus => [it.operand = createALSNumberLiteral => [value = literal.value] ] } | 407 | else {createALSUnaryMinus => [it.operand = createALSNumberLiteral => [value = literal.value] ] } |
380 | } | 408 | } |
409 | def dispatch protected ALSTerm transformTerm(StringLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
410 | createALSStringLiteral => [it.value = literal.value] | ||
411 | } | ||
381 | 412 | ||
382 | def dispatch protected ALSTerm transformTerm(Not not, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | 413 | def dispatch protected ALSTerm transformTerm(Not not, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { |
383 | createALSNot=>[operand = not.operand.transformTerm(trace,variables)] } | 414 | createALSNot=>[operand = not.operand.transformTerm(trace,variables)] } |