1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
|
package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
import hu.bme.mit.inf.dslreasoner.alloyLanguage.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 java.util.List
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)
{
//val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size
// add fact to ensure the existence of all literals in the scope
if(!config.typeScopes.knownStrings.empty) {
specification.factDeclarations += createALSFactDeclaration => [
it.name = "EnsureAllStrings"
val List<? extends ALSTerm> equals = config.typeScopes.knownStrings.map[x|createALSEquals => [
it.leftOperand =createALSStringLiteral => [it.value = x]
it.rightOperand =createALSStringLiteral => [it.value = x]
]].toList
it.term = support.unfoldAnd(equals)
]
}
/*
val upperLimits = new LinkedList
val lowerLimits = new LinkedList
/*val typesWithScopeConstraint = config.typeScopes.maxNewElementsByType.keySet + config.typeScopes.minNewElementsByType.keySet
for(type : typesWithScopeConstraint) {
val max = if(config.typeScopes.maxNewElementsByType.containsKey(type)) {
config.typeScopes.maxNewElementsByType.get(type)
} else {
LogicSolverConfiguration::Unlimited
}
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 )
]
]
} else if(max !== LogicSolverConfiguration::Unlimited) {
upperLimits += createALSSigScope => [
it.type = typeMapper.transformTypeReference(type,mapper,trace).head
it.number = max
it.exactly =exactly
]
} else {
// do nothing
}
if(min != 0 && ! exactly) {
lowerLimits += type->min
}
}*/
specification.runCommand = createALSRunCommand => [
it.typeScopes+= createALSSigScope => [
it.type= typeMapper.getUndefinedSupertype(trace)
it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace)
it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
]
]
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) {
if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) {
throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')
} else {
if(config.typeScopes.maxNewStrings == 0) {
it.typeScopes += createALSStringScope => [it.number = 0]
} else {
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!''')
}
}
}
}
protected def setIntegerScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand command) {
//AlloySolverConfiguration config, ALSRunCommand it
// If the scope is unlimited ...
if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) {
val integersUsed = specification.eAllContents.filter(ALSInt)
if(integersUsed.empty) {
// ... but the problem has no integers => scope can be empty
command.typeScopes+= createALSIntScope => [ it.number = 0 ]
} else {
// If no integer scope is defined, and the problem has integers => error
throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''')
}
} else {
// If the scope is limited, collect the integers in the problem and the scope,...
//val maxIntScope = config.typeScopes.maxNewIntegers
//val minIntScope = config.typeScopes.minNewIntegers
val knownIntegers = config.typeScopes.knownIntegers
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 = #[minKnownInteger,minIntegerInProblem].min
val max = #[maxKnownInteger,maxIntegerInProblem].max
//val abs = Math.max(Math.abs(min),Math.abs(max))
command.typeScopes += createALSIntScope => [
it.number = toBits(min, max)
]
}
// if(config.typeScopes.knownIntegers.empty) {
// return Integer.SIZE-Integer.numberOfLeadingZeros((config.typeScopes.maxNewIntegers+1)/2)
// } else {
// var scope = Math.max(
// Math.abs(config.typeScopes.knownIntegers.max),
// Math.abs(config.typeScopes.knownIntegers.min))
// if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) {
// scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2
// }
// return Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1
// }
}
private static def toBits(int min, int max) {
// 4 Int = {-8, ..., 7}
// x Int = {- (2^(x-1)) , ... , 2^(x-1)-1}
var int bits = 1
// range = 2^(x-1)
var int range = 1
while((!(-range <= min)) || (!(max <= range-1))) {
bits++
range*=2
}
return bits
}
//
// def static void main(String[] args) {
// println('''0,0->«toBits(0,0)»''')
// println('''1,1->«toBits(1,1)»''')
// println('''-1,-1->«toBits(-1,-1)»''')
// println('''5,6->«toBits(5,6)»''')
// println('''0,6->«toBits(0,6)»''')
// println('''-10,0->«toBits(-10,0)»''')
// println('''-8,7->«toBits(-8,7)»''')
// println('''-100,100->«toBits(-100,100)»''')
// println('''-300,300->«toBits(-300,300)»''')
// }
}
|
