63 files changed, 514 insertions, 304 deletions
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin
index 213b9134..ba53fa44 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin
+++ b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin
Binary files differ
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin
index 21d26265..81608794 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin
+++ b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin
Binary files differ
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
index 3e879539..35ffaf65 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
@@ -138,7 +138,7 @@ class GenerationTaskExecutor {
                        
                        // 5.2 set values that defined directly 
                        solverConfig.solutionScope = new SolutionScope => [
-                                it.numberOfRequiredSolution = if(task.numberSpecified) {
+                                it.numberOfRequiredSolutions = if(task.numberSpecified) {
                                        task.number
                                } else {
                                        1
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
index a9573fbf..9eceef5f 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend
@@ -75,7 +75,7 @@ class SolverLoader {
                        ]
                } else if(solver === Solver::VIATRA_SOLVER) {
                        return new ViatraReasonerConfiguration => [c|
-                                c.debugCongiguration.partialInterpretatioVisualiser = new GraphvizVisualiser
+                                c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser
                                if(config.containsKey("diversity-range")) {
                                        val stringValue = config.get("diversity-range")
                                        try{
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/scoping/ApplicationConfigurationScopeProvider.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/scoping/ApplicationConfigurationScopeProvider.xtend
index 9d7e8aec..4daf9831 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/scoping/ApplicationConfigurationScopeProvider.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/scoping/ApplicationConfigurationScopeProvider.xtend
@@ -10,6 +10,7 @@ import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.EPackageI
 import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.MetamodelElement
 import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.MetamodelEntry
 import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.PatternEntry
+import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ReliabilityObjectiveFunction
 import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ViatraImport
 import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.CftModel
 import org.eclipse.emf.ecore.EClass
@@ -22,7 +23,6 @@ import org.eclipse.xtext.naming.IQualifiedNameConverter
 import org.eclipse.xtext.scoping.Scopes
 import static hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ApplicationConfigurationPackage.Literals.*
-import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ReliabilityObjectiveFunction
 /**
 * This class contains custom scoping description.
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend
index d88e2a52..e62a3cb7 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend
@@ -159,7 +159,7 @@ public class TypeScopes {
 */
 public class SolutionScope {
        public static val All = Integer.MAX_VALUE;
-        public var numberOfRequiredSolution = 1
+        public var numberOfRequiredSolutions = 1
 }
 /** Progress monitor class for a solver to
 * <li>(optionally) report progress via {@link worked}</li>
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
index 432651af..ceb78e99 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
@@ -57,7 +57,7 @@ class AlloySolver extends LogicReasoner{
                val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode)
                alloyConfig.progressMonitor.workedSearchFinished
                
-                val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
+                val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolutions,result2,forwardTrace,transformationTime)
                alloyConfig.progressMonitor.workedBackwardTransformationFinished
                //val solverFinish = System.currentTimeMillis-solverStart
                // Finish: Solving Alloy problem
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
index ebbca624..033ced04 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
@@ -184,7 +184,7 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
                                        } else {
                                                lastAnswer = lastAnswer.next
                                        }
-                                        configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution)
+                                        configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolutions)
                                        
                                        val runtime = System.currentTimeMillis -startTime
                                        synchronized(this) {
@@ -201,8 +201,8 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
        }
        
        def hasEnoughSolution(List<?> answers) {
-                if(configuration.solutionScope.numberOfRequiredSolution < 0) return false
+                if(configuration.solutionScope.numberOfRequiredSolutions < 0) return false
-                else return answers.size() == configuration.solutionScope.numberOfRequiredSolution
+                else return answers.size() == configuration.solutionScope.numberOfRequiredSolutions
        }
        
        public def getPartialAnswers() {
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,
-        override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
+                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 ||
-                val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output
+                        viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {
-                if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {
+                        workspace.writeModel(emptySolution, "init.partialmodel")
-                        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))
+                val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolutions)
-                for(additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) {
+                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)
+                dse.setInitialModel(emptySolution, false)
-                
-                val IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) {
+                val IStateCoderFactory statecoder = if (viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) {
-                        new NeighbourhoodBasedStateCoderFactory
+                                new NeighbourhoodBasedStateCoderFactory
-                } else {
+                        } else {
-                        new IdentifierBasedStateCoderFactory
+                                new IdentifierBasedStateCoderFactory
-                }
+                        }
                dse.stateCoderFactory = statecoder
-                
                dse.maxNumberOfThreads = 1
-                
-                val solutionStore =  new SolutionStore(configuration.solutionScope.numberOfRequiredSolution)
+                for (rule : method.relationRefinementRules) {
-                dse.solutionStore = solutionStore
-                
-                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 {
-                try{
+                        stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000);
-                        stoppedByTimeout = dse.startExplorationWithTimeout(strategy,configuration.runtimeLimit*1000);
-                        stoppedByException = false
                } 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 = viatraConfig.runtimeLimit
-                        it.solverTime = (solverTime/1000000) as int
+                        it.solverTime = (solverTime / 1000000) as int
-                        it.transformationTime = (transformationTime/1000000) as int
+                        it.transformationTime = (transformationTime / 1000000) as int
-                        for(x : 0..<strategy.solutionStoreWithCopy.allRuntimes.size) {
+                        for (pair : solutionCopier.getAllCopierRuntimes(true).indexed) {
                                it.entries += createIntStatisticEntry => [
-                                        it.name = '''_Solution«x»FoundAt'''
+                                        it.name = '''_Solution«pair.key»FoundAt'''
-                                        it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int
+                                        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) {
+                if (stoppedByTimeout) {
-                        return createInsuficientResourcesResult=>[
+                        return createInsuficientResourcesResult => [
                                it.problem = problem
-                                it.resourceName="time"
+                                it.resourceName = "time"
-                                it.representation += strategy.solutionStoreWithCopy.solutions
+                                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.trace = solutionCopier.getTraces(true)
-                                        it.representation += strategy.solutionStoreWithCopy.solutions
+                                        it.representation += solutionCopier.getPartialInterpretations(true)
                                        it.statistics = statistics
                                ]
                        }
                }
        }
-    private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) {
+        private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) {
-        sc.sumStatecoderRuntime
+                sc.sumStatecoderRuntime
-    }
+        }
-    private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) {
+        private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) {
-        sc.sumStatecoderRuntime
+                sc.sumStatecoderRuntime
-    }
+        }
        override getInterpretations(ModelResult modelResult) {
-                val indexes = 0..<modelResult.representation.size
+                val indexes = 0 ..< modelResult.representation.size
                val traces = modelResult.trace as List<Map<EObject, EObject>>;
-                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<RelationDeclaration> 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<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> 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<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();
+                final Fitness firstfitness = context.calculateFitness();
-                checkForSolution(firstFittness);
+                checkForSolution(firstfitness);
                
                final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
                final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
-                TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness);
+                TrajectoryWithFitness currentTrajectoryWithfitness = new TrajectoryWithFitness(firstTrajectory, firstfitness);
-                trajectoiresToExplore.add(currentTrajectoryWithFittness);
+                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,
+                                        int compare = objectiveComparatorHelper.compare(currentTrajectoryWithfitness.fitness,
-                                                        nextTrajectoryWithFittness.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);
+                        trajectoiresToExplore.remove(currentTrajectoryWithfitness);
-                        currentTrajectoryWithFittness = null;
+                        currentTrajectoryWithfitness = null;
                }
                logger.info("Interrupted.");
@@ -269,15 +264,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                return activationIds;
        }
-        private void checkForSolution(final Fitness fittness) {
+        private void checkForSolution(final Fitness fitness) {
-                if (fittness.isSatisifiesHardObjectives()) {
+                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{
+@FinalFieldsConstructor
-        val ScopeObjective scopeObjective
+class ModelGenerationCompositeObjective implements IThreeValuedObjective {
-        val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives
+        val IObjective scopeObjective
-        val UnfinishedWFObjective unfinishedWFObjective
+        val List<IObjective> unfinishedMultiplicityObjectives
-        
+        val IObjective unfinishedWFObjective
-        public new(
-                ScopeObjective scopeObjective,
-                List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
-                UnfinishedWFObjective unfinishedWFObjective)
-        {
-                this.scopeObjective = scopeObjective
-                this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives
-                this.unfinishedWFObjective = 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) {
+                for (multiplicityObjective : unfinishedMultiplicityObjectives) {
-                        multiplicity+=multiplicityObjective.getFitness(context)//*0.5
+                        multiplicity += multiplicityObjective.getFitness(context) // *0.5
                }
-                sum+=multiplicity
+                sum += multiplicity
-                sum += unfinishedWFsFitness//*0.5
+                sum += unfinishedWFsFitness // *0.5
-                
+                // println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
-                //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
-                
                return sum
        }
        
-        override getLevel() { 2 }
+        override getWorstPossibleFitness(ThreadContext threadContext) {
-        override getName() { "CompositeUnfinishednessObjective"}
+                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)
+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) {
-        {
+                createConstraintObjective(UNFINISHED_WFS_NAME, unfinishedWF)
-                val res = new ConstraintsObjective('''unfinishedWFs''',
+        }
-                        unfinishedWF.map[
-                                new QueryConstraint(it.fullyQualifiedName,it,2.0)
+        def createInvalidationObjective(
-                        ].toList
+                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
+                res
-        }
-        
-        def IGlobalConstraint createInvalidationObjective(
-                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF)
-        {
-                return new ModelQueriesGlobalConstraint('''invalidatedWFs''',
-                        new ArrayList(invalidatedByWF)
-                )
        }
-}
-\ No newline at end of file
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ide/.CftLanguageIdeModule.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ide/.CftLanguageIdeModule.xtendbin
index b05b37d4..2c3fb067 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ide/.CftLanguageIdeModule.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ide/.CftLanguageIdeModule.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ide/.CftLanguageIdeSetup.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ide/.CftLanguageIdeSetup.xtendbin
index 7a01ace8..dd1a46c1 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ide/.CftLanguageIdeSetup.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ide/.CftLanguageIdeSetup.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/.CftLanguageUiModule.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/.CftLanguageUiModule.xtendbin
index 0e56af1c..1694059d 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/.CftLanguageUiModule.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/.CftLanguageUiModule.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/contentassist/.CftLanguageProposalProvider.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/contentassist/.CftLanguageProposalProvider.xtendbin
index e3b08949..e89abd97 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/contentassist/.CftLanguageProposalProvider.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/contentassist/.CftLanguageProposalProvider.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/labeling/.CftLanguageDescriptionLabelProvider.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/labeling/.CftLanguageDescriptionLabelProvider.xtendbin
index a9a231c9..c2485146 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/labeling/.CftLanguageDescriptionLabelProvider.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/labeling/.CftLanguageDescriptionLabelProvider.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/labeling/.CftLanguageLabelProvider.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/labeling/.CftLanguageLabelProvider.xtendbin
index c96ad697..cdef3946 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/labeling/.CftLanguageLabelProvider.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/labeling/.CftLanguageLabelProvider.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/outline/.CftLanguageOutlineTreeProvider.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/outline/.CftLanguageOutlineTreeProvider.xtendbin
index 7c4945f3..04b65373 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/outline/.CftLanguageOutlineTreeProvider.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/outline/.CftLanguageOutlineTreeProvider.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/quickfix/.CftLanguageQuickfixProvider.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/quickfix/.CftLanguageQuickfixProvider.xtendbin
index 6f9ed2db..13419ed3 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/quickfix/.CftLanguageQuickfixProvider.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/quickfix/.CftLanguageQuickfixProvider.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/syntaxcoloring/.CftLanguageSemanticHighlightingCalculator.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/syntaxcoloring/.CftLanguageSemanticHighlightingCalculator.xtendbin
index 319b1a7b..42bf1c75 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/syntaxcoloring/.CftLanguageSemanticHighlightingCalculator.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/syntaxcoloring/.CftLanguageSemanticHighlightingCalculator.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/syntaxcoloring/.CftLanguageTokenToAttributeIdMapper.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/syntaxcoloring/.CftLanguageTokenToAttributeIdMapper.xtendbin
index 64980787..09c27dfe 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/syntaxcoloring/.CftLanguageTokenToAttributeIdMapper.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components.ui/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/ui/syntaxcoloring/.CftLanguageTokenToAttributeIdMapper.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/.CftLanguageRuntimeModule.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/.CftLanguageRuntimeModule.xtendbin
index e3eb300d..25c11260 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/.CftLanguageRuntimeModule.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/.CftLanguageRuntimeModule.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/.CftLanguageStandaloneSetup.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/.CftLanguageStandaloneSetup.xtendbin
index cf472a5c..7a10919f 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/.CftLanguageStandaloneSetup.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/.CftLanguageStandaloneSetup.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/conversion/.CftLanguageValueConverterService.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/conversion/.CftLanguageValueConverterService.xtendbin
index 9e436c25..f4a74d7b 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/conversion/.CftLanguageValueConverterService.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/conversion/.CftLanguageValueConverterService.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/conversion/.OF_INTValueConverter.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/conversion/.OF_INTValueConverter.xtendbin
index 8dcb67ce..8d4c818e 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/conversion/.OF_INTValueConverter.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/conversion/.OF_INTValueConverter.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/generator/.CftLanguageGenerator.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/generator/.CftLanguageGenerator.xtendbin
index f55b7c31..79e0e382 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/generator/.CftLanguageGenerator.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/generator/.CftLanguageGenerator.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/naming/.CftLanguageQualifiedNameProvider.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/naming/.CftLanguageQualifiedNameProvider.xtendbin
index 1f55e190..51f5e2fe 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/naming/.CftLanguageQualifiedNameProvider.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/naming/.CftLanguageQualifiedNameProvider.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/naming/.PackageNameProvider.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/naming/.PackageNameProvider.xtendbin
index d7439d22..cf8f603b 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/naming/.PackageNameProvider.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/naming/.PackageNameProvider.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/scoping/.CftLanguageImportedNamespaceAwareLocalScopeProvider.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/scoping/.CftLanguageImportedNamespaceAwareLocalScopeProvider.xtendbin
index 4fbc7cd3..116d5bc1 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/scoping/.CftLanguageImportedNamespaceAwareLocalScopeProvider.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/scoping/.CftLanguageImportedNamespaceAwareLocalScopeProvider.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/scoping/.CftLanguageScopeProvider.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/scoping/.CftLanguageScopeProvider.xtendbin
index 5b585e60..7a6eb47e 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/scoping/.CftLanguageScopeProvider.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/scoping/.CftLanguageScopeProvider.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/validation/.CftLanguageValidator.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/validation/.CftLanguageValidator.xtendbin
index 481a23f6..fbb89193 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/validation/.CftLanguageValidator.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.components/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/components/validation/.CftLanguageValidator.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.model/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/model/util/.CftExtensions.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.model/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/model/util/.CftExtensions.xtendbin
index 390ee219..0e63880f 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.model/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/model/util/.CftExtensions.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.model/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/model/util/.CftExtensions.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.Cft2FtTransformation.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.Cft2FtTransformation.xtendbin
index 594bfecb..dfae40e9 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.Cft2FtTransformation.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.Cft2FtTransformation.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventCollection.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventCollection.xtendbin
index a868ae36..0aaf712d 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventCollection.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventCollection.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventMaterializer.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventMaterializer.xtendbin
index f7ca5531..e51f73a6 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventMaterializer.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventMaterializer.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.FaultTreeBuilder.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.FaultTreeBuilder.xtendbin
index 1d15efbb..89e003dc 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.FaultTreeBuilder.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.FaultTreeBuilder.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentFaultTreeTrace.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentFaultTreeTrace.xtendbin
index 3fce519e..028440a8 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentFaultTreeTrace.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentFaultTreeTrace.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentInstanceTrace.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentInstanceTrace.xtendbin
index 564e58c4..d542ba2d 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentInstanceTrace.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentInstanceTrace.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentNameGenerator.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentNameGenerator.xtendbin
index ebcfced8..949da0cd 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentNameGenerator.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentNameGenerator.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.Ecore2CftTransformation.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.Ecore2CftTransformation.xtendbin
index d4b5ecdb..82c045e2 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.Ecore2CftTransformation.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.Ecore2CftTransformation.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.InputTrace.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.InputTrace.xtendbin
index 1faa21b3..ffd70c04 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.InputTrace.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.InputTrace.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.LookupHandler.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.LookupHandler.xtendbin
index afc40951..418c71d4 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.LookupHandler.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.LookupHandler.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingHandler.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingHandler.xtendbin
index 419b9490..86c0d704 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingHandler.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingHandler.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingQueries.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingQueries.xtendbin
index 0e703f40..c9dda5c4 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingQueries.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingQueries.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/.Ft2GalileoTransformation.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/.Ft2GalileoTransformation.xtendbin
index 41e6e441..0956e6e0 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/.Ft2GalileoTransformation.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/.Ft2GalileoTransformation.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin
index ef8c3b88..cdaacb58 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin
index 4aff77d3..6e1908aa 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin
index a2c634bc..5772b0e7 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin
index 45f12291..e1c1a8c7 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin
Binary files differ
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.ui/bin/.gitignore b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.ui/bin/.gitignore
new file mode 100644
index 00000000..1c0a02cd
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.ui/bin/.gitignore
@@ -0,0 +1 @@
+/hu/
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/configs/generation.vsconfig b/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/configs/generation.vsconfig
index 9a073728..490d6942 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/configs/generation.vsconfig
+++ b/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/configs/generation.vsconfig
@@ -7,7 +7,7 @@ generate {
        partial-model = { "inputs/FamInstance.xmi"}
        solver = ViatraSolver
        scope = {
-                #node = 5
+                #node = 500
        }
        
        config = {