diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-07-05 16:31:32 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-07-05 16:31:32 +0200 |
commit | adce403870ea34f79cf2c59b88cdb5b2dcb438a8 (patch) | |
tree | 64a4aeedb53d642c1a60c498be26213b41547497 /Solvers | |
parent | Adding multiple model generation support for the alloy solver. (diff) | |
download | VIATRA-Generator-adce403870ea34f79cf2c59b88cdb5b2dcb438a8.tar.gz VIATRA-Generator-adce403870ea34f79cf2c59b88cdb5b2dcb438a8.tar.zst VIATRA-Generator-adce403870ea34f79cf2c59b88cdb5b2dcb438a8.zip |
Support for generationg multiple difference models by VIATRA-Solver
Diffstat (limited to 'Solvers')
10 files changed, 166 insertions, 36 deletions
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 1653226d..656f806b 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,7 +1,5 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider |
@@ -9,15 +7,13 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRule | |||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
10 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 8 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
11 | import java.util.Collection | 9 | import java.util.Collection |
12 | import java.util.LinkedHashMap | ||
13 | import java.util.List | 10 | import java.util.List |
14 | import org.eclipse.viatra.query.runtime.api.GenericPatternMatch | 11 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
15 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 12 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
16 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 13 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
17 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 14 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
18 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 15 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
19 | import org.eclipse.xtend.lib.annotations.Data | 16 | import org.eclipse.xtend.lib.annotations.Data |
20 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
21 | 17 | ||
22 | class ModelGenerationStatistics { | 18 | class ModelGenerationStatistics { |
23 | public var long transformationExecutionTime = 0 | 19 | public var long transformationExecutionTime = 0 |
@@ -36,6 +32,8 @@ class ModelGenerationStatistics { | |||
36 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | 32 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF |
37 | 33 | ||
38 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | 34 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF |
35 | |||
36 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | ||
39 | } | 37 | } |
40 | enum TypeInferenceMethod { | 38 | enum TypeInferenceMethod { |
41 | Generic, PreliminaryAnalysis | 39 | Generic, PreliminaryAnalysis |
@@ -72,7 +70,8 @@ class ModelGenerationMethodProvider { | |||
72 | relationRefinementRules.values, | 70 | relationRefinementRules.values, |
73 | unfinishedMultiplicities, | 71 | unfinishedMultiplicities, |
74 | unfinishedWF, | 72 | unfinishedWF, |
75 | invalidWF | 73 | invalidWF, |
74 | queries.allQueries | ||
76 | ) | 75 | ) |
77 | } | 76 | } |
78 | } | 77 | } |
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 cac614ad..cc8860b4 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 | |||
@@ -19,6 +19,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | |||
19 | import org.eclipse.xtend.lib.annotations.Data | 19 | import org.eclipse.xtend.lib.annotations.Data |
20 | 20 | ||
21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
22 | import java.util.Collection | ||
22 | 23 | ||
23 | @Data class GeneratedPatterns { | 24 | @Data class GeneratedPatterns { |
24 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries | 25 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries |
@@ -27,6 +28,7 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
27 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries | 28 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries |
28 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | 29 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries |
29 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries | 30 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries |
31 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries | ||
30 | } | 32 | } |
31 | 33 | ||
32 | class PatternProvider { | 34 | class PatternProvider { |
@@ -91,7 +93,8 @@ class PatternProvider { | |||
91 | unfinishedMultiplicityQueries, | 93 | unfinishedMultiplicityQueries, |
92 | refineObjectsQueries, | 94 | refineObjectsQueries, |
93 | refineTypeQueries, | 95 | refineTypeQueries, |
94 | refineRelationQueries | 96 | refineRelationQueries, |
97 | queries.values | ||
95 | ) | 98 | ) |
96 | } | 99 | } |
97 | } | 100 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/.classpath b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/.classpath index 1c96fe2f..2b46fc9b 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/.classpath +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/.classpath | |||
@@ -4,5 +4,6 @@ | |||
4 | <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> | 4 | <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> |
5 | <classpathentry kind="src" path="src"/> | 5 | <classpathentry kind="src" path="src"/> |
6 | <classpathentry kind="src" path="xtend-gen"/> | 6 | <classpathentry kind="src" path="xtend-gen"/> |
7 | <classpathentry kind="src" path="src-gen/"/> | ||
7 | <classpathentry kind="output" path="bin"/> | 8 | <classpathentry kind="output" path="bin"/> |
8 | </classpath> | 9 | </classpath> |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/META-INF/MANIFEST.MF index 24dbd918..f0d42f2c 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/META-INF/MANIFEST.MF | |||
@@ -1,15 +1,14 @@ | |||
1 | Manifest-Version: 1.0 | 1 | Manifest-Version: 1.0 |
2 | Bundle-ManifestVersion: 2 | 2 | Bundle-ManifestVersion: 2 |
3 | Bundle-Name: Partialinterpretation2logic | 3 | Bundle-Name: Partialinterpretation2logic |
4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic | 4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic |
5 | Bundle-Version: 1.0.0.qualifier | 5 | Bundle-Version: 1.0.0.qualifier |
6 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | 6 | Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic |
7 | Require-Bundle: com.google.guava, | 7 | Require-Bundle: com.google.guava, |
8 | org.eclipse.xtext.xbase.lib, | 8 | org.eclipse.xtext.xbase.lib, |
9 | org.eclipse.xtend.lib, | 9 | org.eclipse.xtend.lib, |
10 | org.eclipse.xtend.lib.macro, | 10 | org.eclipse.xtend.lib.macro, |
11 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | 11 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", |
12 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | 12 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", |
13 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0" | 13 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0" |
14 | Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic | 14 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 |
15 | |||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/build.properties b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/build.properties index 41eb6ade..aed85a48 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/build.properties +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/build.properties | |||
@@ -1,4 +1,5 @@ | |||
1 | source.. = src/ | ||
2 | output.. = bin/ | ||
3 | bin.includes = META-INF/,\ | 1 | bin.includes = META-INF/,\ |
4 | . | 2 | . |
3 | source.. = src/,\ | ||
4 | src-gen/ | ||
5 | output.. = bin/ | ||
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 bc965aa4..0e0940bd 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 | |||
@@ -17,7 +17,6 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | |||
17 | org.eclipse.viatra.query.runtime.matchers;bundle-version="1.5.0", | 17 | org.eclipse.viatra.query.runtime.matchers;bundle-version="1.5.0", |
18 | org.eclipse.viatra.query.runtime;bundle-version="1.5.0", | 18 | org.eclipse.viatra.query.runtime;bundle-version="1.5.0", |
19 | org.eclipse.viatra.dse;bundle-version="0.15.0", | 19 | org.eclipse.viatra.dse;bundle-version="0.15.0", |
20 | org.eclipse.viatra.dse.genetic;bundle-version="0.15.0", | ||
21 | org.eclipse.emf.ecore.edit;bundle-version="2.9.0" | 20 | org.eclipse.emf.ecore.edit;bundle-version="2.9.0" |
22 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | 21 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 |
23 | Import-Package: org.apache.log4j | 22 | Import-Package: org.apache.log4j |
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 5d8859bd..fd70688b 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 | |||
@@ -25,6 +25,18 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer | |||
25 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel | 25 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel |
26 | import org.eclipse.viatra.dse.solutionstore.SolutionStore | 26 | import org.eclipse.viatra.dse.solutionstore.SolutionStore |
27 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory | 27 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory |
28 | import java.util.List | ||
29 | import java.util.Map | ||
30 | import org.eclipse.viatra.dse.base.ThreadContext | ||
31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
32 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
33 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
34 | import java.util.Collection | ||
35 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
36 | import java.util.SortedMap | ||
37 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
38 | import org.eclipse.emf.ecore.EObject | ||
39 | import org.eclipse.emf.common.util.EList | ||
28 | 40 | ||
29 | class ViatraReasoner extends LogicReasoner{ | 41 | class ViatraReasoner extends LogicReasoner{ |
30 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() | 42 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() |
@@ -42,6 +54,9 @@ class ViatraReasoner extends LogicReasoner{ | |||
42 | this.inconsistencyDetector = inconsistencyDetector | 54 | this.inconsistencyDetector = inconsistencyDetector |
43 | } | 55 | } |
44 | 56 | ||
57 | public static var Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns = null | ||
58 | //public static var List<SortedMap<String, Integer>> additionalMatches = null | ||
59 | |||
45 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | 60 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { |
46 | val viatraConfig = configuration.asConfig | 61 | val viatraConfig = configuration.asConfig |
47 | val DesignSpaceExplorer dse = new DesignSpaceExplorer(); | 62 | val DesignSpaceExplorer dse = new DesignSpaceExplorer(); |
@@ -71,6 +86,7 @@ class ViatraReasoner extends LogicReasoner{ | |||
71 | viatraConfig.nameNewElements, | 86 | viatraConfig.nameNewElements, |
72 | viatraConfig.typeInferenceMethod | 87 | viatraConfig.typeInferenceMethod |
73 | ) | 88 | ) |
89 | allPatterns = method.allPatterns | ||
74 | 90 | ||
75 | dse.addObjective(new ModelGenerationCompositeObjective( | 91 | dse.addObjective(new ModelGenerationCompositeObjective( |
76 | new ScopeObjective, | 92 | new ScopeObjective, |
@@ -83,7 +99,7 @@ class ViatraReasoner extends LogicReasoner{ | |||
83 | dse.addGlobalConstraint(additionalConstraint.apply(method)) | 99 | dse.addGlobalConstraint(additionalConstraint.apply(method)) |
84 | } | 100 | } |
85 | 101 | ||
86 | dse.setInitialModel(emptySolution) | 102 | dse.setInitialModel(emptySolution,false) |
87 | 103 | ||
88 | var IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) { | 104 | var IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) { |
89 | new NeighbourhoodBasedStateCoderFactory | 105 | new NeighbourhoodBasedStateCoderFactory |
@@ -107,7 +123,8 @@ class ViatraReasoner extends LogicReasoner{ | |||
107 | val strategy = new BestFirstStrategyForModelGeneration( | 123 | val strategy = new BestFirstStrategyForModelGeneration( |
108 | workspace,inconsistencyDetector, | 124 | workspace,inconsistencyDetector, |
109 | viatraConfig.inconsistencDetectorConfiguration, | 125 | viatraConfig.inconsistencDetectorConfiguration, |
110 | viatraConfig.diversityRequirement) | 126 | viatraConfig.diversityRequirement/*, |
127 | method.allPatterns*/) | ||
111 | 128 | ||
112 | val transformationTime = System.nanoTime - transformationStartTime | 129 | val transformationTime = System.nanoTime - transformationStartTime |
113 | val solverStartTime = System.nanoTime | 130 | val solverStartTime = System.nanoTime |
@@ -124,14 +141,15 @@ class ViatraReasoner extends LogicReasoner{ | |||
124 | val solverTime = System.nanoTime - solverStartTime | 141 | val solverTime = System.nanoTime - solverStartTime |
125 | 142 | ||
126 | val statecoderFinal = statecoder | 143 | val statecoderFinal = statecoder |
144 | //additionalMatches = strategy.solutionStoreWithCopy.additionalMatches | ||
127 | val statistics = createStatistics => [ | 145 | val statistics = createStatistics => [ |
128 | //it.solverTime = viatraConfig.runtimeLimit | 146 | //it.solverTime = viatraConfig.runtimeLimit |
129 | it.solverTime = (solverTime/1000000) as int | 147 | it.solverTime = (solverTime/1000000) as int |
130 | it.transformationTime = (transformationTime/1000000) as int | 148 | it.transformationTime = (transformationTime/1000000) as int |
131 | for(x : 0..<strategy.solutionStoreWithCopy.allRuntimes.size) { | 149 | for(x : 0..<strategy.solutionStoreWithCopy.allRuntimes.size) { |
132 | it.entries += createIntStatisticEntry => [ | 150 | it.entries += createIntStatisticEntry => [ |
133 | it.name = '''_Sulution«x»FoundAt''' | 151 | it.name = '''_Solution«x»FoundAt''' |
134 | it.value = strategy.solutionStoreWithCopy.allRuntimes.get(x).intValue | 152 | it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int |
135 | ] | 153 | ] |
136 | } | 154 | } |
137 | it.entries += createIntStatisticEntry => [ | 155 | it.entries += createIntStatisticEntry => [ |
@@ -179,7 +197,7 @@ class ViatraReasoner extends LogicReasoner{ | |||
179 | */ | 197 | */ |
180 | return factory.createModelResult => [ | 198 | return factory.createModelResult => [ |
181 | it.problem = problem | 199 | it.problem = problem |
182 | it.trace = null | 200 | it.trace = strategy.solutionStoreWithCopy.copyTraces |
183 | it.representation += strategy.solutionStoreWithCopy.solutions | 201 | it.representation += strategy.solutionStoreWithCopy.solutions |
184 | it.statistics = statistics | 202 | it.statistics = statistics |
185 | ] | 203 | ] |
@@ -199,11 +217,14 @@ class ViatraReasoner extends LogicReasoner{ | |||
199 | sc.sumStatecoderRuntime | 217 | sc.sumStatecoderRuntime |
200 | } | 218 | } |
201 | 219 | ||
202 | override getInterpretation(ModelResult modelResult) { | 220 | override getInterpretations(ModelResult modelResult) { |
203 | return new PartialModelAsLogicInterpretation | 221 | val indexes = 0..<modelResult.representation.size |
222 | val traces = modelResult.trace as List<Map<EObject, EObject>>; | ||
223 | val res = indexes.map[i | new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation,traces.get(i))].toList | ||
224 | return res | ||
204 | } | 225 | } |
205 | 226 | ||
206 | def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) { | 227 | private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) { |
207 | if(configuration instanceof ViatraReasonerConfiguration) { | 228 | if(configuration instanceof ViatraReasonerConfiguration) { |
208 | return configuration | 229 | return configuration |
209 | } else throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''') | 230 | } else throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''') |
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 5a6fee2c..862ba245 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 | |||
@@ -11,12 +11,17 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse; | |||
11 | 11 | ||
12 | import java.util.ArrayList; | 12 | import java.util.ArrayList; |
13 | import java.util.Arrays; | 13 | import java.util.Arrays; |
14 | import java.util.Collection; | ||
14 | import java.util.Collections; | 15 | import java.util.Collections; |
15 | import java.util.Comparator; | 16 | import java.util.Comparator; |
16 | import java.util.Iterator; | 17 | import java.util.Iterator; |
18 | import java.util.LinkedList; | ||
17 | import java.util.List; | 19 | import java.util.List; |
18 | import java.util.PriorityQueue; | 20 | import java.util.PriorityQueue; |
19 | import java.util.Random; | 21 | import java.util.Random; |
22 | import java.util.SortedMap; | ||
23 | import java.util.TreeMap; | ||
24 | import java.util.TreeSet; | ||
20 | 25 | ||
21 | import org.apache.log4j.Logger; | 26 | import org.apache.log4j.Logger; |
22 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; | 27 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; |
@@ -24,6 +29,10 @@ import org.eclipse.viatra.dse.base.ThreadContext; | |||
24 | import org.eclipse.viatra.dse.objectives.Fitness; | 29 | import org.eclipse.viatra.dse.objectives.Fitness; |
25 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; | 30 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; |
26 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; | 31 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; |
32 | import org.eclipse.viatra.query.runtime.api.IPatternMatch; | ||
33 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; | ||
34 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher; | ||
35 | import org.eclipse.viatra.query.runtime.exception.ViatraQueryException; | ||
27 | 36 | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | 37 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; |
29 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | 38 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; |
@@ -57,12 +66,15 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
57 | private SolutionStoreWithCopy solutionStoreWithCopy; | 66 | private SolutionStoreWithCopy solutionStoreWithCopy; |
58 | private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor; | 67 | private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor; |
59 | private int numberOfStatecoderFail=0; | 68 | private int numberOfStatecoderFail=0; |
69 | //Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> additionalPatterns = null; | ||
70 | //List<ViatraQueryMatcher<? extends IPatternMatch>> additionalMatchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); | ||
60 | 71 | ||
61 | private int maxDepth = Integer.MAX_VALUE; | 72 | private int maxDepth = Integer.MAX_VALUE; |
62 | private boolean isInterrupted = false; | 73 | private boolean isInterrupted = false; |
63 | //private boolean backTrackIfSolution = true; | 74 | //private boolean backTrackIfSolution = true; |
64 | private boolean onlyBetterFirst = false; | 75 | private boolean onlyBetterFirst = false; |
65 | 76 | ||
77 | |||
66 | private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore; | 78 | private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore; |
67 | private Logger logger = Logger.getLogger(IStrategy.class); | 79 | private Logger logger = Logger.getLogger(IStrategy.class); |
68 | 80 | ||
@@ -84,12 +96,15 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
84 | 96 | ||
85 | } | 97 | } |
86 | 98 | ||
87 | public BestFirstStrategyForModelGeneration(ReasonerWorkspace workspace, LogicReasoner reasoner, LogicSolverConfiguration configuration, DiversityDescriptor descriptor) { | 99 | public BestFirstStrategyForModelGeneration( |
88 | this.maxDepth = Integer.MAX_VALUE; | 100 | ReasonerWorkspace workspace, LogicReasoner reasoner, LogicSolverConfiguration configuration, DiversityDescriptor descriptor/*, |
101 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> additionalPatterns*/) { | ||
102 | this.maxDepth = Integer.MAX_VALUE; | ||
89 | this.workspace = workspace; | 103 | this.workspace = workspace; |
90 | this.reasoner = reasoner; | 104 | this.reasoner = reasoner; |
91 | this.configuration = configuration; | 105 | this.configuration = configuration; |
92 | this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(descriptor); | 106 | this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(descriptor); |
107 | //this.additionalPatterns = additionalPatterns; | ||
93 | } | 108 | } |
94 | 109 | ||
95 | @Override | 110 | @Override |
@@ -108,6 +123,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
108 | return objectiveComparatorHelper.compare(o2.fitness, o1.fitness); | 123 | return objectiveComparatorHelper.compare(o2.fitness, o1.fitness); |
109 | } | 124 | } |
110 | }; | 125 | }; |
126 | |||
127 | |||
111 | 128 | ||
112 | trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); | 129 | trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); |
113 | 130 | ||
@@ -127,6 +144,18 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
127 | 144 | ||
128 | @Override | 145 | @Override |
129 | public void explore() { | 146 | public void explore() { |
147 | |||
148 | /*if(this.additionalPatterns!=null) { | ||
149 | for (IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> additionalPattern : additionalPatterns) { | ||
150 | try { | ||
151 | this.additionalMatchers.add(additionalPattern.getMatcher(context.getQueryEngine())); | ||
152 | } catch (ViatraQueryException e) { | ||
153 | // TODO Auto-generated catch block | ||
154 | e.printStackTrace(); | ||
155 | } | ||
156 | } | ||
157 | }*/ | ||
158 | |||
130 | final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); | 159 | final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); |
131 | 160 | ||
132 | boolean globalConstraintsAreSatisfied = context.checkGlobalConstraints(); | 161 | boolean globalConstraintsAreSatisfied = context.checkGlobalConstraints(); |
@@ -210,9 +239,15 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
210 | final Fitness nextFitness = context.calculateFitness(); | 239 | final Fitness nextFitness = context.calculateFitness(); |
211 | if (nextFitness.isSatisifiesHardObjectives()) { | 240 | if (nextFitness.isSatisifiesHardObjectives()) { |
212 | if(solutionStoreWithDiversityDescriptor.isDifferent(context)) { | 241 | if(solutionStoreWithDiversityDescriptor.isDifferent(context)) { |
213 | solutionStoreWithCopy.newSolution(context); | 242 | /*SortedMap<String, Integer> x = new TreeMap<String, Integer>(); |
243 | for(ViatraQueryMatcher<? extends IPatternMatch> additioanMatcher : this.additionalMatchers) { | ||
244 | x.put(additioanMatcher.getPatternName(),additioanMatcher.countMatches()); | ||
245 | }*/ | ||
246 | |||
247 | solutionStoreWithCopy.newSolution(context/*,x*/); | ||
214 | solutionStoreWithDiversityDescriptor.newSolution(context); | 248 | solutionStoreWithDiversityDescriptor.newSolution(context); |
215 | solutionStore.newSolution(context); | 249 | solutionStore.newSolution(context); |
250 | |||
216 | logger.debug("Found a solution."); | 251 | logger.debug("Found a solution."); |
217 | } | 252 | } |
218 | } | 253 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend index b2a7e3f5..56c3c852 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend | |||
@@ -1,16 +1,68 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | ||
13 | import java.util.HashMap | ||
14 | import java.util.List | ||
15 | import java.util.Map | ||
16 | import org.eclipse.emf.ecore.EObject | ||
17 | |||
18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink | ||
8 | 21 | ||
9 | class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | 22 | class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ |
23 | val PartialInterpretation partialInterpretation | ||
24 | val Map<EObject, EObject> trace; | ||
25 | val Map<TypeDeclaration,PartialTypeInterpratation> type2Interpretation | ||
26 | val Map<RelationDeclaration,PartialRelationInterpretation> relation2Interpretation | ||
27 | val Map<DefinedElement,DefinedElement> elementBackwardTrace | ||
10 | 28 | ||
29 | new(PartialInterpretation partialInterpretation, Map<EObject, EObject> forwardMap) { | ||
30 | this.partialInterpretation = partialInterpretation | ||
31 | this.trace = forwardMap | ||
32 | this.type2Interpretation = initTypes(partialInterpretation.partialtypeinterpratation) | ||
33 | this.relation2Interpretation = initRelations(partialInterpretation.partialrelationinterpretation) | ||
34 | this.elementBackwardTrace = initElementBackwardTrace(trace) | ||
35 | } | ||
36 | |||
37 | def initTypes(List<PartialTypeInterpratation> types) { | ||
38 | types.toMap[it.interpretationOf] | ||
39 | } | ||
40 | def initRelations(List<PartialRelationInterpretation> relations) { | ||
41 | relations.toMap[it.interpretationOf] | ||
42 | } | ||
43 | def initElementBackwardTrace(Map<EObject, EObject> trace) { | ||
44 | val entryBackwardMap = new HashMap | ||
45 | for(entry: trace.entrySet) { | ||
46 | if(entry.key instanceof DefinedElement) { | ||
47 | entryBackwardMap.put(entry.value as DefinedElement, entry.key as DefinedElement) | ||
48 | } | ||
49 | } | ||
50 | return entryBackwardMap | ||
51 | } | ||
11 | 52 | ||
12 | override getElements(Type type) { | 53 | override getElements(Type type) { |
13 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 54 | val t1 = type.lookup(trace) as TypeDeclaration |
55 | val t2 = t1.lookup(this.type2Interpretation) | ||
56 | return t2.elements.map[it.elementLookupBackward] | ||
57 | } | ||
58 | |||
59 | def elementLookupForward(DefinedElement e) { | ||
60 | if(this.trace.containsKey(e)) return e.lookup(trace) as DefinedElement | ||
61 | else return e; | ||
62 | } | ||
63 | def elementLookupBackward(DefinedElement e) { | ||
64 | if(this.elementBackwardTrace.containsKey(e)) return e.lookup(this.elementBackwardTrace) | ||
65 | else return e; | ||
14 | } | 66 | } |
15 | 67 | ||
16 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | 68 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { |
@@ -18,13 +70,22 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | |||
18 | } | 70 | } |
19 | 71 | ||
20 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | 72 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { |
21 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 73 | if(parameterSubstitution.size == 2) { |
74 | val param1 = (parameterSubstitution.get(0) as DefinedElement).elementLookupForward | ||
75 | val param2 = (parameterSubstitution.get(1) as DefinedElement).elementLookupForward | ||
76 | val r1 = relation.lookup(trace) as RelationDeclaration | ||
77 | val r2 = r1.lookup(this.relation2Interpretation) | ||
78 | val links = r2.relationlinks.filter(BinaryElementRelationLink) | ||
79 | val existLink = links.exists[it.param1 == param1 && it.param2 == param2] | ||
80 | //println(existLink) | ||
81 | return existLink | ||
82 | } else throw new UnsupportedOperationException | ||
22 | } | 83 | } |
23 | 84 | ||
24 | override getInterpretation(ConstantDeclaration constant) { | 85 | override getInterpretation(ConstantDeclaration constant) { |
25 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 86 | throw new UnsupportedOperationException("TODO: auto-generated method stub") |
26 | } | 87 | } |
27 | 88 | ||
28 | override getMinimalInteger() { 0 } | 89 | override getMinimalInteger() {0} |
29 | override getMaximalInteger() {0 } | 90 | override getMaximalInteger() {0} |
30 | } \ No newline at end of file | 91 | } \ 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/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend index 679b9600..a8b7301e 100644 --- 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 | |||
@@ -7,16 +7,24 @@ import org.eclipse.emf.ecore.EObject | |||
7 | import java.util.Map | 7 | import java.util.Map |
8 | import org.eclipse.emf.ecore.util.EcoreUtil | 8 | import org.eclipse.emf.ecore.util.EcoreUtil |
9 | import org.eclipse.viatra.dse.base.ThreadContext | 9 | import org.eclipse.viatra.dse.base.ThreadContext |
10 | import java.util.TreeMap | ||
11 | import java.util.SortedMap | ||
10 | 12 | ||
11 | class SolutionStoreWithCopy { | 13 | class SolutionStoreWithCopy { |
12 | 14 | ||
13 | long runtime = 0 | 15 | long runtime = 0 |
14 | List<PartialInterpretation> solutions = new LinkedList | 16 | List<PartialInterpretation> solutions = new LinkedList |
17 | //public List<SortedMap<String,Integer>> additionalMatches = new LinkedList | ||
15 | List<Map<EObject,EObject>> copyTraces = new LinkedList | 18 | List<Map<EObject,EObject>> copyTraces = new LinkedList |
16 | 19 | ||
17 | long sartTime = System.nanoTime | 20 | long sartTime = System.nanoTime |
18 | List<Long> solutionTimes = new LinkedList | 21 | List<Long> solutionTimes = new LinkedList |
19 | 22 | ||
23 | /*def newSolution(ThreadContext context, SortedMap<String,Integer> additonalMatch) { | ||
24 | additionalMatches+= additonalMatch | ||
25 | newSolution(context) | ||
26 | }*/ | ||
27 | |||
20 | def newSolution(ThreadContext context) { | 28 | def newSolution(ThreadContext context) { |
21 | //print(System.nanoTime-initTime + ";") | 29 | //print(System.nanoTime-initTime + ";") |
22 | val copyStart = System.nanoTime | 30 | val copyStart = System.nanoTime |
@@ -38,4 +46,7 @@ class SolutionStoreWithCopy { | |||
38 | def getSolutions() { | 46 | def getSolutions() { |
39 | solutions | 47 | solutions |
40 | } | 48 | } |
49 | def getCopyTraces() { | ||
50 | return copyTraces | ||
51 | } | ||
41 | } \ No newline at end of file | 52 | } \ No newline at end of file |