diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner')
4 files changed, 22 insertions, 18 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend index f6b0b4a5..1eb6442b 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | |||
@@ -62,7 +62,7 @@ class AlloySolver extends LogicReasoner{ | |||
62 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) | 62 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) |
63 | alloyConfig.progressMonitor.workedSearchFinished | 63 | alloyConfig.progressMonitor.workedSearchFinished |
64 | 64 | ||
65 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | 65 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolutions,result2,forwardTrace,transformationTime) |
66 | alloyConfig.progressMonitor.workedBackwardTransformationFinished | 66 | alloyConfig.progressMonitor.workedBackwardTransformationFinished |
67 | //val solverFinish = System.currentTimeMillis-solverStart | 67 | //val solverFinish = System.currentTimeMillis-solverStart |
68 | // Finish: Solving Alloy problem | 68 | // Finish: Solving Alloy problem |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend index 2efd6b29..328ca176 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | |||
@@ -9,7 +9,7 @@ class Alloy2LogicMapper { | |||
9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { | 9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { |
10 | val models = monitoredAlloySolution.aswers.map[it.key].toList | 10 | val models = monitoredAlloySolution.aswers.map[it.key].toList |
11 | 11 | ||
12 | if(!monitoredAlloySolution.finishedBeforeTimeout) { | 12 | if(models.empty || !monitoredAlloySolution.finishedBeforeTimeout) { |
13 | return createInsuficientResourcesResult => [ | 13 | return createInsuficientResourcesResult => [ |
14 | it.problem = problem | 14 | it.problem = problem |
15 | it.representation += models | 15 | it.representation += models |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend index 9b4265b9..451aad6e 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | |||
@@ -101,15 +101,8 @@ class AlloyHandler { | |||
101 | try{ | 101 | try{ |
102 | answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS) | 102 | answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS) |
103 | finished = true | 103 | finished = true |
104 | } catch (TimeoutException ex) { | 104 | } catch (TimeoutException | InterruptedException | ExecutionException e) { |
105 | // handle the timeout | 105 | future.cancel(true) |
106 | } catch (InterruptedException e) { | ||
107 | // handle the interrupts | ||
108 | } catch (ExecutionException e) { | ||
109 | // handle other exceptions | ||
110 | } finally { | ||
111 | future.cancel(true); | ||
112 | |||
113 | answers = callable.partialAnswers | 106 | answers = callable.partialAnswers |
114 | finished = false | 107 | finished = false |
115 | } | 108 | } |
@@ -195,7 +188,7 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | |||
195 | } else { | 188 | } else { |
196 | lastAnswer = lastAnswer.next | 189 | lastAnswer = lastAnswer.next |
197 | } | 190 | } |
198 | configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) | 191 | configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolutions) |
199 | 192 | ||
200 | val runtime = System.currentTimeMillis -startTime | 193 | val runtime = System.currentTimeMillis -startTime |
201 | synchronized(this) { | 194 | synchronized(this) { |
@@ -212,8 +205,8 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | |||
212 | } | 205 | } |
213 | 206 | ||
214 | def hasEnoughSolution(List<?> answers) { | 207 | def hasEnoughSolution(List<?> answers) { |
215 | if(configuration.solutionScope.numberOfRequiredSolution < 0) return false | 208 | if(configuration.solutionScope.numberOfRequiredSolutions < 0) return false |
216 | else return answers.size() == configuration.solutionScope.numberOfRequiredSolution | 209 | else return answers.size() == configuration.solutionScope.numberOfRequiredSolutions |
217 | } | 210 | } |
218 | 211 | ||
219 | public def getPartialAnswers() { | 212 | public def getPartialAnswers() { |
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 494197bc..b74017d8 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 | |||
@@ -9,8 +9,12 @@ import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString | |||
9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | 9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm |
10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | 10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
12 | import java.util.List | 14 | import java.util.List |
13 | 15 | ||
16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
17 | |||
14 | class RunCommandMapper { | 18 | class RunCommandMapper { |
15 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 19 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
16 | val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | 20 | val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; |
@@ -89,16 +93,18 @@ class RunCommandMapper { | |||
89 | ] | 93 | ] |
90 | 94 | ||
91 | for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) { | 95 | for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) { |
92 | val limit = upperLimit.value | 96 | val type = upperLimit.key |
97 | val limit = upperLimit.value + getExistingCount(type) | ||
93 | if(limit != LogicSolverConfiguration::Unlimited) { | 98 | if(limit != LogicSolverConfiguration::Unlimited) { |
94 | this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace) | 99 | this.typeScopeMapping.addUpperMultiplicity(specification,type,limit,mapper,trace) |
95 | } | 100 | } |
96 | } | 101 | } |
97 | 102 | ||
98 | for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) { | 103 | for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) { |
99 | val limit = lowerLimit.value | 104 | val type = lowerLimit.key |
105 | val limit = lowerLimit.value + getExistingCount(type) | ||
100 | if(limit != 0) { | 106 | if(limit != 0) { |
101 | this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace) | 107 | this.typeScopeMapping.addLowerMultiplicity(specification,type,limit,mapper,trace) |
102 | } | 108 | } |
103 | } | 109 | } |
104 | 110 | ||
@@ -106,6 +112,11 @@ class RunCommandMapper { | |||
106 | setStringScope(specification,config,specification.runCommand) | 112 | setStringScope(specification,config,specification.runCommand) |
107 | } | 113 | } |
108 | 114 | ||
115 | private def getExistingCount(Type type) { | ||
116 | val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet | ||
117 | existing.size | ||
118 | } | ||
119 | |||
109 | protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { | 120 | protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { |
110 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | 121 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { |
111 | throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') | 122 | throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') |