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/unused
parent: Initial commit, migrating from SVN (diff)
download: VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
4 files changed, 671 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_
new file mode 100644
index 00000000..05b97b0c
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_
@@ -0,0 +1,212 @@
+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.*
+class AlloyModelInterpretation implements LogicModelInterpretation{
+        
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        //protected val extension LogicProblemBuilder builder = new LogicProblemBuilder
+        
+        protected val Logic2AlloyLanguageMapper forwardMapper
+        protected val Logic2AlloyLanguageMapperTrace forwardTrace;
+        
+        private var ExprVar logicLanguage;
+        private var String logicBooleanTrue;
+        private var String logicBooleanFalse;
+                
+        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 (A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) {
+                
+                this.forwardMapper = forwardMapper
+                this.forwardTrace = trace
+                
+                //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: solution.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
+                        } else if(sigName2LogicType.containsKey(typeName) && typeName.lookup(sigName2LogicType) instanceof TypeDefinition) {
+                                val element = elementNameNamel2DefinedElement.get(atomName.head)
+                                alloyAtom2LogicElement.put(atom.label,element)
+                        } else 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 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 throw new UnsupportedOperationException('''Unknown atom: «atom»''')
+                }
+                
+                //TMP field maps
+                val Map<String, Field> name2AlloyField = new HashMap
+                // exploring signatures
+                for(sig:solution.allReachableSigs) {
+                        for(field : sig.fields) {
+                                name2AlloyField.put(field.label,field)
+                        }
+                }
+                
+                // 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
+        }
+        
+        def print() {
+                println('''Elements-----''')
+                interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v»''')]
+                
+                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»)''')]]
+        }
+        
+        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("\\$") }
+        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 isNumber(String s) {
+                try{
+                        Integer.parseInt(s)
+                        return true
+                }catch(NumberFormatException e) {
+                        return false
+                }
+        }
+}
+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/unused/FunctionWithTimeout.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_
new file mode 100644
index 00000000..8c03af6e
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_
@@ -0,0 +1,40 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import org.eclipse.xtext.xbase.lib.Functions.Function0
+import java.util.concurrent.Executors
+import java.util.concurrent.Callable
+import java.util.concurrent.TimeUnit
+import java.util.concurrent.TimeoutException
+import java.util.concurrent.ExecutionException
+class FunctionWithTimeout<Type> {
+        val Function0<Type> function;
+        
+        new(Function0<Type> function) {
+                this.function = function
+        }
+        
+        def execute(long millisecs) {
+                if(millisecs>0) {
+                        val executor = Executors.newCachedThreadPool();
+                        val task = new Callable<Type>() {
+                           override Type call() { function.apply }
+                        };
+                        val future = executor.submit(task);
+                        try {
+                           val result = future.get(millisecs, TimeUnit.MILLISECONDS);
+                           return result
+                        } catch (TimeoutException ex) {
+                           // handle the timeout
+                        } catch (InterruptedException e) {
+                           // handle the interrupts
+                        } catch (ExecutionException e) {
+                           // handle other exceptions
+                        } finally {
+                           future.cancel(true); // may or may not desire this
+                        }
+                        return null
+                }
+                else return function.apply
+        }       
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_
new file mode 100644
index 00000000..29acd681
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_
@@ -0,0 +1,345 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import java.util.Map
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import java.util.List
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant
+import edu.mit.csail.sdg.alloy4compiler.ast.Expr
+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.IntLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
+import java.util.HashMap
+import edu.mit.csail.sdg.alloy4compiler.ast.Decl
+import java.util.ArrayList
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import edu.mit.csail.sdg.alloy4compiler.ast.Attr
+import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import javax.naming.OperationNotSupportedException
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.AlloySpecification
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.Multiplicity
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.InverseReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+class AlloyInput{
+        public val List<PrimSig> typeDeclarations=new ArrayList
+        public val List<Expr> functionDeclarations=new ArrayList
+        public val List<Expr> assertions=new ArrayList
+        public val List<Expr> multiplicityConstraints=new ArrayList
+        public val List<Expr> inverseConstraints=new ArrayList
+}
+class Logic2AlloyApiMapperTrace {
+        val Map<Type, PrimSig> typeMap
+        val Map<DefinedElement, PrimSig> elementMap
+        //val Map<Function, SMTFunctionDeclaration> functionMap
+        val Map<Relation,Expr> relationMap
+        //val Map<Constant,SMTFunctionDeclaration> constantMap
+        
+        new () {
+                this.typeMap = new HashMap
+                this.elementMap = new HashMap
+                //this.functionMap = new HashMap
+                this.relationMap = new HashMap
+                //this.constantMap = new HashMap
+        }
+        new (Map<Type, PrimSig> typeMap,
+                 Map<DefinedElement, PrimSig> elementMap,
+                 //Map<Function, SMTFunctionDeclaration> functionMap,
+                 Map<Relation,Expr> relationMap/*,
+                 Map<Constant,SMTFunctionDeclaration> constantMap*/)
+        {
+                this.typeMap = typeMap
+                this.elementMap = elementMap
+                //this.functionMap = functionMap
+                this.relationMap = relationMap
+                //this.constantMap = constantMap
+        }
+        
+        def types() { typeMap }
+        def elements() { elementMap }
+        //def functions() { functionMap }
+        def relations() { relationMap }
+        //def constants() { constantMap }
+}
+class Logic2AlloyApiMapper{
+        //TODO output
+        public def TracedOutput<List<PrimSig>, Logic2AlloyApiMapperTrace> transformProblem(LogicProblem problem) {
+                val documentInput = new AlloyInput()
+                //createSMTInput => [satCommand = createSMTSimpleSatCommand getModelCommand = createSMTGetModelCommand]
+                //val document = createSMTDocument => [input = documentInput]
+                val List<PrimSig> document=new ArrayList
+                val trace = new Logic2AlloyApiMapperTrace
+                
+                // Trafo
+                documentInput.typeDeclarations          += problem.types.map[transformType(trace)]
+                //documentInput.functionDeclarations    += problem.functions.map[transformFunction(trace)]
+                documentInput.functionDeclarations      += problem.relations.map[transformRelation(trace)]
+                //documentInput.functionDeclarations    += problem.constants.map[transformConstant(trace)]
+                documentInput.assertions                        += problem.assertions.map[transformAssertion(trace)]
+                
+                
+                val alloySpecification = problem.specifications.filter(AlloySpecification).head
+                
+                for(mult: alloySpecification.multiplicities){
+                        if(mult.min>0){
+                                documentInput.multiplicityConstraints+=mult.transformMultiplicityLowerBound(trace)
+                        }
+                        if(mult.max!=-1){
+                                documentInput.multiplicityConstraints+=mult.transformMultiplicityUpperBound(trace)
+                        }
+                }
+                
+                for(inv: alloySpecification.inverses){
+                        documentInput.inverseConstraints += inv.transformInverse(trace)
+                }
+                // End trafo
+                
+                return new TracedOutput(document,trace)
+        }
+        
+        def Expr transformMultiplicityLowerBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){
+                
+                val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl
+                return (forallVariable.get.cardinality.gte(ExprConstant.makeNUMBER(multiplicity.min))).forAll(forallVariable)
+                
+        }
+        
+        def Expr transformMultiplicityUpperBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){
+                
+                val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl
+                return (forallVariable.get.cardinality.lte(ExprConstant.makeNUMBER(multiplicity.max))).forAll(forallVariable)
+                
+        }
+        
+        def Expr transformInverse(InverseReference inverse, Logic2AlloyApiMapperTrace trace){
+                return trace.relations.get(inverse.inverseOf.get(0)).equal(trace.relations.get(inverse.inverseOf.get(1)).transpose)     
+        }
+        
+        private def toID(List<String> names) {names.join("!") }
+        
+        def dispatch protected transformType(TypeDefinition declaration, Logic2AlloyApiMapperTrace trace) {
+                val result = new PrimSig(declaration.name.toID, Attr.ABSTRACT)
+                trace.types.put(declaration,result)
+                return result
+        }
+        
+        def protected transformDefinedElement(TypeDefinition enumType, DefinedElement element, Logic2AlloyApiMapperTrace trace) {
+                val result=new PrimSig(element.name.toID, trace.types.get(enumType), Attr.ONE)
+                trace.elements.put(element,result)
+                return result
+        }
+                
+        def dispatch protected transformType(TypeDeclaration declaration, Logic2AlloyApiMapperTrace trace) {
+                //TODO �r�kles, absztrakt
+                val result = new PrimSig(declaration.name.toID)
+                trace.types.put(declaration,result)
+                return result
+        }
+        
+        def dispatch protected transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyApiMapperTrace trace) {
+                throw new UnsupportedOperationException("BoolTypeReference is not supported.")
+        }
+        def dispatch protected transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyApiMapperTrace trace) {
+                return PrimSig.SIGINT
+        }
+        def dispatch protected transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyApiMapperTrace trace) {
+                throw new UnsupportedOperationException("RealTypeReference is not supported.")
+        }
+        def dispatch protected PrimSig transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyApiMapperTrace trace) {
+                return trace.types.get(complexTypeReference.referred)
+        }
+        
+        /*def protected transformFunction(Function declaration, Logic2AlloyApiMapperTrace trace) {
+                val functionDeclaration = createSMTFunctionDeclaration => [
+                        name = declaration.name.toID
+                        range = declaration.range.transformTypeReference(trace)
+                        parameters+= declaration.parameters.map[transformTypeReference(trace)]
+                ]
+                trace.functions.put(declaration,functionDeclaration)
+                return functionDeclaration
+        }*/
+        
+        def transformRelation(Relation relation, Logic2AlloyApiMapperTrace trace) {
+                if(relation.parameters.size==2){
+                        trace.relations.put(relation,(relation.parameters.get(0).transformTypeReference(trace) as PrimSig).addField(relation.name.toID, (relation.parameters.get(1).transformTypeReference(trace) as PrimSig).setOf))
+                } else{
+                        throw new OperationNotSupportedException("More parameters are not supported.")
+                } 
+        }
+        
+        /*def transformConstant(Constant constant, Logic2AlloyApiMapperTrace trace) {
+                val smtConstant = createSMTFunctionDeclaration => [
+                        name = constant.name.toID
+                        range = transformTypeReference(constant.type, trace)
+                ]
+                trace.constants.put(constant,smtConstant)
+                return smtConstant
+        }*/
+        
+        def protected Expr transformAssertion(Assertion assertion, Logic2AlloyApiMapperTrace trace) {
+                
+                return assertion.value.transformTerm(trace,emptyMap)
+        }
+        
+        def dispatch protected Expr transformTerm(BoolLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                throw new UnsupportedOperationException("Bool is not supported")
+                //open util/boolean, autoPay: Bool
+                //https://code.google.com/p/valloy2009/source/browse/trunk/src/models/util/boolean.als?r=142
+        }
+        def dispatch protected Expr transformTerm(IntLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)  {
+                return ExprConstant.makeNUMBER(literal.value)
+        }
+        def dispatch protected Expr transformTerm(RealLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                throw new UnsupportedOperationException("Real number is not supported")
+        }
+        def dispatch protected Expr transformTerm(Not not, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return not.operand.transformTerm(trace,variables).not}
+        def dispatch protected Expr transformTerm(And and, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                val List<Expr> operands= and.operands.map[transformTerm(trace,variables)]
+                var andTerm=operands.get(0)
+                for(Integer i: 1..(operands.size-1)){
+                        andTerm=andTerm.and(operands.get(i))
+                }
+                return andTerm
+        }
+        def dispatch protected Expr transformTerm(Or or, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                val List<Expr> operands= or.operands.map[transformTerm(trace,variables)]
+                var orTerm=operands.get(0)
+                for(Integer i: 1..(operands.size-1)){
+                        orTerm=orTerm.or(operands.get(i))
+                }
+                return orTerm
+        }
+        def dispatch protected Expr transformTerm(Impl impl, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return impl.leftOperand.transformTerm(trace,variables).implies(impl.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Iff ifExpression, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return ifExpression.leftOperand.transformTerm(trace,variables).iff(ifExpression.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(MoreThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return moreThan.leftOperand.transformTerm(trace,variables).gt(moreThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(LessThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return lessThan.leftOperand.transformTerm(trace,variables).lt(lessThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(MoreOrEqualThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return moreThan.leftOperand.transformTerm(trace,variables).gte(moreThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(LessOrEqualThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return lessThan.leftOperand.transformTerm(trace,variables).lte(lessThan.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Equals equals, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return equals.leftOperand.transformTerm(trace,variables).equal(equals.rightOperand.transformTerm(trace,variables))
+        }
+        /*def dispatch protected Expr transformTerm(Distinct distinct, Logic2AlloyApiMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
+                createSMTDistinct => [ operands += distinct.operands.map[transformTerm(trace,variables)]]}*/
+        def dispatch protected Expr transformTerm(Plus plus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return plus.leftOperand.transformTerm(trace,variables).plus(plus.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Minus minus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return minus.leftOperand.transformTerm(trace,variables).minus(minus.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Multiply multiply, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return multiply.leftOperand.transformTerm(trace,variables).mul(multiply.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Divison div, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return div.leftOperand.transformTerm(trace,variables).div(div.rightOperand.transformTerm(trace,variables))
+        }
+        def dispatch protected Expr transformTerm(Mod mod, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                throw new UnsupportedOperationException("Modulo is not supported.")
+        }
+        def dispatch protected Expr transformTerm(Forall forall, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return configureForall(forall,trace,variables) 
+        }
+        def dispatch protected Expr transformTerm(Exists exists, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return configureExists(exists,trace,variables)
+        }
+        def dispatch protected Expr transformTerm(SymbolicValue symbolicValue, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) }
+        
+        def private configureForall(
+                Forall quantifiedExpression,
+                Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)
+        {
+                val allVariables = new HashMap(variables)
+                val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size)
+                
+                for(logicVariable: quantifiedExpression.quantifiedVariables) {
+                        val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl
+                        allVariables.put(logicVariable, newAlloyVariable)
+                        newAlloyVariables += newAlloyVariable
+                }
+                val variable0=newAlloyVariables.get(0)
+                newAlloyVariables.remove(0)
+                return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forAll(variable0, newAlloyVariables)
+        }
+        
+        def private configureExists(
+                Exists quantifiedExpression,
+                Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)
+        {
+                val allVariables = new HashMap(variables)
+                val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size)
+                
+                for(logicVariable: quantifiedExpression.quantifiedVariables) {
+                        val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl
+                        allVariables.put(logicVariable, newAlloyVariable)
+                        newAlloyVariables += newAlloyVariable
+                }
+                val variable0=newAlloyVariables.get(0)
+                newAlloyVariables.remove(0)
+                return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forSome(variable0, newAlloyVariables)
+        }
+        
+        def dispatch protected Expr transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return trace.elements.get(referred)
+        }
+        def dispatch protected Expr transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return variables.get(variable).get
+        }
+        /*def dispatch protected Expr transformSymbolicReference(Function function, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                val result = createSMTSymbolicValue => [sv | sv.symbolicReference = trace.functions.get(function)]
+                for(paramSubstitution : parameterSubstitutions) {
+                        result.parameterSubstitutions.add(paramSubstitution.transformTerm(trace,variables))
+                }
+                return result
+        }*/
+        def dispatch protected Expr transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                return trace.relations.get(relation)
+        }
+        def dispatch protected Expr transformSymbolicReference(Constant constant, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
+                //createSMTSymbolicValue => [symbolicReference = trace.constants.get(constant)]
+                throw new UnsupportedOperationException("Constant is not supported")
+        }
+}
+\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes
new file mode 100644
index 00000000..5e349ac8
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes
@@ -0,0 +1,74 @@
+/*def dispatch boolean hasDeclaredElement(TypeDefinition type) { return false; }
+        def dispatch boolean hasDeclaredElement(TypeDeclaration type) {
+                if(type.isAbstract) {
+                        type.subtypes.exists[it.hasDeclaredElement]
+                } else return true;
+        }
+        
+        def dispatch List<TypeDefinition> allEnumSubtypes(TypeDefinition type) { return #[type] }
+        def dispatch List<TypeDefinition> allEnumSubtypes(TypeDeclaration type) {
+                return type.subtypes.map[it.allEnumSubtypes].flatten.toList
+        }
+        
+        def protected transformTypes(List<Type> types, Logic2AlloyLanguageMapperTrace trace) {
+                val Map<TypeDeclaration,ALSSignatureDeclaration> signatureTrace = new HashMap;
+                
+                // Creating the root type
+                val objectType = createALSSignatureDeclaration => [ name=#["util","object"].toID it.abstract = true ]
+                trace.objectSupperClass = objectType
+                trace.specification.typeDeclarations += objectType
+                
+                // Creating the images of the types
+                for(type : types) {
+                        if(type instanceof TypeDefinition) {
+                                if(type.elements.empty) {
+                                        trace.type2ALSType.put(type,#[]);
+                                } else {
+                                        val e = createALSEnumDeclaration => [
+                                                it.name = type.name.toID
+                                                it.literal += type.elements.map[transformDefinedElement(trace)]
+                                        ]
+                                        trace.type2ALSType.put(type,#[e])
+                                        trace.specification.typeDeclarations += e
+                                }
+                        }
+                        else if(type instanceof TypeDeclaration) {
+                                if(hasDeclaredElement(type)) {
+                                        val s = createALSSignatureDeclaration => [
+                                                name=type.name.toID
+                                                it.abstract = type.isIsAbstract
+                                        ]
+                                        trace.type2ALSType.put(type,new LinkedList=>[add(s)])
+                                        signatureTrace.put(type, s)
+                                        trace.specification.typeDeclarations += s
+                                }
+                                else {
+                                        signatureTrace.put(type, null)
+                                        trace.type2ALSType.put(type,new LinkedList);// empty
+                                }
+                        }
+                        else throw new IllegalArgumentException('''Unknown type «type.class.name»''')
+                }
+                
+                
+                for(type: types.filter(TypeDeclaration)) {
+                        // Adding inheritance
+                        val s = type.lookup(signatureTrace)
+                        if(s!=null) {
+                                for(supertype : type.supertypes) {
+                                        s.supertype += (supertype as TypeDeclaration).lookup(signatureTrace)
+                                }
+                                if(type.supertypes.empty) {
+                                        s.supertype += objectType
+                                }
+                        }
+                        // Adding enum subtypes
+                        type.lookup(trace.type2ALSType)+=type.allEnumSubtypes.map[it.lookup(trace.type2ALSType)].flatten
+                }
+        }
+        
+        def protected transformDefinedElement(DefinedElement element, Logic2AlloyLanguageMapperTrace trace) {
+                val result = createALSEnumLiteral => [name = element.name.toID]
+                trace.definedElement2EnumProperty.put(element,result)
+                return result
+        }*/
+\ 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/unused
parent	Initial commit, migrating from SVN (diff)
download	VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip