From 64138e8d91bc8d7bb54d9b042f872b43550dec16 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 24 Jul 2019 10:59:02 +0200 Subject: Cardinality propagator WIP --- .../viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index e1be2742..b6fdbe06 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -1,6 +1,6 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns import java.util.ArrayList -- cgit v1.2.3-54-g00ecf From 53ce0bea21c18061eabfd890f6ea6776fe4e1d08 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 12 May 2020 02:38:04 +0200 Subject: advanced goal heuristics for missing containment and non-cont. edges --- .../ModelGenerationMethodProvider.xtend | 2 +- .../MultiplicityGoalConstraintCalculator.xtend | 19 ++++- .../patterns/PConstraintTransformer.xtend | 14 ++-- .../logic2viatra/patterns/PatternProvider.xtend | 25 +++++- .../rules/GoalConstraintProvider.xtend | 89 ++++++++++++++++++++-- .../dse/ModelGenerationCompositeObjective.xtend | 15 ++-- 6 files changed, 139 insertions(+), 25 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend') 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 be11ed78..ca09ae00 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 @@ -77,7 +77,7 @@ class ModelGenerationMethodProvider { objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, queries,scopePropagator,nameNewElements,statistics) val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics) - val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) + val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries) val unfinishedWF = queries.getUnfinishedWFQueries.values val invalidWF = queries.getInvalidWFQueries.values diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend index e05160d0..e1358fb6 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend @@ -10,23 +10,33 @@ class MultiplicityGoalConstraintCalculator { val String targetRelationName; val IQuerySpecification querySpecification; var ViatraQueryMatcher matcher; + val boolean containment + val int cost - public new(String targetRelationName, IQuerySpecification querySpecification) { + public new(String targetRelationName, IQuerySpecification querySpecification, boolean containment, int cost) { this.targetRelationName = targetRelationName this.querySpecification = querySpecification this.matcher = null + this.containment = containment + this.cost = cost } public new(MultiplicityGoalConstraintCalculator other) { this.targetRelationName = other.targetRelationName this.querySpecification = other.querySpecification this.matcher = null + this.containment = other.containment + this.cost = other.cost } def public getName() { targetRelationName } + def isContainment() { + return containment + } + def public init(Notifier notifier) { val engine = ViatraQueryEngine.on(new EMFScope(notifier)) matcher = querySpecification.getMatcher(engine) @@ -36,11 +46,14 @@ class MultiplicityGoalConstraintCalculator { var res = 0 val allMatches = this.matcher.allMatches for(match : allMatches) { - //println(targetRelationName+ " missing multiplicity: "+match.get(3)) + val missingMultiplicity = match.get(4) as Integer res += missingMultiplicity + if(missingMultiplicity!=0) { + println(targetRelationName+ " missing multiplicity: "+missingMultiplicity) + } } //println(targetRelationName+ " all missing multiplicities: "+res) - return res + return res*cost } } \ 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/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend index 4a8da38c..a4dcefbf 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend @@ -235,10 +235,10 @@ class PConstraintTransformer { «ENDFOR» check( «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR» - «IF variable2Type.values.filter(RealTypeReference).empty» - || - («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)») - «ENDIF» +««« «IF variable2Type.values.filter(RealTypeReference).empty» +««« || +««« («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)») +««« «ENDIF» ); ''' } else { // Must or Current @@ -246,9 +246,9 @@ class PConstraintTransformer { «FOR variable: e.affectedVariables» PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)» «ENDFOR» - «IF variable2Type.values.filter(RealTypeReference).empty» - check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»); - «ENDIF» +««« «IF variable2Type.values.filter(RealTypeReference).empty» +««« check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»); +««« «ENDIF» ''' } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index 750107f6..cfea499b 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend @@ -27,7 +27,8 @@ import java.util.HashMap @Data class GeneratedPatterns { public Map>> invalidWFQueries public Map>> unfinishedWFQueries - public Map>> unfinishedMulticiplicityQueries + public Map>> unfinishedContainmentMulticiplicityQueries + public Map>> unfinishedNonContainmentMulticiplicityQueries public Map>> refineObjectQueries public Map>> refineTypeQueries public Map, IQuerySpecification>> refinerelationQueries @@ -86,8 +87,23 @@ class PatternProvider { invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] val Map>> unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] - val Map>> - unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)] + + val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem) + val unfinishedContainmentMultiplicities = new HashMap + val unfinishedNonContainmentMultiplicities = new HashMap + for(entry : unfinishedMultiplicities.entrySet) { + val relation = entry.key + val value = entry.value.lookup(queries) + if(problem.containmentHierarchies.head.containmentRelations.contains(relation)) { + unfinishedContainmentMultiplicities.put(relation,value) + } else { + unfinishedNonContainmentMultiplicities.put(relation,value) + } + } +// val Map>> +// unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)] +// + val Map>> refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] val Map>> @@ -101,7 +117,8 @@ class PatternProvider { return new GeneratedPatterns( invalidWFQueries, unfinishedWFQueries, - unfinishedMultiplicityQueries, + unfinishedContainmentMultiplicities, + unfinishedNonContainmentMultiplicities, refineObjectsQueries, refineTypeQueries, refineRelationQueries, diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index e1be2742..87f7e339 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -1,18 +1,97 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns import java.util.ArrayList +import java.util.HashMap +import java.util.LinkedList +import java.util.List +import java.util.Map +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 static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class GoalConstraintProvider { - def public getUnfinishedMultiplicityQueries(GeneratedPatterns patterns) { - val multiplicityQueries = patterns.unfinishedMulticiplicityQueries - val res = new ArrayList(multiplicityQueries.size) - for(multiplicityQuery : multiplicityQueries.entrySet) { + val calculateObjectCost = true + + def public getUnfinishedMultiplicityQueries(LogicProblem p, GeneratedPatterns patterns) { + val res = new ArrayList() + + res.addAll(patterns.unfinishedContainmentMulticiplicityQueries,true) + if(calculateObjectCost) { + val middingObjectCost = calculateMissingObjectCost(p) + res.addAll(patterns.unfinishedNonContainmentMulticiplicityQueries,false) + } else { + res.addAll(patterns.unfinishedNonContainmentMulticiplicityQueries,false) + } + return res + } + + def addAll(ArrayList res, Map>> queries, boolean containment) { + for(multiplicityQuery : queries.entrySet) { val targetRelationName = multiplicityQuery.key.name val query = multiplicityQuery.value - res += new MultiplicityGoalConstraintCalculator(targetRelationName,query); + res += new MultiplicityGoalConstraintCalculator(targetRelationName,query,containment,1); + } + } + def addAll( + ArrayList res, + Map>> queries, + boolean containment, + Map cost + ) { + for(multiplicityQuery : queries.entrySet) { + val targetRelationName = multiplicityQuery.key.name + val query = multiplicityQuery.value + res += new MultiplicityGoalConstraintCalculator(targetRelationName,query,containment,multiplicityQuery.key.lookup(cost)) + } + } + + def calculateMissingObjectCost(LogicProblem p) { + val containments = p.containmentHierarchies.head.containmentRelations + val containment2Lower = containments.toInvertedMap[containment | + val lower = p.annotations.filter(LowerMultiplicityAssertion).filter[it.relation === containment].head + if(lower !== null) { lower.lower } + else { 0 } + ] + val types = p.types + val Map>> type2NewCost = new HashMap + for(type:types) { + val allSupertypes = (#[type] + type.supertypes).toSet + val allOutgoingContainments = containments.filter[allSupertypes.contains((it.parameters.get(0) as ComplexTypeReference).referred)] + val list = new LinkedList + for(outgoingContainment : allOutgoingContainments) { + val value = containment2Lower.get(outgoingContainment) + if(value>0) { + list.add((outgoingContainment.parameters.get(1) as ComplexTypeReference).referred + -> value) + } + } + type2NewCost.put(type, list) + } + val res = new HashMap + for(containment : containments) { + val key = containment + val value = (containment.parameters.get(1) as ComplexTypeReference).referred.count(type2NewCost) + //println('''«key.name» --> «value» new''') + res.put(key,value) } return res } + + private def int count(Type t, Map>> containments) { + val list = containments.get(t) + var r = 1 + for(element : list) { + r += element.value * element.key.count(containments) + } + return r + } } \ 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 9e4792e0..e75cae41 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 @@ -55,17 +55,22 @@ class ModelGenerationCompositeObjective implements IObjective{ //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) - - var multiplicity = 0.0 + var containmentMultiplicity = 0.0 + var nonContainmentMultiplicity = 0.0 for(multiplicityObjective : unfinishedMultiplicityObjectives) { - multiplicity+=multiplicityObjective.getFitness(context) + if(multiplicityObjective.containment) { + containmentMultiplicity+=multiplicityObjective.getFitness(context) + } else { + nonContainmentMultiplicity+=multiplicityObjective.getFitness(context) + } } var sum = 0.0 sum += scopeFitnes - sum +=multiplicity + sum += containmentMultiplicity + sum += Math.sqrt(nonContainmentMultiplicity) sum += unfinishedWFsFitness//*0.5 - println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') + //println('''Sum=«sum»|Scope=«scopeFitnes»|ContainmentMultiplicity=«containmentMultiplicity»|NonContainmentMultiplicity=«nonContainmentMultiplicity»|WFs=«unfinishedWFsFitness»''') return sum } -- cgit v1.2.3-54-g00ecf From c0568c4373fa00e2ba2e165cfd681dd7cd61add6 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Mon, 18 May 2020 21:45:19 +0200 Subject: removed every occurence of check expressions --- .../MultiplicityGoalConstraintCalculator.xtend | 15 +++++++++---- .../patterns/PConstraintTransformer.xtend | 12 +++++----- .../logic2viatra/patterns/PatternProvider.xtend | 12 +++++----- .../patterns/RelationDeclarationIndexer.xtend | 4 ++-- .../logic2viatra/patterns/UnfinishedIndexer.xtend | 12 +++++----- .../rules/GoalConstraintProvider.xtend | 26 ++++++++++++---------- .../rules/RefinementRuleProvider.xtend | 18 +++++++-------- .../dse/BestFirstStrategyForModelGeneration.java | 12 +++++++++- 8 files changed, 67 insertions(+), 44 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend index 6435806d..05ce4f6e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend @@ -10,13 +10,15 @@ class MultiplicityGoalConstraintCalculator { val String targetRelationName; val IQuerySpecification querySpecification; var ViatraQueryMatcher matcher; + val int minValue val boolean containment val int cost - public new(String targetRelationName, IQuerySpecification querySpecification, boolean containment, int cost) { + public new(String targetRelationName, IQuerySpecification querySpecification, int minValue, boolean containment, int cost) { this.targetRelationName = targetRelationName this.querySpecification = querySpecification this.matcher = null + this.minValue = minValue this.containment = containment this.cost = cost } @@ -25,6 +27,7 @@ class MultiplicityGoalConstraintCalculator { this.targetRelationName = other.targetRelationName this.querySpecification = other.querySpecification this.matcher = null + this.minValue = other.minValue this.containment = other.containment this.cost = other.cost } @@ -47,13 +50,17 @@ class MultiplicityGoalConstraintCalculator { val allMatches = this.matcher.allMatches for(match : allMatches) { - val missingMultiplicity = match.get(4) as Integer - res += missingMultiplicity + val existingMultiplicity = match.get(4) as Integer + if(existingMultiplicity < this.minValue) { + val missingMultiplicity = this.minValue-existingMultiplicity + res += missingMultiplicity + } // if(missingMultiplicity!=0) { // println(targetRelationName+ " missing multiplicity: "+missingMultiplicity) // } } - //println(targetRelationName+ " all missing multiplicities: "+res) +// if(res>0) +// println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost) return res*cost } } \ 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/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend index a4dcefbf..dd5cade1 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend @@ -196,7 +196,9 @@ class PConstraintTransformer { def hasValue(PVariable v, String target, Modality m, List variableMapping) { val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference if(m.isMay) { - '''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpressionByRef(typeReference,v,v.valueVariable)» check(!«v.valueSetted»||«v.valueVariable»==«target»));''' + '''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpressionByRef(typeReference,v,v.valueVariable)» +««« check(!«v.valueSetted»||«v.valueVariable»==«target»)); +''' } else { // Must or current '''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpressionByRef(typeReference,v,target)»''' } @@ -233,13 +235,13 @@ class PConstraintTransformer { «FOR variable: e.affectedVariables» PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)» «ENDFOR» - check( - «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR» +««« check( +««« «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR» ««« «IF variable2Type.values.filter(RealTypeReference).empty» ««« || ««« («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)») ««« «ENDIF» - ); +««« ); ''' } else { // Must or Current return ''' @@ -263,7 +265,7 @@ class PConstraintTransformer { «FOR variable: e.affectedVariables» PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)» «ENDFOR» - check(«FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»); +««« check(«FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»); ''' } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index cfea499b..f3de4ccc 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend @@ -27,8 +27,8 @@ import java.util.HashMap @Data class GeneratedPatterns { public Map>> invalidWFQueries public Map>> unfinishedWFQueries - public Map>> unfinishedContainmentMulticiplicityQueries - public Map>> unfinishedNonContainmentMulticiplicityQueries + public Map>,Integer>> unfinishedContainmentMulticiplicityQueries + public Map>,Integer>> unfinishedNonContainmentMulticiplicityQueries public Map>> refineObjectQueries public Map>> refineTypeQueries public Map, IQuerySpecification>> refinerelationQueries @@ -93,11 +93,13 @@ class PatternProvider { val unfinishedNonContainmentMultiplicities = new HashMap for(entry : unfinishedMultiplicities.entrySet) { val relation = entry.key - val value = entry.value.lookup(queries) + val name = entry.value.key + val amount = entry.value.value + val query = name.lookup(queries) if(problem.containmentHierarchies.head.containmentRelations.contains(relation)) { - unfinishedContainmentMultiplicities.put(relation,value) + unfinishedContainmentMultiplicities.put(relation,query->amount) } else { - unfinishedNonContainmentMultiplicities.put(relation,value) + unfinishedNonContainmentMultiplicities.put(relation,query->amount) } } // val Map>> diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend index f384cd50..cef707c5 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend @@ -90,13 +90,13 @@ class RelationDeclarationIndexer { // There are "numberOfExistingReferences" currently existing instances of the reference from the source, // the upper bound of the multiplicity should be considered. numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» - check(numberOfExistingReferences < «upperMultiplicities.get(relation)»); + numberOfExistingReferences != «upperMultiplicities.get(relation)»; «ENDIF» «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» // There are "numberOfExistingReferences" currently existing instances of the reference to the target, // the upper bound of the opposite reference multiplicity should be considered. numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» - check(numberOfExistingOppositeReferences < «upperMultiplicities.get(inverseRelations.get(relation))»); + numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»; «ENDIF» «IF containments.contains(relation)» // The reference is containment, then a new reference cannot be create if: diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend index ad1c9033..1df402fa 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend @@ -46,14 +46,14 @@ class UnfinishedIndexer { val lowerMultiplicities = base.lowerMultiplicities(problem) return ''' «FOR lowerMultiplicity : lowerMultiplicities» - pattern «unfinishedMultiplicityName(lowerMultiplicity)»(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,missingMultiplicity) { + pattern «unfinishedMultiplicityName(lowerMultiplicity)»(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,numberOfExistingReferences) { find interpretation(problem,interpretation); PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«lowerMultiplicity.relation.name»"); «base.typeIndexer.referInstanceOf(lowerMultiplicity.firstParamTypeOfRelation,Modality::MUST,"object")» numberOfExistingReferences == count «base.referRelation(lowerMultiplicity.relation,"object","_",Modality.MUST,fqn2PQuery)» - check(numberOfExistingReferences < «lowerMultiplicity.lower»); - missingMultiplicity == eval(«lowerMultiplicity.lower»-numberOfExistingReferences); +««« numberOfExistingReferences < «lowerMultiplicity.lower»; +««« missingMultiplicity == eval(«lowerMultiplicity.lower»-numberOfExistingReferences); } «ENDFOR» ''' @@ -61,8 +61,8 @@ class UnfinishedIndexer { def String unfinishedMultiplicityName(LowerMultiplicityAssertion lowerMultiplicityAssertion) '''unfinishedLowerMultiplicity_«base.canonizeName(lowerMultiplicityAssertion.relation.name)»''' - def public referUnfinishedMultiplicityQuery(LowerMultiplicityAssertion lowerMultiplicityAssertion) - '''find «unfinishedMultiplicityName(lowerMultiplicityAssertion)»(problem, interpretation ,object, missingMultiplicity);''' + //def public referUnfinishedMultiplicityQuery(LowerMultiplicityAssertion lowerMultiplicityAssertion) + // '''find «unfinishedMultiplicityName(lowerMultiplicityAssertion)»(problem, interpretation ,object, missingMultiplicity);''' def getFirstParamTypeOfRelation(LowerMultiplicityAssertion lowerMultiplicityAssertion) { val parameters = lowerMultiplicityAssertion.relation.parameters @@ -78,7 +78,7 @@ class UnfinishedIndexer { val lowerMultiplicities = base.lowerMultiplicities(problem) val map = new LinkedHashMap for(lowerMultiplicity : lowerMultiplicities) { - map.put(lowerMultiplicity.relation,unfinishedMultiplicityName(lowerMultiplicity)) + map.put(lowerMultiplicity.relation,unfinishedMultiplicityName(lowerMultiplicity)->lowerMultiplicity.lower) } return map } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index 87f7e339..0e8d341a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -19,38 +19,40 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class GoalConstraintProvider { - val calculateObjectCost = true + val calculateObjectCost = false def public getUnfinishedMultiplicityQueries(LogicProblem p, GeneratedPatterns patterns) { val res = new ArrayList() - res.addAll(patterns.unfinishedContainmentMulticiplicityQueries,true) + res.addAll(patterns.unfinishedNonContainmentMulticiplicityQueries,false) if(calculateObjectCost) { - val middingObjectCost = calculateMissingObjectCost(p) - res.addAll(patterns.unfinishedNonContainmentMulticiplicityQueries,false) + val missingObjectCost = calculateMissingObjectCost(p) + res.addAll(patterns.unfinishedContainmentMulticiplicityQueries,true,missingObjectCost) } else { - res.addAll(patterns.unfinishedNonContainmentMulticiplicityQueries,false) + res.addAll(patterns.unfinishedContainmentMulticiplicityQueries,true) } return res } - def addAll(ArrayList res, Map>> queries, boolean containment) { + def addAll(ArrayList res, Map>,Integer>> queries, boolean containment) { for(multiplicityQuery : queries.entrySet) { val targetRelationName = multiplicityQuery.key.name - val query = multiplicityQuery.value - res += new MultiplicityGoalConstraintCalculator(targetRelationName,query,containment,1); + val query = multiplicityQuery.value.key + val minValue = multiplicityQuery.value.value + res += new MultiplicityGoalConstraintCalculator(targetRelationName,query,minValue,containment,1); } } def addAll( ArrayList res, - Map>> queries, + Map>,Integer>> queries, boolean containment, Map cost ) { for(multiplicityQuery : queries.entrySet) { val targetRelationName = multiplicityQuery.key.name - val query = multiplicityQuery.value - res += new MultiplicityGoalConstraintCalculator(targetRelationName,query,containment,multiplicityQuery.key.lookup(cost)) + val query = multiplicityQuery.value.key + val minValue = multiplicityQuery.value.value + res += new MultiplicityGoalConstraintCalculator(targetRelationName,query,minValue,containment,multiplicityQuery.key.lookup(cost)) } } @@ -80,7 +82,7 @@ class GoalConstraintProvider { for(containment : containments) { val key = containment val value = (containment.parameters.get(1) as ComplexTypeReference).referred.count(type2NewCost) - //println('''«key.name» --> «value» new''') +// println('''«key.name» --> «value» new''') res.put(key,value) } return res 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 16438a5a..23ea118b 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 @@ -413,9 +413,6 @@ class RefinementRuleProvider { newElement.name = '''new «interpretation.newElements.size»''' } - // Existence - interpretation.newElements+=newElement - // Types typeInterpretation.elements += newElement if(typeInterpretation instanceof PartialComplexTypeInterpretation) { @@ -431,6 +428,9 @@ class RefinementRuleProvider { // Scope propagation scopePropagator.propagateAdditionToType(typeInterpretation) + // Existence + interpretation.newElements+=newElement + // Do recursive object creation for(newConstructor : recursiceObjectCreations) { createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator) @@ -454,9 +454,6 @@ class RefinementRuleProvider { newElement.name = '''new «interpretation.newElements.size»''' } - // Existence - interpretation.newElements+=newElement - // Types typeInterpretation.elements += newElement if(typeInterpretation instanceof PartialComplexTypeInterpretation) { @@ -469,6 +466,9 @@ class RefinementRuleProvider { // Scope propagation scopePropagator.propagateAdditionToType(typeInterpretation) + // Existence + interpretation.newElements+=newElement + // Do recursive object creation for(newConstructor : recursiceObjectCreations) { createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator) @@ -490,9 +490,6 @@ class RefinementRuleProvider { newElement.name = '''new «interpretation.newElements.size»''' } - // Existence - interpretation.newElements+=newElement - // Types typeInterpretation.elements += newElement if(typeInterpretation instanceof PartialComplexTypeInterpretation) { @@ -502,6 +499,9 @@ class RefinementRuleProvider { // Scope propagation scopePropagator.propagateAdditionToType(typeInterpretation) + // Existence + interpretation.newElements+=newElement + // Do recursive object creation for(newConstructor : recursiceObjectCreations) { createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator) 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 5869889d..8035c947 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 @@ -9,6 +9,9 @@ *******************************************************************************/ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse; +import java.io.BufferedReader; +import java.io.IOException; +import java.io.InputStreamReader; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; @@ -146,6 +149,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { @Override public void explore() { +// System.out.println("press enter"); +// try { +// new BufferedReader(new InputStreamReader(System.in)).readLine(); +// } catch (IOException e) { +// // TODO Auto-generated catch block +// e.printStackTrace(); +// } this.explorationStarted=System.nanoTime(); if (!context.checkGlobalConstraints()) { logger.info("Global contraint is not satisifed in the first state. Terminate."); @@ -308,7 +318,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000; long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000; this.times.add( - "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime+ + "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ "|StateCoderTime:"+statecoderTime+ "|SolutionCopyTime:"+solutionCopy+ "|ActivationSelectionTime:"+activationSelection+ -- cgit v1.2.3-54-g00ecf From fd2fa1e12353b5cf905358d1446d6469ac04be72 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 19 May 2020 22:38:21 +0200 Subject: option to calculate object creation costs in fitness --- .../mit/inf/dslreasoner/application/execution/SolverLoader.xtend | 6 ++++++ .../viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend | 5 +++-- .../viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend | 3 +-- .../mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | 3 ++- .../viatrasolver/reasoner/ViatraReasonerConfiguration.xtend | 2 ++ 5 files changed, 14 insertions(+), 5 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend') 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 e1d01cb5..48d4fbb4 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 @@ -124,6 +124,12 @@ class SolverLoader { c.unfinishedWFWeight = Integer.parseInt(stringValue) } catch(Exception e) {} } + if(config.containsKey("fitness-objectCreationCosts")) { + val stringValue = config.get("fitness-objectCreationCosts") + try { + c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue) + } catch(Exception e) {} + } ] } else { throw new UnsupportedOperationException('''Unknown solver: «solver»''') 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 ca09ae00..b63607f7 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 @@ -59,7 +59,8 @@ class ModelGenerationMethodProvider { boolean nameNewElements, TypeInferenceMethod typeInferenceMethod, ScopePropagator scopePropagator, - DocumentationLevel debugLevel + DocumentationLevel debugLevel, + boolean objectCreationCosts ) { val statistics = new ModelGenerationStatistics val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) @@ -77,7 +78,7 @@ class ModelGenerationMethodProvider { objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, queries,scopePropagator,nameNewElements,statistics) val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics) - val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries) + val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries,objectCreationCosts) val unfinishedWF = queries.getUnfinishedWFQueries.values val invalidWF = queries.getInvalidWFQueries.values diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index 0e8d341a..e03a8c35 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -19,9 +19,8 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class GoalConstraintProvider { - val calculateObjectCost = false - def public getUnfinishedMultiplicityQueries(LogicProblem p, GeneratedPatterns patterns) { + def public getUnfinishedMultiplicityQueries(LogicProblem p, GeneratedPatterns patterns, boolean calculateObjectCost) { val res = new ArrayList() res.addAll(patterns.unfinishedNonContainmentMulticiplicityQueries,false) 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 df3ccee5..0bd8c50e 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 @@ -75,7 +75,8 @@ class ViatraReasoner extends LogicReasoner{ viatraConfig.nameNewElements, viatraConfig.typeInferenceMethod, scopePropagator, - viatraConfig.documentationLevel + viatraConfig.documentationLevel, + viatraConfig.calculateObjectCreationCosts ) //println("parsed") diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index 7369344c..6e3c5235 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend @@ -53,6 +53,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{ public var conaintmentWeight = 2 public var nonContainmentWeight = 1 public var unfinishedWFWeight = 1 + + public var calculateObjectCreationCosts = false } public class DiversityDescriptor { -- cgit v1.2.3-54-g00ecf From 957082776dbb7efed53a783c5e5be6b443a9bb86 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sat, 27 Jun 2020 17:56:46 +0200 Subject: Fix scope + numerical propagation WIP --- .../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes .../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes .../.SolverSemanticHighlightCalculator.xtendbin | Bin 5334 -> 5334 bytes .../.SolverSemanticTextAttributeProvider.xtendbin | Bin 4902 -> 4902 bytes .../validation/.SolverLanguageValidator.xtendbin | Bin 1717 -> 1717 bytes ....SolverLanguageTokenDefInjectingParser.xtendbin | Bin 2742 -> 2742 bytes ...nguageSyntheticTokenSyntacticSequencer.xtendbin | Bin 2758 -> 2758 bytes .../hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath | 6 +- .../.settings/org.eclipse.jdt.core.prefs | 8 ++ .../lib/libviatracbc.so | Bin 33944 -> 46416 bytes .../MultiplicityGoalConstraintCalculator.xtend | 15 +-- .../cardinality/PolyhedronScopePropagator.xtend | 8 +- .../logic2viatra/cardinality/ScopePropagator.xtend | 14 +- .../rules/GoalConstraintProvider.xtend | 3 +- .../rules/RefinementRuleProvider.xtend | 150 ++++++++++++--------- .../PartialInterpretationInitialiser.xtend | 29 ++-- .../reasoner/ViatraReasonerConfiguration.xtend | 5 +- .../dse/BestFirstStrategyForModelGeneration.java | 22 +-- .../dse/ModelGenerationCompositeObjective.xtend | 2 +- .../viatrasolver/reasoner/dse/ScopeObjective.xtend | 2 +- .../case.study.familyTree.run/bin/.gitignore | 1 - .../inputs/SatelliteInstance.xmi | 2 +- .../src/run/RunGeneratorConfig.xtend | 6 +- 23 files changed, 136 insertions(+), 137 deletions(-) create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs delete mode 100644 Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend') diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin index b5a7c99c..94c786eb 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin index 9274eee0..46ab9b95 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin index 8e8e8c70..27dc1dd4 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin index 741776d1..d71f4f21 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin index 73356e7f..801783da 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin index 24f61d80..30c2ff9e 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin index eae3bd77..261f466c 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin differ diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath index e19039ae..93829d26 100644 --- a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath @@ -1,10 +1,6 @@ - - - - - + diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..9f6ece88 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,8 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.release=disabled +org.eclipse.jdt.core.compiler.source=1.8 diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so index 96289216..ba3cdc06 100755 Binary files a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so and b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so differ diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend index 034420d6..b28cd584 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend @@ -10,15 +10,13 @@ class MultiplicityGoalConstraintCalculator { val String targetRelationName val IQuerySpecification querySpecification var ViatraQueryMatcher matcher - val int minValue val boolean containment val int cost - public new(String targetRelationName, IQuerySpecification querySpecification, int minValue, boolean containment, int cost) { + public new(String targetRelationName, IQuerySpecification querySpecification, boolean containment, int cost) { this.targetRelationName = targetRelationName this.querySpecification = querySpecification this.matcher = null - this.minValue = minValue this.containment = containment this.cost = cost } @@ -27,7 +25,6 @@ class MultiplicityGoalConstraintCalculator { this.targetRelationName = other.targetRelationName this.querySpecification = other.querySpecification this.matcher = null - this.minValue = other.minValue this.containment = other.containment this.cost = other.cost } @@ -49,14 +46,8 @@ class MultiplicityGoalConstraintCalculator { var res = 0 val allMatches = this.matcher.allMatches for(match : allMatches) { - val existingMultiplicity = match.get(4) as Integer - if(existingMultiplicity < this.minValue) { - val missingMultiplicity = this.minValue-existingMultiplicity - res += missingMultiplicity - } -// if(missingMultiplicity!=0) { -// println(targetRelationName+ " missing multiplicity: "+missingMultiplicity) -// } + val missingMultiplicity = match.get(2) as Integer + res += missingMultiplicity } // if(res>0) // println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost) diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index 120fb18a..9b4dff0f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend @@ -88,6 +88,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { val result = operator.saturate() if (result == PolyhedronSaturationResult.EMPTY) { cache.put(signature, PolyhedronSignature.EMPTY) +// println("INVALID") setScopesInvalid() } else { val resultSignature = polyhedron.createSignature @@ -110,11 +111,8 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } } - override propagateAdditionToRelation(Relation r) { - super.propagateAdditionToRelation(r) - if (relevantRelations.contains(r)) { - propagateAllScopeConstraints() - } + override isPropagationNeededAfterAdditionToRelation(Relation r) { + relevantRelations.contains(r) || super.isPropagationNeededAfterAdditionToRelation(r) } def resetBounds() { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend index 8f3a5bb0..8350c7f4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend @@ -114,21 +114,21 @@ class ScopePropagator { } } - def void propagateAdditionToRelation(Relation r) { - // Nothing to propagate. + def isPropagationNeededAfterAdditionToRelation(Relation r) { + 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 } if (scope.minNewElementsHeuristic > 0) { scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1 } + if (scope.maxNewElements > 0) { + scope.maxNewElements = scope.maxNewElements - 1 + } else if (scope.maxNewElements === 0) { + setScopesInvalid() + } } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index 238ade5b..d2ee80dc 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -15,9 +15,8 @@ class GoalConstraintProvider { val queries = entry.value val targetRelationName = constraint.relation.name val query = queries.unfinishedMultiplicityQuery - val minValue = constraint.lowerBound val containment = constraint.containment - res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, minValue, containment, 1) + res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, containment, 1) } } return res 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 0b8a9019..863ee18b 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 @@ -32,9 +32,12 @@ import java.util.LinkedHashMap import java.util.LinkedList import java.util.List import java.util.Map +import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine import org.eclipse.viatra.query.runtime.api.GenericPatternMatch import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.emf.EMFScope import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory import org.eclipse.xtend.lib.annotations.Data @@ -45,6 +48,8 @@ class RefinementRuleProvider { val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE + var AdvancedViatraQueryEngine queryEngine + def canonizeName(String name) { return name.replace(' ','_') } @@ -60,6 +65,7 @@ class RefinementRuleProvider { { val res = new LinkedHashMap val recursiveObjectCreation = recursiveObjectCreation(p,i) + queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine for(LHSEntry: patterns.refineObjectQueries.entrySet) { val containmentRelation = LHSEntry.key.containmentRelation val inverseRelation = LHSEntry.key.inverseContainment @@ -90,8 +96,7 @@ class RefinementRuleProvider { if(inverseRelation!== null) { ruleBuilder.action[match | statistics.incrementTransformationCount -// println(name) - val startTime = System.nanoTime +// println(name) //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation @@ -99,79 +104,89 @@ class RefinementRuleProvider { val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation val container = match.get(5) as DefinedElement - createObjectActionWithContainmentAndInverse( - nameNewElement, - interpretation, - typeInterpretation, - container, - relationInterpretation, - inverseRelationInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createObjectActionWithContainmentAndInverse( + nameNewElement, + interpretation, + typeInterpretation, + container, + relationInterpretation, + inverseRelationInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] ] } else { ruleBuilder.action[match | statistics.incrementTransformationCount // println(name) - val startTime = System.nanoTime //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation val container = match.get(4) as DefinedElement - createObjectActionWithContainment( - nameNewElement, - interpretation, - typeInterpretation, - container, - relationInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createObjectActionWithContainment( + nameNewElement, + interpretation, + typeInterpretation, + container, + relationInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] ] } } else { ruleBuilder.action[match | statistics.incrementTransformationCount // println(name) - val startTime = System.nanoTime //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation - createObjectAction( - nameNewElement, - interpretation, - typeInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createObjectAction( + nameNewElement, + interpretation, + typeInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] ] } return ruleBuilder.build @@ -342,7 +357,7 @@ class RefinementRuleProvider { if (inverseRelation === null) { ruleBuilder.action [ match | statistics.incrementTransformationCount - val startTime = System.nanoTime + // println(name) // val problem = match.get(0) as LogicProblem // val interpretation = match.get(1) as PartialInterpretation @@ -350,19 +365,24 @@ class RefinementRuleProvider { val src = match.get(3) as DefinedElement val trg = match.get(4) as DefinedElement - createRelationLinkAction(src, trg, relationInterpretation) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createRelationLinkAction(src, trg, relationInterpretation) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAdditionToRelation(declaration) - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] + } ] } else { ruleBuilder.action [ match | statistics.incrementTransformationCount - val startTime = System.nanoTime // println(name) // val problem = match.get(0) as LogicProblem // val interpretation = match.get(1) as PartialInterpretation @@ -371,14 +391,20 @@ class RefinementRuleProvider { val src = match.get(4) as DefinedElement val trg = match.get(5) as DefinedElement - createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAdditionToRelation(declaration) - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] + } ] } 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 d37acb6d..20ff58f2 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 @@ -2,19 +2,24 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration 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.logic.model.patterns.SupertypeStar 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.BooleanElement 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.PartialBooleanInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation @@ -22,10 +27,10 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory 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.Map @@ -35,14 +40,6 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope 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.SymbolicValue -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And -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 -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition @Data class Problem2PartialInterpretationTrace { Map type2Interpretation @@ -194,7 +191,7 @@ class PartialInterpretationInitialiser { interpretation.minNewElements = minNewElements interpretation.maxNewElements = maxNewElements // elements from problem are included - if(maxNewElements>0) { + if(maxNewElements != 0) { val newElements = createDefinedElement => [it.name = "New Objects"] interpretation.openWorldElements += newElements } @@ -213,12 +210,8 @@ class PartialInterpretationInitialiser { 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 - } + res.minNewElements = min ?: 0 + res.maxNewElements = max ?: -1 return res } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index ddd25aac..e33a2590 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend @@ -58,13 +58,14 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { public var runIntermediateNumericalConsistencyChecks = true public var punishSize = true - public var scopeWeight = 1 - public var conaintmentWeight = 2 + public var scopeWeight = 2 + public var conaintmentWeight = 1 public var nonContainmentWeight = 1 public var unfinishedWFWeight = 1 public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) +// public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.BasicTypeHierarchy public var List hints = newArrayList 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 e529892c..09575384 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 @@ -18,6 +18,7 @@ import java.util.List; import java.util.PriorityQueue; import java.util.Random; +import org.apache.log4j.Level; import org.apache.log4j.Logger; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.util.EcoreUtil; @@ -76,7 +77,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { private volatile boolean isInterrupted = false; private ModelResult modelResultByInternalSolver = null; private Random random = new Random(); - //private Collection> matchers; +// private Collection> matchers; public ActivationSelector activationSelector = new EvenActivationSelector(random); public ViatraReasonerSolutionSaver solutionSaver; public NumericSolver numericSolver; @@ -100,7 +101,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { this.method = method; this.solutionSaver = solutionSaver; this.numericSolver = numericSolver; - //logger.setLevel(Level.DEBUG); +// logger.setLevel(Level.DEBUG); } public int getNumberOfStatecoderFail() { @@ -136,7 +137,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // ViatraQueryEngine engine = context.getQueryEngine(); // matchers = new LinkedList>(); // for(IQuerySpecification> p : this.method.getAllPatterns()) { -// //System.out.println(p.getSimpleName()); // ViatraQueryMatcher matcher = p.getMatcher(engine); // matchers.add(matcher); // } @@ -154,13 +154,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { @Override public void explore() { -// System.out.println("press enter"); -// try { -// new BufferedReader(new InputStreamReader(System.in)).readLine(); -// } catch (IOException e) { -// // TODO Auto-generated catch block -// e.printStackTrace(); -// } this.explorationStarted=System.nanoTime(); if (!checkGlobalConstraints()) { logger.info("Global contraint is not satisifed in the first state. Terminate."); @@ -219,10 +212,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { while (!isInterrupted && !configuration.progressMonitor.isCancelled() && iterator.hasNext()) { final Object nextActivation = iterator.next(); -// if (!iterator.hasNext()) { -// logger.debug("Last untraversed activation of the state."); -// trajectoiresToExplore.remove(currentTrajectoryWithfitness); -// } logger.debug("Executing new activation: " + nextActivation); context.executeAcitvationId(nextActivation); method.getStatistics().incrementDecisionCount(); @@ -230,10 +219,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { visualiseCurrentState(); // for(ViatraQueryMatcher matcher : matchers) { // int c = matcher.countMatches(); -// if(c>=100) { +// if(c>=1) { // System.out.println(c+ " " +matcher.getPatternName()); -// } -// +// } // } boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness); 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 d2faaa65..481f4ce1 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 @@ -112,7 +112,7 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective { override isHardObjective() { true } - override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } + override satisifiesHardObjective(Double fitness) { fitness <= 0.9 } override setComparator(Comparator comparator) { throw new UnsupportedOperationException("Model generation objective comparator cannot be set.") 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 69a734f8..7abc5cb8 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 @@ -25,7 +25,7 @@ class ScopeObjective implements IObjective{ val interpretation = context.model as PartialInterpretation var res = interpretation.minNewElementsHeuristic.doubleValue for(scope : interpretation.scopes) { - res += scope.minNewElementsHeuristic*2 + res += scope.minNewElementsHeuristic } return res } diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore deleted file mode 100644 index 7050a7e3..00000000 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/queries/ diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi index 3d07a199..66512878 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi @@ -4,4 +4,4 @@ xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:satellite="http://www.example.org/satellite" - xsi:schemaLocation="http://www.example.org/satellite ../model/satellite.ecore"/> + xsi:schemaLocation="http://www.example.org/satellite ../../hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"/> diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend index 20eed2e2..e4d6fe9f 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend @@ -12,7 +12,9 @@ import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.RuntimeEn import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ScopeSpecification import hu.bme.mit.inf.dslreasoner.application.execution.ScriptExecutor import hu.bme.mit.inf.dslreasoner.application.execution.StandaloneScriptExecutor +import hu.bme.mit.inf.dslreasoner.application.execution.StandardOutputBasedScriptConsole import java.io.File +import java.io.PrintWriter import java.text.SimpleDateFormat import java.util.Date import org.apache.commons.cli.BasicParser @@ -23,8 +25,6 @@ import org.apache.commons.cli.Option import org.apache.commons.cli.Options import org.apache.commons.cli.ParseException import org.eclipse.core.runtime.NullProgressMonitor -import com.google.common.io.Files -import java.io.PrintWriter class RunGeneratorConfig { static var SIZE_LB = 20 @@ -102,7 +102,7 @@ class RunGeneratorConfig { val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm") val formattedDate = format.format(date) - val executor = new ScriptExecutor + val executor = new ScriptExecutor(StandardOutputBasedScriptConsole.FACTORY) val path = "config//generic" + DOMAIN + ".vsconfig" var ConfigurationScript config = StandaloneScriptExecutor.loadScript(path) -- cgit v1.2.3-54-g00ecf From 07ae9155ce0ab9407566b075356f9b7220ee8380 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sun, 28 Jun 2020 20:33:48 +0200 Subject: Fix scope + numerical solver interaction --- .../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes .../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes .../.SolverSemanticHighlightCalculator.xtendbin | Bin 5334 -> 5334 bytes .../.SolverSemanticTextAttributeProvider.xtendbin | Bin 4902 -> 4902 bytes .../validation/.SolverLanguageValidator.xtendbin | Bin 1717 -> 1717 bytes ....SolverLanguageTokenDefInjectingParser.xtendbin | Bin 2742 -> 2742 bytes ...nguageSyntheticTokenSyntacticSequencer.xtendbin | Bin 2758 -> 2758 bytes .../ModelGenerationMethodProvider.xtend | 6 + .../MultiplicityGoalConstraintCalculator.xtend | 22 +- .../cardinality/PolyhedronScopePropagator.xtend | 133 +- .../cardinality/RelationConstraintCalculator.xtend | 33 +- .../RemainingMultiplicityCalculator.xtend | 111 + .../logic2viatra/cardinality/ScopePropagator.xtend | 5 + .../logic2viatra/patterns/PatternProvider.xtend | 11 +- .../logic2viatra/patterns/UnfinishedIndexer.xtend | 189 +- .../rules/GoalConstraintProvider.xtend | 5 +- .../viatrasolver/reasoner/ViatraReasoner.xtend | 2 +- .../model/TaxationWithRoot.aird | 10302 +++++++++---------- 18 files changed, 5436 insertions(+), 5383 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend') diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin index 94c786eb..11aee788 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin index 46ab9b95..d0ad3ab3 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin index 27dc1dd4..173a7c4d 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin index d71f4f21..ad60e239 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin index 801783da..01242ec7 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin index 30c2ff9e..1bdcce7f 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin index 261f466c..2c9fbbb2 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin differ 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 6fbbc779..78eda150 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 @@ -24,9 +24,12 @@ import java.util.Collection import java.util.List import java.util.Map import java.util.Set +import org.eclipse.viatra.query.runtime.api.GenericQueryGroup import org.eclipse.viatra.query.runtime.api.IPatternMatch import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.emf.EMFScope import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule @@ -122,6 +125,9 @@ class ModelGenerationMethodProvider { val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) + val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) + GenericQueryGroup.of(queries.allQueries).prepare(queryEngine) + val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) scopePropagator.propagateAllScopeConstraints val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend index b28cd584..392ab3ee 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend @@ -3,29 +3,31 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality import org.eclipse.emf.common.notify.Notifier import org.eclipse.viatra.query.runtime.api.IQuerySpecification import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine -import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher import org.eclipse.viatra.query.runtime.emf.EMFScope class MultiplicityGoalConstraintCalculator { val String targetRelationName val IQuerySpecification querySpecification - var ViatraQueryMatcher matcher + var MultiplicityCalculator calculator val boolean containment + val int lowerBound val int cost - public new(String targetRelationName, IQuerySpecification querySpecification, boolean containment, int cost) { + new(String targetRelationName, IQuerySpecification querySpecification, boolean containment, int lowerBound, int cost) { this.targetRelationName = targetRelationName this.querySpecification = querySpecification - this.matcher = null + this.calculator = null this.containment = containment + this.lowerBound = lowerBound this.cost = cost } new(MultiplicityGoalConstraintCalculator other) { this.targetRelationName = other.targetRelationName this.querySpecification = other.querySpecification - this.matcher = null + this.calculator = null this.containment = other.containment + this.lowerBound = other.lowerBound this.cost = other.cost } @@ -39,16 +41,12 @@ class MultiplicityGoalConstraintCalculator { def init(Notifier notifier) { val engine = ViatraQueryEngine.on(new EMFScope(notifier)) - matcher = querySpecification.getMatcher(engine) + val matcher = querySpecification.getMatcher(engine) + calculator = RemainingMultiplicityCalculator.of(matcher, lowerBound) } def calculateValue() { - var res = 0 - val allMatches = this.matcher.allMatches - for(match : allMatches) { - val missingMultiplicity = match.get(2) as Integer - res += missingMultiplicity - } + val res = calculator.multiplicity // if(res>0) // println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost) return res*cost diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index 9b4dff0f..db22b95c 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend @@ -33,7 +33,7 @@ import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { static val CACHE_SIZE = 10000 - + val boolean updateHeuristic val Map scopeBounds val LinearBoundedExpression topLevelBounds @@ -185,22 +185,6 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { if (bounds.upperBound !== null && bounds.upperBound < 0) { throw new IllegalArgumentException("Negative upper bound: " + bounds) } - } - - private static def getCalculatedMultiplicity(ViatraQueryMatcher matcher, - PartialInterpretation p) { - val match = matcher.newEmptyMatch - match.set(0, p.problem) - match.set(1, p) - val iterator = matcher.streamAllMatches(match).iterator - if (!iterator.hasNext) { - return null - } - val value = iterator.next.get(2) as Integer - if (iterator.hasNext) { - throw new IllegalArgumentException("Multiplicity calculation query has more than one match") - } - value } @FinalFieldsConstructor @@ -243,7 +227,12 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { IQuerySpecification> hasElementInContainmentQuery, Map>> allPatternsByName, Collection hints, int maximumNuberOfNewNodes) { - infinity = maximumNuberOfNewNodes * INFINITY_SCALE + infinity = if (maximumNuberOfNewNodes <= Integer.MAX_VALUE / INFINITY_SCALE) { + maximumNuberOfNewNodes * INFINITY_SCALE + } else { + Integer.MAX_VALUE + } + queryEngine = ViatraQueryEngine.on(new EMFScope(p)) this.allPatternsByName = allPatternsByName updatersBuilder = ImmutableList.builder @@ -254,7 +243,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { buildConstainmentRootConstraints(containmentConstraints.keySet, hasElementInContainmentQuery) for (pair : constraints.entrySet) { val constraint = pair.key - if (!constraint.containment) { + if (!constraint.containment && !constraint.container) { buildNonContainmentConstraints(constraint, pair.value) } } @@ -289,8 +278,8 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { val typeCoefficients = subtypeDimensions.get(containedType) val orphansLowerBoundCoefficients = new HashMap(typeCoefficients) val orphansUpperBoundCoefficients = new HashMap(typeCoefficients) - val unfinishedMultiplicitiesMatchersBuilder = ImmutableList.builder - val remainingContentsQueriesBuilder = ImmutableList.builder + val unfinishedMultiplicitiesBuilder = ImmutableList.builder + val remainingContentsBuilder = ImmutableList.builder for (pair : constraints) { val constraint = pair.key val containerCoefficients = subtypeDimensions.get(constraint.sourceType) @@ -301,23 +290,21 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } orphansUpperBoundCoefficients.addCoefficients(-constraint.lowerBound, containerCoefficients) val queries = pair.value - if (constraint.constrainsUnfinished) { - if (queries.unfinishedMultiplicityQuery === null) { - throw new IllegalArgumentException( - "Containment constraints need unfinished multiplicity queries") + if (queries.existingMultiplicityQuery !== null) { + val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine) + if (constraint.constrainsUnfinished) { + unfinishedMultiplicitiesBuilder.add( + RemainingMultiplicityCalculator.of(matcher, constraint.lowerBound)) } - unfinishedMultiplicitiesMatchersBuilder.add( - queries.unfinishedMultiplicityQuery.getMatcher(queryEngine)) - } - if (queries.remainingContentsQuery === null) { - throw new IllegalArgumentException("Containment constraints need remaining contents queries") + remainingContentsBuilder.add(RemainingMultiplicityCalculator.of(matcher, constraint.upperBound)) + } else if (constraint.constrainsUnfinished) { + throw new IllegalArgumentException("Containment constraints need multiplicity queries") } - remainingContentsQueriesBuilder.add(queries.remainingContentsQuery.getMatcher(queryEngine)) } val orphanLowerBound = orphansLowerBoundCoefficients.toExpression val orphanUpperBound = orphansUpperBoundCoefficients.toExpression - val updater = new ContainmentConstraintUpdater(containedType.name, orphanLowerBound, orphanUpperBound, - unfinishedMultiplicitiesMatchersBuilder.build, remainingContentsQueriesBuilder.build) + val updater = new ContainmentConstraintUpdater(orphanLowerBound, orphanUpperBound, + unfinishedMultiplicitiesBuilder.build, remainingContentsBuilder.build) updatersBuilder.add(updater) } @@ -336,17 +323,21 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, UnifinishedMultiplicityQueries queries) { + if (!constraint.reference) { + return + } if (constraint.constrainsRemainingInverse) { - if (queries.unfinishedMultiplicityQuery === null) { - throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries") - } - val unfinishedMultiplicityMatcher = queries.unfinishedMultiplicityQuery.getMatcher(queryEngine) - if (queries.remainingInverseMultiplicityQuery === null) { - throw new IllegalArgumentException( - "Reference constraints need remaining inverse multiplicity queries") + if (queries.getExistingMultiplicityQuery === null) { + throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries: " + + constraint.relation) } - val remainingInverseMultiplicityMatcher = queries.remainingInverseMultiplicityQuery.getMatcher( + val existingMultiplicityMatcher = queries.getExistingMultiplicityQuery.getMatcher(queryEngine) + val unfinishedMultiplicityCalculator = RemainingMultiplicityCalculator.of(existingMultiplicityMatcher, + constraint.lowerBound) + val existingInverseMultiplicityMatcher = queries.existingInverseMultiplicityQuery.getMatcher( queryEngine) + val remainingInverseMultiplicityCalculator = new RemainingInverseMultiplicityCalculator( + existingInverseMultiplicityMatcher, constraint.upperBound) val availableMultiplicityCoefficients = new HashMap availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, subtypeDimensions.get(constraint.targetType)) @@ -354,18 +345,18 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { subtypeDimensions.get(constraint.targetType)) val availableMultiplicity = availableMultiplicityCoefficients.toExpression updatersBuilder.add( - new UnfinishedMultiplicityConstraintUpdater(constraint.relation.name, availableMultiplicity, - unfinishedMultiplicityMatcher, remainingInverseMultiplicityMatcher)) + new UnfinishedMultiplicityConstraintUpdater(availableMultiplicity, unfinishedMultiplicityCalculator, + remainingInverseMultiplicityCalculator)) } if (constraint.constrainsUnrepairable) { - if (queries.unrepairableMultiplicityQuery === null) { - throw new IllegalArgumentException("Reference constraints need unrepairable multiplicity queries") + if (queries.existingMultiplicityQuery.parameters.size < 5) { + throw new IllegalArgumentException("Reference constraints need repairable multiplicity queries: " + + constraint.relation) } - val unrepairableMultiplicityMatcher = queries.unrepairableMultiplicityQuery.getMatcher(queryEngine) + val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine) + val calculator = new UnrepairableMultiplicityCalculator(matcher, constraint.lowerBound) val targetTypeCardinality = typeBounds.get(constraint.targetType) - updatersBuilder.add( - new UnrepairableMultiplicityConstraintUpdater(constraint.relation.name, targetTypeCardinality, - unrepairableMultiplicityMatcher)) + updatersBuilder.add(new UnrepairableMultiplicityConstraintUpdater(targetTypeCardinality, calculator)) } } @@ -470,11 +461,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { @FinalFieldsConstructor private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { - val String name val LinearBoundedExpression orphansLowerBound val LinearBoundedExpression orphansUpperBound - val List> unfinishedMultiplicitiesMatchers - val List> remainingContentsQueries + val List> unfinishedMultiplicities + val List> remainingContents override update(PartialInterpretation p) { tightenLowerBound(p) @@ -483,12 +473,9 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { private def tightenLowerBound(PartialInterpretation p) { var int sum = 0 - for (matcher : remainingContentsQueries) { - val value = matcher.getCalculatedMultiplicity(p) - if (value === null) { - throw new IllegalArgumentException("Remaining contents count is missing for " + name) - } - if (value == -1) { + for (calculator : remainingContents) { + val value = calculator.getMultiplicity(p) + if (value < 0) { // Infinite upper bound, no need to tighten. return } @@ -499,11 +486,8 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { private def tightenUpperBound(PartialInterpretation p) { var int sum = 0 - for (matcher : unfinishedMultiplicitiesMatchers) { - val value = matcher.getCalculatedMultiplicity(p) - if (value === null) { - throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) - } + for (calculator : unfinishedMultiplicities) { + val value = calculator.getMultiplicity(p) sum += value } orphansUpperBound.tightenLowerBound(sum) @@ -531,20 +515,13 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { @FinalFieldsConstructor private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { - val String name val LinearBoundedExpression availableMultiplicityExpression - val ViatraQueryMatcher unfinishedMultiplicityMatcher - val ViatraQueryMatcher remainingInverseMultiplicityMatcher + val MultiplicityCalculator unfinishedMultiplicityCalculator + val MultiplicityCalculator remainingInverseMultiplcityCalculator override update(PartialInterpretation p) { - val unfinishedMultiplicity = unfinishedMultiplicityMatcher.getCalculatedMultiplicity(p) - if (unfinishedMultiplicity === null) { - throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) - } - val remainingInverseMultiplicity = remainingInverseMultiplicityMatcher.getCalculatedMultiplicity(p) - if (remainingInverseMultiplicity === null) { - throw new IllegalArgumentException("Remaining inverse multiplicity is missing for " + name) - } + val unfinishedMultiplicity = unfinishedMultiplicityCalculator.getMultiplicity(p) + val remainingInverseMultiplicity = remainingInverseMultiplcityCalculator.getMultiplicity(p) val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) } @@ -552,15 +529,11 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { @FinalFieldsConstructor private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { - val String name val LinearBoundedExpression targetCardinalityExpression - val ViatraQueryMatcher unrepairableMultiplicityMatcher + val MultiplicityCalculator calculator override update(PartialInterpretation p) { - val value = unrepairableMultiplicityMatcher.getCalculatedMultiplicity(p) - if (value === null) { - throw new IllegalArgumentException("Unrepairable multiplicity is missing for " + name) - } + val value = calculator.getMultiplicity(p) targetCardinalityExpression.tightenLowerBound(value) } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend index 3e4fea8a..7fec452f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend @@ -46,11 +46,11 @@ class RelationMultiplicityConstraint { def constrainsUnrepairable() { // TODO Optimize the unrepairable matches computation, // or come up with a heuristic when does computing unrepairables worth the overhead. - constrainsUnfinished && canHaveMultipleSourcesPerTarget && false + constrainsUnfinished && canHaveMultipleSourcesPerTarget && reference } def constrainsRemainingInverse() { - lowerBound >= 1 && !containment && inverseUpperBoundFinite + lowerBound >= 1 && !containment && !container && inverseUpperBoundFinite && reference } def constrainsRemainingContents() { @@ -61,6 +61,18 @@ class RelationMultiplicityConstraint { constrainsUnfinished || constrainsUnrepairable || constrainsRemainingInverse || constrainsRemainingContents } + def isSourceTypeComplex() { + getParamTypeReference(0) instanceof ComplexTypeReference + } + + def isTargetTypeComplex() { + getParamTypeReference(1) instanceof ComplexTypeReference + } + + def isReference() { + sourceTypeComplex && targetTypeComplex + } + def getSourceType() { getParamType(0) } @@ -69,15 +81,20 @@ class RelationMultiplicityConstraint { getParamType(1) } - private def getParamType(int i) { + private def getParamTypeReference(int i) { val parameters = relation.parameters if (i < parameters.size) { - val firstParam = parameters.get(i) - if (firstParam instanceof ComplexTypeReference) { - return firstParam.referred - } + return parameters.get(i) + } + throw new IllegalArgumentException("Argument index out of range") + } + + private def getParamType(int i) { + val reference = getParamTypeReference(i) + if (reference instanceof ComplexTypeReference) { + return reference.referred } - throw new IllegalArgumentException("Constraint with unknown source type") + throw new IllegalArgumentException("Constraint with primitive type") } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend new file mode 100644 index 00000000..48b52d28 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend @@ -0,0 +1,111 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import java.util.Iterator +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +@FinalFieldsConstructor +abstract class MultiplicityCalculator { + val ViatraQueryMatcher matcher + + def getMultiplicity() { + val iterator = matcher.streamAllMatches.iterator + getMultiplicity(iterator) + } + + def getMultiplicity(PartialInterpretation interpretation) { + val partialMatch = matcher.newEmptyMatch + partialMatch.set(0, interpretation.problem) + partialMatch.set(1, interpretation) + val iterator = matcher.streamAllMatches(partialMatch).iterator + getMultiplicity(iterator) + } + + protected def int getMultiplicity(Iterator iterator) +} + +class RemainingMultiplicityCalculator extends MultiplicityCalculator { + val int bound + + @FinalFieldsConstructor + private new() { + } + + protected override getMultiplicity(Iterator iterator) { + var res = 0 + while (iterator.hasNext) { + val match = iterator.next + val existingMultiplicity = match.get(3) as Integer + if (existingMultiplicity < bound) { + res += bound - existingMultiplicity + } + } + res + } + + static def of(ViatraQueryMatcher matcher, int bound) { + if (bound < 0) { + new RemainingInfiniteMultiplicityCalculator(matcher) + } else { + new RemainingMultiplicityCalculator(matcher, bound) + } + } +} + +package class RemainingInfiniteMultiplicityCalculator extends MultiplicityCalculator { + + @FinalFieldsConstructor + package new() { + } + + protected override getMultiplicity(Iterator iterator) { + if (iterator.hasNext) { + -1 + } else { + 0 + } + } +} + +@FinalFieldsConstructor +class UnrepairableMultiplicityCalculator extends MultiplicityCalculator { + val int lowerBound + + override protected getMultiplicity(Iterator iterator) { + var res = 0 + while (iterator.hasNext) { + val match = iterator.next + val existingMultiplicity = match.get(3) as Integer + if (existingMultiplicity < lowerBound) { + val missingMultiplcity = lowerBound - existingMultiplicity + val numerOfRepairMatches = match.get(4) as Integer + val unrepairableMultiplicty = missingMultiplcity - numerOfRepairMatches + if (unrepairableMultiplicty > res) { + res = unrepairableMultiplicty + } + } + } + res + } +} + +@FinalFieldsConstructor +class RemainingInverseMultiplicityCalculator extends MultiplicityCalculator { + val int upperBound + + override protected getMultiplicity(Iterator iterator) { + var res = 0 + while (iterator.hasNext) { + val match = iterator.next + val existingMultiplicity = match.get(3) as Integer + if (existingMultiplicity < upperBound) { + val availableMultiplicity = upperBound - existingMultiplicity + val numberOfRepairMatches = match.get(4) as Integer + res += Math.min(availableMultiplicity, numberOfRepairMatches) + } + } + res + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend index 8350c7f4..132ca8e8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend @@ -4,6 +4,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope import java.util.HashMap @@ -80,6 +81,10 @@ class ScopePropagator { } def decrementTypeScope(PartialTypeInterpratation t) { + val isPrimitive = t instanceof PartialPrimitiveInterpretation || t === null + if (isPrimitive) { + return + } // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') val targetScope = type2Scope.get(t) if (targetScope !== null) { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index ac4a0855..2f7c9e2d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend @@ -53,10 +53,8 @@ class ModalPatternQueries { @Data class UnifinishedMultiplicityQueries { - val IQuerySpecification> unfinishedMultiplicityQuery - val IQuerySpecification> unrepairableMultiplicityQuery - val IQuerySpecification> remainingInverseMultiplicityQuery - val IQuerySpecification> remainingContentsQuery + val IQuerySpecification> existingMultiplicityQuery + val IQuerySpecification> existingInverseMultiplicityQuery } class PatternProvider { @@ -108,9 +106,8 @@ class PatternProvider { val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints) val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ - new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries), - unrepairableMultiplicityQueryName?.lookup(queries), - remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries)) + new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries), + existingInverseMultiplicityQueryName?.lookup(queries)) ] val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( queries) diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend index a8a07756..65ad3d48 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend @@ -14,10 +14,8 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* @Data class UnifinishedMultiplicityQueryNames { - val String unfinishedMultiplicityQueryName - val String unrepairableMultiplicityQueryName - val String remainingInverseMultiplicityQueryName - val String remainingContentsQueryName + val String existingMultiplicityQueryName + val String existingInverseMultiplicityQueryName } class UnfinishedIndexer { @@ -58,147 +56,94 @@ class UnfinishedIndexer { def generateUnfinishedMultiplicityQueries(List constraints, Map fqn2PQuery) ''' «FOR constraint : constraints» - «IF constraint.constrainsUnfinished» - private pattern «unfinishedMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, missingMultiplicity:java Integer) { + «IF constraint.shouldIndexExistingMultiplicites(indexUpperMultiplicities)» + private pattern «existingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, numberOfExistingReferences:java Integer«IF constraint.shouldIndexRepairMultiplcities(indexUpperMultiplicities)», numberOfRepairMatches: java Integer«ENDIF») { find interpretation(problem,interpretation); find mustExist(problem,interpretation,object); «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» - check(numberOfExistingReferences < «constraint.lowerBound»); - missingMultiplicity == eval(«constraint.lowerBound»-numberOfExistingReferences); - } - - pattern «unfinishedMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, missingMultiplicity:java Integer) { - find interpretation(problem,interpretation); - missingMultiplicity == sum find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); + «IF constraint.shouldIndexRepairMultiplcities(indexUpperMultiplicities)» + numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); + «ENDIF» } «ENDIF» - «IF indexUpperMultiplicities» - «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse» - private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { - «IF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration» - «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")» - «ELSE» - «IF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration» - «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")» - «ELSE» - find interpretation(problem,interpretation); - find mustExist(problem,interpretation,source); - «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» - find mustExist(problem,interpretation,target); - «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» - neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» - «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» - «ENDIF» - «ENDIF» - } - «ENDIF» - - «IF constraint.constrainsUnrepairable» - private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { - find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); - numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); - check(numberOfRepairMatches < missingMultiplicity); - unrepairableMultiplicity == eval(missingMultiplicity-numberOfRepairMatches); - } - - private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) { - find interpretation(problem,interpretation); - unrepairableMultiplicity == max find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); - } or { - find interpretation(problem,interpretation); - neg find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, _); - unrepairableMultiplicity == 0; - } - «ENDIF» - - «IF constraint.constrainsRemainingInverse» - private pattern «remainingMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) { - find interpretation(problem,interpretation); - find mustExist(problem,interpretation,object); - «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» - numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» - check(numberOfExistingReferences < «constraint.inverseUpperBound»); - numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object); - remainingMultiplicity == eval(Math.min(«constraint.inverseUpperBound»-numberOfExistingReferences, numberOfRepairMatches)); - } - - pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { - find interpretation(problem,interpretation); - remainingMultiplicity == sum find «remainingMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); - } - «ENDIF» - - «IF constraint.constrainsRemainingContents» - «IF constraint.upperBoundFinite» - private pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) { - find interpretation(problem,interpretation); - find mustExist(problem,interpretation,object); - «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» - numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» - check(numberOfExistingReferences < «constraint.upperBound»); - remainingMultiplicity == eval(«constraint.upperBound»-numberOfExistingReferences); - } - - pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { - find interpretation(problem,interpretation); - remainingMultiplicity == sum find «remainingContentsName(constraint)»_helper(problem, interpretation, _, #_); - } + «IF constraint.shouldIndexRepairMatches(indexUpperMultiplicities)» + private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { + «IF constraint.containment || constraint.container» + «repairMatchFallback(constraint, fqn2PQuery)» + «ELSEIF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration» + «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")» + «ELSEIF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration» + «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")» «ELSE» - pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation) { - find interpretation(problem,interpretation); - find mustExist(problem,interpretation,object); - «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» - } - - pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { - find interpretation(problem,interpretation); - find «remainingContentsName(constraint)»_helper(problem, interpretation); - remainingMultiplicity == -1; - } or { - find interpretation(problem,interpretation); - neg find «remainingContentsName(constraint)»_helper(problem, interpretation); - remainingMultiplicity == 0; - } + «repairMatchFallback(constraint, fqn2PQuery)» «ENDIF» - «ENDIF» + } + «ENDIF» + + «IF constraint.shouldIndexInverseMultiplicites(indexUpperMultiplicities)» + private pattern «existingInverseMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, numberOfExistingReferences:java Integer, numberOfRepairMatches: java Integer) { + find interpretation(problem,interpretation); + find mustExist(problem,interpretation,object); + «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» + numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» + numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object); + } «ENDIF» «ENDFOR» ''' - def String unfinishedMultiplicityName( - RelationMultiplicityConstraint constraint) '''unfinishedLowerMultiplicity_«base.canonizeName(constraint.relation.name)»''' + private def repairMatchFallback(RelationMultiplicityConstraint constraint, Map fqn2PQuery) ''' + find interpretation(problem,interpretation); + find mustExist(problem,interpretation,source); + «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» + find mustExist(problem,interpretation,target); + «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» + neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» + «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» + ''' + + def String existingMultiplicityName( + RelationMultiplicityConstraint constraint) '''existingMultiplicity_«base.canonizeName(constraint.relation.name)»''' - def String unrepairableMultiplicityName( - RelationMultiplicityConstraint constraint) '''unrepairableLowerMultiplicity_«base.canonizeName(constraint.relation.name)»''' + def String existingInverseMultiplicityName( + RelationMultiplicityConstraint constraint) '''existingInverseMultiplicity_«base.canonizeName(constraint.relation.name)»''' private def String repairMatchName( RelationMultiplicityConstraint constraint) '''repair_«base.canonizeName(constraint.relation.name)»''' - def String remainingMultiplicityName( - RelationMultiplicityConstraint constraint) '''remainingInverseUpperMultiplicity_«base.canonizeName(constraint.relation.name)»''' - - def String remainingContentsName( - RelationMultiplicityConstraint constraint) '''remainingContents_«base.canonizeName(constraint.relation.name)»''' - def getUnfinishedMultiplicityQueries(List constraints) { constraints.toInvertedMap [ constraint | new UnifinishedMultiplicityQueryNames( - if(constraint.constrainsUnfinished) unfinishedMultiplicityName(constraint) else null, - if (indexUpperMultiplicities && constraint.constrainsUnrepairable) - unrepairableMultiplicityName(constraint) - else - null, - if (indexUpperMultiplicities && constraint.constrainsRemainingInverse) - remainingMultiplicityName(constraint) - else - null, - if (indexUpperMultiplicities && constraint.constrainsRemainingContents) - remainingContentsName(constraint) - else + if (constraint.shouldIndexExistingMultiplicites(indexUpperMultiplicities)) { + existingMultiplicityName(constraint) + } else { + null + }, + if (constraint.shouldIndexInverseMultiplicites(indexUpperMultiplicities)) { + existingInverseMultiplicityName(constraint) + } else { null + } ) ] } + + static def shouldIndexExistingMultiplicites(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { + constrainsUnfinished || (indexUpperMultiplicities && constrainsRemainingContents) + } + + static def shouldIndexRepairMultiplcities(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { + shouldIndexExistingMultiplicites(indexUpperMultiplicities) && constrainsUnrepairable + } + + static def shouldIndexInverseMultiplicites(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { + indexUpperMultiplicities && constrainsRemainingInverse + } + + static def shouldIndexRepairMatches(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { + shouldIndexRepairMultiplcities(indexUpperMultiplicities) || + shouldIndexInverseMultiplicites(indexUpperMultiplicities) + } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index d2ee80dc..7dc21410 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -14,9 +14,10 @@ class GoalConstraintProvider { if (constraint.constrainsUnfinished) { val queries = entry.value val targetRelationName = constraint.relation.name - val query = queries.unfinishedMultiplicityQuery + val query = queries.existingMultiplicityQuery val containment = constraint.containment - res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, containment, 1) + val lowerBound = constraint.lowerBound + res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, containment, 1, lowerBound) } } return res 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 3033eca7..b9056685 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 @@ -26,6 +26,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericSolver import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint @@ -42,7 +43,6 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel import org.eclipse.viatra.dse.solutionstore.SolutionStore import org.eclipse.viatra.dse.statecode.IStateCoderFactory -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericSolver class ViatraReasoner extends LogicReasoner { val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.model/model/TaxationWithRoot.aird b/Tests/MODELS2020-CaseStudies/case.study.pledge.model/model/TaxationWithRoot.aird index e5bce79e..a4252796 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.model/model/TaxationWithRoot.aird +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.model/model/TaxationWithRoot.aird @@ -1,5151 +1,5151 @@ - - - - TaxationWithRoot.ecore - TaxationWithRoot.genmodel - platform:/plugin/org.eclipse.emf.ecore/model/Ecore.ecore - - - - - - - - - - - - - - - - - - - - - - - bold - - - - - - - bold - - - - - - - - - - bold - - - - - - - - - - bold - - - - bold - - - - - - - bold - - - - bold - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - italic - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - - italic - - - - - - - - - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - - - - - - - - - bold - - - - - - - - bold - - - - - - - - - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - - italic - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - italic - - - - - - - - - - - - - - - - bold - - - - - - - - bold - - - - - - - - - italic - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - - italic - - - - - - - - bold - - - - - - - - - - - - - - - - - - - - - - - - bold - - - - - - - - bold - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - bold - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - bold - - - - - - - - bold - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - KEEP_LOCATION - KEEP_SIZE - KEEP_RATIO - - - - - - - - - - - labelSize - bold - - - labelSize - - - - - - - - - - labelSize - bold - - - labelSize - - - - - - - - - - labelSize - bold - - - labelSize - - - - - - - - - - labelSize - bold - - - labelSize - - - - - - - - - - - labelSize - - - labelSize - - - - - - - - - - - labelSize - - - labelSize - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - italic - - - - - - - - - - - - bold - - - bold - - - - - - - - - - - bold - - - bold - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - bold - - - bold - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - bold - - - bold - - - - - - - - - - - bold - - - bold - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - bold - - - bold - - - - - - - - - - - bold - - - bold - - - - - - - - - - - - - - - - - - - - - - bold - - - bold - - - - - - - - - - labelSize - - - labelSize - - - - - - - - - - - - - + + + + TaxationWithRoot.ecore + TaxationWithRoot.genmodel + platform:/plugin/org.eclipse.emf.ecore/model/Ecore.ecore + + + + + + + + + + + + + + + + + + + + + + + bold + + + + + + + bold + + + + + + + + + + bold + + + + + + + + + + bold + + + + bold + + + + + + + bold + + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + italic + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + + italic + + + + + + + + + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + + + + + + + + + bold + + + + + + + + bold + + + + + + + + + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + + italic + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + italic + + + + + + + + + + + + + + + + bold + + + + + + + + bold + + + + + + + + + italic + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + + italic + + + + + + + + bold + + + + + + + + + + + + + + + + + + + + + + + + bold + + + + + + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + + + labelSize + bold + + + labelSize + + + + + + + + + + labelSize + bold + + + labelSize + + + + + + + + + + labelSize + bold + + + labelSize + + + + + + + + + + labelSize + bold + + + labelSize + + + + + + + + + + + labelSize + + + labelSize + + + + + + + + + + + labelSize + + + labelSize + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + bold + + + bold + + + + + + + + + + + bold + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + bold + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + bold + + + bold + + + + + + + + + + + bold + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + bold + + + bold + + + + + + + + + + + bold + + + bold + + + + + + + + + + + + + + + + + + + + + + bold + + + bold + + + + + + + + + + labelSize + + + labelSize + + + + + + + + + + + + + -- cgit v1.2.3-54-g00ecf From a7b9a3eef14fc165909d00c65bb6fc1744a8ebd8 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 7 Jul 2020 15:00:13 +0200 Subject: Trying to fix performance regressions --- .../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes .../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes .../application/execution/SolverLoader.xtend | 56 +++++++++------- .../.SolverSemanticHighlightCalculator.xtendbin | Bin 5334 -> 5334 bytes .../.SolverSemanticTextAttributeProvider.xtendbin | Bin 4902 -> 4902 bytes .../validation/.SolverLanguageValidator.xtendbin | Bin 1717 -> 1717 bytes ....SolverLanguageTokenDefInjectingParser.xtendbin | Bin 2742 -> 2742 bytes ...nguageSyntheticTokenSyntacticSequencer.xtendbin | Bin 2758 -> 2758 bytes .../ModelGenerationMethodProvider.xtend | 3 +- .../MultiplicityGoalConstraintCalculator.xtend | 3 + .../logic2viatra/cardinality/ScopePropagator.xtend | 14 +++- .../logic2viatra/patterns/PatternGenerator.xtend | 2 +- .../patterns/RelationDeclarationIndexer.xtend | 4 +- .../patterns/RelationRefinementGenerator.xtend | 3 +- .../rules/GoalConstraintProvider.xtend | 71 +++++++++++++++++++-- .../viatrasolver/reasoner/ViatraReasoner.xtend | 12 +++- .../reasoner/ViatraReasonerConfiguration.xtend | 7 +- .../dse/BestFirstStrategyForModelGeneration.java | 8 +-- .../dse/ModelGenerationCompositeObjective.xtend | 27 ++++---- .../reasoner/dse/PunishSizeObjective.xtend | 70 ++++++++++++++++++++ .../viatrasolver/reasoner/dse/ScopeObjective.xtend | 2 +- .../case.study.familyTree.run/bin/.gitignore | 1 + .../config/genericSatellite.vsconfig | 7 +- 23 files changed, 227 insertions(+), 63 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PunishSizeObjective.xtend create mode 100644 Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend') diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin index 1641af7c..27ebff86 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin index d06f6684..4c3dcf43 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ 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 b1be56cb..bc4fa42f 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 @@ -10,6 +10,9 @@ import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Threshold 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.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy 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 @@ -98,42 +101,47 @@ class SolverLoader { console.writeError('''Malformed number format: «e.message»''') } } - if(config.containsKey("numeric-solver-at-end")) { + if (config.containsKey("numeric-solver-at-end")) { val stringValue = config.get("numeric-solver-at-end") - if(stringValue.equals("true")) { + if (stringValue.equals("true")) { println("numeric-solver-at-end") c.runIntermediateNumericalConsistencyChecks = false } } - if(config.containsKey("fitness-punishSize")) { + if (config.containsKey("fitness-punishSize")) { val stringValue = config.get("fitness-punishSize") - try { - c.punishSize = Boolean.parseBoolean(stringValue) - } catch(Exception e) {} + c.punishSize = Boolean.parseBoolean(stringValue) } - if(config.containsKey("fitness-scope")) { + if (config.containsKey("fitness-scope")) { val stringValue = config.get("fitness-scope") - try { - c.scopeWeight = Integer.parseInt(stringValue) - } catch(Exception e) {} + c.scopeWeight = Integer.parseInt(stringValue) } - if(config.containsKey("fitness-missing-containent")) { - val stringValue = config.get("fitness-missing-containent") - try { - c.conaintmentWeight = Integer.parseInt(stringValue) - } catch(Exception e) {} + if (config.containsKey("fitness-missing-containment")) { + val stringValue = config.get("fitness-missing-containment") + c.conaintmentWeight = Integer.parseInt(stringValue) } - if(config.containsKey("fitness-missing-noncontainent")) { - val stringValue = config.get("fitness-missing-noncontainent") - try { - c.nonContainmentWeight = Integer.parseInt(stringValue) - } catch(Exception e) {} + if (config.containsKey("fitness-missing-noncontainment")) { + val stringValue = config.get("fitness-missing-noncontainment") + c.nonContainmentWeight = Integer.parseInt(stringValue) } - if(config.containsKey("fitness-missing-wf")) { + if (config.containsKey("fitness-missing-wf")) { val stringValue = config.get("fitness-missing-wf") - try { - c.unfinishedWFWeight = Integer.parseInt(stringValue) - } catch(Exception e) {} + c.unfinishedWFWeight = Integer.parseInt(stringValue) + } + if (config.containsKey("fitness-objectCreationCosts")) { + val stringValue = config.get("fitness-objectCreationCosts") + c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue) + } + if (config.containsKey("scopePropagator")) { + val stringValue = config.get("scopePropagator") + c.scopePropagatorStrategy = switch (stringValue) { + case "polyhedral": new ScopePropagatorStrategy.Polyhedral( + PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp, true) + case "hybrid": new ScopePropagatorStrategy.Polyhedral( + PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp, false) + case "typeHierarchy": ScopePropagatorStrategy.BasicTypeHierarchy + default: throw new IllegalArgumentException("Unknown scope propagator: " + stringValue) + } } for (objectiveEntry : objectiveEntries) { val costObjectiveConfig = new CostObjectiveConfiguration diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin index b54e44de..dbdd38d8 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin index 4976e388..6b2259b5 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin index 6cd15573..5437df8f 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin index 3663bdb4..26756ae5 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin index 08e3330b..6f7cebd0 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin differ 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 78eda150..b79039cb 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 @@ -112,6 +112,7 @@ class ModelGenerationMethodProvider { ReasonerWorkspace workspace, boolean nameNewElements, TypeInferenceMethod typeInferenceMethod, + boolean calculateObjectCreationCosts, ScopePropagatorStrategy scopePropagatorStrategy, Collection hints, DocumentationLevel debugLevel @@ -135,7 +136,7 @@ class ModelGenerationMethodProvider { val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator, statistics) - val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries) + val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries,calculateObjectCreationCosts) val unfinishedWF = queries.getUnfinishedWFQueries.values diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend index 392ab3ee..273e0ac3 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend @@ -14,6 +14,9 @@ class MultiplicityGoalConstraintCalculator { val int cost new(String targetRelationName, IQuerySpecification querySpecification, boolean containment, int lowerBound, int cost) { + if (lowerBound <= 0) { + throw new IllegalArgumentException("Invalid lower bound: " + lowerBound) + } this.targetRelationName = targetRelationName this.querySpecification = querySpecification this.calculator = null diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend index 132ca8e8..3e95b2cc 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend @@ -60,15 +60,23 @@ class ScopePropagator { } } } while (changed) - + copyScopeBoundsToHeuristic() } def propagateAllScopeConstraints() { + if (!valid) { + return + } statistics.incrementScopePropagationCount() doPropagateAllScopeConstraints() } - + + def isValid() { + partialInterpretation.maxNewElements == -1 || + partialInterpretation.minNewElements <= partialInterpretation.maxNewElements + } + protected def copyScopeBoundsToHeuristic() { partialInterpretation.minNewElementsHeuristic = partialInterpretation.minNewElements for (scope : partialInterpretation.scopes) { @@ -109,7 +117,7 @@ class ScopePropagator { // 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»''') } - + protected def setScopesInvalid() { partialInterpretation.minNewElements = Integer.MAX_VALUE partialInterpretation.maxNewElements = 0 diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index f3125b80..80bc3844 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend @@ -51,7 +51,7 @@ class PatternGenerator { @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this) @Accessors(PUBLIC_GETTER) val UnitPropagationPreconditionGenerator unitPropagationPreconditionGenerator = new UnitPropagationPreconditionGenerator(this) - public new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) { + new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) { if(typeInferenceMethod == TypeInferenceMethod.Generic) { this.typeIndexer = new GenericTypeIndexer(this) this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this) diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend index cef707c5..b4403979 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend @@ -19,7 +19,7 @@ class RelationDeclarationIndexer { this.base = base } - public def generateRelationIndexers(LogicProblem problem, Iterable relations, Map fqn2PQuery) { + def generateRelationIndexers(LogicProblem problem, Iterable relations, Map fqn2PQuery) { val upperMultiplicities = new HashMap problem.annotations.filter(UpperMultiplicityAssertion).forEach[ upperMultiplicities.put(it.relation,it.upper) @@ -42,7 +42,7 @@ class RelationDeclarationIndexer { '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»''' } - public def referRelation( + def referRelation( RelationDeclaration referred, String sourceVariable, String targetVariable, diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend index d915d47e..783cd36b 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend @@ -5,12 +5,11 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality import java.util.LinkedList -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference class RelationRefinementGenerator { PatternGenerator base; - public new(PatternGenerator base) { + new(PatternGenerator base) { this.base = base } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index 7dc21410..732c135d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -1,13 +1,25 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns import java.util.ArrayList +import java.util.HashMap +import java.util.LinkedList +import java.util.List +import java.util.Map class GoalConstraintProvider { - - def getUnfinishedMultiplicityQueries(LogicProblem p, GeneratedPatterns patterns) { + + def getUnfinishedMultiplicityQueries(LogicProblem p, GeneratedPatterns patterns, boolean calculateObjectCost) { + val objectCosts = if (calculateObjectCost) { + calculateMissingObjectCost(p) + } else { + emptyMap + } val res = new ArrayList() for (entry : patterns.multiplicityConstraintQueries.entrySet) { val constraint = entry.key @@ -17,10 +29,61 @@ class GoalConstraintProvider { val query = queries.existingMultiplicityQuery val containment = constraint.containment val lowerBound = constraint.lowerBound - res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, containment, 1, lowerBound) + val cost = objectCosts.getOrDefault(constraint.relation, 1) + res += new MultiplicityGoalConstraintCalculator( + targetRelationName, + query, + containment, + lowerBound, + cost + ) } } return res } -} \ No newline at end of file + private def calculateMissingObjectCost(LogicProblem p) { + val containments = p.containmentHierarchies.head.containmentRelations + val containment2Lower = containments.toInvertedMap [ containment | + val lower = p.annotations.filter(LowerMultiplicityAssertion).filter[it.relation === containment].head + if (lower !== null) { + lower.lower + } else { + 0 + } + ] + val types = p.types + val Map>> type2NewCost = new HashMap + for (type : types) { + val allSupertypes = (#[type] + type.supertypes).toSet + val allOutgoingContainments = containments.filter [ + allSupertypes.contains((it.parameters.get(0) as ComplexTypeReference).referred) + ] + val list = new LinkedList + for (outgoingContainment : allOutgoingContainments) { + val value = containment2Lower.get(outgoingContainment) + if (value > 0) { + list.add((outgoingContainment.parameters.get(1) as ComplexTypeReference).referred -> value) + } + } + type2NewCost.put(type, list) + } + val res = new HashMap + for (containment : containments) { + val key = containment + val value = (containment.parameters.get(1) as ComplexTypeReference).referred.count(type2NewCost) +// println('''«key.name» --> «value» new''') + res.put(key, value) + } + return res + } + + private def int count(Type t, Map>> containments) { + val list = containments.get(t) + var r = 1 + for (element : list) { + r += element.value * element.key.count(containments) + } + return r + } +} 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 b9056685..b58033d7 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 @@ -43,6 +43,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel import org.eclipse.viatra.dse.solutionstore.SolutionStore import org.eclipse.viatra.dse.statecode.IStateCoderFactory +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective class ViatraReasoner extends LogicReasoner { val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() @@ -86,17 +87,24 @@ class ViatraReasoner extends LogicReasoner { workspace, viatraConfig.nameNewElements, viatraConfig.typeInferenceMethod, + viatraConfig.calculateObjectCreationCosts, viatraConfig.scopePropagatorStrategy, viatraConfig.hints, viatraConfig.documentationLevel ) - dse.addObjective(new ModelGenerationCompositeObjective( + val compositeObjective = new ModelGenerationCompositeObjective( basicScopeGlobalConstraint ?: new ScopeObjective, method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF), viatraConfig - )) + ) + dse.addObjective(compositeObjective) + if (viatraConfig.punishSize) { + val punishObjective = new PunishSizeObjective + punishObjective.level = compositeObjective.level + 1 + dse.addObjective(punishObjective) + } val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size) for (entry : viatraConfig.costObjectives.indexed) { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index e33a2590..a2f6de22 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend @@ -57,11 +57,12 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { public var runIntermediateNumericalConsistencyChecks = true - public var punishSize = true - public var scopeWeight = 2 - public var conaintmentWeight = 1 + public var punishSize = false + public var scopeWeight = 1 + public var conaintmentWeight = 2 public var nonContainmentWeight = 1 public var unfinishedWFWeight = 1 + public var calculateObjectCreationCosts = false public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) 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 09575384..a2de1abc 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 @@ -18,7 +18,6 @@ import java.util.List; import java.util.PriorityQueue; import java.util.Random; -import org.apache.log4j.Level; import org.apache.log4j.Logger; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.util.EcoreUtil; @@ -29,6 +28,8 @@ import org.eclipse.viatra.dse.objectives.Fitness; import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler; import org.eclipse.viatra.dse.solutionstore.SolutionStore; +import org.eclipse.viatra.query.runtime.api.IPatternMatch; +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher; import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; @@ -137,10 +138,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // ViatraQueryEngine engine = context.getQueryEngine(); // matchers = new LinkedList>(); // for(IQuerySpecification> p : this.method.getAllPatterns()) { -// ViatraQueryMatcher matcher = p.getMatcher(engine); -// matchers.add(matcher); +// ViatraQueryMatcher matcher = p.getMatcher(engine); // } - +// final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); this.comparator = new Comparator() { @Override 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 481f4ce1..27208cf4 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 @@ -9,13 +9,13 @@ import java.util.List import org.eclipse.viatra.dse.base.ThreadContext import org.eclipse.viatra.dse.objectives.Comparators import org.eclipse.viatra.dse.objectives.IObjective +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement class ModelGenerationCompositeObjective implements IThreeValuedObjective { val IObjective scopeObjective val List unfinishedMultiplicityObjectives val UnfinishedWFObjective unfinishedWFObjective var PartialInterpretation model = null - val boolean punishSize val int scopeWeight val int conaintmentWeight val int nonContainmentWeight @@ -28,7 +28,7 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective { ViatraReasonerConfiguration configuration) { this( - scopeObjective, unfinishedMultiplicityObjectives, unfinishedWFObjective, configuration.punishSize, + scopeObjective, unfinishedMultiplicityObjectives, unfinishedWFObjective, configuration.scopeWeight, configuration.conaintmentWeight, configuration.nonContainmentWeight, configuration.unfinishedWFWeight ) @@ -38,13 +38,12 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective { IObjective scopeObjective, List unfinishedMultiplicityObjectives, UnfinishedWFObjective unfinishedWFObjective, - boolean punishSize, int scopeWeight, int conaintmentWeight, int nonContainmentWeight, int unfinishedWFWeight) + int scopeWeight, int conaintmentWeight, int nonContainmentWeight, int unfinishedWFWeight) { this.scopeObjective = scopeObjective this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives this.unfinishedWFObjective = unfinishedWFObjective - this.punishSize = punishSize this.scopeWeight = scopeWeight this.conaintmentWeight = conaintmentWeight this.nonContainmentWeight = nonContainmentWeight @@ -63,7 +62,7 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective { scopeObjective.createNew, ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew as UnfinishedMultiplicityObjective]), unfinishedWFObjective.createNew as UnfinishedWFObjective, - punishSize, scopeWeight, conaintmentWeight, nonContainmentWeight, unfinishedWFWeight + scopeWeight, conaintmentWeight, nonContainmentWeight, unfinishedWFWeight ) } @@ -77,16 +76,14 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective { var containmentMultiplicity = 0.0 var nonContainmentMultiplicity = 0.0 for(multiplicityObjective : unfinishedMultiplicityObjectives) { + val multiplicity = multiplicityObjective.getFitness(context) +// println(multiplicityObjective.name + "=" + multiplicity) if(multiplicityObjective.containment) { - containmentMultiplicity+=multiplicityObjective.getFitness(context) + containmentMultiplicity+=multiplicity } else { - nonContainmentMultiplicity+=multiplicityObjective.getFitness(context) + nonContainmentMultiplicity+=multiplicity } - } - val size = if(punishSize) { - 0.9/model.newElements.size - } else { - 0 + } var sum = 0.0 @@ -94,7 +91,9 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective { sum += containmentMultiplicity*conaintmentWeight sum += nonContainmentMultiplicity*nonContainmentWeight sum += unfinishedWFsFitness*unfinishedWFWeight - sum+=size + +// println('''scope=«scopeFitnes», containment=«containmentMultiplicity», nonContainment=«nonContainmentMultiplicity», wf=«unfinishedWFsFitness», sum=«sum»''') + return sum } @@ -112,7 +111,7 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective { override isHardObjective() { true } - override satisifiesHardObjective(Double fitness) { fitness <= 0.9 } + override satisifiesHardObjective(Double fitness) { fitness < 0.01 } override setComparator(Comparator comparator) { throw new UnsupportedOperationException("Model generation objective comparator cannot be set.") diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PunishSizeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PunishSizeObjective.xtend new file mode 100644 index 00000000..8505661c --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PunishSizeObjective.xtend @@ -0,0 +1,70 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective +import java.util.Comparator +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.viatra.dse.objectives.Comparators +import org.eclipse.xtend.lib.annotations.Accessors + +class PunishSizeObjective implements IThreeValuedObjective { + @Accessors int level = 3 + + override createNew() { + this + } + + override init(ThreadContext context) { + // Nothing to initialize. + } + + override getComparator() { + Comparators.LOWER_IS_BETTER + } + + override getFitness(ThreadContext threadContext) { + val model = threadContext.model + if (model instanceof PartialInterpretation) { + val size = model.newObjectCount +// println('''size=«size»''') + size as double + } else { + throw new IllegalArgumentException("notifier must be a PartialInterpretation") + } + } + + override getBestPossibleFitness(ThreadContext threadContext) { + getFitness(threadContext) + } + + override getWorstPossibleFitness(ThreadContext threadContext) { + val model = threadContext.model + if (model instanceof PartialInterpretation) { + (model.newObjectCount + model.maxNewElements) as double + } else { + throw new IllegalArgumentException("notifier must be a PartialInterpretation") + } + } + + private def getNewObjectCount(PartialInterpretation interpretation) { + interpretation.newElements.reject[it instanceof PrimitiveElement].size + } + + override getName() { + typeof(PunishSizeObjective).name + } + + override isHardObjective() { + false + } + + override satisifiesHardObjective(Double fitness) { + true + } + + override setComparator(Comparator comparator) { + throw new UnsupportedOperationException("Model generation objective comparator cannot be set.") + } + +} \ 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/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 7abc5cb8..b61bd20b 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 @@ -25,7 +25,7 @@ class ScopeObjective implements IObjective{ val interpretation = context.model as PartialInterpretation var res = interpretation.minNewElementsHeuristic.doubleValue for(scope : interpretation.scopes) { - res += scope.minNewElementsHeuristic + res += scope.minNewElementsHeuristic * 2 } return res } diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore new file mode 100644 index 00000000..7050a7e3 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore @@ -0,0 +1 @@ +/queries/ diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig index 127b174d..2ff20880 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig @@ -23,7 +23,7 @@ generate { generate { metamodel = { package satellite } constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } - partial-model = { "inputs/SatelliteInstance.xmi"} + partial-model = { "inputs/SatelliteInstance.xmi" } solver = ViatraSolver scope = { #node += 64..* @@ -33,7 +33,10 @@ generate { runtime = 10000, log-level = normal, "fitness-scope" = "3", - "fitness-objectCreationCosts" = "true" + "fitness-punishSize" = "true", + "fitness-objectCreationCosts" = "true", + "scopePropagator" = "typeHierarchy", + "fitness-missing-containment" = "2" } runs = 1 -- cgit v1.2.3-54-g00ecf