From 21ebd1b18fc450a9fe84bef0af2f85396d05bea9 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Mon, 11 May 2020 00:17:10 +0200 Subject: automated containment and attribute addition for subclasses --- .../rules/RefinementRuleProvider.xtend | 65 ++++++++++++---------- 1 file changed, 37 insertions(+), 28 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') 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 db0e17b9..f2efc87a 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 @@ -176,6 +176,10 @@ class RefinementRuleProvider { val number = lowermultiplicities.head.lower if(number > 0) { val sourceTypeInterpretation = getTypeInterpretation(i, relation, 0) as PartialComplexTypeInterpretation + val subtypeInterpretations = i.partialtypeinterpratation.filter(PartialComplexTypeInterpretation).filter[ + it === sourceTypeInterpretation || + it.supertypeInterpretation.contains(sourceTypeInterpretation) + ] if(containmentReferences.contains(relation)) { val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) @@ -188,41 +192,46 @@ class RefinementRuleProvider { inverseAnnotation.head.inverseA } val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head - for(var times=0; times Date: Mon, 11 May 2020 02:22:15 +0200 Subject: separated must and current UP rules to support non-prop neg finds --- .../ModelGenerationMethodProvider.xtend | 9 ++-- .../logic2viatra/patterns/PatternGenerator.xtend | 12 ++++- .../logic2viatra/patterns/PatternProvider.xtend | 20 +++++--- .../UnitPropagationPreconditionGenerator.xtend | 42 ++++++++++++---- .../dse/BestFirstStrategyForModelGeneration.java | 18 ++++--- .../dse/ModelGenerationCompositeObjective.xtend | 2 +- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 58 +++++++++++++--------- 7 files changed, 106 insertions(+), 55 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') 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 975ace2f..be11ed78 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 @@ -38,7 +38,8 @@ class ModelGenerationStatistics { Collection>> invalidWF - Map>> unitPropagationPreconditions + Map>> mustUnitPropagationPreconditions + Map>> currentUnitPropagationPreconditions Collection>> allPatterns } @@ -81,7 +82,8 @@ class ModelGenerationMethodProvider { val invalidWF = queries.getInvalidWFQueries.values - val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns + val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns + val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns return new ModelGenerationMethod( statistics, @@ -90,7 +92,8 @@ class ModelGenerationMethodProvider { unfinishedMultiplicities, unfinishedWF, invalidWF, - unitPropagationPreconditions, + mustUnitPropagationPreconditions, + currentUnitPropagationPreconditions, queries.allQueries ) } 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 d5ebe318..219f99e9 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 @@ -26,6 +26,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.xtend.lib.annotations.Accessors import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import org.eclipse.xtend.lib.annotations.Data +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint + +@Data class PatternGeneratorResult { + CharSequence patternText + HashMap constraint2MustPreconditionName + HashMap constraint2CurrentPreconditionName +} class PatternGenerator { @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) @@ -149,7 +157,7 @@ class PatternGenerator { problem.allTypeReferences.exists[it instanceof StringTypeReference] } - public def transformBaseProperties( + public def PatternGeneratorResult transformBaseProperties( LogicProblem problem, PartialInterpretation emptySolution, Map fqn2PQuery, @@ -398,6 +406,6 @@ class PatternGenerator { ''' val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) val second = up.definitions - return (first+second) -> up.constraint2PreconditionName + return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName) } } 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 18e3018a..750107f6 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 @@ -31,7 +31,8 @@ import java.util.HashMap public Map>> refineObjectQueries public Map>> refineTypeQueries public Map, IQuerySpecification>> refinerelationQueries - public Map>> unitPropagationPreconditionPatterns + public Map>> mustUnitPropagationPreconditionPatterns + public Map>> currentUnitPropagationPreconditionPatterns public Collection>> allQueries } @@ -60,14 +61,15 @@ class PatternProvider { null } val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) - val baseIndexerFile = patternGeneratorResult.key - val unitPropagationTrace = patternGeneratorResult.value + val baseIndexerFile = patternGeneratorResult.patternText + val mustUnitPropagationTrace = patternGeneratorResult.constraint2MustPreconditionName + val currentUnitPropagationTrace = patternGeneratorResult.constraint2CurrentPreconditionName if(writeToFile) { workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) } val ParseUtil parseUtil = new ParseUtil val generatedQueries = parseUtil.parse(baseIndexerFile) - val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,unitPropagationTrace,generatedQueries); + val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,mustUnitPropagationTrace,currentUnitPropagationTrace,generatedQueries); return runtimeQueries } @@ -76,7 +78,8 @@ class PatternProvider { LogicProblem problem, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult, - HashMap unitPropagationTrace, + HashMap mustUnitPropagationTrace, + HashMap currentUnitPropagationTrace, Map>> queries ) { val Map>> @@ -92,7 +95,9 @@ class PatternProvider { val Map, IQuerySpecification>> refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] val Map>> - unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)] + mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)] + val Map>> + currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)] return new GeneratedPatterns( invalidWFQueries, unfinishedWFQueries, @@ -100,7 +105,8 @@ class PatternProvider { refineObjectsQueries, refineTypeQueries, refineRelationQueries, - unitPropagationPreconditionPatterns, + mustUnitPropagationPreconditionPatterns, + currentUnitPropagationPreconditionPatterns, queries.values ) } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend index d487db64..91a7a2c2 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend @@ -61,7 +61,8 @@ class UnitPropagationPreconditionGenerationResult { @Data class UnitPropagationPreconditionFinalResult { CharSequence definitions - HashMap constraint2PreconditionName + HashMap constraint2MustPreconditionName + HashMap constraint2CurrentPreconditionName } class UnitPropagationPreconditionGenerator { @@ -81,25 +82,34 @@ class UnitPropagationPreconditionGenerator { // Create an empty result val res = new UnitPropagationPreconditionGenerationResult val wfs = base.wfQueries(problem)//.map[it.patternPQuery] - val Map>> mainPropagationNames = new HashMap + val Map>> mainMustPropagationNames = new HashMap + val Map>> mainCurrentPropagationNames = new HashMap for(wf : wfs) { val query = wf.patternPQuery as PQuery val relation = wf.target val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) for(referredCheck : allReferredChecks) { - val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) - if(!mainPropagationNames.containsKey(referredCheck)) { - mainPropagationNames.put(referredCheck,new LinkedList) + val mustPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) + val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT) + if(!mainMustPropagationNames.containsKey(referredCheck)) { + mainMustPropagationNames.put(referredCheck,new LinkedList) } - if(propagationPrecondition !== null) { - mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size) + if(!mainCurrentPropagationNames.containsKey(referredCheck)) { + mainCurrentPropagationNames.put(referredCheck,new LinkedList) + } + if(mustPropagationPrecondition !== null) { + mainMustPropagationNames.get(referredCheck).add(mustPropagationPrecondition->query.parameterNames.size) + } + if(currentPropagationPrecondition !== null) { + mainCurrentPropagationNames.get(referredCheck).add(currentPropagationPrecondition->query.parameterNames.size) } } } val preconditions = new LinkedList - val constraint2Precondition = new HashMap - for(entry : mainPropagationNames.entrySet) { + val constraint2MustPrecondition = new HashMap + val constraint2CurrentPrecondition = new HashMap + for(entry : mainMustPropagationNames.entrySet) { val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; val def = ''' pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») @@ -107,7 +117,17 @@ class UnitPropagationPreconditionGenerator { { find «propagation.key»(problem,interpretation,«FOR index : 0.. trace = solutionStoreWithCopy.newSolution(context); - numericSolver.fillSolutionCopy(trace); - solutionStoreWithDiversityDescriptor.newSolution(context); - solutionStore.newSolution(context); - configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); + if(numericSolver.currentSatisfiable()) { + Map trace = solutionStoreWithCopy.newSolution(context); + numericSolver.fillSolutionCopy(trace); + solutionStoreWithDiversityDescriptor.newSolution(context); + solutionStore.newSolution(context); + configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); - logger.debug("Found a solution."); + logger.debug("Found a solution."); + } } } } 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 a75ddf76..9e4792e0 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 @@ -62,7 +62,7 @@ class ModelGenerationCompositeObjective implements IObjective{ } var sum = 0.0 sum += scopeFitnes - sum +=Math.sqrt(multiplicity *0.1) + sum +=multiplicity sum += unfinishedWFsFitness//*0.5 println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index 71793aa6..fe378bd3 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend @@ -1,30 +1,29 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse -import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod -import java.util.HashMap -import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine -import org.eclipse.viatra.query.runtime.api.IPatternMatch -import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher -import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator -import org.eclipse.viatra.dse.base.ThreadContext -import org.eclipse.emf.ecore.EObject -import java.util.Map -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.logic2viatra.ModelGenerationMethod 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.StringElement +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.partialinterpretationlanguage.partialinterpretation.RealElement -import java.util.List +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement import java.math.BigDecimal -import java.util.LinkedHashSet +import java.util.HashMap import java.util.LinkedHashMap +import java.util.LinkedHashSet +import java.util.List +import java.util.Map +import org.eclipse.emf.ecore.EObject +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint class NumericSolver { val ThreadContext threadContext; - val constraint2UnitPropagationPrecondition = new HashMap> + val constraint2MustUnitPropagationPrecondition = new HashMap> + val constraint2CurrentUnitPropagationPrecondition = new HashMap> NumericTranslator t = new NumericTranslator val boolean caching; @@ -38,11 +37,17 @@ class NumericSolver { new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { this.threadContext = threadContext val engine = threadContext.queryEngine - for(entry : method.unitPropagationPreconditions.entrySet) { + for(entry : method.mustUnitPropagationPreconditions.entrySet) { + val constraint = entry.key + val querySpec = entry.value + val matcher = querySpec.getMatcher(engine); + constraint2MustUnitPropagationPrecondition.put(constraint,matcher) + } + for(entry : method.currentUnitPropagationPreconditions.entrySet) { val constraint = entry.key val querySpec = entry.value val matcher = querySpec.getMatcher(engine); - constraint2UnitPropagationPrecondition.put(constraint,matcher) + constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) } this.caching = caching } @@ -52,14 +57,21 @@ class NumericSolver { def getNumberOfSolverCalls(){numberOfSolverCalls} def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} - def boolean isSatisfiable() { + def boolean maySatisfiable() { + isSatisfiable(this.constraint2MustUnitPropagationPrecondition) + } + def boolean currentSatisfiable() { + isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition) + } + + private def boolean isSatisfiable(Map> matches) { val start = System.nanoTime var boolean finalResult - if(constraint2UnitPropagationPrecondition.empty){ + if(matches.empty){ finalResult=true } else { val propagatedConstraints = new HashMap - for(entry : constraint2UnitPropagationPrecondition.entrySet) { + for(entry : matches.entrySet) { val constraint = entry.key //println(constraint) val allMatches = entry.value.allMatches.map[it.toArray] @@ -108,11 +120,11 @@ class NumericSolver { def fillSolutionCopy(Map trace) { val model = threadContext.getModel as PartialInterpretation val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList - if(constraint2UnitPropagationPrecondition.empty) { + if(constraint2CurrentUnitPropagationPrecondition.empty) { fillWithDefaultValues(dataObjects,trace) } else { val propagatedConstraints = new HashMap - for(entry : constraint2UnitPropagationPrecondition.entrySet) { + for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { val constraint = entry.key val allMatches = entry.value.allMatches.map[it.toArray] propagatedConstraints.put(constraint,allMatches) -- cgit v1.2.3-70-g09d2 From 4c80187e223ed4b500a68a5d83446f80565e3440 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Mon, 11 May 2020 04:06:18 +0200 Subject: Instead of Bigdecimals doubleValue are used in check --- .../patterns/PConstraintTransformer.xtend | 6 +++-- .../patterns/PExpressionGenerator.xtend | 29 ++++++++++++++-------- 2 files changed, 22 insertions(+), 13 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') 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 5ca78e97..423bb204 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 @@ -28,6 +28,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference +import java.util.Map class PConstraintTransformer { val extension RelationDefinitionIndexer relationDefinitionIndexer; @@ -226,6 +227,7 @@ class PConstraintTransformer { throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''') } else { val expression = expressionExtractor.extractExpression(e.evaluator) + val Map variable2Type = e.affectedVariables.toInvertedMap[v|variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference] if(modality.isMay) { return ''' «FOR variable: e.affectedVariables» @@ -234,7 +236,7 @@ class PConstraintTransformer { check( «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR» || - («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])») + («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)») ); ''' } else { // Must or Current @@ -242,7 +244,7 @@ class PConstraintTransformer { «FOR variable: e.affectedVariables» PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)» «ENDFOR» - check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])»); + check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»); ''' } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend index 303c87b9..62ff92b2 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend @@ -8,6 +8,8 @@ import org.eclipse.xtext.xbase.XFeatureCall import org.eclipse.xtext.xbase.XMemberFeatureCall import org.eclipse.xtext.xbase.XNumberLiteral import org.eclipse.xtext.xbase.XUnaryOperation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference class PExpressionGenerator { static val N_Base = "org.eclipse.xtext.xbase.lib." @@ -38,9 +40,9 @@ class PExpressionGenerator { static val N_POWER2 = "java.lang.Math.pow" - def dispatch CharSequence translateExpression(XBinaryOperation e, Map valueName) { - val left = e.leftOperand.translateExpression(valueName) - val right = e.rightOperand.translateExpression(valueName) + def dispatch CharSequence translateExpression(XBinaryOperation e, Map valueName, Map variable2Type) { + val left = e.leftOperand.translateExpression(valueName,variable2Type) + val right = e.rightOperand.translateExpression(valueName,variable2Type) val feature = e.feature.qualifiedName if(feature.isN(N_MINUS2)) { return '''(«left»-«right»)'''} else if(feature.isN(N_PLUS2)) { return '''(«left»+«right»)''' } @@ -65,8 +67,8 @@ class PExpressionGenerator { } } - def dispatch CharSequence translateExpression(XUnaryOperation e, Map valueName) { - val operand = e.operand.translateExpression(valueName) + def dispatch CharSequence translateExpression(XUnaryOperation e, Map valueName, Map variable2Type) { + val operand = e.operand.translateExpression(valueName,variable2Type) val feature = e.feature.qualifiedName if(feature.isN(N_MINUS1)) { return '''(-«operand»)'''} else if(feature.isN(N_PLUS1)) { return '''(+«operand»)'''} @@ -78,8 +80,8 @@ class PExpressionGenerator { } } - def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map valueName) { - val transformedArguments = e.actualArguments.map[translateExpression(valueName)] + def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map valueName, Map variable2Type) { + val transformedArguments = e.actualArguments.map[translateExpression(valueName,variable2Type)] val feature = e.feature.qualifiedName if(feature == N_POWER2) { return '''Math.pow(«transformedArguments.get(0)»,«transformedArguments.get(1)»)''' @@ -91,19 +93,24 @@ class PExpressionGenerator { } } - def dispatch CharSequence translateExpression(XFeatureCall e, Map valueName) { + def dispatch CharSequence translateExpression(XFeatureCall e, Map valueName, Map variable2Type) { val featureName = e.feature.qualifiedName + val type = variable2Type.entrySet.filter[it.key.name===featureName].head.value val entryWithName = valueName.entrySet.filter[it.key.name == featureName].head if(entryWithName !== null) { - return entryWithName.value + if(type instanceof RealTypeReference) { + return '''(«entryWithName.value».doubleValue)''' + } else { + return entryWithName.value + } } else { throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''') } } - def dispatch CharSequence translateExpression(XNumberLiteral l, Map valueName) '''«l.value»''' + def dispatch CharSequence translateExpression(XNumberLiteral l, Map valueName, Map variable2Type) '''«l.value»''' - def dispatch CharSequence translateExpression(XExpression expression, Map valueName) { + def dispatch CharSequence translateExpression(XExpression expression, Map valueName, Map variable2Type) { throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''') } } \ No newline at end of file -- cgit v1.2.3-70-g09d2 From eae32efa9e202025cab8d2e0cb53a425e467c902 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Mon, 11 May 2020 04:21:58 +0200 Subject: temporally removed check expressions for real values --- .../viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') 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 423bb204..4a8da38c 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,8 +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» ); ''' } else { // Must or Current @@ -244,7 +246,9 @@ class PConstraintTransformer { «FOR variable: e.affectedVariables» PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)» «ENDFOR» - check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»); + «IF variable2Type.values.filter(RealTypeReference).empty» + check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»); + «ENDIF» ''' } } -- cgit v1.2.3-70-g09d2 From 90965ed13b119b98298a26a39377cc4120620f5f Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Mon, 11 May 2020 20:56:57 +0200 Subject: fix for inverse references --- .../viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') 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 f2efc87a..1e7f1d2b 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 @@ -184,7 +184,7 @@ class RefinementRuleProvider { if(containmentReferences.contains(relation)) { val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) if(!(targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.isIsAbstract) { - val inverseAnnotation = p.assertions.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] + val inverseAnnotation = p.annotations.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] if(!inverseAnnotation.empty) { val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) { inverseAnnotation.head.inverseB -- cgit v1.2.3-70-g09d2 From cc3c5ecce23e77c960801c9ac6d80aad1deadaec Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 12 May 2020 02:18:02 +0200 Subject: variable indexing bugs in referred patterns in UP --- .../logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend index 91a7a2c2..400f47bc 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend @@ -211,7 +211,7 @@ class UnitPropagationPreconditionGenerator { // Propagation for constraint referred indirectly from this pattern through «referredName» find «referredName»(problem, interpretation, «FOR index : 0.. Date: Tue, 12 May 2020 02:23:24 +0200 Subject: Object is recursively instantiated if it has no subtype alternative --- .../viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') 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 1e7f1d2b..16438a5a 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 @@ -183,7 +183,8 @@ class RefinementRuleProvider { if(containmentReferences.contains(relation)) { val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) - if(!(targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.isIsAbstract) { + val targetType = (targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf + if((!targetType.isIsAbstract) && (targetType.supertypes.empty)) { val inverseAnnotation = p.annotations.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] if(!inverseAnnotation.empty) { val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) { -- cgit v1.2.3-70-g09d2 From 9280c0b646cd446251a1c8e16d1a05eff662bd47 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 12 May 2020 02:25:19 +0200 Subject: removed potential equivalence between real values and integers --- .../logic2viatra/patterns/PatternGenerator.xtend | 38 ---------------------- 1 file changed, 38 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') 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 219f99e9..d92f2e30 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 @@ -239,30 +239,6 @@ class PatternGenerator { RealElement(a); RealElement(b); PrimitiveElement.valueSet(b,false); - } or { - find mayExist(problem,interpretation,a); - find mayExist(problem,interpretation,b); - RealElement(a); - IntegerElement(b); - PrimitiveElement.valueSet(a,false); - } or { - find mayExist(problem,interpretation,a); - find mayExist(problem,interpretation,b); - RealElement(a); - IntegerElement(b); - PrimitiveElement.valueSet(b,false); - } or { - find mayExist(problem,interpretation,a); - find mayExist(problem,interpretation,b); - IntegerElement(a); - RealElement(b); - PrimitiveElement.valueSet(a,false); - } or { - find mayExist(problem,interpretation,a); - find mayExist(problem,interpretation,b); - IntegerElement(a); - RealElement(b); - PrimitiveElement.valueSet(b,false); } or { find mayExist(problem,interpretation,a); find mayExist(problem,interpretation,b); @@ -296,20 +272,6 @@ class PatternGenerator { PrimitiveElement.valueSet(b,true); RealElement.value(a,value); RealElement.value(b,value); - } or { - find mustExist(problem,interpretation,a); - find mustExist(problem,interpretation,b); - PrimitiveElement.valueSet(a,true); - PrimitiveElement.valueSet(b,true); - RealElement.value(a,value); - IntegerElement.value(b,value); - } or { - find mustExist(problem,interpretation,a); - find mustExist(problem,interpretation,b); - PrimitiveElement.valueSet(a,true); - PrimitiveElement.valueSet(b,true); - IntegerElement.value(a,value); - RealElement.value(b,value); } or { find mustExist(problem,interpretation,a); find mustExist(problem,interpretation,b); -- cgit v1.2.3-70-g09d2 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') 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-70-g09d2 From 315747ca5b4b0e78468b49406957ac9ac48ecae1 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Tue, 12 May 2020 03:14:53 +0200 Subject: removed unnecessary printing --- .../logic2viatra/MultiplicityGoalConstraintCalculator.xtend | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') 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 e1358fb6..6435806d 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 @@ -49,9 +49,9 @@ class MultiplicityGoalConstraintCalculator { val missingMultiplicity = match.get(4) as Integer res += missingMultiplicity - if(missingMultiplicity!=0) { - println(targetRelationName+ " missing multiplicity: "+missingMultiplicity) - } +// if(missingMultiplicity!=0) { +// println(targetRelationName+ " missing multiplicity: "+missingMultiplicity) +// } } //println(targetRelationName+ " all missing multiplicities: "+res) return res*cost -- cgit v1.2.3-70-g09d2 From 22404c4023785c3f8922cccfbefc7bc9ac1e1a30 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Wed, 13 May 2020 16:34:19 +0200 Subject: upper limit is soft --- .../inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend index df38337e..0acae00f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend @@ -75,7 +75,8 @@ class ScopePropagator { if(this.partialInterpretation.maxNewElements > 0) { this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1 } else if(this.partialInterpretation.maxNewElements === 0) { - throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') + this.partialInterpretation.maxNewElements = 0 + //throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') } // subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)] -- cgit v1.2.3-70-g09d2 From cf17186c9c84aec2c08836c362515faba9d6bf2a Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Thu, 14 May 2020 00:23:47 +0200 Subject: removeOne for object scope --- .../inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend index 0acae00f..abfa4554 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend @@ -148,7 +148,8 @@ class ScopePropagator { } private def removeOne(Scope scope) { if(scope.maxNewElements===0) { - throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') + scope.maxNewElements=0 + //throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') } else if(scope.maxNewElements>0) { scope.maxNewElements= scope.maxNewElements-1 } -- cgit v1.2.3-70-g09d2 From 6d5b1d25c162f105a2ba1f5019574943d4a3c0e0 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Thu, 14 May 2020 22:55:31 +0200 Subject: fixes for the measurement --- .../application/execution/SolverLoader.xtend | 7 ++ .../logic2viatra/patterns/PatternGenerator.xtend | 114 ++++++++++----------- .../viatrasolver/reasoner/ViatraReasoner.xtend | 6 +- .../reasoner/ViatraReasonerConfiguration.xtend | 2 + .../dse/BestFirstStrategyForModelGeneration.java | 6 +- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 73 +++++++------ 6 files changed, 115 insertions(+), 93 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') 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 3f0ba03f..ca272381 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 @@ -87,6 +87,13 @@ class SolverLoader { ] } catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')} } + if(config.containsKey("numeric-solver-at-end")) { + val stringValue = config.get("numeric-solver-at-end") + if(stringValue.equals("true")) { + println("numeric-solver-at-end") + c.runIntermediateNumericalConsistencyChecks= false + } + } ] } 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/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 d92f2e30..677170b8 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 @@ -215,42 +215,42 @@ class PatternGenerator { find mayExist(problem,interpretation,a); find mayExist(problem,interpretation,b); a == b; - } or { - find mayExist(problem,interpretation,a); - find mayExist(problem,interpretation,b); - IntegerElement(a); - IntegerElement(b); - PrimitiveElement.valueSet(a,false); - } or { - find mayExist(problem,interpretation,a); - find mayExist(problem,interpretation,b); - IntegerElement(a); - IntegerElement(b); - PrimitiveElement.valueSet(b,false); - } or { - find mayExist(problem,interpretation,a); - find mayExist(problem,interpretation,b); - RealElement(a); - RealElement(b); - PrimitiveElement.valueSet(a,false); - } or { - find mayExist(problem,interpretation,a); - find mayExist(problem,interpretation,b); - RealElement(a); - RealElement(b); - PrimitiveElement.valueSet(b,false); - } or { - find mayExist(problem,interpretation,a); - find mayExist(problem,interpretation,b); - StringElement(a); - StringElement(b); - PrimitiveElement.valueSet(a,false); - } or { - find mayExist(problem,interpretation,a); - find mayExist(problem,interpretation,b); - StringElement(a); - StringElement(b); - PrimitiveElement.valueSet(b,false); +««« } or { +««« find mayExist(problem,interpretation,a); +««« find mayExist(problem,interpretation,b); +««« IntegerElement(a); +««« IntegerElement(b); +««« PrimitiveElement.valueSet(a,false); +««« } or { +««« find mayExist(problem,interpretation,a); +««« find mayExist(problem,interpretation,b); +««« IntegerElement(a); +««« IntegerElement(b); +««« PrimitiveElement.valueSet(b,false); +««« } or { +««« find mayExist(problem,interpretation,a); +««« find mayExist(problem,interpretation,b); +««« RealElement(a); +««« RealElement(b); +««« PrimitiveElement.valueSet(a,false); +««« } or { +««« find mayExist(problem,interpretation,a); +««« find mayExist(problem,interpretation,b); +««« RealElement(a); +««« RealElement(b); +««« PrimitiveElement.valueSet(b,false); +««« } or { +««« find mayExist(problem,interpretation,a); +««« find mayExist(problem,interpretation,b); +««« StringElement(a); +««« StringElement(b); +««« PrimitiveElement.valueSet(a,false); +««« } or { +««« find mayExist(problem,interpretation,a); +««« find mayExist(problem,interpretation,b); +««« StringElement(a); +««« StringElement(b); +««« PrimitiveElement.valueSet(b,false); } pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { @@ -258,27 +258,27 @@ class PatternGenerator { find mustExist(problem,interpretation,a); find mustExist(problem,interpretation,b); a == b; - } or { - find mustExist(problem,interpretation,a); - find mustExist(problem,interpretation,b); - PrimitiveElement.valueSet(a,true); - PrimitiveElement.valueSet(b,true); - IntegerElement.value(a,value); - IntegerElement.value(b,value); - } or { - find mustExist(problem,interpretation,a); - find mustExist(problem,interpretation,b); - PrimitiveElement.valueSet(a,true); - PrimitiveElement.valueSet(b,true); - RealElement.value(a,value); - RealElement.value(b,value); - } or { - find mustExist(problem,interpretation,a); - find mustExist(problem,interpretation,b); - PrimitiveElement.valueSet(a,true); - PrimitiveElement.valueSet(b,true); - StringElement.value(a,value); - StringElement.value(b,value); +««« } or { +««« find mustExist(problem,interpretation,a); +««« find mustExist(problem,interpretation,b); +««« PrimitiveElement.valueSet(a,true); +««« PrimitiveElement.valueSet(b,true); +««« IntegerElement.value(a,value); +««« IntegerElement.value(b,value); +««« } or { +««« find mustExist(problem,interpretation,a); +««« find mustExist(problem,interpretation,b); +««« PrimitiveElement.valueSet(a,true); +««« PrimitiveElement.valueSet(b,true); +««« RealElement.value(a,value); +««« RealElement.value(b,value); +««« } or { +««« find mustExist(problem,interpretation,a); +««« find mustExist(problem,interpretation,b); +««« PrimitiveElement.valueSet(a,true); +««« PrimitiveElement.valueSet(b,true); +««« StringElement.value(a,value); +««« StringElement.value(b,value); } ////////// 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 293df935..1fe65afe 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 @@ -113,8 +113,9 @@ class ViatraReasoner extends LogicReasoner{ val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) viatraConfig.progressMonitor.workedForwardTransformation + val transformationFinished = System.nanoTime + val transformationTime = transformationFinished - transformationStartTime - val transformationTime = System.nanoTime - transformationStartTime val solverStartTime = System.nanoTime var boolean stoppedByTimeout @@ -140,6 +141,9 @@ class ViatraReasoner extends LogicReasoner{ it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int ] } + it.entries += createIntStatisticEntry => [ + it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int + ] it.entries += createIntStatisticEntry => [ it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int ] 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 c4d7e231..24578e7b 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 @@ -45,6 +45,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{ * Configuration for cutting search space. */ public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint + + public var runIntermediateNumericalConsistencyChecks = true } public class DiversityDescriptor { 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 45dffe7c..75ce7f10 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 @@ -91,6 +91,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { private int numberOfPrintedModel = 0; private int numberOfSolverCalls = 0; + public long explorationStarted = 0; public BestFirstStrategyForModelGeneration( ReasonerWorkspace workspace, @@ -119,7 +120,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // ViatraQueryEngine engine = context.getQueryEngine(); // // TODO: visualisation -// matchers = new LinkedList>(); +// LinkedList> matchers = new LinkedList>(); // for(IQuerySpecification> p : this.method.getAllPatterns()) { // //System.out.println(p.getSimpleName()); // ViatraQueryMatcher matcher = p.getMatcher(engine); @@ -137,13 +138,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { } }; - this.numericSolver = new NumericSolver(context, method, false); + this.numericSolver = new NumericSolver(context, method, false,this.configuration.runIntermediateNumericalConsistencyChecks); trajectoiresToExplore = new PriorityQueue(11, comparator); } @Override public void explore() { + this.explorationStarted=System.nanoTime(); if (!context.checkGlobalConstraints()) { logger.info("Global contraint is not satisifed in the first state. Terminate."); return; diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index 0fb5d702..a012f51b 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend @@ -26,6 +26,7 @@ class NumericSolver { val constraint2CurrentUnitPropagationPrecondition = new HashMap> NumericTranslator t = new NumericTranslator + val boolean intermediateConsistencyCheck val boolean caching; Map>>,Boolean> satisfiabilityCache = new HashMap @@ -34,7 +35,7 @@ class NumericSolver { var int numberOfSolverCalls = 0 var int numberOfCachedSolverCalls = 0 - new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { + new(ThreadContext threadContext, ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) { this.threadContext = threadContext val engine = threadContext.queryEngine for(entry : method.mustUnitPropagationPreconditions.entrySet) { @@ -49,6 +50,8 @@ class NumericSolver { val matcher = querySpec.getMatcher(engine); constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) } + this.intermediateConsistencyCheck = true + println() this.caching = caching } @@ -70,44 +73,48 @@ class NumericSolver { private def boolean isSatisfiable(Map> matches) { val start = System.nanoTime var boolean finalResult - if(matches.empty){ - finalResult=true - } else { - val propagatedConstraints = new HashMap - for(entry : matches.entrySet) { - val constraint = entry.key - //println(constraint) - val allMatches = entry.value.allMatches.map[it.toArray] - //println(allMatches.toList) - propagatedConstraints.put(constraint,allMatches) - } - if(propagatedConstraints.values.forall[empty]) { + if(intermediateConsistencyCheck) { + if(matches.empty){ finalResult=true } else { - if(caching) { - val code = getCode(propagatedConstraints) - val cachedResult = satisfiabilityCache.get(code) - if(cachedResult === null) { - // println('''new problem, call solver''') - // for(entry : code.entrySet) { - // println('''«entry.key» -> «entry.value»''') - // } - //println(code.hashCode) - this.numberOfSolverCalls++ - val res = t.delegateIsSatisfiable(propagatedConstraints) - satisfiabilityCache.put(code,res) - finalResult=res + val propagatedConstraints = new HashMap + for(entry : matches.entrySet) { + val constraint = entry.key + //println(constraint) + val allMatches = entry.value.allMatches.map[it.toArray] + //println(allMatches.toList) + propagatedConstraints.put(constraint,allMatches) + } + if(propagatedConstraints.values.forall[empty]) { + finalResult=true + } else { + if(caching) { + val code = getCode(propagatedConstraints) + val cachedResult = satisfiabilityCache.get(code) + if(cachedResult === null) { + // println('''new problem, call solver''') + // for(entry : code.entrySet) { + // println('''«entry.key» -> «entry.value»''') + // } + //println(code.hashCode) + this.numberOfSolverCalls++ + val res = t.delegateIsSatisfiable(propagatedConstraints) + satisfiabilityCache.put(code,res) + finalResult=res + } else { + //println('''similar problem, answer from cache''') + finalResult=cachedResult + this.numberOfCachedSolverCalls++ + } } else { - //println('''similar problem, answer from cache''') - finalResult=cachedResult - this.numberOfCachedSolverCalls++ + finalResult= t.delegateIsSatisfiable(propagatedConstraints) + this.numberOfSolverCalls++ } - } else { - finalResult= t.delegateIsSatisfiable(propagatedConstraints) - this.numberOfSolverCalls++ } } - } + } else { + finalResult = true + } this.runtime+=System.nanoTime-start return finalResult } -- cgit v1.2.3-70-g09d2 From d03c841f2e4114a442deb08946c391c823745953 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Sun, 17 May 2020 01:35:57 +0200 Subject: detailed runtimes + counting defined objects only --- .../logic2viatra/ScopePropagator.xtend | 67 ++++++++++++---------- .../viatrasolver/reasoner/ViatraReasoner.xtend | 8 ++- .../dse/BestFirstStrategyForModelGeneration.java | 35 ++++++++--- .../dse/ModelGenerationCompositeObjective.xtend | 15 +++-- 4 files changed, 81 insertions(+), 44 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend index abfa4554..8012776f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend @@ -8,6 +8,7 @@ import java.util.Map import java.util.Set import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation import java.util.HashSet +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation class ScopePropagator { PartialInterpretation partialInterpretation @@ -61,38 +62,42 @@ class ScopePropagator { } def public propagateAdditionToType(PartialTypeInterpratation t) { -// println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') - val targetScope = type2Scope.get(t) - if(targetScope!==null) { - targetScope.removeOne - val sups = superScopes.get(targetScope) - sups.forEach[removeOne] - } - - if(this.partialInterpretation.minNewElements > 0) { - this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1 - } - if(this.partialInterpretation.maxNewElements > 0) { - this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1 - } else if(this.partialInterpretation.maxNewElements === 0) { - this.partialInterpretation.maxNewElements = 0 - //throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') + val isPrimitive = t instanceof PartialPrimitiveInterpretation || t === null + if(!isPrimitive) { + // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') + val targetScope = type2Scope.get(t) + if(targetScope!==null) { + targetScope.removeOne + val sups = superScopes.get(targetScope) + sups.forEach[removeOne] + } + + + if(this.partialInterpretation.minNewElements > 0 ) { + this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1 + } + if(this.partialInterpretation.maxNewElements > 0) { + this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1 + } else if(this.partialInterpretation.maxNewElements === 0) { + this.partialInterpretation.maxNewElements = 0 + //throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') + } + + // subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)] + // for(sup: sups) { + // subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)] + // } + // for(scope : type2Scope.values) { + // propagateUpperLimitDown(scope,partialInterpretation) + // } + + propagateAllScopeConstraints + + // println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') + // println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') + // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] + // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') } - -// subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)] -// for(sup: sups) { -// subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)] -// } -// for(scope : type2Scope.values) { -// propagateUpperLimitDown(scope,partialInterpretation) -// } - - propagateAllScopeConstraints - -// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') -// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') -// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] -// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') } private def propagateLowerLimitUp(Scope subScope, Scope superScope) { 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 1fe65afe..5df28edd 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 @@ -137,10 +137,16 @@ class ViatraReasoner extends LogicReasoner{ it.transformationTime = (transformationTime/1000000) as int for(x : 0.. [ - it.name = '''_Solution«x»FoundAt''' + it.name = '''Solution«x+1»FoundAt''' it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int ] } + for(x: 0.. [ + it.name = '''Solution«x+1»DetailedStatistics''' + it.value = strategy.times.get(x) + ] + } it.entries += createIntStatisticEntry => [ it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int ] 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 75ce7f10..710996a9 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 @@ -44,6 +44,7 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver; import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; @@ -112,7 +113,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { public int getNumberOfStatecoderFail() { return numberOfStatecoderFail; } - + //LinkedList> matchers; @Override public void initStrategy(ThreadContext context) { this.context = context; @@ -120,7 +121,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // ViatraQueryEngine engine = context.getQueryEngine(); // // TODO: visualisation -// LinkedList> matchers = new LinkedList>(); +// matchers = new LinkedList>(); // for(IQuerySpecification> p : this.method.getAllPatterns()) { // //System.out.println(p.getSimpleName()); // ViatraQueryMatcher matcher = p.getMatcher(engine); @@ -213,12 +214,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { visualiseCurrentState(); // for(ViatraQueryMatcher matcher : matchers) { -// System.out.println(matcher.getPatternName()); -// System.out.println("---------"); -// for(IPatternMatch m : matcher.getAllMatches()) { -// System.out.println(m); +// int c = matcher.countMatches(); +// if(c>=100) { +// System.out.println(c+ " " +matcher.getPatternName()); // } -// System.out.println("---------"); +// // } boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); @@ -292,12 +292,31 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { solutionStoreWithDiversityDescriptor.newSolution(context); solutionStore.newSolution(context); configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); - + saveTimes(); logger.debug("Found a solution."); } } } } + public List times = new LinkedList(); + private void saveTimes() { + long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder)this.context.getStateCoder()).getStatecoderRuntime()/1000000; + long solutionCopy = solutionStoreWithCopy.getSumRuntime()/1000000; + long activationSelection = this.activationSelector.getRuntime()/1000000; + long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000; + long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000; + long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000; + long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000; + this.times.add( + "(StateCoderTime:"+statecoderTime+ + "|SolutionCopyTime:"+solutionCopy+ + "|ActivationSelectionTime:"+activationSelection+ + "|NumericalSolverSumTime:"+numericalSolverSumTime+ + "|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+ + "|NumericalSolverSolvingTime:"+numericalSolverSolving+ + "|NumericalSolverInterpretingSolution:"+numericalSolverInterpreting+")"); + + } @Override public void interruptStrategy() { 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 e75cae41..2a4294ad 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 @@ -6,6 +6,7 @@ import org.eclipse.viatra.dse.base.ThreadContext import org.eclipse.viatra.dse.objectives.Comparators import org.eclipse.viatra.dse.objectives.IObjective import org.eclipse.viatra.dse.objectives.impl.BaseObjective +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation //class ViatraReasonerNumbers { // public static val scopePriority = 2 @@ -26,6 +27,7 @@ class ModelGenerationCompositeObjective implements IObjective{ val ScopeObjective scopeObjective val List unfinishedMultiplicityObjectives val UnfinishedWFObjective unfinishedWFObjective + var PartialInterpretation model=null; public new( ScopeObjective scopeObjective, @@ -38,6 +40,7 @@ class ModelGenerationCompositeObjective implements IObjective{ } override init(ThreadContext context) { + model = context.model as PartialInterpretation this.scopeObjective.init(context) this.unfinishedMultiplicityObjectives.forEach[it.init(context)] this.unfinishedWFObjective.init(context) @@ -64,11 +67,15 @@ class ModelGenerationCompositeObjective implements IObjective{ nonContainmentMultiplicity+=multiplicityObjective.getFitness(context) } } + val size = 0.9/model.newElements.size var sum = 0.0 sum += scopeFitnes - sum += containmentMultiplicity - sum += Math.sqrt(nonContainmentMultiplicity) - sum += unfinishedWFsFitness//*0.5 + sum += containmentMultiplicity*2 + sum += nonContainmentMultiplicity + sum += unfinishedWFsFitness + sum+=size + + //println('''Sum=«sum»|Scope=«scopeFitnes»|ContainmentMultiplicity=«containmentMultiplicity»|NonContainmentMultiplicity=«nonContainmentMultiplicity»|WFs=«unfinishedWFsFitness»''') @@ -79,7 +86,7 @@ class ModelGenerationCompositeObjective implements IObjective{ override getName() { "CompositeUnfinishednessObjective"} override isHardObjective() { true } - override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } + override satisifiesHardObjective(Double fitness) { fitness < 0.95 } override setComparator(Comparator comparator) { -- cgit v1.2.3-70-g09d2 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') 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-70-g09d2