/*******************************************************************************
* 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.util.Arrays;
import java.util.Collections;
import java.util.Comparator;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
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.SolutionTrajectory;
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.ISolutionFoundHandler;
import org.eclipse.viatra.dse.solutionstore.SolutionStore;
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.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
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.ModelGenerationMethod;
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
*
*
maximum depth
*
continue the exploration from a state that satisfies the hard objectives
* (the default that it will backtrack),
*
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").
*
*
*/
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 comparator;
private Logger logger = Logger.getLogger(IStrategy.class);
// Running
private PriorityQueue trajectoiresToExplore;
private SolutionStore solutionStore;
private volatile boolean isInterrupted = false;
private ModelResult modelResultByInternalSolver = null;
private Random random = new Random();
// private Collection> matchers;
public ActivationSelector activationSelector = new EvenActivationSelector(random);
public ViatraReasonerSolutionSaver solutionSaver;
public NumericSolver numericSolver;
// 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,
ViatraReasonerSolutionSaver solutionSaver,
NumericSolver numericSolver) {
this.workspace = workspace;
this.configuration = configuration;
this.method = method;
this.solutionSaver = solutionSaver;
this.numericSolver = numericSolver;
// logger.setLevel(Level.DEBUG);
}
public int getNumberOfStatecoderFail() {
return numberOfStatecoderFail;
}
public long getForwardTime() {
return context.getDesignSpaceManager().getForwardTime();
}
public long getBacktrackingTime() {
return context.getDesignSpaceManager().getBacktrackingTime();
}
@Override
public void initStrategy(ThreadContext context) {
this.context = context;
this.solutionStore = context.getGlobalContext().getSolutionStore();
solutionStore.registerSolutionFoundHandler(new ISolutionFoundHandler() {
@Override
public void solutionTriedToSave(ThreadContext context, SolutionTrajectory trajectory) {
// Ignore.
}
@Override
public void solutionFound(ThreadContext context, SolutionTrajectory trajectory) {
configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions);
saveTimes();
logger.debug("Found a solution.");
}
});
numericSolver.init(context);
// ViatraQueryEngine engine = context.getQueryEngine();
// matchers = new LinkedList>();
// for(IQuerySpecification extends ViatraQueryMatcher extends IPatternMatch>> p : this.method.getAllPatterns()) {
// ViatraQueryMatcher extends IPatternMatch> matcher = p.getMatcher(engine);
// }
//
final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
this.comparator = new Comparator() {
@Override
public int compare(TrajectoryWithFitness o1, TrajectoryWithFitness o2) {
return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);
}
};
trajectoiresToExplore = new PriorityQueue(11, comparator);
}
@Override
public void explore() {
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 firstFitness = calculateFitness();
checkForSolution(firstFitness);
final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
TrajectoryWithFitness currentTrajectoryWithFitness = new TrajectoryWithFitness(firstTrajectory, firstFitness);
trajectoiresToExplore.add(currentTrajectoryWithFitness);
//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 (currentTrajectoryWithFitness == null) {
if (trajectoiresToExplore.isEmpty()) {
logger.debug("State space is fully traversed.");
return;
} else {
currentTrajectoryWithFitness = selectState();
if (logger.isDebugEnabled()) {
logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
logger.debug("New trajectory is chosen: " + currentTrajectoryWithFitness);
}
context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFitness.trajectory);
}
}
// visualiseCurrentState();
// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
// if(consistencyCheckResult == true) {
// continue mainLoop;
// }
List