Alloy solver report progress and does not call solver if cancelled

1 files changed, 4 insertions, 0 deletions

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