From 3f9b1c92cc35fa4ed9672a2b8601f4c22af24921 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sun, 7 Apr 2019 13:46:36 +0200 Subject: Infrastructure for objective functions --- .../MultiplicityGoalConstraintCalculator.xtend | 10 +- .../viatrasolver/reasoner/ViatraReasoner.xtend | 188 +++++++++++---------- .../reasoner/ViatraReasonerConfiguration.xtend | 12 +- .../dse/BestFirstStrategyForModelGeneration.java | 57 +++---- .../viatrasolver/reasoner/dse/DseUtils.xtend | 65 +++++++ .../reasoner/dse/IThreeValuedObjective.xtend | 10 ++ .../reasoner/dse/LoggerSolutionFoundHandler.xtend | 24 +++ .../dse/ModelGenerationCompositeObjective.xtend | 77 +++++---- .../viatrasolver/reasoner/dse/SolutionCopier.xtend | 74 ++++++++ .../reasoner/dse/SolutionStoreWithCopy.xtend | 52 ------ .../SurelyViolatedObjectiveGlobalConstraint.xtend | 29 ++++ .../dse/UnfinishedMultiplicityObjective.xtend | 2 +- .../reasoner/dse/UnfinishedWFObjective.xtend | 56 ------ .../reasoner/dse/ViatraReasonerSolutionSaver.xtend | 99 +++++++++++ .../reasoner/dse/WF2ObjectiveConverter.xtend | 44 +++-- 15 files changed, 504 insertions(+), 295 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend delete mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend delete mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend (limited to 'Solvers/VIATRA-Solver') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend index e05160d0..4b9629df 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend @@ -11,28 +11,28 @@ class MultiplicityGoalConstraintCalculator { val IQuerySpecification querySpecification; var ViatraQueryMatcher matcher; - public new(String targetRelationName, IQuerySpecification querySpecification) { + new(String targetRelationName, IQuerySpecification querySpecification) { this.targetRelationName = targetRelationName this.querySpecification = querySpecification this.matcher = null } - public new(MultiplicityGoalConstraintCalculator other) { + new(MultiplicityGoalConstraintCalculator other) { this.targetRelationName = other.targetRelationName this.querySpecification = other.querySpecification this.matcher = null } - def public getName() { + def getName() { targetRelationName } - def public init(Notifier notifier) { + def init(Notifier notifier) { val engine = ViatraQueryEngine.on(new EMFScope(notifier)) matcher = querySpecification.getMatcher(engine) } - def public calculateValue() { + def calculateValue() { var res = 0 val allMatches = this.matcher.allMatches for(match : allMatches) { 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 6639e5f3..8831b0ff 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 @@ -17,11 +17,13 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedWFObjective +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace import java.util.List @@ -31,44 +33,41 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel import org.eclipse.viatra.dse.solutionstore.SolutionStore import org.eclipse.viatra.dse.statecode.IStateCoderFactory -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SolutionStoreWithDiversityDescriptor -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityGranularity -class ViatraReasoner extends LogicReasoner{ +class ViatraReasoner extends LogicReasoner { val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider - val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE + val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter - - - override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { + + override solve(LogicProblem problem, LogicSolverConfiguration configuration, + ReasonerWorkspace workspace) throws LogicReasonerException { val viatraConfig = configuration.asConfig - - if(viatraConfig.debugCongiguration.logging) { + + if (viatraConfig.debugConfiguration.logging) { DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL) } else { DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN) } - + val DesignSpaceExplorer dse = new DesignSpaceExplorer(); - + dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE) dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE) dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE) - + val transformationStartTime = System.nanoTime - - - - val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output - if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { - workspace.writeModel(emptySolution,"init.partialmodel") - } + + val emptySolution = initialiser.initialisePartialInterpretation(problem, viatraConfig.typeScopes).output + if ((viatraConfig.documentationLevel == DocumentationLevel::FULL || + viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { + workspace.writeModel(emptySolution, "init.partialmodel") + } emptySolution.problemConainer = problem - + val ScopePropagator scopePropagator = new ScopePropagator(emptySolution) - scopePropagator.propagateAllScopeConstraints - + scopePropagator.propagateAllScopeConstraints + val method = modelGenerationMethodProvider.createModelGenerationMethod( problem, emptySolution, @@ -78,138 +77,151 @@ class ViatraReasoner extends LogicReasoner{ scopePropagator, viatraConfig.documentationLevel ) - + dse.addObjective(new ModelGenerationCompositeObjective( new ScopeObjective, method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], - new UnfinishedWFObjective(method.unfinishedWF) + wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF) )) - dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF)) - for(additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) { + val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolutions) + solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) + val solutionSaver = new ViatraReasonerSolutionSaver(newArrayOfSize(0, 0)) + val solutionCopier = solutionSaver.solutionCopier + solutionStore.withSolutionSaver(solutionSaver) + dse.solutionStore = solutionStore + + dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationGlobalConstraint(method.invalidWF)) + dse.addGlobalConstraint(new SurelyViolatedObjectiveGlobalConstraint(solutionSaver)) + for (additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) { dse.addGlobalConstraint(additionalConstraint.apply(method)) } - - dse.setInitialModel(emptySolution,false) - - val IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) { - new NeighbourhoodBasedStateCoderFactory - } else { - new IdentifierBasedStateCoderFactory - } + + dse.setInitialModel(emptySolution, false) + + val IStateCoderFactory statecoder = if (viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) { + new NeighbourhoodBasedStateCoderFactory + } else { + new IdentifierBasedStateCoderFactory + } dse.stateCoderFactory = statecoder - + dse.maxNumberOfThreads = 1 - - val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolution) - dse.solutionStore = solutionStore - - for(rule : method.relationRefinementRules) { + + for (rule : method.relationRefinementRules) { dse.addTransformationRule(rule) } - for(rule : method.objectRefinementRules) { + for (rule : method.objectRefinementRules) { dse.addTransformationRule(rule) } - - val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) + + val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method) viatraConfig.progressMonitor.workedForwardTransformation - + val transformationTime = System.nanoTime - transformationStartTime val solverStartTime = System.nanoTime - + var boolean stoppedByTimeout - var boolean stoppedByException - try{ - stoppedByTimeout = dse.startExplorationWithTimeout(strategy,configuration.runtimeLimit*1000); - stoppedByException = false + try { + stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000); } catch (NullPointerException npe) { stoppedByTimeout = false - stoppedByException = true } val solverTime = System.nanoTime - solverStartTime viatraConfig.progressMonitor.workedSearchFinished - - //additionalMatches = strategy.solutionStoreWithCopy.additionalMatches + + // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches val statistics = createStatistics => [ - //it.solverTime = viatraConfig.runtimeLimit - it.solverTime = (solverTime/1000000) as int - it.transformationTime = (transformationTime/1000000) as int - for(x : 0.. [ - it.name = '''_Solution«x»FoundAt''' - it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int + it.name = '''_Solution«pair.key»FoundAt''' + it.value = (pair.value / 1000000) as int ] } it.entries += createIntStatisticEntry => [ - it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int + it.name = "TransformationExecutionTime" + it.value = (method.statistics.transformationExecutionTime / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "TypeAnalysisTime" it.value = (method.statistics.PreliminaryTypeAnalisisTime/1000000) as int + it.name = "TypeAnalysisTime" + it.value = (method.statistics.PreliminaryTypeAnalisisTime / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "StateCoderTime" it.value = (statecoder.runtime/1000000) as int + it.name = "StateCoderTime" + it.value = (statecoder.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 + it.name = "SolutionCopyTime" + it.value = (solutionCopier.getTotalCopierRuntime / 1000000) as int ] - if(strategy.solutionStoreWithDiversityDescriptor.isActive) { + if (strategy.solutionStoreWithDiversityDescriptor.isActive) { it.entries += createIntStatisticEntry => [ - it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int + it.name = "SolutionDiversityCheckTime" + it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime / 1000000) as int ] it.entries += createRealStatisticEntry => [ - it.name = "SolutionDiversitySuccessRate" it.value = strategy.solutionStoreWithDiversityDescriptor.successRate + it.name = "SolutionDiversitySuccessRate" + it.value = strategy.solutionStoreWithDiversityDescriptor.successRate ] } ] - + viatraConfig.progressMonitor.workedBackwardTransformationFinished - - if(stoppedByTimeout) { - return createInsuficientResourcesResult=>[ + + if (stoppedByTimeout) { + return createInsuficientResourcesResult => [ it.problem = problem - it.resourceName="time" - it.representation += strategy.solutionStoreWithCopy.solutions + it.resourceName = "time" + it.representation += solutionCopier.getPartialInterpretations(true) it.statistics = statistics ] } else { - if(solutionStore.solutions.empty) { + if (solutionStore.solutions.empty) { return createInconsistencyResult => [ it.problem = problem - it.representation += strategy.solutionStoreWithCopy.solutions + it.representation += solutionCopier.getPartialInterpretations(true) it.statistics = statistics ] } else { return createModelResult => [ it.problem = problem - it.trace = strategy.solutionStoreWithCopy.copyTraces - it.representation += strategy.solutionStoreWithCopy.solutions + it.trace = solutionCopier.getTraces(true) + it.representation += solutionCopier.getPartialInterpretations(true) it.statistics = statistics ] } } } - private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) { - sc.sumStatecoderRuntime - } + private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) { + sc.sumStatecoderRuntime + } - private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) { - sc.sumStatecoderRuntime - } + private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) { + sc.sumStatecoderRuntime + } override getInterpretations(ModelResult modelResult) { - val indexes = 0..>; - val res = indexes.map[i | new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation,traces.get(i))].toList + val res = indexes.map [ i | + new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation, + traces.get(i)) + ].toList return res } - + private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) { - if(configuration instanceof ViatraReasonerConfiguration) { + if (configuration instanceof ViatraReasonerConfiguration) { return configuration - } else throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''') + } 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/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index c4d7e231..9ef23c59 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 @@ -12,7 +12,7 @@ import java.util.List import java.util.Set import org.eclipse.xtext.xbase.lib.Functions.Function1 -public enum StateCoderStrategy { +enum StateCoderStrategy { Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity } @@ -40,14 +40,14 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{ /** * Configuration for debugging support. */ - public var DebugConfiguration debugCongiguration = new DebugConfiguration + public var DebugConfiguration debugConfiguration = new DebugConfiguration /** * Configuration for cutting search space. */ public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint } -public class DiversityDescriptor { +class DiversityDescriptor { public var ensureDiversity = false public static val FixPointRange = -1 public var int range = FixPointRange @@ -57,19 +57,19 @@ public class DiversityDescriptor { public var Set relevantRelations = null } -public class DebugConfiguration { +class DebugConfiguration { public var logging = false public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null; public var partalInterpretationVisualisationFrequency = 1 } -public class InternalConsistencyCheckerConfiguration { +class InternalConsistencyCheckerConfiguration { public var LogicReasoner internalIncosnsitencyDetector = null public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null public var incternalConsistencyCheckingFrequency = 1 } -public class SearchSpaceConstraint { +class SearchSpaceConstraint { public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE public var int maxDepth = UNLIMITED_MAXDEPTH public var List> additionalGlobalConstraints = new LinkedList 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 60f46033..1234d54b 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 @@ -75,7 +75,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // Running private PriorityQueue trajectoiresToExplore; private SolutionStore solutionStore; - private SolutionStoreWithCopy solutionStoreWithCopy; private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor; private volatile boolean isInterrupted = false; private ModelResult modelResultByInternalSolver = null; @@ -97,9 +96,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { this.method = method; } - public SolutionStoreWithCopy getSolutionStoreWithCopy() { - return solutionStoreWithCopy; - } public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() { return solutionStoreWithDiversityDescriptor; } @@ -121,7 +117,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { matchers.add(matcher); } - this.solutionStoreWithCopy = new SolutionStoreWithCopy(); this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement); final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); @@ -146,13 +141,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { return; } - final Fitness firstFittness = context.calculateFitness(); - checkForSolution(firstFittness); + final Fitness firstfitness = context.calculateFitness(); + checkForSolution(firstfitness); final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); - TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness); - trajectoiresToExplore.add(currentTrajectoryWithFittness); + TrajectoryWithFitness currentTrajectoryWithfitness = new TrajectoryWithFitness(firstTrajectory, firstfitness); + trajectoiresToExplore.add(currentTrajectoryWithfitness); //if(configuration) visualiseCurrentState(); @@ -167,22 +162,22 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) { - if (currentTrajectoryWithFittness == null) { + if (currentTrajectoryWithfitness == null) { if (trajectoiresToExplore.isEmpty()) { logger.debug("State space is fully traversed."); return; } else { - currentTrajectoryWithFittness = selectState(); + currentTrajectoryWithfitness = selectState(); if (logger.isDebugEnabled()) { logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); - logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness); + logger.debug("New trajectory is chosen: " + currentTrajectoryWithfitness); } - context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory); + context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithfitness.trajectory); } } // visualiseCurrentState(); -// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); +// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness); // if(consistencyCheckResult == true) { // continue mainLoop; // } @@ -194,7 +189,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { final Object nextActivation = iterator.next(); // if (!iterator.hasNext()) { // logger.debug("Last untraversed activation of the state."); -// trajectoiresToExplore.remove(currentTrajectoryWithFittness); +// trajectoiresToExplore.remove(currentTrajectoryWithfitness); // } logger.debug("Executing new activation: " + nextActivation); context.executeAcitvationId(nextActivation); @@ -209,7 +204,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // System.out.println("---------"); // } - boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); + boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness); if(consistencyCheckResult == true) { continue mainLoop; } if (context.isCurrentStateAlreadyTraversed()) { @@ -227,31 +222,31 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { continue; } - TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness( + TrajectoryWithFitness nextTrajectoryWithfitness = new TrajectoryWithFitness( context.getTrajectory().toArray(), nextFitness); - trajectoiresToExplore.add(nextTrajectoryWithFittness); + trajectoiresToExplore.add(nextTrajectoryWithfitness); - int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness, - nextTrajectoryWithFittness.fitness); + int compare = objectiveComparatorHelper.compare(currentTrajectoryWithfitness.fitness, + nextTrajectoryWithfitness.fitness); if (compare < 0) { logger.debug("Better fitness, moving on: " + nextFitness); - currentTrajectoryWithFittness = nextTrajectoryWithFittness; + currentTrajectoryWithfitness = nextTrajectoryWithfitness; continue mainLoop; } else if (compare == 0) { logger.debug("Equally good fitness, moving on: " + nextFitness); - currentTrajectoryWithFittness = nextTrajectoryWithFittness; + currentTrajectoryWithfitness = nextTrajectoryWithfitness; continue mainLoop; } else { logger.debug("Worse fitness."); - currentTrajectoryWithFittness = null; + currentTrajectoryWithfitness = null; continue mainLoop; } } } logger.debug("State is fully traversed."); - trajectoiresToExplore.remove(currentTrajectoryWithFittness); - currentTrajectoryWithFittness = null; + trajectoiresToExplore.remove(currentTrajectoryWithfitness); + currentTrajectoryWithfitness = null; } logger.info("Interrupted."); @@ -269,15 +264,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { return activationIds; } - private void checkForSolution(final Fitness fittness) { - if (fittness.isSatisifiesHardObjectives()) { + private void checkForSolution(final Fitness fitness) { + if (fitness.isSatisifiesHardObjectives()) { if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { - solutionStoreWithCopy.newSolution(context); solutionStoreWithDiversityDescriptor.newSolution(context); solutionStore.newSolution(context); - configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); - - logger.debug("Found a solution."); } } } @@ -311,11 +302,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { } public void visualiseCurrentState() { - PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser; + PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.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) { + if (id % configuration.debugConfiguration.partalInterpretationVisualisationFrequency == 0) { PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p); visualisation.writeToFile(workspace, String.format("state%09d.png", id)); } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend new file mode 100644 index 00000000..3a897aa3 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend @@ -0,0 +1,65 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.viatra.dse.objectives.Comparators +import org.eclipse.viatra.dse.objectives.Fitness +import org.eclipse.viatra.dse.objectives.IObjective + +final class DseUtils { + private new() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly.") + } + + static def calculateFitness(ThreadContext it, (IObjective)=>Double getFitness) { + val result = new Fitness + var boolean satisifiesHardObjectives = true + for (objective : objectives) { + val fitness = getFitness.apply(objective) + result.put(objective.name, fitness) + if (objective.isHardObjective() && !objective.satisifiesHardObjective(fitness)) { + satisifiesHardObjectives = false + } + } + result.satisifiesHardObjectives = satisifiesHardObjectives + result + } + + static def caclulateBestPossibleFitness(ThreadContext threadContext) { + threadContext.calculateFitness [ objective | + if (objective instanceof IThreeValuedObjective) { + objective.getBestPossibleFitness(threadContext) + } else { + switch (objective.comparator) { + case Comparators.LOWER_IS_BETTER: + Double.NEGATIVE_INFINITY + case Comparators.HIGHER_IS_BETTER: + Double.POSITIVE_INFINITY + case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER: + 0.0 + default: + throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " + + objective.name) + } + } + ] + } + + static def caclulateWorstPossibleFitness(ThreadContext threadContext) { + threadContext.calculateFitness [ objective | + if (objective instanceof IThreeValuedObjective) { + objective.getWorstPossibleFitness(threadContext) + } else { + switch (objective.comparator) { + case Comparators.LOWER_IS_BETTER, + case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER: + Double.POSITIVE_INFINITY + case Comparators.HIGHER_IS_BETTER: + Double.NEGATIVE_INFINITY + default: + throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " + + objective.name) + } + } + ] + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend new file mode 100644 index 00000000..8c93d4ec --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend @@ -0,0 +1,10 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.viatra.dse.objectives.IObjective + +interface IThreeValuedObjective extends IObjective { + def Double getWorstPossibleFitness(ThreadContext threadContext) + + def Double getBestPossibleFitness(ThreadContext threadContext) +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend new file mode 100644 index 00000000..39ef5f9a --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend @@ -0,0 +1,24 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration +import org.apache.log4j.Logger +import org.eclipse.viatra.dse.api.SolutionTrajectory +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +@FinalFieldsConstructor +class LoggerSolutionFoundHandler implements ISolutionFoundHandler { + val ViatraReasonerConfiguration configuration + + val logger = Logger.getLogger(SolutionCopier) + + override solutionFound(ThreadContext context, SolutionTrajectory trajectory) { + configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions) + logger.debug("Found a solution.") + } + + override solutionTriedToSave(ThreadContext context, SolutionTrajectory trajectory) { + // We are not interested in invalid solutions, ignore. + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend index 2489c751..af6d1bbd 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend @@ -1,11 +1,12 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse +import com.google.common.collect.ImmutableList import java.util.Comparator import java.util.List import org.eclipse.viatra.dse.base.ThreadContext import org.eclipse.viatra.dse.objectives.Comparators import org.eclipse.viatra.dse.objectives.IObjective -import org.eclipse.viatra.dse.objectives.impl.BaseObjective +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor //class ViatraReasonerNumbers { // public static val scopePriority = 2 @@ -22,64 +23,66 @@ import org.eclipse.viatra.dse.objectives.impl.BaseObjective // public static val compositePriority = 2 //} -class ModelGenerationCompositeObjective implements IObjective{ - val ScopeObjective scopeObjective - val List unfinishedMultiplicityObjectives - val UnfinishedWFObjective unfinishedWFObjective - - public new( - ScopeObjective scopeObjective, - List unfinishedMultiplicityObjectives, - UnfinishedWFObjective unfinishedWFObjective) - { - this.scopeObjective = scopeObjective - this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives - this.unfinishedWFObjective = unfinishedWFObjective - } - +@FinalFieldsConstructor +class ModelGenerationCompositeObjective implements IThreeValuedObjective { + val IObjective scopeObjective + val List unfinishedMultiplicityObjectives + val IObjective unfinishedWFObjective + override init(ThreadContext context) { this.scopeObjective.init(context) this.unfinishedMultiplicityObjectives.forEach[it.init(context)] this.unfinishedWFObjective.init(context) } - + override createNew() { return new ModelGenerationCompositeObjective( - this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective) + scopeObjective.createNew, + ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew]), + unfinishedWFObjective.createNew + ) } - + override getComparator() { Comparators.LOWER_IS_BETTER } + override getFitness(ThreadContext context) { var sum = 0.0 val scopeFitnes = scopeObjective.getFitness(context) - //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] + // val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) - - sum+=scopeFitnes + + sum += scopeFitnes var multiplicity = 0.0 - for(multiplicityObjective : unfinishedMultiplicityObjectives) { - multiplicity+=multiplicityObjective.getFitness(context)//*0.5 + for (multiplicityObjective : unfinishedMultiplicityObjectives) { + multiplicity += multiplicityObjective.getFitness(context) // *0.5 } - sum+=multiplicity - sum += unfinishedWFsFitness//*0.5 - - //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') - + sum += multiplicity + sum += unfinishedWFsFitness // *0.5 + // println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') return sum } - override getLevel() { 2 } - override getName() { "CompositeUnfinishednessObjective"} + override getWorstPossibleFitness(ThreadContext threadContext) { + Double.POSITIVE_INFINITY + } + override getBestPossibleFitness(ThreadContext threadContext) { + 0.0 + } + + override getLevel() { 2 } + + override getName() { "CompositeUnfinishednessObjective" } + override isHardObjective() { true } + override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } - - + override setComparator(Comparator comparator) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + throw new UnsupportedOperationException("Model generation objective comparator cannot be set.") } + override setLevel(int level) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + throw new UnsupportedOperationException("Model generation objective level cannot be set.") } - -} \ 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/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend new file mode 100644 index 00000000..d036257d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend @@ -0,0 +1,74 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import com.google.common.collect.ImmutableList +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import java.util.LinkedHashMap +import java.util.List +import java.util.Map +import org.eclipse.emf.ecore.EObject +import org.eclipse.emf.ecore.util.EcoreUtil +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +@FinalFieldsConstructor +class CopiedSolution { + @Accessors val PartialInterpretation partialInterpretations + @Accessors val Map trace + @Accessors val long copierRuntime + @Accessors var boolean current = true +} + +class SolutionCopier { + val copiedSolutions = new LinkedHashMap + + long startTime = System.nanoTime + @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 + + def void copySolution(ThreadContext context, Object solutionId) { + val existingCopy = copiedSolutions.get(solutionId) + if (existingCopy === null) { + val copyStart = System.nanoTime + val solution = context.model as PartialInterpretation + val copier = new EcoreUtil.Copier + val copiedPartialInterpretation = copier.copy(solution) as PartialInterpretation + copier.copyReferences + totalCopierRuntime += System.nanoTime - copyStart + val copierRuntime = System.nanoTime - startTime + val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime) + copiedSolutions.put(solutionId, copiedSolution) + } else { + existingCopy.current = true + } + } + + def void markAsObsolete(Object solutionId) { + val copiedSolution = copiedSolutions.get(solutionId) + if (copiedSolution === null) { + throw new IllegalStateException("No solution to mark as obsolete for state code: " + solutionId) + } + copiedSolution.current = false + } + + def List getPartialInterpretations(boolean currentOnly) { + getListOfCopiedSolutions(currentOnly).map[partialInterpretations] + } + + def List> getTraces(boolean currentOnly) { + getListOfCopiedSolutions(currentOnly).map[trace] + } + + def List getAllCopierRuntimes(boolean currentOnly) { + getListOfCopiedSolutions(currentOnly).map[copierRuntime] + } + + def List getListOfCopiedSolutions(boolean currentOnly) { + val values = copiedSolutions.values + val filteredSolutions = if (currentOnly) { + values.filter[current] + } else { + values + } + ImmutableList.copyOf(filteredSolutions) + } +} 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 deleted file mode 100644 index a8b7301e..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend +++ /dev/null @@ -1,52 +0,0 @@ -package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse - -import java.util.List -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation -import java.util.LinkedList -import org.eclipse.emf.ecore.EObject -import java.util.Map -import org.eclipse.emf.ecore.util.EcoreUtil -import org.eclipse.viatra.dse.base.ThreadContext -import java.util.TreeMap -import java.util.SortedMap - -class SolutionStoreWithCopy { - - long runtime = 0 - List solutions = new LinkedList - //public List> additionalMatches = new LinkedList - List> copyTraces = new LinkedList - - long sartTime = System.nanoTime - List solutionTimes = new LinkedList - - /*def newSolution(ThreadContext context, SortedMap additonalMatch) { - additionalMatches+= additonalMatch - newSolution(context) - }*/ - - def newSolution(ThreadContext context) { - //print(System.nanoTime-initTime + ";") - val copyStart = System.nanoTime - val solution = context.model as PartialInterpretation - val copier = new EcoreUtil.Copier - val solutionCopy = copier.copy(solution) as PartialInterpretation - copier.copyReferences - solutions.add(solutionCopy) - copyTraces.add(copier) - runtime += System.nanoTime - copyStart - solutionTimes.add(System.nanoTime-sartTime) - } - def getSumRuntime() { - return runtime - } - def getAllRuntimes() { - return solutionTimes - } - def getSolutions() { - solutions - } - def getCopyTraces() { - return copyTraces - } -} \ 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/SurelyViolatedObjectiveGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend new file mode 100644 index 00000000..7fd494a0 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend @@ -0,0 +1,29 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.viatra.dse.objectives.IGlobalConstraint +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +@FinalFieldsConstructor +class SurelyViolatedObjectiveGlobalConstraint implements IGlobalConstraint { + val ViatraReasonerSolutionSaver solutionSaver + + override init(ThreadContext context) { + if (solutionSaver !== null) { + return + } + } + + override createNew() { + this + } + + override getName() { + class.name + } + + override checkGlobalConstraint(ThreadContext context) { + val bestFitness = DseUtils.caclulateBestPossibleFitness(context) + bestFitness.satisifiesHardObjectives && !solutionSaver.isFitnessDominated(bestFitness) + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend index aad9a448..7d0a7884 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend @@ -9,7 +9,7 @@ import org.eclipse.viatra.dse.objectives.Comparators class UnfinishedMultiplicityObjective implements IObjective { val MultiplicityGoalConstraintCalculator unfinishedMultiplicity; - public new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) { + new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) { this.unfinishedMultiplicity = unfinishedMultiplicity } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend deleted file mode 100644 index e0111cf6..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend +++ /dev/null @@ -1,56 +0,0 @@ -package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse - -import org.eclipse.viatra.dse.objectives.IObjective -import org.eclipse.viatra.query.runtime.api.IPatternMatch -import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher -import org.eclipse.viatra.query.runtime.api.IQuerySpecification -import java.util.Collection -import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine -import org.eclipse.viatra.query.runtime.emf.EMFScope -import org.eclipse.viatra.dse.base.ThreadContext -import java.util.List -import org.eclipse.viatra.dse.objectives.Comparators -import java.util.ArrayList -import java.util.Comparator - -class UnfinishedWFObjective implements IObjective { - Collection>> unfinishedWFs - val List> matchers - - public new(Collection>> unfinishedWFs) { - this.unfinishedWFs = unfinishedWFs - matchers = new ArrayList(unfinishedWFs.size) - } - override getName() '''unfinishedWFs''' - override createNew() { - return new UnfinishedWFObjective(unfinishedWFs) - } - override init(ThreadContext context) { - val engine = context.queryEngine//ViatraQueryEngine.on(new EMFScope(context.model)) - for(unfinishedWF : unfinishedWFs) { - matchers += unfinishedWF.getMatcher(engine) - } - } - - override getComparator() { Comparators.LOWER_IS_BETTER } - override getFitness(ThreadContext context) { - var sumOfMatches = 0 - for(matcher : matchers) { - val number = matcher.countMatches - //println('''«matcher.patternName» = «number»''') - sumOfMatches+=number - } - return sumOfMatches.doubleValue - } - - override getLevel() { 2 } - override isHardObjective() { true } - override satisifiesHardObjective(Double fitness) { return fitness <=0.01 } - - override setComparator(Comparator comparator) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") - } - override setLevel(int level) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") - } -} \ 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/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend new file mode 100644 index 00000000..5877778e --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend @@ -0,0 +1,99 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import java.util.HashMap +import java.util.Map +import org.eclipse.viatra.dse.api.DSEException +import org.eclipse.viatra.dse.api.Solution +import org.eclipse.viatra.dse.api.SolutionTrajectory +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.viatra.dse.objectives.Fitness +import org.eclipse.viatra.dse.objectives.IObjective +import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper +import org.eclipse.viatra.dse.solutionstore.SolutionStore.ISolutionSaver +import org.eclipse.xtend.lib.annotations.Accessors + +/** + * Based on {@link org.eclipse.viatra.dse.solutionstore.SolutionStore.BestSolutionSaver}. + */ +class ViatraReasonerSolutionSaver implements ISolutionSaver { + @Accessors val solutionCopier = new SolutionCopier + val boolean hasExtremalObjectives + val ObjectiveComparatorHelper comparatorHelper + val Map trajectories = new HashMap + + @Accessors(PUBLIC_SETTER) var Map solutionsCollection + + new(IObjective[][] leveledExtremalObjectives) { + comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) + hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] + } + + override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { + if (hasExtremalObjectives) { + saveBestSolutionOnly(context, id, solutionTrajectory) + } else { + basicSaveSolution(context, id, solutionTrajectory) + } + } + + private def saveBestSolutionOnly(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { + val fitness = context.lastFitness + val dominatedTrajectories = newArrayList + for (entry : trajectories.entrySet) { + val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) + if (isLastFitnessBetter < 0) { + // Found a trajectory that dominates the current one, no need to save + return false + } + if (isLastFitnessBetter > 0) { + dominatedTrajectories += entry.key + } + } + // We must save the new trajectory before removing dominated trajectories + // to avoid removing the current solution when it is reachable only via dominated trajectories. + val solutionSaved = basicSaveSolution(context, id, solutionTrajectory) + for (dominatedTrajectory : dominatedTrajectories) { + trajectories -= dominatedTrajectory + val dominatedSolution = dominatedTrajectory.solution + if (!dominatedSolution.trajectories.remove(dominatedTrajectory)) { + throw new DSEException( + "Dominated solution is not reachable from dominated trajectory. This should never happen!") + } + if (dominatedSolution.trajectories.empty) { + val dominatedSolutionId = dominatedSolution.stateCode + solutionCopier.markAsObsolete(dominatedSolutionId) + solutionsCollection -= dominatedSolutionId + } + } + solutionSaved + } + + private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { + val fitness = context.lastFitness + var boolean solutionSaved = false + var dseSolution = solutionsCollection.get(id) + if (dseSolution === null) { + solutionCopier.copySolution(context, id) + dseSolution = new Solution(id, solutionTrajectory) + solutionsCollection.put(id, dseSolution) + solutionSaved = true + } else { + solutionSaved = dseSolution.trajectories.add(solutionTrajectory) + } + if (solutionSaved) { + solutionTrajectory.solution = dseSolution + trajectories.put(solutionTrajectory, fitness) + } + solutionSaved + } + + def isFitnessDominated(Fitness fitness) { + for (existingFitness : trajectories.values) { + val isNewFitnessBetter = comparatorHelper.compare(fitness, existingFitness) + if (isNewFitnessBetter < 0) { + return true + } + } + false + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend index 5a528a9e..c601de40 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend @@ -1,5 +1,6 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse +import com.google.common.collect.ImmutableList import java.util.ArrayList import java.util.Collection import org.eclipse.viatra.dse.objectives.Comparators @@ -12,25 +13,34 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher class WF2ObjectiveConverter { - + static val UNFINISHED_WFS_NAME = "unfinishedWFs" + static val INVALIDATED_WFS_NAME = "invalidatedWFs" + def createCompletenessObjective( - Collection>> unfinishedWF) - { - val res = new ConstraintsObjective('''unfinishedWFs''', - unfinishedWF.map[ - new QueryConstraint(it.fullyQualifiedName,it,2.0) - ].toList + Collection>> unfinishedWF) { + createConstraintObjective(UNFINISHED_WFS_NAME, unfinishedWF) + } + + def createInvalidationObjective( + Collection>> invalidatedByWF) { + createConstraintObjective(INVALIDATED_WFS_NAME, invalidatedByWF) + } + + def IGlobalConstraint createInvalidationGlobalConstraint( + Collection>> invalidatedByWF) { + new ModelQueriesGlobalConstraint(INVALIDATED_WFS_NAME, new ArrayList(invalidatedByWF)) + } + + private def createConstraintObjective(String name, + Collection>> queries) { + val res = new ConstraintsObjective( + name, + ImmutableList.copyOf(queries.map [ + new QueryConstraint(it.fullyQualifiedName, it, 1.0) + ]) ) res.withComparator(Comparators.LOWER_IS_BETTER) res.level = 2 - return res - } - - def IGlobalConstraint createInvalidationObjective( - Collection>> invalidatedByWF) - { - return new ModelQueriesGlobalConstraint('''invalidatedWFs''', - new ArrayList(invalidatedByWF) - ) + res } -} \ No newline at end of file +} -- cgit v1.2.3-54-g00ecf