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 ++++++++----------- .../alloy/reasoner/builder/AlloyHandler.xtend | 8 ++------ 2 files changed, 10 insertions(+), 17 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src') 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 } 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 b78165dc..51cc8c42 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 @@ -48,7 +48,7 @@ class AlloyHandler { //val fileName = "problem.als" - public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, String alloyCode) { + public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { val writeToFile = ( configuration.documentationLevel===DocumentationLevel::NORMAL || configuration.documentationLevel===DocumentationLevel::FULL) @@ -83,11 +83,7 @@ class AlloyHandler { // Start: Alloy -> Kodkod val kodkodTransformStart = System.currentTimeMillis(); try { - if(writeToFile) { - compModule = CompUtil.parseEverything_fromFile(reporter,null,path) - } else { - compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) - } + compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) if(compModule.allCommands.size != 1) throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') command = compModule.allCommands.head -- cgit v1.2.3-54-g00ecf