aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszkar.semerath@gmail.com>2018-11-07 12:19:47 +0100
committerLibravatar OszkarSemerath <oszkar.semerath@gmail.com>2018-11-07 12:19:47 +0100
commiteccbce5001c00413805037bc416bb14e97390c3c (patch)
tree9eb2c43d5dce6c747581c1cf901e71aae3babde9
parentAttributes are filled in instance models (diff)
downloadVIATRA-Generator-eccbce5001c00413805037bc416bb14e97390c3c.tar.gz
VIATRA-Generator-eccbce5001c00413805037bc416bb14e97390c3c.tar.zst
VIATRA-Generator-eccbce5001c00413805037bc416bb14e97390c3c.zip
Fixes in string scope and string interpretation for Alloy
Diffstat
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend47
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend83
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend105
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
19import java.util.List 19import java.util.List
20import java.util.Map 20import java.util.Map
21import java.util.Set 21import java.util.Set
22import java.util.SortedSet
23import java.util.TreeSet
22 24
23import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 25import 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
12import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion 12import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion
13import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion 13import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion
14import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion 14import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion
15import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
16import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput 15import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And 16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion 17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
@@ -48,6 +47,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
48import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference 47import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
49import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration 48import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
50import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition 49import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
50import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral
51import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
51import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue 52import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
52import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term 53import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
53import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure 54import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure
@@ -65,14 +66,11 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope
65import org.eclipse.xtend.lib.annotations.Accessors 66import org.eclipse.xtend.lib.annotations.Accessors
66 67
67import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 68import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
68import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt
69import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
70import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral
71import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSStringLiteral
72 69
73class Logic2AlloyLanguageMapper { 70class 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 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2
3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
5import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt
6import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
7import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
8import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
10import java.util.LinkedList
11import java.util.List
12
13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
14
15class 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-06 18:38:23 +0000