From eccbce5001c00413805037bc416bb14e97390c3c Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 7 Nov 2018 12:19:47 +0100 Subject: Fixes in string scope and string interpretation for Alloy --- .../builder/AlloyModelInterpretation.xtend | 47 ++++++--- .../builder/Logic2AlloyLanguageMapper.xtend | 83 +--------------- .../alloy/reasoner/builder/RunCommandMapper.xtend | 105 +++++++++++++++++++++ 3 files changed, 142 insertions(+), 93 deletions(-) create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend 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 95216835..107aa001 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 @@ -19,6 +19,8 @@ import java.util.LinkedList import java.util.List import java.util.Map import java.util.Set +import java.util.SortedSet +import java.util.TreeSet import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* @@ -34,6 +36,8 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ private var String logicBooleanTrue; private var String logicBooleanFalse; + private SortedSet integerAtoms = new TreeSet + private SortedSet stringAtoms = new TreeSet private val Map alloyAtom2LogicElement = new HashMap private val Map> interpretationOfUndefinedType = new HashMap @@ -42,8 +46,8 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ private val Map> function2Value private val Map> relation2Value - private val int minInt - private val int maxInt + //private val int minInt + //private val int maxInt public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { this.typeInterpretator = typeInterpretator @@ -60,8 +64,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ name2AlloyField.put(field.label,field) } } - - val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution.allAtoms) + val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution) this.typeInterpretator.resolveUnknownAtoms( unknownAtoms, solution, @@ -101,31 +104,46 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ this.relation2Value = Union(hostedRelation2Value,globalRelation2Value) //Int limits - this.minInt = solution.min - this.maxInt = solution.max + //this.minInt = solution.min + //this.maxInt = solution.max //print(trace) } - def List collectUnknownAndResolveKnownAtoms(Iterable allAtoms) { + def List collectUnknownAndResolveKnownAtoms(A4Solution solution) { + val Iterable allAtoms = solution.allAtoms val List unknownAtoms = new LinkedList for(atom: allAtoms) { val typeName = getName(atom.type) val atomName = atom.name - //println(atom.toString + " < - " + typeName) + println(atom.toString + " < - " + typeName) if(typeName == forwardTrace.logicLanguage.name) { this.logicLanguage = atom } else if(typeName == "Int" || typeName == "seq/Int") { - // do nothing, integers will be parsed from the string + val value = Integer.parseInt(atomName.join) + this.integerAtoms.add(value) } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') + } else if(typeName == "String") { + val value = parseString(atomName.join) + this.stringAtoms.add(value) + } else { + unknownAtoms += atom } - else unknownAtoms += atom } - + val integerSignature = solution.allReachableSigs.filter[it.label=="Int"].head + for(i : solution.eval(integerSignature)) { + val value = Integer.parseInt(i.atom(0)) + this.integerAtoms.add(value) + } + val stringSignature = solution.allReachableSigs.filter[it.label=="String"].head + for(i : solution.eval(stringSignature)) { + val value = parseString(i.atom(0)) + this.stringAtoms.add(value) + } return unknownAtoms } @@ -196,17 +214,16 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ } override getAllIntegersInStructure() { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + this.integerAtoms } override getAllRealsInStructure() { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + new TreeSet } override getAllStringsInStructure() { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + this.stringAtoms } - } /** 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 import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion -import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion @@ -48,6 +47,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure @@ -65,14 +66,11 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope import org.eclipse.xtend.lib.annotations.Accessors import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral -import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSStringLiteral class Logic2AlloyLanguageMapper { private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + private val RunCommandMapper runCommandMapper @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this) @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this) @@ -81,6 +79,7 @@ class Logic2AlloyLanguageMapper { public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { this.typeMapper = typeMapper + this.runCommandMapper = new RunCommandMapper(typeMapper) } public def TracedOutput transformProblem(LogicProblem problem, AlloySolverConfiguration config) { @@ -146,7 +145,7 @@ class Logic2AlloyLanguageMapper { } } - transformRunCommand(specification, trace, config) + runCommandMapper.transformRunCommand(this, specification, trace, config) return new TracedOutput(specification,trace) } @@ -303,78 +302,6 @@ class Logic2AlloyLanguageMapper { def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) - } - - ////////////// - // Scopes - ////////////// - - def transformRunCommand(ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) - { - val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size - - // add fact to ensure the existence of all literals in the scope - if(!config.typeScopes.knownStrings.empty) { - specification.factDeclarations += createALSFactDeclaration => [ - it.name = "EnsureAllStrings" - val List equals = config.typeScopes.knownStrings.map[x|createALSEquals => [ - it.leftOperand =createALSStringLiteral => [it.value = x] - it.rightOperand =createALSStringLiteral => [it.value = x] - ]].toList - it.term = support.unfoldAnd(equals) - ] - } - - specification.runCommand = createALSRunCommand => [ - it.typeScopes+= createALSSigScope => [ - it.type= typeMapper.getUndefinedSupertype(trace) - 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!''') - } - } 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 - } - ] - } - if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { - throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') - } else { - if(config.typeScopes.maxNewStrings != 0) { - it.typeScopes += createALSStringScope => [it.number = config.typeScopes.maxNewStrings - knownStringNumber] - } - } - -// for(definedScope : config.typeScopes.allDefinedScope) { -// it.typeScopes += createALSSigScope => [ -// it.type = definedScope.type.lookup(trace.type2ALSType) -// it.number = definedScope.upperLimit -// it.exactly = (definedScope.upperLimit == definedScope.lowerLimit) -// ] -// } - ] } ////////////// 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 new file mode 100644 index 00000000..3e96f7f4 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend @@ -0,0 +1,105 @@ +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.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 { + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; + + public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { + this.typeMapper = typeMapper + } + + def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) + { + //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size + + // add fact to ensure the existence of all literals in the scope + if(!config.typeScopes.knownStrings.empty) { + specification.factDeclarations += createALSFactDeclaration => [ + it.name = "EnsureAllStrings" + val List equals = config.typeScopes.knownStrings.map[x|createALSEquals => [ + it.leftOperand =createALSStringLiteral => [it.value = x] + it.rightOperand =createALSStringLiteral => [it.value = x] + ]].toList + 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 int n = existing.size-amount + typeScopes += createALSSigScope => [ + it.type = typeMapper.transformTypeReference(key,mapper,trace).head + it.number = n + it.exactly =exactly + ] + } + + specification.runCommand = createALSRunCommand => [ + it.typeScopes+= createALSSigScope => [ + it.type= typeMapper.getUndefinedSupertype(trace) + 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!''') + } + } 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 + } + ] + } + if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { + throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') + } else { + if(config.typeScopes.maxNewStrings != 0) { + it.typeScopes += createALSStringScope => [it.number = 0] + } + } + ] + } +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf