diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src')
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 { | |||
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 | ||