From bb1c86e0c99adead52edde0cb60dcb7f7ef6ea2d Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sun, 25 Feb 2018 22:39:10 -0500 Subject: Alloy solver use the als file for logging only And not for parsing --- .../inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend') 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 9c2d7bf1..1658a5b8 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 @@ -43,25 +43,22 @@ class AlloySolver extends LogicReasoner{ val alloyProblem = result.output val forwardTrace = result.trace - var String fileURI = null; - var String alloyCode = null; + //var String fileURI = null; + var String alloyCode = workspace.writeModelToString(alloyProblem,fileName) if(writeToFile) { - fileURI = workspace.writeModel(alloyProblem,fileName).toFileString - } else { - alloyCode = workspace.writeModelToString(alloyProblem,fileName) - } + workspace.writeModel(alloyProblem,fileName) + } val transformationTime = System.currentTimeMillis - transformationStart // Finish: Logic -> Alloy mapping - // Start: Solving Alloy problem - val solverStart = System.currentTimeMillis - val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode) + //val solverStart = System.currentTimeMillis + val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) - val solverFinish = System.currentTimeMillis-solverStart + //val solverFinish = System.currentTimeMillis-solverStart // Finish: Solving Alloy problem - if(writeToFile) workspace.deactivateModel(fileName) + //logicResult.statistics = return logicResult } -- cgit v1.2.3-70-g09d2