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. --- .../inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | 2 +- .../mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | 7 +++---- 2 files changed, 4 insertions(+), 5 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder') 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