From 3f9b1c92cc35fa4ed9672a2b8601f4c22af24921 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sun, 7 Apr 2019 13:46:36 +0200 Subject: Infrastructure for objective functions --- .../src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | 2 +- .../mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) (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/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend index 432651af..ceb78e99 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend @@ -57,7 +57,7 @@ class AlloySolver extends LogicReasoner{ val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) alloyConfig.progressMonitor.workedSearchFinished - val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) + val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolutions,result2,forwardTrace,transformationTime) alloyConfig.progressMonitor.workedBackwardTransformationFinished //val solverFinish = System.currentTimeMillis-solverStart // Finish: Solving Alloy problem 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..033ced04 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 @@ -184,7 +184,7 @@ class AlloyCallerWithTimeout implements Callable>>{ } else { lastAnswer = lastAnswer.next } - configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) + configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolutions) val runtime = System.currentTimeMillis -startTime synchronized(this) { @@ -201,8 +201,8 @@ class AlloyCallerWithTimeout implements Callable>>{ } def hasEnoughSolution(List answers) { - if(configuration.solutionScope.numberOfRequiredSolution < 0) return false - else return answers.size() == configuration.solutionScope.numberOfRequiredSolution + if(configuration.solutionScope.numberOfRequiredSolutions < 0) return false + else return answers.size() == configuration.solutionScope.numberOfRequiredSolutions } public def getPartialAnswers() { -- cgit v1.2.3-70-g09d2 From b15b3d49ead78c9124a98ab982a4488e4d7bc3d4 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 29 Oct 2019 17:32:38 +0100 Subject: Alloy cardinality fixes --- .../alloy/reasoner/queries/typeQueries.vql | 2 +- .../alloy/reasoner/builder/Alloy2LogicMapper.xtend | 2 +- .../reasoner/builder/AlloyModelInterpretation.xtend | 2 +- ...AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | 2 +- .../alloy/reasoner/builder/RunCommandMapper.xtend | 19 +++++++++++++++---- 5 files changed, 19 insertions(+), 8 deletions(-) (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/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql index 8d93cafb..14cf3594 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql @@ -81,5 +81,5 @@ private pattern typeDoesNotCoverElementOccurance(element: DefinedElement, type: find supertype(containerType,type); TypeDefinition.elements(containerType,element); TypeDefinition.elements(uncoveredOccurance,element); - neg find supertype(uncoveredOccurance,type); + neg find supertype(type,uncoveredOccurance); } \ 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/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..328ca176 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,7 +9,7 @@ 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) { + if(models.empty || !monitoredAlloySolution.finishedBeforeTimeout) { return createInsuficientResourcesResult => [ it.problem = problem it.representation += models 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 107aa001..29eabe2c 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 @@ -117,7 +117,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ 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") { 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..ae7a1e6b 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 @@ -124,7 +124,7 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL for(type : types.filter[it.supertypes.size>=2]) { trace.specification.factDeclarations += createALSFactDeclaration => [ it.name = support.toIDMultiple("abstract",type.name) - it.term = createALSEquals => [ + it.term = createALSSubset => [ it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] it.rightOperand = support.unfoldIntersection(type.supertypes.map[e| createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) 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 494197bc..b74017d8 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 @@ -9,8 +9,12 @@ 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.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition 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; @@ -89,16 +93,18 @@ class RunCommandMapper { ] for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) { - val limit = upperLimit.value + val type = upperLimit.key + val limit = upperLimit.value + getExistingCount(type) if(limit != LogicSolverConfiguration::Unlimited) { - this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace) + this.typeScopeMapping.addUpperMultiplicity(specification,type,limit,mapper,trace) } } for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) { - val limit = lowerLimit.value + val type = lowerLimit.key + val limit = lowerLimit.value + getExistingCount(type) if(limit != 0) { - this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace) + this.typeScopeMapping.addLowerMultiplicity(specification,type,limit,mapper,trace) } } @@ -106,6 +112,11 @@ class RunCommandMapper { setStringScope(specification,config,specification.runCommand) } + private def getExistingCount(Type type) { + val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet + existing.size + } + 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!''') -- cgit v1.2.3-70-g09d2 From b84e5c63aaded9d15d38b43ea9fbfb09a976e12a Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 12 Feb 2020 20:40:38 +0100 Subject: Fix concurrency bug in AlloyHandler --- .../inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (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/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 ed2ef6b7..451aad6e 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 @@ -101,15 +101,8 @@ class AlloyHandler { try{ answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS) finished = true - } catch (TimeoutException ex) { - // handle the timeout - } catch (InterruptedException e) { - // handle the interrupts - } catch (ExecutionException e) { - // handle other exceptions - } finally { - future.cancel(true); - + } catch (TimeoutException | InterruptedException | ExecutionException e) { + future.cancel(true) answers = callable.partialAnswers finished = false } -- cgit v1.2.3-70-g09d2