diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | 19 |
1 files changed, 8 insertions, 11 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 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{ | |||
43 | val alloyProblem = result.output | 43 | val alloyProblem = result.output |
44 | val forwardTrace = result.trace | 44 | val forwardTrace = result.trace |
45 | 45 | ||
46 | var String fileURI = null; | 46 | //var String fileURI = null; |
47 | var String alloyCode = null; | 47 | var String alloyCode = workspace.writeModelToString(alloyProblem,fileName) |
48 | if(writeToFile) { | 48 | if(writeToFile) { |
49 | fileURI = workspace.writeModel(alloyProblem,fileName).toFileString | 49 | workspace.writeModel(alloyProblem,fileName) |
50 | } else { | 50 | } |
51 | alloyCode = workspace.writeModelToString(alloyProblem,fileName) | ||
52 | } | ||
53 | val transformationTime = System.currentTimeMillis - transformationStart | 51 | val transformationTime = System.currentTimeMillis - transformationStart |
54 | // Finish: Logic -> Alloy mapping | 52 | // Finish: Logic -> Alloy mapping |
55 | 53 | ||
56 | |||
57 | // Start: Solving Alloy problem | 54 | // Start: Solving Alloy problem |
58 | val solverStart = System.currentTimeMillis | 55 | //val solverStart = System.currentTimeMillis |
59 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode) | 56 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) |
60 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | 57 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) |
61 | val solverFinish = System.currentTimeMillis-solverStart | 58 | //val solverFinish = System.currentTimeMillis-solverStart |
62 | // Finish: Solving Alloy problem | 59 | // Finish: Solving Alloy problem |
63 | 60 | ||
64 | if(writeToFile) workspace.deactivateModel(fileName) | 61 | //logicResult.statistics = |
65 | 62 | ||
66 | return logicResult | 63 | return logicResult |
67 | } | 64 | } |