From ae596d22260beead480e9936a2ec391fe3cb7727 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 12 Jul 2017 15:35:45 +0200 Subject: Rearranged the solver configuration into different subsections DiversityDescriptor * Describes the required diversity between the solutions. * Null means that the solutions have to have different state codes only. InternalConsistencyCheckerConfiguration * A logic solver that able to check the consistency of an intermediate solution. * Null means that no solver is called. DebugConfiguration * Configuration for debugging support. SearchSpaceConstraint * Configuration for cutting search space. --- .../viatrasolver/reasoner/ViatraReasoner.xtend | 39 +- .../reasoner/ViatraReasonerConfiguration.xtend | 59 +- .../dse/BestFirstStrategyForModelGeneration.java | 646 ++++++++++----------- .../reasoner/dse/TrajectoryWithFitness.java | 22 + 4 files changed, 373 insertions(+), 393 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/TrajectoryWithFitness.java (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver') 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 fd70688b..e00c864a 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 @@ -44,28 +44,17 @@ class ViatraReasoner extends LogicReasoner{ val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter - val LogicReasoner inconsistencyDetector - - public new() { - this.inconsistencyDetector=null - } - - public new(LogicReasoner inconsistencyDetector) { - this.inconsistencyDetector = inconsistencyDetector - } - - public static var Collection>> allPatterns = null - //public static var List> additionalMatches = null override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { val viatraConfig = configuration.asConfig - val DesignSpaceExplorer dse = new DesignSpaceExplorer(); - /* - DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL) - /*/ - DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN) - //*/ + if(viatraConfig.debugCongiguration.logging) { + DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL) + } else { + DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN) + } + + val DesignSpaceExplorer dse = new DesignSpaceExplorer(); dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE) dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE) @@ -86,7 +75,6 @@ class ViatraReasoner extends LogicReasoner{ viatraConfig.nameNewElements, viatraConfig.typeInferenceMethod ) - allPatterns = method.allPatterns dse.addObjective(new ModelGenerationCompositeObjective( new ScopeObjective, @@ -95,7 +83,7 @@ class ViatraReasoner extends LogicReasoner{ )) dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF)) - for(additionalConstraint : configuration.asConfig.additionalGlobalConstraints) { + for(additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) { dse.addGlobalConstraint(additionalConstraint.apply(method)) } @@ -121,10 +109,7 @@ class ViatraReasoner extends LogicReasoner{ } val strategy = new BestFirstStrategyForModelGeneration( - workspace,inconsistencyDetector, - viatraConfig.inconsistencDetectorConfiguration, - viatraConfig.diversityRequirement/*, - method.allPatterns*/) + workspace,viatraConfig) val transformationTime = System.nanoTime - transformationStartTime val solverStartTime = System.nanoTime @@ -162,7 +147,7 @@ class ViatraReasoner extends LogicReasoner{ it.name = "StateCoderTime" it.value = (statecoderFinal.runtime/1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "StateCoderFailCount" it.value = strategy.numberOfStatecoderFaiL + it.name = "StateCoderFailCount" it.value = strategy.numberOfStatecoderFail ] it.entries += createIntStatisticEntry => [ it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int @@ -204,10 +189,6 @@ class ViatraReasoner extends LogicReasoner{ } } } - - /*private def simpleWeithts(List objectives) { - objectives.map[1.0].toList - }*/ private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) { sc.sumStatecoderRuntime 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 d638dd71..f32078a2 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 @@ -1,15 +1,17 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod -import java.util.LinkedList -import java.util.List +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser import java.util.Set import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import java.util.LinkedList +import java.util.List import org.eclipse.xtext.xbase.lib.Functions.Function1 +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod public enum StateCoderStrategy { Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity @@ -17,26 +19,59 @@ public enum StateCoderStrategy { class ViatraReasonerConfiguration extends LogicSolverConfiguration{ public var Iterable existingQueries - public var LogicSolverConfiguration inconsistencDetectorConfiguration = null - public var List> additionalGlobalConstraints = new LinkedList - int maxDepth = -1 - - public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.Generic public var nameNewElements = false public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood + public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis + /** + * Once per 1/randomBacktrackChance the search selects a random state. + */ + public var int randomBacktrackChance = 20; /** * Describes the required diversity between the solutions. * Null means that the solutions have to have different state codes only. */ - public var DiversityDescriptor diversityRequirement = null + public var DiversityDescriptor diversityRequirement = new DiversityDescriptor + /** + * A logic solver that able to check the consistency of an intermediate solution. + * Null means that no solver is called. + */ + public var InternalConsistencyCheckerConfiguration internalConsistencyCheckerConfiguration = new InternalConsistencyCheckerConfiguration + /** + * Configuration for debugging support. + */ + public var DebugConfiguration debugCongiguration = new DebugConfiguration + /** + * Configuration for cutting search space. + */ + public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint } public class DiversityDescriptor { - public var int range = -1 + public var ensureDiversity = false + public static val FixPointRange = -1 + public var int range = FixPointRange public var int parallels = Integer.MAX_VALUE public var int maxNumber = Integer.MAX_VALUE - public var Set relevantTypes - public var Set relevantRelations + public var Set relevantTypes = null + public var Set relevantRelations = null +} + +public class DebugConfiguration { + public var logging = false + public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null; + public var partalInterpretationVisualisationFrequency = 1 +} + +public class InternalConsistencyCheckerConfiguration { + public var LogicReasoner internalIncosnsitencyDetector = null + public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null + public var incternalConsistencyCheckingFrequency = 1 +} + +public class SearchSpaceConstraint { + public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE + public var int maxDepth = UNLIMITED_MAXDEPTH + public var List> additionalGlobalConstraints = new LinkedList } \ 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/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 862ba245..346ed886 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,397 +11,339 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse; 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.PriorityQueue; import java.util.Random; -import java.util.SortedMap; -import java.util.TreeMap; -import java.util.TreeSet; import org.apache.log4j.Logger; +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.IPatternMatch; -import org.eclipse.viatra.query.runtime.api.IQuerySpecification; -import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher; -import org.eclipse.viatra.query.runtime.exception.ViatraQueryException; +import org.eclipse.xtend.lib.annotations.AccessorType; +import org.eclipse.xtend.lib.annotations.Accessors; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; +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.PartialInterpretation2Gml; +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.DebugConfiguration; import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor; +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}. + * 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").
    • + *
  • 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").
    • *
* - * @author Andras Szabolcs Nagy - * */ public class BestFirstStrategyForModelGeneration implements IStrategy { - - private ThreadContext context; - private SolutionStore solutionStore; - private SolutionStoreWithCopy solutionStoreWithCopy; - private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor; - private int numberOfStatecoderFail=0; - //Collection>> additionalPatterns = null; - //List> additionalMatchers = new LinkedList>(); - - private int maxDepth = Integer.MAX_VALUE; - private boolean isInterrupted = false; - //private boolean backTrackIfSolution = true; - private boolean onlyBetterFirst = false; - - - private PriorityQueue trajectoiresToExplore; - private Logger logger = Logger.getLogger(IStrategy.class); - - private static class TrajectoryWithFitness { - - public Object[] trajectory; - public Fitness fitness; - - public TrajectoryWithFitness(Object[] trajectory, Fitness fitness) { - super(); - this.trajectory = trajectory; - this.fitness = fitness; - } - - @Override - public String toString() { - return Arrays.toString(trajectory) + fitness.toString(); - } - - } - - public BestFirstStrategyForModelGeneration( - ReasonerWorkspace workspace, LogicReasoner reasoner, LogicSolverConfiguration configuration, DiversityDescriptor descriptor/*, - Collection>> additionalPatterns*/) { - this.maxDepth = Integer.MAX_VALUE; - this.workspace = workspace; - this.reasoner = reasoner; - this.configuration = configuration; - this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(descriptor); - //this.additionalPatterns = additionalPatterns; - } - - @Override - public void initStrategy(ThreadContext context) { - this.context = context; - this.solutionStore = context.getGlobalContext().getSolutionStore(); - this.solutionStoreWithCopy = new SolutionStoreWithCopy(); - - - final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); - - Comparator comparator = new Comparator() { - - @Override - public int compare(TrajectoryWithFitness o1, TrajectoryWithFitness o2) { - return objectiveComparatorHelper.compare(o2.fitness, o1.fitness); - } - }; - - - - trajectoiresToExplore = new PriorityQueue(11, comparator); - - } - - public SolutionStoreWithCopy getSolutionStoreWithCopy() { - return solutionStoreWithCopy; + + // Services and Configuration + private ThreadContext context; + private ReasonerWorkspace workspace; + private ViatraReasonerConfiguration configuration; + private PartialInterpretation2Logic partialInterpretation2Logic = new PartialInterpretation2Logic(); + private Comparator comparator; + private Logger logger = Logger.getLogger(IStrategy.class); + + // Running + private PriorityQueue trajectoiresToExplore; + private SolutionStore solutionStore; + private SolutionStoreWithCopy solutionStoreWithCopy; + private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor; + private boolean isInterrupted = false; + private ModelResult modelResultByInternalSolver = null; + private Random random = new Random(); + + // Statistics + private int numberOfStatecoderFail = 0; + private int numberOfPrintedModel = 0; + private int numberOfSolverCalls = 0; + + public BestFirstStrategyForModelGeneration( + ReasonerWorkspace workspace, + ViatraReasonerConfiguration configuration) + { + this.workspace = workspace; + this.configuration = configuration; + } + + public SolutionStoreWithCopy getSolutionStoreWithCopy() { + return solutionStoreWithCopy; + } + public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() { + return solutionStoreWithDiversityDescriptor; + } + public int getNumberOfStatecoderFail() { + return numberOfStatecoderFail; + } + + @Override + public void initStrategy(ThreadContext context) { + this.context = context; + this.solutionStore = context.getGlobalContext().getSolutionStore(); + this.solutionStoreWithCopy = new SolutionStoreWithCopy(); + this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement); + + 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() { + if (!context.checkGlobalConstraints()) { + logger.info("Global contraint is 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; + } - public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() { - return solutionStoreWithDiversityDescriptor; - } + final Fitness firstFittness = context.calculateFitness(); + checkForSolution(firstFittness); - public int getNumberOfStatecoderFaiL() { - return numberOfStatecoderFail; + final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); + final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); + TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness); + trajectoiresToExplore.add(currentTrajectoryWithFittness); + + mainLoop: while (!isInterrupted) { + + 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 activationIds = selectActivation(); + Iterator iterator = activationIds.iterator(); + + while (!isInterrupted && 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(); + boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); + if(consistencyCheckResult == true) { continue mainLoop; } + + if (context.isCurrentStateAlreadyTraversed()) { + logger.info("The new state is already visited."); + context.backtrack(); + } else if (!context.checkGlobalConstraints()) { + logger.debug("Global contraint is not satisifed."); + context.backtrack(); + } else { + final Fitness nextFitness = context.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; + } + } } - @Override - public void explore() { - - /*if(this.additionalPatterns!=null) { - for (IQuerySpecification> additionalPattern : additionalPatterns) { + logger.debug("State is fully traversed."); + trajectoiresToExplore.remove(currentTrajectoryWithFittness); + currentTrajectoryWithFittness = null; + + } + logger.info("Interrupted."); + } + + private List selectActivation() { + List activationIds; + try { + activationIds = new ArrayList(context.getUntraversedActivationIds()); + Collections.shuffle(activationIds); + } catch (NullPointerException e) { + numberOfStatecoderFail++; + activationIds = Collections.emptyList(); + } + return activationIds; + } + + private void checkForSolution(final Fitness fittness) { + if (fittness.isSatisifiesHardObjectives()) { + if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { + solutionStoreWithCopy.newSolution(context); + solutionStoreWithDiversityDescriptor.newSolution(context); + solutionStore.newSolution(context); + + logger.debug("Found a solution."); + } + } + } + + @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 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) { + 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", id)); + } + } + } + + protected boolean checkConsistency(TrajectoryWithFitness t) { + LogicReasoner internalIncosnsitencyDetector = configuration.internalConsistencyCheckerConfiguration.internalIncosnsitencyDetector; + if (internalIncosnsitencyDetector!= null) { + int id = ++numberOfSolverCalls; + if (id % configuration.internalConsistencyCheckerConfiguration.incternalConsistencyCheckingFrequency == 0) { try { - this.additionalMatchers.add(additionalPattern.getMatcher(context.getQueryEngine())); - } catch (ViatraQueryException e) { - // TODO Auto-generated catch block + 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; } } - }*/ - - final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); - - boolean globalConstraintsAreSatisfied = context.checkGlobalConstraints(); - if (!globalConstraintsAreSatisfied) { - logger.info("Global contraint is not satisifed in the first state. Terminate."); - return; - } - - final Fitness firstFittness = context.calculateFitness(); - if (firstFittness.isSatisifiesHardObjectives()) { - context.newSolution(); - logger.info("First state is a solution. Terminate."); - return; - } - - if (maxDepth == 0) { - return; - } - - final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); - TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness); - trajectoiresToExplore.add(currentTrajectoryWithFittness); - - mainLoop: while (!isInterrupted) { - - if (currentTrajectoryWithFittness == null) { - if (trajectoiresToExplore.isEmpty()) { - logger.debug("State space is fully traversed."); - return; - } else { - currentTrajectoryWithFittness = selectRandomState();// trajectoiresToExplore.element(); - if (logger.isDebugEnabled()) { - logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); - logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness); - } -// context.backtrackUntilRoot(); -// context.executeTrajectoryWithoutStateCoding(currentTrajectoryWithFittness.trajectory); - context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory); - } - - } - - List activationIds; - try { - activationIds = new ArrayList(context.getUntraversedActivationIds()); - Collections.shuffle(activationIds); - } catch (NullPointerException e) { - numberOfStatecoderFail++; - activationIds = Collections.emptyList(); - } - - Iterator iterator = activationIds.iterator(); - -// writeCurrentState(); -// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); -// if(consistencyCheckResult == true) { -// continue mainLoop; -// } - - while (!isInterrupted && iterator.hasNext()) { - final Object nextActivation = iterator.next(); - if (!iterator.hasNext()) { - logger.debug("Last untraversed activation of the state."); - trajectoiresToExplore.remove(currentTrajectoryWithFittness); - } - - if (logger.isDebugEnabled()) { - logger.debug("Executing new activation: " + nextActivation); - } - context.executeAcitvationId(nextActivation); - -// writeCurrentState(); - - if (context.isCurrentStateAlreadyTraversed()) { - logger.info("The new state is already visited."); - context.backtrack(); - } else if (!context.checkGlobalConstraints()) { - logger.debug("Global contraint is not satisifed."); - context.backtrack(); - } else { - final Fitness nextFitness = context.calculateFitness(); - if (nextFitness.isSatisifiesHardObjectives()) { - if(solutionStoreWithDiversityDescriptor.isDifferent(context)) { - /*SortedMap x = new TreeMap(); - for(ViatraQueryMatcher additioanMatcher : this.additionalMatchers) { - x.put(additioanMatcher.getPatternName(),additioanMatcher.countMatches()); - }*/ - - solutionStoreWithCopy.newSolution(context/*,x*/); - solutionStoreWithDiversityDescriptor.newSolution(context); - solutionStore.newSolution(context); - - logger.debug("Found a solution."); - } - } - if (context.getDepth() > 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) { - if (onlyBetterFirst) { - logger.debug("Equally good fitness, backtrack: " + nextFitness); - context.backtrack(); - continue; - } else { - logger.debug("Equally good fitness, moving on: " + nextFitness); - currentTrajectoryWithFittness = nextTrajectoryWithFittness; - continue mainLoop; - } - } else { - logger.debug("Worse fitness."); -// context.backtrack(); - currentTrajectoryWithFittness = null; - continue mainLoop; - } - } - } - - logger.debug("State is fully traversed."); - trajectoiresToExplore.remove(currentTrajectoryWithFittness); - currentTrajectoryWithFittness = null; - - } - logger.info("Interrupted."); - } - - @Override - public void interruptStrategy() { - isInterrupted = true; - } - - Random random = new Random(); - private TrajectoryWithFitness selectRandomState() { - int randomNumber = random.nextInt(100); - if(randomNumber < 5) { - int elements = trajectoiresToExplore.size(); - int randomElementIndex = random.nextInt(elements); - logger.debug("Randomly backtract to the " + randomElementIndex + " best solution..."); - Iterator 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(); - } - } - - private PartialInterpretation2Logic partialInterpretation2Logic = new PartialInterpretation2Logic(); - private LogicReasoner reasoner; - private PartialInterpretation2Gml partialInterpretation2Gml = new PartialInterpretation2Gml(); - private ReasonerWorkspace workspace; - private LogicSolverConfiguration configuration; - int numberOfPrintedModel = 0; - public ModelResult modelResultByTheSolver = null; - public void writeCurrentState() { - PartialInterpretation p = (PartialInterpretation)(context.getModel()); - int id= ++numberOfPrintedModel; - if(id%100 == 1) { - String text = this.partialInterpretation2Gml.transform(p); - this.workspace.writeText(id+".gml", text); - this.workspace.writeModel(p, id+".partialinterpretation"); - logger.debug("State "+id+" is saved."); - } - } - -// int numberOfSolverCalls = 0; -// -// protected boolean checkConsistency(TrajectoryWithFitness t) { -// if (reasoner != null) { -// int id = ++numberOfSolverCalls; -// if (id % 100 == 1) { -// 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 = reasoner.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); - -// modelResultByTheSolver = (ModelResult) result; -// return true; -// } else { -// logger.debug("Failed consistency check."); -// return false; -// } -// } catch (Exception e) { -// // TODO Auto-generated catch block -// e.printStackTrace(); -// return false; -// } -// } -// -// } -// return false; -// } -// -// protected void removeSubtreeFromQueue(TrajectoryWithFitness t) { -// PriorityQueue 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); -// } -// } -// - + + } + return false; + } + + protected void removeSubtreeFromQueue(TrajectoryWithFitness t) { + PriorityQueue 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); + } + } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/TrajectoryWithFitness.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/TrajectoryWithFitness.java new file mode 100644 index 00000000..a7a6ab36 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/TrajectoryWithFitness.java @@ -0,0 +1,22 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse; + +import java.util.Arrays; + +import org.eclipse.viatra.dse.objectives.Fitness; + +class TrajectoryWithFitness { + + public Object[] trajectory; + public Fitness fitness; + + public TrajectoryWithFitness(Object[] trajectory, Fitness fitness) { + super(); + this.trajectory = trajectory; + this.fitness = fitness; + } + + @Override + public String toString() { + return Arrays.toString(trajectory) + fitness.toString(); + } +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf