From c1f185fd8fc2c3dfc123d9271726c588963c7c01 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 8 Apr 2019 00:58:00 +0200 Subject: Objective POC implementation --- .../execution/GenerationTaskExecutor.xtend | 4 +- .../application/execution/ScriptExecutor.xtend | 20 ++- .../application/execution/SolverLoader.xtend | 182 +++++++++++++++------ 3 files changed, 147 insertions(+), 59 deletions(-) (limited to 'Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution') diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend index 35ffaf65..8ea674d3 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend @@ -133,7 +133,9 @@ class GenerationTaskExecutor { // 5. create a solver and a configuration // 5.1 initialize val solver = solverLoader.loadSolver(task.solver,configurationMap) - val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,console) + val objectiveSpecification = scriptExecutor.getObjectiveSpecification(task.objectives) + val objectiveEntries = objectiveSpecification?.entries ?: emptyList + val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,objectiveEntries,console) // 5.2 set values that defined directly diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend index 0512a5ee..25036df6 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend @@ -30,6 +30,8 @@ import org.eclipse.core.runtime.Status import org.eclipse.core.runtime.jobs.Job import org.eclipse.emf.common.util.URI import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveSpecification +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveReference @FinalFieldsConstructor class ScriptExecutor { @@ -40,7 +42,7 @@ class ScriptExecutor { /** * Executes a script */ - public def executeScript(URI uri) { + def executeScript(URI uri) { val job = new Job('''Model Generation: «uri.lastSegment»''') { override protected run(IProgressMonitor monitor) { try{ @@ -57,7 +59,7 @@ class ScriptExecutor { job.schedule(); } - public def executeScript(ConfigurationScript script, IProgressMonitor monitor) { + def executeScript(ConfigurationScript script, IProgressMonitor monitor) { script.activateAllEPackageReferences val tasks = script.commands.filter(Task) @@ -94,12 +96,12 @@ class ScriptExecutor { // } } - def public dispatch execute(GenerationTask task, IProgressMonitor monitor) { + def dispatch void execute(GenerationTask task, IProgressMonitor monitor) { val generationTaskExecutor = new GenerationTaskExecutor generationTaskExecutor.executeGenerationTask(task,this,scriptConsoleFactory,monitor) } - def public dispatch execute(Task task, IProgressMonitor monitor) { + def dispatch void execute(Task task, IProgressMonitor monitor) { throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''') } @@ -174,6 +176,16 @@ class ScriptExecutor { null } + def dispatch getObjectiveSpecification(ObjectiveSpecification config) { + config + } + def dispatch getObjectiveSpecification(ObjectiveReference config) { + config.referred.specification + } + def dispatch getObjectiveSpecification(Void config) { + null + } + def dispatch getConfiguration(ConfigSpecification config) { config } diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend index 9eceef5f..f769d46f 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend @@ -1,44 +1,47 @@ package hu.bme.mit.inf.dslreasoner.application.execution -import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CostObjectiveFunction +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveEntry +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.OptimizationEntry import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ThresholdEntry import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold +import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser +import java.util.List import java.util.Map import java.util.Optional +import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel +import org.eclipse.xtext.EcoreUtil2 import org.eclipse.xtext.xbase.lib.Functions.Function1 -import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor class SolverLoader { def loadSolver(Solver solver, Map config) { - switch(solver) { + switch (solver) { case ALLOY_SOLVER: return new AlloySolver case SMT_SOLVER: return new SMTSolver case VIATRA_SOLVER: return new ViatraReasoner } } - - - - private def Optional getAsType( - Map config, - String key, - ScriptConsole console, - Function1 parser, - Class requestedType) - { - if(config.containsKey(key)) { + + private def Optional getAsType(Map config, String key, ScriptConsole console, + Function1 parser, Class requestedType) { + if (config.containsKey(key)) { val stringValue = config.get(key) - try{ + try { val parsedValue = parser.apply(stringValue) return Optional.of(parsedValue) - } catch(Exception e) { + } catch (Exception e) { console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''') return Optional::empty } @@ -46,60 +49,131 @@ class SolverLoader { return Optional::empty } } + private def getAsInteger(Map config, String key, ScriptConsole console) { - return getAsType(config,key,console,[x|Integer.parseInt(x)],Integer) + return getAsType(config, key, console, [x|Integer.parseInt(x)], Integer) } + private def getAsBoolean(Map config, String key, ScriptConsole console) { - return getAsType(config,key,console,[x|Boolean.parseBoolean(x)],Boolean) + return getAsType(config, key, console, [x|Boolean.parseBoolean(x)], Boolean) } + private def getAsDouble(Map config, String key, ScriptConsole console) { - return getAsType(config,key,console,[x|Double.parseDouble(x)],Double) + return getAsType(config, key, console, [x|Double.parseDouble(x)], Double) } - - def loadSolverConfig( - Solver solver, - Map config, - ScriptConsole console) - { - if(solver === Solver::ALLOY_SOLVER) { - return new AlloySolverConfiguration => [c| - config.getAsInteger("symmetry",console) - .ifPresent[c.symmetry = it] - config.getAsType("solver",console,[x|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver) - .ifPresent[c.solver = it] - ] - } else if(solver === Solver::SMT_SOLVER) { - return new SmtSolverConfiguration => [c| - config.getAsBoolean("fixRandomSeed",console).ifPresent[c.fixRandomSeed = it] - config.getAsType("path",console,[it],String).ifPresent[c.solverPath = it] - ] - } else if(solver === Solver::VIATRA_SOLVER) { - return new ViatraReasonerConfiguration => [c| + + def loadSolverConfig(Solver solver, Map config, List objectiveEntries, + ScriptConsole console) { + switch (solver) { + case ALLOY_SOLVER: { + if (!objectiveEntries.empty) { + throw new IllegalArgumentException("Objectives are not supported by Alloy.") + } + val c = new SmtSolverConfiguration + config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] + config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] + c + } + case SMT_SOLVER: { + if (!objectiveEntries.empty) { + throw new IllegalArgumentException("Objectives are not supported by Z3.") + } + val c = new SmtSolverConfiguration + config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] + config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] + c + } + case VIATRA_SOLVER: { + val c = new ViatraReasonerConfiguration c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser - if(config.containsKey("diversity-range")) { + if (config.containsKey("diversity-range")) { val stringValue = config.get("diversity-range") - try{ + try { val range = Integer.parseInt(stringValue) c.diversityRequirement = new DiversityDescriptor => [ it.ensureDiversity = true it.range = range ] - } catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')} + } catch (NumberFormatException e) { + console.writeError('''Malformed number format: «e.message»''') + } } - ] - } else { - throw new UnsupportedOperationException('''Unknown solver: «solver»''') + for (objectiveEntry : objectiveEntries) { + val costObjectiveConfig = new CostObjectiveConfiguration + switch (objectiveEntry) { + OptimizationEntry: { + costObjectiveConfig.findExtremum = true + costObjectiveConfig.kind = switch (direction : objectiveEntry.direction) { + case MAXIMIZE: + ObjectiveKind.HIGHER_IS_BETTER + case MINIMIZE: + ObjectiveKind.LOWER_IS_BETTER + default: + throw new IllegalArgumentException("Unknown direction: " + direction) + } + costObjectiveConfig.threshold = ObjectiveThreshold.NO_THRESHOLD + } + ThresholdEntry: { + costObjectiveConfig.findExtremum = false + val threshold = objectiveEntry.threshold.doubleValue + switch (operator : objectiveEntry.operator) { + case LESS: { + costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER + costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) + } + case GREATER: { + costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER + costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) + } + case LESS_EQUALS: { + costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER + costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) + } + case GREATER_EQUALS: { + costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER + costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) + } + default: + throw new IllegalArgumentException("Unknown operator: " + operator) + } + } + } + val function = objectiveEntry.function + if (function instanceof CostObjectiveFunction) { + for (costEntry : function.entries) { + val element = new CostObjectiveElementConfiguration + val pattern = costEntry.patternElement.pattern + val packageName = costEntry.patternElement.package?.packageName ?: + EcoreUtil2.getContainerOfType(pattern, PatternModel)?.packageName + element.patternQualifiedName = if (packageName.nullOrEmpty) { + pattern.name + } else { + packageName + "." + pattern.name + } + costObjectiveConfig.elements += element + } + } else { + throw new IllegalArgumentException("Only cost objectives are supported by VIATRA.") + } + c.costObjectives += costObjectiveConfig + } + c + } + default: + throw new UnsupportedOperationException('''Unknown solver: «solver»''') } } - - def dispatch void setRunIndex(AlloySolverConfiguration config, Map parameters, int runIndex, ScriptConsole console) { - parameters.getAsBoolean("randomize",console).ifPresent[ - if(it) { - config.randomise = runIndex-1 + + def dispatch void setRunIndex(AlloySolverConfiguration config, Map parameters, int runIndex, + ScriptConsole console) { + parameters.getAsBoolean("randomize", console).ifPresent [ + if (it) { + config.randomise = runIndex - 1 } ] } - def dispatch void setRunIndex(LogicSolverConfiguration config, Map parameters, int runIndex, ScriptConsole console) { - + + def dispatch void setRunIndex(LogicSolverConfiguration config, Map parameters, int runIndex, + ScriptConsole console) { } -} \ No newline at end of file +} -- cgit v1.2.3-70-g09d2