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 +++++++++------- .../alloy/reasoner/builder/Alloy2LogicMapper.xtend | 50 +++++++--- .../alloy/reasoner/builder/AlloyHandler.xtend | 111 +++++++++++++++++---- .../builder/Logic2AlloyLanguageMapper.xtend | 2 +- 4 files changed, 178 insertions(+), 70 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy') 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 diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend index 637752b0..7db9e0ea 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend @@ -6,28 +6,30 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory class Alloy2LogicMapper { val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE - public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { - if(solution == null) { + public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { + val models = monitoredAlloySolution.aswers.map[it.key].toList + + if(monitoredAlloySolution.finishedBeforeTimeout) { return createInsuficientResourcesResult => [ it.problem = problem - it.statistics = transformStatistics(solution,transformationTime) + it.representation += models + it.trace = trace + it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) ] } else { - val logicResult = solution.solution - if(logicResult.satisfiable) { + if(models.last.satisfiable || requiredNumberOfSolution == -1) { return createModelResult => [ it.problem = problem - it.representation += solution - it.maxInteger = logicResult.max - it.minInteger = logicResult.min + it.representation += models it.trace = trace - it.statistics = transformStatistics(solution,transformationTime) + it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) ] } else { return createInconsistencyResult => [ it.problem = problem - //trace? - it.statistics = transformStatistics(solution,transformationTime) + it.representation += models + it.trace = trace + it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) ] } } @@ -36,13 +38,29 @@ class Alloy2LogicMapper { def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { createStatistics => [ it.transformationTime = transformationTime as int - if(solution != null) { - it.solverTime = solution.runtimeTime as int - it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [ - it.name = "KoodkodToCNFTransformationTime" - it.value = solution.getKodkodTime as int + for(solutionIndex : 0.. [ + it.name = '''Answer«solutionIndex»Time''' + it.value = solutionTime.intValue ] } + it.entries+= createIntStatisticEntry => [ + it.name = "Alloy2KodKodTransformationTime" + it.value = solution.kodkodTime as int + ] + it.entries+= createIntStatisticEntry => [ + it.name = "Alloy2KodKodTransformationTime" + it.value = solution.kodkodTime as int + ] + it.entries+= createStringStatisticEntry => [ + it.name = "warnings" + it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]''' + ] ] } + + def sum(Iterable ints) { + ints.reduce[p1, p2|p1+p2] + } } \ No newline at end of file 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 6bac4130..17220776 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 @@ -21,6 +21,11 @@ import org.eclipse.emf.common.CommonPlugin import java.util.ArrayList import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import com.google.common.util.concurrent.SimpleTimeLimiter +import java.util.concurrent.Callable +import java.util.concurrent.TimeUnit +import com.google.common.util.concurrent.UncheckedTimeoutException +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration class AlloySolverException extends Exception{ new(String s) { super(s) } @@ -34,9 +39,8 @@ class AlloySolverException extends Exception{ List warnings List debugs long kodkodTime - long runtimeTime - - A4Solution solution + val List> aswers + val boolean finishedBeforeTimeout } class AlloyHandler { @@ -63,6 +67,7 @@ class AlloyHandler { if(configuration.solver.externalSolver) { it.solverDirectory = configuration.solverPath } + //it.inferPartialInstance it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString ] @@ -70,8 +75,8 @@ class AlloyHandler { var Command command = null; var CompModule compModule = null + // Start: Alloy -> Kodkod val kodkodTransformStart = System.currentTimeMillis(); - try { if(configuration.writeToFile) { compModule = CompUtil.parseEverything_fromFile(reporter,null,path) @@ -85,23 +90,26 @@ class AlloyHandler { throw new AlloySolverException(e.message,warnings,e) } val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart + // Finish: Alloy -> Kodkod - //Execute - var A4Solution answer = null; - try { - answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) - }catch(Exception e) { - warnings +=e.message - } - - var long runtimeFromAnswer; - if(runtime.empty) { - runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish) + val limiter = new SimpleTimeLimiter + val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration.solutionScope.numberOfRequiredSolution) + var List> answers + var boolean finished + if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { + answers = callable.call + finished = true } else { - runtimeFromAnswer = runtime.head + try{ + answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) + finished = true + } catch (UncheckedTimeoutException e) { + answers = callable.partialAnswers + finished = false + } } - - return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer) + + new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) } val static Map previousSolverConfigurations = new HashMap @@ -138,6 +146,73 @@ class AlloyHandler { } } +class AlloyCallerWithTimeout implements Callable>>{ + + val List warnings + val List debugs + val A4Reporter reporter + val A4Options options + + val Command command + val CompModule compModule + val int numberOfRequiredSolution + + val List> answers = new LinkedList() + + new(List warnings, + List debugs, + A4Reporter reporter, + A4Options options, + Command command, + CompModule compModule, + int numberOfRequiredSolution) + { + this.warnings = warnings + this.debugs = debugs + this.reporter = reporter + this.options = options + this.command = command + this.compModule = compModule + this.numberOfRequiredSolution = numberOfRequiredSolution + } + + override call() throws Exception { + val startTime = System.currentTimeMillis + + // Start: Execute + var A4Solution lastAnswer = null + try { + do{ + if(lastAnswer == null) { + lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) + } else { + lastAnswer = lastAnswer.next + } + + val runtime = System.currentTimeMillis -startTime + synchronized(this) { + answers += lastAnswer->runtime + } + println( answers.size ) + } while(lastAnswer.satisfiable != false && hasEnoughSolution(answers)) + + }catch(Exception e) { + warnings +=e.message + } + // Finish: execute + return answers + } + + def hasEnoughSolution(List answers) { + if(numberOfRequiredSolution < 0) return false + else return answers.size < numberOfRequiredSolution + } + + public def getPartialAnswers() { + return answers + } +} + @Data class SolverConfiguration { AlloyBackendSolver backedSolver String path diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend index 23b9027f..65fdcfdf 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend @@ -277,7 +277,7 @@ class Logic2AlloyLanguageMapper { it.typeScopes+= createALSSigScope => [ it.type= typeMapper.getUndefinedSupertype(trace) it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) - //it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements) + it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) ] if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( '''An integer scope have to be specified for Alloy!''') -- cgit v1.2.3-54-g00ecf