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 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-54-g00ecf