diff options
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 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend | |
parent | Whitespacing in manifest updated (diff) | |
download | VIATRA-Generator-49c349e361c5c026334c566a1f8b3357056f4e6e.tar.gz VIATRA-Generator-49c349e361c5c026334c566a1f8b3357056f4e6e.tar.zst VIATRA-Generator-49c349e361c5c026334c566a1f8b3357056f4e6e.zip |
scopes added to alloy
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend | 102 |
1 files changed, 72 insertions, 30 deletions
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 | ||