From 79eb47516a27ebe1801fb8e9087f3ee1b4d123d1 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 27 Aug 2019 18:45:22 +0200 Subject: Alloy RunCommand int scope fix candidate --- .../alloy/reasoner/builder/RunCommandMapper.xtend | 123 ++++++++++++++------- 1 file changed, 86 insertions(+), 37 deletions(-) (limited to 'Solvers/Alloy-Solver') diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend index 3e96f7f4..cbd56abb 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend @@ -3,6 +3,8 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration @@ -13,15 +15,15 @@ import java.util.List import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class RunCommandMapper { - private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE - private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; - private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; + val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + val Logic2AlloyLanguageMapper_TypeMapper typeMapper; - public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { + new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { this.typeMapper = typeMapper } - def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) + def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) { //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size @@ -65,41 +67,88 @@ class RunCommandMapper { it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) ] - if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { - val integersUsed = specification.eAllContents.filter(ALSInt) - if(integersUsed.empty) { - // If no integer scope is defined, but the problem has no integers - // => scope can be empty - it.typeScopes+= createALSIntScope => [ - it.number = 0 - ] - } else { - // If no integer scope is defined, and the problem has integers - // => error - throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') - } + setIntegerScope(specification,config,it) + setStringScope(specification,config,it) + ] + } + + protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { + if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { + throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') + } else { + if(config.typeScopes.maxNewStrings == 0) { + it.typeScopes += createALSStringScope => [it.number = 0] } else { - it.typeScopes += createALSIntScope => [ - if(config.typeScopes.knownIntegers.empty) { - number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) - } else { - var scope = Math.max( - Math.abs(config.typeScopes.knownIntegers.max), - Math.abs(config.typeScopes.knownIntegers.min)) - if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { - scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 - } - number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 - } - ] + throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') } - if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { - throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') + } + } + + protected def setIntegerScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand command) { + //AlloySolverConfiguration config, ALSRunCommand it + + // If the scope is unlimited ... + if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { + val integersUsed = specification.eAllContents.filter(ALSInt) + if(integersUsed.empty) { + // ... but the problem has no integers => scope can be empty + command.typeScopes+= createALSIntScope => [ it.number = 0 ] } else { - if(config.typeScopes.maxNewStrings != 0) { - it.typeScopes += createALSStringScope => [it.number = 0] - } + // If no integer scope is defined, and the problem has integers => error + throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') } - ] + } else { + // If the scope is limited, collect the integers in the problem and the scope,... + val maxIntScope = config.typeScopes.maxNewIntegers + val minIntScope = config.typeScopes.minNewIntegers + val knownIntegers = config.typeScopes.knownIntegers + val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value] + // And select the range of integers + val min = #[minIntScope,knownIntegers.min,integersInProblem.min].min + val max = #[maxIntScope,knownIntegers.max,integersInProblem.max].max + //val abs = Math.max(Math.abs(min),Math.abs(max)) + + + command.typeScopes += createALSIntScope => [ + it.number = toBits(min, max) + ] + } + +// if(config.typeScopes.knownIntegers.empty) { +// return Integer.SIZE-Integer.numberOfLeadingZeros((config.typeScopes.maxNewIntegers+1)/2) +// } else { +// var scope = Math.max( +// Math.abs(config.typeScopes.knownIntegers.max), +// Math.abs(config.typeScopes.knownIntegers.min)) +// if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { +// scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 +// } +// return Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 +// } + } + + private static def toBits(int min, int max) { + // 4 Int = {-8, ..., 7} + // x Int = {- (2^(x-1)) , ... , 2^(x-1)-1} + var int bits = 1 + // range = 2^(x-1) + var int range = 1 + while((!(-range <= min)) || (!(max <= range-1))) { + bits++ + range*=2 + } + return bits } +// +// def static void main(String[] args) { +// println('''0,0->«toBits(0,0)»''') +// println('''1,1->«toBits(1,1)»''') +// println('''-1,-1->«toBits(-1,-1)»''') +// println('''5,6->«toBits(5,6)»''') +// println('''0,6->«toBits(0,6)»''') +// println('''-10,0->«toBits(-10,0)»''') +// println('''-8,7->«toBits(-8,7)»''') +// println('''-100,100->«toBits(-100,100)»''') +// println('''-300,300->«toBits(-300,300)»''') +// } } \ No newline at end of file -- cgit v1.2.3-70-g09d2 From 98fc5c726a87677cde3a7a67e599d642fbce781d Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Fri, 30 Aug 2019 14:32:37 +0200 Subject: Whitespacing in manifest updated --- .../META-INF/MANIFEST.MF | 24 +++++++++++----------- 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'Solvers/Alloy-Solver') diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF index 87ff7abc..b944302b 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF @@ -4,22 +4,22 @@ Bundle-Name: %pluginName Bundle-SymbolicName: hu.bme.mit.inf.dlsreasoner.alloy.reasoner;singleton:=true Bundle-Version: 1.0.0.qualifier Bundle-ClassPath: lib/alloy4.2_2015-02-22.jar, - . + . Bundle-Vendor: %providerName Bundle-Localization: plugin Export-Package: hu.bme.mit.inf.dlsreasoner.alloy.reasoner, - hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder, - hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries + hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder, + hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries Require-Bundle: com.google.guava, - org.eclipse.xtend.lib, - org.eclipse.xtext.xbase.lib, - org.eclipse.core.runtime, - org.eclipse.emf.ecore;visibility:=reexport, - hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport, - hu.bme.mit.inf.dslreasoner.alloy.language;bundle-version="1.0.0", - org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.3.0", - hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", - org.eclipse.viatra.query.runtime;bundle-version="2.0.0" + org.eclipse.xtend.lib, + org.eclipse.xtext.xbase.lib, + org.eclipse.core.runtime, + org.eclipse.emf.ecore;visibility:=reexport, + hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport, + hu.bme.mit.inf.dslreasoner.alloy.language;bundle-version="1.0.0", + org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.3.0", + hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", + org.eclipse.viatra.query.runtime;bundle-version="2.0.0" Import-Package: org.apache.log4j;version="1.2.15" Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner Bundle-ActivationPolicy: lazy -- cgit v1.2.3-70-g09d2 From 49c349e361c5c026334c566a1f8b3357056f4e6e Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Fri, 30 Aug 2019 14:33:06 +0200 Subject: scopes added to alloy --- .../Logic2AlloyLanguageMapper_RelationMapper.xtend | 13 ++- ...ogic2AlloyLanguageMapper_TypeScopeMapping.xtend | 44 +++++++++ .../alloy/reasoner/builder/RunCommandMapper.xtend | 102 +++++++++++++++------ 3 files changed, 124 insertions(+), 35 deletions(-) create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend (limited to 'Solvers/Alloy-Solver') 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 { public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { if(relation.parameters.size === 2) { /** 1. Create a relation that can be used in ^relation expressions */ - val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace) + val declaration = this.createRelationDeclaration(support.toID('''AsDeclaration «relation.name»'''),relation.parameters,trace) trace.relationInTransitiveToHosterField.put(relation,declaration) /** 2. Add fact that the declaration corresponds to the definition */ val fact = createALSFactDeclaration => [ - it.name = '''EqualsAsDeclaration «relation.name»''' + it.name = support.toID('''EqualsAsDeclaration «relation.name»''') it.term = createALSQuantifiedEx => [ val a = createALSVariableDeclaration => [ it.name = "a" @@ -157,7 +157,7 @@ class Logic2AlloyLanguageMapper_RelationMapper { it.params += createALSReference => [ it.referred = b ] ] it.rightOperand = createALSSubset => [ - it.leftOperand = createALSJoin => [ + it.leftOperand = createALSDirectProduct => [ it.leftOperand = createALSReference => [ referred = a ] it.rightOperand = createALSReference => [ referred = b ] ] @@ -183,12 +183,15 @@ class Logic2AlloyLanguageMapper_RelationMapper { rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] ] } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ - createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] + createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] + ] } else { throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') } return createALSSubset => [ - it.leftOperand = createALSJoin => [ + it.leftOperand = createALSDirectProduct => [ it.leftOperand = source it.rightOperand = target ] diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend new file mode 100644 index 00000000..a270cb73 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend @@ -0,0 +1,44 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory + +interface Logic2AlloyLanguageMapper_TypeScopeMapping { + def void addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) + def void addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) +} + +class Logic2AlloyLanguageMapper_AsConstraint implements Logic2AlloyLanguageMapper_TypeScopeMapping { + val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + val Logic2AlloyLanguageMapper_TypeMapper typeMapper + + new(Logic2AlloyLanguageMapper_TypeMapper mapper) { + this.typeMapper = mapper + } + + override addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { + document.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["LowerMultiplicity",support.toID(type.name),lowerMultiplicty.toString]) + it.term = createALSLeq => [ + it.leftOperand = createALSCardinality => [ + it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) + ] + it.rightOperand = createALSNumberLiteral => [it.value = lowerMultiplicty] + ] + ] + } + + override addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { + document.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["UpperMultiplicity",support.toID(type.name),upperMultiplicty.toString]) + it.term = createALSMeq => [ + it.leftOperand = createALSCardinality => [ + it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) + ] + it.rightOperand = createALSNumberLiteral => [it.value = upperMultiplicty] + ] + ] + } +} \ 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/RunCommandMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend index cbd56abb..494197bc 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend @@ -5,22 +5,21 @@ import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition -import java.util.LinkedList import java.util.List -import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* - class RunCommandMapper { val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; val Logic2AlloyLanguageMapper_TypeMapper typeMapper; + val Logic2AlloyLanguageMapper_TypeScopeMapping typeScopeMapping; new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { this.typeMapper = typeMapper + this.typeScopeMapping = new Logic2AlloyLanguageMapper_AsConstraint(typeMapper) } def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) @@ -38,28 +37,47 @@ class RunCommandMapper { it.term = support.unfoldAnd(equals) ] } - val typeScopes = new LinkedList - for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) { - val key = definedScope.key - val amount = definedScope.value - val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount - - val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet - if(amount == 0 && exactly) { - specification.factDeclarations += createALSFactDeclaration => [ - it.term = createALSEquals => [ - it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) - it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) - ] + + /* + val upperLimits = new LinkedList + val lowerLimits = new LinkedList + + /*val typesWithScopeConstraint = config.typeScopes.maxNewElementsByType.keySet + config.typeScopes.minNewElementsByType.keySet + for(type : typesWithScopeConstraint) { + val max = if(config.typeScopes.maxNewElementsByType.containsKey(type)) { + config.typeScopes.maxNewElementsByType.get(type) + } else { + LogicSolverConfiguration::Unlimited + } + val min = if(config.typeScopes.minNewElementsByType.containsKey(type)) { + config.typeScopes.minNewElementsByType.get(type) + } else { + 0 + } + + val exactly = min === max + + if(max === 0) { + val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet + specification.factDeclarations += createALSFactDeclaration => [ + it.term = createALSEquals => [ + it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) + it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) ] - } - val int n = existing.size-amount - typeScopes += createALSSigScope => [ - it.type = typeMapper.transformTypeReference(key,mapper,trace).head - it.number = n + ] + } else if(max !== LogicSolverConfiguration::Unlimited) { + upperLimits += createALSSigScope => [ + it.type = typeMapper.transformTypeReference(type,mapper,trace).head + it.number = max it.exactly =exactly ] + } else { + // do nothing + } + if(min != 0 && ! exactly) { + lowerLimits += type->min } + }*/ specification.runCommand = createALSRunCommand => [ it.typeScopes+= createALSSigScope => [ @@ -67,9 +85,25 @@ class RunCommandMapper { it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) ] - setIntegerScope(specification,config,it) - setStringScope(specification,config,it) + ] + + for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) { + val limit = upperLimit.value + if(limit != LogicSolverConfiguration::Unlimited) { + this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace) + } + } + + for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) { + val limit = lowerLimit.value + if(limit != 0) { + this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace) + } + } + + setIntegerScope(specification,config,specification.runCommand) + setStringScope(specification,config,specification.runCommand) } protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { @@ -79,7 +113,11 @@ class RunCommandMapper { if(config.typeScopes.maxNewStrings == 0) { it.typeScopes += createALSStringScope => [it.number = 0] } else { - throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') + if(specification.eAllContents.filter(ALSString).empty) { + it.typeScopes += createALSStringScope => [it.number = 0] + } else { + throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') + } } } } @@ -99,13 +137,17 @@ class RunCommandMapper { } } else { // If the scope is limited, collect the integers in the problem and the scope,... - val maxIntScope = config.typeScopes.maxNewIntegers - val minIntScope = config.typeScopes.minNewIntegers + //val maxIntScope = config.typeScopes.maxNewIntegers + //val minIntScope = config.typeScopes.minNewIntegers val knownIntegers = config.typeScopes.knownIntegers - val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value] + val minKnownInteger = if(knownIntegers.empty) { Integer.MAX_VALUE } else { knownIntegers.min } + val maxKnownInteger = if(knownIntegers.empty) { Integer.MIN_VALUE } else { knownIntegers.max } + val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value].toList + val minIntegerInProblem = if(integersInProblem.empty) { Integer.MAX_VALUE } else { integersInProblem.min } + val maxIntegerInProblem = if(integersInProblem.empty) { Integer.MIN_VALUE } else { integersInProblem.max } // And select the range of integers - val min = #[minIntScope,knownIntegers.min,integersInProblem.min].min - val max = #[maxIntScope,knownIntegers.max,integersInProblem.max].max + val min = #[minKnownInteger,minIntegerInProblem].min + val max = #[maxKnownInteger,maxIntegerInProblem].max //val abs = Math.max(Math.abs(min),Math.abs(max)) -- cgit v1.2.3-70-g09d2