diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder')
3 files changed, 142 insertions, 93 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend index 95216835..107aa001 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend | |||
@@ -19,6 +19,8 @@ import java.util.LinkedList | |||
19 | import java.util.List | 19 | import java.util.List |
20 | import java.util.Map | 20 | import java.util.Map |
21 | import java.util.Set | 21 | import java.util.Set |
22 | import java.util.SortedSet | ||
23 | import java.util.TreeSet | ||
22 | 24 | ||
23 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 25 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
24 | 26 | ||
@@ -34,6 +36,8 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
34 | 36 | ||
35 | private var String logicBooleanTrue; | 37 | private var String logicBooleanTrue; |
36 | private var String logicBooleanFalse; | 38 | private var String logicBooleanFalse; |
39 | private SortedSet<Integer> integerAtoms = new TreeSet | ||
40 | private SortedSet<String> stringAtoms = new TreeSet | ||
37 | 41 | ||
38 | private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap | 42 | private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap |
39 | private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap | 43 | private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap |
@@ -42,8 +46,8 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
42 | private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value | 46 | private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value |
43 | private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value | 47 | private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value |
44 | 48 | ||
45 | private val int minInt | 49 | //private val int minInt |
46 | private val int maxInt | 50 | //private val int maxInt |
47 | 51 | ||
48 | public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { | 52 | public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { |
49 | this.typeInterpretator = typeInterpretator | 53 | this.typeInterpretator = typeInterpretator |
@@ -60,8 +64,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
60 | name2AlloyField.put(field.label,field) | 64 | name2AlloyField.put(field.label,field) |
61 | } | 65 | } |
62 | } | 66 | } |
63 | 67 | val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution) | |
64 | val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution.allAtoms) | ||
65 | this.typeInterpretator.resolveUnknownAtoms( | 68 | this.typeInterpretator.resolveUnknownAtoms( |
66 | unknownAtoms, | 69 | unknownAtoms, |
67 | solution, | 70 | solution, |
@@ -101,31 +104,46 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
101 | this.relation2Value = Union(hostedRelation2Value,globalRelation2Value) | 104 | this.relation2Value = Union(hostedRelation2Value,globalRelation2Value) |
102 | 105 | ||
103 | //Int limits | 106 | //Int limits |
104 | this.minInt = solution.min | 107 | //this.minInt = solution.min |
105 | this.maxInt = solution.max | 108 | //this.maxInt = solution.max |
106 | 109 | ||
107 | //print(trace) | 110 | //print(trace) |
108 | } | 111 | } |
109 | 112 | ||
110 | def List<ExprVar> collectUnknownAndResolveKnownAtoms(Iterable<ExprVar> allAtoms) { | 113 | def List<ExprVar> collectUnknownAndResolveKnownAtoms(A4Solution solution) { |
114 | val Iterable<ExprVar> allAtoms = solution.allAtoms | ||
111 | val List<ExprVar> unknownAtoms = new LinkedList | 115 | val List<ExprVar> unknownAtoms = new LinkedList |
112 | 116 | ||
113 | for(atom: allAtoms) { | 117 | for(atom: allAtoms) { |
114 | val typeName = getName(atom.type) | 118 | val typeName = getName(atom.type) |
115 | val atomName = atom.name | 119 | val atomName = atom.name |
116 | //println(atom.toString + " < - " + typeName) | 120 | println(atom.toString + " < - " + typeName) |
117 | if(typeName == forwardTrace.logicLanguage.name) { | 121 | if(typeName == forwardTrace.logicLanguage.name) { |
118 | this.logicLanguage = atom | 122 | this.logicLanguage = atom |
119 | } else if(typeName == "Int" || typeName == "seq/Int") { | 123 | } else if(typeName == "Int" || typeName == "seq/Int") { |
120 | // do nothing, integers will be parsed from the string | 124 | val value = Integer.parseInt(atomName.join) |
125 | this.integerAtoms.add(value) | ||
121 | } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { | 126 | } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { |
122 | if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } | 127 | if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } |
123 | else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} | 128 | else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} |
124 | else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') | 129 | else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') |
130 | } else if(typeName == "String") { | ||
131 | val value = parseString(atomName.join) | ||
132 | this.stringAtoms.add(value) | ||
133 | } else { | ||
134 | unknownAtoms += atom | ||
125 | } | 135 | } |
126 | else unknownAtoms += atom | ||
127 | } | 136 | } |
128 | 137 | val integerSignature = solution.allReachableSigs.filter[it.label=="Int"].head | |
138 | for(i : solution.eval(integerSignature)) { | ||
139 | val value = Integer.parseInt(i.atom(0)) | ||
140 | this.integerAtoms.add(value) | ||
141 | } | ||
142 | val stringSignature = solution.allReachableSigs.filter[it.label=="String"].head | ||
143 | for(i : solution.eval(stringSignature)) { | ||
144 | val value = parseString(i.atom(0)) | ||
145 | this.stringAtoms.add(value) | ||
146 | } | ||
129 | return unknownAtoms | 147 | return unknownAtoms |
130 | } | 148 | } |
131 | 149 | ||
@@ -196,17 +214,16 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
196 | } | 214 | } |
197 | 215 | ||
198 | override getAllIntegersInStructure() { | 216 | override getAllIntegersInStructure() { |
199 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 217 | this.integerAtoms |
200 | } | 218 | } |
201 | 219 | ||
202 | override getAllRealsInStructure() { | 220 | override getAllRealsInStructure() { |
203 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 221 | new TreeSet |
204 | } | 222 | } |
205 | 223 | ||
206 | override getAllStringsInStructure() { | 224 | override getAllStringsInStructure() { |
207 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 225 | this.stringAtoms |
208 | } | 226 | } |
209 | |||
210 | } | 227 | } |
211 | 228 | ||
212 | /** | 229 | /** |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend index 1076019f..3fc3971d 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | |||
@@ -12,7 +12,6 @@ import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | |||
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | 12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion |
13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | 13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion |
14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | 14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion |
@@ -48,6 +47,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | |||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | 47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference |
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | 52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue |
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | 53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term |
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure | 54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure |
@@ -65,14 +66,11 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope | |||
65 | import org.eclipse.xtend.lib.annotations.Accessors | 66 | import org.eclipse.xtend.lib.annotations.Accessors |
66 | 67 | ||
67 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 68 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
68 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt | ||
69 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference | ||
70 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral | ||
71 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSStringLiteral | ||
72 | 69 | ||
73 | class Logic2AlloyLanguageMapper { | 70 | class Logic2AlloyLanguageMapper { |
74 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 71 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
75 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | 72 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; |
73 | private val RunCommandMapper runCommandMapper | ||
76 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | 74 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; |
77 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this) | 75 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this) |
78 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this) | 76 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this) |
@@ -81,6 +79,7 @@ class Logic2AlloyLanguageMapper { | |||
81 | 79 | ||
82 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | 80 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { |
83 | this.typeMapper = typeMapper | 81 | this.typeMapper = typeMapper |
82 | this.runCommandMapper = new RunCommandMapper(typeMapper) | ||
84 | } | 83 | } |
85 | 84 | ||
86 | public def TracedOutput<ALSDocument,Logic2AlloyLanguageMapperTrace> transformProblem(LogicProblem problem, AlloySolverConfiguration config) { | 85 | public def TracedOutput<ALSDocument,Logic2AlloyLanguageMapperTrace> transformProblem(LogicProblem problem, AlloySolverConfiguration config) { |
@@ -146,7 +145,7 @@ class Logic2AlloyLanguageMapper { | |||
146 | } | 145 | } |
147 | } | 146 | } |
148 | 147 | ||
149 | transformRunCommand(specification, trace, config) | 148 | runCommandMapper.transformRunCommand(this, specification, trace, config) |
150 | 149 | ||
151 | return new TracedOutput(specification,trace) | 150 | return new TracedOutput(specification,trace) |
152 | } | 151 | } |
@@ -303,78 +302,6 @@ class Logic2AlloyLanguageMapper { | |||
303 | def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { | 302 | def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { |
304 | val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) | 303 | val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) |
305 | return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) | 304 | return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) |
306 | } | ||
307 | |||
308 | ////////////// | ||
309 | // Scopes | ||
310 | ////////////// | ||
311 | |||
312 | def transformRunCommand(ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) | ||
313 | { | ||
314 | val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size | ||
315 | |||
316 | // add fact to ensure the existence of all literals in the scope | ||
317 | if(!config.typeScopes.knownStrings.empty) { | ||
318 | specification.factDeclarations += createALSFactDeclaration => [ | ||
319 | it.name = "EnsureAllStrings" | ||
320 | val List<? extends ALSTerm> equals = config.typeScopes.knownStrings.map[x|createALSEquals => [ | ||
321 | it.leftOperand =createALSStringLiteral => [it.value = x] | ||
322 | it.rightOperand =createALSStringLiteral => [it.value = x] | ||
323 | ]].toList | ||
324 | it.term = support.unfoldAnd(equals) | ||
325 | ] | ||
326 | } | ||
327 | |||
328 | specification.runCommand = createALSRunCommand => [ | ||
329 | it.typeScopes+= createALSSigScope => [ | ||
330 | it.type= typeMapper.getUndefinedSupertype(trace) | ||
331 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | ||
332 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | ||
333 | ] | ||
334 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | ||
335 | val integersUsed = specification.eAllContents.filter(ALSInt) | ||
336 | if(integersUsed.empty) { | ||
337 | // If no integer scope is defined, but the problem has no integers | ||
338 | // => scope can be empty | ||
339 | it.typeScopes+= createALSIntScope => [ | ||
340 | it.number = 0 | ||
341 | ] | ||
342 | } else { | ||
343 | // If no integer scope is defined, and the problem has integers | ||
344 | // => error | ||
345 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') | ||
346 | } | ||
347 | } else { | ||
348 | it.typeScopes += createALSIntScope => [ | ||
349 | if(config.typeScopes.knownIntegers.empty) { | ||
350 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | ||
351 | } else { | ||
352 | var scope = Math.max( | ||
353 | Math.abs(config.typeScopes.knownIntegers.max), | ||
354 | Math.abs(config.typeScopes.knownIntegers.min)) | ||
355 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
356 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
357 | } | ||
358 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 | ||
359 | } | ||
360 | ] | ||
361 | } | ||
362 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | ||
363 | throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') | ||
364 | } else { | ||
365 | if(config.typeScopes.maxNewStrings != 0) { | ||
366 | it.typeScopes += createALSStringScope => [it.number = config.typeScopes.maxNewStrings - knownStringNumber] | ||
367 | } | ||
368 | } | ||
369 | |||
370 | // for(definedScope : config.typeScopes.allDefinedScope) { | ||
371 | // it.typeScopes += createALSSigScope => [ | ||
372 | // it.type = definedScope.type.lookup(trace.type2ALSType) | ||
373 | // it.number = definedScope.upperLimit | ||
374 | // it.exactly = (definedScope.upperLimit == definedScope.lowerLimit) | ||
375 | // ] | ||
376 | // } | ||
377 | ] | ||
378 | } | 305 | } |
379 | 306 | ||
380 | ////////////// | 307 | ////////////// |
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 new file mode 100644 index 00000000..3e96f7f4 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend | |||
@@ -0,0 +1,105 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
10 | import java.util.LinkedList | ||
11 | import java.util.List | ||
12 | |||
13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
14 | |||
15 | class RunCommandMapper { | ||
16 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
17 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
18 | private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | ||
19 | |||
20 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | ||
21 | this.typeMapper = typeMapper | ||
22 | } | ||
23 | |||
24 | def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) | ||
25 | { | ||
26 | //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size | ||
27 | |||
28 | // add fact to ensure the existence of all literals in the scope | ||
29 | if(!config.typeScopes.knownStrings.empty) { | ||
30 | specification.factDeclarations += createALSFactDeclaration => [ | ||
31 | it.name = "EnsureAllStrings" | ||
32 | val List<? extends ALSTerm> equals = config.typeScopes.knownStrings.map[x|createALSEquals => [ | ||
33 | it.leftOperand =createALSStringLiteral => [it.value = x] | ||
34 | it.rightOperand =createALSStringLiteral => [it.value = x] | ||
35 | ]].toList | ||
36 | it.term = support.unfoldAnd(equals) | ||
37 | ] | ||
38 | } | ||
39 | val typeScopes = new LinkedList | ||
40 | for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) { | ||
41 | val key = definedScope.key | ||
42 | val amount = definedScope.value | ||
43 | val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount | ||
44 | |||
45 | val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet | ||
46 | if(amount == 0 && exactly) { | ||
47 | specification.factDeclarations += createALSFactDeclaration => [ | ||
48 | it.term = createALSEquals => [ | ||
49 | it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
50 | it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) | ||
51 | ] | ||
52 | ] | ||
53 | } | ||
54 | val int n = existing.size-amount | ||
55 | typeScopes += createALSSigScope => [ | ||
56 | it.type = typeMapper.transformTypeReference(key,mapper,trace).head | ||
57 | it.number = n | ||
58 | it.exactly =exactly | ||
59 | ] | ||
60 | } | ||
61 | |||
62 | specification.runCommand = createALSRunCommand => [ | ||
63 | it.typeScopes+= createALSSigScope => [ | ||
64 | it.type= typeMapper.getUndefinedSupertype(trace) | ||
65 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | ||
66 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | ||
67 | ] | ||
68 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | ||
69 | val integersUsed = specification.eAllContents.filter(ALSInt) | ||
70 | if(integersUsed.empty) { | ||
71 | // If no integer scope is defined, but the problem has no integers | ||
72 | // => scope can be empty | ||
73 | it.typeScopes+= createALSIntScope => [ | ||
74 | it.number = 0 | ||
75 | ] | ||
76 | } else { | ||
77 | // If no integer scope is defined, and the problem has integers | ||
78 | // => error | ||
79 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') | ||
80 | } | ||
81 | } else { | ||
82 | it.typeScopes += createALSIntScope => [ | ||
83 | if(config.typeScopes.knownIntegers.empty) { | ||
84 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | ||
85 | } else { | ||
86 | var scope = Math.max( | ||
87 | Math.abs(config.typeScopes.knownIntegers.max), | ||
88 | Math.abs(config.typeScopes.knownIntegers.min)) | ||
89 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
90 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
91 | } | ||
92 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 | ||
93 | } | ||
94 | ] | ||
95 | } | ||
96 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | ||
97 | throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') | ||
98 | } else { | ||
99 | if(config.typeScopes.maxNewStrings != 0) { | ||
100 | it.typeScopes += createALSStringScope => [it.number = 0] | ||
101 | } | ||
102 | } | ||
103 | ] | ||
104 | } | ||
105 | } \ No newline at end of file | ||