diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse')
3 files changed, 116 insertions, 9 deletions
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 |