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 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu
parent: Initial commit, migrating from SVN (diff)
download: VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
16 files changed, 2614 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend
new file mode 100644
index 00000000..cdf21174
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend
@@ -0,0 +1,32 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+class AlloySolverConfiguration extends LogicSolverConfiguration {
+        /*public var boolean createCommonSupertype
+        public var int intScope = 1 // 5 by default
+        public def setIntScopeFor(int max) {
+                intScope = 31 - Integer.numberOfLeadingZeros(max) + 1
+        }*/
+        public var int symmetry = 0 // by default
+        public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J
+        public var boolean writeToFile = false
+}
+enum AlloyBackendSolver {
+        BerkMinPIPE,
+        SpearPIPE,
+        MiniSatJNI,
+        MiniSatProverJNI,
+        LingelingJNI,
+        PLingelingJNI,
+        GlucoseJNI,
+        CryptoMiniSatJNI,
+        SAT4J,
+        CNF,
+        KodKod
+}
+enum TypeMappingTechnique {
+        FilteredTypes
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
new file mode 100644
index 00000000..7dfc3161
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
@@ -0,0 +1,72 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution
+import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes
+import org.eclipse.emf.common.util.URI
+class AlloySolver extends LogicReasoner{
+        
+        new() {
+                AlloyLanguagePackage.eINSTANCE.eClass
+                val x = new AlloyLanguageStandaloneSetupGenerated
+                x.createInjectorAndDoEMFRegistration
+        }
+        
+        val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes)
+        val AlloyHandler handler = new AlloyHandler
+        val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper
+        
+        val fileName = "problem.als"
+        
+        override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
+                if(configuration instanceof AlloySolverConfiguration) {
+                        val transformationStart = System.currentTimeMillis
+                        val result = forwardMapper.transformProblem(problem,configuration)
+                        val alloyProblem = result.output
+                        
+                        /*val x = alloyProblem.eAllContents.filter(ALSFunctionCall).filter[it.referredDefinition == null].toList
+                        println(x)*/
+                        val forwardTrace = result.trace
+                        
+                        var String fileURI = null;
+                        var String alloyCode = null;
+                        if(configuration.writeToFile) {
+                                fileURI = workspace.writeModel(alloyProblem,fileName).toFileString
+                        } else {
+                                alloyCode = workspace.writeModelToString(alloyProblem,fileName)
+                        }
+                        
+                        //val alloyCode = workspace.readText(fileName)
+                        //val FunctionWithTimeout<MonitoredAlloySolution> call = new FunctionWithTimeout[] 
+                        
+                        val transformationTime = System.currentTimeMillis - transformationStart
+                        val result2 = handler.callSolver(alloyProblem,workspace,configuration,fileURI,alloyCode)
+                        workspace.deactivateModel(fileName)
+                        val logicResult = backwardMapper.transformOutput(problem,result2,forwardTrace,transformationTime)
+                        return logicResult
+                } else throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''')
+        }
+        
+        override getInterpretation(ModelResult modelResult) {
+                return new AlloyModelInterpretation(
+                        new AlloyModelInterpretation_TypeInterpretation_FilteredTypes,
+                        (modelResult.representation as MonitoredAlloySolution).solution,
+                        forwardMapper,
+                        modelResult.trace as Logic2AlloyLanguageMapperTrace
+                );
+        }       
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
new file mode 100644
index 00000000..637752b0
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
@@ -0,0 +1,48 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
+class Alloy2LogicMapper {
+        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
+        
+        public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
+                if(solution == null) {
+                        return createInsuficientResourcesResult => [
+                                it.problem = problem
+                                it.statistics = transformStatistics(solution,transformationTime)
+                        ]
+                } else {
+                        val logicResult = solution.solution
+                        if(logicResult.satisfiable) {
+                                return createModelResult => [
+                                        it.problem = problem
+                                        it.representation += solution
+                                        it.maxInteger = logicResult.max
+                                        it.minInteger = logicResult.min
+                                        it.trace = trace
+                                        it.statistics = transformStatistics(solution,transformationTime)
+                                ]
+                        } else {
+                                return createInconsistencyResult => [
+                                        it.problem = problem
+                                        //trace?
+                                        it.statistics = transformStatistics(solution,transformationTime)
+                                ]
+                        }
+                }
+        }
+        
+        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
+                createStatistics => [
+                        it.transformationTime = transformationTime as int
+                        if(solution != null) {
+                                it.solverTime = solution.runtimeTime as int
+                                it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [
+                                        it.name = "KoodkodToCNFTransformationTime"
+                                        it.value = solution.getKodkodTime as int
+                                ]
+                        }
+                ]
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
new file mode 100644
index 00000000..6bac4130
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
@@ -0,0 +1,145 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import edu.mit.csail.sdg.alloy4.A4Reporter
+import edu.mit.csail.sdg.alloy4.Err
+import edu.mit.csail.sdg.alloy4.ErrorWarning
+import edu.mit.csail.sdg.alloy4compiler.ast.Command
+import edu.mit.csail.sdg.alloy4compiler.parser.CompModule
+import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Options
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
+import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import java.util.LinkedList
+import java.util.List
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
+import org.eclipse.xtend.lib.annotations.Data
+import java.util.Map
+import java.util.HashMap
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver
+import org.eclipse.emf.common.CommonPlugin
+import java.util.ArrayList
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
+class AlloySolverException extends Exception{
+        new(String s) { super(s) }
+        new(String s, Exception e) { super(s,e) }
+        new(String s, List<String> errors, Exception e) {
+                super(s + '\n' + errors.join('\n'), e)
+        }
+}
+@Data class MonitoredAlloySolution{
+        List<String> warnings
+        List<String> debugs
+        long kodkodTime
+        long runtimeTime
+        
+        A4Solution solution
+}
+class AlloyHandler {
+        
+        //val fileName = "problem.als"
+        
+        public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, String alloyCode) {
+                //Prepare
+                
+                val warnings = new LinkedList<String>
+                val debugs = new LinkedList<String>
+                val runtime = new ArrayList<Long>
+                val reporter = new A4Reporter() {
+                        override debug(String message) { debugs += message }
+                        override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime }
+                        override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime }
+                        override warning(ErrorWarning msg) { warnings += msg.message }
+                }
+                
+                val options = new A4Options() => [
+                        it.symmetry = configuration.symmetry
+                        it.noOverflow = true
+                        it.solver = getSolver(configuration.solver, configuration)
+                        if(configuration.solver.externalSolver) {
+                                it.solverDirectory = configuration.solverPath
+                        }
+                        it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString
+                ]
+                
+                // Transform
+                var Command command = null;
+                var CompModule compModule = null
+                
+                val kodkodTransformStart = System.currentTimeMillis();
+                
+                try {
+                        if(configuration.writeToFile) {
+                                compModule = CompUtil.parseEverything_fromFile(reporter,null,path)
+                        } else {
+                                compModule = CompUtil.parseEverything_fromString(reporter,alloyCode)
+                        }
+                        if(compModule.allCommands.size != 1)
+                                throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''')
+                        command = compModule.allCommands.head
+                } catch (Err e){
+                        throw new AlloySolverException(e.message,warnings,e)
+                }
+                val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart
+                
+                //Execute
+                var A4Solution answer = null;
+                try {
+                        answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
+                }catch(Exception e) {
+                        warnings +=e.message
+                }
+                
+                var long runtimeFromAnswer;
+                if(runtime.empty) {
+                        runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish)
+                } else {
+                        runtimeFromAnswer = runtime.head
+                }
+                
+                return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer)
+        }
+        
+        val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap
+        def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) {
+                val config = new SolverConfiguration(backedSolver,path,options)
+                if(previousSolverConfigurations.containsKey(config)) {
+                        return previousSolverConfigurations.get(config)
+                } else {
+                        val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»'''
+                        val newSolver = A4Options.SatSolver.make(id,id,path,options)
+                        previousSolverConfigurations.put(config,newSolver)
+                        return newSolver
+                }
+        }
+        
+        def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) {
+                switch(backedSolver){
+                        case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE
+                        case SpearPIPE: return A4Options.SatSolver.SpearPIPE
+                        case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI
+                        case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI
+                        case LingelingJNI: return A4Options.SatSolver.LingelingJNI
+                        case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null)
+                        case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI
+                        case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI
+                        case SAT4J: return A4Options.SatSolver.SAT4J
+                        case CNF: return A4Options.SatSolver.CNF
+                        case KodKod: return A4Options.SatSolver.KK
+                }
+        }
+        
+        def isExternalSolver(AlloyBackendSolver backedSolver) {
+                return !(backedSolver == AlloyBackendSolver.SAT4J)
+        }
+}
+@Data class SolverConfiguration {
+        AlloyBackendSolver backedSolver
+        String path
+        String[] options
+}
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
new file mode 100644
index 00000000..d00291e0
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
@@ -0,0 +1,331 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
+import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
+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.LogiclanguageFactory
+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.Arrays
+import java.util.HashMap
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import java.util.Set
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import edu.mit.csail.sdg.alloy4compiler.ast.Sig
+import java.util.ArrayList
+interface AlloyModelInterpretation_TypeInterpretation {
+        def void resolveUnknownAtoms(
+                Iterable<ExprVar> objectAtoms, 
+                A4Solution solution,
+                Logic2AlloyLanguageMapperTrace forwardTrace,
+                Map<String, Sig> name2AlloySig,
+                Map<String, Field> name2AlloyField,
+                Map<String,DefinedElement> expression2DefinedElement,
+                Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)
+}
+class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        
+        override resolveUnknownAtoms(
+                Iterable<ExprVar> objectAtoms, 
+                A4Solution solution,
+                Logic2AlloyLanguageMapperTrace forwardTrace,
+                Map<String, Sig> name2AlloySig,
+                Map<String, Field> name2AlloyField,
+                Map<String,DefinedElement> expression2DefinedElement,
+                Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)
+        {
+                /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap()
+                val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/
+                
+                val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
+                
+                // 1. Evaluate the defined elements
+                for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) {
+                        val name = definedElementMappingEntry.value.name
+                        val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)
+                        val elementsOfSingletonSignature = solution.eval(matchingSig)
+                        if(elementsOfSingletonSignature.size != 1) {
+                                throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''')
+                        } else {
+                                val expressionOfDefinedElement  = elementsOfSingletonSignature.head.atom(0)// as ExprVar
+                                expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key)
+                        }
+                }
+                
+                // 2. evaluate the signatures and create new elements if necessary
+                for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) {
+                        val type = type2SingatureEntry.key
+                        if(type instanceof TypeDeclaration) {
+                                val name = type2SingatureEntry.value.name
+                                val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)
+                                val elementsOfSignature = solution.eval(matchingSig)
+                                val elementList = new ArrayList(elementsOfSignature.size)
+                                var newVariableIndex = 1;
+                                for(elementOfSignature : elementsOfSignature) {
+                                        val expressionOfDefinedElement  = elementOfSignature.atom(0)
+                                        if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) {
+                                                elementList += expressionOfDefinedElement.lookup(expression2DefinedElement)
+                                        } else {
+                                                val newElementName = '''newObject «newVariableIndex.toString»'''
+                                                val newRepresentation = createDefinedElement => [
+                                                        it.name = newElementName
+                                                ]
+                                                elementList += newRepresentation
+                                                expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation)
+                                        }
+                                }
+                                interpretationOfUndefinedType.put(type,elementList)
+                        }
+                }
+        }
+}
+/*
+class AlloyModelInterpretation_TypeInterpretation_Horizontal implements AlloyModelInterpretation_TypeInterpretation{
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        
+        override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String,DefinedElement> alloyAtom2LogicElement) {
+                val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;
+                
+                //TMP sig maps to identify alloy signatures by their names
+                val Map<String,Type> sigName2LogicType =
+                        forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name]
+                //val Map<String,DefinedElement> elementNameNamel2DefinedElement = 
+                //      forwardTrace.definedElement2Declaration.keySet.toMap[x|forwardTrace.definedElement2Declaration.get(x).name]
+                        
+                // Fill the interpretation map with empty lists
+                forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x|interpretationOfUndefinedType.put(x,new LinkedList)]
+                
+                // exporing individuals
+                for(atom: objectAtoms) {
+                        val typeName = getName(atom.type)
+                        //val atomName = atom.name
+                        
+                        if(sigName2LogicType.containsKey(typeName)) {
+                                val type = sigName2LogicType.get(typeName)
+                                val elementsOfType = interpretationOfUndefinedType.get(type)
+                                val element = createDefinedElement => [
+                                        it.name += type.name
+                                        it.name += (elementsOfType.size+1).toString
+                                ]
+                                alloyAtom2LogicElement.put(atom.label,element)
+                                elementsOfType+=element
+                        }
+                        else throw new UnsupportedOperationException('''Unknown atom: «atom»''')
+                }
+                
+                return interpretationOfUndefinedType
+        }
+        
+        def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) {
+                val name = type.toString
+                if(name.startsWith("{this/") && name.endsWith("}")) {
+                        return type.toString.replaceFirst("\\{this\\/","").replace("}","")
+                }
+                else throw new IllegalArgumentException('''Unknown type format: "«name»"!''')
+        }
+        //def private getName(ExprVar atom) { atom.toString.split("\\$") }
+}*/
+class AlloyModelInterpretation implements LogicModelInterpretation{
+        
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        protected val AlloyModelInterpretation_TypeInterpretation typeInterpretator
+                
+        protected val Logic2AlloyLanguageMapper forwardMapper
+        protected val Logic2AlloyLanguageMapperTrace forwardTrace;
+        
+        private var ExprVar logicLanguage;
+        
+        private var String logicBooleanTrue;
+        private var String logicBooleanFalse;
+                
+        private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap
+        private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap
+        
+        private val Map<ConstantDeclaration, Object> constant2Value
+        private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value
+        private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value
+        
+        private val int minInt
+        private val int maxInt
+        
+        public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) {
+                this.typeInterpretator = typeInterpretator
+                this.forwardMapper = forwardMapper
+                this.forwardTrace = trace
+                
+                // Maps to trace language elements to the parsed problem.
+                val Map<String, Sig> name2AlloySig = new HashMap
+                val Map<String, Field> name2AlloyField = new HashMap
+                // exploring signatures
+                for(sig:solution.allReachableSigs) {
+                        name2AlloySig.put(sig.label,sig)
+                        for(field : sig.fields) {
+                                name2AlloyField.put(field.label,field)
+                        }
+                }
+                
+                val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution.allAtoms)
+                this.typeInterpretator.resolveUnknownAtoms(
+                        unknownAtoms,
+                        solution,
+                        forwardTrace,
+                        name2AlloySig,
+                        name2AlloyField,
+                        alloyAtom2LogicElement,
+                        interpretationOfUndefinedType)
+                
+                // eval consants
+                constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[
+                        solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term
+                ]
+                // eval functions
+                val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function |
+                        newHashMap(
+                                solution.eval(function.name.lookup(name2AlloyField))
+                                        .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])]
+                
+                val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function |
+                        val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField)
+                        val paramIndexes = 1..(function.parameters.size)
+                        return newHashMap(
+                                solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t |
+                                        new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term])
+                                                ->
+                                        t.atom(function.parameters.size + 1).atomLabel2Term
+                                ])]
+                this.function2Value = Union(hostedfunction2Value,globalfunction2Value)
+                // eval relations
+                val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation |
+                        solution.eval(relation.name.lookup(name2AlloyField)).map[ t |
+                                new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet]
+                val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation |
+                        solution.eval(relation.name.lookup(name2AlloyField)).map[ t |
+                                new ParameterSubstitution((1..<t.arity).map[int a|t.atom(a).atomLabel2Term])].toSet]
+                this.relation2Value = Union(hostedRelation2Value,globalRelation2Value)
+                
+                //Int limits
+                this.minInt = solution.min
+                this.maxInt = solution.max
+                
+                //print(trace)
+        }
+        
+        def List<ExprVar> collectUnknownAndResolveKnownAtoms(Iterable<ExprVar> allAtoms) {
+                val List<ExprVar> unknownAtoms = new LinkedList
+                
+                for(atom: allAtoms) {
+                        val typeName = getName(atom.type)
+                        val atomName = atom.name
+                        //println(atom.toString + "  < -  " + typeName)
+                        if(typeName == forwardTrace.logicLanguage.name) {
+                                this.logicLanguage = atom
+                        } else if(typeName == "Int" || typeName == "seq/Int") {
+                                // do nothing, integers will be parsed from the string
+                        } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) {
+                                if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label }
+                                else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label}
+                                else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''')
+                        }
+                        else unknownAtoms += atom
+                }
+                
+                return unknownAtoms
+        }
+        
+        def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) {
+                val name = type.toString
+                if(name.startsWith("{this/") && name.endsWith("}")) {
+                        return type.toString.replaceFirst("\\{this\\/","").replace("}","")
+                }
+                else throw new IllegalArgumentException('''Unknown type format: "«name»"!''')
+        }
+        def private getName(ExprVar atom) { atom.toString.split("\\$") }
+        
+        def print(Logic2AlloyLanguageMapperTrace trace) {
+                println('''Undefined-----''')
+                interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v.map[name]»''')]
+                //println('''Defined-----''')
+                //trace.type2ALSType.keySet.filter(TypeDefinition).forEach[println('''«it.name» -> «it.elements.map[name.join]»''')]
+                
+                println('''Constants-----''')
+                constant2Value.forEach[k, v|println('''«k.name» : «v»''')]
+                println('''Functions-----''')
+                function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]]
+                println('''Relations-----''')
+                relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]]
+        }
+        override getElements(Type type) { getElementsDispatch(type) }
+        def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) }
+        def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements }
+        
+        override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
+                val transformedParams = new ParameterSubstitution(parameterSubstitution)
+                return transformedParams.lookup(
+                        function.lookup(this.function2Value)
+                )
+        }
+        
+        override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+                relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution))
+        }
+        
+        override getInterpretation(ConstantDeclaration constant) {
+                constant.lookup(this.constant2Value)
+        }
+        
+        override getMinimalInteger() { this.minInt }
+        override getMaximalInteger() { this.maxInt }
+        
+        // Alloy term -> logic term
+        def private atomLabel2Term(String label) {
+                if(label.number) return Integer.parseInt(label)
+                else if(label == this.logicBooleanTrue) return true
+                else if(label == this.logicBooleanFalse) return false
+                else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement)
+                else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''')
+        }
+        def private isNumber(String s) {
+                try{
+                        Integer.parseInt(s)
+                        return true
+                }catch(NumberFormatException e) {
+                        return false
+                }
+        }
+}
+/**
+ * Helper class for efficiently matching parameter substitutions for functions and relations.
+ */
+class ParameterSubstitution{
+        val Object[] data;
+        
+        new(Object[] data) { this.data = data }
+        
+        override equals(Object obj) {
+                if(obj === this) return true
+                else if(obj == null) return false
+                if(obj instanceof ParameterSubstitution) {
+                        return Arrays.equals(this.data,obj.data)
+                }
+                return false
+        }
+        
+        override hashCode() {
+                Arrays.hashCode(data)
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
new file mode 100644
index 00000000..23b9027f
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
@@ -0,0 +1,467 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumericOperator
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
+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.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+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.Iff
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf
+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.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.RealTypeReference
+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.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import java.util.Collections
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.viatra.query.runtime.emf.EMFScope
+import org.eclipse.xtend.lib.annotations.Accessors
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation
+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation
+import java.util.Collection
+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion
+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct
+class Logic2AlloyLanguageMapper {
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
+        @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this)
+        @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this)
+        @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_RelationMapper relationMapper = new Logic2AlloyLanguageMapper_RelationMapper(this)
+        @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_Containment containmentMapper = new Logic2AlloyLanguageMapper_Containment(this)
+        
+        public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
+                this.typeMapper = typeMapper
+        }
+        
+        public def TracedOutput<ALSDocument,Logic2AlloyLanguageMapperTrace> transformProblem(LogicProblem problem, AlloySolverConfiguration config) {
+                val logicLanguage = createALSSignatureBody => [
+                                it.multiplicity = ALSMultiplicity.ONE
+                                it.declarations +=
+                                        createALSSignatureDeclaration => [
+                                                        it.name = support.toID(#["util", "language"]) ] 
+                ]
+                
+                val specification = createALSDocument=>[
+                        it.signatureBodies+=logicLanguage
+                ]
+                val trace = new Logic2AlloyLanguageMapperTrace => [
+                        it.specification = specification
+                        it.logicLanguage = logicLanguage.declarations.head
+                        it.logicLanguageBody = logicLanguage
+                        
+                        it.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem))
+                ]
+                
+                typeMapper.transformTypes(problem.types,problem.elements,this,trace)
+                
+                trace.constantDefinitions = problem.collectConstantDefinitions
+                trace.functionDefinitions = problem.collectFunctionDefinitions
+                trace.relationDefinitions = problem.collectRelationDefinitions
+                
+                problem.constants.forEach[this.constantMapper.transformConstant(it,trace)]
+                problem.functions.forEach[this.functionMapper.transformFunction(it, trace)]
+                problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
+                
+                problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstantDefinitionSpecification(it,trace)]
+                problem.functions.filter(FunctionDefinition).forEach[this.functionMapper.transformFunctionDefinitionSpecification(it,trace)]
+                problem.relations.filter(RelationDefinition).forEach[this.relationMapper.transformRelationDefinitionSpecification(it,trace)]
+                
+                val containment = problem.getContainmentHierarchies.head
+                if(containment !== null) {
+                        this.containmentMapper.transformContainmentHierarchy(containment,trace)
+                }
+                
+                ////////////////////
+                // Collect EMF-specific assertions
+                ////////////////////
+                val assertion2InverseRelation = problem.annotations.collectAnnotations(InverseRelationAssertion)
+                val assertion2UpperMultiplicityAssertion = problem.annotations.collectAnnotations(UpperMultiplicityAssertion)
+                val assertion2LowerMultiplicityAssertion = problem.annotations.collectAnnotations(LowerMultiplicityAssertion)
+                
+                ////////////////////
+                // Transform Assertions
+                ////////////////////
+                for(assertion : problem.assertions) {
+                        if(assertion2InverseRelation.containsKey(assertion)) {
+                                transformInverseAssertion(assertion.lookup(assertion2InverseRelation),trace)
+                        } else if(assertion2UpperMultiplicityAssertion.containsKey(assertion)) {
+                                transformUpperMultiplicityAssertion(assertion.lookup(assertion2UpperMultiplicityAssertion),trace)
+                        } else if(assertion2LowerMultiplicityAssertion.containsKey(assertion)) {
+                                transformLowerMultiplicityAssertion(assertion.lookup(assertion2LowerMultiplicityAssertion),trace)
+                        } else {
+                                transformAssertion(assertion,trace)
+                        }
+                }
+                
+                transformRunCommand(specification, trace, config)
+                
+                return new TracedOutput(specification,trace)
+        }
+        
+        def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) {
+                val a = assertion.inverseA
+                val b = assertion.inverseB
+                if(a instanceof RelationDeclaration && b instanceof RelationDeclaration &&
+                        !trace.relationDefinitions.containsKey(a) && !trace.relationDefinitions.containsKey(b))
+                {
+                        val fact = createALSFactDeclaration => [
+                                it.name = support.toID(assertion.target.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = relationMapper.transformRelationReference(a as RelationDeclaration, trace)
+                                        it.rightOperand = createALSInverseRelation => [it.operand = relationMapper.transformRelationReference(b as RelationDeclaration, trace) ]
+                                ]
+                        ]
+                        trace.specification.factDeclarations += fact
+                } else {
+                        return transformAssertion(assertion.target,trace)
+                }
+        }
+        
+        def transformUpperMultiplicityAssertion(UpperMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) {
+                val x = assertion.relation
+                if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) {
+                        val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace)
+                        val type = relation.type
+                        
+                        if(type instanceof ALSDirectProduct) {
+                                type.rightMultiplicit = type.rightMultiplicit.addUpper
+                        } else {
+                                relation.multiplicity = relation.multiplicity.addUpper
+                        }
+                        
+                        if(assertion.upper === 1) {
+                                return true
+                        } else {
+                                return transformAssertion(assertion.target,trace)
+                        }
+                        
+                } else {
+                        return transformAssertion(assertion.target,trace)
+                }
+        }
+        
+        def transformLowerMultiplicityAssertion(LowerMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) {
+                val x = assertion.relation
+                if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) {
+                        val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace)
+                        val type = relation.type
+                        
+                        if(type instanceof ALSDirectProduct) {
+                                type.rightMultiplicit = type.rightMultiplicit.addLower
+                        } else {
+                                relation.multiplicity = relation.multiplicity.addLower
+                        }
+                        
+                        if(assertion.lower === 1) {
+                                return true
+                        } else {
+                                return transformAssertion(assertion.target,trace)
+                        }
+                        
+                } else {
+                        return transformAssertion(assertion.target,trace)
+                }
+        }
+        
+        private def addLower(ALSMultiplicity multiplicity) {
+                if(multiplicity === ALSMultiplicity::SET || multiplicity === null) {
+                        return ALSMultiplicity::SOME
+                } else if(multiplicity === ALSMultiplicity::LONE) {
+                        return ALSMultiplicity::ONE
+                } else {
+                        throw new IllegalArgumentException('''Lower multiplicity is already set!''')
+                }
+        }
+        private def addUpper(ALSMultiplicity multiplicity) {
+                if(multiplicity === ALSMultiplicity::SET || multiplicity === null) {
+                        return ALSMultiplicity::LONE
+                } else if(multiplicity === ALSMultiplicity::SOME) {
+                        return ALSMultiplicity::ONE
+                } else {
+                        throw new IllegalArgumentException('''Upper multiplicity is already set!''')
+                }
+        }
+        
+        private def <T extends AssertionAnnotation>  collectAnnotations(Collection<? extends Annotation> collection, Class<T> annotationKind) {
+                val res = new HashMap
+                collection.filter(annotationKind).forEach[res.put(it.target,it)]
+                return res
+        }
+        
+        private def collectConstantDefinitions(LogicProblem problem) {
+                val res = new HashMap
+                problem.constants.filter(ConstantDefinition).filter[it.defines!==null].forEach[
+                        res.put(it.defines,it)
+                ]
+                return res
+        }
+        private def collectFunctionDefinitions(LogicProblem problem) {
+                val res = new HashMap
+                problem.functions.filter(FunctionDefinition).filter[it.defines!==null].forEach[
+                        res.put(it.defines,it)
+                ]
+                return res
+        }
+        private def collectRelationDefinitions(LogicProblem problem) {
+                val res = new HashMap
+                problem.relations.filter(RelationDefinition).filter[it.defines!==null].forEach[
+                        res.put(it.defines,it)
+                ]
+                return res
+        }
+        
+        ////////////////////
+        // Type References
+        ////////////////////
+        def dispatch protected ALSTerm transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyLanguageMapperTrace trace) {
+                return createALSReference => [ it.referred = support.getBooleanType(trace) ]
+        }
+        def dispatch protected ALSTerm transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt }
+        def dispatch protected ALSTerm transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyLanguageMapperTrace trace) {throw new UnsupportedOperationException('''Real types are not supported in Alloy.''')}
+        def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) {
+                val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace)
+                return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]])
+        }       
+        
+        //////////////
+        // Scopes
+        //////////////
+        
+        def transformRunCommand(ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) {
+                specification.runCommand = createALSRunCommand => [
+                        it.typeScopes+= createALSSigScope => [
+                                it.type= typeMapper.getUndefinedSupertype(trace)
+                                it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) 
+                                //it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements)
+                        ]
+                        if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException(
+                                '''An integer scope have to be specified for Alloy!''')
+                        it.typeScopes += createALSIntScope => [
+                                number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxIntScope)
+                        ]
+//                      for(definedScope : config.typeScopes.allDefinedScope) {
+//                              it.typeScopes += createALSSigScope => [
+//                                      it.type = definedScope.type.lookup(trace.type2ALSType)
+//                                      it.number = definedScope.upperLimit
+//                                      it.exactly = (definedScope.upperLimit == definedScope.lowerLimit)
+//                              ]
+//                      }
+                ]
+        }
+        
+        
+        //////////////
+        // Assertions + Terms
+        //////////////
+        
+        def protected transformAssertion(Assertion assertion, Logic2AlloyLanguageMapperTrace trace) {
+                val res = createALSFactDeclaration => [
+                        it.name = support.toID(assertion.name)
+                        it.term = assertion.value.transformTerm(trace,Collections.EMPTY_MAP)
+                ]
+                trace.specification.factDeclarations += res
+        }       
+        
+        def dispatch protected ALSTerm transformTerm(BoolLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                var ALSEnumLiteral ref;
+                if(literal.value==true) {ref = support.getBooleanTrue(trace)}
+                else {ref = support.getBooleanFalse(trace)}
+                val refFinal = ref
+                
+                return  support.booleanToLogicValue((createALSReference => [referred = refFinal]),trace)
+        }
+        def dispatch protected ALSTerm transformTerm(RealLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                throw new UnsupportedOperationException("RealLiteral is not supported")
+        }
+        def dispatch protected ALSTerm transformTerm(IntLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables)  {
+                if(literal.value>=0) { createALSNumberLiteral => [value = literal.value]}
+                else {createALSUnaryMinus  => [it.operand = createALSNumberLiteral => [value = literal.value] ] } 
+        }
+        
+        def dispatch protected ALSTerm transformTerm(Not not, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSNot=>[operand = not.operand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(And and, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                support.unfoldAnd(and.operands.map[transformTerm(trace,variables)]) }
+        def dispatch protected ALSTerm transformTerm(Or or, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                support.unfoldOr(or.operands.map[transformTerm(trace,variables)],trace) }
+        def dispatch protected ALSTerm transformTerm(Impl impl, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSImpl => [leftOperand = impl.leftOperand.transformTerm(trace,variables) rightOperand = impl.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(Iff iff, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSIff => [leftOperand = iff.leftOperand.transformTerm(trace,variables) rightOperand = iff.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(MoreThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(LessThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(MoreOrEqualThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(LessOrEqualThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(Equals equals, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSEquals => [leftOperand = equals.leftOperand.transformTerm(trace,variables) rightOperand = equals.rightOperand.transformTerm(trace,variables)] }
+        def dispatch protected ALSTerm transformTerm(Distinct distinct, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                support.unfoldDistinctTerms(this,distinct.operands,trace,variables) }
+                
+        def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] }
+        def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] }
+        def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] }
+        def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] }
+        def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] }
+        
+        def dispatch protected ALSTerm transformTerm(Forall forall, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                support.createQuantifiedExpression(this,forall,ALSMultiplicity.ALL,trace,variables) }
+        def dispatch protected ALSTerm transformTerm(Exists exists, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                support.createQuantifiedExpression(this,exists,ALSMultiplicity.SOME,trace,variables) }
+        
+        def dispatch protected ALSTerm transformTerm(InstanceOf instanceOf, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                return createALSSubset => [
+                        it.leftOperand = instanceOf.value.transformTerm(trace,variables)
+                        it.rightOperand = instanceOf.range.transformTypeReference(trace)
+                ]
+        }
+        
+        def dispatch protected ALSTerm transformTerm(SymbolicValue symbolicValue, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) }
+        
+        def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                typeMapper.transformReference(referred,trace)}
+        def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                if(trace.constantDefinitions.containsKey(constant)) {
+                        return this.transformSymbolicReference(constant.lookup(trace.constantDefinitions),parameterSubstitutions,trace,variables)
+                } else {
+                        val res = createALSJoin=> [
+                                leftOperand = createALSReference => [ referred = trace.logicLanguage ]
+                                rightOperand = createALSReference => [ referred = constant.lookup(trace.constantDeclaration2LanguageField) ]
+                        ]
+                        return support.postprocessResultOfSymbolicReference(constant.type,res,trace)
+                }
+        }
+        def dispatch protected ALSTerm transformSymbolicReference(ConstantDefinition constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                val res = createALSFunctionCall => [
+                        it.referredDefinition = constant.lookup(trace.constantDefinition2Function)
+                ]
+                return support.postprocessResultOfSymbolicReference(constant.type,res,trace)
+        }
+        def dispatch protected ALSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                val res = createALSReference => [referred = variable.lookup(variables)]
+                return support.postprocessResultOfSymbolicReference(variable.range,res,trace)
+        }
+        def dispatch protected ALSTerm transformSymbolicReference(FunctionDeclaration function, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                if(trace.functionDefinitions.containsKey(function)) {
+                        return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables)
+                } else {
+                        if(functionMapper.transformedToHostedField(function,trace)) {
+                                val param = parameterSubstitutions.get(0).transformTerm(trace,variables)
+                                val res = createALSJoin => [
+                                        leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace)
+                                        rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)]
+                                ]
+                                return support.postprocessResultOfSymbolicReference(function.range,res,trace)
+                        } else {
+                                val functionExpression = createALSJoin=>[
+                                                leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                                rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)]
+                                        ]
+                                val res =  support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables)
+                                return support.postprocessResultOfSymbolicReference(function.range,res,trace)
+                        }
+                }
+        }
+        def dispatch protected ALSTerm transformSymbolicReference(FunctionDefinition function, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                val result = createALSFunctionCall => [
+                        it.referredDefinition = function.lookup(trace.functionDefinition2Function)
+                        it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)]
+                ]
+                return support.postprocessResultOfSymbolicReference(function.range,result,trace)
+        }
+        def dispatch protected ALSTerm transformSymbolicReference(RelationDeclaration relation, List<Term> parameterSubstitutions,
+                Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                if(trace.relationDefinitions.containsKey(relation)) {
+                        this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),parameterSubstitutions,trace,variables)
+                } else {
+                        if(relationMapper.transformToHostedField(relation,trace)) {
+                                val alsRelation = relation.lookup(trace.relationDeclaration2Field)
+                                // R(a,b) =>
+                                // b in a.R
+                                return createALSSubset => [
+                                        it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace,variables)
+                                        it.rightOperand = createALSJoin => [
+                                                it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace,variables)
+                                                it.rightOperand = createALSReference => [ it.referred = alsRelation ]
+                                        ]
+                                ]
+                        } else {
+                                val target = createALSJoin => [
+                                        leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                        rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]]
+                                val source = support.unfoldTermDirectProduct(this,parameterSubstitutions,trace,variables)
+                                
+                                return  createALSSubset => [
+                                        leftOperand = source
+                                        rightOperand = target
+                                ]
+                        }
+                }
+        }
+        
+        
+        def dispatch protected ALSTerm transformSymbolicReference(RelationDefinition relation, List<Term> parameterSubstitutions,
+                Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables)
+        {
+                return createALSFunctionCall => [
+                        it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)
+                        it.params += parameterSubstitutions.map[p | p.transformTerm(trace,variables)]
+                ]
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend
new file mode 100644
index 00000000..22f49c98
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend
@@ -0,0 +1,49 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSFieldDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSFunctionDefinition
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRelationDefinition
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+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.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import java.util.HashMap
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+interface Logic2AlloyLanguageMapper_TypeMapperTrace {}
+class Logic2AlloyLanguageMapperTrace {
+        public var ViatraQueryEngine incqueryEngine;
+        
+        public var ALSDocument specification;
+        public var ALSSignatureDeclaration logicLanguage;
+        public var ALSSignatureBody logicLanguageBody;
+        public var ALSEnumDeclaration boolType;
+        public var ALSEnumLiteral boolTrue;
+        public var ALSEnumLiteral boolFalse;
+        
+        public var Logic2AlloyLanguageMapper_TypeMapperTrace typeMapperTrace 
+        
+        public val Map<ConstantDeclaration, ALSFieldDeclaration> constantDeclaration2LanguageField = new HashMap
+        public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap
+        
+        public val Map<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2HostedField = new HashMap
+        public val Map<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2LanguageField = new HashMap
+        public val Map<FunctionDefinition,ALSFunctionDefinition> functionDefinition2Function = new HashMap
+        
+        public val Map<RelationDeclaration,ALSFieldDeclaration> relationDeclaration2Global = new HashMap
+        public val Map<RelationDeclaration, ALSFieldDeclaration> relationDeclaration2Field = new HashMap
+        public val Map<RelationDefinition,ALSRelationDefinition> relationDefinition2Predicate = new HashMap
+        
+        public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions
+        public var Map<FunctionDeclaration, FunctionDefinition> functionDefinitions
+        public var Map<RelationDeclaration, RelationDefinition> relationDefinitions
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend
new file mode 100644
index 00000000..401c2ec2
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend
@@ -0,0 +1,43 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2AlloyLanguageMapper_ConstantMapper {
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper base;
+        public new(Logic2AlloyLanguageMapper base) {
+                this.base = base
+        }
+        
+        def protected dispatch transformConstant(ConstantDeclaration constant, Logic2AlloyLanguageMapperTrace trace) {
+                if(!trace.constantDefinitions.containsKey(constant)) {
+                        val c = createALSFieldDeclaration=> [
+                                name = support.toID(constant.name)
+                                it.type = base.transformTypeReference(constant.type,trace)
+                                it.multiplicity = ALSMultiplicity.ONE
+                        ]
+                        trace.logicLanguageBody.fields+= c
+                        trace.constantDeclaration2LanguageField.put(constant,c)
+                }
+        }
+        
+        def protected dispatch transformConstant(ConstantDefinition constant, Logic2AlloyLanguageMapperTrace trace) {
+                val c = createALSFunctionDefinition=> [
+                        name = support.toID(constant.name)
+                        it.type = base.transformTypeReference(constant.type,trace)
+                        // the value is set later
+                ]
+                trace.specification.functionDefinitions += c
+                trace.constantDefinition2Function.put(constant,c)
+        }
+        
+        def protected transformConstantDefinitionSpecification(ConstantDefinition constant, Logic2AlloyLanguageMapperTrace trace) {
+                val definition = constant.lookup(trace.constantDefinition2Function)
+                definition.value = base.transformTerm(constant.value, trace,emptyMap)
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend
new file mode 100644
index 00000000..fd519c1e
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend
@@ -0,0 +1,260 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
+import java.util.HashMap
+class Logic2AlloyLanguageMapper_Containment {
+        val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper base;
+        public new(Logic2AlloyLanguageMapper base) {
+                this.base = base
+        }
+        
+        def protected transformContainmentHierarchy(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) {
+                // Single root
+                val rootField = createALSFieldDeclaration => [
+                        it.name= support.toID(#["util", "root"])
+                        it.multiplicity = ALSMultiplicity.ONE
+                        it.type = typesOrderedInContainment(containment,trace)
+                ]
+                trace.logicLanguageBody.fields += rootField
+                
+                val contains = createALSFieldDeclaration => [
+                        it.name = support.toID(#["util", "contains"])
+                        //it.multiplicity = ALSMultiplicity::SET
+                        it.type = createALSDirectProduct => [
+                                it.leftMultiplicit = ALSMultiplicity::LONE
+                                it.rightMultiplicit = ALSMultiplicity::SET
+                                it.leftOperand = typesOrderedInContainment(containment,trace)
+                                it.rightOperand = typesOrderedInContainment(containment,trace)
+                        ]
+                ]
+                trace.logicLanguageBody.fields += contains
+                
+                val containmentRelationDefinition = createALSFactDeclaration => [
+                        it.name = support.toID(#["util", "containmentDefinition"])              
+                ]
+                
+                if(containment.containmentRelations.forall[it instanceof RelationDeclaration]) {
+                        val containmentRelations = containment.containmentRelations.filter(RelationDeclaration).map[relation|
+                                base.relationMapper.transformRelationReference(relation,trace)
+                        ].toList
+                        
+                        containmentRelationDefinition.term = createALSEquals => [
+                                leftOperand = createALSJoin => [
+                                        leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                        rightOperand = createALSReference => [ referred = contains ]]
+                                rightOperand = support.unfoldPlus(containmentRelations)
+                        ]
+                } else {
+                        val parent = createALSVariableDeclaration => [
+                                it.name = "parent"
+                                it.range = typesOrderedInContainment(containment, trace)
+                        ]
+                        val child = createALSVariableDeclaration => [
+                                it.name = "child"
+                                it.range = typesOrderedInContainment(containment, trace)
+                        ]
+                        
+                        val logicFactory = LogiclanguageFactory.eINSTANCE
+                        val logicParentVariable = logicFactory.createVariable
+                        val logicChildVariable = logicFactory.createVariable
+                        val logicParent = logicFactory.createSymbolicValue => [it.symbolicReference = logicParentVariable]
+                        val logicChild = logicFactory.createSymbolicValue => [it.symbolicReference = logicChildVariable]
+                        val variableMap = new HashMap => [put(logicParentVariable,parent) put(logicChildVariable,child)]
+                        val possibleRelations = containment.containmentRelations.map[relation |
+                                base.transformSymbolicReference(relation,#[logicParent,logicChild],trace,variableMap)
+                        ]
+                        
+                        containmentRelationDefinition.term = createALSQuantifiedEx => [
+                                it.type = ALSMultiplicity.ALL
+                                it.variables += parent
+                                it.variables += child
+                                it.expression = createALSIff => [
+                                        it.leftOperand = createALSSubset => [
+                                                it.leftOperand = createALSDirectProduct => [
+                                                        it.leftOperand = createALSReference => [it.referred = child]
+                                                        it.rightOperand = createALSReference => [it.referred = parent]
+                                                ]
+                                                it.rightOperand = createALSJoin => [
+                                                        leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                                        rightOperand = createALSReference => [ referred = contains ]
+                                                ]
+                                        ]
+                                        it.rightOperand = support.unfoldOr(possibleRelations,trace)
+                                ]
+                        ]
+                }
+                
+                trace.specification.factDeclarations += containmentRelationDefinition
+                
+                // With the exception of the root, every object has at least one parent
+                // No parent for root
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["util", "noParentForRoot"])
+                        it.term = createALSQuantifiedEx => [
+                                it.type = ALSMultiplicity::NO
+                                val parent = createALSVariableDeclaration => [
+                                        it.name = "parent"
+                                        it.range = typesOrderedInContainment(containment,trace)
+                                ]
+                                it.variables += parent
+                                it.expression = createALSSubset => [
+                                        it.leftOperand = createALSDirectProduct => [
+                                                it.leftOperand = createALSReference => [it.referred = parent]
+                                                it.rightOperand = createALSJoin => [
+                                                        it.leftOperand = createALSReference => [it.referred = trace.logicLanguage]
+                                                        it.rightOperand = createALSReference => [it.referred = rootField]
+                                                ]
+                                        ]
+                                        it.rightOperand = createALSJoin => [
+                                                leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                                rightOperand = createALSReference => [ referred = contains ]
+                                        ]
+                                ]
+                        ]
+                ]
+                // Parent for nonroot
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["util", "atLeastOneParent"])
+                        it.term = createALSQuantifiedEx => [
+                                it.type = ALSMultiplicity::ALL
+                                val child = createALSVariableDeclaration => [
+                                        it.name = "child"
+                                        it.range = typesOrderedInContainment(containment,trace)
+                                ]
+                                it.variables += child
+                                it.expression = createALSOr => [
+                                        it.leftOperand = createALSEquals => [
+                                                it.leftOperand = createALSReference => [it.referred = child]
+                                                it.rightOperand = createALSJoin => [
+                                                        it.leftOperand = createALSReference => [it.referred = trace.logicLanguage]
+                                                        it.rightOperand = createALSReference => [it.referred = rootField]
+                                                ]
+                                        ]
+                                        it.rightOperand = createALSQuantifiedEx => [
+                                                it.type = ALSMultiplicity::SOME
+                                                val parent = createALSVariableDeclaration => [
+                                                        it.name = "parent"
+                                                        it.range = typesOrderedInContainment(containment, trace)
+                                                ]
+                                                it.variables += parent
+                                                it.expression = createALSSubset => [
+                                                        it.leftOperand = createALSDirectProduct => [
+                                                                it.leftOperand = createALSReference => [it.referred = parent]
+                                                                it.rightOperand = createALSReference => [it.referred = child]
+                                                        ]
+                                                        it.rightOperand = createALSJoin => [
+                                                                leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                                                rightOperand = createALSReference => [ referred = contains ]
+                                                        ]
+                                                ]
+                                        ]
+                                ]
+                        ]
+                ]
+                
+                // Every object has at most one parent
+//              trace.specification.factDeclarations += createALSFactDeclaration => [
+//                      it.name = support.toID(#["util", "atMostOneParent"])
+//                      it.term = createALSQuantifiedEx => [
+//                              it.type = ALSMultiplicity::ALL
+//                              val child = createALSVariableDeclaration => [
+//                                      it.name = "child"
+//                                      it.range = typesOrderedInContainment(containment,trace)
+//                              ]
+//                              it.variables += child
+//                              it.expression = createALSQuantifiedEx => [
+//                                      it.type = ALSMultiplicity::LONE
+//                                      val parent = createALSVariableDeclaration => [
+//                                              it.name = "parent"
+//                                              it.range = typesOrderedInContainment(containment, trace)
+//                                      ]
+//                                      it.variables += parent
+//                                      it.expression = createALSFunctionCall => [
+//                                              it.referredDefinition = containmentRelation
+//                                              it.params += createALSReference => [
+//                                                      it.referred = parent
+//                                                      it.referred = child
+//                                              ]
+//                                      ]
+//                              ]
+//                      ]
+//              ]
+                
+                // No circle in containment
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["util", "noCircularContainment"])
+                        it.term = createALSQuantifiedEx => [
+                                it.type = ALSMultiplicity::NO
+                                val variable = createALSVariableDeclaration => [
+                                        it.name = "circle"
+                                        it.range = typesOrderedInContainment(containment,trace)
+                                ]
+                                it.variables += variable
+                                it.expression = createALSSubset => [
+                                        it.leftOperand = createALSDirectProduct => [
+                                                it.leftOperand = createALSReference => [it.referred = variable]
+                                                it.rightOperand = createALSReference => [it.referred = variable]
+                                        ]
+                                        it.rightOperand = createAlSTransitiveClosure => [
+                                                it.operand = createALSJoin => [
+                                                        leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                                        rightOperand = createALSReference => [ referred = contains ]
+                                                ]
+                                        ]
+                                ]
+                        ]
+                ]
+                
+        }
+        
+        /*def protected calculateContainmentTypeCoveringSignatures(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) {
+                val types = containment.typesOrderedInHierarchy
+                val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten.toList
+//              val uncoveredSignatures = new ArrayList(signaturesInContainment)
+//              val coveringSignatures = new LinkedList
+//              
+                val engine = ViatraQueryEngine.on(new EMFScope(trace.specification))
+                //val directSubsetMatcher = DirectSubsetMatcher.on(engine)
+                // x <= y
+                val subsetMatcher = SubsetMatcher.on(engine) 
+                
+                if()
+        }*/
+        
+        /*def boolean coveringAllSignaturesInContainment(ALSSignatureDeclaration target, List<ALSSignatureDeclaration> signaturesInContainment, SubsetMatcher matcher) {
+                for(signatureInContainment : signaturesInContainment) {
+                        if(!matcher.hasMatch(signatureInContainment,target)) {
+                                return false
+                        }
+                }
+                return true
+        }*/
+        
+        /*def boolean coveringSignatureNotInContainment(ALSSignatureDeclaration target, List<ALSSignatureDeclaration> signaturesInContainment, SubsetMatcher matcher) {
+                val subtypes = matcher.getAllValuesOfx(target);
+                for(subType : subtypes) {
+                        val isSubtypeOfASignatureInContainment = signaturesInContainment.exists[contained |
+                                matcher.hasMatch(subType,contained)
+                        ]
+                        if(!isSubtypeOfASignatureInContainment) {
+                                return false
+                        }
+                }
+                return true
+        }*/
+        
+        def protected typesOrderedInContainment(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) {
+                val types = containment.typesOrderedInHierarchy
+                val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten
+                // val allSignatures = trace.specification.signatureBodies.map[declarations].flatten
+                val typeReferences = signaturesInContainment.map[sig | createALSReference => [it.referred = sig]].toList
+                return support.unfoldPlus(typeReferences)
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend
new file mode 100644
index 00000000..ff18ef80
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend
@@ -0,0 +1,87 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import java.util.HashMap
+class Logic2AlloyLanguageMapper_FunctionMapper {
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper base;
+        public new(Logic2AlloyLanguageMapper base) {
+                this.base = base
+        }
+        
+        def protected dispatch transformFunction(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) {
+                if(!trace.constantDefinitions.containsKey(f)) {
+                        if(transformedToHostedField(f,trace)) transformFunctionToFieldOfSignature(f,trace)
+                        else transformFunctionToGlobalRelation(f,trace)
+                }
+        }
+        
+        def protected transformedToHostedField(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) {
+                if(f.parameters.size == 1 && f.parameters.head instanceof ComplexTypeReference) {
+                        val head = f.parameters.head
+                        if(head instanceof ComplexTypeReference) {
+                                val types = base.typeMapper.transformTypeReference(head.referred,base,trace)
+                                return types.size == 1
+                        }
+                }
+                return (f.parameters.size == 1 && f.parameters.head instanceof ComplexTypeReference)
+        }
+        def protected transformFunctionToFieldOfSignature(FunctionDeclaration f,Logic2AlloyLanguageMapperTrace trace) {
+                val param = (f.parameters.head as ComplexTypeReference)
+                val referred = param.referred
+                val field = createALSFieldDeclaration => [
+                        it.name = support.toID(f.getName)
+                        it.multiplicity = ALSMultiplicity.ONE
+                        it.type = base.transformTypeReference(f.range,trace)
+                ]
+                val host = base.typeMapper.transformTypeReference(referred,base,trace).get(0)
+                (host.eContainer as ALSSignatureBody).fields += field
+                trace.functionDeclaration2HostedField.put(f, field)
+        }
+        def protected transformFunctionToGlobalRelation(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) {
+                val field = createALSFieldDeclaration => [
+                        it.name = support.toID(f.name)
+                        it.multiplicity = ALSMultiplicity.SET
+                        it.type = createALSDirectProduct => [
+                                it.leftOperand = support.unfoldReferenceDirectProduct(base,f.parameters,trace)
+                                it.rightMultiplicit = ALSMultiplicity.ONE
+                                it.rightOperand = base.transformTypeReference(f.range,trace)
+                        ]
+                ]
+                trace.logicLanguageBody.fields += field
+                trace.functionDeclaration2LanguageField.put(f, field)
+        }
+        
+        def protected dispatch transformFunction(FunctionDefinition f, Logic2AlloyLanguageMapperTrace trace) {
+                val res = createALSFunctionDefinition => [
+                        name = support.toID(f.name)
+                        // variables + specification later
+                ]
+                trace.specification.functionDefinitions+=res;
+                trace.functionDefinition2Function.put(f,res)
+        }
+        
+        def protected transformFunctionDefinitionSpecification(FunctionDefinition f, Logic2AlloyLanguageMapperTrace trace) {
+                val target = f.lookup(trace.functionDefinition2Function)
+                val variableMap = new HashMap
+                for(variable : f.variable) {
+                        val v = createALSVariableDeclaration => [
+                                it.name = support.toID(variable.name)
+                                it.range = base.transformTypeReference(variable.range,trace)
+                                // specification later
+                        ]
+                        target.variables+=v
+                        variableMap.put(variable,v)
+                }
+                target.value = base.transformTerm(f.value,trace,variableMap)
+        }
+        
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend
new file mode 100644
index 00000000..9dd4da2f
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend
@@ -0,0 +1,111 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import java.util.HashMap
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2AlloyLanguageMapper_RelationMapper {        
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper base;
+        public new(Logic2AlloyLanguageMapper base) {
+                this.base = base
+        }
+                
+        def dispatch protected void  transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) {
+                if(!trace.relationDefinitions.containsKey(r)) {
+                        if(r.transformToHostedField(trace)) {
+                                transformRelationDeclarationToHostedField(r,trace)
+                        } else {
+                                transformRelationDeclarationToGlobalField(r,trace)
+                        }
+                }
+        }
+        
+        def protected transformToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) {
+                val first = r.parameters.get(0)
+                if(r.parameters.size == 2) {
+                        if(first instanceof ComplexTypeReference) {
+                                val types = base.typeMapper.transformTypeReference(first.referred,base,trace)
+                                if(types.size == 1) {
+                                        return true
+                                }
+                        }
+                }
+                return false
+        }
+        
+        def protected transformRelationDeclarationToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) {
+                val hostType = (r.parameters.head as ComplexTypeReference).referred
+                
+                val targetBody = base.typeMapper.transformTypeReference(hostType,base,trace).get(0).eContainer as ALSSignatureBody
+                val field = createALSFieldDeclaration => [
+                        it.name = support.toID(r.getName)
+                        it.multiplicity = ALSMultiplicity.SET
+                        it.type = base.transformTypeReference(r.parameters.get(1),trace)
+                ]
+                targetBody.fields += field
+                trace.relationDeclaration2Field.put(r,field)
+                
+        }
+        
+        def protected transformRelationDeclarationToGlobalField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) {
+                val field = createALSFieldDeclaration => [
+                        it.name = support.toID(r.name)
+                        it.type = support.unfoldReferenceDirectProduct(base,r.parameters,trace)
+                ]
+                trace.logicLanguageBody.fields += field
+                trace.relationDeclaration2Global.put(r, field)
+        }
+        def dispatch protected void transformRelation(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) {
+                val res = createALSRelationDefinition => [
+                        name = support.toID(r.name)
+                        // fill the variables later
+                        // fill the expression later
+                ]
+                
+                trace.relationDefinition2Predicate.put(r,res)
+                trace.specification.relationDefinitions+=res;
+        }
+        
+        def protected void transformRelationDefinitionSpecification(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) {
+                val predicate = r.lookup(trace.relationDefinition2Predicate)
+                if(predicate !== null) {
+                        val variableMap = new HashMap
+                        for(variable : r.variables) {
+                                val v = createALSVariableDeclaration => [
+                                        it.name = support.toID(variable.name)
+                                        it.range = base.transformTypeReference(variable.range,trace)
+                                ]
+                                predicate.variables+=v
+                                variableMap.put(variable,v)
+                        }
+                        predicate.value = base.transformTerm(r.value,trace,variableMap)
+                }
+        }
+        
+        def public transformRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) {
+                if(relation.transformToHostedField(trace)) {
+                        return createALSReference => [it.referred = relation.lookup(trace.relationDeclaration2Field) ]
+                } else {
+                        return createALSJoin => [
+                                leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]]
+                }
+        }
+        
+        def public getRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) {
+                if(relation.transformToHostedField(trace)) {
+                        return relation.lookup(trace.relationDeclaration2Field)
+                } else {
+                        return relation.lookup(trace.relationDeclaration2Global)
+                }
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend
new file mode 100644
index 00000000..39896c27
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend
@@ -0,0 +1,207 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEquals
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSReference
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+import org.eclipse.emf.ecore.util.EcoreUtil
+class Logic2AlloyLanguageMapper_Support {
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        
+        /// ID handling
+        def protected String toIDMultiple(String... ids) {
+                ids.map[it.split("\\s+").join("'")].join("'")
+        }
+        
+        def protected  String toID(String ids) {
+                ids.split("\\s+").join("'")
+        }
+        def protected  String toID(List<String> ids) {
+                ids.map[it.split("\\s+").join("'")].join("'")
+        }
+        
+        /// Support functions
+        
+        def protected getBooleanType(Logic2AlloyLanguageMapperTrace trace) {
+                if(trace.boolType!=null) {
+                        return trace.boolType
+                } else {
+                        trace.boolType = createALSEnumDeclaration => [
+                                it.name = toID(#["util","boolean"])
+                                trace.boolTrue = createALSEnumLiteral =>[it.name=toID(#["util","boolean","true"])]
+                                it.literal += trace.boolTrue
+                                trace.boolFalse = createALSEnumLiteral =>[it.name=toID(#["util","boolean","false"])]
+                                it.literal += trace.boolFalse
+                        ]
+                        trace.specification.enumDeclarations+=trace.boolType
+                        return trace.boolType
+                }
+        }
+        def protected getBooleanTrue(Logic2AlloyLanguageMapperTrace trace) {
+                getBooleanType(trace)
+                return trace.boolTrue   
+        }
+        def protected getBooleanFalse(Logic2AlloyLanguageMapperTrace trace) {
+                getBooleanType(trace)
+                return trace.boolFalse
+        }
+        
+        def protected booleanToLogicValue(ALSTerm boolReference, Logic2AlloyLanguageMapperTrace trace) {
+                //println((boolReference as ALSReference).referred)
+                createALSEquals => [
+                        leftOperand = EcoreUtil.copy(boolReference)
+                        rightOperand = createALSReference => [referred = getBooleanTrue(trace)]
+                ]
+        }
+        def protected booleanToEnumValue(ALSTerm value, Logic2AlloyLanguageMapperTrace trace) {
+                if(value instanceof ALSEquals) {
+                        val rightOperand = value.rightOperand
+                        if(rightOperand instanceof ALSReference) {
+                                if(rightOperand.referred == getBooleanTrue(trace)) {
+                                        return value.leftOperand
+                                }
+                        }
+                }
+                return value;
+        }
+        def protected prepareParameterOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) {
+                if(type instanceof BoolTypeReference) {
+                        return booleanToEnumValue(term,trace)
+                }
+                else return term
+        }
+        def protected postprocessResultOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) {
+                if(type instanceof BoolTypeReference) {
+                        return booleanToLogicValue(term,trace)
+                }
+                else return term
+        }
+         
+        def protected ALSTerm unfoldAnd(List<? extends ALSTerm> operands) {
+                if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSAnd=>[
+                        leftOperand=operands.head
+                        rightOperand=operands.subList(1,operands.size).unfoldAnd
+                ]}
+                else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        def protected ALSTerm unfoldOr(List<? extends ALSTerm> operands, Logic2AlloyLanguageMapperTrace trace) {
+                if(operands.size == 0) { return unfoldTrueStatement(trace)}
+                else if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSOr=>[
+                        leftOperand=operands.head
+                        rightOperand=unfoldOr(operands.subList(1,operands.size),trace)
+                ]}
+                //else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        protected def unfoldTrueStatement(Logic2AlloyLanguageMapperTrace trace) {
+                createALSEquals => [
+                                it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                                it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                        ]
+        }
+        
+        protected def unfoldTFalseStatement(Logic2AlloyLanguageMapper m, Logic2AlloyLanguageMapperTrace trace) {
+                createALSEquals => [
+                                it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                                it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)]
+                        ]
+        }
+        
+        def protected ALSTerm unfoldPlus(List<? extends ALSTerm> operands) {
+                if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSPlus=>[
+                        leftOperand=operands.head
+                        rightOperand=operands.subList(1,operands.size).unfoldPlus
+                ]}
+                else return createALSNone
+        }
+        
+        def protected ALSTerm unfoldIntersection(List<? extends ALSTerm> operands) {
+                if(operands.size == 1) { return operands.head }
+                else if(operands.size > 1) { return createALSIntersection=>[
+                        leftOperand=operands.head
+                        rightOperand=operands.subList(1,operands.size).unfoldIntersection
+                ]}
+                else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        def protected ALSTerm unfoldDistinctTerms(Logic2AlloyLanguageMapper m, List<Term> operands, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) }
+                else if(operands.size > 1) {
+                        val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2)
+                        for(i:0..<operands.size) {
+                                for(j: i+1..<operands.size) {
+                                        notEquals+=createALSNotEquals=>[
+                                                leftOperand = m.transformTerm(operands.get(i),trace,variables)
+                                                rightOperand = m.transformTerm(operands.get(j),trace,variables)
+                                        ]
+                                }
+                        }
+                        return notEquals.unfoldAnd
+                 }
+                else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+        }
+        
+        def protected ALSTerm unfoldReferenceDirectProduct(Logic2AlloyLanguageMapper m, List<TypeReference> references,Logic2AlloyLanguageMapperTrace trace) {
+                if(references.size == 1) return m.transformTypeReference(references.head,trace)
+                else if(references.size > 1) return createALSDirectProduct => [
+                        it.leftOperand = m.transformTypeReference(references.head,trace)
+                        it.rightOperand = unfoldReferenceDirectProduct(m,references.subList(1,references.size),trace)
+                ]
+                else throw new UnsupportedOperationException
+        }
+        
+        def protected ALSTerm unfoldDotJoin(Logic2AlloyLanguageMapper m, List<Term> elements, ALSTerm target, Logic2AlloyLanguageMapperTrace trace,
+                Map<Variable, ALSVariableDeclaration> variables) {
+                if (elements.size == 1) {
+                        return createALSJoin => [
+                                it.leftOperand = m.transformTerm(elements.head,trace, variables)
+                                it.rightOperand = target
+                        ]
+                } else if (elements.size > 1) {
+                        return createALSJoin => [
+                                it.leftOperand = m.transformTerm(elements.last,trace, variables)
+                                it.rightOperand = m.unfoldDotJoin(elements.subList(0, elements.size - 1), target, trace, variables)
+                        ]
+                } else
+                        throw new UnsupportedOperationException
+        }
+        
+        def protected ALSTerm unfoldTermDirectProduct(Logic2AlloyLanguageMapper m, List<Term> references,Logic2AlloyLanguageMapperTrace trace,Map<Variable, ALSVariableDeclaration> variables) {
+                if(references.size == 1) return m.transformTerm(references.head,trace,variables)
+                else if(references.size > 1) return createALSDirectProduct => [
+                        it.leftOperand = m.transformTerm(references.head,trace,variables)
+                        it.rightOperand = unfoldTermDirectProduct(m,references.subList(1,references.size),trace, variables)
+                ]
+                else throw new UnsupportedOperationException
+        }
+        
+        def protected createQuantifiedExpression(Logic2AlloyLanguageMapper m, QuantifiedExpression q, ALSMultiplicity multiplicity, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
+                val variableMap = q.quantifiedVariables.toInvertedMap[v | createALSVariableDeclaration=> [
+                                it.name = toID(v.name)
+                                it.range = m.transformTypeReference(v.range,trace) ]]
+                        
+                createALSQuantifiedEx=>[
+                        it.type = multiplicity
+                        it.variables += variableMap.values
+                        it.expression = m.transformTerm(q.expression,trace,variables.withAddition(variableMap))
+                ]
+        }
+        
+        def protected withAddition(Map<Variable, ALSVariableDeclaration> v1, Map<Variable, ALSVariableDeclaration> v2) { new HashMap(v1) => [putAll(v2)] }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend
new file mode 100644
index 00000000..9927f1cc
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend
@@ -0,0 +1,16 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import java.util.Collection
+import java.util.List
+interface Logic2AlloyLanguageMapper_TypeMapper {
+        def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace);
+        def List<ALSSignatureDeclaration> transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace)
+        def ALSSignatureDeclaration getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace)
+        def int getUndefinedSupertypeScope(int undefinedScope,Logic2AlloyLanguageMapperTrace trace)
+        def ALSTerm transformReference(DefinedElement referred,Logic2AlloyLanguageMapperTrace trace)
+}
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
new file mode 100644
index 00000000..ade9860b
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -0,0 +1,268 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+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.logicproblem.LogicproblemPackage
+import java.util.ArrayList
+import java.util.Collection
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
+        implements Logic2AlloyLanguageMapper_TypeMapperTrace
+{
+        public var ALSSignatureDeclaration objectSupperClass;
+        public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap;
+        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
+}
+/**
+ * Each object is an element of an Object set, and types are subsets of the objects.
+ */
+class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyLanguageMapper_TypeMapper{
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        
+        new() {
+                // Initialize package
+                LogicproblemPackage.eINSTANCE.class
+        }
+        
+        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
+                trace.typeMapperTrace = typeTrace
+                
+                // 1. A global type for Objects is created
+                val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])]
+                val objectBody = createALSSignatureBody => [
+                        it.declarations += objectSig
+                        it.abstract = true
+                ]
+                typeTrace.objectSupperClass = objectSig
+                trace.specification.signatureBodies += objectBody
+                
+                // 2. Each type is mapped to a unique sig
+                for(type : types) {
+                        val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)]
+                        val body = createALSSignatureBody => [it.declarations += sig]
+                        trace.specification.signatureBodies += body
+                        typeTrace.type2ALSType.put(type,sig)
+                }
+                
+                // 3. The elements of a defined type is mapped to singleton signatures
+                // 3.1 Collect the elements
+                val elementMatcher = TypeQueries.instance.getLowestCommonSupertypeOfAllOccuranceOfElement(trace.incqueryEngine)
+                val topmostType2Elements = new HashMap<ALSSignatureDeclaration,List<DefinedElement>>
+                for(element : elements) {
+                        val topmostTypes = elementMatcher.getAllValuesOftype(element)
+                        var ALSSignatureDeclaration selectedTopmostType;
+                        if(topmostTypes.empty) {
+                                selectedTopmostType = objectSig
+                        } else{
+                                selectedTopmostType = topmostTypes.head.lookup(typeTrace.type2ALSType)
+                        }
+                        topmostType2Elements.putOrAddToList(selectedTopmostType,element)
+                }
+                
+                // 4. For each topmost types several singleton classes are generated, which represents the elements.
+                // For the sake of clarity, common bodies are used.
+                for(topmostEntry : topmostType2Elements.entrySet) {
+                        
+                        for(element : topmostEntry.value) {
+                                val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]
+                                typeTrace.definedElement2Declaration.put(element,signature)
+                        }
+                        
+                        val body = createALSSignatureBody => [
+                                it.multiplicity = ALSMultiplicity.ONE
+                                it.declarations += topmostEntry.value.map[it.lookup(typeTrace.definedElement2Declaration)]
+                        ]
+                        
+                        val containerLogicType = topmostEntry.key
+                        body.superset += containerLogicType
+                        
+                        trace.specification.signatureBodies+=body
+                }
+                
+                // 5.1 Each Defined Type is specified as the union of its elements
+                for(definedType : types.filter(TypeDefinition)) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("typedefinition",definedType.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [ it.referred = definedType.lookup(typeTrace.type2ALSType) ]
+                                        it.rightOperand = support.unfoldPlus(definedType.elements.map[e|
+                                                createALSReference => [it.referred = e.lookup(typeTrace.definedElement2Declaration)]])
+                                ]
+                        ]
+                }
+                // 5.2 Each Defined Element is unique
+                for(definedType : types.filter(TypeDefinition)) {
+                        val allElementsIncludingSubtypes = 
+                                definedType.<Type>transitiveClosureStar[it.subtypes].filter(TypeDefinition)
+                                        .map[elements].flatten.toSet.toList
+                        if(allElementsIncludingSubtypes.size>=2) {
+                                trace.specification.factDeclarations += createALSFactDeclaration => [
+                                        it.name = support.toIDMultiple("typeElementsUnique",definedType.name)
+                                        it.term = unfoldDistinctElements(allElementsIncludingSubtypes,trace)
+                                ]
+                        }
+                }
+                
+                // 6. Each inheritance is modeled by subset operator 'in'
+                for(type : types) {
+                        val sigBody = type.lookup(typeTrace.type2ALSType).eContainer as ALSSignatureBody
+                        if(type.supertypes.empty)  {
+                                sigBody.superset += typeTrace.objectSupperClass
+                        } else {
+                                sigBody.superset += type.supertypes.map[lookup(typeTrace.type2ALSType)]
+                        }
+                }
+                
+                
+                // 7. Each type is in the intersection of the supertypes
+                for(type : types.filter[it.supertypes.size>=2]) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("abstract",type.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
+                                        it.rightOperand = support.unfoldIntersection(type.supertypes.map[e|
+                                                createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
+                                ]
+                        ]
+                }
+                
+                // 8. Each abstract type is equal to the union of the subtypes
+                for(type : types.filter[isIsAbstract]) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("abstract",type.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
+                                        it.rightOperand = support.unfoldPlus(type.subtypes.map[e|
+                                                createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
+                                ]
+                        ]
+                }
+                // 8.1 The object type is the union of the root types.
+                val rootTypes = types.filter[it.supertypes.empty].toList
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toIDMultiple(#["ObjectTypeDefinition"])
+                        it.term = createALSEquals => [
+                                it.leftOperand = createALSReference => [ it.referred = typeTrace.objectSupperClass ]
+                                it.rightOperand = support.unfoldPlus(rootTypes.map[e|
+                                        createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
+                        ]
+                ]
+                
+                // 9. For each type X (including Object)
+                //    only the common subtypes are in the intersection
+                //    of the two subtype.
+                // 9.1. for the object
+                {
+                        val rootTypeList = types.filter[it.supertypes.empty].toList
+                        for(type1Index: 0..<rootTypeList.size) {
+                                for(type2Index: 0..<type1Index) {
+                                        trace.specification.factDeclarations += 
+                                                commonSubtypeOnlyInDiamonds(rootTypeList.get(type1Index),rootTypeList.get(type2Index),trace)
+                                }
+                        }
+                }
+                
+                //9.3 for the subtypes of each objects
+                {
+                        for(inScope : types) {
+                                val subtypeList = inScope.subtypes//.toList
+                                if(subtypeList.size>=2) {
+                                        for(type1Index: 0..<subtypeList.size) {
+                                                for(type2Index: 0..<type1Index) {
+                                                        trace.specification.factDeclarations += 
+                                                                commonSubtypeOnlyInDiamonds(subtypeList.get(type1Index),subtypeList.get(type2Index),trace)
+                                                }
+                                        }
+                                }
+                        }
+                }
+        }
+        
+        private def isEnumlikeType(Type type) {
+                if(type instanceof TypeDefinition) {
+                        val elements = type.elements
+                        return elements.forall[it.definedInType.size === 1 && it.definedInType.head === type]
+                }
+                return false
+        }
+        
+        private def isEnumlikeElement(DefinedElement d) {
+                d.definedInType.size === 1 && d.definedInType.head.isEnumlikeType 
+        }
+        
+        def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
+                val res = trace.typeMapperTrace
+                if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes) {
+                        return res
+                } else {
+                        throw new IllegalArgumentException('''
+                        Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name»,
+                        but found «res.class.name»''')
+                }
+        }
+        
+        def private commonSubtypeOnlyInDiamonds(Type t1, Type t2, Logic2AlloyLanguageMapperTrace trace) {
+                val topmostCommonSubtypes = TypeQueries.instance.getTopmostCommonSubtypes(trace.incqueryEngine)
+                val allTopmostCommon = topmostCommonSubtypes.getAllValuesOfcommon(t1,t2).toList
+                return createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("common","types",t1.name,t2.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSIntersection => [
+                                                it.leftOperand = createALSReference => [it.referred = t1.lookup(trace.typeTrace.type2ALSType)]
+                                                it.rightOperand = createALSReference => [it.referred = t2.lookup(trace.typeTrace.type2ALSType)]
+                                        ]
+                                        it.rightOperand = support.unfoldPlus(allTopmostCommon.map[t|createALSReference => [it.referred = t.lookup(trace.typeTrace.type2ALSType)]])
+                                ]
+                        ]
+        }
+        
+        def private unfoldDistinctElements(
+                List<DefinedElement> operands,
+                Logic2AlloyLanguageMapperTrace trace
+        ) {
+                if(operands.size == 1 || operands.size == 0) {support.unfoldTrueStatement(trace);}
+                else {
+                        val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2)
+                        for(i:0..<operands.size) {
+                                for(j: i+1..<operands.size) {
+                                        notEquals+=createALSNotEquals=>[
+                                                leftOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(i)) ]
+                                                rightOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(j)) ]
+                                        ]
+                                }
+                        }
+                        return support.unfoldAnd(notEquals)
+                }
+        }
+        
+        override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                return #[trace.typeTrace.type2ALSType.get(referred)]
+        }
+        
+        override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) {
+                trace.typeTrace.objectSupperClass
+        }
+        
+        override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
+                createALSReference => [it.referred = referred.lookup(trace.typeTrace.definedElement2Declaration)]
+        }
+        
+        override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {
+                return undefinedScope + trace.typeTrace.definedElement2Declaration.size
+        }
+        
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old
new file mode 100644
index 00000000..7383904d
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old
@@ -0,0 +1,428 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSIntersection
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+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.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher
+import java.util.HashMap
+import java.util.LinkedHashSet
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.viatra.query.runtime.emf.EMFScope
+import org.eclipse.xtend.lib.annotations.Data
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal
+        implements Logic2AlloyLanguageMapper_TypeMapperTrace {
+        public var ALSSignatureDeclaration declaredSupertype
+        public var ALSSignatureDeclaration definedSupertype
+        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
+        
+        public val Map<TypeDefinition,  ALSSignatureDeclaration> definition2definition = new HashMap
+        public val Map<TypeDeclaration, ALSSignatureDeclaration> declaration2definition = new HashMap
+        public val Map<TypeDeclaration, ALSSignatureDeclaration> undefined2definition = new HashMap
+        public val Map<TypeDeclaration, ALSSignatureDeclaration> new2declaration = new HashMap
+        
+        def getAllDefinedTypes() {
+                return (definition2definition.values) +
+                       (declaration2definition.values) +
+                       (undefined2definition.values)
+        }
+        def getAllDeclaredTypes() {
+                return new2declaration.values
+        }
+        
+        public val Map<Type,List<ALSSignatureDeclaration>> type2AllSignatures = new HashMap;
+}
+@Data
+class DynamicTypeConstraints {
+        List<List<Type>> positiveCNF
+        LinkedHashSet<Type> negative
+        public new() {
+                this.positiveCNF = new LinkedList
+                this.negative = new LinkedHashSet
+        }
+        def public void addPositiveTypeOptions(List<Type> typeDisjunction) {
+                this.positiveCNF.add(typeDisjunction)
+        }
+        def public void addNegativeTypes(Iterable<Type> negativeTypes) {
+                this.negative.addAll(negativeTypes)
+        }
+}
+/**
+ * Dynamic types are represented by disjoint sets, and 
+ * static types are represented by the union of the dynamic type sets.
+ * 
+ * Definition                         Declaration
+ *     |                              /         \
+ *     |                  W/DefinedSuper       Wo/DefinedSuper
+ *     |                     |                  /           \
+ *     |                     |      undefined2declaration  new2declaration
+ * definition2definition  definition2declaration
+ * +----------------------------------------------------+  +-------------+
+ *        Defined                                              Declared
+ */
+class Logic2AlloyLanguageMapper_TypeMapper_Horizontal implements Logic2AlloyLanguageMapper_TypeMapper{
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        
+        override transformTypes(LogicProblem problem, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                // 0. Creating the traces
+                val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal
+                trace.typeMapperTrace = typeTrace
+                /**
+                 * Static type -> list of possible dynamic type map
+                 */
+                val typeToConcreteSubtypes = problem.typeToConcreteSubtypes(trace)
+                
+                
+                
+                // 1. Transforming the types
+                
+                // There are two kind of types:
+                // A: one with defined supertypes (including itself), that only has defined elements
+                // Those types can have instances only from the defined elements, ie they are subset of problem.elements
+                // B: one without defined supertypes 
+                // Those types can have instances from two sources
+                // B.1 from elements that dont have definitions
+                // B.2 from newly created elements
+                val allConcreteTypes = problem.types.filter[!it.isAbstract]
+                val definitions = allConcreteTypes.filter(TypeDefinition).toList
+                val declarationsWithDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[it.hasDefinedSupertype].toList
+                val declarationsWithoutDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[!it.hasDefinedSupertype].toList
+                
+                // 2. If there are defined elements
+                if(trace.typeTrace.definedSupertype != null) {
+                        // 3 mapping the elements
+                        problem.elements.transformDefinedSupertype(trace)
+                        // 4. if there are elements that are added to types, then it have to be mapped to defined parts
+                        if(problem.elements.exists[!it.definedInType.empty]) {
+                                definitions.forEach[it.transformDefinition2Definition(trace)]
+                                declarationsWithDefinedSupertype.forEach[it.transformDeclaration2Definition(trace)]
+                        }
+                        // 5. if there are elements that are not added to types, then it have to be mapped to declarations without definitions
+                        if(problem.elements.exists[it.definedInType.empty]) {
+                                declarationsWithoutDefinedSupertype.forEach[it.transformUndefined2Definition(trace)]
+                        }
+                        
+                        definedConcreteTypesAreFull(trace)
+                        definedConcreteTypesAreDisjoint(trace)
+                        problem.definedConcreteTypesAreSatisfyingDefinitions(typeToConcreteSubtypes,trace)
+                }
+                
+                // Transforming the declared and defined concrete types
+                problem.elements.transformDefinedSupertype(trace)
+                if(trace.typeTrace.definedSupertype != null) {
+                        problem.elements.transformDefinedElements(trace)
+                        declarationsWithoutDefinedSupertype.forEach[it.transformNew2Declaration(trace)]
+                }
+                
+                // 2: Caching the types by filling type2AllSignatures
+                for(typeToConcreteSubtypesEntry : typeToConcreteSubtypes.entrySet) {
+                        val type = typeToConcreteSubtypesEntry.key
+                        val List<ALSSignatureDeclaration> signatures = new LinkedList
+                        
+                }
+        }
+        
+        def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
+                val res = trace.typeMapperTrace
+                if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal) {
+                        return res
+                } else {
+                        throw new IllegalArgumentException('''
+                        Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal.name»,
+                        but found «res.class.name»''')
+                }
+        }
+        
+        private def boolean hasDefinedSupertype(Type type) {
+                if(type instanceof TypeDefinition) {
+                        return true
+                } else {
+                        if(type.supertypes.empty) return false
+                        else return type.supertypes.exists[it.hasDefinedSupertype]
+                }
+        }
+        
+        private def transformDefinedSupertype(List<DefinedElement> elements, Logic2AlloyLanguageMapperTrace trace) {
+                trace.typeTrace.definedSupertype = createALSSignatureDeclaration => [
+                        it.name = support.toID(#["util","defined","Object"])
+                ]
+                trace.specification.signatureBodies += createALSSignatureBody => [
+                        it.abstract = true
+                        it.declarations += trace.typeTrace.definedSupertype
+                ]
+        }
+        
+        private def transformDefinedElements(List<DefinedElement> elements,
+                Logic2AlloyLanguageMapperTrace trace){
+                if(trace.typeTrace.definedSupertype != null) {                  
+                        // 2. Create elements as singleton signatures subtype of definedSupertype
+                        val elementBodies = createALSSignatureBody => [
+                                it.multiplicity = ALSMultiplicity::ONE
+                                it.supertype = trace.typeTrace.definedSupertype
+                        ]
+                        trace.specification.signatureBodies += elementBodies
+                        for(element : elements) {
+                                val elementDeclaration = createALSSignatureDeclaration => [
+                                        it.name = support.toIDMultiple(#["element"],element.name)
+                                ]
+                                elementBodies.declarations += elementDeclaration
+                                trace.typeTrace.definedElement2Declaration.put(element,elementDeclaration)
+                        }
+                        // 3. Specify that definedSupertype is equal to the union of specified
+                        /*trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toID(#["util","typehierarchy","definitionOfElements"])
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype]
+                                        it.rightOperand = support.unfoldPlus(elements.map[element|createALSReference=>[
+                                                it.referred = element.lookup(trace.typeTrace.definedElement2Declaration)
+                                        ]])
+                                ]
+                        ]*/
+                }
+        }
+        
+        ///// Type definitions
+        
+        protected def void transformDefinition2Definition(TypeDefinition type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["definition2definition"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.superset += trace.typeTrace.definedSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.definition2definition.put(type,sig)
+        }
+        protected def void transformDeclaration2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaration2definition"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.superset += trace.typeTrace.definedSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.declaration2definition.put(type,sig)
+        }
+        protected def void transformUndefined2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["undefined2definition"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.supertype = trace.typeTrace.definedSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.undefined2definition.put(type,sig)
+        }
+        protected def void transformNew2Declaration(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaredPartOfDeclaration"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.supertype = trace.typeTrace.declaredSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.new2declaration.put(type,sig)
+        }
+        
+        /**
+         * The dynamic types cover each concrete types
+         */
+        protected def definedConcreteTypesAreFull(Logic2AlloyLanguageMapperTrace trace) {
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["util","typehierarchy","elementFull"])
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype]
+                                        it.rightOperand = support.unfoldPlus(
+                                                trace.typeTrace.allDefinedTypes.map[type|
+                                                        createALSReference=>[referred = type]
+                                                ].toList
+                                        )
+                                ]
+                ]
+                
+        }
+        /**
+         * The dynamic types are disjoint
+         */
+        protected def definedConcreteTypesAreDisjoint(Logic2AlloyLanguageMapperTrace trace) {
+                val types = trace.getTypeTrace.allDefinedTypes.toList
+                if (types.size >= 2) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toID(#["util", "typehierarchy", "elementFull"])
+                                it.term = types.disjointSets
+                        ]
+                }
+        }
+        /**
+         * The dynamic types are subtypes of the types where it is defined, but not subtypes where it is not
+         */
+        protected def definedConcreteTypesAreSatisfyingDefinitions(LogicProblem problem, Map<Type,List<Type>> typeToConcreteSubtypes, Logic2AlloyLanguageMapperTrace trace) {
+                val constraintOnElements = problem.elements.typeConstraints(typeToConcreteSubtypes)
+                for(constraintOnElement : constraintOnElements.entrySet) {
+                        val element = constraintOnElement.key
+                        val elementSignature = element.lookup(trace.typeTrace.definedElement2Declaration)
+                        val constraint = constraintOnElement.value
+                        
+                        var ALSTerm negativeConstraints;
+                        if(constraint.negative.isEmpty) {
+                                negativeConstraints = null
+                        } else {
+                                negativeConstraints = support.unfoldAnd(constraint.negative.map[type|
+                                        createALSNot=> [ elementInDefinedType(elementSignature, type, trace) ]
+                                ].toList)
+                        }
+                        
+                        var ALSTerm positiveTypeConstraints
+                        if(constraint.positiveCNF.isEmpty) {
+                                positiveTypeConstraints = null
+                        } else {
+                                positiveTypeConstraints = support.unfoldAnd(constraint.positiveCNF.map[ typeConstraintFromDefinition |
+                                        support.unfoldOr(typeConstraintFromDefinition.map[type |
+                                                elementInDefinedType(elementSignature,type,trace)
+                                        ].toList,trace)
+                                ])
+                        }
+                        
+                        var ALSTerm typeConstraint
+                        if(negativeConstraints != null && positiveTypeConstraints == null) {
+                                typeConstraint = negativeConstraints
+                        } else if (negativeConstraints == null && positiveTypeConstraints != null) {
+                                typeConstraint = positiveTypeConstraints
+                        } else if (negativeConstraints != null && positiveTypeConstraints != null) {
+                                val and = createALSAnd
+                                and.leftOperand = positiveTypeConstraints
+                                and.rightOperand = negativeConstraints
+                                typeConstraint = and
+                        } else {
+                                typeConstraint = null
+                        }
+                        
+                        if(typeConstraint != null) {
+                                val fact =  createALSFactDeclaration => [
+                                        name = support.toIDMultiple(#["util","typehierarchy","definition"],element.name)
+                                ]
+                                fact.term = typeConstraint
+                                trace.specification.factDeclarations +=fact
+                        }
+                        // otherwise there is no type constraint on element
+                }
+        }
+        
+        private def elementInDefinedType(
+                ALSSignatureDeclaration elementSignature,
+                Type type,
+                Logic2AlloyLanguageMapperTrace trace)
+        {
+                var ALSSignatureDeclaration signature
+                if(type instanceof TypeDeclaration) {
+                        if(trace.typeTrace.declaration2definition.containsKey(type)) {
+                                signature = type.lookup(trace.typeTrace.declaration2definition)
+                        } else if(trace.typeTrace.undefined2definition.containsKey(type)) {
+                                signature = type.lookup(trace.typeTrace.undefined2definition)
+                        } else {
+                                return null
+                        }
+                } else if(type instanceof TypeDefinition) {
+                        if(trace.typeTrace.definition2definition.containsKey(type)) {
+                                signature = type.lookup(trace.typeTrace.definition2definition)
+                        } else {
+                                return null
+                        }
+                } else throw new IllegalArgumentException('''Unknownt type «type.class.name»''')
+                
+                val finalSignature = signature
+                return createALSSubset => [
+                        leftOperand = createALSReference => [
+                                referred = elementSignature
+                        ]
+                        rightOperand = createALSReference => [
+                                referred = finalSignature
+                        ]
+                ]
+        }
+        
+        def private typeToConcreteSubtypes(LogicProblem problem, Logic2AlloyLanguageMapperTrace trace) {
+                if(trace.incqueryEngine == null) {
+                        trace.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem))
+                }
+                val matcher = SupertypeStarMatcher.on(trace.incqueryEngine)
+                val Map<Type,List<Type>> typeToConcreteSubtypes = new HashMap
+                for(supertype : problem.types) {
+                        typeToConcreteSubtypes.put(
+                                supertype,
+                                matcher.getAllValuesOfsubtype(supertype)
+                                        .filter[!it.isIsAbstract].toList)
+                }
+                return typeToConcreteSubtypes
+        }
+        
+        /**
+         * Gives type constraints in a form of CNF 
+         */
+        def private Map<DefinedElement,DynamicTypeConstraints> typeConstraints(List<DefinedElement> elements, Map<Type,List<Type>> typeToConcreteSubtypes) {
+                val Map<DefinedElement,DynamicTypeConstraints> constraints = new HashMap
+                elements.forEach[constraints.put(it,new DynamicTypeConstraints)]
+                
+                for(type : typeToConcreteSubtypes.keySet.filter(TypeDefinition)) {
+                        val subtypes = type.lookup(typeToConcreteSubtypes)
+                        for(elementInType:type.elements) {
+                                elementInType.lookup(constraints).addPositiveTypeOptions(subtypes)
+                        }
+                        for(elementNotInType:elements.filter[!type.elements.contains(it)]) {
+                                elementNotInType.lookup(constraints).addNegativeTypes(subtypes)
+                        }
+                }
+                
+                return constraints
+        }
+        
+        private def ALSTerm disjointSets(List<ALSSignatureDeclaration> signatures) {
+                if(signatures.size >= 2){
+                        val top = createALSEquals => [
+                                it.leftOperand = signatures.intersectionOfTypes
+                                it.rightOperand = createALSNone
+                        ]
+                        if(signatures.size > 2) {
+                                return createALSAnd => [
+                                        it.leftOperand = top
+                                        it.rightOperand = signatures.subList(1,signatures.size).disjointSets
+                                ]
+                        } else{
+                                return top
+                        }
+                } else {
+                        throw new UnsupportedOperationException()
+                }
+        }
+        
+        private def ALSIntersection intersectionOfTypes(List<ALSSignatureDeclaration> signatures) {
+                if(signatures.size == 2) {
+                        return createALSIntersection => [
+                                leftOperand = createALSReference => [it.referred = signatures.get(0)]
+                                rightOperand = createALSReference => [it.referred = signatures.get(1)]
+                        ]
+                } else if(signatures.size > 2) {
+                        return createALSIntersection => [
+                                leftOperand = createALSReference => [it.referred = signatures.get(0)]
+                                rightOperand = signatures.subList(1,signatures.size).intersectionOfTypes
+                        ]
+                } else throw new UnsupportedOperationException()
+        }
+        
+        
+        override transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                //trace.typeTrace.
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend
new file mode 100644
index 00000000..6533ad36
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend
@@ -0,0 +1,50 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+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.logicproblem.LogicProblem
+import java.util.HashMap
+import java.util.Map
+import java.util.Collection
+class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace {
+        val Map<TypeDeclaration,ALSSignatureDeclaration> newElementTypes = new HashMap
+        val Map<Type,ALSSignatureDeclaration> definedElementTypes = new HashMap
+        var ALSSignatureDeclaration undefinedSupertype
+        var ALSSignatureDeclaration definedSupertype
+}
+class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{
+        
+        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        private def boolean hasDefinedSupertype(Type type) {
+                if(type instanceof TypeDefinition) {
+                        return true
+                } else {
+                        if(type.supertypes.empty) return false
+                        else return type.supertypes.exists[it.hasDefinedSupertype]
+                }
+        }       
+        
+        override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+}
+\ 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 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu
parent	Initial commit, migrating from SVN (diff)
download	VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip