From 28bd83cecdd9510a46aa443d6d4c5fe09e6eda93 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Fri, 14 Sep 2018 16:38:04 +0200 Subject: Update support for java and emf DATATYPES, and basic scope propagator --- .../META-INF/MANIFEST.MF | 3 +- .../ModelGenerationMethodProvider.xtend | 10 +- .../logic2viatra/ScopePropagator.xtend | 156 +++++++++++++++++++++ .../logic2viatra/patterns/GenericTypeIndexer.xtend | 6 + .../patterns/RelationDefinitionIndexer.xtend | 30 ++++ .../TypeIndexerWithPreliminaryTypeAnalysis.xtend | 11 ++ .../rules/RefinementRuleProvider.xtend | 27 +++- 7 files changed, 231 insertions(+), 12 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend (limited to 'Solvers/VIATRA-Solver') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF index b2e3667c..0241969b 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF @@ -4,7 +4,8 @@ Bundle-Name: Logic2viatra Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;singleton:=true Bundle-Version: 1.0.0.qualifier Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, - hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index ff8ab437..f43ab96d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend @@ -2,6 +2,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider @@ -9,14 +10,13 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace import java.util.Collection import java.util.List +import java.util.Set import org.eclipse.viatra.query.runtime.api.IPatternMatch import org.eclipse.viatra.query.runtime.api.IQuerySpecification import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule import org.eclipse.xtend.lib.annotations.Data -import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery -import java.util.Set class ModelGenerationStatistics { public var long transformationExecutionTime = 0 @@ -53,6 +53,7 @@ class ModelGenerationMethodProvider { ReasonerWorkspace workspace, boolean nameNewElements, TypeInferenceMethod typeInferenceMethod, + ScopePropagator scopePropagator, DocumentationLevel debugLevel ) { val statistics = new ModelGenerationStatistics @@ -66,10 +67,9 @@ class ModelGenerationMethodProvider { .map[it.patternPQuery as PQuery] .toSet - val queries = patternProvider.generateQueries(logicProblem,emptySolution,statistics,existingQueries,workspace,typeInferenceMethod,writeFiles) - + val queries = patternProvider.generateQueries(logicProblem,emptySolution,statistics,existingQueries,workspace,typeInferenceMethod,writeFiles) val //LinkedHashMap, BatchTransformationRule>> - objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries,nameNewElements,statistics) + objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries,scopePropagator,nameNewElements,statistics) val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics) val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend new file mode 100644 index 00000000..38633c07 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend @@ -0,0 +1,156 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra + +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope +import java.util.HashMap +import java.util.Map +import java.util.Set +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation +import java.util.HashSet + +class ScopePropagator { + PartialInterpretation partialInterpretation + Map type2Scope + + val Map> superScopes + val Map> subScopes + + public new(PartialInterpretation p) { + partialInterpretation = p + type2Scope = new HashMap + for(scope : p.scopes) { + type2Scope.put(scope.targetTypeInterpretation,scope) + } + + superScopes = new HashMap + subScopes = new HashMap + for(scope : p.scopes) { + superScopes.put(scope,new HashSet) + subScopes.put(scope,new HashSet) + } + + for(scope : p.scopes) { + val target = scope.targetTypeInterpretation + if(target instanceof PartialComplexTypeInterpretation) { + val supertypeInterpretations = target.supertypeInterpretation + for(supertypeInterpretation : supertypeInterpretations) { + val supertypeScope = type2Scope.get(supertypeInterpretation) + superScopes.get(scope).add(supertypeScope) + subScopes.get(supertypeScope).add(scope) + } + } + } + } + + def public propagateAllScopeConstraints() { + var boolean hadChanged + do{ + hadChanged = false + for(superScopeEntry : superScopes.entrySet) { + val sub = superScopeEntry.key + hadChanged = propagateLowerLimitUp(sub,partialInterpretation) || hadChanged + hadChanged = propagateUpperLimitDown(sub,partialInterpretation) || hadChanged + for(sup: superScopeEntry.value) { + hadChanged = propagateLowerLimitUp(sub,sup) || hadChanged + hadChanged = propagateUpperLimitDown(sub,sup) || hadChanged + } + } + } while(hadChanged) +// println('''All constraints are propagated.''') + } + + def public propagateAdditionToType(PartialTypeInterpratation t) { +// println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') + val targetScope = type2Scope.get(t) + targetScope.removeOne + val sups = superScopes.get(targetScope) + sups.forEach[removeOne] + if(this.partialInterpretation.minNewElements > 0) { + this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1 + } + if(this.partialInterpretation.maxNewElements > 0) { + this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1 + } else if(this.partialInterpretation.maxNewElements === 0) { + throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') + } + +// subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)] +// for(sup: sups) { +// subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)] +// } +// for(scope : type2Scope.values) { +// propagateUpperLimitDown(scope,partialInterpretation) +// } + + propagateAllScopeConstraints + +// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') +// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') +// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] +// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') + } + + private def propagateLowerLimitUp(Scope subScope, Scope superScope) { + if(subScope.minNewElements>superScope.minNewElements) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» +// superScope.minNewElements «superScope.minNewElements» = subScope.minNewElements «subScope.minNewElements» +// ''') + superScope.minNewElements = subScope.minNewElements + return true + } else { + return false + } + } + + private def propagateUpperLimitDown(Scope subScope, Scope superScope) { + if(superScope.maxNewElements>=0 && (superScope.maxNewElements «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» +// subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» +// ''') + subScope.maxNewElements = superScope.maxNewElements + return true + } else { + return false + } + } + + private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { + if(subScope.minNewElements>p.minNewElements) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes +// p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» +// ''') + p.minNewElements = subScope.minNewElements + return true + } else { + return false + } + } + + private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { + if(p.maxNewElements>=0 && (p.maxNewElements nodes +// subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» +// ''') + subScope.maxNewElements = p.maxNewElements + return true + } else { + return false + } + } + private def removeOne(Scope scope) { + if(scope.maxNewElements===0) { + throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') + } else if(scope.maxNewElements>0) { + scope.maxNewElements= scope.maxNewElements-1 + } + if(scope.minNewElements>0) { + scope.minNewElements= scope.minNewElements-1 + } + } +} + \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend index d11b5960..d6a15c1a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend @@ -155,6 +155,11 @@ class GenericTypeIndexer extends TypeIndexer { find supertypeStar(type,definedSupertype); TypeDefinition(definedSupertype); } + + private pattern scopeDisallowsNewElementsFromType(typeInterpretation:PartialComplexTypeInterpretation) { + Scope.targetTypeInterpretation(scope,typeInterpretation); + Scope.maxNewElements(scope,0); + } ''' public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) { @@ -190,6 +195,7 @@ class GenericTypeIndexer extends TypeIndexer { Type.name(type,"«type.name»"); find possibleDynamicType(problem,interpretation,dynamic,element); find supertypeStar(dynamic,type); + neg find scopeDisallowsNewElementsFromType(dynamic); } ''' } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend index 39b6fbc0..329d3658 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend @@ -24,6 +24,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeCo import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint class RelationDefinitionIndexer { val PatternGenerator base; @@ -141,6 +142,35 @@ class RelationDefinitionIndexer { throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') } } + private dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) { + val touple = constraint.variablesTuple + if(touple.size == 1) { + val inputKey = constraint.equivalentJudgement.inputKey + if(inputKey instanceof EClassTransitiveInstancesKey) { + return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, + (constraint.getVariablesTuple.get(0) as PVariable).canonizeName) + } else if(inputKey instanceof EDataTypeInSlotsKey){ + return '''// type constraint is enforced by construction''' + } + + } else if(touple.size == 2){ + val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey + if(key instanceof EReference) { + return base.referRelationByName( + key, + (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, + (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, + modality.toMustMay) + } else if (key instanceof EAttribute) { + return base.referAttributeByName(key, + (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, + (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, + modality.toMustMay) + } else throw new UnsupportedOperationException('''unknown key: «key.class»''') + } else { + throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') + } + } private dispatch def transformConstraint(Equality equality, Modality modality) { val a = equality.who diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend index 67a886d1..d3af0426 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend @@ -72,6 +72,15 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ null } ''' + private pattern scopeDisallowsNew«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation) { + find interpretation(problem,interpretation); + PartialInterpretation.scopes(interpretation,scope); + Scope.targetTypeInterpretation(scope,typeInterpretation); + Scope.maxNewElements(scope,0); + PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); + Type.name(type,"«type.name»"); + } + /** * An element may be an instance of type "«type.name»". */ @@ -82,6 +91,7 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ «FOR inhibitorType : inhibitorTypes» neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» «ENDFOR» + neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); neg find isPrimitive(element); } or { find interpretation(problem,interpretation); @@ -89,6 +99,7 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ «FOR inhibitorType : inhibitorTypes» neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» «ENDFOR» + neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); neg find isPrimitive(element); } or «ENDIF» diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index 0a21d99e..20d24b77 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend @@ -6,6 +6,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation @@ -31,6 +32,7 @@ class RefinementRuleProvider { def LinkedHashMap>> createObjectRefinementRules( GeneratedPatterns patterns, + ScopePropagator scopePropagator, boolean nameNewElement, ModelGenerationStatistics statistics ) @@ -41,7 +43,7 @@ class RefinementRuleProvider { val inverseRelation = LHSEntry.key.inverseContainment val type = LHSEntry.key.newType val lhs = LHSEntry.value as IQuerySpecification> - val rule = createObjectCreationRule(containmentRelation,inverseRelation,type,lhs,nameNewElement,statistics) + val rule = createObjectCreationRule(containmentRelation,inverseRelation,type,lhs,nameNewElement,scopePropagator,statistics) res.put(LHSEntry.key,rule) } return res @@ -53,6 +55,7 @@ class RefinementRuleProvider { Type type, IQuerySpecification> lhs, boolean nameNewElement, + ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { val name = '''addObject_«type.name.canonizeName»« @@ -80,10 +83,10 @@ class RefinementRuleProvider { // Existence interpretation.newElements+=newElement - interpretation.maxNewElements=interpretation.maxNewElements-1 + /*interpretation.maxNewElements=interpretation.maxNewElements-1 if(interpretation.minNewElements > 0) { interpretation.minNewElements=interpretation.minNewElements-1 - } + }*/ // Types typeInterpretation.elements += newElement @@ -94,6 +97,10 @@ class RefinementRuleProvider { // Inverse Containment val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container] inverseRelationInterpretation.relationlinks+=newLink2 + + // Scope propagation + scopePropagator.propagateAdditionToType(typeInterpretation) + statistics.addExecutionTime(System.nanoTime-startTime) ] } else { @@ -113,10 +120,10 @@ class RefinementRuleProvider { // Existence interpretation.newElements+=newElement - interpretation.maxNewElements=interpretation.maxNewElements-1 + /*interpretation.maxNewElements=interpretation.maxNewElements-1 if(interpretation.minNewElements > 0) { interpretation.minNewElements=interpretation.minNewElements-1 - } + }*/ // Types typeInterpretation.elements += newElement @@ -124,6 +131,10 @@ class RefinementRuleProvider { // ContainmentRelation val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] relationInterpretation.relationlinks+=newLink + + // Scope propagation + scopePropagator.propagateAdditionToType(typeInterpretation) + statistics.addExecutionTime(System.nanoTime-startTime) ] } @@ -141,15 +152,19 @@ class RefinementRuleProvider { // Existence interpretation.newElements+=newElement + /* interpretation.maxNewElements=interpretation.maxNewElements-1 if(interpretation.minNewElements > 0) { interpretation.minNewElements=interpretation.minNewElements-1 - } + }*/ // Types typeInterpretation.elements += newElement typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] + // Scope propagation + scopePropagator.propagateAdditionToType(typeInterpretation) + statistics.addExecutionTime(System.nanoTime-startTime) ] } -- cgit v1.2.3-70-g09d2 From 94d65ce02c5ef302f91bf383643c2535001ae6a9 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Fri, 14 Sep 2018 16:38:34 +0200 Subject: Scope initialisation is default --- .../PartialInterpretationInitialiser.xtend | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'Solvers/VIATRA-Solver') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend index cc76ce3f..d0fdeac4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend @@ -41,6 +41,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral 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 +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation @Data class Problem2PartialInterpretationTrace { Map type2Interpretation @@ -201,11 +202,25 @@ class PartialInterpretationInitialiser { val typeInterpretation = typeDeclaration.initialisePartialTypeInterpretation(engine) interpretation.partialtypeinterpratation += typeInterpretation type2Interpretation.put(typeDeclaration,typeInterpretation) + interpretation.scopes += initialiseTypeScope(typeInterpretation, minNewElementsByType.get(typeDeclaration),maxNewElementsByType.get(typeDeclaration)) + } interpretation.problem.connectSuperypes(type2Interpretation) return type2Interpretation } + def private initialiseTypeScope(PartialTypeInterpratation interpretation, Integer min, Integer max) { + val res = createScope + res.targetTypeInterpretation = interpretation + if(min !== null) { + res.minNewElements = min + } + if(max !== null) { + res.maxNewElements = max + } + return res + } + def private connectSuperypes(LogicProblem problem, Map trace) { for(typeDeclaration : problem.types.filter(TypeDeclaration)) { val supertypes = typeDeclaration.transitiveClosurePlus[it.supertypes] -- cgit v1.2.3-70-g09d2 From c2b846f93e4807d89e9cb1d385a5f540d89a69c4 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Fri, 14 Sep 2018 16:39:19 +0200 Subject: If scope available, then it is maintained during generation via VS --- .../mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | 7 +++++++ .../reasoner/dse/BestFirstStrategyForModelGeneration.java | 2 +- .../reasoner/dse/ModelGenerationCompositeObjective.xtend | 2 +- .../inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend | 7 +++++-- .../viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend | 2 +- .../viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend | 2 +- 6 files changed, 16 insertions(+), 6 deletions(-) (limited to 'Solvers/VIATRA-Solver') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index 42aa1654..dfd8ca1a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend @@ -10,6 +10,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage @@ -55,18 +56,24 @@ class ViatraReasoner extends LogicReasoner{ val transformationStartTime = System.nanoTime + + val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { workspace.writeModel(emptySolution,"init.partialmodel") } emptySolution.problemConainer = problem + val ScopePropagator scopePropagator = new ScopePropagator(emptySolution) + scopePropagator.propagateAllScopeConstraints + val method = modelGenerationMethodProvider.createModelGenerationMethod( problem, emptySolution, workspace, viatraConfig.nameNewElements, viatraConfig.typeInferenceMethod, + scopePropagator, viatraConfig.documentationLevel ) diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index effc37f8..60f46033 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java @@ -383,4 +383,4 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { return Arrays.equals(part, substring); } } -} +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend index 1ca2343f..2489c751 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend @@ -63,7 +63,7 @@ class ModelGenerationCompositeObjective implements IObjective{ sum+=multiplicity sum += unfinishedWFsFitness//*0.5 -// println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') + //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') return sum } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend index d3497ef2..69efe0d7 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend @@ -23,8 +23,11 @@ class ScopeObjective implements IObjective{ override getFitness(ThreadContext context) { val interpretation = context.model as PartialInterpretation - val res = interpretation.minNewElements - return res.doubleValue + var res = interpretation.minNewElements.doubleValue + for(scope : interpretation.scopes) { + res += scope.minNewElements*2 + } + return res } override isHardObjective() { true } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend index 0fd20fa3..e0111cf6 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend @@ -37,7 +37,7 @@ class UnfinishedWFObjective implements IObjective { var sumOfMatches = 0 for(matcher : matchers) { val number = matcher.countMatches -// println('''«matcher.patternName» = «number»''') + //println('''«matcher.patternName» = «number»''') sumOfMatches+=number } return sumOfMatches.doubleValue diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend index 4fd297ca..5a528a9e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend @@ -18,7 +18,7 @@ class WF2ObjectiveConverter { { val res = new ConstraintsObjective('''unfinishedWFs''', unfinishedWF.map[ - new QueryConstraint(it.fullyQualifiedName,it,1.0) + new QueryConstraint(it.fullyQualifiedName,it,2.0) ].toList ) res.withComparator(Comparators.LOWER_IS_BETTER) -- cgit v1.2.3-70-g09d2