12 files changed, 393 insertions, 196 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
index 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<TrajectoryWithFitness> 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<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives

-        val UnfinishedWFObjective unfinishedWFObjective

-        

-        public new(

-                ScopeObjective scopeObjective,

-                List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,

-                UnfinishedWFObjective unfinishedWFObjective)

-        {

-                this.scopeObjective = scopeObjective

-                this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives

-                this.unfinishedWFObjective = unfinishedWFObjective

-        }

-        

+@FinalFieldsConstructor

+class ModelGenerationCompositeObjective implements IThreeValuedObjective {

+        val IObjective scopeObjective

+        val List<IObjective> 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<Double> 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<EObject, EObject> trace
+        @Accessors val long copierRuntime
+        @Accessors var boolean current = true
+}
+
+class SolutionCopier {
+        val copiedSolutions = new LinkedHashMap<Object, CopiedSolution>
+
+        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<PartialInterpretation> getPartialInterpretations(boolean currentOnly) {
+                getListOfCopiedSolutions(currentOnly).map[partialInterpretations]
+        }
+
+        def List<Map<EObject, EObject>> getTraces(boolean currentOnly) {
+                getListOfCopiedSolutions(currentOnly).map[trace]
+        }
+
+        def List<Long> getAllCopierRuntimes(boolean currentOnly) {
+                getListOfCopiedSolutions(currentOnly).map[copierRuntime]
+        }
+
+        def List<CopiedSolution> 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<PartialInterpretation> solutions = new LinkedList

-        //public List<SortedMap<String,Integer>> additionalMatches = new LinkedList

-        List<Map<EObject,EObject>> copyTraces = new LinkedList

-        

-        long sartTime = System.nanoTime

-        List<Long> solutionTimes = new LinkedList

-        

-        /*def newSolution(ThreadContext context, SortedMap<String,Integer> 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<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs

-        val List<ViatraQueryMatcher<?>> matchers

-        

-        public new(Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 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<Double> 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<SolutionTrajectory, Fitness> trajectories = new HashMap
+
+        @Accessors(PUBLIC_SETTER) var Map<Object, Solution> 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<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF)

-        {

-                val res = new ConstraintsObjective('''unfinishedWFs''',

-                        unfinishedWF.map[

-                                new QueryConstraint(it.fullyQualifiedName,it,2.0)

-                        ].toList

+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) {

+                createConstraintObjective(UNFINISHED_WFS_NAME, unfinishedWF)

+        }

+

+        def createInvalidationObjective(

+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {

+                createConstraintObjective(INVALIDATED_WFS_NAME, invalidatedByWF)

+        }

+

+        def IGlobalConstraint createInvalidationGlobalConstraint(

+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {

+                new ModelQueriesGlobalConstraint(INVALIDATED_WFS_NAME, new ArrayList(invalidatedByWF))

+        }

+

+        private def createConstraintObjective(String name,

+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 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<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF)

-        {

-                return new ModelQueriesGlobalConstraint('''invalidatedWFs''',

-                        new ArrayList(invalidatedByWF)

-                )

+                res

         }

-}
\ No newline at end of file
+}