From 25a4b1b53add70e268c3083682f8a3508c618ec2 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 25 Oct 2019 04:15:39 -0400 Subject: VAMPIRE: post-submission push --- .../alloy/reasoner/builder/Alloy2LogicMapper.xtend | 20 +- .../alloy/reasoner/builder/AlloyHandler.xtend | 23 ++- ...peInterpretation_InheritanceAndHorizontal.xtend | 63 ++++++- .../builder/Logic2AlloyLanguageMapper.xtend | 11 +- .../Logic2AlloyLanguageMapper_RelationMapper.xtend | 13 +- ...oyLanguageMapper_TypeMapper_FilteredTypes.xtend | 2 +- ...ogic2AlloyLanguageMapper_TypeScopeMapping.xtend | 44 +++++ .../alloy/reasoner/builder/RunCommandMapper.xtend | 207 +++++++++++++++------ 8 files changed, 292 insertions(+), 91 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/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy') diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend index 2efd6b29..59ec2ae4 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend @@ -9,15 +9,15 @@ class Alloy2LogicMapper { public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { val models = monitoredAlloySolution.aswers.map[it.key].toList - if(!monitoredAlloySolution.finishedBeforeTimeout) { - return createInsuficientResourcesResult => [ - it.problem = problem - it.representation += models - it.trace = trace - it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) - ] - } else { - if(models.last.satisfiable || requiredNumberOfSolution == -1) { +// if(!monitoredAlloySolution.finishedBeforeTimeout) { +// return createInsuficientResourcesResult => [ +// it.problem = problem +// it.representation += models +// it.trace = trace +// it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) +// ] +// } else { + if((!models.isEmpty && models.last.satisfiable) || requiredNumberOfSolution == -1) { return createModelResult => [ it.problem = problem it.representation += models @@ -32,7 +32,7 @@ class Alloy2LogicMapper { it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) ] } - } +// } } def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend index ebbca624..9b4265b9 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend @@ -1,7 +1,5 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder -import com.google.common.util.concurrent.SimpleTimeLimiter -import com.google.common.util.concurrent.UncheckedTimeoutException import edu.mit.csail.sdg.alloy4.A4Reporter import edu.mit.csail.sdg.alloy4.Err import edu.mit.csail.sdg.alloy4.ErrorWarning @@ -23,7 +21,11 @@ import java.util.LinkedList import java.util.List import java.util.Map import java.util.concurrent.Callable +import java.util.concurrent.ExecutionException +import java.util.concurrent.ExecutorService +import java.util.concurrent.Executors import java.util.concurrent.TimeUnit +import java.util.concurrent.TimeoutException import org.eclipse.xtend.lib.annotations.Data class AlloySolverException extends Exception{ @@ -46,7 +48,7 @@ class AlloyHandler { //val fileName = "problem.als" - public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { + def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { //Prepare val warnings = new LinkedList @@ -87,7 +89,6 @@ class AlloyHandler { val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart // Finish: Alloy -> Kodkod - val limiter = new SimpleTimeLimiter val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) var List> answers var boolean finished @@ -95,10 +96,20 @@ class AlloyHandler { answers = callable.call finished = true } else { + val ExecutorService executor = Executors.newCachedThreadPool(); + val future = executor.submit(callable) try{ - answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) + answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS) finished = true - } catch (UncheckedTimeoutException e) { + } catch (TimeoutException ex) { + // handle the timeout + } catch (InterruptedException e) { + // handle the interrupts + } catch (ExecutionException e) { + // handle other exceptions + } finally { + future.cancel(true); + answers = callable.partialAnswers finished = false } diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend index 8019c6b5..ac75b2a1 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend @@ -1,20 +1,73 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar -import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution -import java.util.Map import edu.mit.csail.sdg.alloy4compiler.ast.Sig import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import java.util.ArrayList import java.util.List -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import java.util.Map + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{ protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE - override resolveUnknownAtoms(Iterable objectAtoms, A4Solution solution, Logic2AlloyLanguageMapperTrace forwardTrace, Map name2AlloySig, Map name2AlloyField, Map expression2DefinedElement, Map> interpretationOfUndefinedType) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + override resolveUnknownAtoms( + Iterable objectAtoms, + A4Solution solution, + Logic2AlloyLanguageMapperTrace forwardTrace, + Map name2AlloySig, + Map name2AlloyField, + Map expression2DefinedElement, + Map> interpretationOfUndefinedType) + { + /*val Map expression2DefinedElement = new HashMap() + val Map> interpretationOfUndefinedType = new HashMap;*/ + + val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal + + // 1. Evaluate the defined elements + for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) { + val name = definedElementMappingEntry.value.name + val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) + val elementsOfSingletonSignature = solution.eval(matchingSig) + if(elementsOfSingletonSignature.size != 1) { + throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''') + } else { + val expressionOfDefinedElement = elementsOfSingletonSignature.head.atom(0)// as ExprVar + expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key) + } + } + + // 2. evaluate the signatures and create new elements if necessary + for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) { + val type = type2SingatureEntry.key + if(type instanceof TypeDeclaration) { + val name = type2SingatureEntry.value.name + val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) + val elementsOfSignature = solution.eval(matchingSig) + val elementList = new ArrayList(elementsOfSignature.size) + var newVariableIndex = 1; + for(elementOfSignature : elementsOfSignature) { + val expressionOfDefinedElement = elementOfSignature.atom(0) + if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) { + elementList += expressionOfDefinedElement.lookup(expression2DefinedElement) + } else { + val newElementName = '''newObject «newVariableIndex.toString»''' + val newRepresentation = createDefinedElement => [ + it.name = newElementName + ] + elementList += newRepresentation + expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation) + } + } + interpretationOfUndefinedType.put(type,elementList) + } + } } } \ 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/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 3fc3971d..e1ffe531 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 @@ -194,13 +194,12 @@ class Logic2AlloyLanguageMapper { val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) val type = relation.type - if(type instanceof ALSDirectProduct) { - type.rightMultiplicit = type.rightMultiplicit.addUpper - } else { - relation.multiplicity = relation.multiplicity.addUpper - } - if(assertion.upper === 1) { + if(type instanceof ALSDirectProduct) { + type.rightMultiplicit = type.rightMultiplicit.addUpper + } else { + relation.multiplicity = relation.multiplicity.addUpper + } return true } else { return transformAssertion(assertion.target,trace) 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_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend index 397fb84b..2d79e364 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend @@ -254,7 +254,7 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL } override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { - return undefinedScope + trace.typeTrace.definedElement2Declaration.size + if(undefinedScope == Integer.MAX_VALUE) return undefinedScope else return undefinedScope + trace.typeTrace.definedElement2Declaration.size } override getTypeInterpreter() { 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..98d769bf --- /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 3e96f7f4..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 @@ -3,25 +3,26 @@ 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.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 { - 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; + val Logic2AlloyLanguageMapper_TypeScopeMapping typeScopeMapping; - public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { + new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { this.typeMapper = typeMapper + this.typeScopeMapping = new Logic2AlloyLanguageMapper_AsConstraint(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 @@ -36,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 => [ @@ -65,41 +85,112 @@ 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!''') - } - } 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 - } - ] + + ] + + for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) { + val limit = upperLimit.value + if(limit != LogicSolverConfiguration::Unlimited) { + this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace) } - if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { - throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') + } + + 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) { + 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 { - if(config.typeScopes.maxNewStrings != 0) { + 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!''') } } - ] + } + } + + 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 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 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 = #[minKnownInteger,minIntegerInProblem].min + val max = #[maxKnownInteger,maxIntegerInProblem].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