aboutsummaryrefslogtreecommitdiffstats
path: root/Application/hu.bme.mit.inf.dslreasoner.application
diff options
context:
space:
mode:
Diffstat (limited to 'Application/hu.bme.mit.inf.dslreasoner.application')
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/EclipseBasedProgressMonitor.xtend8
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend23
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend37
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend4
-rw-r--r--Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend6
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
35import org.eclipse.xtend.lib.annotations.Data 35import org.eclipse.xtend.lib.annotations.Data
36 36
37import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 37import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
38import 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
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-04 01:32:36 +0000