aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml28
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend85
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend10
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend4
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend24
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF3
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend227
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend44
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java70
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend184
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend66
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend24
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend78
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend74
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend52
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend120
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend29
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend137
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend45
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend102
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend10
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java36
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend85
25 files changed, 1106 insertions, 435 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml
index 05e00983..6e4d96ca 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/plugin.xml
@@ -1,14 +1,14 @@
1<?xml version="1.0" encoding="UTF-8"?><plugin> 1<?xml version="1.0" encoding="UTF-8"?><plugin>
2 <extension id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" point="org.eclipse.viatra.query.runtime.queryspecification"> 2 <extension id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" point="org.eclipse.viatra.query.runtime.queryspecification">
3 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis"> 3 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis" id="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.TypeAnalysis">
4 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.hasDefinedSupertype"/> 4 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.hasDefinedSupertype"/>
5 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.dontHaveDefinedSupertype"/> 5 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.dontHaveDefinedSupertype"/>
6 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeConstructor"/> 6 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeConstructor"/>
7 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementTarget"/> 7 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementTarget"/>
8 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleSuperType"/> 8 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleSuperType"/>
9 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleTopType"/> 9 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.incompatibleTopType"/>
10 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementNegativeConstraint"/> 10 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementTypeRefinementNegativeConstraint"/>
11 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementMayTypeNegativeConstraint"/> 11 <query-specification fqn="hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.newElementMayTypeNegativeConstraint"/>
12 </group> 12 </group>
13 </extension> 13 </extension>
14</plugin> 14</plugin>
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 f43ab96d..b6918294 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
@@ -1,8 +1,10 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
2 2
3import com.google.common.collect.ImmutableMap
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel 4import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
4import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 5import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
5import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery 6import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider 8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider 9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider 10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider
@@ -10,6 +12,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
10import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 12import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
11import java.util.Collection 13import java.util.Collection
12import java.util.List 14import java.util.List
15import java.util.Map
13import java.util.Set 16import java.util.Set
14import org.eclipse.viatra.query.runtime.api.IPatternMatch 17import org.eclipse.viatra.query.runtime.api.IPatternMatch
15import org.eclipse.viatra.query.runtime.api.IQuerySpecification 18import org.eclipse.viatra.query.runtime.api.IQuerySpecification
@@ -20,34 +23,41 @@ import org.eclipse.xtend.lib.annotations.Data
20 23
21class ModelGenerationStatistics { 24class ModelGenerationStatistics {
22 public var long transformationExecutionTime = 0 25 public var long transformationExecutionTime = 0
26
23 synchronized def addExecutionTime(long amount) { 27 synchronized def addExecutionTime(long amount) {
24 transformationExecutionTime+=amount 28 transformationExecutionTime += amount
25 } 29 }
30
26 public var long PreliminaryTypeAnalisisTime = 0 31 public var long PreliminaryTypeAnalisisTime = 0
27} 32}
33
28@Data class ModelGenerationMethod { 34@Data class ModelGenerationMethod {
29 ModelGenerationStatistics statistics 35 ModelGenerationStatistics statistics
30 36
31 Collection<? extends BatchTransformationRule<?,?>> objectRefinementRules 37 Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules
32 Collection<? extends BatchTransformationRule<?,?>> relationRefinementRules 38 Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules
33 39
34 List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities 40 List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities
35 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF 41 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF
36 42
37 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF 43 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
38 44
39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns 45 Map<String, ModalPatternQueries> modalRelationQueries
46
47 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
40} 48}
49
41enum TypeInferenceMethod { 50enum TypeInferenceMethod {
42 Generic, PreliminaryAnalysis 51 Generic,
52 PreliminaryAnalysis
43} 53}
44 54
45class ModelGenerationMethodProvider { 55class ModelGenerationMethodProvider {
46 private val PatternProvider patternProvider = new PatternProvider 56 val PatternProvider patternProvider = new PatternProvider
47 private val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider 57 val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider
48 private val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider 58 val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider
49 59
50 public def ModelGenerationMethod createModelGenerationMethod( 60 def ModelGenerationMethod createModelGenerationMethod(
51 LogicProblem logicProblem, 61 LogicProblem logicProblem,
52 PartialInterpretation emptySolution, 62 PartialInterpretation emptySolution,
53 ReasonerWorkspace workspace, 63 ReasonerWorkspace workspace,
@@ -58,25 +68,31 @@ class ModelGenerationMethodProvider {
58 ) { 68 ) {
59 val statistics = new ModelGenerationStatistics 69 val statistics = new ModelGenerationStatistics
60 val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) 70 val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL)
61 71
62 val Set<PQuery> existingQueries = logicProblem 72 val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery).
63 .relations 73 map[it.patternPQuery as PQuery].toSet
64 .map[annotations] 74
65 .flatten 75 val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries,
66 .filter(TransfomedViatraQuery) 76 workspace, typeInferenceMethod, writeFiles)
67 .map[it.patternPQuery as PQuery] 77 val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>>
68 .toSet 78 objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator,
69 79 nameNewElements, statistics)
70 val queries = patternProvider.generateQueries(logicProblem,emptySolution,statistics,existingQueries,workspace,typeInferenceMethod,writeFiles) 80 val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, statistics)
71 val //LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> 81
72 objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries,scopePropagator,nameNewElements,statistics)
73 val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics)
74
75 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) 82 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries)
76 val unfinishedWF = queries.getUnfinishedWFQueries.values 83 val unfinishedWF = queries.getUnfinishedWFQueries.values
77 84
85 val modalRelationQueriesBuilder = ImmutableMap.builder
86 for (entry : queries.modalRelationQueries.entrySet) {
87 val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head
88 if (annotation !== null) {
89 modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value)
90 }
91 }
92 val modalRelationQueries = modalRelationQueriesBuilder.build
93
78 val invalidWF = queries.getInvalidWFQueries.values 94 val invalidWF = queries.getInvalidWFQueries.values
79 95
80 return new ModelGenerationMethod( 96 return new ModelGenerationMethod(
81 statistics, 97 statistics,
82 objectRefinementRules.values, 98 objectRefinementRules.values,
@@ -84,6 +100,7 @@ class ModelGenerationMethodProvider {
84 unfinishedMultiplicities, 100 unfinishedMultiplicities,
85 unfinishedWF, 101 unfinishedWF,
86 invalidWF, 102 invalidWF,
103 modalRelationQueries,
87 queries.allQueries 104 queries.allQueries
88 ) 105 )
89 } 106 }
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..4b9629df 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
@@ -11,28 +11,28 @@ class MultiplicityGoalConstraintCalculator {
11 val IQuerySpecification<?> querySpecification; 11 val IQuerySpecification<?> querySpecification;
12 var ViatraQueryMatcher<?> matcher; 12 var ViatraQueryMatcher<?> matcher;
13 13
14 public new(String targetRelationName, IQuerySpecification<?> querySpecification) { 14 new(String targetRelationName, IQuerySpecification<?> querySpecification) {
15 this.targetRelationName = targetRelationName 15 this.targetRelationName = targetRelationName
16 this.querySpecification = querySpecification 16 this.querySpecification = querySpecification
17 this.matcher = null 17 this.matcher = null
18 } 18 }
19 19
20 public new(MultiplicityGoalConstraintCalculator other) { 20 new(MultiplicityGoalConstraintCalculator other) {
21 this.targetRelationName = other.targetRelationName 21 this.targetRelationName = other.targetRelationName
22 this.querySpecification = other.querySpecification 22 this.querySpecification = other.querySpecification
23 this.matcher = null 23 this.matcher = null
24 } 24 }
25 25
26 def public getName() { 26 def getName() {
27 targetRelationName 27 targetRelationName
28 } 28 }
29 29
30 def public init(Notifier notifier) { 30 def init(Notifier notifier) {
31 val engine = ViatraQueryEngine.on(new EMFScope(notifier)) 31 val engine = ViatraQueryEngine.on(new EMFScope(notifier))
32 matcher = querySpecification.getMatcher(engine) 32 matcher = querySpecification.getMatcher(engine)
33 } 33 }
34 34
35 def public calculateValue() { 35 def calculateValue() {
36 var res = 0 36 var res = 0
37 val allMatches = this.matcher.allMatches 37 val allMatches = this.matcher.allMatches
38 for(match : allMatches) { 38 for(match : allMatches) {
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 d4c76bb4..24b3e870 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
@@ -55,7 +55,7 @@ class PatternGenerator {
55 typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis 55 typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis
56 } 56 }
57 57
58 public dispatch def referRelation( 58 public dispatch def CharSequence referRelation(
59 RelationDeclaration referred, 59 RelationDeclaration referred,
60 String sourceVariable, 60 String sourceVariable,
61 String targetVariable, 61 String targetVariable,
@@ -64,7 +64,7 @@ class PatternGenerator {
64 { 64 {
65 return this.relationDeclarationIndexer.referRelation(referred,sourceVariable,targetVariable,modality) 65 return this.relationDeclarationIndexer.referRelation(referred,sourceVariable,targetVariable,modality)
66 } 66 }
67 public dispatch def referRelation( 67 public dispatch def CharSequence referRelation(
68 RelationDefinition referred, 68 RelationDefinition referred,
69 String sourceVariable, 69 String sourceVariable,
70 String targetVariable, 70 String targetVariable,
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 0e13a5e1..e87f52af 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
@@ -2,8 +2,10 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2 2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation 3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration 4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 7import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics 9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis 10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult 11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
@@ -11,7 +13,9 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil 13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
13import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 15import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
16import java.util.Collection
14import java.util.Map 17import java.util.Map
18import java.util.Set
15import org.eclipse.viatra.query.runtime.api.IPatternMatch 19import org.eclipse.viatra.query.runtime.api.IPatternMatch
16import org.eclipse.viatra.query.runtime.api.IQuerySpecification 20import org.eclipse.viatra.query.runtime.api.IQuerySpecification
17import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 21import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
@@ -19,8 +23,6 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
19import org.eclipse.xtend.lib.annotations.Data 23import org.eclipse.xtend.lib.annotations.Data
20 24
21import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 25import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
22import java.util.Collection
23import java.util.Set
24 26
25@Data class GeneratedPatterns { 27@Data class GeneratedPatterns {
26 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries 28 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries
@@ -29,9 +31,16 @@ import java.util.Set
29 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries 31 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries
30 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries 32 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries
31 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries 33 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries
34 public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries
32 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries 35 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries
33} 36}
34 37
38@Data class ModalPatternQueries {
39 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayQuery
40 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustQuery
41 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentQuery
42}
43
35class PatternProvider { 44class PatternProvider {
36 45
37 val TypeAnalysis typeAnalysis = new TypeAnalysis 46 val TypeAnalysis typeAnalysis = new TypeAnalysis
@@ -71,7 +80,7 @@ class PatternProvider {
71 LogicProblem problem, 80 LogicProblem problem,
72 PartialInterpretation emptySolution, 81 PartialInterpretation emptySolution,
73 TypeAnalysisResult typeAnalysisResult, 82 TypeAnalysisResult typeAnalysisResult,
74 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries 83 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries
75 ) { 84 ) {
76 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 85 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
77 invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] 86 invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]
@@ -85,6 +94,14 @@ class PatternProvider {
85 refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] 94 refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]
86 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 95 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
87 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] 96 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]
97 val Map<RelationDefinition, ModalPatternQueries> modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition |
98 val indexer = patternGenerator.relationDefinitionIndexer
99 new ModalPatternQueries(
100 indexer.relationDefinitionName(relationDefinition, Modality.MAY).lookup(queries),
101 indexer.relationDefinitionName(relationDefinition, Modality.MUST).lookup(queries),
102 indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries)
103 )
104 ])
88 return new GeneratedPatterns( 105 return new GeneratedPatterns(
89 invalidWFQueries, 106 invalidWFQueries,
90 unfinishedWFQueries, 107 unfinishedWFQueries,
@@ -92,6 +109,7 @@ class PatternProvider {
92 refineObjectsQueries, 109 refineObjectsQueries,
93 refineTypeQueries, 110 refineTypeQueries,
94 refineRelationQueries, 111 refineRelationQueries,
112 modalRelationQueries,
95 queries.values 113 queries.values
96 ) 114 )
97 } 115 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
index 9723373f..cedcec5a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
@@ -71,7 +71,7 @@ class RelationDefinitionIndexer {
71 ] 71 ]
72 } 72 }
73 73
74 private def relationDefinitionName(RelationDefinition relation, Modality modality) 74 def String relationDefinitionName(RelationDefinition relation, Modality modality)
75 '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' 75 '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»'''
76 76
77 private def canonizeName(PVariable v) { 77 private def canonizeName(PVariable v) {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
index 2a271acf..4ad61ccb 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
@@ -3,7 +3,8 @@ Bundle-ManifestVersion: 2
3Bundle-Name: Reasoner 3Bundle-Name: Reasoner
4Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner 4Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
5Bundle-Version: 1.0.0.qualifier 5Bundle-Version: 1.0.0.qualifier
6Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner 6Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner,
7 hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
7Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", 8Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
8 hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", 9 hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
9 hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", 10 hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0",
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 6639e5f3..edcca676 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
@@ -1,5 +1,7 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
2 2
3import com.google.common.collect.ImmutableList
4import com.google.common.collect.Lists
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel 5import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
4import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner 6import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException 7import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
@@ -17,12 +19,17 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory 19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory 20import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory
19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration 21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration
22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler
20import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective 24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective
21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation 25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation
22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective 26import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective
27import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective 28import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedWFObjective 29import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver
25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter 30import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter
31import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement
32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective
26import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 33import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
27import java.util.List 34import java.util.List
28import java.util.Map 35import java.util.Map
@@ -31,44 +38,41 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer
31import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel 38import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel
32import org.eclipse.viatra.dse.solutionstore.SolutionStore 39import org.eclipse.viatra.dse.solutionstore.SolutionStore
33import org.eclipse.viatra.dse.statecode.IStateCoderFactory 40import org.eclipse.viatra.dse.statecode.IStateCoderFactory
34import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SolutionStoreWithDiversityDescriptor
35import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityGranularity
36 41
37class ViatraReasoner extends LogicReasoner{ 42class ViatraReasoner extends LogicReasoner {
38 val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() 43 val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()
39 val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider 44 val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider
40 val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE 45 val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE
41 val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter 46 val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter
42 47
43 48 override solve(LogicProblem problem, LogicSolverConfiguration configuration,
44 override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { 49 ReasonerWorkspace workspace) throws LogicReasonerException {
45 val viatraConfig = configuration.asConfig 50 val viatraConfig = configuration.asConfig
46 51
47 if(viatraConfig.debugCongiguration.logging) { 52 if (viatraConfig.debugConfiguration.logging) {
48 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL) 53 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL)
49 } else { 54 } else {
50 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN) 55 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN)
51 } 56 }
52 57
53 val DesignSpaceExplorer dse = new DesignSpaceExplorer(); 58 val DesignSpaceExplorer dse = new DesignSpaceExplorer();
54 59
55 dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE) 60 dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE)
56 dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE) 61 dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE)
57 dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE) 62 dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE)
58 63
59 val transformationStartTime = System.nanoTime 64 val transformationStartTime = System.nanoTime
60 65
61 66 val emptySolution = initialiser.initialisePartialInterpretation(problem, viatraConfig.typeScopes).output
62 67 if ((viatraConfig.documentationLevel == DocumentationLevel::FULL ||
63 val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output 68 viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {
64 if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { 69 workspace.writeModel(emptySolution, "init.partialmodel")
65 workspace.writeModel(emptySolution,"init.partialmodel") 70 }
66 }
67 emptySolution.problemConainer = problem 71 emptySolution.problemConainer = problem
68 72
69 val ScopePropagator scopePropagator = new ScopePropagator(emptySolution) 73 val ScopePropagator scopePropagator = new ScopePropagator(emptySolution)
70 scopePropagator.propagateAllScopeConstraints 74 scopePropagator.propagateAllScopeConstraints
71 75
72 val method = modelGenerationMethodProvider.createModelGenerationMethod( 76 val method = modelGenerationMethodProvider.createModelGenerationMethod(
73 problem, 77 problem,
74 emptySolution, 78 emptySolution,
@@ -78,138 +82,185 @@ class ViatraReasoner extends LogicReasoner{
78 scopePropagator, 82 scopePropagator,
79 viatraConfig.documentationLevel 83 viatraConfig.documentationLevel
80 ) 84 )
81 85
82 dse.addObjective(new ModelGenerationCompositeObjective( 86 dse.addObjective(new ModelGenerationCompositeObjective(
83 new ScopeObjective, 87 new ScopeObjective,
84 method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], 88 method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)],
85 new UnfinishedWFObjective(method.unfinishedWF) 89 wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF)
86 )) 90 ))
87 91
88 dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF)) 92 val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size)
89 for(additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) { 93 for (entry : viatraConfig.costObjectives.indexed) {
90 dse.addGlobalConstraint(additionalConstraint.apply(method)) 94 val objectiveName = '''costObjective«entry.key»'''
95 val objectiveConfig = entry.value
96 val elementsBuilder = ImmutableList.builder
97 for (elementConfig : objectiveConfig.elements) {
98 val relationName = elementConfig.patternQualifiedName
99 val modalQueries = method.modalRelationQueries.get(relationName)
100 if (modalQueries === null) {
101 throw new IllegalArgumentException("Unknown relation: " + relationName)
102 }
103 elementsBuilder.add(new ThreeValuedCostElement(
104 modalQueries.currentQuery,
105 modalQueries.mayQuery,
106 modalQueries.mustQuery,
107 elementConfig.weight
108 ))
109 }
110 val costElements = elementsBuilder.build
111 val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind,
112 objectiveConfig.threshold, 3)
113 dse.addObjective(costObjective)
114 if (objectiveConfig.findExtremum) {
115 extremalObjectives += costObjective
116 }
91 } 117 }
92 118
93 dse.setInitialModel(emptySolution,false) 119 val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions
94 120 val solutionStore = if (extremalObjectives.empty) {
95 val IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) { 121 new SolutionStore(numberOfRequiredSolutions)
96 new NeighbourhoodBasedStateCoderFactory 122 } else {
97 } else { 123 new SolutionStore()
98 new IdentifierBasedStateCoderFactory 124 }
125 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))
126 val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement)
127 val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions,
128 diversityChecker)
129 val solutionCopier = solutionSaver.solutionCopier
130 solutionStore.withSolutionSaver(solutionSaver)
131 dse.solutionStore = solutionStore
132
133 dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationGlobalConstraint(method.invalidWF))
134 dse.addGlobalConstraint(new SurelyViolatedObjectiveGlobalConstraint(solutionSaver))
135 for (additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) {
136 dse.addGlobalConstraint(additionalConstraint.apply(method))
99 } 137 }
138
139 dse.setInitialModel(emptySolution, false)
140
141 val IStateCoderFactory statecoder = if (viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) {
142 new NeighbourhoodBasedStateCoderFactory
143 } else {
144 new IdentifierBasedStateCoderFactory
145 }
100 dse.stateCoderFactory = statecoder 146 dse.stateCoderFactory = statecoder
101 147
102 dse.maxNumberOfThreads = 1 148 dse.maxNumberOfThreads = 1
103 149
104 val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolution) 150 for (rule : method.relationRefinementRules) {
105 dse.solutionStore = solutionStore
106
107 for(rule : method.relationRefinementRules) {
108 dse.addTransformationRule(rule) 151 dse.addTransformationRule(rule)
109 } 152 }
110 for(rule : method.objectRefinementRules) { 153 for (rule : method.objectRefinementRules) {
111 dse.addTransformationRule(rule) 154 dse.addTransformationRule(rule)
112 } 155 }
113 156
114 val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) 157 val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method)
115 viatraConfig.progressMonitor.workedForwardTransformation 158 viatraConfig.progressMonitor.workedForwardTransformation
116 159
117 val transformationTime = System.nanoTime - transformationStartTime 160 val transformationTime = System.nanoTime - transformationStartTime
118 val solverStartTime = System.nanoTime 161 val solverStartTime = System.nanoTime
119 162
120 var boolean stoppedByTimeout 163 var boolean stoppedByTimeout
121 var boolean stoppedByException 164 try {
122 try{ 165 stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000);
123 stoppedByTimeout = dse.startExplorationWithTimeout(strategy,configuration.runtimeLimit*1000);
124 stoppedByException = false
125 } catch (NullPointerException npe) { 166 } catch (NullPointerException npe) {
126 stoppedByTimeout = false 167 stoppedByTimeout = false
127 stoppedByException = true
128 } 168 }
129 val solverTime = System.nanoTime - solverStartTime 169 val solverTime = System.nanoTime - solverStartTime
130 viatraConfig.progressMonitor.workedSearchFinished 170 viatraConfig.progressMonitor.workedSearchFinished
131 171
132 //additionalMatches = strategy.solutionStoreWithCopy.additionalMatches 172 // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches
133 val statistics = createStatistics => [ 173 val statistics = createStatistics => [
134 //it.solverTime = viatraConfig.runtimeLimit 174 // it.solverTime = viatraConfig.runtimeLimit
135 it.solverTime = (solverTime/1000000) as int 175 it.solverTime = (solverTime / 1000000) as int
136 it.transformationTime = (transformationTime/1000000) as int 176 it.transformationTime = (transformationTime / 1000000) as int
137 for(x : 0..<strategy.solutionStoreWithCopy.allRuntimes.size) { 177 for (pair : solutionCopier.getAllCopierRuntimes(true).indexed) {
138 it.entries += createIntStatisticEntry => [ 178 it.entries += createIntStatisticEntry => [
139 it.name = '''_Solution«x»FoundAt''' 179 it.name = '''_Solution«pair.key»FoundAt'''
140 it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int 180 it.value = (pair.value / 1000000) as int
141 ] 181 ]
142 } 182 }
143 it.entries += createIntStatisticEntry => [ 183 it.entries += createIntStatisticEntry => [
144 it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int 184 it.name = "TransformationExecutionTime"
185 it.value = (method.statistics.transformationExecutionTime / 1000000) as int
145 ] 186 ]
146 it.entries += createIntStatisticEntry => [ 187 it.entries += createIntStatisticEntry => [
147 it.name = "TypeAnalysisTime" it.value = (method.statistics.PreliminaryTypeAnalisisTime/1000000) as int 188 it.name = "TypeAnalysisTime"
189 it.value = (method.statistics.PreliminaryTypeAnalisisTime / 1000000) as int
148 ] 190 ]
149 it.entries += createIntStatisticEntry => [ 191 it.entries += createIntStatisticEntry => [
150 it.name = "StateCoderTime" it.value = (statecoder.runtime/1000000) as int 192 it.name = "StateCoderTime"
193 it.value = (statecoder.runtime / 1000000) as int
151 ] 194 ]
152 it.entries += createIntStatisticEntry => [ 195 it.entries += createIntStatisticEntry => [
153 it.name = "StateCoderFailCount" it.value = strategy.numberOfStatecoderFail 196 it.name = "StateCoderFailCount"
197 it.value = strategy.numberOfStatecoderFail
154 ] 198 ]
155 it.entries += createIntStatisticEntry => [ 199 it.entries += createIntStatisticEntry => [
156 it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int 200 it.name = "SolutionCopyTime"
201 it.value = (solutionCopier.getTotalCopierRuntime / 1000000) as int
157 ] 202 ]
158 if(strategy.solutionStoreWithDiversityDescriptor.isActive) { 203 if (diversityChecker.isActive) {
159 it.entries += createIntStatisticEntry => [ 204 it.entries += createIntStatisticEntry => [
160 it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int 205 it.name = "SolutionDiversityCheckTime"
206 it.value = (diversityChecker.totalRuntime / 1000000) as int
161 ] 207 ]
162 it.entries += createRealStatisticEntry => [ 208 it.entries += createRealStatisticEntry => [
163 it.name = "SolutionDiversitySuccessRate" it.value = strategy.solutionStoreWithDiversityDescriptor.successRate 209 it.name = "SolutionDiversitySuccessRate"
210 it.value = diversityChecker.successRate
164 ] 211 ]
165 } 212 }
166 ] 213 ]
167 214
168 viatraConfig.progressMonitor.workedBackwardTransformationFinished 215 viatraConfig.progressMonitor.workedBackwardTransformationFinished
169 216
170 if(stoppedByTimeout) { 217 if (stoppedByTimeout) {
171 return createInsuficientResourcesResult=>[ 218 return createInsuficientResourcesResult => [
172 it.problem = problem 219 it.problem = problem
173 it.resourceName="time" 220 it.resourceName = "time"
174 it.representation += strategy.solutionStoreWithCopy.solutions 221 it.representation += solutionCopier.getPartialInterpretations(true)
175 it.statistics = statistics 222 it.statistics = statistics
176 ] 223 ]
177 } else { 224 } else {
178 if(solutionStore.solutions.empty) { 225 if (solutionStore.solutions.empty) {
179 return createInconsistencyResult => [ 226 return createInconsistencyResult => [
180 it.problem = problem 227 it.problem = problem
181 it.representation += strategy.solutionStoreWithCopy.solutions 228 it.representation += solutionCopier.getPartialInterpretations(true)
182 it.statistics = statistics 229 it.statistics = statistics
183 ] 230 ]
184 } else { 231 } else {
185 return createModelResult => [ 232 return createModelResult => [
186 it.problem = problem 233 it.problem = problem
187 it.trace = strategy.solutionStoreWithCopy.copyTraces 234 it.trace = solutionCopier.getTraces(true)
188 it.representation += strategy.solutionStoreWithCopy.solutions 235 it.representation += solutionCopier.getPartialInterpretations(true)
189 it.statistics = statistics 236 it.statistics = statistics
190 ] 237 ]
191 } 238 }
192 } 239 }
193 } 240 }
194 241
195 private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) { 242 private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) {
196 sc.sumStatecoderRuntime 243 sc.sumStatecoderRuntime
197 } 244 }
198 245
199 private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) { 246 private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) {
200 sc.sumStatecoderRuntime 247 sc.sumStatecoderRuntime
201 } 248 }
202 249
203 override getInterpretations(ModelResult modelResult) { 250 override getInterpretations(ModelResult modelResult) {
204 val indexes = 0..<modelResult.representation.size 251 val indexes = 0 ..< modelResult.representation.size
205 val traces = modelResult.trace as List<Map<EObject, EObject>>; 252 val traces = modelResult.trace as List<Map<EObject, EObject>>;
206 val res = indexes.map[i | new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation,traces.get(i))].toList 253 val res = indexes.map [ i |
254 new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation,
255 traces.get(i))
256 ].toList
207 return res 257 return res
208 } 258 }
209 259
210 private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) { 260 private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) {
211 if(configuration instanceof ViatraReasonerConfiguration) { 261 if (configuration instanceof ViatraReasonerConfiguration) {
212 return configuration 262 return configuration
213 } else throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''') 263 } else
264 throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''')
214 } 265 }
215} 266}
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..e6aee20c 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
@@ -7,18 +7,22 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod 7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod 8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser 9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser
10import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
11import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
10import java.util.LinkedList 12import java.util.LinkedList
11import java.util.List 13import java.util.List
12import java.util.Set 14import java.util.Set
13import org.eclipse.xtext.xbase.lib.Functions.Function1 15import org.eclipse.xtext.xbase.lib.Functions.Function1
14 16
15public enum StateCoderStrategy { 17enum StateCoderStrategy {
16 Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity 18 Neighbourhood,
19 NeighbourhoodWithEquivalence,
20 IDBased,
21 DefinedByDiversity
17} 22}
18 23
19class ViatraReasonerConfiguration extends LogicSolverConfiguration{ 24class ViatraReasonerConfiguration extends LogicSolverConfiguration {
20 //public var Iterable<PQuery> existingQueries 25 // public var Iterable<PQuery> existingQueries
21
22 public var nameNewElements = false 26 public var nameNewElements = false
23 public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood 27 public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood
24 public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis 28 public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
@@ -26,7 +30,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
26 * Once per 1/randomBacktrackChance the search selects a random state. 30 * Once per 1/randomBacktrackChance the search selects a random state.
27 */ 31 */
28 public var int randomBacktrackChance = 20; 32 public var int randomBacktrackChance = 20;
29 33
30 /** 34 /**
31 * Describes the required diversity between the solutions. 35 * Describes the required diversity between the solutions.
32 * Null means that the solutions have to have different state codes only. 36 * Null means that the solutions have to have different state codes only.
@@ -40,14 +44,16 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
40 /** 44 /**
41 * Configuration for debugging support. 45 * Configuration for debugging support.
42 */ 46 */
43 public var DebugConfiguration debugCongiguration = new DebugConfiguration 47 public var DebugConfiguration debugConfiguration = new DebugConfiguration
44 /** 48 /**
45 * Configuration for cutting search space. 49 * Configuration for cutting search space.
46 */ 50 */
47 public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint 51 public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint
52
53 public var List<CostObjectiveConfiguration> costObjectives = newArrayList
48} 54}
49 55
50public class DiversityDescriptor { 56class DiversityDescriptor {
51 public var ensureDiversity = false 57 public var ensureDiversity = false
52 public static val FixPointRange = -1 58 public static val FixPointRange = -1
53 public var int range = FixPointRange 59 public var int range = FixPointRange
@@ -57,20 +63,32 @@ public class DiversityDescriptor {
57 public var Set<RelationDeclaration> relevantRelations = null 63 public var Set<RelationDeclaration> relevantRelations = null
58} 64}
59 65
60public class DebugConfiguration { 66class DebugConfiguration {
61 public var logging = false 67 public var logging = false
62 public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null; 68 public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null;
63 public var partalInterpretationVisualisationFrequency = 1 69 public var partalInterpretationVisualisationFrequency = 1
64} 70}
65 71
66public class InternalConsistencyCheckerConfiguration { 72class InternalConsistencyCheckerConfiguration {
67 public var LogicReasoner internalIncosnsitencyDetector = null 73 public var LogicReasoner internalIncosnsitencyDetector = null
68 public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null 74 public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null
69 public var incternalConsistencyCheckingFrequency = 1 75 public var incternalConsistencyCheckingFrequency = 1
70} 76}
71 77
72public class SearchSpaceConstraint { 78class SearchSpaceConstraint {
73 public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE 79 public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE
74 public var int maxDepth = UNLIMITED_MAXDEPTH 80 public var int maxDepth = UNLIMITED_MAXDEPTH
75 public var List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList 81 public var List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList
76} \ No newline at end of file 82}
83
84class CostObjectiveConfiguration {
85 public var List<CostObjectiveElementConfiguration> elements = newArrayList
86 public var ObjectiveKind kind
87 public var ObjectiveThreshold threshold
88 public var boolean findExtremum
89}
90
91class CostObjectiveElementConfiguration {
92 public var String patternQualifiedName
93 public var int weight
94}
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 60f46033..6ff867d7 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
@@ -75,8 +75,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
75 // Running 75 // Running
76 private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore; 76 private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore;
77 private SolutionStore solutionStore; 77 private SolutionStore solutionStore;
78 private SolutionStoreWithCopy solutionStoreWithCopy;
79 private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor;
80 private volatile boolean isInterrupted = false; 78 private volatile boolean isInterrupted = false;
81 private ModelResult modelResultByInternalSolver = null; 79 private ModelResult modelResultByInternalSolver = null;
82 private Random random = new Random(); 80 private Random random = new Random();
@@ -97,12 +95,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
97 this.method = method; 95 this.method = method;
98 } 96 }
99 97
100 public SolutionStoreWithCopy getSolutionStoreWithCopy() {
101 return solutionStoreWithCopy;
102 }
103 public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
104 return solutionStoreWithDiversityDescriptor;
105 }
106 public int getNumberOfStatecoderFail() { 98 public int getNumberOfStatecoderFail() {
107 return numberOfStatecoderFail; 99 return numberOfStatecoderFail;
108 } 100 }
@@ -121,9 +113,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
121 matchers.add(matcher); 113 matchers.add(matcher);
122 } 114 }
123 115
124 this.solutionStoreWithCopy = new SolutionStoreWithCopy();
125 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
126
127 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); 116 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
128 this.comparator = new Comparator<TrajectoryWithFitness>() { 117 this.comparator = new Comparator<TrajectoryWithFitness>() {
129 @Override 118 @Override
@@ -146,13 +135,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
146 return; 135 return;
147 } 136 }
148 137
149 final Fitness firstFittness = context.calculateFitness(); 138 final Fitness firstfitness = context.calculateFitness();
150 checkForSolution(firstFittness); 139 solutionStore.newSolution(context);
151 140
152 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); 141 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
153 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); 142 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
154 TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness); 143 TrajectoryWithFitness currentTrajectoryWithfitness = new TrajectoryWithFitness(firstTrajectory, firstfitness);
155 trajectoiresToExplore.add(currentTrajectoryWithFittness); 144 trajectoiresToExplore.add(currentTrajectoryWithfitness);
156 145
157 //if(configuration) 146 //if(configuration)
158 visualiseCurrentState(); 147 visualiseCurrentState();
@@ -167,22 +156,22 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
167 156
168 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) { 157 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) {
169 158
170 if (currentTrajectoryWithFittness == null) { 159 if (currentTrajectoryWithfitness == null) {
171 if (trajectoiresToExplore.isEmpty()) { 160 if (trajectoiresToExplore.isEmpty()) {
172 logger.debug("State space is fully traversed."); 161 logger.debug("State space is fully traversed.");
173 return; 162 return;
174 } else { 163 } else {
175 currentTrajectoryWithFittness = selectState(); 164 currentTrajectoryWithfitness = selectState();
176 if (logger.isDebugEnabled()) { 165 if (logger.isDebugEnabled()) {
177 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); 166 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
178 logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness); 167 logger.debug("New trajectory is chosen: " + currentTrajectoryWithfitness);
179 } 168 }
180 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory); 169 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithfitness.trajectory);
181 } 170 }
182 } 171 }
183 172
184// visualiseCurrentState(); 173// visualiseCurrentState();
185// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); 174// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
186// if(consistencyCheckResult == true) { 175// if(consistencyCheckResult == true) {
187// continue mainLoop; 176// continue mainLoop;
188// } 177// }
@@ -194,7 +183,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
194 final Object nextActivation = iterator.next(); 183 final Object nextActivation = iterator.next();
195// if (!iterator.hasNext()) { 184// if (!iterator.hasNext()) {
196// logger.debug("Last untraversed activation of the state."); 185// logger.debug("Last untraversed activation of the state.");
197// trajectoiresToExplore.remove(currentTrajectoryWithFittness); 186// trajectoiresToExplore.remove(currentTrajectoryWithfitness);
198// } 187// }
199 logger.debug("Executing new activation: " + nextActivation); 188 logger.debug("Executing new activation: " + nextActivation);
200 context.executeAcitvationId(nextActivation); 189 context.executeAcitvationId(nextActivation);
@@ -209,7 +198,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
209// System.out.println("---------"); 198// System.out.println("---------");
210// } 199// }
211 200
212 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); 201 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
213 if(consistencyCheckResult == true) { continue mainLoop; } 202 if(consistencyCheckResult == true) { continue mainLoop; }
214 203
215 if (context.isCurrentStateAlreadyTraversed()) { 204 if (context.isCurrentStateAlreadyTraversed()) {
@@ -220,38 +209,38 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
220 context.backtrack(); 209 context.backtrack();
221 } else { 210 } else {
222 final Fitness nextFitness = context.calculateFitness(); 211 final Fitness nextFitness = context.calculateFitness();
223 checkForSolution(nextFitness); 212 solutionStore.newSolution(context);
224 if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) { 213 if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) {
225 logger.debug("Reached max depth."); 214 logger.debug("Reached max depth.");
226 context.backtrack(); 215 context.backtrack();
227 continue; 216 continue;
228 } 217 }
229 218
230 TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness( 219 TrajectoryWithFitness nextTrajectoryWithfitness = new TrajectoryWithFitness(
231 context.getTrajectory().toArray(), nextFitness); 220 context.getTrajectory().toArray(), nextFitness);
232 trajectoiresToExplore.add(nextTrajectoryWithFittness); 221 trajectoiresToExplore.add(nextTrajectoryWithfitness);
233 222
234 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness, 223 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithfitness.fitness,
235 nextTrajectoryWithFittness.fitness); 224 nextTrajectoryWithfitness.fitness);
236 if (compare < 0) { 225 if (compare < 0) {
237 logger.debug("Better fitness, moving on: " + nextFitness); 226 logger.debug("Better fitness, moving on: " + nextFitness);
238 currentTrajectoryWithFittness = nextTrajectoryWithFittness; 227 currentTrajectoryWithfitness = nextTrajectoryWithfitness;
239 continue mainLoop; 228 continue mainLoop;
240 } else if (compare == 0) { 229 } else if (compare == 0) {
241 logger.debug("Equally good fitness, moving on: " + nextFitness); 230 logger.debug("Equally good fitness, moving on: " + nextFitness);
242 currentTrajectoryWithFittness = nextTrajectoryWithFittness; 231 currentTrajectoryWithfitness = nextTrajectoryWithfitness;
243 continue mainLoop; 232 continue mainLoop;
244 } else { 233 } else {
245 logger.debug("Worse fitness."); 234 logger.debug("Worse fitness.");
246 currentTrajectoryWithFittness = null; 235 currentTrajectoryWithfitness = null;
247 continue mainLoop; 236 continue mainLoop;
248 } 237 }
249 } 238 }
250 } 239 }
251 240
252 logger.debug("State is fully traversed."); 241 logger.debug("State is fully traversed.");
253 trajectoiresToExplore.remove(currentTrajectoryWithFittness); 242 trajectoiresToExplore.remove(currentTrajectoryWithfitness);
254 currentTrajectoryWithFittness = null; 243 currentTrajectoryWithfitness = null;
255 244
256 } 245 }
257 logger.info("Interrupted."); 246 logger.info("Interrupted.");
@@ -269,19 +258,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
269 return activationIds; 258 return activationIds;
270 } 259 }
271 260
272 private void checkForSolution(final Fitness fittness) {
273 if (fittness.isSatisifiesHardObjectives()) {
274 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
275 solutionStoreWithCopy.newSolution(context);
276 solutionStoreWithDiversityDescriptor.newSolution(context);
277 solutionStore.newSolution(context);
278 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
279
280 logger.debug("Found a solution.");
281 }
282 }
283 }
284
285 @Override 261 @Override
286 public void interruptStrategy() { 262 public void interruptStrategy() {
287 isInterrupted = true; 263 isInterrupted = true;
@@ -311,11 +287,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
311 } 287 }
312 288
313 public void visualiseCurrentState() { 289 public void visualiseCurrentState() {
314 PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser; 290 PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser;
315 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) { 291 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) {
316 PartialInterpretation p = (PartialInterpretation) (context.getModel()); 292 PartialInterpretation p = (PartialInterpretation) (context.getModel());
317 int id = ++numberOfPrintedModel; 293 int id = ++numberOfPrintedModel;
318 if (id % configuration.debugCongiguration.partalInterpretationVisualisationFrequency == 0) { 294 if (id % configuration.debugConfiguration.partalInterpretationVisualisationFrequency == 0) {
319 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p); 295 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p);
320 visualisation.writeToFile(workspace, String.format("state%09d.png", id)); 296 visualisation.writeToFile(workspace, String.format("state%09d.png", id));
321 } 297 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend
new file mode 100644
index 00000000..fb1b2066
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend
@@ -0,0 +1,184 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import com.google.common.collect.HashMultiset
4import com.google.common.collect.ImmutableSet
5import com.google.common.collect.Multiset
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.NeighbourhoodWithTraces
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
10import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
11import java.util.Collection
12import java.util.HashSet
13import java.util.Map
14import java.util.Set
15import org.eclipse.viatra.dse.base.ThreadContext
16import org.eclipse.xtend.lib.annotations.Accessors
17
18interface DiversityChecker {
19 public static val NO_DIVERSITY_CHECKER = new DiversityChecker {
20 override isActive() {
21 false
22 }
23
24 override getTotalRuntime() {
25 0
26 }
27
28 override getSuccessRate() {
29 1.0
30 }
31
32 override newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) {
33 true
34 }
35 }
36
37 def boolean isActive()
38
39 def long getTotalRuntime()
40
41 def double getSuccessRate()
42
43 def boolean newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds)
44
45 static def of(DiversityDescriptor descriptor) {
46 if (descriptor.ensureDiversity) {
47 new NodewiseDiversityChecker(descriptor)
48 } else {
49 NO_DIVERSITY_CHECKER
50 }
51 }
52}
53
54abstract class AbstractDiversityChecker implements DiversityChecker {
55 val DiversityDescriptor descriptor
56 val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice
57
58 @Accessors(PUBLIC_GETTER) var long totalRuntime = 0
59 var int allCheckCount = 0
60 var int successfulCheckCount = 0
61
62 protected new(DiversityDescriptor descriptor) {
63 if (!descriptor.ensureDiversity) {
64 throw new IllegalArgumentException(
65 "Diversity description should enforce diversity or NO_DIVERSITY_CHECKER should be used instead.")
66 }
67 this.descriptor = descriptor
68 }
69
70 override isActive() {
71 true
72 }
73
74 override getTotalRuntime() {
75 throw new UnsupportedOperationException("TODO: auto-generated method stub")
76 }
77
78 override getSuccessRate() {
79 (allCheckCount as double) / (successfulCheckCount as double)
80 }
81
82 override newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) {
83 val start = System.nanoTime
84 val model = threadContext.model as PartialInterpretation
85 val representation = solutionCoder.createRepresentation(model, descriptor.range, descriptor.parallels,
86 descriptor.maxNumber, descriptor.relevantTypes, descriptor.relevantRelations)
87 val isDifferent = internalNewSolution(representation, solutionId, dominatedSolutionIds)
88 totalRuntime += System.nanoTime - start
89 allCheckCount++
90 if (isDifferent) {
91 successfulCheckCount++
92 }
93 isDifferent
94 }
95
96 protected abstract def boolean internalNewSolution(
97 NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation,
98 Object solutionId, Collection<Object> dominatedSolutionIds)
99}
100
101class NodewiseDiversityChecker extends AbstractDiversityChecker {
102 var Multiset<Integer> nodeCodes = HashMultiset.create
103 val Map<Object, Set<Integer>> tracedNodeCodes = newHashMap
104
105 new(DiversityDescriptor descriptor) {
106 super(descriptor)
107 }
108
109 override protected internalNewSolution(
110 NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation,
111 Object solutionId, Collection<Object> dominatedSolutionIds) {
112 val nodeCodesInSolution = ImmutableSet.copyOf(representation.modelRepresentation.keySet.map[hashCode])
113 val remainingNodeCodes = if (dominatedSolutionIds.empty) {
114 nodeCodes
115 } else {
116 getRemainingNodeCodes(dominatedSolutionIds)
117 }
118 val hasNewCode = nodeCodesInSolution.exists[!remainingNodeCodes.contains(it)]
119 if (hasNewCode) {
120 nodeCodes = remainingNodeCodes
121 nodeCodes.addAll(nodeCodesInSolution)
122 for (dominatedSolutionId : dominatedSolutionIds) {
123 tracedNodeCodes.remove(dominatedSolutionId)
124 }
125 tracedNodeCodes.put(solutionId, nodeCodesInSolution)
126 }
127 hasNewCode
128 }
129
130 private def getRemainingNodeCodes(Collection<Object> dominatedSolutionIds) {
131 // TODO Optimize multiset operations.
132 val copyOfNodeCodes = HashMultiset.create(nodeCodes)
133 for (dominatedSolutionId : dominatedSolutionIds) {
134 val dominatedModelCode = tracedNodeCodes.get(dominatedSolutionId)
135 if (dominatedModelCode === null) {
136 throw new IllegalArgumentException("Unknown dominated solution: " + dominatedSolutionId)
137 }
138 copyOfNodeCodes.removeAll(dominatedModelCode)
139 }
140 copyOfNodeCodes
141 }
142}
143
144class GraphwiseDiversityChecker extends AbstractDiversityChecker {
145 var Set<Integer> modelCodes = newHashSet
146 val Map<Object, Integer> tracedModelCodes = newHashMap
147
148 new(DiversityDescriptor descriptor) {
149 super(descriptor)
150 }
151
152 override protected internalNewSolution(
153 NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation,
154 Object solutionId, Collection<Object> dominatedSolutionIds) {
155 val modelCodeOfSolution = representation.modelRepresentation.hashCode
156 val remainingModelCodes = if (dominatedSolutionIds.empty) {
157 modelCodes
158 } else {
159 getRemainingModelCodes(dominatedSolutionIds)
160 }
161 val isNewCode = !remainingModelCodes.contains(modelCodeOfSolution)
162 if (isNewCode) {
163 modelCodes = remainingModelCodes
164 modelCodes += modelCodeOfSolution
165 for (dominatedSolutionId : dominatedSolutionIds) {
166 tracedModelCodes.remove(dominatedSolutionId)
167 }
168 tracedModelCodes.put(solutionId, modelCodeOfSolution)
169 }
170 isNewCode
171 }
172
173 private def getRemainingModelCodes(Collection<Object> dominatedSolutionIds) {
174 val copyOfModelCodes = new HashSet(modelCodes)
175 for (dominatedSolutionId : dominatedSolutionIds) {
176 val dominatedModelCode = tracedModelCodes.get(dominatedSolutionId)
177 if (dominatedModelCode === null) {
178 throw new IllegalArgumentException("Unknown dominated solution: " + dominatedSolutionId)
179 }
180 copyOfModelCodes -= dominatedModelCode
181 }
182 copyOfModelCodes
183 }
184}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend
new file mode 100644
index 00000000..3c2e3319
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend
@@ -0,0 +1,66 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective
4import org.eclipse.viatra.dse.base.ThreadContext
5import org.eclipse.viatra.dse.objectives.Comparators
6import org.eclipse.viatra.dse.objectives.Fitness
7import org.eclipse.viatra.dse.objectives.IObjective
8
9final class DseUtils {
10 private new() {
11 throw new IllegalStateException("This is a static utility class and should not be instantiated directly.")
12 }
13
14 static def calculateFitness(ThreadContext it, (IObjective)=>Double getFitness) {
15 val result = new Fitness
16 var boolean satisifiesHardObjectives = true
17 for (objective : objectives) {
18 val fitness = getFitness.apply(objective)
19 result.put(objective.name, fitness)
20 if (objective.isHardObjective() && !objective.satisifiesHardObjective(fitness)) {
21 satisifiesHardObjectives = false
22 }
23 }
24 result.satisifiesHardObjectives = satisifiesHardObjectives
25 result
26 }
27
28 static def caclulateBestPossibleFitness(ThreadContext threadContext) {
29 threadContext.calculateFitness [ objective |
30 if (objective instanceof IThreeValuedObjective) {
31 objective.getBestPossibleFitness(threadContext)
32 } else {
33 switch (objective.comparator) {
34 case Comparators.LOWER_IS_BETTER:
35 Double.NEGATIVE_INFINITY
36 case Comparators.HIGHER_IS_BETTER:
37 Double.POSITIVE_INFINITY
38 case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER:
39 0.0
40 default:
41 throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " +
42 objective.name)
43 }
44 }
45 ]
46 }
47
48 static def caclulateWorstPossibleFitness(ThreadContext threadContext) {
49 threadContext.calculateFitness [ objective |
50 if (objective instanceof IThreeValuedObjective) {
51 objective.getWorstPossibleFitness(threadContext)
52 } else {
53 switch (objective.comparator) {
54 case Comparators.LOWER_IS_BETTER,
55 case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER:
56 Double.POSITIVE_INFINITY
57 case Comparators.HIGHER_IS_BETTER:
58 Double.NEGATIVE_INFINITY
59 default:
60 throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " +
61 objective.name)
62 }
63 }
64 ]
65 }
66}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend
new file mode 100644
index 00000000..39ef5f9a
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend
@@ -0,0 +1,24 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
4import org.apache.log4j.Logger
5import org.eclipse.viatra.dse.api.SolutionTrajectory
6import org.eclipse.viatra.dse.base.ThreadContext
7import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler
8import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
9
10@FinalFieldsConstructor
11class LoggerSolutionFoundHandler implements ISolutionFoundHandler {
12 val ViatraReasonerConfiguration configuration
13
14 val logger = Logger.getLogger(SolutionCopier)
15
16 override solutionFound(ThreadContext context, SolutionTrajectory trajectory) {
17 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions)
18 logger.debug("Found a solution.")
19 }
20
21 override solutionTriedToSave(ThreadContext context, SolutionTrajectory trajectory) {
22 // We are not interested in invalid solutions, ignore.
23 }
24}
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 2489c751..9a33753c 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
@@ -1,11 +1,13 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import com.google.common.collect.ImmutableList
4import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective
3import java.util.Comparator 5import java.util.Comparator
4import java.util.List 6import java.util.List
5import org.eclipse.viatra.dse.base.ThreadContext 7import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.dse.objectives.Comparators 8import org.eclipse.viatra.dse.objectives.Comparators
7import org.eclipse.viatra.dse.objectives.IObjective 9import org.eclipse.viatra.dse.objectives.IObjective
8import org.eclipse.viatra.dse.objectives.impl.BaseObjective 10import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
9 11
10//class ViatraReasonerNumbers { 12//class ViatraReasonerNumbers {
11// public static val scopePriority = 2 13// public static val scopePriority = 2
@@ -22,64 +24,66 @@ import org.eclipse.viatra.dse.objectives.impl.BaseObjective
22// public static val compositePriority = 2 24// public static val compositePriority = 2
23//} 25//}
24 26
25class ModelGenerationCompositeObjective implements IObjective{ 27@FinalFieldsConstructor
26 val ScopeObjective scopeObjective 28class ModelGenerationCompositeObjective implements IThreeValuedObjective {
27 val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives 29 val IObjective scopeObjective
28 val UnfinishedWFObjective unfinishedWFObjective 30 val List<IObjective> unfinishedMultiplicityObjectives
29 31 val IObjective unfinishedWFObjective
30 public new( 32
31 ScopeObjective scopeObjective,
32 List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
33 UnfinishedWFObjective unfinishedWFObjective)
34 {
35 this.scopeObjective = scopeObjective
36 this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives
37 this.unfinishedWFObjective = unfinishedWFObjective
38 }
39
40 override init(ThreadContext context) { 33 override init(ThreadContext context) {
41 this.scopeObjective.init(context) 34 this.scopeObjective.init(context)
42 this.unfinishedMultiplicityObjectives.forEach[it.init(context)] 35 this.unfinishedMultiplicityObjectives.forEach[it.init(context)]
43 this.unfinishedWFObjective.init(context) 36 this.unfinishedWFObjective.init(context)
44 } 37 }
45 38
46 override createNew() { 39 override createNew() {
47 return new ModelGenerationCompositeObjective( 40 return new ModelGenerationCompositeObjective(
48 this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective) 41 scopeObjective.createNew,
42 ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew]),
43 unfinishedWFObjective.createNew
44 )
49 } 45 }
50 46
51 override getComparator() { Comparators.LOWER_IS_BETTER } 47 override getComparator() { Comparators.LOWER_IS_BETTER }
48
52 override getFitness(ThreadContext context) { 49 override getFitness(ThreadContext context) {
53 var sum = 0.0 50 var sum = 0.0
54 val scopeFitnes = scopeObjective.getFitness(context) 51 val scopeFitnes = scopeObjective.getFitness(context)
55 //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] 52 // val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]
56 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) 53 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)
57 54
58 sum+=scopeFitnes 55 sum += scopeFitnes
59 var multiplicity = 0.0 56 var multiplicity = 0.0
60 for(multiplicityObjective : unfinishedMultiplicityObjectives) { 57 for (multiplicityObjective : unfinishedMultiplicityObjectives) {
61 multiplicity+=multiplicityObjective.getFitness(context)//*0.5 58 multiplicity += multiplicityObjective.getFitness(context) // *0.5
62 } 59 }
63 sum+=multiplicity 60 sum += multiplicity
64 sum += unfinishedWFsFitness//*0.5 61 sum += unfinishedWFsFitness // *0.5
65 62 // println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
66 //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
67
68 return sum 63 return sum
69 } 64 }
70 65
71 override getLevel() { 2 } 66 override getWorstPossibleFitness(ThreadContext threadContext) {
72 override getName() { "CompositeUnfinishednessObjective"} 67 Double.POSITIVE_INFINITY
68 }
73 69
70 override getBestPossibleFitness(ThreadContext threadContext) {
71 0.0
72 }
73
74 override getLevel() { 2 }
75
76 override getName() { "CompositeUnfinishednessObjective" }
77
74 override isHardObjective() { true } 78 override isHardObjective() { true }
79
75 override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } 80 override satisifiesHardObjective(Double fitness) { fitness <= 0.001 }
76 81
77
78 override setComparator(Comparator<Double> comparator) { 82 override setComparator(Comparator<Double> comparator) {
79 throw new UnsupportedOperationException("TODO: auto-generated method stub") 83 throw new UnsupportedOperationException("Model generation objective comparator cannot be set.")
80 } 84 }
85
81 override setLevel(int level) { 86 override setLevel(int level) {
82 throw new UnsupportedOperationException("TODO: auto-generated method stub") 87 throw new UnsupportedOperationException("Model generation objective level cannot be set.")
83 } 88 }
84 89}
85} \ 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/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
new file mode 100644
index 00000000..d036257d
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
@@ -0,0 +1,74 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import com.google.common.collect.ImmutableList
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import java.util.LinkedHashMap
6import java.util.List
7import java.util.Map
8import org.eclipse.emf.ecore.EObject
9import org.eclipse.emf.ecore.util.EcoreUtil
10import org.eclipse.viatra.dse.base.ThreadContext
11import org.eclipse.xtend.lib.annotations.Accessors
12import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
13
14@FinalFieldsConstructor
15class CopiedSolution {
16 @Accessors val PartialInterpretation partialInterpretations
17 @Accessors val Map<EObject, EObject> trace
18 @Accessors val long copierRuntime
19 @Accessors var boolean current = true
20}
21
22class SolutionCopier {
23 val copiedSolutions = new LinkedHashMap<Object, CopiedSolution>
24
25 long startTime = System.nanoTime
26 @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0
27
28 def void copySolution(ThreadContext context, Object solutionId) {
29 val existingCopy = copiedSolutions.get(solutionId)
30 if (existingCopy === null) {
31 val copyStart = System.nanoTime
32 val solution = context.model as PartialInterpretation
33 val copier = new EcoreUtil.Copier
34 val copiedPartialInterpretation = copier.copy(solution) as PartialInterpretation
35 copier.copyReferences
36 totalCopierRuntime += System.nanoTime - copyStart
37 val copierRuntime = System.nanoTime - startTime
38 val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime)
39 copiedSolutions.put(solutionId, copiedSolution)
40 } else {
41 existingCopy.current = true
42 }
43 }
44
45 def void markAsObsolete(Object solutionId) {
46 val copiedSolution = copiedSolutions.get(solutionId)
47 if (copiedSolution === null) {
48 throw new IllegalStateException("No solution to mark as obsolete for state code: " + solutionId)
49 }
50 copiedSolution.current = false
51 }
52
53 def List<PartialInterpretation> getPartialInterpretations(boolean currentOnly) {
54 getListOfCopiedSolutions(currentOnly).map[partialInterpretations]
55 }
56
57 def List<Map<EObject, EObject>> getTraces(boolean currentOnly) {
58 getListOfCopiedSolutions(currentOnly).map[trace]
59 }
60
61 def List<Long> getAllCopierRuntimes(boolean currentOnly) {
62 getListOfCopiedSolutions(currentOnly).map[copierRuntime]
63 }
64
65 def List<CopiedSolution> getListOfCopiedSolutions(boolean currentOnly) {
66 val values = copiedSolutions.values
67 val filteredSolutions = if (currentOnly) {
68 values.filter[current]
69 } else {
70 values
71 }
72 ImmutableList.copyOf(filteredSolutions)
73 }
74}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
deleted file mode 100644
index a8b7301e..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
+++ /dev/null
@@ -1,52 +0,0 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.List
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import java.util.LinkedList
6import org.eclipse.emf.ecore.EObject
7import java.util.Map
8import org.eclipse.emf.ecore.util.EcoreUtil
9import org.eclipse.viatra.dse.base.ThreadContext
10import java.util.TreeMap
11import java.util.SortedMap
12
13class SolutionStoreWithCopy {
14
15 long runtime = 0
16 List<PartialInterpretation> solutions = new LinkedList
17 //public List<SortedMap<String,Integer>> additionalMatches = new LinkedList
18 List<Map<EObject,EObject>> copyTraces = new LinkedList
19
20 long sartTime = System.nanoTime
21 List<Long> solutionTimes = new LinkedList
22
23 /*def newSolution(ThreadContext context, SortedMap<String,Integer> additonalMatch) {
24 additionalMatches+= additonalMatch
25 newSolution(context)
26 }*/
27
28 def newSolution(ThreadContext context) {
29 //print(System.nanoTime-initTime + ";")
30 val copyStart = System.nanoTime
31 val solution = context.model as PartialInterpretation
32 val copier = new EcoreUtil.Copier
33 val solutionCopy = copier.copy(solution) as PartialInterpretation
34 copier.copyReferences
35 solutions.add(solutionCopy)
36 copyTraces.add(copier)
37 runtime += System.nanoTime - copyStart
38 solutionTimes.add(System.nanoTime-sartTime)
39 }
40 def getSumRuntime() {
41 return runtime
42 }
43 def getAllRuntimes() {
44 return solutionTimes
45 }
46 def getSolutions() {
47 solutions
48 }
49 def getCopyTraces() {
50 return copyTraces
51 }
52} \ 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/SolutionStoreWithDiversityDescriptor.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend
deleted file mode 100644
index 1e7f18a8..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend
+++ /dev/null
@@ -1,120 +0,0 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
6import java.util.LinkedList
7import java.util.List
8import org.eclipse.viatra.dse.base.ThreadContext
9import java.util.HashSet
10import java.util.Set
11
12enum DiversityGranularity {
13 Nodewise, Graphwise
14}
15
16class SolutionStoreWithDiversityDescriptor {
17 val DiversityDescriptor descriptor
18 DiversityGranularity granularity
19 val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice
20 val Set<Integer> solutionCodeList = new HashSet
21
22 var long runtime
23 var int allCheck
24 var int successfulCheck
25
26 new(DiversityDescriptor descriptor) {
27 if(descriptor.ensureDiversity) {
28 this.descriptor = descriptor
29 this.granularity = DiversityGranularity::Nodewise
30 } else {
31 this.descriptor = null
32 this.granularity = DiversityGranularity::Nodewise
33 }
34 }
35
36 def public isActive() {
37 descriptor!==null
38 }
39
40 def getSumRuntime() {
41 return runtime
42 }
43 def getSuccessRate() {
44 return successfulCheck as double / allCheck
45 }
46
47 def isDifferent(ThreadContext context) {
48 if(active) {
49 val start = System.nanoTime
50 val model = context.model as PartialInterpretation
51 var boolean isDifferent
52 if(this.granularity == DiversityGranularity::Graphwise) {
53 val code = solutionCoder.createRepresentation(model,
54 descriptor.range,
55 descriptor.parallels,
56 descriptor.maxNumber,
57 descriptor.relevantTypes,
58 descriptor.relevantRelations).modelRepresentation.hashCode
59
60 isDifferent = !solutionCodeList.contains(code)
61 } else if(this.granularity == DiversityGranularity::Nodewise){
62 val codes = solutionCoder.createRepresentation(model,
63 descriptor.range,
64 descriptor.parallels,
65 descriptor.maxNumber,
66 descriptor.relevantTypes,
67 descriptor.relevantRelations).modelRepresentation.keySet.map[hashCode].toList
68 val differentCodes = codes.filter[!solutionCodeList.contains(it)]
69 //println(differentCodes.size)
70
71 isDifferent = differentCodes.size>=1
72 } else {
73 throw new UnsupportedOperationException('''Unsupported diversity type: «this.granularity»''')
74 }
75
76 runtime += System.nanoTime - start
77 allCheck++
78 if(isDifferent) { successfulCheck++ }
79 return isDifferent
80 } else {
81 allCheck++
82 successfulCheck++
83 return true
84 }
85 }
86
87 def canBeDifferent(ThreadContext context) {
88 return true
89 }
90
91 def newSolution(ThreadContext context) {
92 if(active) {
93 val start = System.nanoTime
94 val model = context.model as PartialInterpretation
95 if(this.granularity == DiversityGranularity::Graphwise) {
96 val code = solutionCoder.createRepresentation(model,
97 descriptor.range,
98 descriptor.parallels,
99 descriptor.maxNumber,
100 descriptor.relevantTypes,
101 descriptor.relevantRelations).modelRepresentation.hashCode
102
103 solutionCodeList += code.hashCode
104 } else if(this.granularity == DiversityGranularity::Nodewise){
105 val codes = solutionCoder.createRepresentation(model,
106 descriptor.range,
107 descriptor.parallels,
108 descriptor.maxNumber,
109 descriptor.relevantTypes,
110 descriptor.relevantRelations).modelRepresentation.keySet.map[hashCode].toList
111
112 solutionCodeList += codes.map[it.hashCode]
113 } else {
114 throw new UnsupportedOperationException('''Unsupported diversity type: «this.granularity»''')
115 }
116
117 runtime += System.nanoTime - start
118 }
119 }
120} \ 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/SurelyViolatedObjectiveGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend
new file mode 100644
index 00000000..f54a31ca
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend
@@ -0,0 +1,29 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import org.eclipse.viatra.dse.base.ThreadContext
4import org.eclipse.viatra.dse.objectives.IGlobalConstraint
5import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
6
7@FinalFieldsConstructor
8class SurelyViolatedObjectiveGlobalConstraint implements IGlobalConstraint {
9 val ViatraReasonerSolutionSaver solutionSaver
10
11 override init(ThreadContext context) {
12 if (solutionSaver !== null) {
13 return
14 }
15 }
16
17 override createNew() {
18 this
19 }
20
21 override getName() {
22 class.name
23 }
24
25 override checkGlobalConstraint(ThreadContext context) {
26 val bestFitness = DseUtils.caclulateBestPossibleFitness(context)
27 bestFitness.satisifiesHardObjectives && solutionSaver.fitnessMayBeSaved(bestFitness)
28 }
29}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
index aad9a448..7d0a7884 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
@@ -9,7 +9,7 @@ import org.eclipse.viatra.dse.objectives.Comparators
9class UnfinishedMultiplicityObjective implements IObjective { 9class UnfinishedMultiplicityObjective implements IObjective {
10 val MultiplicityGoalConstraintCalculator unfinishedMultiplicity; 10 val MultiplicityGoalConstraintCalculator unfinishedMultiplicity;
11 11
12 public new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) { 12 new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {
13 this.unfinishedMultiplicity = unfinishedMultiplicity 13 this.unfinishedMultiplicity = unfinishedMultiplicity
14 } 14 }
15 15
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
new file mode 100644
index 00000000..6bffeb59
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
@@ -0,0 +1,137 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.HashMap
4import java.util.Map
5import org.eclipse.viatra.dse.api.DSEException
6import org.eclipse.viatra.dse.api.Solution
7import org.eclipse.viatra.dse.api.SolutionTrajectory
8import org.eclipse.viatra.dse.base.ThreadContext
9import org.eclipse.viatra.dse.objectives.Fitness
10import org.eclipse.viatra.dse.objectives.IObjective
11import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper
12import org.eclipse.viatra.dse.solutionstore.SolutionStore.ISolutionSaver
13import org.eclipse.xtend.lib.annotations.Accessors
14
15/**
16 * Based on {@link SolutionStore.BestSolutionSaver}.
17 */
18class ViatraReasonerSolutionSaver implements ISolutionSaver {
19 @Accessors val solutionCopier = new SolutionCopier
20 @Accessors val DiversityChecker diversityChecker
21 val boolean hasExtremalObjectives
22 val int numberOfRequiredSolutions
23 val ObjectiveComparatorHelper comparatorHelper
24 val Map<SolutionTrajectory, Fitness> trajectories = new HashMap
25
26 @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection
27
28 new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) {
29 this.diversityChecker = diversityChecker
30 comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives)
31 hasExtremalObjectives = leveledExtremalObjectives.exists[!empty]
32 this.numberOfRequiredSolutions = numberOfRequiredSolutions
33 }
34
35 override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
36 if (hasExtremalObjectives) {
37 saveBestSolutionOnly(context, id, solutionTrajectory)
38 } else {
39 saveAnyDiverseSolution(context, id, solutionTrajectory)
40 }
41 }
42
43 private def saveBestSolutionOnly(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
44 val fitness = context.lastFitness
45 if (!fitness.satisifiesHardObjectives) {
46 return false
47 }
48 val dominatedTrajectories = newArrayList
49 for (entry : trajectories.entrySet) {
50 val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value)
51 if (isLastFitnessBetter < 0) {
52 // Found a trajectory that dominates the current one, no need to save
53 return false
54 }
55 if (isLastFitnessBetter > 0) {
56 dominatedTrajectories += entry.key
57 }
58 }
59 if (dominatedTrajectories.size == 0 && !needsMoreSolutionsWithSameFitness) {
60 return false
61 }
62 if (!diversityChecker.newSolution(context, id, dominatedTrajectories.map[solution.stateCode])) {
63 return false
64 }
65 // We must save the new trajectory before removing dominated trajectories
66 // to avoid removing the current solution when it is reachable only via dominated trajectories.
67 val solutionSaved = basicSaveSolution(context, id, solutionTrajectory, fitness)
68 for (dominatedTrajectory : dominatedTrajectories) {
69 trajectories -= dominatedTrajectory
70 val dominatedSolution = dominatedTrajectory.solution
71 if (!dominatedSolution.trajectories.remove(dominatedTrajectory)) {
72 throw new DSEException(
73 "Dominated solution is not reachable from dominated trajectory. This should never happen!")
74 }
75 if (dominatedSolution.trajectories.empty) {
76 val dominatedSolutionId = dominatedSolution.stateCode
77 solutionCopier.markAsObsolete(dominatedSolutionId)
78 solutionsCollection -= dominatedSolutionId
79 }
80 }
81 solutionSaved
82 }
83
84 private def saveAnyDiverseSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
85 val fitness = context.lastFitness
86 if (!fitness.satisifiesHardObjectives) {
87 return false
88 }
89 if (!diversityChecker.newSolution(context, id, emptyList)) {
90 return false
91 }
92 basicSaveSolution(context, id, solutionTrajectory, fitness)
93 }
94
95 private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, Fitness fitness) {
96 var boolean solutionSaved = false
97 var dseSolution = solutionsCollection.get(id)
98 if (dseSolution === null) {
99 solutionCopier.copySolution(context, id)
100 dseSolution = new Solution(id, solutionTrajectory)
101 solutionsCollection.put(id, dseSolution)
102 solutionSaved = true
103 } else {
104 solutionSaved = dseSolution.trajectories.add(solutionTrajectory)
105 }
106 if (solutionSaved) {
107 solutionTrajectory.solution = dseSolution
108 trajectories.put(solutionTrajectory, fitness)
109 }
110 solutionSaved
111 }
112
113 def fitnessMayBeSaved(Fitness fitness) {
114 if (!hasExtremalObjectives) {
115 return true
116 }
117 var boolean mayDominate
118 for (existingFitness : trajectories.values) {
119 val isNewFitnessBetter = comparatorHelper.compare(fitness, existingFitness)
120 if (isNewFitnessBetter < 0) {
121 return false
122 }
123 if (isNewFitnessBetter > 0) {
124 mayDominate = true
125 }
126 }
127 mayDominate || needsMoreSolutionsWithSameFitness
128 }
129
130 private def boolean needsMoreSolutionsWithSameFitness() {
131 if (solutionsCollection === null) {
132 // The solutions collection will only be initialized upon saving the first solution.
133 return true
134 }
135 solutionsCollection.size < numberOfRequiredSolutions
136 }
137}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
index 5a528a9e..63d78220 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
@@ -1,5 +1,6 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import com.google.common.collect.ImmutableList
3import java.util.ArrayList 4import java.util.ArrayList
4import java.util.Collection 5import java.util.Collection
5import org.eclipse.viatra.dse.objectives.Comparators 6import org.eclipse.viatra.dse.objectives.Comparators
@@ -12,25 +13,35 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification
12import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 13import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
13 14
14class WF2ObjectiveConverter { 15class WF2ObjectiveConverter {
15 16 static val UNFINISHED_WFS_NAME = "unfinishedWFs"
17 static val INVALIDATED_WFS_NAME = "invalidatedWFs"
18
16 def createCompletenessObjective( 19 def createCompletenessObjective(
17 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) 20 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) {
18 { 21 // createConstraintObjective(UNFINISHED_WFS_NAME, unfinishedWF)
19 val res = new ConstraintsObjective('''unfinishedWFs''', 22 new UnfinishedWFObjective(unfinishedWF)
20 unfinishedWF.map[ 23 }
21 new QueryConstraint(it.fullyQualifiedName,it,2.0) 24
22 ].toList 25 def createInvalidationObjective(
26 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {
27 createConstraintObjective(INVALIDATED_WFS_NAME, invalidatedByWF)
28 }
29
30 def IGlobalConstraint createInvalidationGlobalConstraint(
31 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {
32 new ModelQueriesGlobalConstraint(INVALIDATED_WFS_NAME, new ArrayList(invalidatedByWF))
33 }
34
35 private def createConstraintObjective(String name,
36 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries) {
37 val res = new ConstraintsObjective(
38 name,
39 ImmutableList.copyOf(queries.map [
40 new QueryConstraint(it.fullyQualifiedName, it, 1.0)
41 ])
23 ) 42 )
24 res.withComparator(Comparators.LOWER_IS_BETTER) 43 res.withComparator(Comparators.LOWER_IS_BETTER)
25 res.level = 2 44 res.level = 2
26 return res 45 res
27 }
28
29 def IGlobalConstraint createInvalidationObjective(
30 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF)
31 {
32 return new ModelQueriesGlobalConstraint('''invalidatedWFs''',
33 new ArrayList(invalidatedByWF)
34 )
35 } 46 }
36} \ No newline at end of file 47}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend
new file mode 100644
index 00000000..241bef2a
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend
@@ -0,0 +1,102 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2
3import java.util.Comparator
4import org.eclipse.viatra.dse.base.ThreadContext
5import org.eclipse.xtend.lib.annotations.Accessors
6import org.eclipse.xtend.lib.annotations.Data
7
8abstract class ObjectiveThreshold {
9 public static val NO_THRESHOLD = new hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold {
10 override isHard() {
11 false
12 }
13
14 override satisfiesThreshold(double cost, Comparator<Double> comparator) {
15 true
16 }
17 }
18
19 private new() {
20 }
21
22 def boolean isHard() {
23 true
24 }
25
26 def boolean satisfiesThreshold(double cost, Comparator<Double> comparator)
27
28 @Data
29 static class Exclusive extends ObjectiveThreshold {
30 val double threshold
31
32 override satisfiesThreshold(double cost, Comparator<Double> comparator) {
33 comparator.compare(threshold, cost) > 0
34 }
35 }
36
37 @Data
38 static class Inclusive extends ObjectiveThreshold {
39 val double threshold
40
41 override satisfiesThreshold(double cost, Comparator<Double> comparator) {
42 comparator.compare(threshold, cost) >= 0
43 }
44 }
45}
46
47abstract class AbstractThreeValuedObjective implements IThreeValuedObjective {
48 @Accessors val String name
49 @Accessors ObjectiveKind kind
50 @Accessors ObjectiveThreshold threshold
51 @Accessors int level
52
53 protected new(String name, ObjectiveKind kind, ObjectiveThreshold threshold, int level) {
54 this.name = name
55 this.kind = kind
56 this.threshold = threshold
57 this.level = level
58 }
59
60 abstract def double getLowestPossibleFitness(ThreadContext threadContext)
61
62 abstract def double getHighestPossibleFitness(ThreadContext threadContext)
63
64 override getWorstPossibleFitness(ThreadContext threadContext) {
65 switch (kind) {
66 case LOWER_IS_BETTER:
67 getHighestPossibleFitness(threadContext)
68 case HIGHER_IS_BETTER:
69 getLowestPossibleFitness(threadContext)
70 default:
71 throw new IllegalStateException("Unknown three valued objective kind: " + kind)
72 }
73 }
74
75 override getBestPossibleFitness(ThreadContext threadContext) {
76 switch (kind) {
77 case LOWER_IS_BETTER:
78 getLowestPossibleFitness(threadContext)
79 case HIGHER_IS_BETTER:
80 getHighestPossibleFitness(threadContext)
81 default:
82 throw new IllegalStateException("Unknown three valued objective kind: " + kind)
83 }
84 }
85
86 override isHardObjective() {
87 threshold.hard
88 }
89
90 override satisifiesHardObjective(Double fitness) {
91 threshold.satisfiesThreshold(fitness, comparator)
92 }
93
94 override getComparator() {
95 kind.comparator
96 }
97
98 override setComparator(Comparator<Double> comparator) {
99 kind = ObjectiveKind.fromComparator(comparator)
100 }
101
102}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend
new file mode 100644
index 00000000..4a870a3e
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend
@@ -0,0 +1,10 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2
3import org.eclipse.viatra.dse.base.ThreadContext
4import org.eclipse.viatra.dse.objectives.IObjective
5
6interface IThreeValuedObjective extends IObjective {
7 def Double getWorstPossibleFitness(ThreadContext threadContext)
8
9 def Double getBestPossibleFitness(ThreadContext threadContext)
10}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java
new file mode 100644
index 00000000..f65428fe
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java
@@ -0,0 +1,36 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization;
2
3import java.util.Comparator;
4
5import org.eclipse.viatra.dse.objectives.Comparators;
6
7public enum ObjectiveKind {
8 LOWER_IS_BETTER {
9
10 @Override
11 public Comparator<Double> getComparator() {
12 return Comparators.LOWER_IS_BETTER;
13 }
14
15 },
16 HIGHER_IS_BETTER {
17
18 @Override
19 public Comparator<Double> getComparator() {
20 return Comparators.HIGHER_IS_BETTER;
21 }
22
23 };
24
25 public abstract Comparator<Double> getComparator();
26
27 public static ObjectiveKind fromComparator(Comparator<Double> comparator) {
28 if (Comparators.LOWER_IS_BETTER.equals(comparator)) {
29 return ObjectiveKind.LOWER_IS_BETTER;
30 } else if (Comparators.HIGHER_IS_BETTER.equals(comparator)) {
31 return ObjectiveKind.HIGHER_IS_BETTER;
32 } else {
33 throw new IllegalStateException("Only LOWER_IS_BETTER and HIGHER_IS_BETTER comparators are supported.");
34 }
35 }
36}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend
new file mode 100644
index 00000000..e2585c83
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend
@@ -0,0 +1,85 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2
3import com.google.common.collect.ImmutableList
4import java.util.Collection
5import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.query.runtime.api.IPatternMatch
7import org.eclipse.viatra.query.runtime.api.IQuerySpecification
8import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
9import org.eclipse.xtend.lib.annotations.Data
10
11@Data
12class ThreeValuedCostElement {
13 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentMatchQuery
14 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayMatchQuery
15 val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustMatchQuery
16 val int weight
17}
18
19class ThreeValuedCostObjective extends AbstractThreeValuedObjective {
20 val Collection<ThreeValuedCostElement> costElements
21 Collection<CostElementMatchers> matchers
22
23 new(String name, Collection<ThreeValuedCostElement> costElements, ObjectiveKind kind, ObjectiveThreshold threshold,
24 int level) {
25 super(name, kind, threshold, level)
26 this.costElements = costElements
27 }
28
29 override createNew() {
30 new ThreeValuedCostObjective(name, costElements, kind, threshold, level)
31 }
32
33 override init(ThreadContext context) {
34 val queryEngine = context.queryEngine
35 matchers = ImmutableList.copyOf(costElements.map [ element |
36 new CostElementMatchers(
37 queryEngine.getMatcher(element.currentMatchQuery),
38 queryEngine.getMatcher(element.mayMatchQuery),
39 queryEngine.getMatcher(element.mustMatchQuery),
40 element.weight
41 )
42 ])
43 }
44
45 override getFitness(ThreadContext context) {
46 var int cost = 0
47 for (matcher : matchers) {
48 cost += matcher.weight * matcher.currentMatcher.countMatches
49 }
50 cost as double
51 }
52
53 override getLowestPossibleFitness(ThreadContext threadContext) {
54 var int cost = 0
55 for (matcher : matchers) {
56 if (matcher.weight >= 0) {
57 cost += matcher.weight * matcher.mustMatcher.countMatches
58 } else if (matcher.mayMatcher.countMatches > 0) {
59 // TODO Count may matches.
60 return Double.NEGATIVE_INFINITY
61 }
62 }
63 cost as double
64 }
65
66 override getHighestPossibleFitness(ThreadContext threadContext) {
67 var int cost = 0
68 for (matcher : matchers) {
69 if (matcher.weight <= 0) {
70 cost += matcher.weight * matcher.mustMatcher.countMatches
71 } else if (matcher.mayMatcher.countMatches > 0) {
72 return Double.POSITIVE_INFINITY
73 }
74 }
75 cost as double
76 }
77
78 @Data
79 private static class CostElementMatchers {
80 val ViatraQueryMatcher<? extends IPatternMatch> currentMatcher
81 val ViatraQueryMatcher<? extends IPatternMatch> mayMatcher
82 val ViatraQueryMatcher<? extends IPatternMatch> mustMatcher
83 val int weight
84 }
85}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-03 16:47:19 +0000