diff options
Diffstat (limited to 'Application/hu.bme.mit.inf.dslreasoner.application')
5 files changed, 54 insertions, 24 deletions
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/EclipseBasedProgressMonitor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/EclipseBasedProgressMonitor.xtend index 624e75a5..be35b64a 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/EclipseBasedProgressMonitor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/EclipseBasedProgressMonitor.xtend | |||
@@ -9,9 +9,15 @@ class EclipseBasedProgressMonitor extends SolverProgressMonitor{ | |||
9 | public new(IProgressMonitor internalMonitor) { | 9 | public new(IProgressMonitor internalMonitor) { |
10 | this.internalMonitor = internalMonitor | 10 | this.internalMonitor = internalMonitor |
11 | } | 11 | } |
12 | var double currentDouble = 0.0 | ||
13 | var int currentInt = 0 | ||
12 | 14 | ||
13 | override protected processWorked(double amount) { | 15 | override protected processWorked(double amount) { |
14 | internalMonitor.worked((amount*1000).intValue) | 16 | val newDouble = currentDouble+amount |
17 | val newInt = (newDouble*1000).intValue | ||
18 | internalMonitor.worked(newInt-currentInt) | ||
19 | currentDouble = newDouble | ||
20 | currentInt = newInt | ||
15 | } | 21 | } |
16 | 22 | ||
17 | override isCancelled() { | 23 | override isCancelled() { |
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend index ad950fc8..c9d38c7d 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend | |||
@@ -186,6 +186,7 @@ class GenerationTaskExecutor { | |||
186 | console.writeMessage("Model generation started") | 186 | console.writeMessage("Model generation started") |
187 | for(run : 1..runs) { | 187 | for(run : 1..runs) { |
188 | monitor.subTask('''Solving problem«IF runs>0» «run»/«runs»«ENDIF»''') | 188 | monitor.subTask('''Solving problem«IF runs>0» «run»/«runs»«ENDIF»''') |
189 | val visualisationProgressMonitor= new EclipseBasedProgressMonitor(monitor) | ||
189 | 190 | ||
190 | // 6.2 For each run, the configuration and the workspace is adjusted | 191 | // 6.2 For each run, the configuration and the workspace is adjusted |
191 | solverLoader.setRunIndex(solverConfig,configurationMap,run,console) | 192 | solverLoader.setRunIndex(solverConfig,configurationMap,run,console) |
@@ -240,44 +241,44 @@ class GenerationTaskExecutor { | |||
240 | dotRepresentations += outputWorkspaceForRun.getFile(dotFileName) | 241 | dotRepresentations += outputWorkspaceForRun.getFile(dotFileName) |
241 | } | 242 | } |
242 | else { | 243 | else { |
243 | dotRepresentations += null | 244 | dotRepresentations.add(null) |
244 | } | 245 | } |
245 | } else { | 246 | } else { |
246 | gmlRepresentations += null | 247 | gmlRepresentations.add(null) |
247 | dotRepresentations += null | 248 | dotRepresentations.add(null) |
248 | } | 249 | } |
249 | } | 250 | } |
250 | monitor.worked(100) | 251 | visualisationProgressMonitor.worked(1.0/interpretations.size) |
251 | } | 252 | } |
252 | if(!emfRepresentations.empty) { | 253 | if(!emfRepresentations.empty) { |
253 | console.writeMessage( | 254 | console.writeMessage( |
254 | '''Models: «FOR f : emfRepresentations»#«ENDFOR»''', | 255 | '''Models: «FOR f : emfRepresentations.filterNull»#«ENDFOR»''', |
255 | "#", | 256 | "#", |
256 | emfRepresentations.map[ | 257 | emfRepresentations.filterNull.map[ |
257 | new ScriptConsoleDecorator('''«it.fileRepresentationInConsole»''',it) | 258 | new ScriptConsoleDecorator('''«it.fileRepresentationInConsole»''',it) |
258 | ] | 259 | ] |
259 | ) | 260 | ) |
260 | } | 261 | } |
261 | if(!gmlRepresentations.empty) { | 262 | if(!gmlRepresentations.empty) { |
262 | console.writeMessage( | 263 | console.writeMessage( |
263 | '''Visualisations: «FOR f : gmlRepresentations»#«ENDFOR»''', | 264 | '''Visualisations: «FOR f : gmlRepresentations.filterNull»#«ENDFOR»''', |
264 | "#", | 265 | "#", |
265 | gmlRepresentations.map[ | 266 | gmlRepresentations.filterNull.map[ |
266 | new ScriptConsoleDecorator('''«it.fileRepresentationInConsole»''',it) | 267 | new ScriptConsoleDecorator('''«it.fileRepresentationInConsole»''',it) |
267 | ] | 268 | ] |
268 | ) | 269 | ) |
269 | } | 270 | } |
270 | if(!dotRepresentations.empty) { | 271 | if(!dotRepresentations.empty) { |
271 | console.writeMessage( | 272 | console.writeMessage( |
272 | '''Visualisations: «FOR f : dotRepresentations»#«ENDFOR»''', | 273 | '''Visualisations: «FOR f : dotRepresentations.filterNull»#«ENDFOR»''', |
273 | "#", | 274 | "#", |
274 | dotRepresentations.map[ | 275 | dotRepresentations.filterNull.map[ |
275 | new ScriptConsoleDecorator('''«it.fileRepresentationInConsole»''',it) | 276 | new ScriptConsoleDecorator('''«it.fileRepresentationInConsole»''',it) |
276 | ] | 277 | ] |
277 | ) | 278 | ) |
278 | } | 279 | } |
279 | } else { | 280 | } else { |
280 | monitor.worked(solverConfig.solutionScope.numberOfRequiredSolution*100) | 281 | visualisationProgressMonitor.worked(1.0) |
281 | } | 282 | } |
282 | solutionVisualisationTime = System.nanoTime - solutionVisualisationTime | 283 | solutionVisualisationTime = System.nanoTime - solutionVisualisationTime |
283 | 284 | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend index 4f1a8f38..dcaf74cd 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend | |||
@@ -35,6 +35,7 @@ import org.eclipse.emf.ecore.EClass | |||
35 | import org.eclipse.xtend.lib.annotations.Data | 35 | import org.eclipse.xtend.lib.annotations.Data |
36 | 36 | ||
37 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 37 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
38 | import java.util.HashSet | ||
38 | 39 | ||
39 | @Data class KnownElements { | 40 | @Data class KnownElements { |
40 | val Map<Type,Set<DefinedElement>> knownElementsByType | 41 | val Map<Type,Set<DefinedElement>> knownElementsByType |
@@ -58,11 +59,18 @@ class ScopeLoader { | |||
58 | 59 | ||
59 | def protected initialiseknownElements(LogicProblem p, TypeScopes s) { | 60 | def protected initialiseknownElements(LogicProblem p, TypeScopes s) { |
60 | val Map<Type,Set<DefinedElement>> res = new HashMap | 61 | val Map<Type,Set<DefinedElement>> res = new HashMap |
62 | |||
63 | // 1. fill map with every types | ||
64 | for(t : p.types) { | ||
65 | res.put(t,new HashSet) | ||
66 | } | ||
67 | |||
68 | // 2. fill map with every objects | ||
61 | for(definedType : p.types.filter(TypeDefinition)) { | 69 | for(definedType : p.types.filter(TypeDefinition)) { |
62 | val supertypes = definedType.<Type>transitiveClosureStar[x|x.supertypes] | 70 | val supertypes = definedType.<Type>transitiveClosureStar[x|x.supertypes] |
63 | for(supertype : supertypes) { | 71 | for(supertype : supertypes) { |
64 | for(element : definedType.elements) { | 72 | for(element : definedType.elements) { |
65 | res.putOrAddToSet(supertype,element) | 73 | res.get(supertype).add(element) |
66 | } | 74 | } |
67 | } | 75 | } |
68 | } | 76 | } |
@@ -107,7 +115,7 @@ class ScopeLoader { | |||
107 | updateLowerLimit( | 115 | updateLowerLimit( |
108 | scope.setsNew, | 116 | scope.setsNew, |
109 | known, | 117 | known, |
110 | type.lookup(aggregated.minNewElementsByType), | 118 | aggregated.minNewElementsByType.get(type), |
111 | getLowerLimit(scope.number) | 119 | getLowerLimit(scope.number) |
112 | ) | 120 | ) |
113 | ) | 121 | ) |
@@ -115,7 +123,7 @@ class ScopeLoader { | |||
115 | updateUpperLimit( | 123 | updateUpperLimit( |
116 | scope.setsNew, | 124 | scope.setsNew, |
117 | known, | 125 | known, |
118 | type.lookup(aggregated.minNewElementsByType), | 126 | aggregated.maxNewElementsByType.get(type), |
119 | getUpperLimit(scope.number) | 127 | getUpperLimit(scope.number) |
120 | ) | 128 | ) |
121 | ) | 129 | ) |
@@ -128,6 +136,9 @@ class ScopeLoader { | |||
128 | val number = scope.number | 136 | val number = scope.number |
129 | if(number instanceof IntEnumberation) { | 137 | if(number instanceof IntEnumberation) { |
130 | addToKnownCollection(aggregated.knownIntegers,number.entry,scope.isSetsNew,inconsistencies) | 138 | addToKnownCollection(aggregated.knownIntegers,number.entry,scope.isSetsNew,inconsistencies) |
139 | if(!scope.isSetsNew) { | ||
140 | aggregated.maxNewIntegers = 0 | ||
141 | } | ||
131 | } else { | 142 | } else { |
132 | aggregated.minNewIntegers = updateLowerLimit(scope.isSetsNew,aggregated.knownIntegers.size,aggregated.minNewIntegers,number.lowerLimit) | 143 | aggregated.minNewIntegers = updateLowerLimit(scope.isSetsNew,aggregated.knownIntegers.size,aggregated.minNewIntegers,number.lowerLimit) |
133 | aggregated.maxNewIntegers = updateLowerLimit(scope.isSetsNew,aggregated.knownIntegers.size,aggregated.maxNewIntegers,number.upperLimit) | 144 | aggregated.maxNewIntegers = updateLowerLimit(scope.isSetsNew,aggregated.knownIntegers.size,aggregated.maxNewIntegers,number.upperLimit) |
@@ -139,6 +150,9 @@ class ScopeLoader { | |||
139 | if(number instanceof RealEnumeration) { | 150 | if(number instanceof RealEnumeration) { |
140 | val x = number.entry; | 151 | val x = number.entry; |
141 | <BigDecimal>addToKnownCollection(aggregated.knownReals,x,scope.isSetsNew,inconsistencies) | 152 | <BigDecimal>addToKnownCollection(aggregated.knownReals,x,scope.isSetsNew,inconsistencies) |
153 | if(!scope.isSetsNew) { | ||
154 | aggregated.maxNewReals = 0 | ||
155 | } | ||
142 | } else { | 156 | } else { |
143 | aggregated.minNewReals = updateLowerLimit(scope.isSetsNew,aggregated.knownReals.size,aggregated.minNewReals,number.lowerLimit) | 157 | aggregated.minNewReals = updateLowerLimit(scope.isSetsNew,aggregated.knownReals.size,aggregated.minNewReals,number.lowerLimit) |
144 | aggregated.maxNewReals = updateLowerLimit(scope.isSetsNew,aggregated.knownReals.size,aggregated.maxNewReals,number.upperLimit) | 158 | aggregated.maxNewReals = updateLowerLimit(scope.isSetsNew,aggregated.knownReals.size,aggregated.maxNewReals,number.upperLimit) |
@@ -148,6 +162,9 @@ class ScopeLoader { | |||
148 | val number = scope.number | 162 | val number = scope.number |
149 | if(number instanceof StringEnumeration) { | 163 | if(number instanceof StringEnumeration) { |
150 | <String>addToKnownCollection(aggregated.knownStrings,number.entry,scope.isSetsNew,inconsistencies) | 164 | <String>addToKnownCollection(aggregated.knownStrings,number.entry,scope.isSetsNew,inconsistencies) |
165 | if(!scope.isSetsNew) { | ||
166 | aggregated.maxNewStrings = 0 | ||
167 | } | ||
151 | } else { | 168 | } else { |
152 | aggregated.minNewStrings = updateLowerLimit(scope.isSetsNew,aggregated.knownStrings.size,aggregated.minNewStrings,number.lowerLimit) | 169 | aggregated.minNewStrings = updateLowerLimit(scope.isSetsNew,aggregated.knownStrings.size,aggregated.minNewStrings,number.lowerLimit) |
153 | aggregated.maxNewStrings = updateLowerLimit(scope.isSetsNew,aggregated.knownStrings.size,aggregated.maxNewStrings,number.upperLimit) | 170 | aggregated.maxNewStrings = updateLowerLimit(scope.isSetsNew,aggregated.knownStrings.size,aggregated.maxNewStrings,number.upperLimit) |
@@ -166,19 +183,21 @@ class ScopeLoader { | |||
166 | } | 183 | } |
167 | } | 184 | } |
168 | 185 | ||
169 | def updateLowerLimit(boolean isAdditional, int known, int original, int value) { | 186 | def updateLowerLimit(boolean isAdditional, int known, Integer original, int value) { |
187 | val o = if(original === null) {0} else {original} | ||
170 | if(isAdditional) { | 188 | if(isAdditional) { |
171 | return Math.max(original,value) | 189 | return Math.max(o,value) |
172 | } else { | 190 | } else { |
173 | return Math.max(original,value-known) | 191 | return Math.max(o,value-known) |
174 | } | 192 | } |
175 | } | 193 | } |
176 | def updateUpperLimit(boolean isAdditional, int known, int original, int value) { | 194 | def updateUpperLimit(boolean isAdditional, int known, Integer original, int value) { |
195 | val o = if(original === null) {Integer.MAX_VALUE} else {original} | ||
177 | if(isAdditional) { | 196 | if(isAdditional) { |
178 | return Math.min(original,value) | 197 | return Math.min(o,value) |
179 | } else { | 198 | } else { |
180 | val target = if(value == Integer.MAX_VALUE) { Integer.MAX_VALUE } else {value-known} | 199 | val target = if(value == Integer.MAX_VALUE) { Integer.MAX_VALUE } else {value-known} |
181 | return Math.min(original,target) | 200 | return Math.min(o,target) |
182 | } | 201 | } |
183 | } | 202 | } |
184 | 203 | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend index b9813040..c9ec68bb 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend | |||
@@ -102,12 +102,12 @@ class ScriptExecutor { | |||
102 | /** | 102 | /** |
103 | * Mapping time = 100 | 103 | * Mapping time = 100 |
104 | * Solving = 1000 * runs | 104 | * Solving = 1000 * runs |
105 | * Visualisation = runs * number * 100 | 105 | * Visualisation = 1000 * runs |
106 | */ | 106 | */ |
107 | def protected dispatch getTotalWork(GenerationTask task) { | 107 | def protected dispatch getTotalWork(GenerationTask task) { |
108 | val runs = if(task.runSpecified) { task.runs } else { 1 } | 108 | val runs = if(task.runSpecified) { task.runs } else { 1 } |
109 | val number = if(task.numberSpecified) { task.number } else { 1 } | 109 | val number = if(task.numberSpecified) { task.number } else { 1 } |
110 | return 100 + runs*1000 +runs*number*100 | 110 | return 100 + runs*1000 +runs*1000 |
111 | } | 111 | } |
112 | def protected dispatch getTotalWork(Task task) { | 112 | def protected dispatch getTotalWork(Task task) { |
113 | throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''') | 113 | throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''') |
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend index e6f42709..a9573fbf 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend | |||
@@ -93,7 +93,11 @@ class SolverLoader { | |||
93 | } | 93 | } |
94 | 94 | ||
95 | def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { | 95 | def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { |
96 | parameters.getAsBoolean("randomise",console).ifPresent[config.randomise = runIndex] | 96 | parameters.getAsBoolean("randomize",console).ifPresent[ |
97 | if(it) { | ||
98 | config.randomise = runIndex-1 | ||
99 | } | ||
100 | ] | ||
97 | } | 101 | } |
98 | def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { | 102 | def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { |
99 | 103 | ||