From b217dfc7e7bd7beb73c8cc23ad82383309ceb697 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 18 Jul 2019 15:21:56 +0200 Subject: Implement Coin-OR CBC polyhedron saturation operator --- .../hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath (limited to 'Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath') diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath new file mode 100644 index 00000000..e19039ae --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath @@ -0,0 +1,15 @@ + + + + + + + + + + + + + + + -- cgit v1.2.3-70-g09d2 From 957082776dbb7efed53a783c5e5be6b443a9bb86 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sat, 27 Jun 2020 17:56:46 +0200 Subject: Fix scope + numerical propagation WIP --- .../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes .../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes .../.SolverSemanticHighlightCalculator.xtendbin | Bin 5334 -> 5334 bytes .../.SolverSemanticTextAttributeProvider.xtendbin | Bin 4902 -> 4902 bytes .../validation/.SolverLanguageValidator.xtendbin | Bin 1717 -> 1717 bytes ....SolverLanguageTokenDefInjectingParser.xtendbin | Bin 2742 -> 2742 bytes ...nguageSyntheticTokenSyntacticSequencer.xtendbin | Bin 2758 -> 2758 bytes .../hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath | 6 +- .../.settings/org.eclipse.jdt.core.prefs | 8 ++ .../lib/libviatracbc.so | Bin 33944 -> 46416 bytes .../MultiplicityGoalConstraintCalculator.xtend | 15 +-- .../cardinality/PolyhedronScopePropagator.xtend | 8 +- .../logic2viatra/cardinality/ScopePropagator.xtend | 14 +- .../rules/GoalConstraintProvider.xtend | 3 +- .../rules/RefinementRuleProvider.xtend | 150 ++++++++++++--------- .../PartialInterpretationInitialiser.xtend | 29 ++-- .../reasoner/ViatraReasonerConfiguration.xtend | 5 +- .../dse/BestFirstStrategyForModelGeneration.java | 22 +-- .../dse/ModelGenerationCompositeObjective.xtend | 2 +- .../viatrasolver/reasoner/dse/ScopeObjective.xtend | 2 +- .../case.study.familyTree.run/bin/.gitignore | 1 - .../inputs/SatelliteInstance.xmi | 2 +- .../src/run/RunGeneratorConfig.xtend | 6 +- 23 files changed, 136 insertions(+), 137 deletions(-) create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs delete mode 100644 Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore (limited to 'Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath') diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin index b5a7c99c..94c786eb 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin index 9274eee0..46ab9b95 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin index 8e8e8c70..27dc1dd4 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin index 741776d1..d71f4f21 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin index 73356e7f..801783da 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin index 24f61d80..30c2ff9e 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin index eae3bd77..261f466c 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin differ diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath index e19039ae..93829d26 100644 --- a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath @@ -1,10 +1,6 @@ - - - - - + diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..9f6ece88 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,8 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.release=disabled +org.eclipse.jdt.core.compiler.source=1.8 diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so index 96289216..ba3cdc06 100755 Binary files a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so and b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so differ diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend index 034420d6..b28cd584 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend @@ -10,15 +10,13 @@ class MultiplicityGoalConstraintCalculator { val String targetRelationName val IQuerySpecification querySpecification var ViatraQueryMatcher matcher - val int minValue val boolean containment val int cost - public new(String targetRelationName, IQuerySpecification querySpecification, int minValue, boolean containment, int cost) { + public new(String targetRelationName, IQuerySpecification querySpecification, boolean containment, int cost) { this.targetRelationName = targetRelationName this.querySpecification = querySpecification this.matcher = null - this.minValue = minValue this.containment = containment this.cost = cost } @@ -27,7 +25,6 @@ class MultiplicityGoalConstraintCalculator { this.targetRelationName = other.targetRelationName this.querySpecification = other.querySpecification this.matcher = null - this.minValue = other.minValue this.containment = other.containment this.cost = other.cost } @@ -49,14 +46,8 @@ class MultiplicityGoalConstraintCalculator { var res = 0 val allMatches = this.matcher.allMatches for(match : allMatches) { - val existingMultiplicity = match.get(4) as Integer - if(existingMultiplicity < this.minValue) { - val missingMultiplicity = this.minValue-existingMultiplicity - res += missingMultiplicity - } -// if(missingMultiplicity!=0) { -// println(targetRelationName+ " missing multiplicity: "+missingMultiplicity) -// } + val missingMultiplicity = match.get(2) as Integer + res += missingMultiplicity } // if(res>0) // println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost) diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index 120fb18a..9b4dff0f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend @@ -88,6 +88,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { val result = operator.saturate() if (result == PolyhedronSaturationResult.EMPTY) { cache.put(signature, PolyhedronSignature.EMPTY) +// println("INVALID") setScopesInvalid() } else { val resultSignature = polyhedron.createSignature @@ -110,11 +111,8 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } } - override propagateAdditionToRelation(Relation r) { - super.propagateAdditionToRelation(r) - if (relevantRelations.contains(r)) { - propagateAllScopeConstraints() - } + override isPropagationNeededAfterAdditionToRelation(Relation r) { + relevantRelations.contains(r) || super.isPropagationNeededAfterAdditionToRelation(r) } def resetBounds() { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend index 8f3a5bb0..8350c7f4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend @@ -114,21 +114,21 @@ class ScopePropagator { } } - def void propagateAdditionToRelation(Relation r) { - // Nothing to propagate. + def isPropagationNeededAfterAdditionToRelation(Relation r) { + false } private def removeOne(Scope scope) { - if (scope.maxNewElements === 0) { - throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') - } else if (scope.maxNewElements > 0) { - scope.maxNewElements = scope.maxNewElements - 1 - } if (scope.minNewElements > 0) { scope.minNewElements = scope.minNewElements - 1 } if (scope.minNewElementsHeuristic > 0) { scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1 } + if (scope.maxNewElements > 0) { + scope.maxNewElements = scope.maxNewElements - 1 + } else if (scope.maxNewElements === 0) { + setScopesInvalid() + } } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index 238ade5b..d2ee80dc 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -15,9 +15,8 @@ class GoalConstraintProvider { val queries = entry.value val targetRelationName = constraint.relation.name val query = queries.unfinishedMultiplicityQuery - val minValue = constraint.lowerBound val containment = constraint.containment - res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, minValue, containment, 1) + res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, containment, 1) } } return res diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index 0b8a9019..863ee18b 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend @@ -32,9 +32,12 @@ import java.util.LinkedHashMap import java.util.LinkedList import java.util.List import java.util.Map +import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine import org.eclipse.viatra.query.runtime.api.GenericPatternMatch import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.emf.EMFScope import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory import org.eclipse.xtend.lib.annotations.Data @@ -45,6 +48,8 @@ class RefinementRuleProvider { val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE + var AdvancedViatraQueryEngine queryEngine + def canonizeName(String name) { return name.replace(' ','_') } @@ -60,6 +65,7 @@ class RefinementRuleProvider { { val res = new LinkedHashMap val recursiveObjectCreation = recursiveObjectCreation(p,i) + queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine for(LHSEntry: patterns.refineObjectQueries.entrySet) { val containmentRelation = LHSEntry.key.containmentRelation val inverseRelation = LHSEntry.key.inverseContainment @@ -90,8 +96,7 @@ class RefinementRuleProvider { if(inverseRelation!== null) { ruleBuilder.action[match | statistics.incrementTransformationCount -// println(name) - val startTime = System.nanoTime +// println(name) //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation @@ -99,79 +104,89 @@ class RefinementRuleProvider { val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation val container = match.get(5) as DefinedElement - createObjectActionWithContainmentAndInverse( - nameNewElement, - interpretation, - typeInterpretation, - container, - relationInterpretation, - inverseRelationInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createObjectActionWithContainmentAndInverse( + nameNewElement, + interpretation, + typeInterpretation, + container, + relationInterpretation, + inverseRelationInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] ] } else { ruleBuilder.action[match | statistics.incrementTransformationCount // println(name) - val startTime = System.nanoTime //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation val container = match.get(4) as DefinedElement - createObjectActionWithContainment( - nameNewElement, - interpretation, - typeInterpretation, - container, - relationInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createObjectActionWithContainment( + nameNewElement, + interpretation, + typeInterpretation, + container, + relationInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] ] } } else { ruleBuilder.action[match | statistics.incrementTransformationCount // println(name) - val startTime = System.nanoTime //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation - createObjectAction( - nameNewElement, - interpretation, - typeInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createObjectAction( + nameNewElement, + interpretation, + typeInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] ] } return ruleBuilder.build @@ -342,7 +357,7 @@ class RefinementRuleProvider { if (inverseRelation === null) { ruleBuilder.action [ match | statistics.incrementTransformationCount - val startTime = System.nanoTime + // println(name) // val problem = match.get(0) as LogicProblem // val interpretation = match.get(1) as PartialInterpretation @@ -350,19 +365,24 @@ class RefinementRuleProvider { val src = match.get(3) as DefinedElement val trg = match.get(4) as DefinedElement - createRelationLinkAction(src, trg, relationInterpretation) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createRelationLinkAction(src, trg, relationInterpretation) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAdditionToRelation(declaration) - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] + } ] } else { ruleBuilder.action [ match | statistics.incrementTransformationCount - val startTime = System.nanoTime // println(name) // val problem = match.get(0) as LogicProblem // val interpretation = match.get(1) as PartialInterpretation @@ -371,14 +391,20 @@ class RefinementRuleProvider { val src = match.get(4) as DefinedElement val trg = match.get(5) as DefinedElement - createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAdditionToRelation(declaration) - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] + } ] } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend index d37acb6d..20ff58f2 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend @@ -2,19 +2,24 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStar import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.PartialModelRelation2Assertion -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.NaryRelationLink import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation @@ -22,10 +27,10 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.UnaryElementRelationLink import java.math.BigDecimal import java.util.HashMap import java.util.Map @@ -35,14 +40,6 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope import org.eclipse.xtend.lib.annotations.Data import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition @Data class Problem2PartialInterpretationTrace { Map type2Interpretation @@ -194,7 +191,7 @@ class PartialInterpretationInitialiser { interpretation.minNewElements = minNewElements interpretation.maxNewElements = maxNewElements // elements from problem are included - if(maxNewElements>0) { + if(maxNewElements != 0) { val newElements = createDefinedElement => [it.name = "New Objects"] interpretation.openWorldElements += newElements } @@ -213,12 +210,8 @@ class PartialInterpretationInitialiser { def private initialiseTypeScope(PartialTypeInterpratation interpretation, Integer min, Integer max) { val res = createScope res.targetTypeInterpretation = interpretation - if(min !== null) { - res.minNewElements = min - } - if(max !== null) { - res.maxNewElements = max - } + res.minNewElements = min ?: 0 + res.maxNewElements = max ?: -1 return res } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index ddd25aac..e33a2590 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend @@ -58,13 +58,14 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { public var runIntermediateNumericalConsistencyChecks = true public var punishSize = true - public var scopeWeight = 1 - public var conaintmentWeight = 2 + public var scopeWeight = 2 + public var conaintmentWeight = 1 public var nonContainmentWeight = 1 public var unfinishedWFWeight = 1 public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) +// public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.BasicTypeHierarchy public var List hints = newArrayList diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index e529892c..09575384 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java @@ -18,6 +18,7 @@ import java.util.List; import java.util.PriorityQueue; import java.util.Random; +import org.apache.log4j.Level; import org.apache.log4j.Logger; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.util.EcoreUtil; @@ -76,7 +77,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { private volatile boolean isInterrupted = false; private ModelResult modelResultByInternalSolver = null; private Random random = new Random(); - //private Collection> matchers; +// private Collection> matchers; public ActivationSelector activationSelector = new EvenActivationSelector(random); public ViatraReasonerSolutionSaver solutionSaver; public NumericSolver numericSolver; @@ -100,7 +101,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { this.method = method; this.solutionSaver = solutionSaver; this.numericSolver = numericSolver; - //logger.setLevel(Level.DEBUG); +// logger.setLevel(Level.DEBUG); } public int getNumberOfStatecoderFail() { @@ -136,7 +137,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // ViatraQueryEngine engine = context.getQueryEngine(); // matchers = new LinkedList>(); // for(IQuerySpecification> p : this.method.getAllPatterns()) { -// //System.out.println(p.getSimpleName()); // ViatraQueryMatcher matcher = p.getMatcher(engine); // matchers.add(matcher); // } @@ -154,13 +154,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { @Override public void explore() { -// System.out.println("press enter"); -// try { -// new BufferedReader(new InputStreamReader(System.in)).readLine(); -// } catch (IOException e) { -// // TODO Auto-generated catch block -// e.printStackTrace(); -// } this.explorationStarted=System.nanoTime(); if (!checkGlobalConstraints()) { logger.info("Global contraint is not satisifed in the first state. Terminate."); @@ -219,10 +212,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { while (!isInterrupted && !configuration.progressMonitor.isCancelled() && iterator.hasNext()) { final Object nextActivation = iterator.next(); -// if (!iterator.hasNext()) { -// logger.debug("Last untraversed activation of the state."); -// trajectoiresToExplore.remove(currentTrajectoryWithfitness); -// } logger.debug("Executing new activation: " + nextActivation); context.executeAcitvationId(nextActivation); method.getStatistics().incrementDecisionCount(); @@ -230,10 +219,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { visualiseCurrentState(); // for(ViatraQueryMatcher matcher : matchers) { // int c = matcher.countMatches(); -// if(c>=100) { +// if(c>=1) { // System.out.println(c+ " " +matcher.getPatternName()); -// } -// +// } // } boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness); diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend index d2faaa65..481f4ce1 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend @@ -112,7 +112,7 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective { override isHardObjective() { true } - override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } + override satisifiesHardObjective(Double fitness) { fitness <= 0.9 } override setComparator(Comparator comparator) { throw new UnsupportedOperationException("Model generation objective comparator cannot be set.") diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend index 69a734f8..7abc5cb8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend @@ -25,7 +25,7 @@ class ScopeObjective implements IObjective{ val interpretation = context.model as PartialInterpretation var res = interpretation.minNewElementsHeuristic.doubleValue for(scope : interpretation.scopes) { - res += scope.minNewElementsHeuristic*2 + res += scope.minNewElementsHeuristic } return res } diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore deleted file mode 100644 index 7050a7e3..00000000 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/queries/ diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi index 3d07a199..66512878 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi @@ -4,4 +4,4 @@ xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:satellite="http://www.example.org/satellite" - xsi:schemaLocation="http://www.example.org/satellite ../model/satellite.ecore"/> + xsi:schemaLocation="http://www.example.org/satellite ../../hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"/> diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend index 20eed2e2..e4d6fe9f 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend @@ -12,7 +12,9 @@ import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.RuntimeEn import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ScopeSpecification import hu.bme.mit.inf.dslreasoner.application.execution.ScriptExecutor import hu.bme.mit.inf.dslreasoner.application.execution.StandaloneScriptExecutor +import hu.bme.mit.inf.dslreasoner.application.execution.StandardOutputBasedScriptConsole import java.io.File +import java.io.PrintWriter import java.text.SimpleDateFormat import java.util.Date import org.apache.commons.cli.BasicParser @@ -23,8 +25,6 @@ import org.apache.commons.cli.Option import org.apache.commons.cli.Options import org.apache.commons.cli.ParseException import org.eclipse.core.runtime.NullProgressMonitor -import com.google.common.io.Files -import java.io.PrintWriter class RunGeneratorConfig { static var SIZE_LB = 20 @@ -102,7 +102,7 @@ class RunGeneratorConfig { val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm") val formattedDate = format.format(date) - val executor = new ScriptExecutor + val executor = new ScriptExecutor(StandardOutputBasedScriptConsole.FACTORY) val path = "config//generic" + DOMAIN + ".vsconfig" var ConfigurationScript config = StandaloneScriptExecutor.loadScript(path) -- cgit v1.2.3-70-g09d2