From 53cf6e18913a9f0c7717ff84eedd56941944367a Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 5 Jul 2017 15:00:37 +0200 Subject: Adding multiple model generation support for the alloy solver. --- .../bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | 12 +++++++----- .../alloy/reasoner/builder/Alloy2LogicMapper.xtend | 2 +- .../dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | 7 +++---- 3 files changed, 11 insertions(+), 10 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner') 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 d0c7d320..65539155 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 @@ -16,6 +16,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution +import java.util.List class AlloySolver extends LogicReasoner{ @@ -72,16 +74,16 @@ class AlloySolver extends LogicReasoner{ } override getInterpretations(ModelResult modelResult) { - val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] - val res = answers.map [ + //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] + val sols = modelResult.representation// as List + //val res = answers.map + sols.map[ new AlloyModelInterpretation( new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, - it, + it as A4Solution, forwardMapper, modelResult.trace as Logic2AlloyLanguageMapperTrace ) ] - - return res } } \ 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 7db9e0ea..2efd6b29 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(!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/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 17220776..c1f2ec4c 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 @@ -191,10 +191,9 @@ class AlloyCallerWithTimeout implements Callable>>{ val runtime = System.currentTimeMillis -startTime synchronized(this) { - answers += lastAnswer->runtime + answers += (lastAnswer->runtime) } - println( answers.size ) - } while(lastAnswer.satisfiable != false && hasEnoughSolution(answers)) + } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers)) }catch(Exception e) { warnings +=e.message @@ -205,7 +204,7 @@ class AlloyCallerWithTimeout implements Callable>>{ def hasEnoughSolution(List answers) { if(numberOfRequiredSolution < 0) return false - else return answers.size < numberOfRequiredSolution + else return answers.size() == numberOfRequiredSolution } public def getPartialAnswers() { -- cgit v1.2.3-54-g00ecf