From 5f1117a84bc3c24ec71d6bcb9d3f2badffca28c2 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 24 Feb 2018 20:56:42 -0500 Subject: Execution update --- .../execution/GenerationTaskExecutor.xtend | 70 +++++++++++++++----- .../application/execution/NullWorkspace.xtend | 4 +- .../application/execution/ScriptConsole.xtend | 21 ++++-- .../application/execution/ScriptExecutor.xtend | 55 +++++++++++++++- .../application/execution/SolverLoader.xtend | 77 +++++++++++++++++++--- .../util/ApplicationConfigurationParser.xtend | 18 +++++ .../application/execution/util/VQLParser.xtend | 7 +- .../ApplicationConfigurationLinkingService.xtend | 4 +- 8 files changed, 218 insertions(+), 38 deletions(-) create mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/ApplicationConfigurationParser.xtend (limited to 'Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner') 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 635d9dcc..44d9fab0 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 @@ -5,6 +5,7 @@ import hu.bme.mit.inf.dslreasoner.application.validation.MetamodelValidator import hu.bme.mit.inf.dslreasoner.application.validation.QueryAndMetamodelValidator import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolutionScope import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult @@ -14,6 +15,7 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic import hu.bme.mit.inf.dslreasoner.workspace.ProjectWorkspace +import java.util.Optional import org.eclipse.emf.common.util.URI class GenerationTaskExecutor { @@ -36,13 +38,17 @@ class GenerationTaskExecutor { val patternSpecification = scriptExecutor.getPatternSpecification(task.patterns) val partialmodelSpecification = scriptExecutor.getPartialModelSpecification(task.partialModel) val scopeSpecification = scriptExecutor.getScopeSpecification(task.scope) - val configurationMap = scriptExecutor.transformToMap( - scriptExecutor.getConfiguration(task.config)) + val messageFile = scriptExecutor.getFileSpecification(task.targetLogFile) val debugFolder = scriptExecutor.getFileSpecification(task.debugFolder) val outputFolder = scriptExecutor.getFileSpecification(task.getTagetFolder) val statisticsFile = scriptExecutor.getFileSpecification(task.targetStatisticsFile) + val configSpecification = scriptExecutor.getConfiguration(task.config) + val configurationMap = scriptExecutor.transformToMap(configSpecification) + val documentationLevel = scriptExecutor.getDocumentation(configSpecification) + val runtieLimit = scriptExecutor.getRuntimeLimit(configSpecification) + val memoryLimit = scriptExecutor.getMemoryLimit(configSpecification) // 2. create console val console = new ScriptConsole(true,true, @@ -94,12 +100,16 @@ 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) + val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,console) val reasonerWorkspace = if(debugFolder!== null) { new ProjectWorkspace(debugFolder.path,"") } else { new NullWorkspace } + reasonerWorkspace.initAndClear + if(documentationLevel.atLeastNormal) { + reasonerWorkspace.writeModel(problem,"generation.logicproblem") + } // 5.2 set values that defined directly solverConfig.solutionScope = new SolutionScope => [ @@ -116,33 +126,55 @@ class GenerationTaskExecutor { modelGeneration.trace ) + // 5.3 set resource limits + documentationLevel.ifPresent[solverConfig.documentationLevel = it] + runtieLimit.ifPresent[solverConfig.runtimeLimit = it] + memoryLimit.ifPresent[solverConfig.memoryLimit = it] + // 6. execute the solver on the problem with the configuration - val runs = if(task.runSpecified) { - task.runs - } else { - 1 - } - console.writeMessage("Start model generation") + // 6.1 calculating the runs + val runs = if(task.runSpecified) { task.runs } else { 1 } + console.writeMessage("Model generation started") for(run : 1..runs) { - val solution = solver.solve(problem,solverConfig,reasonerWorkspace) + + // 6.2 For each run, the configuration and the workspace is adjusted + solverLoader.setRunIndex(solverConfig,configurationMap,run,console) + val reasonerWorkspaceForRun = if(runs > 1) { + reasonerWorkspace.subWorkspace('''run«run»''',"") => [initAndClear] + } else { + reasonerWorkspace + } + + // 7. Solver call + + val solution = solver.solve(problem,solverConfig,reasonerWorkspaceForRun) + console.writeMessage(solution.soutionDescription.toString) + + // 8. Solution processing + if(solution instanceof ModelResult) { + // + val interpretations = solver.getInterpretations(solution) + } + } + console.writeMessage("Model generation finished") } private def dispatch soutionDescription(InconsistencyResult s) { - if(s.representation.size == 1) { - '''Problem is inconsistent!''' + if(s.representation.size == 0) { + '''Problem is inconsistent, no model is created!''' } else { - '''Problem is inconsistent, only «s.representation.size» model can be created!''' + '''Problem is inconsistent, only «s.representation.size» model«IF s.representation.size>1»s«ENDIF» can be created!''' } } private def dispatch soutionDescription(ModelResult s) { if(s.representation.size == 1) { - '''Problem is consistent!''' + '''Problem is consistent, a model is generated''' } else { - '''Problem is consistent, «s.representation.size» model generated!''' + '''Problem is consistent, «s.representation.size» models are generated!''' } } @@ -153,4 +185,12 @@ class GenerationTaskExecutor { '''Unable to solve problem, but «s.representation.size» model generated!''' } } + + private def atLeastNormal(Optional level) { + if(level.isPresent) { + return (level.get !== DocumentationLevel.NONE) + } else { + return false + } + } } \ No newline at end of file diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/NullWorkspace.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/NullWorkspace.xtend index 4cc44df3..fd3e7348 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/NullWorkspace.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/NullWorkspace.xtend @@ -31,7 +31,9 @@ class NullWorkspace extends ReasonerWorkspace{ protected override Resource getResource(String name) { throw new UnsupportedOperationException(message) } - override public URI writeModel(EObject modelRoot, String name) { } + override public URI writeModel(EObject modelRoot, String name) { } + override writeModelToString(EObject modelRoot, String name) { } + override public RootType reloadModel(Class type, String name) { throw new UnsupportedOperationException(message) } diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptConsole.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptConsole.xtend index 24f77754..2dc329a0 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptConsole.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptConsole.xtend @@ -93,12 +93,23 @@ class ScriptConsole implements Closeable { if (uri === null) { return null } else { - val fileString = uri.toFileString - val file = new File(fileString) - if (this.cleanFiles && file.exists) { - file.delete + if(uri.isFile) { + val fileString = uri.toFileString + val file = new File(fileString) + if (this.cleanFiles && file.exists) { + file.delete + } + return file + } else if(uri.isPlatformResource) { + val platformString = uri.toPlatformString(true) + val file = new File(platformString) + if (this.cleanFiles && file.exists) { + file.delete + } + return file + } else { + throw new UnsupportedOperationException('''Unksupported file usi: "«uri»"!''') } - return file } } 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 c783c9b9..7bd73792 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 @@ -3,22 +3,29 @@ package hu.bme.mit.inf.dslreasoner.application.execution import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ConfigReference import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ConfigSpecification import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ConfigurationScript +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CustomEntry +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.DocumentationEntry +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.EPackageImport import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.FileReference import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.FileSpecification import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.GenerationTask import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.GraphPatternReference +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.MemoryEntry import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.MetamodelReference import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.MetamodelSpecification import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.PartialModelReference import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.PartialModelSpecification import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.PatternSpecification +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.RuntimeEntry import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ScopeReference import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ScopeSpecification import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Task import hu.bme.mit.inf.dslreasoner.application.execution.util.ApplicationConfigurationParser +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import java.util.LinkedHashMap +import java.util.Optional import org.eclipse.emf.common.util.URI -import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.EPackageImport +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.DocumentLevelSpecification class ScriptExecutor { val parser = new ApplicationConfigurationParser @@ -140,11 +147,55 @@ class ScriptExecutor { val map = new LinkedHashMap if(config != null) { - for(entry : config.entries) { + for(entry : config.entries.filter(CustomEntry)) { map.put(entry.key,entry.value) } } return map } + def getRuntimeLimit(ConfigSpecification config) { + if(config === null) { + return Optional::empty + } else { + val runtimeEntry = config.entries.filter(RuntimeEntry).head + if(runtimeEntry!==null) { + return Optional::of(runtimeEntry.millisecLimit) + } else { + return Optional::empty + } + } + } + def getMemoryLimit(ConfigSpecification config) { + if(config === null) { + return Optional::empty + } else { + val memoryEntry = config.entries.filter(MemoryEntry).head + if(memoryEntry!==null) { + return Optional::of(memoryEntry.megabyteLimit) + } else { + return Optional::empty + } + } + } + def getDocumentation(ConfigSpecification config) { + if(config === null) { + return Optional::empty + } else { + val documentationEntry = config.entries.filter(DocumentationEntry).head + if(documentationEntry!==null) { + val DocumentLevelSpecification value = documentationEntry.level + val translatedValue = if(value===DocumentLevelSpecification::FULL) { + DocumentationLevel::FULL + } else if(value===DocumentLevelSpecification::NORMAL) { + DocumentationLevel::NORMAL + } else if(value===DocumentLevelSpecification::NONE) { + DocumentationLevel::NONE + } else { + throw new UnsupportedOperationException('''Unable to translate documentation level "«value»"!''') + } + return Optional::of(translatedValue) + } + } + } } \ No newline at end of file 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 dcd89981..9ae1ba6b 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,13 +1,17 @@ package hu.bme.mit.inf.dslreasoner.application.execution -import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver -import java.util.Map +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver -import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver +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.ViatraReasoner import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration +import java.util.Map +import java.util.Optional +import org.eclipse.xtext.xbase.lib.Functions.Function1 class SolverLoader { def loadSolver(Solver solver, Map config) { @@ -18,11 +22,66 @@ class SolverLoader { } } - def loadSolverConfig(Solver solver, Map config) { - switch(solver) { - case ALLOY_SOLVER: return new AlloySolverConfiguration - case SMT_SOLVER: return new SmtSolverConfiguration - case VIATRA_SOLVER: return new ViatraReasonerConfiguration + + + private def Optional getAsType( + Map config, + String key, + ScriptConsole console, + Function1 parser, + Class requestedType) + { + if(config.containsKey(key)) { + val stringValue = config.get(key) + try{ + val parsedValue = parser.apply(stringValue) + return Optional.of(parsedValue) + } catch(Exception e) { + console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''') + return Optional::empty + } + } else { + return Optional::empty + } + } + private def getAsInteger(Map config, String key, ScriptConsole console) { + 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) + } + private def getAsDouble(Map config, String key, ScriptConsole console) { + 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] + ] + } else if(solver === Solver::VIATRA_SOLVER) { + return new ViatraReasonerConfiguration => [c| + ] + } else { + throw new UnsupportedOperationException('''Unknown solver: «solver»''') } } + + def dispatch void setRunIndex(AlloySolverConfiguration config, Map parameters, int runIndex, ScriptConsole console) { + parameters.getAsBoolean("randomise",console).ifPresent[config.randomise = runIndex] + } + def dispatch void setRunIndex(LogicSolverConfiguration config, Map parameters, int runIndex, ScriptConsole console) { + + } } \ No newline at end of file diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/ApplicationConfigurationParser.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/ApplicationConfigurationParser.xtend new file mode 100644 index 00000000..ea738c5a --- /dev/null +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/ApplicationConfigurationParser.xtend @@ -0,0 +1,18 @@ +package hu.bme.mit.inf.dslreasoner.application.execution.util + +import org.eclipse.emf.common.util.URI +import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ConfigurationScript + +class ApplicationConfigurationParser { + public def parse(URI uri) { + val rs = new ResourceSetImpl + val res = rs.getResource(uri,true) + val content = res.contents.head + if(content instanceof ConfigurationScript) { + return content + } else { + throw new IllegalArgumentException('''Content is not an ConfigurationScript! (got: «content.class.simpleName»)''') + } + } +} \ No newline at end of file diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/VQLParser.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/VQLParser.xtend index f85e3dcf..0da42e0f 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/VQLParser.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/VQLParser.xtend @@ -3,6 +3,7 @@ package hu.bme.mit.inf.dslreasoner.application.execution.util import com.google.inject.Guice import com.google.inject.Injector import com.google.inject.Module +import hu.bme.mit.inf.dslreasoner.application.execution.ScriptConsole import java.util.LinkedHashMap import java.util.List import org.eclipse.emf.common.util.URI @@ -17,13 +18,11 @@ import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandalone import org.eclipse.viatra.query.patternlanguage.emf.GenmodelExtensionLoader import org.eclipse.viatra.query.patternlanguage.emf.IGenmodelMappingLoader import org.eclipse.viatra.query.patternlanguage.emf.eMFPatternLanguage.PatternModel +import org.eclipse.viatra.query.patternlanguage.emf.scoping.CompoundMetamodelProviderService +import org.eclipse.viatra.query.patternlanguage.emf.scoping.IMetamodelProvider import org.eclipse.viatra.query.patternlanguage.emf.specification.SpecificationBuilder import org.eclipse.viatra.query.runtime.api.IQuerySpecification import org.eclipse.xtext.resource.XtextResourceSet -import hu.bme.mit.inf.dslreasoner.application.execution.ScriptConsole -import org.eclipse.viatra.query.patternlanguage.emf.scoping.IMetamodelProvider -import hu.bme.mit.inf.dslreasoner.application.linking.PreloadedMetamodelProvider -import org.eclipse.viatra.query.patternlanguage.emf.scoping.CompoundMetamodelProviderService class MyModule extends EMFPatternLanguageRuntimeModule implements Module { def public Class bindAnnotationValidatorLoader() { diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/linking/ApplicationConfigurationLinkingService.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/linking/ApplicationConfigurationLinkingService.xtend index e48b74ba..41a89e6f 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/linking/ApplicationConfigurationLinkingService.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/linking/ApplicationConfigurationLinkingService.xtend @@ -79,7 +79,7 @@ class ApplicationConfigurationLinkingService extends DefaultLinkingService{ } catch(RuntimeException e){ return super.getLinkedObjects(viatraImport, viatraImport_ImportedViatra, node) } - if(res!==null && !res.contents.empty) { + if(res!==null && !res.contents.nullOrEmpty) { return #[res.contents.head] } else { return super.getLinkedObjects(viatraImport, viatraImport_ImportedViatra, node) @@ -88,7 +88,7 @@ class ApplicationConfigurationLinkingService extends DefaultLinkingService{ return super.getLinkedObjects(viatraImport, viatraImport_ImportedViatra, node) } } - + private def getNSUri(INode node) { try { val convertedValue = valueConverterService.toValue(node.text, -- cgit v1.2.3-54-g00ecf