1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
|
/*******************************************************************************
* Copyright (c) 2010-2017, Andras Szabolcs Nagy and Daniel Varro
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
* Contributors:
* Andras Szabolcs Nagy - initial API and implementation
*******************************************************************************/
package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse;
import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
import java.util.Comparator;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.PriorityQueue;
import java.util.Random;
import org.apache.log4j.Logger;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.util.EcoreUtil;
import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;
import org.eclipse.viatra.dse.base.ThreadContext;
import org.eclipse.viatra.dse.objectives.Fitness;
import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper;
import org.eclipse.viatra.dse.solutionstore.SolutionStore;
import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine;
import org.eclipse.viatra.query.runtime.api.IPatternMatch;
import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;
import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher;
import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult;
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver;
import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser;
import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration;
import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
/**
* This exploration strategy eventually explorers the whole design space but
* goes in the most promising directions first, based on the {@link Fitness}.
*
* There are a few parameter to tune such as
* <ul>
* <li>maximum depth</li>
* <li>continue the exploration from a state that satisfies the hard objectives
* (the default that it will backtrack),</li>
* <li>whether to continue the exploration from the newly explored state if it
* is at least equally good than the previous one or only if it is better
* (default is "at least equally good").</li>
* </ul>
*
*/
public class BestFirstStrategyForModelGeneration implements IStrategy {
// Services and Configuration
private ThreadContext context;
private ReasonerWorkspace workspace;
private ViatraReasonerConfiguration configuration;
private ModelGenerationMethod method;
private PartialInterpretation2Logic partialInterpretation2Logic = new PartialInterpretation2Logic();
private Comparator<TrajectoryWithFitness> comparator;
private Logger logger = Logger.getLogger(IStrategy.class);
// Running
private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore;
private SolutionStore solutionStore;
private SolutionStoreWithCopy solutionStoreWithCopy;
private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor;
private volatile boolean isInterrupted = false;
private ModelResult modelResultByInternalSolver = null;
private Random random = new Random();
//private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;
public ActivationSelector activationSelector = new EvenActivationSelector(random);
public NumericSolver numericSolver = null;
// Statistics
private int numberOfStatecoderFail = 0;
private int numberOfPrintedModel = 0;
private int numberOfSolverCalls = 0;
public long globalConstraintEvaluationTime = 0;
public long fitnessCalculationTime = 0;
public long explorationStarted = 0;
public BestFirstStrategyForModelGeneration(
ReasonerWorkspace workspace,
ViatraReasonerConfiguration configuration,
ModelGenerationMethod method)
{
this.workspace = workspace;
this.configuration = configuration;
this.method = method;
}
public SolutionStoreWithCopy getSolutionStoreWithCopy() {
return solutionStoreWithCopy;
}
public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
return solutionStoreWithDiversityDescriptor;
}
public int getNumberOfStatecoderFail() {
return numberOfStatecoderFail;
}
public long getForwardTime() {
return context.getDesignSpaceManager().getForwardTime();
}
public long getBacktrackingTime() {
return context.getDesignSpaceManager().getBacktrackingTime();
}
//LinkedList<ViatraQueryMatcher<? extends IPatternMatch>> matchers;
@Override
public void initStrategy(ThreadContext context) {
this.context = context;
this.solutionStore = context.getGlobalContext().getSolutionStore();
// ViatraQueryEngine engine = context.getQueryEngine();
// // TODO: visualisation
// matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
// for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {
// //System.out.println(p.getSimpleName());
// ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);
// matchers.add(matcher);
// }
this.solutionStoreWithCopy = new SolutionStoreWithCopy();
this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
this.comparator = new Comparator<TrajectoryWithFitness>() {
@Override
public int compare(TrajectoryWithFitness o1, TrajectoryWithFitness o2) {
return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);
}
};
this.numericSolver = new NumericSolver(context, method, this.configuration.runIntermediateNumericalConsistencyChecks, false);
trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);
}
@Override
public void explore() {
// System.out.println("press enter");
// try {
// new BufferedReader(new InputStreamReader(System.in)).readLine();
// } catch (IOException e) {
// // TODO Auto-generated catch block
// e.printStackTrace();
// }
this.explorationStarted=System.nanoTime();
if (!checkGlobalConstraints()) {
logger.info("Global contraint is not satisifed in the first state. Terminate.");
return;
} else if(!numericSolver.maySatisfiable()) {
logger.info("Numeric contraints are not satisifed in the first state. Terminate.");
return;
}
if (configuration.searchSpaceConstraints.maxDepth == 0) {
logger.info("Maximal depth is reached in the initial solution. Terminate.");
return;
}
final Fitness firstFittness = calculateFitness();
checkForSolution(firstFittness);
final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness);
trajectoiresToExplore.add(currentTrajectoryWithFittness);
//if(configuration)
visualiseCurrentState();
// for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
// System.out.println(matcher.getPatternName());
// System.out.println("---------");
// for(IPatternMatch m : matcher.getAllMatches()) {
// System.out.println(m);
// }
// System.out.println("---------");
// }
mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) {
if (currentTrajectoryWithFittness == null) {
if (trajectoiresToExplore.isEmpty()) {
logger.debug("State space is fully traversed.");
return;
} else {
currentTrajectoryWithFittness = selectState();
if (logger.isDebugEnabled()) {
logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness);
}
context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory);
}
}
// visualiseCurrentState();
// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);
// if(consistencyCheckResult == true) {
// continue mainLoop;
// }
List<Object> activationIds = selectActivation();
Iterator<Object> iterator = activationIds.iterator();
while (!isInterrupted && !configuration.progressMonitor.isCancelled() && iterator.hasNext()) {
final Object nextActivation = iterator.next();
// if (!iterator.hasNext()) {
// logger.debug("Last untraversed activation of the state.");
// trajectoiresToExplore.remove(currentTrajectoryWithFittness);
// }
logger.debug("Executing new activation: " + nextActivation);
context.executeAcitvationId(nextActivation);
visualiseCurrentState();
// for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
// int c = matcher.countMatches();
// if(c>=100) {
// System.out.println(c+ " " +matcher.getPatternName());
// }
//
// }
boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);
if(consistencyCheckResult == true) { continue mainLoop; }
if (context.isCurrentStateAlreadyTraversed()) {
logger.info("The new state is already visited.");
context.backtrack();
} else if (!checkGlobalConstraints()) {
logger.debug("Global contraint is not satisifed.");
context.backtrack();
} else if (!numericSolver.maySatisfiable()) {
logger.debug("Numeric constraints are not satisifed.");
context.backtrack();
} else {
final Fitness nextFitness = calculateFitness();
checkForSolution(nextFitness);
if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) {
logger.debug("Reached max depth.");
context.backtrack();
continue;
}
TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness(
context.getTrajectory().toArray(), nextFitness);
trajectoiresToExplore.add(nextTrajectoryWithFittness);
int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness,
nextTrajectoryWithFittness.fitness);
if (compare < 0) {
logger.debug("Better fitness, moving on: " + nextFitness);
currentTrajectoryWithFittness = nextTrajectoryWithFittness;
continue mainLoop;
} else if (compare == 0) {
logger.debug("Equally good fitness, moving on: " + nextFitness);
currentTrajectoryWithFittness = nextTrajectoryWithFittness;
continue mainLoop;
} else {
logger.debug("Worse fitness.");
currentTrajectoryWithFittness = null;
continue mainLoop;
}
}
}
logger.debug("State is fully traversed.");
trajectoiresToExplore.remove(currentTrajectoryWithFittness);
currentTrajectoryWithFittness = null;
}
logger.info("Interrupted.");
}
private boolean checkGlobalConstraints() {
long start = System.nanoTime();
boolean result = context.checkGlobalConstraints();
globalConstraintEvaluationTime += System.nanoTime() - start;
return result;
}
private Fitness calculateFitness() {
long start = System.nanoTime();
Fitness fitness = context.calculateFitness();
fitnessCalculationTime += System.nanoTime() - start;
return fitness;
}
private List<Object> selectActivation() {
List<Object> activationIds;
try {
activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds());
} catch (NullPointerException e) {
numberOfStatecoderFail++;
activationIds = Collections.emptyList();
}
return activationIds;
}
private void checkForSolution(final Fitness fittness) {
if (fittness.isSatisifiesHardObjectives()) {
if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
if(numericSolver.currentSatisfiable()) {
Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context);
numericSolver.fillSolutionCopy(trace);
solutionStoreWithDiversityDescriptor.newSolution(context);
solutionStore.newSolution(context);
configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
saveTimes();
logger.debug("Found a solution.");
}
}
}
}
public List<String> times = new LinkedList<String>();
private void saveTimes() {
long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder)this.context.getStateCoder()).getStatecoderRuntime()/1000000;
long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000;
long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000;
long solutionCopy = solutionStoreWithCopy.getSumRuntime()/1000000;
long activationSelection = this.activationSelector.getRuntime()/1000000;
long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000;
long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000;
long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000;
long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000;
this.times.add(
"(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+
"|StateCoderTime:"+statecoderTime+
"|ForwardTime:"+forwardTime+
"|Backtrackingtime:"+backtrackingTime+
"|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+
"|FitnessCalculationTime:"+(fitnessCalculationTime/1000000)+
"|SolutionCopyTime:"+solutionCopy+
"|ActivationSelectionTime:"+activationSelection+
"|NumericalSolverSumTime:"+numericalSolverSumTime+
"|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+
"|NumericalSolverSolvingTime:"+numericalSolverSolving+
"|NumericalSolverInterpretingSolution:"+numericalSolverInterpreting+")");
}
@Override
public void interruptStrategy() {
isInterrupted = true;
}
private TrajectoryWithFitness selectState() {
int randomNumber = random.nextInt(configuration.randomBacktrackChance);
if (randomNumber == 0) {
int elements = trajectoiresToExplore.size();
int randomElementIndex = random.nextInt(elements);
logger.debug("Randomly backtract to the " + randomElementIndex + " best solution...");
Iterator<TrajectoryWithFitness> iterator = trajectoiresToExplore.iterator();
while (randomElementIndex != 0) {
iterator.next();
randomElementIndex--;
}
TrajectoryWithFitness res = iterator.next();
if (res == null) {
return trajectoiresToExplore.element();
} else {
return res;
}
} else {
return trajectoiresToExplore.element();
}
}
public void visualiseCurrentState() {
PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser;
if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) {
PartialInterpretation p = (PartialInterpretation) (context.getModel());
int id = ++numberOfPrintedModel;
if (id % configuration.debugCongiguration.partalInterpretationVisualisationFrequency == 0) {
PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p);
visualisation.writeToFile(workspace, String.format("state%09d.png", id));
}
}
}
protected boolean checkConsistency(TrajectoryWithFitness t) {
LogicReasoner internalIncosnsitencyDetector = configuration.internalConsistencyCheckerConfiguration.internalIncosnsitencyDetector;
if (internalIncosnsitencyDetector!= null) {
int id = ++numberOfSolverCalls;
if (id % configuration.internalConsistencyCheckerConfiguration.incternalConsistencyCheckingFrequency == 0) {
try {
PartialInterpretation interpretation = (PartialInterpretation) (context.getModel());
PartialInterpretation copied = EcoreUtil.copy(interpretation);
this.partialInterpretation2Logic.transformPartialIntepretation2Logic(copied.getProblem(), copied);
LogicProblem newProblem = copied.getProblem();
this.configuration.typeScopes.maxNewElements = interpretation.getMaxNewElements();
this.configuration.typeScopes.minNewElements = interpretation.getMinNewElements();
LogicResult result = internalIncosnsitencyDetector.solve(newProblem, configuration, workspace);
if (result instanceof InconsistencyResult) {
logger.debug("Solver found an Inconsistency!");
removeSubtreeFromQueue(t);
return true;
} else if (result instanceof ModelResult) {
logger.debug("Solver found a model!");
solutionStore.newSolution(context);
this.modelResultByInternalSolver = (ModelResult) result;
return true;
} else {
logger.debug("Failed consistency check.");
return false;
}
} catch (Exception e) {
logger.debug("Problem with internal consistency checking: "+e.getMessage());
e.printStackTrace();
return false;
}
}
}
return false;
}
protected void removeSubtreeFromQueue(TrajectoryWithFitness t) {
PriorityQueue<TrajectoryWithFitness> previous = this.trajectoiresToExplore;
this.trajectoiresToExplore = new PriorityQueue<>(this.comparator);
for (TrajectoryWithFitness trajectoryWithFitness : previous) {
if (!containsAsSubstring(trajectoryWithFitness.trajectory, t.trajectory)) {
this.trajectoiresToExplore.add(trajectoryWithFitness);
} else {
logger.debug("State has been excluded due to inherent inconsistency");
}
}
}
private boolean containsAsSubstring(Object[] full, Object[] substring) {
if (substring.length > full.length) {
return false;
} else if (substring.length == full.length) {
return Arrays.equals(full, substring);
} else {
Object[] part = Arrays.copyOfRange(full, 0, substring.length);
return Arrays.equals(part, substring);
}
}
}
|