From d2478be3f7ad7ebfe60125aa555388fe79003fe2 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 3 Mar 2018 02:03:09 -0500 Subject: Alloy solver report progress and does not call solver if cancelled --- .../dlsreasoner/alloy/reasoner/AlloySolver.xtend | 4 ++ .../alloy/reasoner/builder/AlloyHandler.xtend | 47 ++++++++++------------ 2 files changed, 26 insertions(+), 25 deletions(-) (limited to 'Solvers/Alloy-Solver') 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 1658a5b8..e664b3b5 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 @@ -49,12 +49,16 @@ class AlloySolver extends LogicReasoner{ workspace.writeModel(alloyProblem,fileName) } val transformationTime = System.currentTimeMillis - transformationStart + alloyConfig.progressMonitor.workedForwardTransformation // Finish: Logic -> Alloy mapping // Start: Solving Alloy problem //val solverStart = System.currentTimeMillis val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) + alloyConfig.progressMonitor.workedSearchFinished + val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,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 51cc8c42..ebbca624 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 @@ -24,9 +24,7 @@ import java.util.List import java.util.Map import java.util.concurrent.Callable import java.util.concurrent.TimeUnit -import org.eclipse.emf.common.CommonPlugin import org.eclipse.xtend.lib.annotations.Data -import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel class AlloySolverException extends Exception{ new(String s) { super(s) } @@ -49,12 +47,8 @@ class AlloyHandler { //val fileName = "problem.als" public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { - val writeToFile = ( - configuration.documentationLevel===DocumentationLevel::NORMAL || - configuration.documentationLevel===DocumentationLevel::FULL) //Prepare - val warnings = new LinkedList val debugs = new LinkedList val runtime = new ArrayList @@ -73,7 +67,7 @@ class AlloyHandler { it.solverDirectory = configuration.solverPath } //it.inferPartialInstance - it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString + //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString ] // Transform @@ -94,7 +88,7 @@ class AlloyHandler { // Finish: Alloy -> Kodkod val limiter = new SimpleTimeLimiter - val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration.solutionScope.numberOfRequiredSolution) + val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) var List> answers var boolean finished if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { @@ -156,7 +150,7 @@ class AlloyCallerWithTimeout implements Callable>>{ val Command command val CompModule compModule - val int numberOfRequiredSolution + val AlloySolverConfiguration configuration val List> answers = new LinkedList() @@ -166,7 +160,7 @@ class AlloyCallerWithTimeout implements Callable>>{ A4Options options, Command command, CompModule compModule, - int numberOfRequiredSolution) + AlloySolverConfiguration configuration) { this.warnings = warnings this.debugs = debugs @@ -174,7 +168,7 @@ class AlloyCallerWithTimeout implements Callable>>{ this.options = options this.command = command this.compModule = compModule - this.numberOfRequiredSolution = numberOfRequiredSolution + this.configuration = configuration } override call() throws Exception { @@ -183,19 +177,22 @@ class AlloyCallerWithTimeout implements Callable>>{ // Start: Execute var A4Solution lastAnswer = null try { - do{ - if(lastAnswer == null) { - lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) - } else { - lastAnswer = lastAnswer.next - } + if(!configuration.progressMonitor.isCancelled) { + do{ + if(lastAnswer == null) { + lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) + } else { + lastAnswer = lastAnswer.next + } + configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) + + val runtime = System.currentTimeMillis -startTime + synchronized(this) { + answers += (lastAnswer->runtime) + } + } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) - val runtime = System.currentTimeMillis -startTime - synchronized(this) { - answers += (lastAnswer->runtime) - } - } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers)) - + } }catch(Exception e) { warnings +=e.message } @@ -204,8 +201,8 @@ class AlloyCallerWithTimeout implements Callable>>{ } def hasEnoughSolution(List answers) { - if(numberOfRequiredSolution < 0) return false - else return answers.size() == numberOfRequiredSolution + if(configuration.solutionScope.numberOfRequiredSolution < 0) return false + else return answers.size() == configuration.solutionScope.numberOfRequiredSolution } public def getPartialAnswers() { -- cgit v1.2.3-54-g00ecf