diff options
author | 2017-07-02 23:34:27 +0200 | |
---|---|---|
committer | 2017-07-02 23:34:27 +0200 | |
commit | f00ce77fdc3a1417ddfd833f122b64ecef80d7d6 (patch) | |
tree | 2a26b61a43576f58ed4c35680bd47fa3c15df3d8 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src | |
parent | Multiple model with interpretations (diff) | |
download | VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.tar.gz VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.tar.zst VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.zip |
Alloy implementation of multiple model generation
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src')
4 files changed, 178 insertions, 70 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 7dfc3161..d0c7d320 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 | |||
@@ -3,8 +3,10 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper | 3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper |
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler | 4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler |
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation | 5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation |
6 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes | ||
6 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper | 7 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper |
7 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace | 8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace |
9 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes | ||
8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution | 10 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution |
9 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated | 11 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated |
10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage | 12 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage |
@@ -14,9 +16,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | |||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
16 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
17 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes | ||
18 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes | ||
19 | import org.eclipse.emf.common.util.URI | ||
20 | 19 | ||
21 | class AlloySolver extends LogicReasoner{ | 20 | class AlloySolver extends LogicReasoner{ |
22 | 21 | ||
@@ -33,40 +32,56 @@ class AlloySolver extends LogicReasoner{ | |||
33 | val fileName = "problem.als" | 32 | val fileName = "problem.als" |
34 | 33 | ||
35 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | 34 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { |
35 | val alloyConfig = configuration.asConfig | ||
36 | |||
37 | // Start: Logic -> Alloy mapping | ||
38 | val transformationStart = System.currentTimeMillis | ||
39 | val result = forwardMapper.transformProblem(problem,alloyConfig) | ||
40 | val alloyProblem = result.output | ||
41 | val forwardTrace = result.trace | ||
42 | |||
43 | var String fileURI = null; | ||
44 | var String alloyCode = null; | ||
45 | if(alloyConfig.writeToFile) { | ||
46 | fileURI = workspace.writeModel(alloyProblem,fileName).toFileString | ||
47 | } else { | ||
48 | alloyCode = workspace.writeModelToString(alloyProblem,fileName) | ||
49 | } | ||
50 | val transformationTime = System.currentTimeMillis - transformationStart | ||
51 | // Finish: Logic -> Alloy mapping | ||
52 | |||
53 | |||
54 | // Start: Solving Alloy problem | ||
55 | val solverStart = System.currentTimeMillis | ||
56 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode) | ||
57 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | ||
58 | val solverFinish = System.currentTimeMillis-solverStart | ||
59 | // Finish: Solving Alloy problem | ||
60 | |||
61 | if(alloyConfig.writeToFile) workspace.deactivateModel(fileName) | ||
62 | |||
63 | return logicResult | ||
64 | } | ||
65 | |||
66 | def asConfig(LogicSolverConfiguration configuration) { | ||
36 | if(configuration instanceof AlloySolverConfiguration) { | 67 | if(configuration instanceof AlloySolverConfiguration) { |
37 | val transformationStart = System.currentTimeMillis | 68 | return configuration |
38 | val result = forwardMapper.transformProblem(problem,configuration) | 69 | } else { |
39 | val alloyProblem = result.output | 70 | throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''') |
40 | 71 | } | |
41 | /*val x = alloyProblem.eAllContents.filter(ALSFunctionCall).filter[it.referredDefinition == null].toList | ||
42 | println(x)*/ | ||
43 | val forwardTrace = result.trace | ||
44 | |||
45 | var String fileURI = null; | ||
46 | var String alloyCode = null; | ||
47 | if(configuration.writeToFile) { | ||
48 | fileURI = workspace.writeModel(alloyProblem,fileName).toFileString | ||
49 | } else { | ||
50 | alloyCode = workspace.writeModelToString(alloyProblem,fileName) | ||
51 | } | ||
52 | |||
53 | //val alloyCode = workspace.readText(fileName) | ||
54 | //val FunctionWithTimeout<MonitoredAlloySolution> call = new FunctionWithTimeout[] | ||
55 | |||
56 | val transformationTime = System.currentTimeMillis - transformationStart | ||
57 | val result2 = handler.callSolver(alloyProblem,workspace,configuration,fileURI,alloyCode) | ||
58 | workspace.deactivateModel(fileName) | ||
59 | val logicResult = backwardMapper.transformOutput(problem,result2,forwardTrace,transformationTime) | ||
60 | return logicResult | ||
61 | } else throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''') | ||
62 | } | 72 | } |
63 | 73 | ||
64 | override getInterpretation(ModelResult modelResult) { | 74 | override getInterpretations(ModelResult modelResult) { |
65 | return new AlloyModelInterpretation( | 75 | val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] |
66 | new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, | 76 | val res = answers.map [ |
67 | (modelResult.representation as MonitoredAlloySolution).solution, | 77 | new AlloyModelInterpretation( |
68 | forwardMapper, | 78 | new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, |
69 | modelResult.trace as Logic2AlloyLanguageMapperTrace | 79 | it, |
70 | ); | 80 | forwardMapper, |
81 | modelResult.trace as Logic2AlloyLanguageMapperTrace | ||
82 | ) | ||
83 | ] | ||
84 | |||
85 | return res | ||
71 | } | 86 | } |
72 | } \ No newline at end of file | 87 | } \ No newline at end of file |
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 637752b0..7db9e0ea 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 | |||
@@ -6,28 +6,30 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | |||
6 | class Alloy2LogicMapper { | 6 | class Alloy2LogicMapper { |
7 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | 7 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE |
8 | 8 | ||
9 | public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { | 9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { |
10 | if(solution == null) { | 10 | val models = monitoredAlloySolution.aswers.map[it.key].toList |
11 | |||
12 | if(monitoredAlloySolution.finishedBeforeTimeout) { | ||
11 | return createInsuficientResourcesResult => [ | 13 | return createInsuficientResourcesResult => [ |
12 | it.problem = problem | 14 | it.problem = problem |
13 | it.statistics = transformStatistics(solution,transformationTime) | 15 | it.representation += models |
16 | it.trace = trace | ||
17 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
14 | ] | 18 | ] |
15 | } else { | 19 | } else { |
16 | val logicResult = solution.solution | 20 | if(models.last.satisfiable || requiredNumberOfSolution == -1) { |
17 | if(logicResult.satisfiable) { | ||
18 | return createModelResult => [ | 21 | return createModelResult => [ |
19 | it.problem = problem | 22 | it.problem = problem |
20 | it.representation += solution | 23 | it.representation += models |
21 | it.maxInteger = logicResult.max | ||
22 | it.minInteger = logicResult.min | ||
23 | it.trace = trace | 24 | it.trace = trace |
24 | it.statistics = transformStatistics(solution,transformationTime) | 25 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) |
25 | ] | 26 | ] |
26 | } else { | 27 | } else { |
27 | return createInconsistencyResult => [ | 28 | return createInconsistencyResult => [ |
28 | it.problem = problem | 29 | it.problem = problem |
29 | //trace? | 30 | it.representation += models |
30 | it.statistics = transformStatistics(solution,transformationTime) | 31 | it.trace = trace |
32 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
31 | ] | 33 | ] |
32 | } | 34 | } |
33 | } | 35 | } |
@@ -36,13 +38,29 @@ class Alloy2LogicMapper { | |||
36 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { | 38 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { |
37 | createStatistics => [ | 39 | createStatistics => [ |
38 | it.transformationTime = transformationTime as int | 40 | it.transformationTime = transformationTime as int |
39 | if(solution != null) { | 41 | for(solutionIndex : 0..<solution.aswers.size) { |
40 | it.solverTime = solution.runtimeTime as int | 42 | val solutionTime = solution.aswers.get(solutionIndex).value |
41 | it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [ | 43 | it.entries+= createIntStatisticEntry => [ |
42 | it.name = "KoodkodToCNFTransformationTime" | 44 | it.name = '''Answer«solutionIndex»Time''' |
43 | it.value = solution.getKodkodTime as int | 45 | it.value = solutionTime.intValue |
44 | ] | 46 | ] |
45 | } | 47 | } |
48 | it.entries+= createIntStatisticEntry => [ | ||
49 | it.name = "Alloy2KodKodTransformationTime" | ||
50 | it.value = solution.kodkodTime as int | ||
51 | ] | ||
52 | it.entries+= createIntStatisticEntry => [ | ||
53 | it.name = "Alloy2KodKodTransformationTime" | ||
54 | it.value = solution.kodkodTime as int | ||
55 | ] | ||
56 | it.entries+= createStringStatisticEntry => [ | ||
57 | it.name = "warnings" | ||
58 | it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]''' | ||
59 | ] | ||
46 | ] | 60 | ] |
47 | } | 61 | } |
62 | |||
63 | def sum(Iterable<Long> ints) { | ||
64 | ints.reduce[p1, p2|p1+p2] | ||
65 | } | ||
48 | } \ No newline at end of file | 66 | } \ No newline at end of file |
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 6bac4130..17220776 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 | |||
@@ -21,6 +21,11 @@ import org.eclipse.emf.common.CommonPlugin | |||
21 | import java.util.ArrayList | 21 | import java.util.ArrayList |
22 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | 22 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument |
23 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 23 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration |
24 | import com.google.common.util.concurrent.SimpleTimeLimiter | ||
25 | import java.util.concurrent.Callable | ||
26 | import java.util.concurrent.TimeUnit | ||
27 | import com.google.common.util.concurrent.UncheckedTimeoutException | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
24 | 29 | ||
25 | class AlloySolverException extends Exception{ | 30 | class AlloySolverException extends Exception{ |
26 | new(String s) { super(s) } | 31 | new(String s) { super(s) } |
@@ -34,9 +39,8 @@ class AlloySolverException extends Exception{ | |||
34 | List<String> warnings | 39 | List<String> warnings |
35 | List<String> debugs | 40 | List<String> debugs |
36 | long kodkodTime | 41 | long kodkodTime |
37 | long runtimeTime | 42 | val List<Pair<A4Solution, Long>> aswers |
38 | 43 | val boolean finishedBeforeTimeout | |
39 | A4Solution solution | ||
40 | } | 44 | } |
41 | 45 | ||
42 | class AlloyHandler { | 46 | class AlloyHandler { |
@@ -63,6 +67,7 @@ class AlloyHandler { | |||
63 | if(configuration.solver.externalSolver) { | 67 | if(configuration.solver.externalSolver) { |
64 | it.solverDirectory = configuration.solverPath | 68 | it.solverDirectory = configuration.solverPath |
65 | } | 69 | } |
70 | //it.inferPartialInstance | ||
66 | it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString | 71 | it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString |
67 | ] | 72 | ] |
68 | 73 | ||
@@ -70,8 +75,8 @@ class AlloyHandler { | |||
70 | var Command command = null; | 75 | var Command command = null; |
71 | var CompModule compModule = null | 76 | var CompModule compModule = null |
72 | 77 | ||
78 | // Start: Alloy -> Kodkod | ||
73 | val kodkodTransformStart = System.currentTimeMillis(); | 79 | val kodkodTransformStart = System.currentTimeMillis(); |
74 | |||
75 | try { | 80 | try { |
76 | if(configuration.writeToFile) { | 81 | if(configuration.writeToFile) { |
77 | compModule = CompUtil.parseEverything_fromFile(reporter,null,path) | 82 | compModule = CompUtil.parseEverything_fromFile(reporter,null,path) |
@@ -85,23 +90,26 @@ class AlloyHandler { | |||
85 | throw new AlloySolverException(e.message,warnings,e) | 90 | throw new AlloySolverException(e.message,warnings,e) |
86 | } | 91 | } |
87 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | 92 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart |
93 | // Finish: Alloy -> Kodkod | ||
88 | 94 | ||
89 | //Execute | 95 | val limiter = new SimpleTimeLimiter |
90 | var A4Solution answer = null; | 96 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration.solutionScope.numberOfRequiredSolution) |
91 | try { | 97 | var List<Pair<A4Solution, Long>> answers |
92 | answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | 98 | var boolean finished |
93 | }catch(Exception e) { | 99 | if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { |
94 | warnings +=e.message | 100 | answers = callable.call |
95 | } | 101 | finished = true |
96 | |||
97 | var long runtimeFromAnswer; | ||
98 | if(runtime.empty) { | ||
99 | runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish) | ||
100 | } else { | 102 | } else { |
101 | runtimeFromAnswer = runtime.head | 103 | try{ |
104 | answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) | ||
105 | finished = true | ||
106 | } catch (UncheckedTimeoutException e) { | ||
107 | answers = callable.partialAnswers | ||
108 | finished = false | ||
109 | } | ||
102 | } | 110 | } |
103 | 111 | ||
104 | return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer) | 112 | new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) |
105 | } | 113 | } |
106 | 114 | ||
107 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap | 115 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap |
@@ -138,6 +146,73 @@ class AlloyHandler { | |||
138 | } | 146 | } |
139 | } | 147 | } |
140 | 148 | ||
149 | class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | ||
150 | |||
151 | val List<String> warnings | ||
152 | val List<String> debugs | ||
153 | val A4Reporter reporter | ||
154 | val A4Options options | ||
155 | |||
156 | val Command command | ||
157 | val CompModule compModule | ||
158 | val int numberOfRequiredSolution | ||
159 | |||
160 | val List<Pair<A4Solution,Long>> answers = new LinkedList() | ||
161 | |||
162 | new(List<String> warnings, | ||
163 | List<String> debugs, | ||
164 | A4Reporter reporter, | ||
165 | A4Options options, | ||
166 | Command command, | ||
167 | CompModule compModule, | ||
168 | int numberOfRequiredSolution) | ||
169 | { | ||
170 | this.warnings = warnings | ||
171 | this.debugs = debugs | ||
172 | this.reporter = reporter | ||
173 | this.options = options | ||
174 | this.command = command | ||
175 | this.compModule = compModule | ||
176 | this.numberOfRequiredSolution = numberOfRequiredSolution | ||
177 | } | ||
178 | |||
179 | override call() throws Exception { | ||
180 | val startTime = System.currentTimeMillis | ||
181 | |||
182 | // Start: Execute | ||
183 | var A4Solution lastAnswer = null | ||
184 | try { | ||
185 | do{ | ||
186 | if(lastAnswer == null) { | ||
187 | lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | ||
188 | } else { | ||
189 | lastAnswer = lastAnswer.next | ||
190 | } | ||
191 | |||
192 | val runtime = System.currentTimeMillis -startTime | ||
193 | synchronized(this) { | ||
194 | answers += lastAnswer->runtime | ||
195 | } | ||
196 | println( answers.size ) | ||
197 | } while(lastAnswer.satisfiable != false && hasEnoughSolution(answers)) | ||
198 | |||
199 | }catch(Exception e) { | ||
200 | warnings +=e.message | ||
201 | } | ||
202 | // Finish: execute | ||
203 | return answers | ||
204 | } | ||
205 | |||
206 | def hasEnoughSolution(List<?> answers) { | ||
207 | if(numberOfRequiredSolution < 0) return false | ||
208 | else return answers.size < numberOfRequiredSolution | ||
209 | } | ||
210 | |||
211 | public def getPartialAnswers() { | ||
212 | return answers | ||
213 | } | ||
214 | } | ||
215 | |||
141 | @Data class SolverConfiguration { | 216 | @Data class SolverConfiguration { |
142 | AlloyBackendSolver backedSolver | 217 | AlloyBackendSolver backedSolver |
143 | String path | 218 | String path |
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 23b9027f..65fdcfdf 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 | |||
@@ -277,7 +277,7 @@ class Logic2AlloyLanguageMapper { | |||
277 | it.typeScopes+= createALSSigScope => [ | 277 | it.typeScopes+= createALSSigScope => [ |
278 | it.type= typeMapper.getUndefinedSupertype(trace) | 278 | it.type= typeMapper.getUndefinedSupertype(trace) |
279 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | 279 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) |
280 | //it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements) | 280 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) |
281 | ] | 281 | ] |
282 | if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( | 282 | if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( |
283 | '''An integer scope have to be specified for Alloy!''') | 283 | '''An integer scope have to be specified for Alloy!''') |