From 59a53fc819355fb2809b23544a5ca19ffff802fb Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Mon, 16 Jul 2018 18:25:34 +0200 Subject: Scope support for attributes --- .../application/ApplicationConfiguration.xtext | 8 +- .../execution/GenerationTaskExecutor.xtend | 153 ++++++++++-------- .../application/execution/ScopeLoader.xtend | 171 ++++++++++++++++++--- 3 files changed, 239 insertions(+), 93 deletions(-) (limited to 'Application/hu.bme.mit.inf.dslreasoner.application/src/hu') diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfiguration.xtext b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfiguration.xtext index 1f9495cf..6af31723 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfiguration.xtext +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfiguration.xtext @@ -15,8 +15,8 @@ Command : QualifiedName returns ecore::EString: ID ('.' ID)*; -//terminal REAL returns ecore::EBigDecimal: '-'? INT '.' INT; -//terminal INTEGER returns ecore::EInt: '-'? INT; +REALLiteral returns ecore::EBigDecimal: '-'? INT '.' INT; +INTLiteral returns ecore::EInt: '-'? INT; /////////////////////////////////////////////////// // Imports @@ -144,8 +144,8 @@ StringReference: {StringScope} 'string'; NumberSpecification: ExactNumber | IntervallNumber | IntEnumberation | RealEnumeration | StringEnumeration; ExactNumber: exactNumber = INT | exactUnlimited ?= '*'; IntervallNumber: min = INT '..' (maxNumber = INT | maxUnlimited ?= '*'); -IntEnumberation: {IntEnumberation} '{' (entry += INT (',' entry += INT)*)?'}'; -RealEnumeration: {RealEnumeration} '{' (entry += INT (',' entry += INT)*)?'}'; +IntEnumberation: {IntEnumberation} '{' (entry += INTLiteral (',' entry += INTLiteral)*)?'}'; +RealEnumeration: {RealEnumeration} '{' (entry += REALLiteral (',' entry += REALLiteral)*)?'}'; StringEnumeration: {StringEnumeration} '{' (entry += STRING (',' entry += STRING)*)?'}'; ScopeDeclaration: 'scope' name = ID specification = ScopeSpecification; 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 40ffaf28..9a8ac8a3 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 @@ -143,89 +143,114 @@ class GenerationTaskExecutor { 1 } ] - solverConfig.typeScopes = scopeLoader.loadScope( + + val typeScopes = scopeLoader.loadScope( scopeSpecification, problem, ecore2Logic, 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 - // 6.1 calculating the runs - val runs = if(task.runSpecified) { task.runs } else { 1 } - monitor.worked(50) - - console.writeMessage("Model generation started") - for(run : 1..runs) { - monitor.subTask('''Solving problem«IF runs>0» «run»/«runs»«ENDIF»''') + // If the type scope contains errors, then the problem is inconsistent + if(!typeScopes.value.empty) { + monitor.worked(50) + console.writeMessage("Model generation started") + typeScopes.value.forEach[console.writeMessage(it)] - // 6.2 For each run, the configuration and the workspace is adjusted - solverLoader.setRunIndex(solverConfig,configurationMap,run,console) - solverConfig.progressMonitor = new EclipseBasedProgressMonitor(monitor) - val reasonerWorkspaceForRun = if(runs > 1) { - reasonerWorkspace.subWorkspace('''run«run»''',"") => [initAndClear] - } else { - reasonerWorkspace + val runs = if(task.runSpecified) { task.runs } else { 1 } + for(run : 1..runs) { + console.writeMessage('''Problem is inconsistent, no model is created!''') + val statistics = new LinkedHashMap + statistics.put("Task",(task.eContainer as ConfigurationScript).commands.indexOf(task)+1) + statistics.put("Run",run) + statistics.put("Result","InconsistencyResult") + statistics.put("Domain to logic transformation time",domain2LogicTransformationTime/1000000) + statistics.put("Logic to solver transformation time",0) + statistics.put("Solver time",0) + statistics.put("Postprocessing time",0) + console.addStatistics(statistics) } - // 7. Solver call - val solution = solver.solve(problem,solverConfig,reasonerWorkspaceForRun) - console.writeMessage(solution.soutionDescription.toString) + } else { + solverConfig.typeScopes = typeScopes.key + + // 5.3 set resource limits + documentationLevel.ifPresent[solverConfig.documentationLevel = it] + runtieLimit.ifPresent[solverConfig.runtimeLimit = it] + memoryLimit.ifPresent[solverConfig.memoryLimit = it] - // 8. Solution processing + // 6. execute the solver on the problem with the configuration + // 6.1 calculating the runs + val runs = if(task.runSpecified) { task.runs } else { 1 } + monitor.worked(50) - // 8.1 Visualisation - var solutionVisualisationTime = System.nanoTime - if(solution instanceof ModelResult) { - val interpretations = solver.getInterpretations(solution) - val outputWorkspaceForRun = if(runs > 1) { - outputWorkspace.subWorkspace('''run«run»''',"") => [initAndClear] + console.writeMessage("Model generation started") + for(run : 1..runs) { + monitor.subTask('''Solving problem«IF runs>0» «run»/«runs»«ENDIF»''') + + // 6.2 For each run, the configuration and the workspace is adjusted + solverLoader.setRunIndex(solverConfig,configurationMap,run,console) + solverConfig.progressMonitor = new EclipseBasedProgressMonitor(monitor) + val reasonerWorkspaceForRun = if(runs > 1) { + reasonerWorkspace.subWorkspace('''run«run»''',"") => [initAndClear] } else { - outputWorkspace + reasonerWorkspace } - for(interpretationIndex : 0..0» «run»/«runs»«ENDIF»: Visualising solution «interpretationIndex+1»/«interpretations.size»''') - val interpretation = interpretations.get(interpretationIndex) - val model = logic2Ecore.transformInterpretation(interpretation,modelGeneration.trace) - outputWorkspaceForRun.writeModel(model,'''model«IF runs>1»_«run»«ENDIF»_«interpretationIndex+1».xmi''') + // 7. Solver call + val solution = solver.solve(problem,solverConfig,reasonerWorkspaceForRun) + console.writeMessage(solution.soutionDescription.toString) + + // 8. Solution processing + + // 8.1 Visualisation + var solutionVisualisationTime = System.nanoTime + if(solution instanceof ModelResult) { + val interpretations = solver.getInterpretations(solution) + val outputWorkspaceForRun = if(runs > 1) { + outputWorkspace.subWorkspace('''run«run»''',"") => [initAndClear] + } else { + outputWorkspace + } - val representation = solution.representation.get(interpretationIndex) - if(representation instanceof PartialInterpretation) { - val vis1 = new PartialInterpretation2Gml - val gml = vis1.transform(representation) - outputWorkspaceForRun.writeText('''model«IF runs>1»_«run»«ENDIF»_«interpretationIndex+1».gml''',gml) - if(representation.newElements.size + representation.problem.elements.size < 150) { - val vis2 = new GraphvizVisualiser - val dot = vis2.visualiseConcretization(representation) - dot.writeToFile(outputWorkspaceForRun,'''model«IF runs>1»_«run»«ENDIF»_«interpretationIndex+1».png''') + for(interpretationIndex : 0..0» «run»/«runs»«ENDIF»: Visualising solution «interpretationIndex+1»/«interpretations.size»''') + val interpretation = interpretations.get(interpretationIndex) + val model = logic2Ecore.transformInterpretation(interpretation,modelGeneration.trace) + outputWorkspaceForRun.writeModel(model,'''model«IF runs>1»_«run»«ENDIF»_«interpretationIndex+1».xmi''') + + val representation = solution.representation.get(interpretationIndex) + if(representation instanceof PartialInterpretation) { + val vis1 = new PartialInterpretation2Gml + val gml = vis1.transform(representation) + outputWorkspaceForRun.writeText('''model«IF runs>1»_«run»«ENDIF»_«interpretationIndex+1».gml''',gml) + if(representation.newElements.size + representation.problem.elements.size < 150) { + val vis2 = new GraphvizVisualiser + val dot = vis2.visualiseConcretization(representation) + dot.writeToFile(outputWorkspaceForRun,'''model«IF runs>1»_«run»«ENDIF»_«interpretationIndex+1».png''') + } } + monitor.worked(100) } - monitor.worked(100) + } else { + monitor.worked(solverConfig.solutionScope.numberOfRequiredSolution*100) } - } else { - monitor.worked(solverConfig.solutionScope.numberOfRequiredSolution*100) + solutionVisualisationTime = System.nanoTime - solutionVisualisationTime + + // 8.2 Statistics + val statistics = new LinkedHashMap + statistics.put("Task",(task.eContainer as ConfigurationScript).commands.indexOf(task)+1) + statistics.put("Run",run) + statistics.put("Result",solution.class.simpleName) + statistics.put("Domain to logic transformation time",domain2LogicTransformationTime/1000000) + statistics.put("Logic to solver transformation time",solution.statistics.transformationTime) + statistics.put("Solver time",solution.statistics.solverTime) + statistics.put("Postprocessing time",solutionVisualisationTime) + for(entry: solution.statistics.entries) { + statistics.put(entry.name,statisticsUtil.readValue(entry)) + } + console.addStatistics(statistics) } - solutionVisualisationTime = System.nanoTime - solutionVisualisationTime - // 8.2 Statistics - val statistics = new LinkedHashMap - statistics.put("Task",(task.eContainer as ConfigurationScript).commands.indexOf(task)+1) - statistics.put("Run",run) - statistics.put("Result",solution.class.simpleName) - statistics.put("Domain to logic transformation time",domain2LogicTransformationTime/1000000) - statistics.put("Logic to solver transformation time",solution.statistics.transformationTime) - statistics.put("Solver time",solution.statistics.solverTime) - statistics.put("Postprocessing time",solutionVisualisationTime) - for(entry: solution.statistics.entries) { - statistics.put(entry.name,statisticsUtil.readValue(entry)) - } - console.addStatistics(statistics) } console.flushStatistics console.writeMessage("Model generation finished") diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend index ee1a92f0..9b2b4a3e 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend @@ -14,49 +14,172 @@ import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.StringTyp import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.PartialModelRelation2Assertion +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.NaryRelationLink +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.UnaryElementRelationLink +import java.math.BigDecimal +import java.util.HashMap +import java.util.LinkedList +import java.util.List +import java.util.Map +import java.util.Set import org.eclipse.emf.ecore.EClass +import org.eclipse.xtend.lib.annotations.Data + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral + +@Data class KnownElements { + val Map> knownElementsByType + val Set knownIntegers + val Set knownReals + val Set knownStrings +} class ScopeLoader { - def TypeScopes loadScope(ScopeSpecification specification, LogicProblem problem, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { + def loadScope(ScopeSpecification specification, LogicProblem problem, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { val res = new TypeScopes + val knownElements = initialiseknownElements(problem,res) + val inconsistencies = new LinkedList() + for(scopeSpecification : specification.scopes) { - setSpecification(scopeSpecification,res,ecore2Logic,trace) + setSpecification(scopeSpecification,res,knownElements,ecore2Logic,trace,inconsistencies) } - return res + + return res -> inconsistencies + } + + def protected initialiseknownElements(LogicProblem p, TypeScopes s) { + val Map> res = new HashMap + for(definedType : p.types.filter(TypeDefinition)) { + val supertypes = definedType.transitiveClosureStar[x|x.supertypes] + for(supertype : supertypes) { + for(element : definedType.elements) { + res.putOrAddToSet(supertype,element) + } + } + } + val partailModelContents = p.annotations.filter(PartialModelRelation2Assertion).map[target].toList.map[eAllContents.toIterable].flatten.toList + s.knownIntegers += partailModelContents.filter(IntLiteral).map[it.value] + s.knownReals += partailModelContents.filter(RealLiteral).map[it.value] + s.knownStrings += partailModelContents.filter(StringLiteral).map[it.value] + + res + } + + def dispatch getElements(UnaryElementRelationLink link) { + #[link.param1] + } + def dispatch getElements(BinaryElementRelationLink link) { + #[link.param1,link.param2] + } + def dispatch getElements(NaryRelationLink link) { + link.elements } - def dispatch setSpecification(ObjectTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { - //val existingObjects = - aggregated.minNewElements = getLowerLimit(scope.number) - aggregated.maxNewElements = getUpperLimit(scope.number) + def dispatch setSpecification(ObjectTypeScope scope, TypeScopes aggregated, Map> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List inconsistencies) { + val numberOfKnownElements = knownElements.values.flatten.toSet.size + + aggregated.minNewElements = updateLowerLimit(scope.isSetsNew,numberOfKnownElements,aggregated.minNewElements,getLowerLimit(scope.number)) + aggregated.maxNewElements = updateUpperLimit(scope.isSetsNew,numberOfKnownElements,aggregated.maxNewElements,getUpperLimit(scope.number)) } - def dispatch setSpecification(ClassTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { + def dispatch setSpecification(ClassTypeScope scope, TypeScopes aggregated, Map> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List inconsistencies) { val target = scope.type.element - if(target.feature != null) { + if(target.feature !== null) { throw new IllegalArgumentException('''Feature scopes are not supported: "«target.feature.name»"!''') } else { val targetClassifier = target.classifier if(targetClassifier instanceof EClass) { val type = ecore2Logic.TypeofEClass(trace,targetClassifier) - aggregated.minNewElementsByType.put(type,getLowerLimit(scope.number)) - aggregated.maxNewElementsByType.put(type,getUpperLimit(scope.number)) + val known = type.lookup(knownElements).size + aggregated.minNewElementsByType.put(type, + updateLowerLimit( + scope.setsNew, + known, + type.lookup(aggregated.minNewElementsByType), + getLowerLimit(scope.number) + ) + ) + aggregated.maxNewElementsByType.put(type, + updateUpperLimit( + scope.setsNew, + known, + type.lookup(aggregated.minNewElementsByType), + getUpperLimit(scope.number) + ) + ) } else { throw new IllegalArgumentException('''Non-EClass scopes are not supported: "«targetClassifier.name»"!''') } } } - def dispatch setSpecification(IntegerTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { - aggregated.minNewIntegers = scope.number.lowerLimit - aggregated.maxNewIntegers = scope.number.upperLimit + def dispatch setSpecification(IntegerTypeScope scope, TypeScopes aggregated, Map> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List inconsistencies) { + val number = scope.number + if(number instanceof IntEnumberation) { + addToKnownCollection(aggregated.knownIntegers,number.entry,scope.isSetsNew,inconsistencies) + } else { + aggregated.minNewIntegers = updateLowerLimit(scope.isSetsNew,aggregated.knownIntegers.size,aggregated.minNewIntegers,number.lowerLimit) + aggregated.maxNewIntegers = updateLowerLimit(scope.isSetsNew,aggregated.knownIntegers.size,aggregated.maxNewIntegers,number.upperLimit) + } + } + + def dispatch setSpecification(RealTypeScope scope, TypeScopes aggregated, Map> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List inconsistencies) { + val number = scope.number + if(number instanceof RealEnumeration) { + val x = number.entry; + addToKnownCollection(aggregated.knownReals,x,scope.isSetsNew,inconsistencies) + } else { + aggregated.minNewReals = updateLowerLimit(scope.isSetsNew,aggregated.knownReals.size,aggregated.minNewReals,number.lowerLimit) + aggregated.maxNewReals = updateLowerLimit(scope.isSetsNew,aggregated.knownReals.size,aggregated.maxNewReals,number.upperLimit) + } + } + def dispatch setSpecification(StringTypeScope scope, TypeScopes aggregated, Map> knownElements, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace, List inconsistencies) { + val number = scope.number + if(number instanceof StringEnumeration) { + addToKnownCollection(aggregated.knownStrings,number.entry,scope.isSetsNew,inconsistencies) + } else { + aggregated.minNewStrings = updateLowerLimit(scope.isSetsNew,aggregated.knownStrings.size,aggregated.minNewStrings,number.lowerLimit) + aggregated.maxNewStrings = updateLowerLimit(scope.isSetsNew,aggregated.knownStrings.size,aggregated.maxNewStrings,number.upperLimit) + } + } + def addToKnownCollection(Set known, List definedInScope, boolean isSetNew, List inconsistencies) { + if(isSetNew) { + known += definedInScope + } else { + if(!definedInScope.containsAll(known)) { + val notDefinedInScope = known.filter[!definedInScope.contains(it)] + inconsistencies += '''Inconsistent scope: problem already contains literal«IF notDefinedInScope.size > 0»s«ENDIF» that excluded by a scope: «FOR e: notDefinedInScope SEPARATOR ", "»«e»«ENDFOR».''' + } + known.clear + known += definedInScope + } } - def dispatch setSpecification(RealTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { - aggregated.minNewReals = scope.number.lowerLimit - aggregated.maxNewReals = scope.number.upperLimit + + def updateLowerLimit(boolean isAdditional, int known, int original, int value) { + if(isAdditional) { + return Math.max(original,value) + } else { + return Math.max(original,value-known) + } } - def dispatch setSpecification(StringTypeScope scope, TypeScopes aggregated, Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { - aggregated.minNewStrings = scope.number.lowerLimit - aggregated.maxNewStrings = scope.number.upperLimit + def updateUpperLimit(boolean isAdditional, int known, int original, int value) { + if(isAdditional) { + return Math.min(original,value) + } else { + val target = if(value == Integer.MAX_VALUE) { Integer.MAX_VALUE } else {value-known} + return Math.min(original,target) + } } def dispatch getLowerLimit(IntervallNumber specification) { @@ -70,14 +193,12 @@ class ScopeLoader { def dispatch getLowerLimit(RealEnumeration specification) { 0 } def dispatch getLowerLimit(StringEnumeration specification) { 0 } def dispatch getUpperLimit(IntervallNumber specification) { - if(specification.isMaxUnlimited) return -1 + if(specification.isMaxUnlimited) return Integer.MAX_VALUE else return specification.maxNumber } def dispatch getUpperLimit(ExactNumber specification) { - if(specification.isExactUnlimited) return -1 + if(specification.isExactUnlimited) return Integer.MAX_VALUE else return specification.exactNumber } - def dispatch getUpperLimit(IntEnumberation specification) { 0 } - def dispatch getUpperLimit(RealEnumeration specification) { 0 } - def dispatch getUpperLimit(StringEnumeration specification) { 0 } + } \ No newline at end of file -- cgit v1.2.3-70-g09d2