scopes added to alloy

author: Oszkar Semerath <semerath@mit.bme.hu> 2019-08-30 14:33:06 +0200
committer: Oszkar Semerath <semerath@mit.bme.hu> 2019-08-30 14:33:06 +0200
commit: 49c349e361c5c026334c566a1f8b3357056f4e6e (patch)
tree: 65c105c2c9ec6f2344056ffab98f85748d76a309
parent: Whitespacing in manifest updated (diff)
download: VIATRA-Generator-49c349e361c5c026334c566a1f8b3357056f4e6e.tar.gz
VIATRA-Generator-49c349e361c5c026334c566a1f8b3357056f4e6e.tar.zst
VIATRA-Generator-49c349e361c5c026334c566a1f8b3357056f4e6e.zip
3 files changed, 124 insertions, 35 deletions
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
index 0762efce..8de9688b 100644
--- 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
@@ -133,11 +133,11 @@ class Logic2AlloyLanguageMapper_RelationMapper {
        public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) {
                if(relation.parameters.size === 2) {
                        /** 1. Create a relation that can be used in ^relation expressions */ 
-                        val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace)
+                        val declaration = this.createRelationDeclaration(support.toID('''AsDeclaration «relation.name»'''),relation.parameters,trace)
                        trace.relationInTransitiveToHosterField.put(relation,declaration)
                        /** 2. Add fact that the declaration corresponds to the definition */
                        val fact = createALSFactDeclaration => [
-                                it.name = '''EqualsAsDeclaration «relation.name»'''
+                                it.name = support.toID('''EqualsAsDeclaration «relation.name»''')
                                it.term = createALSQuantifiedEx => [
                                        val a = createALSVariableDeclaration => [
                                                it.name = "a"
@@ -157,7 +157,7 @@ class Logic2AlloyLanguageMapper_RelationMapper {
                                                        it.params += createALSReference => [ it.referred = b ]
                                                ]
                                                it.rightOperand = createALSSubset => [
-                                                        it.leftOperand = createALSJoin => [
+                                                        it.leftOperand = createALSDirectProduct => [
                                                                it.leftOperand = createALSReference => [ referred = a ]
                                                                it.rightOperand = createALSReference => [ referred = b ]
                                                        ]
@@ -183,12 +183,15 @@ class Logic2AlloyLanguageMapper_RelationMapper {
                                rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ]
                        ]
                } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){
-                        createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ]
+                        createALSJoin => [
+                                leftOperand = createALSReference => [referred = trace.logicLanguage]
+                                rightOperand = createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ]
+                                ]
                } else {
                        throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''')
                }
                return createALSSubset => [
-                        it.leftOperand = createALSJoin => [
+                        it.leftOperand = createALSDirectProduct => [
                                it.leftOperand = source
                                it.rightOperand = target
                        ]
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend
new file mode 100644
index 00000000..a270cb73
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend
@@ -0,0 +1,44 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+interface Logic2AlloyLanguageMapper_TypeScopeMapping {
+        def void addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace)
+        def void addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace)
+}
+class Logic2AlloyLanguageMapper_AsConstraint implements Logic2AlloyLanguageMapper_TypeScopeMapping {
+        val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper_TypeMapper typeMapper
+        
+        new(Logic2AlloyLanguageMapper_TypeMapper mapper) {
+                this.typeMapper = mapper
+        }
+        
+        override addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                document.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["LowerMultiplicity",support.toID(type.name),lowerMultiplicty.toString])
+                        it.term = createALSLeq => [
+                                it.leftOperand = createALSCardinality => [
+                                        it.operand =  support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList)
+                                ]
+                                it.rightOperand = createALSNumberLiteral => [it.value = lowerMultiplicty]
+                        ]
+                ]
+        }
+        
+        override addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                document.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["UpperMultiplicity",support.toID(type.name),upperMultiplicty.toString])
+                        it.term = createALSMeq => [
+                                it.leftOperand = createALSCardinality => [
+                                        it.operand =  support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList)
+                                ]
+                                it.rightOperand = createALSNumberLiteral => [it.value = upperMultiplicty]
+                        ]
+                ]
+        }
+}
+\ 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/RunCommandMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
index cbd56abb..494197bc 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
@@ -5,22 +5,21 @@ import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
 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.logiclanguage.TypeDefinition
-import java.util.LinkedList
 import java.util.List
-import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 class RunCommandMapper {
        val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
        val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
        val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
+        val Logic2AlloyLanguageMapper_TypeScopeMapping typeScopeMapping;
        
        new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
                this.typeMapper = typeMapper
+                this.typeScopeMapping = new Logic2AlloyLanguageMapper_AsConstraint(typeMapper)
        }
        
        def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config)
@@ -38,28 +37,47 @@ class RunCommandMapper {
                                it.term = support.unfoldAnd(equals)
                        ]
                }
-                val typeScopes = new LinkedList
+                
-                for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) {
+                /*
-                                val key = definedScope.key
+                val upperLimits = new LinkedList
-                                val amount = definedScope.value
+                val lowerLimits = new LinkedList
-                                val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount
+                
-                                
+                /*val typesWithScopeConstraint = config.typeScopes.maxNewElementsByType.keySet + config.typeScopes.minNewElementsByType.keySet
-                                val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet
+                for(type : typesWithScopeConstraint) {
-                                if(amount == 0 && exactly) {
+                        val max = if(config.typeScopes.maxNewElementsByType.containsKey(type)) {
-                                        specification.factDeclarations += createALSFactDeclaration => [
+                                config.typeScopes.maxNewElementsByType.get(type)
-                                                it.term = createALSEquals => [
+                        } else {
-                                                        it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList)
+                                LogicSolverConfiguration::Unlimited
-                                                        it.rightOperand =  support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList )
+                        }
-                                                ]
+                        val min = if(config.typeScopes.minNewElementsByType.containsKey(type)) {
+                                config.typeScopes.minNewElementsByType.get(type)
+                        } else {
+                                0
+                        }
+                        
+                        val exactly = min === max
+                        
+                        if(max === 0) {
+                                val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet
+                                specification.factDeclarations += createALSFactDeclaration => [
+                                        it.term = createALSEquals => [
+                                                it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList)
+                                                it.rightOperand =  support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList )
                                        ]
-                                }
+                                ]
-                                val int n = existing.size-amount
+                        } else if(max !== LogicSolverConfiguration::Unlimited) {
-                                typeScopes += createALSSigScope => [
+                                upperLimits += createALSSigScope => [
-                                        it.type = typeMapper.transformTypeReference(key,mapper,trace).head
+                                        it.type = typeMapper.transformTypeReference(type,mapper,trace).head
-                                        it.number = n
+                                        it.number = max
                                        it.exactly =exactly
                                ]
+                        } else {
+                                // do nothing
+                        }
+                        if(min != 0 && ! exactly) {
+                                lowerLimits += type->min
                        }
+                }*/
                
                specification.runCommand = createALSRunCommand => [
                        it.typeScopes+= createALSSigScope => [
@@ -67,9 +85,25 @@ class RunCommandMapper {
                                it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) 
                                it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
                        ]
-                        setIntegerScope(specification,config,it)
+                        
-                        setStringScope(specification,config,it)
                ]
+                
+                for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) {
+                        val limit = upperLimit.value
+                        if(limit != LogicSolverConfiguration::Unlimited) {
+                                this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace)
+                        }
+                }
+                
+                for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) {
+                        val limit = lowerLimit.value
+                        if(limit != 0) {
+                                this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace)
+                        }
+                }
+                
+                setIntegerScope(specification,config,specification.runCommand)
+                setStringScope(specification,config,specification.runCommand)
        }
        
        protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) {
@@ -79,7 +113,11 @@ class RunCommandMapper {
                        if(config.typeScopes.maxNewStrings == 0) {
                                it.typeScopes += createALSStringScope => [it.number = 0]
                        } else {
-                                throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')
+                                if(specification.eAllContents.filter(ALSString).empty) {
+                                        it.typeScopes += createALSStringScope => [it.number = 0]
+                                } else {
+                                        throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')
+                                }
                        }
                }
        }
@@ -99,13 +137,17 @@ class RunCommandMapper {
                        }
                } else {
                        // If the scope is limited, collect the integers in the problem and the scope,...
-                        val maxIntScope = config.typeScopes.maxNewIntegers
+                        //val maxIntScope = config.typeScopes.maxNewIntegers
-                        val minIntScope = config.typeScopes.minNewIntegers
+                        //val minIntScope = config.typeScopes.minNewIntegers
                        val knownIntegers = config.typeScopes.knownIntegers
-                        val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value]
+                        val minKnownInteger = if(knownIntegers.empty) { Integer.MAX_VALUE } else { knownIntegers.min }
+                        val maxKnownInteger = if(knownIntegers.empty) { Integer.MIN_VALUE } else { knownIntegers.max }
+                        val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value].toList
+                        val minIntegerInProblem = if(integersInProblem.empty) { Integer.MAX_VALUE } else { integersInProblem.min }
+                        val maxIntegerInProblem = if(integersInProblem.empty) { Integer.MIN_VALUE } else { integersInProblem.max }
                        // And select the range of integers
-                        val min = #[minIntScope,knownIntegers.min,integersInProblem.min].min
+                        val min = #[minKnownInteger,minIntegerInProblem].min
-                        val max = #[maxIntScope,knownIntegers.max,integersInProblem.max].max
+                        val max = #[maxKnownInteger,maxIntegerInProblem].max
                        //val abs = Math.max(Math.abs(min),Math.abs(max))
author	Oszkar Semerath <semerath@mit.bme.hu>	2019-08-30 14:33:06 +0200
committer	Oszkar Semerath <semerath@mit.bme.hu>	2019-08-30 14:33:06 +0200
commit	49c349e361c5c026334c566a1f8b3357056f4e6e (patch)
tree	65c105c2c9ec6f2344056ffab98f85748d76a309
parent	Whitespacing in manifest updated (diff)
download	VIATRA-Generator-49c349e361c5c026334c566a1f8b3357056f4e6e.tar.gz VIATRA-Generator-49c349e361c5c026334c566a1f8b3357056f4e6e.tar.zst VIATRA-Generator-49c349e361c5c026334c566a1f8b3357056f4e6e.zip

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 index 0762efce..8de9688b 100644 --- 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
@@ -133,11 +133,11 @@ class Logic2AlloyLanguageMapper_RelationMapper {
133	public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) {	133	public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) {
134	if(relation.parameters.size === 2) {	134	if(relation.parameters.size === 2) {
135	/** 1. Create a relation that can be used in ^relation expressions */	135	/** 1. Create a relation that can be used in ^relation expressions */
136	val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace)	136	val declaration = this.createRelationDeclaration(support.toID('''AsDeclaration «relation.name»'''),relation.parameters,trace)
137	trace.relationInTransitiveToHosterField.put(relation,declaration)	137	trace.relationInTransitiveToHosterField.put(relation,declaration)
138	/** 2. Add fact that the declaration corresponds to the definition */	138	/** 2. Add fact that the declaration corresponds to the definition */
139	val fact = createALSFactDeclaration => [	139	val fact = createALSFactDeclaration => [
140	it.name = '''EqualsAsDeclaration «relation.name»'''	140	it.name = support.toID('''EqualsAsDeclaration «relation.name»''')
141	it.term = createALSQuantifiedEx => [	141	it.term = createALSQuantifiedEx => [
142	val a = createALSVariableDeclaration => [	142	val a = createALSVariableDeclaration => [
143	it.name = "a"	143	it.name = "a"
@@ -157,7 +157,7 @@ class Logic2AlloyLanguageMapper_RelationMapper {
157	it.params += createALSReference => [ it.referred = b ]	157	it.params += createALSReference => [ it.referred = b ]
158	]	158	]
159	it.rightOperand = createALSSubset => [	159	it.rightOperand = createALSSubset => [
160	it.leftOperand = createALSJoin => [	160	it.leftOperand = createALSDirectProduct => [
161	it.leftOperand = createALSReference => [ referred = a ]	161	it.leftOperand = createALSReference => [ referred = a ]
162	it.rightOperand = createALSReference => [ referred = b ]	162	it.rightOperand = createALSReference => [ referred = b ]
163	]	163	]
@@ -183,12 +183,15 @@ class Logic2AlloyLanguageMapper_RelationMapper {
183	rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ]	183	rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ]
184	]	184	]
185	} else if(trace.relationInTransitiveToHosterField.containsKey(relation)){	185	} else if(trace.relationInTransitiveToHosterField.containsKey(relation)){
186	createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ]	186	createALSJoin => [
		187	leftOperand = createALSReference => [referred = trace.logicLanguage]
		188	rightOperand = createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ]
		189	]
187	} else {	190	} else {
188	throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''')	191	throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''')
189	}	192	}
190	return createALSSubset => [	193	return createALSSubset => [
191	it.leftOperand = createALSJoin => [	194	it.leftOperand = createALSDirectProduct => [
192	it.leftOperand = source	195	it.leftOperand = source
193	it.rightOperand = target	196	it.rightOperand = target
194	]	197	]


diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend new file mode 100644 index 00000000..a270cb73 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend
@@ -0,0 +1,44 @@
		1	package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
		2
		3	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
		4	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
		5	import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
		6
		7	interface Logic2AlloyLanguageMapper_TypeScopeMapping {
		8	def void addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace)
		9	def void addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace)
		10	}
		11
		12	class Logic2AlloyLanguageMapper_AsConstraint implements Logic2AlloyLanguageMapper_TypeScopeMapping {
		13	val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
		14	val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
		15	val Logic2AlloyLanguageMapper_TypeMapper typeMapper
		16
		17	new(Logic2AlloyLanguageMapper_TypeMapper mapper) {
		18	this.typeMapper = mapper
		19	}
		20
		21	override addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
		22	document.factDeclarations += createALSFactDeclaration => [
		23	it.name = support.toID(#["LowerMultiplicity",support.toID(type.name),lowerMultiplicty.toString])
		24	it.term = createALSLeq => [
		25	it.leftOperand = createALSCardinality => [
		26	it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t\|createALSReference => [it.referred = t]].toList)
		27	]
		28	it.rightOperand = createALSNumberLiteral => [it.value = lowerMultiplicty]
		29	]
		30	]
		31	}
		32
		33	override addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
		34	document.factDeclarations += createALSFactDeclaration => [
		35	it.name = support.toID(#["UpperMultiplicity",support.toID(type.name),upperMultiplicty.toString])
		36	it.term = createALSMeq => [
		37	it.leftOperand = createALSCardinality => [
		38	it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t\|createALSReference => [it.referred = t]].toList)
		39	]
		40	it.rightOperand = createALSNumberLiteral => [it.value = upperMultiplicty]
		41	]
		42	]
		43	}
		44	} \ 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/RunCommandMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend index cbd56abb..494197bc 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
@@ -5,22 +5,21 @@ import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
5	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt	5	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt
6	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral	6	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral
7	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand	7	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand
		8	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString
8	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm	9	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
9	import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory	10	import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
10	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration	11	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
11	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
12	import java.util.LinkedList
13	import java.util.List	12	import java.util.List
14		13
15	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
16
17	class RunCommandMapper {	14	class RunCommandMapper {
18	val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE	15	val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
19	val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;	16	val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
20	val Logic2AlloyLanguageMapper_TypeMapper typeMapper;	17	val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
		18	val Logic2AlloyLanguageMapper_TypeScopeMapping typeScopeMapping;
21		19
22	new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {	20	new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
23	this.typeMapper = typeMapper	21	this.typeMapper = typeMapper
		22	this.typeScopeMapping = new Logic2AlloyLanguageMapper_AsConstraint(typeMapper)
24	}	23	}
25		24
26	def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config)	25	def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config)
@@ -38,28 +37,47 @@ class RunCommandMapper {
38	it.term = support.unfoldAnd(equals)	37	it.term = support.unfoldAnd(equals)
39	]	38	]
40	}	39	}
41	val typeScopes = new LinkedList	40
42	for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) {	41	/*
43	val key = definedScope.key	42	val upperLimits = new LinkedList
44	val amount = definedScope.value	43	val lowerLimits = new LinkedList
45	val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount	44
46		45	/*val typesWithScopeConstraint = config.typeScopes.maxNewElementsByType.keySet + config.typeScopes.minNewElementsByType.keySet
47	val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet	46	for(type : typesWithScopeConstraint) {
48	if(amount == 0 && exactly) {	47	val max = if(config.typeScopes.maxNewElementsByType.containsKey(type)) {
49	specification.factDeclarations += createALSFactDeclaration => [	48	config.typeScopes.maxNewElementsByType.get(type)
50	it.term = createALSEquals => [	49	} else {
51	it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t\|createALSReference => [it.referred = t]].toList)	50	LogicSolverConfiguration::Unlimited
52	it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList )	51	}
53	]	52	val min = if(config.typeScopes.minNewElementsByType.containsKey(type)) {
		53	config.typeScopes.minNewElementsByType.get(type)
		54	} else {
		55	0
		56	}
		57
		58	val exactly = min === max
		59
		60	if(max === 0) {
		61	val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet
		62	specification.factDeclarations += createALSFactDeclaration => [
		63	it.term = createALSEquals => [
		64	it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t\|createALSReference => [it.referred = t]].toList)
		65	it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList )
54	]	66	]
55	}	67	]
56	val int n = existing.size-amount	68	} else if(max !== LogicSolverConfiguration::Unlimited) {
57	typeScopes += createALSSigScope => [	69	upperLimits += createALSSigScope => [
58	it.type = typeMapper.transformTypeReference(key,mapper,trace).head	70	it.type = typeMapper.transformTypeReference(type,mapper,trace).head
59	it.number = n	71	it.number = max
60	it.exactly =exactly	72	it.exactly =exactly
61	]	73	]
		74	} else {
		75	// do nothing
		76	}
		77	if(min != 0 && ! exactly) {
		78	lowerLimits += type->min
62	}	79	}
		80	}*/
63		81
64	specification.runCommand = createALSRunCommand => [	82	specification.runCommand = createALSRunCommand => [
65	it.typeScopes+= createALSSigScope => [	83	it.typeScopes+= createALSSigScope => [
@@ -67,9 +85,25 @@ class RunCommandMapper {
67	it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace)	85	it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace)
68	it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)	86	it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
69	]	87	]
70	setIntegerScope(specification,config,it)	88
71	setStringScope(specification,config,it)
72	]	89	]
		90
		91	for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) {
		92	val limit = upperLimit.value
		93	if(limit != LogicSolverConfiguration::Unlimited) {
		94	this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace)
		95	}
		96	}
		97
		98	for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) {
		99	val limit = lowerLimit.value
		100	if(limit != 0) {
		101	this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace)
		102	}
		103	}
		104
		105	setIntegerScope(specification,config,specification.runCommand)
		106	setStringScope(specification,config,specification.runCommand)
73	}	107	}
74		108
75	protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) {	109	protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) {
@@ -79,7 +113,11 @@ class RunCommandMapper {
79	if(config.typeScopes.maxNewStrings == 0) {	113	if(config.typeScopes.maxNewStrings == 0) {
80	it.typeScopes += createALSStringScope => [it.number = 0]	114	it.typeScopes += createALSStringScope => [it.number = 0]
81	} else {	115	} else {
82	throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')	116	if(specification.eAllContents.filter(ALSString).empty) {
		117	it.typeScopes += createALSStringScope => [it.number = 0]
		118	} else {
		119	throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')
		120	}
83	}	121	}
84	}	122	}
85	}	123	}
@@ -99,13 +137,17 @@ class RunCommandMapper {
99	}	137	}
100	} else {	138	} else {
101	// If the scope is limited, collect the integers in the problem and the scope,...	139	// If the scope is limited, collect the integers in the problem and the scope,...
102	val maxIntScope = config.typeScopes.maxNewIntegers	140	//val maxIntScope = config.typeScopes.maxNewIntegers
103	val minIntScope = config.typeScopes.minNewIntegers	141	//val minIntScope = config.typeScopes.minNewIntegers
104	val knownIntegers = config.typeScopes.knownIntegers	142	val knownIntegers = config.typeScopes.knownIntegers
105	val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value]	143	val minKnownInteger = if(knownIntegers.empty) { Integer.MAX_VALUE } else { knownIntegers.min }
		144	val maxKnownInteger = if(knownIntegers.empty) { Integer.MIN_VALUE } else { knownIntegers.max }
		145	val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value].toList
		146	val minIntegerInProblem = if(integersInProblem.empty) { Integer.MAX_VALUE } else { integersInProblem.min }
		147	val maxIntegerInProblem = if(integersInProblem.empty) { Integer.MIN_VALUE } else { integersInProblem.max }
106	// And select the range of integers	148	// And select the range of integers
107	val min = #[minIntScope,knownIntegers.min,integersInProblem.min].min	149	val min = #[minKnownInteger,minIntegerInProblem].min
108	val max = #[maxIntScope,knownIntegers.max,integersInProblem.max].max	150	val max = #[maxKnownInteger,maxIntegerInProblem].max
109	//val abs = Math.max(Math.abs(min),Math.abs(max))	151	//val abs = Math.max(Math.abs(min),Math.abs(max))
110		152
111		153