diff options
| author |  OszkarSemerath <oszkar.semerath@gmail.com> | 2018-02-25 22:39:10 -0500 |
|---|---|---|
| committer | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-02-25 22:39:10 -0500 |
| commit | bb1c86e0c99adead52edde0cb60dcb7f7ef6ea2d (patch) | |
| tree | 21e19d490b63c40538383584ec931c576ca9e874 /Solvers | |
| parent | Config file: documentation -> log-level (diff) | |
| download | VIATRA-Generator-bb1c86e0c99adead52edde0cb60dcb7f7ef6ea2d.tar.gz VIATRA-Generator-bb1c86e0c99adead52edde0cb60dcb7f7ef6ea2d.tar.zst VIATRA-Generator-bb1c86e0c99adead52edde0cb60dcb7f7ef6ea2d.zip | |
Alloy solver use the als file for logging only
And not for parsing
Diffstat (limited to 'Solvers')
2 files changed, 10 insertions, 17 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 | } |
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 { | |||
| 48 | 48 | ||
| 49 | //val fileName = "problem.als" | 49 | //val fileName = "problem.als" |
| 50 | 50 | ||
| 51 | public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, String alloyCode) { | 51 | public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { |
| 52 | val writeToFile = ( | 52 | val writeToFile = ( |
| 53 | configuration.documentationLevel===DocumentationLevel::NORMAL || | 53 | configuration.documentationLevel===DocumentationLevel::NORMAL || |
| 54 | configuration.documentationLevel===DocumentationLevel::FULL) | 54 | configuration.documentationLevel===DocumentationLevel::FULL) |
| @@ -83,11 +83,7 @@ class AlloyHandler { | |||
| 83 | // Start: Alloy -> Kodkod | 83 | // Start: Alloy -> Kodkod |
| 84 | val kodkodTransformStart = System.currentTimeMillis(); | 84 | val kodkodTransformStart = System.currentTimeMillis(); |
| 85 | try { | 85 | try { |
| 86 | if(writeToFile) { | 86 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) |
| 87 | compModule = CompUtil.parseEverything_fromFile(reporter,null,path) | ||
| 88 | } else { | ||
| 89 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) | ||
| 90 | } | ||
| 91 | if(compModule.allCommands.size != 1) | 87 | if(compModule.allCommands.size != 1) |
| 92 | throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') | 88 | throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') |
| 93 | command = compModule.allCommands.head | 89 | command = compModule.allCommands.head |