diff options
author | 2018-11-07 12:19:47 +0100 | |
---|---|---|
committer | 2018-11-07 12:19:47 +0100 | |
commit | eccbce5001c00413805037bc416bb14e97390c3c (patch) | |
tree | 9eb2c43d5dce6c747581c1cf901e71aae3babde9 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | |
parent | Attributes are filled in instance models (diff) | |
download | VIATRA-Generator-eccbce5001c00413805037bc416bb14e97390c3c.tar.gz VIATRA-Generator-eccbce5001c00413805037bc416bb14e97390c3c.tar.zst VIATRA-Generator-eccbce5001c00413805037bc416bb14e97390c3c.zip |
Fixes in string scope and string interpretation for 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 | 83 |
1 files changed, 5 insertions, 78 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 1076019f..3fc3971d 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 | |||
@@ -12,7 +12,6 @@ import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | |||
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | 12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion |
13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | 13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion |
14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | 14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion |
@@ -48,6 +47,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | |||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | 47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference |
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 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 | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | 52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue |
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | 53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term |
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure | 54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure |
@@ -65,14 +66,11 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope | |||
65 | import org.eclipse.xtend.lib.annotations.Accessors | 66 | import org.eclipse.xtend.lib.annotations.Accessors |
66 | 67 | ||
67 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 68 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
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 | ||
72 | 69 | ||
73 | class Logic2AlloyLanguageMapper { | 70 | class Logic2AlloyLanguageMapper { |
74 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 71 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
75 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | 72 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; |
73 | private val RunCommandMapper runCommandMapper | ||
76 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | 74 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; |
77 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this) | 75 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this) |
78 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this) | 76 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this) |
@@ -81,6 +79,7 @@ class Logic2AlloyLanguageMapper { | |||
81 | 79 | ||
82 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | 80 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { |
83 | this.typeMapper = typeMapper | 81 | this.typeMapper = typeMapper |
82 | this.runCommandMapper = new RunCommandMapper(typeMapper) | ||
84 | } | 83 | } |
85 | 84 | ||
86 | public def TracedOutput<ALSDocument,Logic2AlloyLanguageMapperTrace> transformProblem(LogicProblem problem, AlloySolverConfiguration config) { | 85 | public def TracedOutput<ALSDocument,Logic2AlloyLanguageMapperTrace> transformProblem(LogicProblem problem, AlloySolverConfiguration config) { |
@@ -146,7 +145,7 @@ class Logic2AlloyLanguageMapper { | |||
146 | } | 145 | } |
147 | } | 146 | } |
148 | 147 | ||
149 | transformRunCommand(specification, trace, config) | 148 | runCommandMapper.transformRunCommand(this, specification, trace, config) |
150 | 149 | ||
151 | return new TracedOutput(specification,trace) | 150 | return new TracedOutput(specification,trace) |
152 | } | 151 | } |
@@ -303,78 +302,6 @@ class Logic2AlloyLanguageMapper { | |||
303 | def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { | 302 | def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { |
304 | val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) | 303 | val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) |
305 | return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) | 304 | return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) |
306 | } | ||
307 | |||
308 | ////////////// | ||
309 | // Scopes | ||
310 | ////////////// | ||
311 | |||
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 | |||
328 | specification.runCommand = createALSRunCommand => [ | ||
329 | it.typeScopes+= createALSSigScope => [ | ||
330 | it.type= typeMapper.getUndefinedSupertype(trace) | ||
331 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | ||
332 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | ||
333 | ] | ||
334 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | ||
335 | val integersUsed = specification.eAllContents.filter(ALSInt) | ||
336 | if(integersUsed.empty) { | ||
337 | // If no integer scope is defined, but the problem has no integers | ||
338 | // => scope can be empty | ||
339 | it.typeScopes+= createALSIntScope => [ | ||
340 | it.number = 0 | ||
341 | ] | ||
342 | } else { | ||
343 | // If no integer scope is defined, and the problem has integers | ||
344 | // => error | ||
345 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') | ||
346 | } | ||
347 | } else { | ||
348 | it.typeScopes += createALSIntScope => [ | ||
349 | if(config.typeScopes.knownIntegers.empty) { | ||
350 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | ||
351 | } else { | ||
352 | var scope = Math.max( | ||
353 | Math.abs(config.typeScopes.knownIntegers.max), | ||
354 | Math.abs(config.typeScopes.knownIntegers.min)) | ||
355 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
356 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
357 | } | ||
358 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 | ||
359 | } | ||
360 | ] | ||
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 | |||
370 | // for(definedScope : config.typeScopes.allDefinedScope) { | ||
371 | // it.typeScopes += createALSSigScope => [ | ||
372 | // it.type = definedScope.type.lookup(trace.type2ALSType) | ||
373 | // it.number = definedScope.upperLimit | ||
374 | // it.exactly = (definedScope.upperLimit == definedScope.lowerLimit) | ||
375 | // ] | ||
376 | // } | ||
377 | ] | ||
378 | } | 305 | } |
379 | 306 | ||
380 | ////////////// | 307 | ////////////// |