From f00ce77fdc3a1417ddfd833f122b64ecef80d7d6 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sun, 2 Jul 2017 23:34:27 +0200 Subject: Alloy implementation of multiple model generation --- .../dlsreasoner/alloy/reasoner/AlloySolver.xtend | 85 +++++++++++++--------- 1 file changed, 50 insertions(+), 35 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 7dfc3161..d0c7d320 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 @@ -3,8 +3,10 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage @@ -14,9 +16,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace -import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes -import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes -import org.eclipse.emf.common.util.URI class AlloySolver extends LogicReasoner{ @@ -33,40 +32,56 @@ class AlloySolver extends LogicReasoner{ val fileName = "problem.als" override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { + val alloyConfig = configuration.asConfig + + // Start: Logic -> Alloy mapping + val transformationStart = System.currentTimeMillis + val result = forwardMapper.transformProblem(problem,alloyConfig) + val alloyProblem = result.output + val forwardTrace = result.trace + + var String fileURI = null; + var String alloyCode = null; + if(alloyConfig.writeToFile) { + fileURI = workspace.writeModel(alloyProblem,fileName).toFileString + } else { + alloyCode = workspace.writeModelToString(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 logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) + val solverFinish = System.currentTimeMillis-solverStart + // Finish: Solving Alloy problem + + if(alloyConfig.writeToFile) workspace.deactivateModel(fileName) + + return logicResult + } + + def asConfig(LogicSolverConfiguration configuration) { if(configuration instanceof AlloySolverConfiguration) { - val transformationStart = System.currentTimeMillis - val result = forwardMapper.transformProblem(problem,configuration) - val alloyProblem = result.output - - /*val x = alloyProblem.eAllContents.filter(ALSFunctionCall).filter[it.referredDefinition == null].toList - println(x)*/ - val forwardTrace = result.trace - - var String fileURI = null; - var String alloyCode = null; - if(configuration.writeToFile) { - fileURI = workspace.writeModel(alloyProblem,fileName).toFileString - } else { - alloyCode = workspace.writeModelToString(alloyProblem,fileName) - } - - //val alloyCode = workspace.readText(fileName) - //val FunctionWithTimeout call = new FunctionWithTimeout[] - - val transformationTime = System.currentTimeMillis - transformationStart - val result2 = handler.callSolver(alloyProblem,workspace,configuration,fileURI,alloyCode) - workspace.deactivateModel(fileName) - val logicResult = backwardMapper.transformOutput(problem,result2,forwardTrace,transformationTime) - return logicResult - } else throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''') + return configuration + } else { + throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''') + } } - override getInterpretation(ModelResult modelResult) { - return new AlloyModelInterpretation( - new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, - (modelResult.representation as MonitoredAlloySolution).solution, - forwardMapper, - modelResult.trace as Logic2AlloyLanguageMapperTrace - ); + override getInterpretations(ModelResult modelResult) { + val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] + val res = answers.map [ + new AlloyModelInterpretation( + new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, + it, + forwardMapper, + modelResult.trace as Logic2AlloyLanguageMapperTrace + ) + ] + + return res } } \ No newline at end of file -- cgit v1.2.3-70-g09d2