Migrating Additional projects

author: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
committer: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
commit: 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree: 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme
parent: Initial commit, migrating from SVN (diff)
download: VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
17 files changed, 1911 insertions, 0 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicModelInterpretation.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicModelInterpretation.xtend
new file mode 100644
index 00000000..a2d30b1b
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicModelInterpretation.xtend
@@ -0,0 +1,102 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import java.util.List
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+interface LogicModelInterpretation{
+        
+        /**
+         * Returns the elements of a type.
+         */     
+        def List<DefinedElement> getElements(Type type)
+        /**
+         * Returns the interpretation of a function. The parameters and the return values are encoded to primitive java objects defined by the following table:
+         * <p><table>
+         * <tr><th>Term type</th><th>Java object type</th></tr>
+         * <tr><td>Element of a type </td><td>DefinedElement </td></tr>
+         * <tr><td>Boolean literal </td><td>Boolean </td></tr>
+         * <tr><td>Integer literal </td><td>Integer </td></tr>
+         * <tr><td>Real literal </td><td>BigDecimal </td></tr>
+         * </table></p>
+         * @param function The target function to be interpreted.
+         * @param parameterSubstitution The array of the substituted parameters encoded as defined in the table.
+         * @return The result of the function call encoded as defined in the table.
+         */
+        def Object getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution)
+        /**
+         * Returns the interpretation of a relation. The parameters are encoded to primitive java objects defined by the following table:
+         * <p><table>
+         * <tr><th>Term type</th><th>Java object type</th></tr>
+         * <tr><td>Element of a type </td><td>DefinedElement </td></tr>
+         * <tr><td>Boolean literal </td><td>Boolean </td></tr>
+         * <tr><td>Integer literal </td><td>Integer </td></tr>
+         * <tr><td>Real literal </td><td>BigDecimal </td></tr>
+         * </table></p>
+         * @param relation The target relation to be interpreted.
+         * @param parameterSubstitution The array of the substituted parameters encoded as defined in the table.
+         * @return If the parameter tuple is in the relation.
+         */
+        def boolean getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution)
+        /**
+         * Returns the interpretation of a constant. The value is encoded to primitive java objects defined by the following table:
+         * <p><table>
+         * <tr><th>Term type</th><th>Java object type</th></tr>
+         * <tr><td>Element of a type </td><td>DefinedElement </td></tr>
+         * <tr><td>Boolean literal </td><td>Boolean </td></tr>
+         * <tr><td>Integer literal </td><td>Integer </td></tr>
+         * <tr><td>Real literal </td><td>BigDecimal </td></tr>
+         * </table></p>
+         * @param constant The target constant to be interpreted.
+         * @return The value of the constant encoded as specified in the table.
+         */
+        def Object getInterpretation(ConstantDeclaration constant)
+        def int getMinimalInteger()
+        def int getMaximalInteger()
+}
+class Uninterpreted implements LogicModelInterpretation {
+        /*private val static unknownBecauseUninterpreted = LogiclanguageFactory.eINSTANCE.createUnknownBecauseUninterpreted
+        public def static getUnknownBecauseUninterpreted() {return Uninterpreted.unknownBecauseUninterpreted}*/
+        
+        override getElements(Type type) {
+                throw new UnsupportedOperationException("The interpteration is unknown.")
+        }
+        
+        def getKnownElements(Type type) {
+                val allSubtypes = type.transitiveClosureStar[it.subtypes]
+                return allSubtypes.filter(TypeDefinition).map[elements].flatten.toList
+        }
+        
+        def allElementsAreInterpreted(Type type) {
+                val allSubtypes = type.transitiveClosureStar[it.subtypes]
+                return allSubtypes.exists[it instanceof TypeDeclaration]
+        }
+        
+        override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
+                throw new UnsupportedOperationException("The interpteration is unknown.")
+        }
+        
+        override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+                throw new UnsupportedOperationException("The interpteration is unknown.")
+        }
+        
+        override getInterpretation(ConstantDeclaration constant) {
+                throw new UnsupportedOperationException("The interpteration is unknown.")
+        }
+        
+        override getMinimalInteger() {
+                throw new UnsupportedOperationException("The interpteration is unknown.")
+        }
+        
+        override getMaximalInteger() {
+                throw new UnsupportedOperationException("The interpteration is unknown.")
+        }
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend
new file mode 100644
index 00000000..ba1b9fd6
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend
@@ -0,0 +1,563 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemFactory
+import hu.bme.mit.inf.dslreasoner.util.LogicProblemBuilder_AdvancedConstructs
+import java.math.BigDecimal
+import java.util.ArrayList
+import java.util.Collections
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.emf.ecore.util.EcoreUtil
+import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.xtext.xbase.lib.Functions.Function1
+@Data class FunctionDescription {
+        Iterable<TypeReference> parameters
+        TypeReference range
+}
+class LogicProblemBuilderException extends Exception {
+        new(String reason) {
+                super(reason)
+        }
+}
+public class LogicProblemBuilder{
+        val protected extension LogiclanguageFactory logicFactiory = LogiclanguageFactory.eINSTANCE
+        val protected extension LogicproblemFactory problemFactory = LogicproblemFactory.eINSTANCE
+        val protected advancedConstructs = new LogicProblemBuilder_AdvancedConstructs(this)
+        
+        def public createProblem(){     createLogicProblem      }
+        
+        // Names
+        def protected String canonize(CharSequence name) {
+                if(name == null) return ""
+                val result = name.toString.split("\\s+");
+                if(result.size == 1) {
+                        val element = result.get(0);
+                        if(element == "bool" ||
+                           element == "int" ||
+                           element == "real") throw new LogicProblemBuilderException('''Reserved keyword "«element»"!''')
+                        else return result.join(' ')
+                }
+                else return result.join(' ')
+        }
+        def protected String generateUniqueName(Iterable<String> previous, Function1<Integer,String> namer) {
+                var int i = 0
+                var generateNew = false;
+                var String finalName;
+                do {
+                        i = i+1;
+                        val nameCandidate = namer.apply(i)
+                        finalName = nameCandidate
+                        generateNew = previous.exists[equals(nameCandidate)]
+                }
+                while(generateNew)
+                return finalName
+        }
+        
+        // Type builders
+        def public Element(CharSequence elementName) { return createDefinedElement => [x|x.name = elementName.canonize] }
+        def public Element() { return createDefinedElement }
+        def public TypeDeclaration(CharSequence name, boolean isAbstract) { TypeDeclaration => [x | x.name = name.canonize x.isAbstract = isAbstract] }
+        def public TypeDeclaration() { createTypeDeclaration }
+        def public TypeDefinition(CharSequence name, boolean isAbstract, DefinedElement... elements) { TypeDefinition(name, isAbstract, elements as Iterable<DefinedElement>) }
+        def public TypeDefinition(CharSequence name, boolean isAbstract, Iterable<DefinedElement> elements) { createTypeDefinition => [x | x.name = name.canonize x.isAbstract = isAbstract x.elements += elements ] }
+        
+        def public Supertype(Type subtype, Type supertype) {
+                subtype.supertypes+=supertype
+        }
+        def public SetSupertype(Type subtype, Type supertype, boolean value) {
+                if(value) subtype.supertypes+=supertype
+                else subtype.subtypes-=supertype
+        }
+        
+        // Type add
+        def public add(LogicProblem problem, Type type) {
+                problem.nameIfAnonymType(type)
+                problem.types+=type
+                if(type instanceof TypeDefinition) {
+                        problem.elements+=type.elements
+                }
+                return type
+        }
+        def protected dispatch nameIfAnonymType(LogicProblem problem, Type typeDeclaration) {
+                if(typeDeclaration.name.nullOrEmpty) 
+                        typeDeclaration.name = problem.types.map[it.name].generateUniqueName[i | '''type «i.toString»''']
+        }
+        def protected dispatch nameIfAnonymType(LogicProblem problem, TypeDefinition typeDefinition) {
+                if(typeDefinition.name.nullOrEmpty) 
+                        typeDefinition.name = problem.types.map[it.name].generateUniqueName[i | '''type «i.toString»''']
+                for(element : typeDefinition.elements) 
+                        if(element.name.nullOrEmpty) 
+                                element.name = typeDefinition.elements.map[it.name].generateUniqueName[i | '''type «i.toString»''']           
+        }
+        
+        def public LogicBool() { createBoolTypeReference }
+        def public LogicInt() { createIntTypeReference }
+        def public LogicReal() { createRealTypeReference }
+        def toTypeReference(TypeDescriptor descriptor) {
+                if(descriptor instanceof TypeReference) { return EcoreUtil.copy(descriptor); }
+                else if(descriptor instanceof Type) { return createComplexTypeReference => [referred = descriptor]}
+                else throw new UnsupportedOperationException("Unsupported type descriptor: " + descriptor.class)
+        }
+        
+        // Variables
+        def public createVar(CharSequence name, TypeDescriptor range) {
+                return createVariable => [it.name = name.canonize it.range = range.toTypeReference]
+        }
+        
+        // Functions
+        def public FunctionDescription ->(TypeDescriptor parameter, TypeDescriptor range) { return #[parameter] -> range }
+        def public FunctionDescription ->(Iterable<? extends TypeDescriptor> parameters, TypeDescriptor range) { return new FunctionDescription(parameters.map[toTypeReference], range.toTypeReference); }
+        def public FunctionDeclaration(CharSequence name, FunctionDescription functionDescription) { FunctionDeclaration(name,functionDescription.range, functionDescription.parameters) }
+        def public FunctionDeclaration(FunctionDescription functionDescription) { FunctionDeclaration(functionDescription.range, functionDescription.parameters) }
+        def public FunctionDeclaration(CharSequence name, TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(name, range, parameters as Iterable<? extends TypeReference>)       }       
+        def public FunctionDeclaration(TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(range, parameters as Iterable<? extends TypeReference>)        }
+        def public FunctionDeclaration(CharSequence name, TypeDescriptor range, Iterable<? extends TypeDescriptor> parameters) { return FunctionDeclaration(range,parameters) => [x|x.name = name.canonize] }
+        def public FunctionDeclaration(TypeDescriptor range, Iterable<? extends TypeDescriptor> parameters) {
+                val function = createFunctionDeclaration
+                for(parameter : parameters) function.parameters+=parameter.toTypeReference
+                function.range = range.toTypeReference
+                return function
+        }
+        
+        def public FunctionDefinition(CharSequence name, TypeDescriptor range, Function1<VariableContext, ? extends TermDescription> expression) {
+                val context = new VariableContext(this,logicFactiory)
+                val definition = expression.apply(context)
+                return FunctionDefinition(name,range,context.variables,definition);
+        }
+        def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<Variable> variables, TermDescription definition) {
+                return createFunctionDefinition => [
+                        it.name = name.canonize
+                        it.parameters += variables.map[it.range.toTypeReference]
+                        it.variable += variables
+                        it.range = range.toTypeReference
+                        it.value = definition.toTerm
+                ]
+        }
+        def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<TypeDescriptor> parameters, Map<List<Term>,Term> parametersToValue) {
+                return FunctionDefinition(name,range,parameters,parametersToValue,null)
+        }
+        def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<TypeDescriptor> parameters, Map<List<Term>,Term> parametersToValue, Term defaultValue) {
+                val parameterList = parameters.toList;
+                val variableList = (1..parameterList.size).map[index | '''param «index»'''.createVar(parameterList.get(index-1))].toList
+                return FunctionDefinition(name,range,variableList,advancedConstructs.FunctionDefinitionBody(variableList,parametersToValue,defaultValue))
+        }
+        
+        // Add function to a problem
+        def public add(LogicProblem input, Function function) {
+                input.nameIfAnonymFunction(function)
+                input.checkFunction(function)
+                input.functions += function
+                return function
+        }
+        def public add(LogicProblem input, FunctionDescription functionDescription) { input.add(FunctionDeclaration(functionDescription)) }
+        def protected nameIfAnonymFunction(LogicProblem problem, Function functionDeclaration) {
+                if(functionDeclaration.name.nullOrEmpty) {
+                        functionDeclaration.name = problem.functions.map[it.name].generateUniqueName[i | "function"+i]
+                }
+        }
+        def protected checkFunction(LogicProblem problem, Function function) {
+                if(problem.functions.exists(x|x.name == function.name))
+                        throw new LogicProblemBuilderException('''Function with the following name is already defined: "«function.name»"!''')
+                for(ref : function.parameters.filter(typeof(ComplexTypeReference)).map[referred]) {
+                        if(!problem.types.contains(ref))
+                                throw new LogicProblemBuilderException('''Type "«ref.name»" is not availabe in the logic problem!''')
+                }
+                val range = function.range
+                if(range instanceof ComplexTypeReference) {
+                        if(!problem.types.contains(range.referred))
+                                throw new LogicProblemBuilderException('''Type "«range.referred.name»" is not availabe in the logic problem!''')
+                }
+        }
+        
+        // Constants
+        def public ConstantDeclaration(CharSequence name, TypeDescriptor type) { ConstantDeclaration(type) => [it.name = name.canonize] }
+        def public ConstantDeclaration(TypeDescriptor type) { createConstantDeclaration => [it.type = type.toTypeReference] }
+        
+        def public ConstantDefinition(CharSequence name, TypeDescriptor type, TermDescription value) {
+                createConstantDefinition => [it.name = name.canonize it.type = type.toTypeReference it.value = value.toTerm]
+        }
+        
+        // Add constant to a problem
+        def public add(LogicProblem problem, Constant constant) {
+                problem.nameIfAnonymConstant(constant);
+                problem.checkConstant(constant)
+                problem.constants += constant
+                return constant
+        }
+        def protected nameIfAnonymConstant(LogicProblem problem, Constant constant) {
+                if(constant.name.nullOrEmpty) {
+                        constant.name = problem.constants.map[it.name].generateUniqueName[i | "constant"+i]
+                }
+        }
+        def protected checkConstant(LogicProblem problem, Constant constant) {
+                if(problem.constants.exists(x|x.name == constant.name))
+                        throw new LogicProblemBuilderException('''Constant with the following name is already defined: "«constant.name»"!''')
+                if((constant.type instanceof ComplexTypeReference) && ! (problem.types.contains((constant.type as ComplexTypeReference).referred))) 
+                                throw new LogicProblemBuilderException('''Type "«(constant.type as ComplexTypeReference).referred.name»" is not availabe in the logic problem!''')
+        }
+        
+        // Relations    
+        def public RelationDeclaration(CharSequence name,  TypeDescriptor... parameters) { return RelationDeclaration(name, parameters as Iterable<? extends TypeReference>)    }
+        def public RelationDeclaration(CharSequence name, Iterable<? extends TypeDescriptor> parameters) { return RelationDeclaration(parameters) => [x|x.name = name.canonize] }
+        def public RelationDeclaration(TypeDescriptor... parameters) { RelationDeclaration( parameters as Iterable<? extends TypeReference>)    }
+        def public RelationDeclaration(Iterable<? extends TypeDescriptor> parameters) {
+                val relation = createRelationDeclaration
+                for(parameter : parameters) {
+                        relation.parameters+=parameter.toTypeReference
+                }
+                return relation
+        }
+        
+        def public RelationDefinition(CharSequence name, Function1<VariableContext, ? extends TermDescription> expression) {
+                val context = new VariableContext(this,logicFactiory);
+                val definition = expression.apply(context);
+                return RelationDefinition(name,context.variables,definition)
+        }
+        def public RelationDefinition(CharSequence name, Iterable<Variable> variables, TermDescription definition) {
+                return createRelationDefinition => [
+                        it.name = name.canonize
+                        it.parameters += variables.map[it.range.toTypeReference]
+                        it.variables += variables
+                        it.value = definition?.toTerm
+                ]
+        }
+        def public RelationDefinition(CharSequence name, Iterable<? extends TypeDescriptor> parameters, Iterable<? extends List<? extends TermDescription>> possibleValues) {
+                val res = createRelationDefinition => [it.name = name.canonize]
+                val variableMap = new ArrayList(parameters.size)
+                var index = 0
+                for(parameter : parameters) {
+                        val actualIndex = index
+                        val newVar = createVariable=>[it.name ='''var «actualIndex»'''.canonize it.range = parameter.toTypeReference]
+                        variableMap.add(index,newVar)
+                        res.variables+=newVar
+                        res.parameters+=newVar.range
+                        index+=1
+                }
+                res.value = possibleValues.map[possibleValue |(0..<parameters.size).map[i| variableMap.get(i) == possibleValue.get(i).toTerm].And].Or
+                return res      
+        }
+        
+        // Add Relation to a problem
+        def public add(LogicProblem input, Relation relation) {
+                input.nameIfAnonymRelation(relation)
+                input.checkRelation(relation)
+                input.relations+=relation
+                //println('''«relation.name» - [«relation.parameters»]''')
+                return relation
+        }
+        
+        def protected nameIfAnonymRelation(LogicProblem problem, Relation relation) {
+                if(relation.name.nullOrEmpty) {
+                        relation.name = problem.relations.map[it.name].generateUniqueName[i | "relation"+i]
+                }
+        }
+        def protected checkRelation(LogicProblem problem, Relation relation) {
+                if(problem.relations.exists(x|x.name == relation.name))
+                        throw new LogicProblemBuilderException('''Relation with the following name is already defined: "«relation.name»"!''')
+                for(ref : relation.parameters.filter(typeof(ComplexTypeReference)).map[referred]) {
+                        if(!problem.types.contains(ref))
+                                throw new LogicProblemBuilderException('''Type "«ref.name»" is not availabe in the logic problem!''')
+                }
+                if(relation instanceof RelationDefinition) {
+                        checkDefinition(relation)
+                }
+        }
+        
+        // Assertion
+        def public Assertion(TermDescription term) {
+                val result = term.toTerm
+                result.nameAnonymVariables(Collections.EMPTY_LIST)
+                createAssertion => [it.value = result]
+        }
+        def public Assertion(CharSequence name, TermDescription term) {
+                val result = term.toTerm
+                result.nameAnonymVariables(Collections.EMPTY_LIST)
+                createAssertion => [it.value = result it.name=name.canonize]
+        }
+        def public add(LogicProblem problem, Assertion assertion) {
+                if(assertion.name.nullOrEmpty) {
+                        val name = problem.assertions.map[name].generateUniqueName["assertion"+it]
+                        assertion.name=name
+                }
+                checkAssertion(assertion)
+                problem.assertions+=assertion
+                return assertion
+        }
+        
+        def public add(LogicProblem problem, TermDescription term) {
+                problem.add(Assertion(term))
+        }
+        
+                
+        def checkAssertion(Assertion assertion) {
+                for(value : assertion.eAllContents.filter(SymbolicValue).toIterable) {
+                        var referred = value.symbolicReference
+                        if(referred instanceof Variable) {
+                                if(!value.hasDeclaredVariable(referred)){
+                                        throw new LogicProblemBuilderException('''Variable "«referred.name»" is not availabe in the logic problem!''')
+                                }
+                        }
+                }
+        }
+        
+        def public checkDefinition(EObject definition) {
+                /*for(value : definition.eAllContents.filter(SymbolicValue).toIterable) {
+                        var referred = value.symbolicReference
+                        if(referred instanceof Variable) {
+                                if(!value.hasDeclaredVariable(referred)){
+                                        throw new LogicProblemBuilderException('''Variable "«referred.name»" is not availabe in the logic problem!''')
+                                }
+                        }
+                }*/
+        }
+        
+        // Containment
+        def public ContainmentHierarchy(
+                Iterable<? extends Type> typesInHierarchy,
+                Iterable<? extends Function> containmentFunctions,
+                Iterable<? extends Relation> containmentRelations,
+                Constant rootConstant
+        ) {
+                val result = createContainmentHierarchy => [
+                        it.typesOrderedInHierarchy += typesInHierarchy
+                        it.containmentFunctions += containmentFunctions
+                        it.containmentRelations += containmentRelations
+                        it.rootConstant = rootConstant
+                ]
+                return result
+        }
+        def public add(LogicProblem problem, ContainmentHierarchy hierarchy) {
+                problem.containmentHierarchies+=hierarchy
+                return hierarchy
+        }
+        
+        // Terms
+        
+        private dispatch def boolean hasDeclaredVariable(QuantifiedExpression term, Variable variable) {
+                return term.quantifiedVariables.contains(variable) || ((term.eContainer instanceof Term) && (term.eContainer as Term).hasDeclaredVariable(variable))
+        }
+        private dispatch def boolean hasDeclaredVariable(Term term, Variable variable) {
+                return (term.eContainer instanceof Term) && (term.eContainer as Term).hasDeclaredVariable(variable)
+        }
+        private dispatch def boolean hasDeclaredVariable(RelationDefinition relation, Variable variable) {
+                relation.variables.contains(variable)
+        }
+        private dispatch def boolean hasDeclaredVariable(Void term, Variable variable) {
+                return false
+        }
+        
+        def protected void nameAnonymVariables(EObject termSegment, List<String> previousNames) {
+                if(termSegment instanceof QuantifiedExpression) {
+                        val newNames = new LinkedList(previousNames)
+                        for(variable : termSegment.quantifiedVariables) {
+                                var String newName
+                                if(variable.name.nullOrEmpty) {
+                                        newName = newNames.generateUniqueName[i | 
+                                                var x = variable.range.variableAnonymName
+                                                x+="var"+i.toString
+                                                //println(x)
+                                                return x
+                                        ]
+                                        variable.name = newName
+                                }
+                                else newName = variable.name
+                                newNames+= newName
+                        }
+                        termSegment.expression.nameAnonymVariables(newNames)
+                }
+                else {
+                        for(subTerm : termSegment.eContents) {
+                                subTerm.nameAnonymVariables(previousNames)
+                        }
+                }
+        }
+        def protected dispatch String variableAnonymName(BoolTypeReference ref) { "bool" }
+        def protected dispatch String variableAnonymName(IntTypeReference ref)  { "int" }
+        def protected dispatch String variableAnonymName(RealTypeReference ref) { "real" }
+        def protected dispatch String variableAnonymName(ComplexTypeReference ref) { ref.referred.name.toLowerCase }
+         
+        def protected allSubterms(Term term) {
+                val content = term.eAllContents
+                val result =  new ArrayList<EObject>(content.size+1)
+                result+=term
+                result+=content.toIterable
+                return result;
+        }
+        
+        def public Term toTerm(TermDescription term) {
+                if(term instanceof Term) return term
+                else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term]
+                else if (term instanceof Constant) return term.call()
+                else if (term instanceof DefinedElement) return createSymbolicValue => [symbolicReference = term]
+                else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name)
+        }
+        
+        def public !(TermDescription term) { Not(term) }
+        def public Not(TermDescription term) { createNot => [operand = term.toTerm] }
+        
+        def public &&(TermDescription a, TermDescription b) { And(a,b) }
+        def public And(TermDescription... terms) { return And(terms as Iterable<? extends TermDescription>) }   
+        def public And(Iterable<? extends TermDescription> terms) { createAnd => [operands += terms.map[toTerm]] }
+        
+        def public ||(TermDescription a, TermDescription b) { Or(a,b) } 
+        def public Or(TermDescription... terms) { Or(terms as Iterable<? extends TermDescription>) }    
+        def public Or(Iterable<? extends TermDescription> terms) { createOr => [operands += terms.map[toTerm]] }
+        
+        def public =>(TermDescription a, TermDescription b) { Impl(a,b) }
+        def public Impl(TermDescription a, TermDescription b) { createImpl => [leftOperand = a.toTerm rightOperand = b.toTerm] }
+        
+        def public <=>(TermDescription a, TermDescription b) { Iff(a,b)}
+        def public Iff(TermDescription a, TermDescription b) { createIff =>[leftOperand=a.toTerm rightOperand=b.toTerm] }
+        
+        def public ITE(TermDescription condition, TermDescription ifTrue, TermDescription ifFalse) {
+                createIfThenElse => [it.condition = condition.toTerm it.ifTrue = ifTrue.toTerm it.ifFalse = ifFalse.toTerm]
+        }
+        
+        def public >(TermDescription left, TermDescription right) { MoreThan(left,right)}
+        def public MoreThan(TermDescription left, TermDescription right) { createMoreThan => [leftOperand=left.toTerm rightOperand=right.toTerm] }
+        
+        def public <(TermDescription left, TermDescription right) { LessThan(left,right)}
+        def public LessThan(TermDescription left, TermDescription right) { createLessThan => [leftOperand=left.toTerm rightOperand=right.toTerm] }
+        
+        def public <=(TermDescription left, TermDescription right) { LessOrEqual(left,right) }
+        def public LessOrEqual(TermDescription left, TermDescription right) { createLessOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] }
+        
+        def public >=(TermDescription left, TermDescription right) { MoreOrEqual(left,right) }
+        def public MoreOrEqual(TermDescription left, TermDescription right) { createMoreOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] }
+        
+        def public ==(TermDescription left, TermDescription right) {Equals(left,right)}
+        def public Equals(TermDescription left, TermDescription right) { createEquals => [leftOperand=left.toTerm rightOperand=right.toTerm] }
+        
+        def public !=(TermDescription left, TermDescription right) { Distinct(left,right) }
+        def public Distinct(TermDescription... terms) { return Distinct(terms as Iterable<? extends TermDescription>) }
+        def public Distinct(Iterable<? extends TermDescription> terms) { createDistinct => [operands += terms.map[toTerm]] }
+        
+        def public +(TermDescription left, TermDescription right) { Plus(left,right) }
+        def public Plus(TermDescription left, TermDescription right) { createPlus => [leftOperand=left.toTerm rightOperand=right.toTerm] }
+        
+        def public -(TermDescription left, TermDescription right) { Minus(left,right) }
+        def public Minus(TermDescription left, TermDescription right) { createMinus => [leftOperand=left.toTerm rightOperand=right.toTerm] }
+        
+        def public *(TermDescription left, TermDescription right) { Multiply(left,right) }
+        def public Multiply(TermDescription left, TermDescription right) { createMultiply => [leftOperand=left.toTerm rightOperand=right.toTerm] }
+        
+        def public /(TermDescription left, TermDescription right) { Divide(left,right) }
+        def public Divide(TermDescription left, TermDescription right) { createDivison => [leftOperand = left.toTerm rightOperand = right.toTerm]}
+        
+        def public %(TermDescription left, TermDescription right) { Modulo(left,right) }
+        def public Modulo(TermDescription left, TermDescription right) { createMod => [leftOperand = left.toTerm rightOperand = right.toTerm]}
+        
+        def public asTerm(boolean value) { createBoolLiteral => [x|x.value = value]  }
+        def public asTerm(int value) { createIntLiteral => [x|x.value = value] }
+        def public asTerm(double value) { createRealLiteral => [x|x.value = BigDecimal.valueOf(value)] }
+        
+        def public InstanceOf(TermDescription term, TypeDescriptor type) {
+                createInstanceOf => [
+                        it.value = term.toTerm
+                        it.range = type.toTypeReference
+                ]
+        }
+        
+        // QuantifiedExpressions
+        
+        def public Forall(Function1<VariableContext, ? extends TermDescription> expression) {
+                val context = new VariableContext(this,logicFactiory)
+                val term = expression.apply(context)
+                return createForall => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm]
+        }
+        def public Forall(TermDescription expression, Variable... variables) {
+                Forall(variables,expression) }  
+        def public Forall(Iterable<? extends Variable> variables,TermDescription expression) {
+                val forallExpression = createForall
+                for(variable : variables) forallExpression.quantifiedVariables += variable
+                forallExpression.expression = expression.toTerm
+                return forallExpression
+        }
+        
+        def public Exists(Function1<VariableContext, ? extends TermDescription> expression) {
+                val context = new VariableContext(this,logicFactiory)
+                val term = expression.apply(context)
+                return createExists => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm]
+        }
+        def public Exists(TermDescription expression, Variable... variables) {
+                Exists(variables,expression) }
+        def public Exists(Iterable<? extends Variable> variables, TermDescription expression) {
+                val existsExpression = createExists
+                for(variable : variables) existsExpression.quantifiedVariables += variable
+                existsExpression.expression = expression.toTerm
+                return existsExpression
+        }
+        
+        // Function calls
+        def public call(Function function, TermDescription... substitutions) {
+                call(function, substitutions as Iterable<? extends TermDescription>) }
+        def public call(Function function, Iterable<? extends TermDescription> substitutions) {
+                val functionReference = createSymbolicValue
+                functionReference.symbolicReference=function
+                val List<TermDescription> l= new LinkedList()
+                l.addAll(substitutions)
+                for(substitution : l)
+                        functionReference.parameterSubstitutions += substitution.toTerm
+                functionReference.checkFunctionCall(function)
+                return functionReference
+        }
+        def private checkFunctionCall(SymbolicValue value, Function referredFunction) {
+                if(value.parameterSubstitutions.size != referredFunction.parameters.size)
+                        throw new LogicProblemBuilderException(
+                        '''The function called has «referredFunction.parameters.size» parameters but it is called with «value.parameterSubstitutions.size»!''')
+        }
+        
+        //  Relation calls
+        def public call(Relation relation, TermDescription... substitution) { relation.call(substitution as Iterable<? extends TermDescription>)}
+        def public call(Relation relation, Iterable<? extends TermDescription> substitution) {
+                val relationReference = createSymbolicValue
+                relationReference.symbolicReference = relation
+                //println('''«relation.name»(«substitution.size»->«relation.parameters»)''')
+                for(value : substitution)
+                        relationReference.parameterSubstitutions += value.toTerm
+                relationReference.checkRelationCall(relation)
+                return relationReference
+        }
+        def private checkRelationCall(SymbolicValue value, Relation referredRelation) {
+                if(value.parameterSubstitutions.size != referredRelation.parameters.size) {
+                        throw new LogicProblemBuilderException(
+                                '''The relation "«referredRelation.name»" called has «referredRelation.parameters.size» parameters but it is called with «value.parameterSubstitutions.size»!''')
+                }
+        }
+        
+        // constant evaluation
+        def public call(Constant constant) {
+                val constantReference = createSymbolicValue
+                constantReference.symbolicReference = constant
+                return constantReference
+        }
+        
+        
+}
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
new file mode 100644
index 00000000..2e3d57cf
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend
@@ -0,0 +1,47 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+abstract class LogicReasoner {
+        def abstract LogicResult solve(
+                LogicProblem problem,
+                LogicSolverConfiguration configuration,
+                ReasonerWorkspace workspace) throws LogicReasonerException
+        def abstract LogicModelInterpretation getInterpretation(ModelResult modelResult)
+}
+public class LogicReasonerException extends Exception {
+        new(String message, Exception cause) { super(message,cause) }
+        new(Exception cause) { super("The reasoner has failed",cause)}
+        new(String message) { super(message) }
+}
+abstract class LogicSolverConfiguration {
+        public static val Unlimited = -1;
+        public static val String UndefinedPath = null
+        
+        /** The URI string to the independent solver application */
+        public String solverPath = UndefinedPath
+        /** Max runtime limit in seconds. */
+        public int runtimeLimit = Unlimited
+        /** Max runtime limit in seconds. */
+        public int memoryLimit = Unlimited
+        
+        public var TypeScopes typeScopes = new TypeScopes;
+        public var SolutionScope solutionScope = new SolutionScope
+}
+public class TypeScopes{
+        public static val Unlimited = -1;
+        public var maxIntScope = Unlimited
+        public var minNewElements = 0
+        public var maxNewElements = Unlimited
+}
+public class SolutionScope{
+        public static val Unlimited = -1;
+        public var numberOfRequiredSolution = 1
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend
new file mode 100644
index 00000000..b3e44b46
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend
@@ -0,0 +1,407 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import java.math.BigDecimal
+import java.util.ArrayList
+import java.util.Collection
+import java.util.Collections
+import java.util.HashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import org.eclipse.xtend.lib.annotations.Data
+@Data class InterpretationValidationResult {
+        val List<String> problems;
+        val List<Assertion> invalidAssertions;
+        def isValid() { return problems.empty && invalidAssertions.empty}
+}
+class LogicStructureBuilder{
+        val protected extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        
+        def public dispatch Collection<DefinedElement> getElements(LogicModelInterpretation interpretation, TypeDeclaration type) {
+                return interpretation.getElements(type)
+        }
+        def public dispatch Collection<DefinedElement> getElements(LogicModelInterpretation interpretation, TypeDefinition type) {
+                return type.elements
+        }
+        def public Term evalAsTerm(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap).toTerm }
+        def public boolean evalAsBool(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as Boolean}
+        def public int evalAsInt(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as Integer }
+        def public BigDecimal evalAsReal(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as BigDecimal }
+        /**
+         * Evaluate the expression on a solution to an logic element.
+         * @param interpretation The interpretation which the expression is evaluated on.
+         * @param term An expression which results in a logic element.
+         * @return The logic element value of the expression. Returns the element directly, not a symbolic reference!
+         */
+        def public DefinedElement evalAsElement(LogicModelInterpretation interpretation, TermDescription term) { term.resolve(interpretation,emptyMap) as DefinedElement}
+        /**
+         * Checks if the interpretation is a valid solution of the problem by checking the satisfactions of each assertion.
+         * Returns the collection of failed assertions.
+         * @param interpretation The checked interpretation.
+         * @param problem The interpretation is checked on this problem.
+         * @return The collection of failed assertions.
+         */
+        def public validateInterpretationOnProblem(LogicModelInterpretation interpretation, LogicProblem problem) {
+                val List<String> problems = new LinkedList
+                
+                // Checking types
+                val type2ElementsMap = problem.types.toInvertedMap[interpretation.getElements(it)]
+                
+                // Checking definition does not changed
+                for(type : problem.types.filter(TypeDefinition)) {
+                        val elements = type2ElementsMap.get(type)
+                        if(!type.elements.containsAll(elements))
+                                problems+='''The interpretation of «type.name» does not contains each elements of the problem'''
+                        if(!elements.containsAll(type.elements))
+                                problems+='''The interpretation of «type.name» does not contains additional elements not specified in the problem'''
+                }
+                // Checking the type table
+                val allElements = type2ElementsMap.values.flatten.toSet
+                for (element : allElements) {
+                        if(! checkElement(problem, type2ElementsMap, element)) {
+                                problems += '''«element.name» does not follows the type hierarchy'''
+                        }
+                }
+        
+                // Checking assertions
+                val List<Assertion> invalidAssertions = new LinkedList
+                for(assertion : problem.assertions) {
+                        if(! interpretation.evalAsBool(assertion.value)) {
+                                invalidAssertions+= assertion
+                                problems += '''«assertion.name» is violated!'''
+                        }
+                }
+                return new InterpretationValidationResult(problems,invalidAssertions)
+                //problem.assertions.filter[x | ! interpretation.evalAsBool(x.value)]
+        }
+        
+        private def checkElement(LogicProblem problem, Map<Type, List<DefinedElement>> type2ElementsMap, DefinedElement element) {
+                val compatibleDynamicTypes = new LinkedList
+                for(possibleDynamicType: problem.types.filter[!it.isIsAbstract]) {
+                        //println(possibleDynamicType.name)
+                        val compatibleTypes = possibleDynamicType.transitiveClosureStar[it.supertypes]
+                        //compatibleTypes.forEach[print(''' + «it.name»''')]
+                        val incompatibleTypes = problem.types.filter[!compatibleTypes.contains(it)]
+                        //incompatibleTypes.forEach[print(''' - «it.name»''')]
+                        if(compatibleTypes.forall[ type2ElementsMap.get(it).contains(element)] && incompatibleTypes.forall[!type2ElementsMap.get(it).contains(element)]) {
+                                //println("Ok")
+                                compatibleDynamicTypes += possibleDynamicType
+                        }
+                }
+                return compatibleDynamicTypes.size == 1
+        }
+        
+        def protected dispatch Term toTerm(Integer o)  { createIntLiteral=>[value = o] }
+        def protected dispatch Term toTerm(BigDecimal o) { createRealLiteral=>[value = o]}
+        def protected dispatch Term toTerm(Boolean o) { createBoolLiteral=>[value = o]}
+        def protected dispatch Term toTerm(SymbolicDeclaration o) { createSymbolicValue=>[symbolicReference = o]}
+        def public Term termDescriptiontoTerm(TermDescription term) {
+                if(term instanceof Term) return term
+                else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term]
+                else if (term instanceof Constant) return createSymbolicValue=>[symbolicReference = term]
+                else if (term instanceof DefinedElement) return createSymbolicValue => [symbolicReference = term]
+                else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name)
+        }
+        /**
+         * Returns if the operation with the numbers in the parameter requires the use of <code>BigDecimal</code>.
+         */
+        def private isBigDecimalRequired(Object... numbers) { return numbers.exists[it instanceof BigDecimal || it instanceof RealLiteral] }
+        def private dispatch BigDecimal asBigDecimal(IntLiteral i) { i.value.asBigDecimal }
+        def private dispatch BigDecimal asBigDecimal(RealLiteral i) { i.value.asBigDecimal }
+        def private dispatch BigDecimal asBigDecimal(Integer i) { BigDecimal.valueOf(i) }
+        def private dispatch BigDecimal asBigDecimal(BigDecimal i) { i }
+        def private dispatch Integer asInteger(Integer i) { i }
+        def private dispatch Integer asInteger(BigDecimal i) { i.intValue }
+        def private dispatch Integer asInteger(IntLiteral i) { i.value.asInteger }
+        
+        // Atomic resoulutions
+        def protected dispatch Object resolve(IntLiteral literal,  LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { return literal.value as Integer }
+        def protected dispatch Object resolve(BoolLiteral literal, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { return literal.value }
+        def protected dispatch Object resolve(RealLiteral literal, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { return literal.value as BigDecimal }
+        
+        def protected dispatch Object resolve(Not not, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                return ! (not.operand.resolve(interpretation,variableBinding) as Boolean) }
+        def protected dispatch Object resolve(And and, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                //for(operand : and.operands) {
+                        //val r = operand.resolve(interpretation,variableBinding) as Boolean
+                        //println(r)
+                //}
+                return and.operands.forall[resolve(interpretation,variableBinding) as Boolean] as Boolean }
+        def protected dispatch Object resolve(Or or, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                //val resolved = or.operands.map[resolve(interpretation,variableBinding) as Boolean]
+                //println(resolved)
+                return or.operands.exists[resolve(interpretation,variableBinding) as Boolean] }
+        def protected dispatch Object resolve(Impl impl, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left = impl.leftOperand. resolve(interpretation,variableBinding) as Boolean
+                val right = impl.rightOperand.resolve(interpretation,variableBinding) as Boolean
+                return (! left) || (right) }
+        def protected dispatch Object resolve(Iff iff, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                return (iff.leftOperand.resolve(interpretation,variableBinding) as Boolean) ==
+                       (iff.rightOperand.resolve(interpretation,variableBinding) as Boolean) }
+        def protected dispatch Object resolve(IfThenElse ite, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val condition = ite.condition.resolve(interpretation,variableBinding) as Boolean
+                if(condition) return ite.ifTrue.resolve(interpretation,variableBinding)
+                else return ite.ifFalse.resolve(interpretation,variableBinding)
+        }
+        def protected dispatch Object resolve(MoreThan moreThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left = moreThan.leftOperand.resolve(interpretation,variableBinding) as Number
+                val right = moreThan.rightOperand.resolve(interpretation,variableBinding) as Number
+                if(isBigDecimalRequired(left,right)) {
+                        return left.asBigDecimal.compareTo(right.asBigDecimal) > 0 }
+                else { return left.asInteger > right.asInteger } }
+        def protected dispatch Object resolve(LessThan lessThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left = lessThan.leftOperand.resolve(interpretation,variableBinding) as Number
+                val right = lessThan.rightOperand.resolve(interpretation,variableBinding) as Number
+                if(isBigDecimalRequired(left,right)) {
+                        return left.asBigDecimal.compareTo(right.asBigDecimal) < 0 }
+                else { return left.asInteger < right.asInteger } }
+        def protected dispatch Object resolve(MoreOrEqualThan moreThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left = moreThan.leftOperand.resolve(interpretation,variableBinding) as Number
+                val right = moreThan.rightOperand.resolve(interpretation,variableBinding) as Number
+                if(isBigDecimalRequired(left,right)) {
+                        return left.asBigDecimal.compareTo(right.asBigDecimal) >= 0 }
+                else { return left.asInteger >= right.asInteger } }
+        def protected dispatch Object resolve(LessOrEqualThan lessThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left = lessThan.leftOperand.resolve(interpretation,variableBinding) as Number
+                val right = lessThan.rightOperand.resolve(interpretation,variableBinding) as Number
+                if(isBigDecimalRequired(left,right)) return left.asBigDecimal.compareTo(right.asBigDecimal) <= 0 
+                else { return left.asInteger <= right.asInteger } }
+        
+        def protected dispatch Object resolve(Equals equals, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left = equals.leftOperand.resolve(interpretation,variableBinding)
+                val right = equals.rightOperand.resolve(interpretation,variableBinding)
+                return compare(left,right)
+        }
+        def protected dispatch Object resolve(Distinct distinct, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val elements = distinct.operands.map[it.resolve(interpretation,variableBinding)]
+                if(elements.size== 0) return true
+                else {
+                        val res = (0..<elements.size).forall[i |
+                                (0..<i).forall[j|
+                                        ! this.compare(elements.get(i),elements.get(j))]]
+                        //println('''«elements» = «res»''')
+                        return res
+                }
+                                
+                //return elements.forall[x| elements.filter[it!=x].forall[y | x != y ]]
+        }
+        
+        def protected dispatch Object resolve(Plus plus, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left  = plus.leftOperand.resolve(interpretation,variableBinding) as Number
+                val right = plus.rightOperand.resolve(interpretation,variableBinding) as Number
+                if(isBigDecimalRequired(left,right)) return left.asBigDecimal.add(right.asBigDecimal)
+                else return left.asInteger + right.asInteger
+        }
+        def protected dispatch Object resolve(Minus minus, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left  = minus.leftOperand.resolve(interpretation,variableBinding) as Number
+                val right = minus.rightOperand.resolve(interpretation,variableBinding) as Number
+                if(isBigDecimalRequired(left,right)) return left.asBigDecimal.subtract(right.asBigDecimal)
+                else return left.asInteger - right.asInteger
+        }
+        def protected dispatch Object resolve(Multiply multiply, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left  = multiply.leftOperand.resolve(interpretation,variableBinding)
+                val right = multiply.rightOperand.resolve(interpretation,variableBinding)
+                if(isBigDecimalRequired(left,right)) return left.asBigDecimal.multiply(right.asBigDecimal)
+                else return left.asInteger * right.asInteger
+        }
+        def protected dispatch Object resolve(Divison divide, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left  = divide.leftOperand.resolve(interpretation,variableBinding) as Number
+                val right = divide.rightOperand.resolve(interpretation,variableBinding) as Number
+                if(isBigDecimalRequired(left,right)) return left.asBigDecimal.divide(right.asBigDecimal)
+                return left.asInteger / right.asInteger
+        }
+        def protected dispatch Object resolve(Mod modulo, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val left  = modulo.leftOperand.resolve(interpretation,variableBinding) as Number
+                val right = modulo.rightOperand.resolve(interpretation,variableBinding) as Number
+                if(isBigDecimalRequired(left,right)) return left.asBigDecimal.remainder(right.asBigDecimal)
+                else return left.asInteger % right.asInteger
+        }
+        
+        def protected dispatch Object resolve(Exists exists, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                executeExists(exists.expression,interpretation,variableBinding,exists.quantifiedVariables) }
+        def protected dispatch Object resolve(Forall forall, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                executeForall(forall.expression,interpretation,variableBinding,forall.quantifiedVariables) }
+        
+        def protected dispatch Object resolve(SymbolicValue symbolicValue, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                val referenced = symbolicValue.symbolicReference
+                if(referenced instanceof DefinedElement) {
+                        return referenced
+                } else if(referenced instanceof Variable)  {
+                        return variableBinding.get(referenced)
+                } else if(referenced instanceof FunctionDeclaration) {
+                        val parameterSubstitution = new ArrayList<Object>
+                        if(! symbolicValue.parameterSubstitutions.empty) {
+                                for(place : 0..symbolicValue.parameterSubstitutions.size-1) {
+                                        val variable = symbolicValue.parameterSubstitutions.get(place)
+                                        parameterSubstitution += variable.resolve(interpretation,variableBinding)
+                                }
+                        }
+                        return interpretation.getInterpretation(referenced,parameterSubstitution)
+                } else if(referenced instanceof FunctionDefinition) {
+                        val parameterSubstitution = new HashMap<Variable,Object>()
+                        for(place: 0..<referenced.variable.size) {
+                                parameterSubstitution.put(
+                                        referenced.variable.get(place),
+                                        symbolicValue.parameterSubstitutions.get(place).resolve(interpretation,variableBinding))
+                        }
+                        return referenced.value.resolve(interpretation,parameterSubstitution)
+                } else if(referenced instanceof RelationDeclaration) {
+                        val parameterSubstitunion = new ArrayList<Object>
+                        if(! symbolicValue.parameterSubstitutions.empty) {
+                                for(place : 0..symbolicValue.parameterSubstitutions.size-1) {
+                                        val variable = symbolicValue.parameterSubstitutions.get(place)
+                                        parameterSubstitunion += variable.resolve(interpretation,variableBinding)
+                                }
+                        }
+                        return (interpretation.getInterpretation(referenced,parameterSubstitunion) as Boolean)
+                } else if(referenced instanceof RelationDefinition) {
+                        val parameterSubstitution = new HashMap<Variable,Object>()
+                        for(place: 0..<referenced.variables.size) {
+                                parameterSubstitution.put(
+                                        referenced.variables.get(place),
+                                        symbolicValue.parameterSubstitutions.get(place).resolve(interpretation,variableBinding))
+                        }
+                        return referenced.value.resolve(interpretation,parameterSubstitution)
+                } else if(referenced instanceof ConstantDeclaration) {
+                        return interpretation.getInterpretation(referenced)
+                } else if(referenced instanceof ConstantDefinition) {
+                        return referenced.value.resolve(interpretation,Collections.emptyMap);
+                } else throw new IllegalArgumentException('''Unknown referred symbol: «referenced»''')
+        }
+        
+        // TermDescriptions are reduced to terms
+        def protected dispatch resolve(Variable variable, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                return variableBinding.get(variable)
+        }
+        def protected dispatch resolve(DefinedElement definedElement, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) {
+                return definedElement
+        }
+        
+        def private compare(Object left, Object right) {
+                if(left instanceof Number && right instanceof Number) {
+                        if(isBigDecimalRequired(left as Number,right as Number)) {
+                                return (left as Number).asBigDecimal.compareTo((right as Number).asBigDecimal) == 0
+                        } else {
+                                return (left as Number).asInteger == (right as Number).asInteger
+                        }
+                } else return left.equals(right)
+        }       
+        def allIntegers(LogicModelInterpretation interpretation) {
+                if(interpretation.minimalInteger <= interpretation.maximalInteger) {
+                        (interpretation.minimalInteger .. interpretation.maximalInteger).map[asInteger]
+                } else return emptySet
+        }
+        
+        def private boolean executeExists(
+                Term expression,
+                LogicModelInterpretation interpretation,
+                Map<Variable,Object> variableBinding,
+                List<Variable> variablesToBind)
+        {
+                if(variablesToBind.empty) {
+                        val res = expression.resolve(interpretation,variableBinding) as Boolean
+                        return res
+                }
+                else {
+                        val unfoldedVariable = variablesToBind.head
+                        val possibleValuesType = unfoldedVariable.range
+                        if(possibleValuesType instanceof ComplexTypeReference) {
+                                return this.getElements(interpretation,possibleValuesType.referred).exists[newBinding |
+                                        executeExists(
+                                        expression,
+                                        interpretation,
+                                        new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)],
+                                        variablesToBind.subList(1,variablesToBind.size))]
+                        } else if(possibleValuesType instanceof IntTypeReference) {
+                                return interpretation.allIntegers.exists[newBinding |
+                                        executeExists(
+                                        expression,
+                                        interpretation,
+                                        new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)],
+                                        variablesToBind.subList(1,variablesToBind.size))]
+                        }
+                        else throw new UnsupportedOperationException('''Quantifying over type "«possibleValuesType»" is unsupported.''')
+                }
+        }
+        
+        def private boolean executeForall(
+                Term expression,
+                LogicModelInterpretation interpretation,
+                Map<Variable,Object> variableBinding,
+                List<Variable> variablesToBind)
+        {
+                if(variablesToBind.empty) {
+                        return expression.resolve(interpretation,variableBinding) as Boolean
+                }
+                else {
+                        val unfoldedVariable = variablesToBind.head
+                        val possibleValuesType = unfoldedVariable.range
+                        if(possibleValuesType instanceof ComplexTypeReference) {
+                                return this.getElements(interpretation,possibleValuesType.referred).forall[newBinding |
+                                        executeForall(
+                                        expression,
+                                        interpretation,
+                                        new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)],
+                                        variablesToBind.subList(1,variablesToBind.size))]
+                        } else if(possibleValuesType instanceof IntTypeReference) {
+                                return interpretation.allIntegers.forall[newBinding |
+                                        executeForall(
+                                        expression,
+                                        interpretation,
+                                        new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)],
+                                        variablesToBind.subList(1,variablesToBind.size))]
+                        } else throw new UnsupportedOperationException('''Quantifying over type "«possibleValuesType»" is unsupported.''')
+                }
+        }
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedLogicProblem.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedLogicProblem.xtend
new file mode 100644
index 00000000..9862a6c1
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedLogicProblem.xtend
@@ -0,0 +1,26 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+class TracedLogicProblem {
+        val LogicProblemBuilder builder = new LogicProblemBuilder
+        val LogicProblem problem = builder.createProblem
+        
+        def public getProblem() { return problem }
+        
+        def public add(TypeDeclaration type) { builder.add(problem,type) }
+        def public add(TypeDefinition type) { builder.add(problem,type) }
+        def public add(Function function) { builder.add(problem,function) }
+        def public add(FunctionDescription functionDescription) { builder.add(problem,functionDescription) }
+        def public add(Relation relation) { builder.add(problem, relation) }
+        def public add(Constant constant) { builder.add(problem, constant) }
+        def public add(Assertion assertion) { builder.add(problem,assertion) }
+        def public add(TermDescription termDescription) { builder.add(problem,termDescription) }
+}
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedOutput.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedOutput.xtend
new file mode 100644
index 00000000..6ffc3524
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedOutput.xtend
@@ -0,0 +1,6 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder
+@Data class TracedOutput<OUTPUT,TRACE> {
+        OUTPUT output
+        TRACE trace
+}
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/VariableContext.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/VariableContext.xtend
new file mode 100644
index 00000000..3073d88f
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/VariableContext.xtend
@@ -0,0 +1,33 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import java.util.List
+import java.util.LinkedList
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor
+class VariableContext {
+        val extension LogiclanguageFactory language;
+        val extension LogicProblemBuilder logicProblemBuilder;
+        
+        new(LogicProblemBuilder logicProblemBuilder, LogiclanguageFactory language) {
+                this.logicProblemBuilder = logicProblemBuilder
+                this.language = language
+        }
+        
+        private List<Variable> variables = new LinkedList;
+        def public getVariables(){variables}
+        
+        
+        //def public -(TypeDescriptor type) { Variable(type) }
+        def public Variable addVar(TypeDescriptor type) {       
+                return addVar(null, type);
+        }
+        
+        def public Variable addVar(CharSequence variableName, TypeDescriptor type) {
+                if(variables.exists[name.equals(variableName)]) throw new IllegalArgumentException("Variable with name " + variableName +" is already defined.")
+                val variable = createVariable => [name = variableName.canonize range = type.toTypeReference]
+                variables += variable
+                return variable
+        }
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/consistencychecker/TypeConsistencyChecker.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/consistencychecker/TypeConsistencyChecker.xtend
new file mode 100644
index 00000000..abb05e83
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/consistencychecker/TypeConsistencyChecker.xtend
@@ -0,0 +1,75 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.builder.consistencychecker
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
+import org.eclipse.viatra.query.runtime.emf.EMFScope
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.patterns.TypeSystemIsInconsistentMatcher
+import hu.bme.mit.inf.dslreasoner.logic.model.patterns.ElementNotDefinedInSupertypeMatcher
+import hu.bme.mit.inf.dslreasoner.logic.model.patterns.ElementWithNoPossibleDynamicTypeMatcher
+import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher
+class TypeConsistencyChecker extends LogicReasoner{
+        val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE
+                
+        new() {
+                LogicproblemPackage.eINSTANCE.class
+        }
+        
+        override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
+                val statistics = createStatistics => [
+                        it.transformationTime = 0
+                        it.solverMemory = -1
+                ]
+                
+                val start = System.currentTimeMillis
+                
+                val queryEngine = ViatraQueryEngine.on(new EMFScope(problem))
+                
+                val typeSystemInconsistencyMatcher = TypeSystemIsInconsistentMatcher.on(queryEngine)
+                val elementNotDefinedInSupertype = ElementNotDefinedInSupertypeMatcher.on(queryEngine)
+                val elementWithNoPossibleDynamicType = ElementWithNoPossibleDynamicTypeMatcher.on(queryEngine)
+                val possibleDynamicType = PossibleDynamicTypeMatcher.on(queryEngine)
+                
+                val hasErrorPatternMatch = typeSystemInconsistencyMatcher.hasMatch(problem)
+                
+                statistics.solverTime = (System.currentTimeMillis - start) as int
+                
+                val possibleDynamicTypeStatisticEntry = problem.elements.map[e|
+                        '''«e.name»: [«possibleDynamicType.getAllValuesOfdynamic(problem,e).map[it.name].join(", ")»]'''
+                ].join("\n")
+                
+                if(hasErrorPatternMatch) {
+                        return createInconsistencyResult =>[
+                                it.problem = problem 
+                                it.statistics = statistics 
+                                it.statistics.entries += createStringStatisticEntry => [
+                                        it.name = "possibleDynamicType"
+                                        it.value = possibleDynamicTypeStatisticEntry
+                                ]
+                                it.statistics.entries += createStringStatisticEntry => [
+                                                it.name = "elementNotDefinedInSupertype"
+                                                it.value=elementNotDefinedInSupertype.allValuesOfelement.map[it.name].join(", ")
+                                        ]
+                                
+                                it.statistics.entries += createStringStatisticEntry => [
+                                        it.name = "elementWithNoPossibleDynamicType"
+                                        it.value=elementWithNoPossibleDynamicType.allValuesOfelement.map[it.name].join(", ")
+                                ]
+                        ]
+                } else {
+                        return createUndecidableResult => 
+                                [it.problem = problem it.statistics = statistics]
+                }
+        }
+        
+        override getInterpretation(ModelResult modelResult) {
+                throw new UnsupportedOperationException('''This solver is unable to create interpretations!''')
+        }
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend
new file mode 100644
index 00000000..442de6d9
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend
@@ -0,0 +1,89 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.statistics
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.IntStatisticEntry
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+class StatisticsData {
+        public var List<Pair<String,String>> inputConfiguration
+        public var List<Pair<String,String>> outputMetrics
+        public var Statistics solverStatistics
+}
+class StatisticSections2CSV {
+        static val separator = ';'
+        static val empty = ""
+        
+        private def getValue(Map<String, String> map,String key) {
+                if(map.containsKey(key)) return map.get(key)
+                else return empty
+        }
+        private def addKey(List<String> list, String newValue) {
+                if(! list.contains(newValue)) list+=newValue
+        }
+        
+        public def CharSequence transformStatisticDatas2CSV(
+                List<StatisticsData> statistics)
+        {
+                val inputConfigurationColumns = new LinkedList
+                val inputConfigurationValues = new ArrayList(statistics.length)
+                val solverStatisticColumns = new LinkedList
+                val solverStatisticValues = new ArrayList(statistics.length)
+                val outputMetricColumns = new LinkedList
+                val outputMetricValues = new ArrayList(statistics.length)
+                
+                statistics.map[inputConfiguration].indexColumnsForPairs(inputConfigurationColumns, inputConfigurationValues)
+                statistics.map[it.solverStatistics].indexColumnsForEntries(solverStatisticColumns, solverStatisticValues)
+                statistics.map[outputMetrics].indexColumnsForPairs(outputMetricColumns,outputMetricValues)
+                                
+                return '''
+                ID« // Header
+                IF inputConfigurationColumns.length>0»«separator»«FOR name : inputConfigurationColumns SEPARATOR separator»«name»«ENDFOR»«ENDIF»«
+                separator»Transformation_Time«separator»Solver_Time«separator»Solver_Memory«
+                IF solverStatisticColumns.length>0»«separator»«ENDIF»«
+                FOR name:solverStatisticColumns SEPARATOR separator»«name»«ENDFOR»«
+                IF outputMetricColumns.length>0»«separator»«ENDIF»«
+                FOR name:outputMetricColumns SEPARATOR separator»«name»«ENDFOR»
+                « // Table
+                FOR index : 0..<statistics.size»
+                «index+1 /*ID*/»«
+                        IF inputConfigurationColumns.size>0»«separator»«ENDIF»«
+                        FOR name : inputConfigurationColumns SEPARATOR separator»«inputConfigurationValues.get(index).getValue(name)»«ENDFOR»«
+                                separator»«statistics.get(index).solverStatistics.transformationTime»«
+                                separator»«statistics.get(index).solverStatistics.solverTime»«
+                                separator»«statistics.get(index).solverStatistics.solverMemory»«
+                        IF solverStatisticColumns.size>0»«separator»«ENDIF»«
+                        FOR name:solverStatisticColumns SEPARATOR separator»«solverStatisticValues.get(index).getValue(name)»«ENDFOR»«
+                        IF outputMetricColumns.size>0»«separator»«ENDIF»«
+                        FOR name:outputMetricColumns SEPARATOR separator»«outputMetricValues.get(index).getValue(name)»«ENDFOR»
+                «ENDFOR»'''
+        }
+        
+        def private indexColumnsForPairs(List<List<Pair<String, String>>> datas, List<String> columns, List<Map<String, String>> values) {
+                for(inputConfiguration : datas) {
+                        val map = new HashMap
+                        for(entry : inputConfiguration) {
+                                columns.addKey(entry.key)
+                                map.put(entry.key,entry.value)  
+                        }
+                        values+=map
+                }
+        }
+        def private indexColumnsForEntries(List<Statistics> datas, List<String> columns, List<Map<String, String>> values) {
+                for(inputConfiguration : datas) {
+                        val map = new HashMap
+                        for(entry : inputConfiguration.entries) {
+                                columns.addKey(entry.name)
+                                map.put(entry.name,entry.readValue)     
+                        }
+                        values+=map
+                }
+        }
+        private def dispatch String readValue(IntStatisticEntry e) { return e.value.toString }
+        private def dispatch String readValue(RealStatisticEntry e){ return e.value.toString }
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend
new file mode 100644
index 00000000..08efa811
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend
@@ -0,0 +1,23 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.statistics
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.IntStatisticEntry
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry
+import java.util.List
+class StatisticSections2Print {
+        public def CharSequence transformStatisticDatas2CSV(
+                List<StatisticEntry> statistics)
+        {
+                var result = "";
+                for(statistic : statistics) {
+                        result+= '''«statistic.readValue»;'''
+                }
+                return result
+        }
+        
+        private def dispatch String readValue(IntStatisticEntry e) { return e.value.toString }
+        private def dispatch String readValue(RealStatisticEntry e){ return e.value.toString }
+        private def dispatch String readValue(StringStatisticEntry e) { return "\n" + e.value }
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/CollectionsUtil.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/CollectionsUtil.xtend
new file mode 100644
index 00000000..25cddc05
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/CollectionsUtil.xtend
@@ -0,0 +1,82 @@
+package hu.bme.mit.inf.dslreasoner.util
+import java.util.HashSet
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import java.util.Set
+import org.eclipse.xtext.xbase.lib.Functions.Function1
+import java.util.HashMap
+import java.util.LinkedHashMap
+class CollectionsUtil {
+        public def static <FROM,TO> TO lookup(FROM from, Map<? super FROM,TO> map) {
+                if(map.containsKey(from)) {
+                        return map.get(from)
+                } else throw new IllegalArgumentException('''
+                The map does not contains the key "«from.toString»"!
+                --- Elements: ---
+                «FOR entry : map.entrySet SEPARATOR '\n'»«entry.key» -> «entry.value»«ENDFOR»
+                -----------------''');
+        }
+        public def <FROM,TO> TO ifThenElse(FROM source, Function1<FROM,Boolean> condition, Function1<FROM,TO> ifTrue, Function1<FROM,TO> ifFalse) {
+                if(condition.apply(source)) {
+                        return ifTrue.apply(source)
+                        }
+                else {
+                        return ifFalse.apply(source)
+                }
+        }
+        public def static <Key,Value> Union(Map<Key,Value> a, Map<Key,Value> b) {
+                (a.keySet + b.keySet).toInvertedMap[key |
+                        if(a.containsKey(key)) a.get(key)
+                        else b.get(key)
+                ]
+        }
+        public def static <Key,Value> putOrAddToSet(Map<Key,Set<Value>> map, Key key, Value value) {
+                if(map.containsKey(key)) {
+                        map.get(key).add(value)
+                }else{
+                        val set = new HashSet<Value>() => [it.add(value)]
+                        map.put(key, set)
+                }
+        }
+        public def static <Key,Value> putOrAddToList(Map<Key,List<Value>> map, Key key, Value value) {
+                if(map.containsKey(key)) {
+                        map.get(key).add(value)
+                }else{
+                        val set = new LinkedList<Value>() => [it.add(value)]
+                        map.put(key, set)
+                }
+        }
+        def public static <From,To,Property> Map<From,To> copyMap(Map<From,To> oldMap, Iterable<To> newValues, Function1<To,Property> indexExtractor) {
+                val Map<Property,To> valueIndexes = oldMap.values.toMap[to|indexExtractor.apply(to)];
+                val res = oldMap.mapValues[value | indexExtractor.apply(value).lookup(valueIndexes)]
+                return res
+        }
+        def public static <From,To> Map<To,From> bijectiveInverse(Map<From,To> m) { m.keySet.toMap[x|x.lookup(m)] }
+        def public static <From,To> Map<To,List<From>> inverse(Map<From,To> m) {
+                val res = new LinkedHashMap<To,List<From>>
+                m.entrySet.forEach[res.putOrAddToList(it.value,it.key)]
+                return res
+        }
+        
+        def public static <Type> List<Type> transitiveClosurePlus(Type source, Function1<Type,Iterable<Type>> next) {
+                val res = new LinkedList()
+                transitiveClosureHelper(res,source,next)
+                return res
+        }
+        def public static <Type> List<Type> transitiveClosureStar(Type source, Function1<Type,Iterable<Type>> next) {
+                val res = new LinkedList()
+                res += source
+                transitiveClosureHelper(res,source,next)
+                return res
+        }
+        def private static <Type> void transitiveClosureHelper(List<Type> result, Type actual, Function1<Type,Iterable<Type>> next) {
+                val front = next.apply(actual)
+                for(elementInFront : front) {
+                        result += elementInFront
+                        transitiveClosureHelper(result,elementInFront,next)
+                }
+        }
+}
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/LogicProblemBuilder_AdvancedConstructs.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/LogicProblemBuilder_AdvancedConstructs.xtend
new file mode 100644
index 00000000..3db0e2a6
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/LogicProblemBuilder_AdvancedConstructs.xtend
@@ -0,0 +1,71 @@
+package hu.bme.mit.inf.dslreasoner.util
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import java.util.ArrayList
+import java.util.Collection
+import java.util.List
+import java.util.Map
+class LogicProblemBuilder_AdvancedConstructs {
+        val extension LogicProblemBuilder builder;
+        public new(LogicProblemBuilder builder) {
+                this.builder = builder
+        }
+        
+        def public FunctionDefinitionBody(Iterable<Variable> variables, Map<List<Term>,Term> parametersToValue, Term other) {
+                val variableList = variables.toList
+                val entryList = parametersToValue.entrySet.toList
+                
+                // Size = 0
+                if(entryList.empty && other === null) {
+                        throw new IllegalArgumentException('''No possible value is specified!''')
+                // Size = 1
+                } else if(entryList.size == 1 && other === null) {
+                        return entryList.head.value
+                // Size = 1
+                } else if(entryList.empty && !(other === null)) {
+                        return other
+                // Size > 1
+                }else {
+                        // Transforming values to IF-Then-Else structures
+                        /**The number of IF-THEN-ELSE structures needed*/
+                        var int iteNumber
+                        if(other === null) iteNumber = entryList.size-1
+                        else iteNumber = entryList.size
+                        
+                        val ites = new ArrayList<IfThenElse>(iteNumber)
+                        for (element : 0 ..< iteNumber) {
+                                ites += ITE(
+                                        entryList.get(element).key.substitutionIsEqual(variableList),
+                                        entryList.get(element).value,
+                                        null)
+                        }
+                        
+                        // Linking the IF-Then-Else structures to a chain
+                        for (optionIndex : 1 ..< ites.size) {
+                                val prev = ites.get(optionIndex - 1)
+                                val next = ites.get(optionIndex)
+                                prev.ifFalse = next
+                        }
+                        
+                        if(other === null) ites.last.ifFalse = entryList.last.value
+                        else ites.last.ifFalse = other
+                        
+                        // return the head of the chain
+                        return ites.head
+                }
+        }
+        
+        def public RelationDefinitionBody(Iterable<Variable> variables, Collection<List<Term>> elements) {
+                val variableList = variables.toList
+                return elements.map[row | row.substitutionIsEqual(variableList)].Or
+        }
+        
+        def private substitutionIsEqual(List<Term> substitution, List<Variable> variables) {
+                val parameterIndexes = 0..<variables.size
+                return And(parameterIndexes.map[index | substitution.get(index) == variables.get(index)])
+        }
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/SetWithCustomEquivalence.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/SetWithCustomEquivalence.xtend
new file mode 100644
index 00000000..ae2cfb04
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/SetWithCustomEquivalence.xtend
@@ -0,0 +1,103 @@
+package hu.bme.mit.inf.dslreasoner.util
+import org.eclipse.xtext.xbase.lib.Functions.Function1
+import java.util.HashMap
+import java.util.Set
+import java.util.Collection
+import java.util.HashSet
+class SetWithCustomEquivalence<Type,Representation> implements Set<Type>{
+        val Function1<Type,Representation> representer;
+        val HashMap<Representation,Type> map
+        
+        public new(Function1<Type,Representation> representer) {
+                this.representer = representer
+                this.map = new HashMap<Representation,Type>
+        }
+        public new(Function1<Type,Representation> representer, Collection<? extends Type> initialElements) {
+                this.representer = representer
+                this.map = new HashMap
+                initialElements.forEach[add]
+        }
+        
+        override add(Type arg0) {
+                val representation = representer.apply(arg0)
+                if(!map.containsKey(representation)) {
+                        map.put(representation,arg0);
+                        return true
+                } else return false
+        }
+        
+        override addAll(Collection<? extends Type> arg0) {
+                val originalSize = this.size
+                arg0.forEach[add(it)]
+                return (this.size != originalSize)
+        }
+        
+        override clear() {
+                map.clear
+        }
+        
+        override contains(Object arg0) {
+                try {
+                        val rep = this.representer.apply(arg0 as Type)
+                        return map.containsKey(rep)
+                } catch (ClassCastException e) {
+                        return false
+                }
+        }
+        
+        override containsAll(Collection<?> arg0) {
+                arg0.forall[it.contains]
+        }
+        
+        override isEmpty() {
+                return map.isEmpty
+        }
+        
+        override iterator() {
+                return map.values.iterator
+        }
+        
+        override remove(Object arg0) {
+                try {
+                        val rep = this.representer.apply(arg0 as Type)
+                        return map.remove(rep) != null
+                } catch (ClassCastException e) {
+                        return false
+                }
+        }
+        
+        override removeAll(Collection<?> arg0) {
+                val originalSize = this.size
+                arg0.forEach[remove(it)]
+                return (this.size != originalSize)
+        }
+        
+        override retainAll(Collection<?> arg0) {
+                val Set<Representation> representationsOfArg0 = new HashSet
+                for(element: arg0) {
+                        try {
+                                representationsOfArg0 += this.representer.apply(element as Type)
+                        } catch(ClassCastException e) {}
+                }
+                val originalSize = this.size
+                for(r:this.map.keySet) {
+                        if(!representationsOfArg0.contains(r))
+                                this.map.remove(r)
+                }
+                return (this.size != originalSize)
+        }
+        
+        override size() {
+                return this.map.size
+        }
+        
+        override toArray() {
+                map.values.toArray
+        }
+        
+        override <T> toArray(T[] arg0) {
+                map.values.toArray(arg0)
+        }
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/visualisation/Interpretation2Gml.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/visualisation/Interpretation2Gml.xtend
new file mode 100644
index 00000000..472799f9
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/visualisation/Interpretation2Gml.xtend
@@ -0,0 +1,5 @@
+package hu.bme.mit.inf.dslreasoner.util.visualisation
+class Interpretation2Gml {
+        
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/FileSystemWorkspace.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/FileSystemWorkspace.xtend
new file mode 100644
index 00000000..6041fdbf
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/FileSystemWorkspace.xtend
@@ -0,0 +1,74 @@
+package hu.bme.mit.inf.dslreasoner.workspace
+import java.io.BufferedReader
+import java.io.FileReader
+import java.io.PrintWriter
+import org.eclipse.emf.common.util.URI
+import java.io.File
+class FileSystemWorkspace extends ReasonerWorkspace{
+        
+        new(String targetFolder, String prefix) {
+                super(targetFolder/*.replaceAll("\\\\","/").replaceAll("/\\.","")*/, prefix)
+        }
+        
+        override protected getURI(String name) {
+                URI.createFileURI(targetFolder + "/" + prefix + name)
+        }
+        
+        def protected getFolderURI() {
+                URI.createFileURI(targetFolder)
+        }
+        
+        override getWorkspaceURI() {
+                getFolderURI
+        }
+        
+        override initAndClear() {
+                val folder = new File(folderURI.toFileString)
+                folder.mkdirs
+                for(file : folder.listFiles) {
+                        file.deleteFile
+                }
+        }
+        
+        def void deleteFile(File file) {
+                if (file.isDirectory()) {
+                        file.listFiles().forEach[deleteFile]
+                        file.delete
+                } else {
+                        file.delete;
+                }
+        }
+        
+        override writeText(String name, CharSequence content) {
+                val uri = getURI(name)
+                val writer = new PrintWriter(uri.toFileString, "UTF-8");
+                writer.println(content);
+                writer.close();
+                return uri
+        }
+        
+        override readText(String name) {
+                var String line;
+                var String result = "";
+        val in = new BufferedReader(new FileReader(getURI(name).toFileString))
+                while ((line = in.readLine()) != null) {
+                        result = result.concat(line)
+                }
+                in.close
+        return result
+        }
+        
+        override protected renameFile(String name) {
+                val uri = getURI(name)
+                val uri2 = getURI(name+deactivationPostfix)
+                val file = new File(uri. toFileString)
+                val file2 = new File(uri2.toFileString)
+                file.renameTo(file2)
+        }
+        
+        override subWorkspace(String targetFolder, String prefix) {
+                return new FileSystemWorkspace(this.targetFolder + "/" + targetFolder, this.prefix + prefix)
+        }
+}
+\ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ProjectWorkspace.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ProjectWorkspace.xtend
new file mode 100644
index 00000000..5703bd5a
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ProjectWorkspace.xtend
@@ -0,0 +1,105 @@
+package hu.bme.mit.inf.dslreasoner.workspace
+import java.io.BufferedReader
+import java.io.ByteArrayInputStream
+import java.io.IOException
+import java.io.InputStreamReader
+import org.eclipse.core.resources.IContainer
+import org.eclipse.core.resources.IFolder
+import org.eclipse.core.resources.IProject
+import org.eclipse.core.resources.IWorkspaceRoot
+import org.eclipse.core.resources.ResourcesPlugin
+import org.eclipse.core.runtime.NullProgressMonitor
+import org.eclipse.emf.common.util.URI
+class ProjectWorkspace extends ReasonerWorkspace{
+        
+        val monitor = new NullProgressMonitor
+        var IContainer target;
+        
+        new(String targetFolder, String prefix) {
+                super(targetFolder, prefix)
+        }
+        
+        override protected getURI(String name) {
+                URI.createPlatformResourceURI(targetFolder + "/" + prefix + name,true);
+        }
+        
+        def protected getDirUri() {
+                URI.createPlatformResourceURI(targetFolder,true)
+        }
+        
+        override getWorkspaceURI() {
+                getDirUri
+        }
+        
+        override initAndClear() {
+                target = ResourcesPlugin.workspace.root
+                for(nameSegment : dirUri.segments) {
+                        target = createContainer(target,nameSegment)
+                }
+                target.members.forEach[delete(false,monitor)]
+        }
+        
+        def protected dispatch createContainer(IWorkspaceRoot root, String name) {
+                val project = root.getProject(name)
+                if(project.exists) {
+                        if(!project.open) {
+                                project.open(monitor)
+                        }
+                } else {
+                        project.create(monitor)
+                }
+                return project
+        }
+        
+        def protected dispatch createContainer(IProject root, String name) {
+                val folder = root.getFolder(name);
+                if(folder.exists) {
+                        folder.create(false,true,monitor)
+                }
+                return folder
+        }
+        
+        def protected dispatch createContainer(IFolder root, String name) {
+                val folder = root.getFolder(name);
+                if(folder.exists) {
+                        folder.create(false,true,monitor)
+                }
+                return folder
+        }
+        
+        def dispatch getTargetFile(IFolder targetFolder, String name) { targetFolder.getFile(name) }
+        def dispatch getTargetFile(IProject targetProject, String name) { targetProject.getFile(name) }
+        
+        override writeText(String name, CharSequence content) {
+                val file = target.getTargetFile(name);
+                if(!file.exists()) {
+                        file.create(new ByteArrayInputStream(content.toString().getBytes()),true, new NullProgressMonitor());
+                        return URI.createPlatformResourceURI(file.projectRelativePath.toString,true)
+                }
+                else throw new IOException("The file is already existing.")
+        }
+        
+        override readText(String name) {                
+                val file = target.getTargetFile(name)
+                val in = new BufferedReader(new InputStreamReader(file.contents))
+                
+                var result = ""
+                var String line;
+                
+                while ((line = in.readLine()) != null) {
+                        result = result.concat(line)
+                }
+                
+        return result
+        }
+        
+        override protected renameFile(String name) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override subWorkspace(String targetFolder, String prefix) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+}
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ReasonerWorkspace.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ReasonerWorkspace.xtend
new file mode 100644
index 00000000..a7e3a48b
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ReasonerWorkspace.xtend
@@ -0,0 +1,100 @@
+package hu.bme.mit.inf.dslreasoner.workspace
+import java.io.FileNotFoundException
+import java.util.Collections
+import org.eclipse.emf.common.util.URI
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.emf.ecore.resource.ResourceSet
+import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl
+import org.eclipse.emf.ecore.resource.Resource
+import java.io.ByteArrayOutputStream
+import java.io.IOException
+abstract class ReasonerWorkspace{
+        
+        protected val String targetFolder;
+        protected val String prefix;
+        val ResourceSet resSet = new ResourceSetImpl();
+        
+        public new(String targetFolder, String prefix) {
+                this.targetFolder = targetFolder
+                this.prefix = prefix
+        }
+        
+        public def ReasonerWorkspace subWorkspace(String targetFolder, String prefix);
+        
+        def URI getWorkspaceURI();
+        
+        /**
+         * Creates the target folder and clears the workspace for the reasoning
+         */
+        def public void initAndClear()
+        
+        def protected URI getURI(String name);
+        protected def Resource getResource(String name) {
+                val prevoius = resSet.getResource(getURI(name),false);
+                if(prevoius!= null) prevoius.delete(Collections.EMPTY_MAP)
+                
+                val URI resourceURI = getURI(name)
+                return resSet.createResource(resourceURI);
+        }
+        
+        
+        /**
+         * Writes a model 
+         */
+        def public URI writeModel(EObject modelRoot, String name) {
+            val resource = getResource(name);
+            resource.getContents().add(modelRoot);
+                resource.save(Collections.EMPTY_MAP);
+                return resource.URI
+        }
+        
+        
+        def public String writeModelToString(EObject modelRoot, String name) {
+                val resource = getResource(name);
+                resource.getContents().add(modelRoot);
+                val ByteArrayOutputStream outputStream = new ByteArrayOutputStream();
+                resource.save(outputStream, null);
+                return outputStream.toString();
+        }
+        
+        def public <RootType extends EObject> RootType reloadModel(Class<RootType> type, String name) {
+                try {
+                        val resource = resSet.getResource(getURI(name),false);
+                        if(resource.loaded) {
+                                resource.unload
+                        }
+                        resource.load(Collections.EMPTY_MAP)
+                        if(resource == null) throw new FileNotFoundException(getURI(name).toString)
+                        else return resource.contents.get(0) as RootType        
+                } catch(Exception e) {
+                        throw new FileNotFoundException(getURI(name).toString)
+                }
+        } 
+        
+        def public <RootType extends EObject> RootType readModel(Class<RootType> type, String name) {
+                try {
+                        val resource = resSet.getResource(getURI(name),true);
+                        if(resource == null) throw new FileNotFoundException(getURI(name).toString)
+                        else return resource.contents.get(0) as RootType        
+                } catch(Exception e) {
+                        throw new FileNotFoundException(getURI(name).toString + "reason: " + e.message)
+                }
+        }
+        
+        def public deactivateModel(String name) {
+                val resource = resSet.getResource(getURI(name),true);
+                resource.unload
+                renameFile(name)
+        }
+        val static protected deactivationPostfix = ".deactivated"
+        def protected void renameFile(String name)
+        
+//      def void reactivate()
+//      def void deactivate()
+        def public URI writeText(String name, CharSequence content);
+        
+        def public String readText(String name);
+}
+\ No newline at end of file
author	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
committer	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
commit	60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree	5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme
parent	Initial commit, migrating from SVN (diff)
download	VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip