diff options
author | 2019-10-25 04:15:39 -0400 | |
---|---|---|
committer | 2020-06-07 19:43:49 -0400 | |
commit | 32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f (patch) | |
tree | 0e67f50df5b4d9a42f0075e1e19be988eae59bf9 /Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit | |
parent | mid-measurement push (diff) | |
download | VIATRA-Generator-32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f.tar.gz VIATRA-Generator-32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f.tar.zst VIATRA-Generator-32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f.zip |
VAMPIRE: post-submission push
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit')
21 files changed, 2656 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend new file mode 100644 index 00000000..b16ed27f --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend | |||
@@ -0,0 +1,28 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
4 | |||
5 | class AlloySolverConfiguration extends LogicSolverConfiguration { | ||
6 | public var int symmetry = 20 // by default | ||
7 | public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J | ||
8 | public var TypeMappingTechnique typeMapping = TypeMappingTechnique.InheritanceAndHorizontal | ||
9 | public var randomise = 0 | ||
10 | } | ||
11 | |||
12 | enum AlloyBackendSolver { | ||
13 | BerkMinPIPE, | ||
14 | SpearPIPE, | ||
15 | MiniSatJNI, | ||
16 | MiniSatProverJNI, | ||
17 | LingelingJNI, | ||
18 | PLingelingJNI, | ||
19 | GlucoseJNI, | ||
20 | CryptoMiniSatJNI, | ||
21 | SAT4J, | ||
22 | CNF, | ||
23 | KodKod | ||
24 | } | ||
25 | |||
26 | enum TypeMappingTechnique { | ||
27 | FilteredTypes, InheritanceAndHorizontal | ||
28 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend new file mode 100644 index 00000000..9cfa7391 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | |||
@@ -0,0 +1,91 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper | ||
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler | ||
6 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation | ||
7 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper | ||
8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace | ||
9 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes | ||
10 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated | ||
11 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
19 | |||
20 | class AlloySolver extends LogicReasoner{ | ||
21 | |||
22 | new() { | ||
23 | AlloyLanguagePackage.eINSTANCE.eClass | ||
24 | val x = new AlloyLanguageStandaloneSetupGenerated | ||
25 | x.createInjectorAndDoEMFRegistration | ||
26 | } | ||
27 | |||
28 | val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes) | ||
29 | val AlloyHandler handler = new AlloyHandler | ||
30 | val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper | ||
31 | |||
32 | val fileName = "problem.als" | ||
33 | |||
34 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | ||
35 | val alloyConfig = configuration.asConfig | ||
36 | val writeFile = ( | ||
37 | configuration.documentationLevel===DocumentationLevel::NORMAL || | ||
38 | configuration.documentationLevel===DocumentationLevel::FULL) | ||
39 | |||
40 | // Start: Logic -> Alloy mapping | ||
41 | val transformationStart = System.currentTimeMillis | ||
42 | val result = forwardMapper.transformProblem(problem,alloyConfig) | ||
43 | val alloyProblem = result.output | ||
44 | val forwardTrace = result.trace | ||
45 | |||
46 | //var String fileURI = null; | ||
47 | var String alloyCode = workspace.writeModelToString(alloyProblem,fileName) | ||
48 | if(writeFile) { | ||
49 | workspace.writeModel(alloyProblem,fileName) | ||
50 | } | ||
51 | val transformationTime = System.currentTimeMillis - transformationStart | ||
52 | alloyConfig.progressMonitor.workedForwardTransformation | ||
53 | // Finish: Logic -> Alloy mapping | ||
54 | |||
55 | // Start: Solving Alloy problem | ||
56 | //val solverStart = System.currentTimeMillis | ||
57 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) | ||
58 | alloyConfig.progressMonitor.workedSearchFinished | ||
59 | |||
60 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | ||
61 | alloyConfig.progressMonitor.workedBackwardTransformationFinished | ||
62 | //val solverFinish = System.currentTimeMillis-solverStart | ||
63 | // Finish: Solving Alloy problem | ||
64 | |||
65 | //logicResult.statistics = | ||
66 | |||
67 | return logicResult | ||
68 | } | ||
69 | |||
70 | def asConfig(LogicSolverConfiguration configuration) { | ||
71 | if(configuration instanceof AlloySolverConfiguration) { | ||
72 | return configuration | ||
73 | } else { | ||
74 | throw new IllegalArgumentException('''The configuration has to be an «AlloySolverConfiguration.simpleName»!''') | ||
75 | } | ||
76 | } | ||
77 | |||
78 | override getInterpretations(ModelResult modelResult) { | ||
79 | //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] | ||
80 | val sols = modelResult.representation// as List<A4Solution> | ||
81 | //val res = answers.map | ||
82 | sols.map[ | ||
83 | new AlloyModelInterpretation( | ||
84 | forwardMapper.typeMapper.typeInterpreter, | ||
85 | it as A4Solution, | ||
86 | forwardMapper, | ||
87 | modelResult.trace as Logic2AlloyLanguageMapperTrace | ||
88 | ) | ||
89 | ] | ||
90 | } | ||
91 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend new file mode 100644 index 00000000..09b67599 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | |||
@@ -0,0 +1,66 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
5 | |||
6 | class Alloy2LogicMapper { | ||
7 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | ||
8 | |||
9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { | ||
10 | val models = monitoredAlloySolution.aswers.map[it.key].toList | ||
11 | |||
12 | if(!monitoredAlloySolution.finishedBeforeTimeout) { | ||
13 | return createInsuficientResourcesResult => [ | ||
14 | it.problem = problem | ||
15 | it.representation += models | ||
16 | it.trace = trace | ||
17 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
18 | ] | ||
19 | } else { | ||
20 | if(models.last.satisfiable || requiredNumberOfSolution == -1) { | ||
21 | return createModelResult => [ | ||
22 | it.problem = problem | ||
23 | it.representation += models | ||
24 | it.trace = trace | ||
25 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
26 | ] | ||
27 | } else { | ||
28 | return createInconsistencyResult => [ | ||
29 | it.problem = problem | ||
30 | it.representation += models | ||
31 | it.trace = trace | ||
32 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
33 | ] | ||
34 | } | ||
35 | } | ||
36 | } | ||
37 | |||
38 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { | ||
39 | createStatistics => [ | ||
40 | it.transformationTime = transformationTime as int | ||
41 | for(solutionIndex : 0..<solution.aswers.size) { | ||
42 | val solutionTime = solution.aswers.get(solutionIndex).value | ||
43 | it.entries+= createIntStatisticEntry => [ | ||
44 | it.name = '''Answer«solutionIndex»Time''' | ||
45 | it.value = solutionTime.intValue | ||
46 | ] | ||
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 | ] | ||
60 | ] | ||
61 | } | ||
62 | |||
63 | def sum(Iterable<Long> ints) { | ||
64 | ints.reduce[p1, p2|p1+p2] | ||
65 | } | ||
66 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend new file mode 100644 index 00000000..eee2d649 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | |||
@@ -0,0 +1,228 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4.A4Reporter | ||
4 | import edu.mit.csail.sdg.alloy4.Err | ||
5 | import edu.mit.csail.sdg.alloy4.ErrorWarning | ||
6 | import edu.mit.csail.sdg.alloy4compiler.ast.Command | ||
7 | import edu.mit.csail.sdg.alloy4compiler.parser.CompModule | ||
8 | import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil | ||
9 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Options | ||
10 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver | ||
11 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
12 | import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod | ||
13 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | ||
14 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
15 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
17 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
18 | import java.util.ArrayList | ||
19 | import java.util.HashMap | ||
20 | import java.util.LinkedList | ||
21 | import java.util.List | ||
22 | import java.util.Map | ||
23 | import java.util.concurrent.Callable | ||
24 | import java.util.concurrent.ExecutionException | ||
25 | import java.util.concurrent.ExecutorService | ||
26 | import java.util.concurrent.Executors | ||
27 | import java.util.concurrent.TimeUnit | ||
28 | import java.util.concurrent.TimeoutException | ||
29 | import org.eclipse.xtend.lib.annotations.Data | ||
30 | |||
31 | class AlloySolverException extends Exception{ | ||
32 | new(String s) { super(s) } | ||
33 | new(String s, Exception e) { super(s,e) } | ||
34 | new(String s, List<String> errors, Exception e) { | ||
35 | super(s + '\n' + errors.join('\n'), e) | ||
36 | } | ||
37 | } | ||
38 | |||
39 | @Data class MonitoredAlloySolution{ | ||
40 | List<String> warnings | ||
41 | List<String> debugs | ||
42 | long kodkodTime | ||
43 | val List<Pair<A4Solution, Long>> aswers | ||
44 | val boolean finishedBeforeTimeout | ||
45 | } | ||
46 | |||
47 | class AlloyHandler { | ||
48 | |||
49 | //val fileName = "problem.als" | ||
50 | |||
51 | def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { | ||
52 | |||
53 | //Prepare | ||
54 | val warnings = new LinkedList<String> | ||
55 | val debugs = new LinkedList<String> | ||
56 | val runtime = new ArrayList<Long> | ||
57 | val reporter = new A4Reporter() { | ||
58 | override debug(String message) { debugs += message } | ||
59 | override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
60 | override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
61 | override warning(ErrorWarning msg) { warnings += msg.message } | ||
62 | } | ||
63 | |||
64 | val options = new A4Options() => [ | ||
65 | it.symmetry = configuration.symmetry | ||
66 | it.noOverflow = true | ||
67 | it.solver = getSolver(configuration.solver, configuration) | ||
68 | if(configuration.solver.externalSolver) { | ||
69 | it.solverDirectory = configuration.solverPath | ||
70 | } | ||
71 | //it.inferPartialInstance | ||
72 | //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString | ||
73 | ] | ||
74 | |||
75 | // Transform | ||
76 | var Command command = null; | ||
77 | var CompModule compModule = null | ||
78 | |||
79 | // Start: Alloy -> Kodkod | ||
80 | val kodkodTransformStart = System.currentTimeMillis(); | ||
81 | try { | ||
82 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) | ||
83 | if(compModule.allCommands.size != 1) | ||
84 | throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') | ||
85 | command = compModule.allCommands.head | ||
86 | } catch (Err e){ | ||
87 | throw new AlloySolverException(e.message,warnings,e) | ||
88 | } | ||
89 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | ||
90 | // Finish: Alloy -> Kodkod | ||
91 | |||
92 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) | ||
93 | var List<Pair<A4Solution, Long>> answers | ||
94 | var boolean finished | ||
95 | if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { | ||
96 | answers = callable.call | ||
97 | finished = true | ||
98 | } else { | ||
99 | val ExecutorService executor = Executors.newCachedThreadPool(); | ||
100 | val future = executor.submit(callable) | ||
101 | try{ | ||
102 | answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS) | ||
103 | finished = true | ||
104 | } catch (TimeoutException ex) { | ||
105 | // handle the timeout | ||
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 | ||
114 | finished = false | ||
115 | } | ||
116 | } | ||
117 | |||
118 | new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) | ||
119 | } | ||
120 | |||
121 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap | ||
122 | def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { | ||
123 | val config = new SolverConfiguration(backedSolver,path,options) | ||
124 | if(previousSolverConfigurations.containsKey(config)) { | ||
125 | return previousSolverConfigurations.get(config) | ||
126 | } else { | ||
127 | val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' | ||
128 | val newSolver = A4Options.SatSolver.make(id,id,path,options) | ||
129 | previousSolverConfigurations.put(config,newSolver) | ||
130 | return newSolver | ||
131 | } | ||
132 | } | ||
133 | |||
134 | def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { | ||
135 | switch(backedSolver){ | ||
136 | case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE | ||
137 | case SpearPIPE: return A4Options.SatSolver.SpearPIPE | ||
138 | case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI | ||
139 | case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI | ||
140 | case LingelingJNI: return A4Options.SatSolver.LingelingJNI | ||
141 | case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) | ||
142 | case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI | ||
143 | case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI | ||
144 | case SAT4J: return A4Options.SatSolver.SAT4J | ||
145 | case CNF: return A4Options.SatSolver.CNF | ||
146 | case KodKod: return A4Options.SatSolver.KK | ||
147 | } | ||
148 | } | ||
149 | |||
150 | def isExternalSolver(AlloyBackendSolver backedSolver) { | ||
151 | return !(backedSolver == AlloyBackendSolver.SAT4J) | ||
152 | } | ||
153 | } | ||
154 | |||
155 | class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | ||
156 | |||
157 | val List<String> warnings | ||
158 | val List<String> debugs | ||
159 | val A4Reporter reporter | ||
160 | val A4Options options | ||
161 | |||
162 | val Command command | ||
163 | val CompModule compModule | ||
164 | val AlloySolverConfiguration configuration | ||
165 | |||
166 | val List<Pair<A4Solution,Long>> answers = new LinkedList() | ||
167 | |||
168 | new(List<String> warnings, | ||
169 | List<String> debugs, | ||
170 | A4Reporter reporter, | ||
171 | A4Options options, | ||
172 | Command command, | ||
173 | CompModule compModule, | ||
174 | AlloySolverConfiguration configuration) | ||
175 | { | ||
176 | this.warnings = warnings | ||
177 | this.debugs = debugs | ||
178 | this.reporter = reporter | ||
179 | this.options = options | ||
180 | this.command = command | ||
181 | this.compModule = compModule | ||
182 | this.configuration = configuration | ||
183 | } | ||
184 | |||
185 | override call() throws Exception { | ||
186 | val startTime = System.currentTimeMillis | ||
187 | |||
188 | // Start: Execute | ||
189 | var A4Solution lastAnswer = null | ||
190 | try { | ||
191 | if(!configuration.progressMonitor.isCancelled) { | ||
192 | do{ | ||
193 | if(lastAnswer == null) { | ||
194 | lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | ||
195 | } else { | ||
196 | lastAnswer = lastAnswer.next | ||
197 | } | ||
198 | configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) | ||
199 | |||
200 | val runtime = System.currentTimeMillis -startTime | ||
201 | synchronized(this) { | ||
202 | answers += (lastAnswer->runtime) | ||
203 | } | ||
204 | } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) | ||
205 | |||
206 | } | ||
207 | }catch(Exception e) { | ||
208 | warnings +=e.message | ||
209 | } | ||
210 | // Finish: execute | ||
211 | return answers | ||
212 | } | ||
213 | |||
214 | def hasEnoughSolution(List<?> answers) { | ||
215 | if(configuration.solutionScope.numberOfRequiredSolution < 0) return false | ||
216 | else return answers.size() == configuration.solutionScope.numberOfRequiredSolution | ||
217 | } | ||
218 | |||
219 | public def getPartialAnswers() { | ||
220 | return answers | ||
221 | } | ||
222 | } | ||
223 | |||
224 | @Data class SolverConfiguration { | ||
225 | AlloyBackendSolver backedSolver | ||
226 | String path | ||
227 | String[] options | ||
228 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend new file mode 100644 index 00000000..dcb4bb32 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend | |||
@@ -0,0 +1,249 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar | ||
4 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | ||
5 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | ||
6 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
16 | import java.util.Arrays | ||
17 | import java.util.HashMap | ||
18 | import java.util.LinkedList | ||
19 | import java.util.List | ||
20 | import java.util.Map | ||
21 | import java.util.Set | ||
22 | import java.util.SortedSet | ||
23 | import java.util.TreeSet | ||
24 | |||
25 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
26 | |||
27 | class AlloyModelInterpretation implements LogicModelInterpretation{ | ||
28 | |||
29 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
30 | protected val AlloyModelInterpretation_TypeInterpretation typeInterpretator | ||
31 | |||
32 | protected val Logic2AlloyLanguageMapper forwardMapper | ||
33 | protected val Logic2AlloyLanguageMapperTrace forwardTrace; | ||
34 | |||
35 | private var ExprVar logicLanguage; | ||
36 | |||
37 | private var String logicBooleanTrue; | ||
38 | private var String logicBooleanFalse; | ||
39 | private SortedSet<Integer> integerAtoms = new TreeSet | ||
40 | private SortedSet<String> stringAtoms = new TreeSet | ||
41 | |||
42 | private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap | ||
43 | private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap | ||
44 | |||
45 | private val Map<ConstantDeclaration, Object> constant2Value | ||
46 | private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value | ||
47 | private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value | ||
48 | |||
49 | //private val int minInt | ||
50 | //private val int maxInt | ||
51 | |||
52 | public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { | ||
53 | this.typeInterpretator = typeInterpretator | ||
54 | this.forwardMapper = forwardMapper | ||
55 | this.forwardTrace = trace | ||
56 | |||
57 | // Maps to trace language elements to the parsed problem. | ||
58 | val Map<String, Sig> name2AlloySig = new HashMap | ||
59 | val Map<String, Field> name2AlloyField = new HashMap | ||
60 | // exploring signatures | ||
61 | for(sig:solution.allReachableSigs) { | ||
62 | name2AlloySig.put(sig.label,sig) | ||
63 | for(field : sig.fields) { | ||
64 | name2AlloyField.put(field.label,field) | ||
65 | } | ||
66 | } | ||
67 | val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution) | ||
68 | this.typeInterpretator.resolveUnknownAtoms( | ||
69 | unknownAtoms, | ||
70 | solution, | ||
71 | forwardTrace, | ||
72 | name2AlloySig, | ||
73 | name2AlloyField, | ||
74 | alloyAtom2LogicElement, | ||
75 | interpretationOfUndefinedType) | ||
76 | |||
77 | // eval consants | ||
78 | constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[ | ||
79 | solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term | ||
80 | ] | ||
81 | // eval functions | ||
82 | val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function | | ||
83 | newHashMap( | ||
84 | solution.eval(function.name.lookup(name2AlloyField)) | ||
85 | .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])] | ||
86 | |||
87 | val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function | | ||
88 | val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField) | ||
89 | val paramIndexes = 1..(function.parameters.size) | ||
90 | return newHashMap( | ||
91 | solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t | | ||
92 | new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term]) | ||
93 | -> | ||
94 | t.atom(function.parameters.size + 1).atomLabel2Term | ||
95 | ])] | ||
96 | this.function2Value = Union(hostedfunction2Value,globalfunction2Value) | ||
97 | // eval relations | ||
98 | val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation | | ||
99 | solution.eval(relation.name.lookup(name2AlloyField)).map[ t | | ||
100 | new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet] | ||
101 | val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation | | ||
102 | solution.eval(relation.name.lookup(name2AlloyField)).map[ t | | ||
103 | new ParameterSubstitution((1..<t.arity).map[int a|t.atom(a).atomLabel2Term])].toSet] | ||
104 | this.relation2Value = Union(hostedRelation2Value,globalRelation2Value) | ||
105 | |||
106 | //Int limits | ||
107 | //this.minInt = solution.min | ||
108 | //this.maxInt = solution.max | ||
109 | |||
110 | //print(trace) | ||
111 | } | ||
112 | |||
113 | def List<ExprVar> collectUnknownAndResolveKnownAtoms(A4Solution solution) { | ||
114 | val Iterable<ExprVar> allAtoms = solution.allAtoms | ||
115 | val List<ExprVar> unknownAtoms = new LinkedList | ||
116 | |||
117 | for(atom: allAtoms) { | ||
118 | val typeName = getName(atom.type) | ||
119 | val atomName = atom.name | ||
120 | println(atom.toString + " < - " + typeName) | ||
121 | if(typeName == forwardTrace.logicLanguage.name) { | ||
122 | this.logicLanguage = atom | ||
123 | } else if(typeName == "Int" || typeName == "seq/Int") { | ||
124 | val value = Integer.parseInt(atomName.join) | ||
125 | this.integerAtoms.add(value) | ||
126 | } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { | ||
127 | if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } | ||
128 | else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} | ||
129 | else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') | ||
130 | } else if(typeName == "String") { | ||
131 | val value = parseString(atomName.join) | ||
132 | this.stringAtoms.add(value) | ||
133 | } else { | ||
134 | unknownAtoms += atom | ||
135 | } | ||
136 | } | ||
137 | val integerSignature = solution.allReachableSigs.filter[it.label=="Int"].head | ||
138 | for(i : solution.eval(integerSignature)) { | ||
139 | val value = Integer.parseInt(i.atom(0)) | ||
140 | this.integerAtoms.add(value) | ||
141 | } | ||
142 | val stringSignature = solution.allReachableSigs.filter[it.label=="String"].head | ||
143 | for(i : solution.eval(stringSignature)) { | ||
144 | val value = parseString(i.atom(0)) | ||
145 | this.stringAtoms.add(value) | ||
146 | } | ||
147 | return unknownAtoms | ||
148 | } | ||
149 | |||
150 | def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) { | ||
151 | val name = type.toString | ||
152 | if(name.startsWith("{this/") && name.endsWith("}")) { | ||
153 | return type.toString.replaceFirst("\\{this\\/","").replace("}","") | ||
154 | } | ||
155 | else throw new IllegalArgumentException('''Unknown type format: "«name»"!''') | ||
156 | } | ||
157 | def private getName(ExprVar atom) { atom.toString.split("\\$") } | ||
158 | |||
159 | def print(Logic2AlloyLanguageMapperTrace trace) { | ||
160 | println('''Undefined-----''') | ||
161 | interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v.map[name]»''')] | ||
162 | //println('''Defined-----''') | ||
163 | //trace.type2ALSType.keySet.filter(TypeDefinition).forEach[println('''«it.name» -> «it.elements.map[name.join]»''')] | ||
164 | |||
165 | println('''Constants-----''') | ||
166 | constant2Value.forEach[k, v|println('''«k.name» : «v»''')] | ||
167 | println('''Functions-----''') | ||
168 | function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]] | ||
169 | println('''Relations-----''') | ||
170 | relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]] | ||
171 | } | ||
172 | |||
173 | override getElements(Type type) { getElementsDispatch(type) } | ||
174 | def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) } | ||
175 | def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } | ||
176 | |||
177 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | ||
178 | val transformedParams = new ParameterSubstitution(parameterSubstitution) | ||
179 | return transformedParams.lookup( | ||
180 | function.lookup(this.function2Value) | ||
181 | ) | ||
182 | } | ||
183 | |||
184 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | ||
185 | relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution)) | ||
186 | } | ||
187 | |||
188 | override getInterpretation(ConstantDeclaration constant) { | ||
189 | constant.lookup(this.constant2Value) | ||
190 | } | ||
191 | |||
192 | // Alloy term -> logic term | ||
193 | def private atomLabel2Term(String label) { | ||
194 | if(label.number) return Integer.parseInt(label) | ||
195 | else if(label == this.logicBooleanTrue) return true | ||
196 | else if(label == this.logicBooleanFalse) return false | ||
197 | else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement) | ||
198 | else if(label.isString) return parseString(label) | ||
199 | else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''') | ||
200 | } | ||
201 | def private isNumber(String s) { | ||
202 | try{ | ||
203 | Integer.parseInt(s) | ||
204 | return true | ||
205 | }catch(NumberFormatException e) { | ||
206 | return false | ||
207 | } | ||
208 | } | ||
209 | def private isString(String label) { | ||
210 | label.startsWith("\"") && label.endsWith("\"") | ||
211 | } | ||
212 | def private parseString(String label) { | ||
213 | label.substring(1,label.length-1) | ||
214 | } | ||
215 | |||
216 | override getAllIntegersInStructure() { | ||
217 | this.integerAtoms | ||
218 | } | ||
219 | |||
220 | override getAllRealsInStructure() { | ||
221 | new TreeSet | ||
222 | } | ||
223 | |||
224 | override getAllStringsInStructure() { | ||
225 | this.stringAtoms | ||
226 | } | ||
227 | } | ||
228 | |||
229 | /** | ||
230 | * Helper class for efficiently matching parameter substitutions for functions and relations. | ||
231 | */ | ||
232 | class ParameterSubstitution{ | ||
233 | val Object[] data; | ||
234 | |||
235 | new(Object[] data) { this.data = data } | ||
236 | |||
237 | override equals(Object obj) { | ||
238 | if(obj === this) return true | ||
239 | else if(obj == null) return false | ||
240 | if(obj instanceof ParameterSubstitution) { | ||
241 | return Arrays.equals(this.data,obj.data) | ||
242 | } | ||
243 | return false | ||
244 | } | ||
245 | |||
246 | override hashCode() { | ||
247 | Arrays.hashCode(data) | ||
248 | } | ||
249 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend new file mode 100644 index 00000000..7082c946 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend | |||
@@ -0,0 +1,21 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar | ||
4 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
5 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | ||
6 | import java.util.Map | ||
7 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
10 | import java.util.List | ||
11 | |||
12 | interface AlloyModelInterpretation_TypeInterpretation { | ||
13 | def void resolveUnknownAtoms( | ||
14 | Iterable<ExprVar> objectAtoms, | ||
15 | A4Solution solution, | ||
16 | Logic2AlloyLanguageMapperTrace forwardTrace, | ||
17 | Map<String, Sig> name2AlloySig, | ||
18 | Map<String, Field> name2AlloyField, | ||
19 | Map<String,DefinedElement> expression2DefinedElement, | ||
20 | Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) | ||
21 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend new file mode 100644 index 00000000..d486649c --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend | |||
@@ -0,0 +1,72 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar | ||
4 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | ||
5 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | ||
6 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
10 | import java.util.ArrayList | ||
11 | import java.util.List | ||
12 | import java.util.Map | ||
13 | |||
14 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
15 | |||
16 | class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{ | ||
17 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
18 | |||
19 | override resolveUnknownAtoms( | ||
20 | Iterable<ExprVar> objectAtoms, | ||
21 | A4Solution solution, | ||
22 | Logic2AlloyLanguageMapperTrace forwardTrace, | ||
23 | Map<String, Sig> name2AlloySig, | ||
24 | Map<String, Field> name2AlloyField, | ||
25 | Map<String,DefinedElement> expression2DefinedElement, | ||
26 | Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) | ||
27 | { | ||
28 | /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap() | ||
29 | val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/ | ||
30 | |||
31 | val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
32 | |||
33 | // 1. Evaluate the defined elements | ||
34 | for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) { | ||
35 | val name = definedElementMappingEntry.value.name | ||
36 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
37 | val elementsOfSingletonSignature = solution.eval(matchingSig) | ||
38 | if(elementsOfSingletonSignature.size != 1) { | ||
39 | throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''') | ||
40 | } else { | ||
41 | val expressionOfDefinedElement = elementsOfSingletonSignature.head.atom(0)// as ExprVar | ||
42 | expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key) | ||
43 | } | ||
44 | } | ||
45 | |||
46 | // 2. evaluate the signatures and create new elements if necessary | ||
47 | for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) { | ||
48 | val type = type2SingatureEntry.key | ||
49 | if(type instanceof TypeDeclaration) { | ||
50 | val name = type2SingatureEntry.value.name | ||
51 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
52 | val elementsOfSignature = solution.eval(matchingSig) | ||
53 | val elementList = new ArrayList(elementsOfSignature.size) | ||
54 | var newVariableIndex = 1; | ||
55 | for(elementOfSignature : elementsOfSignature) { | ||
56 | val expressionOfDefinedElement = elementOfSignature.atom(0) | ||
57 | if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) { | ||
58 | elementList += expressionOfDefinedElement.lookup(expression2DefinedElement) | ||
59 | } else { | ||
60 | val newElementName = '''newObject «newVariableIndex.toString»''' | ||
61 | val newRepresentation = createDefinedElement => [ | ||
62 | it.name = newElementName | ||
63 | ] | ||
64 | elementList += newRepresentation | ||
65 | expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation) | ||
66 | } | ||
67 | } | ||
68 | interpretationOfUndefinedType.put(type,elementList) | ||
69 | } | ||
70 | } | ||
71 | } | ||
72 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend new file mode 100644 index 00000000..249820b6 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend | |||
@@ -0,0 +1,20 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar | ||
4 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
5 | import java.util.Map | ||
6 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | ||
7 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
10 | import java.util.List | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
12 | |||
13 | class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{ | ||
14 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
15 | |||
16 | override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, A4Solution solution, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String, Sig> name2AlloySig, Map<String, Field> name2AlloyField, Map<String, DefinedElement> expression2DefinedElement, Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) { | ||
17 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
18 | } | ||
19 | |||
20 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend new file mode 100644 index 00000000..65eaad47 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | |||
@@ -0,0 +1,491 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumericOperator | ||
9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration | ||
11 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | ||
13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | ||
14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference | ||
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure | ||
55 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
56 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation | ||
57 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation | ||
58 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
59 | import java.util.Collection | ||
60 | import java.util.Collections | ||
61 | import java.util.HashMap | ||
62 | import java.util.List | ||
63 | import java.util.Map | ||
64 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
65 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
66 | import org.eclipse.xtend.lib.annotations.Accessors | ||
67 | |||
68 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
69 | |||
70 | class Logic2AlloyLanguageMapper { | ||
71 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
72 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
73 | private val RunCommandMapper runCommandMapper | ||
74 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | ||
75 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this) | ||
76 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this) | ||
77 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_RelationMapper relationMapper = new Logic2AlloyLanguageMapper_RelationMapper(this) | ||
78 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_Containment containmentMapper = new Logic2AlloyLanguageMapper_Containment(this) | ||
79 | |||
80 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | ||
81 | this.typeMapper = typeMapper | ||
82 | this.runCommandMapper = new RunCommandMapper(typeMapper) | ||
83 | } | ||
84 | |||
85 | public def TracedOutput<ALSDocument,Logic2AlloyLanguageMapperTrace> transformProblem(LogicProblem problem, AlloySolverConfiguration config) { | ||
86 | val logicLanguage = createALSSignatureBody => [ | ||
87 | it.multiplicity = ALSMultiplicity.ONE | ||
88 | it.declarations += | ||
89 | createALSSignatureDeclaration => [ | ||
90 | it.name = support.toID(#["util", "language"]) ] | ||
91 | ] | ||
92 | |||
93 | val specification = createALSDocument=>[ | ||
94 | it.signatureBodies+=logicLanguage | ||
95 | ] | ||
96 | val trace = new Logic2AlloyLanguageMapperTrace => [ | ||
97 | it.specification = specification | ||
98 | it.logicLanguage = logicLanguage.declarations.head | ||
99 | it.logicLanguageBody = logicLanguage | ||
100 | |||
101 | it.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem)) | ||
102 | ] | ||
103 | specification.transformRandomisation(config.randomise) | ||
104 | |||
105 | typeMapper.transformTypes(problem.types,problem.elements,this,trace) | ||
106 | |||
107 | trace.constantDefinitions = problem.collectConstantDefinitions | ||
108 | trace.functionDefinitions = problem.collectFunctionDefinitions | ||
109 | trace.relationDefinitions = problem.collectRelationDefinitions | ||
110 | val calledInTransitiveClosure = problem.collectTransitiveRelationCalls | ||
111 | |||
112 | problem.constants.forEach[this.constantMapper.transformConstant(it, trace)] | ||
113 | problem.functions.forEach[this.functionMapper.transformFunction(it, trace)] | ||
114 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] | ||
115 | calledInTransitiveClosure.forEach[this.relationMapper.prepareTransitiveClosure(it, trace)] | ||
116 | |||
117 | problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstantDefinitionSpecification(it,trace)] | ||
118 | problem.functions.filter(FunctionDefinition).forEach[this.functionMapper.transformFunctionDefinitionSpecification(it,trace)] | ||
119 | problem.relations.filter(RelationDefinition).forEach[this.relationMapper.transformRelationDefinitionSpecification(it,trace)] | ||
120 | |||
121 | val containment = problem.getContainmentHierarchies.head | ||
122 | if(containment !== null) { | ||
123 | this.containmentMapper.transformContainmentHierarchy(containment,trace) | ||
124 | } | ||
125 | |||
126 | //////////////////// | ||
127 | // Collect EMF-specific assertions | ||
128 | //////////////////// | ||
129 | val assertion2InverseRelation = problem.annotations.collectAnnotations(InverseRelationAssertion) | ||
130 | val assertion2UpperMultiplicityAssertion = problem.annotations.collectAnnotations(UpperMultiplicityAssertion) | ||
131 | val assertion2LowerMultiplicityAssertion = problem.annotations.collectAnnotations(LowerMultiplicityAssertion) | ||
132 | |||
133 | //////////////////// | ||
134 | // Transform Assertions | ||
135 | //////////////////// | ||
136 | for(assertion : problem.assertions) { | ||
137 | if(assertion2InverseRelation.containsKey(assertion)) { | ||
138 | transformInverseAssertion(assertion.lookup(assertion2InverseRelation),trace) | ||
139 | } else if(assertion2UpperMultiplicityAssertion.containsKey(assertion)) { | ||
140 | transformUpperMultiplicityAssertion(assertion.lookup(assertion2UpperMultiplicityAssertion),trace) | ||
141 | } else if(assertion2LowerMultiplicityAssertion.containsKey(assertion)) { | ||
142 | transformLowerMultiplicityAssertion(assertion.lookup(assertion2LowerMultiplicityAssertion),trace) | ||
143 | } else { | ||
144 | transformAssertion(assertion,trace) | ||
145 | } | ||
146 | } | ||
147 | |||
148 | runCommandMapper.transformRunCommand(this, specification, trace, config) | ||
149 | |||
150 | return new TracedOutput(specification,trace) | ||
151 | } | ||
152 | |||
153 | def transformRandomisation(ALSDocument document, int randomisation) { | ||
154 | if(randomisation !== 0) { | ||
155 | document.signatureBodies += createALSSignatureBody => [ | ||
156 | val declaration = createALSSignatureDeclaration => [ | ||
157 | it.name = support.toID(#["language","util","randomseed"]) | ||
158 | ] | ||
159 | it.declarations += declaration | ||
160 | it.multiplicity = ALSMultiplicity::ONE | ||
161 | for(i : 1..randomisation) { | ||
162 | it.fields+=createALSFieldDeclaration => [ | ||
163 | it.name = support.toID(#["language","util","randomseedField",i.toString]) | ||
164 | it.multiplicity = ALSMultiplicity::ONE | ||
165 | it.type = createALSReference => [referred = declaration] | ||
166 | ] | ||
167 | } | ||
168 | ] | ||
169 | } | ||
170 | } | ||
171 | |||
172 | def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
173 | val a = assertion.inverseA | ||
174 | val b = assertion.inverseB | ||
175 | if(a instanceof RelationDeclaration && b instanceof RelationDeclaration && | ||
176 | !trace.relationDefinitions.containsKey(a) && !trace.relationDefinitions.containsKey(b)) | ||
177 | { | ||
178 | val fact = createALSFactDeclaration => [ | ||
179 | it.name = support.toID(assertion.target.name) | ||
180 | it.term = createALSEquals => [ | ||
181 | it.leftOperand = relationMapper.transformRelationReference(a as RelationDeclaration, trace) | ||
182 | it.rightOperand = createALSInverseRelation => [it.operand = relationMapper.transformRelationReference(b as RelationDeclaration, trace) ] | ||
183 | ] | ||
184 | ] | ||
185 | trace.specification.factDeclarations += fact | ||
186 | } else { | ||
187 | return transformAssertion(assertion.target,trace) | ||
188 | } | ||
189 | } | ||
190 | |||
191 | def transformUpperMultiplicityAssertion(UpperMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
192 | val x = assertion.relation | ||
193 | if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) { | ||
194 | val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) | ||
195 | val type = relation.type | ||
196 | |||
197 | if(type instanceof ALSDirectProduct) { | ||
198 | type.rightMultiplicit = type.rightMultiplicit.addUpper | ||
199 | } else { | ||
200 | relation.multiplicity = relation.multiplicity.addUpper | ||
201 | } | ||
202 | |||
203 | if(assertion.upper === 1) { | ||
204 | return true | ||
205 | } else { | ||
206 | return transformAssertion(assertion.target,trace) | ||
207 | } | ||
208 | |||
209 | } else { | ||
210 | return transformAssertion(assertion.target,trace) | ||
211 | } | ||
212 | } | ||
213 | |||
214 | def transformLowerMultiplicityAssertion(LowerMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
215 | val x = assertion.relation | ||
216 | if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) { | ||
217 | val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) | ||
218 | val type = relation.type | ||
219 | |||
220 | if(type instanceof ALSDirectProduct) { | ||
221 | type.rightMultiplicit = type.rightMultiplicit.addLower | ||
222 | } else { | ||
223 | relation.multiplicity = relation.multiplicity.addLower | ||
224 | } | ||
225 | |||
226 | if(assertion.lower === 1) { | ||
227 | return true | ||
228 | } else { | ||
229 | return transformAssertion(assertion.target,trace) | ||
230 | } | ||
231 | |||
232 | } else { | ||
233 | return transformAssertion(assertion.target,trace) | ||
234 | } | ||
235 | } | ||
236 | |||
237 | private def addLower(ALSMultiplicity multiplicity) { | ||
238 | if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { | ||
239 | return ALSMultiplicity::SOME | ||
240 | } else if(multiplicity === ALSMultiplicity::LONE) { | ||
241 | return ALSMultiplicity::ONE | ||
242 | } else if(multiplicity == ALSMultiplicity::ONE) { | ||
243 | return ALSMultiplicity::ONE | ||
244 | } else { | ||
245 | throw new IllegalArgumentException('''Lower multiplicity is already set!''') | ||
246 | } | ||
247 | } | ||
248 | private def addUpper(ALSMultiplicity multiplicity) { | ||
249 | if(multiplicity === ALSMultiplicity::ALL) { | ||
250 | return ALSMultiplicity::LONE | ||
251 | } else if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { | ||
252 | return ALSMultiplicity::LONE | ||
253 | } else if(multiplicity === ALSMultiplicity::SOME) { | ||
254 | return ALSMultiplicity::ONE | ||
255 | } else if(multiplicity == ALSMultiplicity::ONE) { | ||
256 | return ALSMultiplicity::ONE | ||
257 | } else { | ||
258 | throw new IllegalArgumentException('''Upper multiplicity is already set!''') | ||
259 | } | ||
260 | } | ||
261 | |||
262 | private def <T extends AssertionAnnotation> collectAnnotations(Collection<? extends Annotation> collection, Class<T> annotationKind) { | ||
263 | val res = new HashMap | ||
264 | collection.filter(annotationKind).forEach[res.put(it.target,it)] | ||
265 | return res | ||
266 | } | ||
267 | |||
268 | private def collectConstantDefinitions(LogicProblem problem) { | ||
269 | val res = new HashMap | ||
270 | problem.constants.filter(ConstantDefinition).filter[it.defines!==null].forEach[ | ||
271 | res.put(it.defines,it) | ||
272 | ] | ||
273 | return res | ||
274 | } | ||
275 | private def collectFunctionDefinitions(LogicProblem problem) { | ||
276 | val res = new HashMap | ||
277 | problem.functions.filter(FunctionDefinition).filter[it.defines!==null].forEach[ | ||
278 | res.put(it.defines,it) | ||
279 | ] | ||
280 | return res | ||
281 | } | ||
282 | private def collectRelationDefinitions(LogicProblem problem) { | ||
283 | val res = new HashMap | ||
284 | problem.relations.filter(RelationDefinition).filter[it.defines!==null].forEach[ | ||
285 | res.put(it.defines,it) | ||
286 | ] | ||
287 | return res | ||
288 | } | ||
289 | private def collectTransitiveRelationCalls(LogicProblem problem) { | ||
290 | return problem.eAllContents.filter(TransitiveClosure).map[it.relation].toSet | ||
291 | } | ||
292 | |||
293 | //////////////////// | ||
294 | // Type References | ||
295 | //////////////////// | ||
296 | def dispatch protected ALSTerm transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyLanguageMapperTrace trace) { | ||
297 | return createALSReference => [ it.referred = support.getBooleanType(trace) ] | ||
298 | } | ||
299 | def dispatch protected ALSTerm transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt } | ||
300 | def dispatch protected ALSTerm transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt } | ||
301 | def dispatch protected ALSTerm transformTypeReference(StringTypeReference stringTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSString } | ||
302 | def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { | ||
303 | val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) | ||
304 | return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) | ||
305 | } | ||
306 | |||
307 | ////////////// | ||
308 | // Assertions + Terms | ||
309 | ////////////// | ||
310 | |||
311 | def protected transformAssertion(Assertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
312 | val res = createALSFactDeclaration => [ | ||
313 | it.name = support.toID(assertion.name) | ||
314 | it.term = assertion.value.transformTerm(trace,Collections.EMPTY_MAP) | ||
315 | ] | ||
316 | trace.specification.factDeclarations += res | ||
317 | } | ||
318 | |||
319 | def dispatch protected ALSTerm transformTerm(BoolLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
320 | var ALSEnumLiteral ref; | ||
321 | if(literal.value==true) {ref = support.getBooleanTrue(trace)} | ||
322 | else {ref = support.getBooleanFalse(trace)} | ||
323 | val refFinal = ref | ||
324 | |||
325 | return support.booleanToLogicValue((createALSReference => [referred = refFinal]),trace) | ||
326 | } | ||
327 | def dispatch protected ALSTerm transformTerm(RealLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
328 | val v = literal.value.intValue | ||
329 | if(v>=0) { createALSNumberLiteral => [value = v]} | ||
330 | else {createALSUnaryMinus => [it.operand = createALSNumberLiteral => [value = v] ] } | ||
331 | } | ||
332 | def dispatch protected ALSTerm transformTerm(IntLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
333 | if(literal.value>=0) { createALSNumberLiteral => [value = literal.value]} | ||
334 | else {createALSUnaryMinus => [it.operand = createALSNumberLiteral => [value = literal.value] ] } | ||
335 | } | ||
336 | def dispatch protected ALSTerm transformTerm(StringLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
337 | createALSStringLiteral => [it.value = literal.value] | ||
338 | } | ||
339 | |||
340 | def dispatch protected ALSTerm transformTerm(Not not, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
341 | createALSNot=>[operand = not.operand.transformTerm(trace,variables)] } | ||
342 | def dispatch protected ALSTerm transformTerm(And and, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
343 | support.unfoldAnd(and.operands.map[transformTerm(trace,variables)]) } | ||
344 | def dispatch protected ALSTerm transformTerm(Or or, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
345 | support.unfoldOr(or.operands.map[transformTerm(trace,variables)],trace) } | ||
346 | def dispatch protected ALSTerm transformTerm(Impl impl, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
347 | createALSImpl => [leftOperand = impl.leftOperand.transformTerm(trace,variables) rightOperand = impl.rightOperand.transformTerm(trace,variables)] } | ||
348 | def dispatch protected ALSTerm transformTerm(Iff iff, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
349 | createALSIff => [leftOperand = iff.leftOperand.transformTerm(trace,variables) rightOperand = iff.rightOperand.transformTerm(trace,variables)] } | ||
350 | def dispatch protected ALSTerm transformTerm(MoreThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
351 | createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } | ||
352 | def dispatch protected ALSTerm transformTerm(LessThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
353 | createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } | ||
354 | def dispatch protected ALSTerm transformTerm(MoreOrEqualThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
355 | createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } | ||
356 | def dispatch protected ALSTerm transformTerm(LessOrEqualThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
357 | createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } | ||
358 | def dispatch protected ALSTerm transformTerm(Equals equals, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
359 | createALSEquals => [leftOperand = equals.leftOperand.transformTerm(trace,variables) rightOperand = equals.rightOperand.transformTerm(trace,variables)] } | ||
360 | def dispatch protected ALSTerm transformTerm(Distinct distinct, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
361 | support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } | ||
362 | |||
363 | def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
364 | createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] } | ||
365 | def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
366 | createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] } | ||
367 | def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
368 | createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] } | ||
369 | def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
370 | createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] } | ||
371 | def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
372 | createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] } | ||
373 | |||
374 | def dispatch protected ALSTerm transformTerm(Forall forall, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
375 | support.createQuantifiedExpression(this,forall,ALSMultiplicity.ALL,trace,variables) } | ||
376 | def dispatch protected ALSTerm transformTerm(Exists exists, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
377 | support.createQuantifiedExpression(this,exists,ALSMultiplicity.SOME,trace,variables) } | ||
378 | |||
379 | def dispatch protected ALSTerm transformTerm(InstanceOf instanceOf, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
380 | return createALSSubset => [ | ||
381 | it.leftOperand = instanceOf.value.transformTerm(trace,variables) | ||
382 | it.rightOperand = instanceOf.range.transformTypeReference(trace) | ||
383 | ] | ||
384 | } | ||
385 | |||
386 | def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
387 | return this.relationMapper.transformTransitiveRelationReference( | ||
388 | tc.relation, | ||
389 | tc.leftOperand.transformTerm(trace,variables), | ||
390 | tc.rightOperand.transformTerm(trace,variables), | ||
391 | trace | ||
392 | ) | ||
393 | } | ||
394 | |||
395 | def dispatch protected ALSTerm transformTerm(SymbolicValue symbolicValue, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
396 | symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } | ||
397 | |||
398 | def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
399 | typeMapper.transformReference(referred,trace) | ||
400 | } | ||
401 | def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
402 | if(trace.constantDefinitions.containsKey(constant)) { | ||
403 | return this.transformSymbolicReference(constant.lookup(trace.constantDefinitions),parameterSubstitutions,trace,variables) | ||
404 | } else { | ||
405 | val res = createALSJoin=> [ | ||
406 | leftOperand = createALSReference => [ referred = trace.logicLanguage ] | ||
407 | rightOperand = createALSReference => [ referred = constant.lookup(trace.constantDeclaration2LanguageField) ] | ||
408 | ] | ||
409 | return support.postprocessResultOfSymbolicReference(constant.type,res,trace) | ||
410 | } | ||
411 | } | ||
412 | def dispatch protected ALSTerm transformSymbolicReference(ConstantDefinition constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
413 | val res = createALSFunctionCall => [ | ||
414 | it.referredDefinition = constant.lookup(trace.constantDefinition2Function) | ||
415 | ] | ||
416 | return support.postprocessResultOfSymbolicReference(constant.type,res,trace) | ||
417 | } | ||
418 | def dispatch protected ALSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
419 | val res = createALSReference => [referred = variable.lookup(variables)] | ||
420 | return support.postprocessResultOfSymbolicReference(variable.range,res,trace) | ||
421 | } | ||
422 | def dispatch protected ALSTerm transformSymbolicReference(FunctionDeclaration function, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
423 | if(trace.functionDefinitions.containsKey(function)) { | ||
424 | return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) | ||
425 | } else { | ||
426 | if(functionMapper.transformedToHostedField(function,trace)) { | ||
427 | val param = parameterSubstitutions.get(0).transformTerm(trace,variables) | ||
428 | val res = createALSJoin => [ | ||
429 | leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace) | ||
430 | rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)] | ||
431 | ] | ||
432 | return support.postprocessResultOfSymbolicReference(function.range,res,trace) | ||
433 | } else { | ||
434 | val functionExpression = createALSJoin=>[ | ||
435 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
436 | rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)] | ||
437 | ] | ||
438 | val res = support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables) | ||
439 | return support.postprocessResultOfSymbolicReference(function.range,res,trace) | ||
440 | } | ||
441 | } | ||
442 | } | ||
443 | def dispatch protected ALSTerm transformSymbolicReference(FunctionDefinition function, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
444 | val result = createALSFunctionCall => [ | ||
445 | it.referredDefinition = function.lookup(trace.functionDefinition2Function) | ||
446 | it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] | ||
447 | ] | ||
448 | return support.postprocessResultOfSymbolicReference(function.range,result,trace) | ||
449 | } | ||
450 | |||
451 | def dispatch protected ALSTerm transformSymbolicReference(RelationDeclaration relation, List<Term> parameterSubstitutions, | ||
452 | Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
453 | if(trace.relationDefinitions.containsKey(relation)) { | ||
454 | this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),parameterSubstitutions,trace,variables) | ||
455 | } else { | ||
456 | if(relationMapper.transformToHostedField(relation,trace)) { | ||
457 | val alsRelation = relation.lookup(trace.relationDeclaration2Field) | ||
458 | // R(a,b) => | ||
459 | // b in a.R | ||
460 | return createALSSubset => [ | ||
461 | it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace,variables) | ||
462 | it.rightOperand = createALSJoin => [ | ||
463 | it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace,variables) | ||
464 | it.rightOperand = createALSReference => [ it.referred = alsRelation ] | ||
465 | ] | ||
466 | ] | ||
467 | } else { | ||
468 | val target = createALSJoin => [ | ||
469 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
470 | rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]] | ||
471 | val source = support.unfoldTermDirectProduct(this,parameterSubstitutions,trace,variables) | ||
472 | |||
473 | return createALSSubset => [ | ||
474 | leftOperand = source | ||
475 | rightOperand = target | ||
476 | ] | ||
477 | } | ||
478 | } | ||
479 | } | ||
480 | |||
481 | |||
482 | |||
483 | def dispatch protected ALSTerm transformSymbolicReference(RelationDefinition relation, List<Term> parameterSubstitutions, | ||
484 | Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) | ||
485 | { | ||
486 | return createALSFunctionCall => [ | ||
487 | it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) | ||
488 | it.params += parameterSubstitutions.map[p | p.transformTerm(trace,variables)] | ||
489 | ] | ||
490 | } | ||
491 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend new file mode 100644 index 00000000..6aadb285 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend | |||
@@ -0,0 +1,56 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumDeclaration | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSFieldDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSFunctionDefinition | ||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRelationDefinition | ||
9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody | ||
10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
17 | import java.util.HashMap | ||
18 | import java.util.Map | ||
19 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
21 | |||
22 | interface Logic2AlloyLanguageMapper_TypeMapperTrace {} | ||
23 | |||
24 | class Logic2AlloyLanguageMapperTrace { | ||
25 | public var ViatraQueryEngine incqueryEngine; | ||
26 | |||
27 | public var ALSDocument specification; | ||
28 | public var ALSSignatureDeclaration logicLanguage; | ||
29 | public var ALSSignatureBody logicLanguageBody; | ||
30 | public var ALSEnumDeclaration boolType; | ||
31 | public var ALSEnumLiteral boolTrue; | ||
32 | public var ALSEnumLiteral boolFalse; | ||
33 | |||
34 | public var Logic2AlloyLanguageMapper_TypeMapperTrace typeMapperTrace | ||
35 | |||
36 | public val Map<ConstantDeclaration, ALSFieldDeclaration> constantDeclaration2LanguageField = new HashMap | ||
37 | public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap | ||
38 | |||
39 | public val Map<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2HostedField = new HashMap | ||
40 | public val Map<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2LanguageField = new HashMap | ||
41 | public val Map<FunctionDefinition,ALSFunctionDefinition> functionDefinition2Function = new HashMap | ||
42 | |||
43 | public val Map<RelationDeclaration, ALSFieldDeclaration> relationDeclaration2Global = new HashMap | ||
44 | public val Map<RelationDeclaration, ALSFieldDeclaration> relationDeclaration2Field = new HashMap | ||
45 | public val Map<RelationDefinition,ALSRelationDefinition> relationDefinition2Predicate = new HashMap | ||
46 | |||
47 | public val Map<RelationDeclaration, ALSFieldDeclaration> transitiveClosureTarget2Global = new HashMap | ||
48 | public val Map<RelationDeclaration, ALSFieldDeclaration> transitiveClosureTarget2Field = new HashMap | ||
49 | |||
50 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | ||
51 | public var Map<FunctionDeclaration, FunctionDefinition> functionDefinitions | ||
52 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | ||
53 | |||
54 | public var Map<Relation, ALSFieldDeclaration> relationInTransitiveToGlobalField = new HashMap | ||
55 | public var Map<Relation, ALSFieldDeclaration> relationInTransitiveToHosterField = new HashMap | ||
56 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend new file mode 100644 index 00000000..22650a92 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend | |||
@@ -0,0 +1,43 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
7 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
8 | |||
9 | class Logic2AlloyLanguageMapper_ConstantMapper { | ||
10 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
11 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
12 | val Logic2AlloyLanguageMapper base; | ||
13 | public new(Logic2AlloyLanguageMapper base) { | ||
14 | this.base = base | ||
15 | } | ||
16 | |||
17 | def protected dispatch transformConstant(ConstantDeclaration constant, Logic2AlloyLanguageMapperTrace trace) { | ||
18 | if(!trace.constantDefinitions.containsKey(constant)) { | ||
19 | val c = createALSFieldDeclaration=> [ | ||
20 | name = support.toID(constant.name) | ||
21 | it.type = base.transformTypeReference(constant.type,trace) | ||
22 | it.multiplicity = ALSMultiplicity.ONE | ||
23 | ] | ||
24 | trace.logicLanguageBody.fields+= c | ||
25 | trace.constantDeclaration2LanguageField.put(constant,c) | ||
26 | } | ||
27 | } | ||
28 | |||
29 | def protected dispatch transformConstant(ConstantDefinition constant, Logic2AlloyLanguageMapperTrace trace) { | ||
30 | val c = createALSFunctionDefinition=> [ | ||
31 | name = support.toID(constant.name) | ||
32 | it.type = base.transformTypeReference(constant.type,trace) | ||
33 | // the value is set later | ||
34 | ] | ||
35 | trace.specification.functionDefinitions += c | ||
36 | trace.constantDefinition2Function.put(constant,c) | ||
37 | } | ||
38 | |||
39 | def protected transformConstantDefinitionSpecification(ConstantDefinition constant, Logic2AlloyLanguageMapperTrace trace) { | ||
40 | val definition = constant.lookup(trace.constantDefinition2Function) | ||
41 | definition.value = base.transformTerm(constant.value, trace,emptyMap) | ||
42 | } | ||
43 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend new file mode 100644 index 00000000..399a4eaf --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend | |||
@@ -0,0 +1,260 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
8 | import java.util.HashMap | ||
9 | |||
10 | class Logic2AlloyLanguageMapper_Containment { | ||
11 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
12 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
13 | val Logic2AlloyLanguageMapper base; | ||
14 | public new(Logic2AlloyLanguageMapper base) { | ||
15 | this.base = base | ||
16 | } | ||
17 | |||
18 | def protected transformContainmentHierarchy(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { | ||
19 | // Single root | ||
20 | val rootField = createALSFieldDeclaration => [ | ||
21 | it.name= support.toID(#["util", "root"]) | ||
22 | it.multiplicity = ALSMultiplicity.ONE | ||
23 | it.type = typesOrderedInContainment(containment,trace) | ||
24 | ] | ||
25 | trace.logicLanguageBody.fields += rootField | ||
26 | |||
27 | val contains = createALSFieldDeclaration => [ | ||
28 | it.name = support.toID(#["util", "contains"]) | ||
29 | //it.multiplicity = ALSMultiplicity::SET | ||
30 | it.type = createALSDirectProduct => [ | ||
31 | it.leftMultiplicit = ALSMultiplicity::LONE | ||
32 | it.rightMultiplicit = ALSMultiplicity::SET | ||
33 | it.leftOperand = typesOrderedInContainment(containment,trace) | ||
34 | it.rightOperand = typesOrderedInContainment(containment,trace) | ||
35 | ] | ||
36 | ] | ||
37 | trace.logicLanguageBody.fields += contains | ||
38 | |||
39 | val containmentRelationDefinition = createALSFactDeclaration => [ | ||
40 | it.name = support.toID(#["util", "containmentDefinition"]) | ||
41 | ] | ||
42 | |||
43 | if(containment.containmentRelations.forall[it instanceof RelationDeclaration]) { | ||
44 | val containmentRelations = containment.containmentRelations.filter(RelationDeclaration).map[relation| | ||
45 | base.relationMapper.transformRelationReference(relation,trace) | ||
46 | ].toList | ||
47 | |||
48 | containmentRelationDefinition.term = createALSEquals => [ | ||
49 | leftOperand = createALSJoin => [ | ||
50 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
51 | rightOperand = createALSReference => [ referred = contains ]] | ||
52 | rightOperand = support.unfoldPlus(containmentRelations) | ||
53 | ] | ||
54 | } else { | ||
55 | val parent = createALSVariableDeclaration => [ | ||
56 | it.name = "parent" | ||
57 | it.range = typesOrderedInContainment(containment, trace) | ||
58 | ] | ||
59 | val child = createALSVariableDeclaration => [ | ||
60 | it.name = "child" | ||
61 | it.range = typesOrderedInContainment(containment, trace) | ||
62 | ] | ||
63 | |||
64 | val logicFactory = LogiclanguageFactory.eINSTANCE | ||
65 | val logicParentVariable = logicFactory.createVariable | ||
66 | val logicChildVariable = logicFactory.createVariable | ||
67 | val logicParent = logicFactory.createSymbolicValue => [it.symbolicReference = logicParentVariable] | ||
68 | val logicChild = logicFactory.createSymbolicValue => [it.symbolicReference = logicChildVariable] | ||
69 | val variableMap = new HashMap => [put(logicParentVariable,parent) put(logicChildVariable,child)] | ||
70 | val possibleRelations = containment.containmentRelations.map[relation | | ||
71 | base.transformSymbolicReference(relation,#[logicParent,logicChild],trace,variableMap) | ||
72 | ] | ||
73 | |||
74 | containmentRelationDefinition.term = createALSQuantifiedEx => [ | ||
75 | it.type = ALSMultiplicity.ALL | ||
76 | it.variables += parent | ||
77 | it.variables += child | ||
78 | it.expression = createALSIff => [ | ||
79 | it.leftOperand = createALSSubset => [ | ||
80 | it.leftOperand = createALSDirectProduct => [ | ||
81 | it.leftOperand = createALSReference => [it.referred = child] | ||
82 | it.rightOperand = createALSReference => [it.referred = parent] | ||
83 | ] | ||
84 | it.rightOperand = createALSJoin => [ | ||
85 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
86 | rightOperand = createALSReference => [ referred = contains ] | ||
87 | ] | ||
88 | ] | ||
89 | it.rightOperand = support.unfoldOr(possibleRelations,trace) | ||
90 | ] | ||
91 | ] | ||
92 | } | ||
93 | |||
94 | trace.specification.factDeclarations += containmentRelationDefinition | ||
95 | |||
96 | // With the exception of the root, every object has at least one parent | ||
97 | // No parent for root | ||
98 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
99 | it.name = support.toID(#["util", "noParentForRoot"]) | ||
100 | it.term = createALSQuantifiedEx => [ | ||
101 | it.type = ALSMultiplicity::NO | ||
102 | val parent = createALSVariableDeclaration => [ | ||
103 | it.name = "parent" | ||
104 | it.range = typesOrderedInContainment(containment,trace) | ||
105 | ] | ||
106 | it.variables += parent | ||
107 | it.expression = createALSSubset => [ | ||
108 | it.leftOperand = createALSDirectProduct => [ | ||
109 | it.leftOperand = createALSReference => [it.referred = parent] | ||
110 | it.rightOperand = createALSJoin => [ | ||
111 | it.leftOperand = createALSReference => [it.referred = trace.logicLanguage] | ||
112 | it.rightOperand = createALSReference => [it.referred = rootField] | ||
113 | ] | ||
114 | ] | ||
115 | it.rightOperand = createALSJoin => [ | ||
116 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
117 | rightOperand = createALSReference => [ referred = contains ] | ||
118 | ] | ||
119 | ] | ||
120 | ] | ||
121 | ] | ||
122 | // Parent for nonroot | ||
123 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
124 | it.name = support.toID(#["util", "atLeastOneParent"]) | ||
125 | it.term = createALSQuantifiedEx => [ | ||
126 | it.type = ALSMultiplicity::ALL | ||
127 | val child = createALSVariableDeclaration => [ | ||
128 | it.name = "child" | ||
129 | it.range = typesOrderedInContainment(containment,trace) | ||
130 | ] | ||
131 | it.variables += child | ||
132 | it.expression = createALSOr => [ | ||
133 | it.leftOperand = createALSEquals => [ | ||
134 | it.leftOperand = createALSReference => [it.referred = child] | ||
135 | it.rightOperand = createALSJoin => [ | ||
136 | it.leftOperand = createALSReference => [it.referred = trace.logicLanguage] | ||
137 | it.rightOperand = createALSReference => [it.referred = rootField] | ||
138 | ] | ||
139 | ] | ||
140 | it.rightOperand = createALSQuantifiedEx => [ | ||
141 | it.type = ALSMultiplicity::SOME | ||
142 | val parent = createALSVariableDeclaration => [ | ||
143 | it.name = "parent" | ||
144 | it.range = typesOrderedInContainment(containment, trace) | ||
145 | ] | ||
146 | it.variables += parent | ||
147 | it.expression = createALSSubset => [ | ||
148 | it.leftOperand = createALSDirectProduct => [ | ||
149 | it.leftOperand = createALSReference => [it.referred = parent] | ||
150 | it.rightOperand = createALSReference => [it.referred = child] | ||
151 | ] | ||
152 | it.rightOperand = createALSJoin => [ | ||
153 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
154 | rightOperand = createALSReference => [ referred = contains ] | ||
155 | ] | ||
156 | ] | ||
157 | ] | ||
158 | ] | ||
159 | ] | ||
160 | ] | ||
161 | |||
162 | // Every object has at most one parent | ||
163 | // trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
164 | // it.name = support.toID(#["util", "atMostOneParent"]) | ||
165 | // it.term = createALSQuantifiedEx => [ | ||
166 | // it.type = ALSMultiplicity::ALL | ||
167 | // val child = createALSVariableDeclaration => [ | ||
168 | // it.name = "child" | ||
169 | // it.range = typesOrderedInContainment(containment,trace) | ||
170 | // ] | ||
171 | // it.variables += child | ||
172 | // it.expression = createALSQuantifiedEx => [ | ||
173 | // it.type = ALSMultiplicity::LONE | ||
174 | // val parent = createALSVariableDeclaration => [ | ||
175 | // it.name = "parent" | ||
176 | // it.range = typesOrderedInContainment(containment, trace) | ||
177 | // ] | ||
178 | // it.variables += parent | ||
179 | // it.expression = createALSFunctionCall => [ | ||
180 | // it.referredDefinition = containmentRelation | ||
181 | // it.params += createALSReference => [ | ||
182 | // it.referred = parent | ||
183 | // it.referred = child | ||
184 | // ] | ||
185 | // ] | ||
186 | // ] | ||
187 | // ] | ||
188 | // ] | ||
189 | |||
190 | // No circle in containment | ||
191 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
192 | it.name = support.toID(#["util", "noCircularContainment"]) | ||
193 | it.term = createALSQuantifiedEx => [ | ||
194 | it.type = ALSMultiplicity::NO | ||
195 | val variable = createALSVariableDeclaration => [ | ||
196 | it.name = "circle" | ||
197 | it.range = typesOrderedInContainment(containment,trace) | ||
198 | ] | ||
199 | it.variables += variable | ||
200 | it.expression = createALSSubset => [ | ||
201 | it.leftOperand = createALSDirectProduct => [ | ||
202 | it.leftOperand = createALSReference => [it.referred = variable] | ||
203 | it.rightOperand = createALSReference => [it.referred = variable] | ||
204 | ] | ||
205 | it.rightOperand = createAlSTransitiveClosure => [ | ||
206 | it.operand = createALSJoin => [ | ||
207 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
208 | rightOperand = createALSReference => [ referred = contains ] | ||
209 | ] | ||
210 | ] | ||
211 | ] | ||
212 | ] | ||
213 | ] | ||
214 | |||
215 | } | ||
216 | |||
217 | /*def protected calculateContainmentTypeCoveringSignatures(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { | ||
218 | val types = containment.typesOrderedInHierarchy | ||
219 | val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten.toList | ||
220 | // val uncoveredSignatures = new ArrayList(signaturesInContainment) | ||
221 | // val coveringSignatures = new LinkedList | ||
222 | // | ||
223 | val engine = ViatraQueryEngine.on(new EMFScope(trace.specification)) | ||
224 | //val directSubsetMatcher = DirectSubsetMatcher.on(engine) | ||
225 | // x <= y | ||
226 | val subsetMatcher = SubsetMatcher.on(engine) | ||
227 | |||
228 | if() | ||
229 | }*/ | ||
230 | |||
231 | /*def boolean coveringAllSignaturesInContainment(ALSSignatureDeclaration target, List<ALSSignatureDeclaration> signaturesInContainment, SubsetMatcher matcher) { | ||
232 | for(signatureInContainment : signaturesInContainment) { | ||
233 | if(!matcher.hasMatch(signatureInContainment,target)) { | ||
234 | return false | ||
235 | } | ||
236 | } | ||
237 | return true | ||
238 | }*/ | ||
239 | |||
240 | /*def boolean coveringSignatureNotInContainment(ALSSignatureDeclaration target, List<ALSSignatureDeclaration> signaturesInContainment, SubsetMatcher matcher) { | ||
241 | val subtypes = matcher.getAllValuesOfx(target); | ||
242 | for(subType : subtypes) { | ||
243 | val isSubtypeOfASignatureInContainment = signaturesInContainment.exists[contained | | ||
244 | matcher.hasMatch(subType,contained) | ||
245 | ] | ||
246 | if(!isSubtypeOfASignatureInContainment) { | ||
247 | return false | ||
248 | } | ||
249 | } | ||
250 | return true | ||
251 | }*/ | ||
252 | |||
253 | def protected typesOrderedInContainment(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { | ||
254 | val types = containment.typesOrderedInHierarchy | ||
255 | val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten | ||
256 | // val allSignatures = trace.specification.signatureBodies.map[declarations].flatten | ||
257 | val typeReferences = signaturesInContainment.map[sig | createALSReference => [it.referred = sig]].toList | ||
258 | return support.unfoldPlus(typeReferences) | ||
259 | } | ||
260 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend new file mode 100644 index 00000000..0915c306 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend | |||
@@ -0,0 +1,87 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
9 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
10 | import java.util.HashMap | ||
11 | |||
12 | class Logic2AlloyLanguageMapper_FunctionMapper { | ||
13 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
14 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
15 | val Logic2AlloyLanguageMapper base; | ||
16 | public new(Logic2AlloyLanguageMapper base) { | ||
17 | this.base = base | ||
18 | } | ||
19 | |||
20 | def protected dispatch transformFunction(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) { | ||
21 | if(!trace.constantDefinitions.containsKey(f)) { | ||
22 | if(transformedToHostedField(f,trace)) transformFunctionToFieldOfSignature(f,trace) | ||
23 | else transformFunctionToGlobalRelation(f,trace) | ||
24 | } | ||
25 | } | ||
26 | |||
27 | def protected transformedToHostedField(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) { | ||
28 | if(f.parameters.size == 1 && f.parameters.head instanceof ComplexTypeReference) { | ||
29 | val head = f.parameters.head | ||
30 | if(head instanceof ComplexTypeReference) { | ||
31 | val types = base.typeMapper.transformTypeReference(head.referred,base,trace) | ||
32 | return types.size == 1 | ||
33 | } | ||
34 | } | ||
35 | return (f.parameters.size == 1 && f.parameters.head instanceof ComplexTypeReference) | ||
36 | } | ||
37 | def protected transformFunctionToFieldOfSignature(FunctionDeclaration f,Logic2AlloyLanguageMapperTrace trace) { | ||
38 | val param = (f.parameters.head as ComplexTypeReference) | ||
39 | val referred = param.referred | ||
40 | val field = createALSFieldDeclaration => [ | ||
41 | it.name = support.toID(f.getName) | ||
42 | it.multiplicity = ALSMultiplicity.ONE | ||
43 | it.type = base.transformTypeReference(f.range,trace) | ||
44 | ] | ||
45 | val host = base.typeMapper.transformTypeReference(referred,base,trace).get(0) | ||
46 | (host.eContainer as ALSSignatureBody).fields += field | ||
47 | trace.functionDeclaration2HostedField.put(f, field) | ||
48 | } | ||
49 | def protected transformFunctionToGlobalRelation(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) { | ||
50 | val field = createALSFieldDeclaration => [ | ||
51 | it.name = support.toID(f.name) | ||
52 | it.multiplicity = ALSMultiplicity.SET | ||
53 | it.type = createALSDirectProduct => [ | ||
54 | it.leftOperand = support.unfoldReferenceDirectProduct(base,f.parameters,trace) | ||
55 | it.rightMultiplicit = ALSMultiplicity.ONE | ||
56 | it.rightOperand = base.transformTypeReference(f.range,trace) | ||
57 | ] | ||
58 | ] | ||
59 | trace.logicLanguageBody.fields += field | ||
60 | trace.functionDeclaration2LanguageField.put(f, field) | ||
61 | } | ||
62 | |||
63 | def protected dispatch transformFunction(FunctionDefinition f, Logic2AlloyLanguageMapperTrace trace) { | ||
64 | val res = createALSFunctionDefinition => [ | ||
65 | name = support.toID(f.name) | ||
66 | // variables + specification later | ||
67 | ] | ||
68 | trace.specification.functionDefinitions+=res; | ||
69 | trace.functionDefinition2Function.put(f,res) | ||
70 | } | ||
71 | |||
72 | def protected transformFunctionDefinitionSpecification(FunctionDefinition f, Logic2AlloyLanguageMapperTrace trace) { | ||
73 | val target = f.lookup(trace.functionDefinition2Function) | ||
74 | val variableMap = new HashMap | ||
75 | for(variable : f.variable) { | ||
76 | val v = createALSVariableDeclaration => [ | ||
77 | it.name = support.toID(variable.name) | ||
78 | it.range = base.transformTypeReference(variable.range,trace) | ||
79 | // specification later | ||
80 | ] | ||
81 | target.variables+=v | ||
82 | variableMap.put(variable,v) | ||
83 | } | ||
84 | target.value = base.transformTerm(f.value,trace,variableMap) | ||
85 | } | ||
86 | |||
87 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend new file mode 100644 index 00000000..d300a28b --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend | |||
@@ -0,0 +1,199 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
9 | import java.util.HashMap | ||
10 | |||
11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
13 | import java.util.List | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
15 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
16 | |||
17 | class Logic2AlloyLanguageMapper_RelationMapper { | ||
18 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
19 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
20 | val Logic2AlloyLanguageMapper base; | ||
21 | public new(Logic2AlloyLanguageMapper base) { | ||
22 | this.base = base | ||
23 | } | ||
24 | |||
25 | def dispatch public void transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
26 | if(!trace.relationDefinitions.containsKey(r)) { | ||
27 | if(r.transformToHostedField(trace)) { | ||
28 | transformRelationDeclarationToHostedField(r,trace) | ||
29 | } else { | ||
30 | transformRelationDeclarationToGlobalField(r,trace) | ||
31 | } | ||
32 | } | ||
33 | } | ||
34 | |||
35 | def public createRelationDeclaration(String name, List<TypeReference> paramTypes, Logic2AlloyLanguageMapperTrace trace) { | ||
36 | val field = createALSFieldDeclaration => [ | ||
37 | it.name = support.toID(name) | ||
38 | it.type = support.unfoldReferenceDirectProduct(base,paramTypes,trace) | ||
39 | ] | ||
40 | trace.logicLanguageBody.fields += field | ||
41 | return field | ||
42 | } | ||
43 | |||
44 | def protected transformToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
45 | val first = r.parameters.get(0) | ||
46 | if(r.parameters.size == 2) { | ||
47 | if(first instanceof ComplexTypeReference) { | ||
48 | val types = base.typeMapper.transformTypeReference(first.referred,base,trace) | ||
49 | if(types.size == 1) { | ||
50 | return true | ||
51 | } | ||
52 | } | ||
53 | } | ||
54 | return false | ||
55 | } | ||
56 | |||
57 | def protected transformRelationDeclarationToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
58 | val hostType = (r.parameters.head as ComplexTypeReference).referred | ||
59 | |||
60 | val targetBody = base.typeMapper.transformTypeReference(hostType,base,trace).get(0).eContainer as ALSSignatureBody | ||
61 | val field = createALSFieldDeclaration => [ | ||
62 | it.name = support.toID(r.getName) | ||
63 | it.multiplicity = ALSMultiplicity.SET | ||
64 | it.type = base.transformTypeReference(r.parameters.get(1),trace) | ||
65 | ] | ||
66 | targetBody.fields += field | ||
67 | trace.relationDeclaration2Field.put(r,field) | ||
68 | |||
69 | } | ||
70 | |||
71 | def protected transformRelationDeclarationToGlobalField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
72 | val field = createALSFieldDeclaration => [ | ||
73 | it.name = support.toID(r.name) | ||
74 | it.type = support.unfoldReferenceDirectProduct(base,r.parameters,trace) | ||
75 | ] | ||
76 | trace.logicLanguageBody.fields += field | ||
77 | trace.relationDeclaration2Global.put(r, field) | ||
78 | } | ||
79 | |||
80 | def dispatch public void transformRelation(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { | ||
81 | val res = createALSRelationDefinition => [ | ||
82 | name = support.toID(r.name) | ||
83 | // fill the variables later | ||
84 | // fill the expression later | ||
85 | ] | ||
86 | |||
87 | trace.relationDefinition2Predicate.put(r,res) | ||
88 | trace.specification.relationDefinitions+=res; | ||
89 | } | ||
90 | |||
91 | def protected void transformRelationDefinitionSpecification(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { | ||
92 | val predicate = r.lookup(trace.relationDefinition2Predicate) | ||
93 | if(predicate !== null) { | ||
94 | val variableMap = new HashMap | ||
95 | for(variable : r.variables) { | ||
96 | val v = createALSVariableDeclaration => [ | ||
97 | it.name = support.toID(variable.name) | ||
98 | it.range = base.transformTypeReference(variable.range,trace) | ||
99 | ] | ||
100 | predicate.variables+=v | ||
101 | variableMap.put(variable,v) | ||
102 | } | ||
103 | predicate.value = base.transformTerm(r.value,trace,variableMap) | ||
104 | } | ||
105 | } | ||
106 | |||
107 | def public transformRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { | ||
108 | if(relation.transformToHostedField(trace)) { | ||
109 | return createALSReference => [it.referred = relation.lookup(trace.relationDeclaration2Field) ] | ||
110 | } else { | ||
111 | return createALSJoin => [ | ||
112 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
113 | rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]] | ||
114 | } | ||
115 | } | ||
116 | |||
117 | def public getRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { | ||
118 | if(relation.transformToHostedField(trace)) { | ||
119 | return relation.lookup(trace.relationDeclaration2Field) | ||
120 | } else { | ||
121 | return relation.lookup(trace.relationDeclaration2Global) | ||
122 | } | ||
123 | } | ||
124 | |||
125 | public def dispatch void prepareTransitiveClosure(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { | ||
126 | // There is nothing to do, relation can be used in ^relation expressions | ||
127 | if(transformToHostedField(relation,trace)) { | ||
128 | trace.relationInTransitiveToHosterField.put(relation,relation.lookup(trace.relationDeclaration2Field)) | ||
129 | } else { | ||
130 | trace.relationInTransitiveToGlobalField.put(relation,relation.lookup(trace.relationDeclaration2Global)) | ||
131 | } | ||
132 | } | ||
133 | public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { | ||
134 | if(relation.parameters.size === 2) { | ||
135 | /** 1. Create a relation that can be used in ^relation expressions */ | ||
136 | val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace) | ||
137 | trace.relationInTransitiveToHosterField.put(relation,declaration) | ||
138 | /** 2. Add fact that the declaration corresponds to the definition */ | ||
139 | val fact = createALSFactDeclaration => [ | ||
140 | it.name = '''EqualsAsDeclaration «relation.name»''' | ||
141 | it.term = createALSQuantifiedEx => [ | ||
142 | val a = createALSVariableDeclaration => [ | ||
143 | it.name = "a" | ||
144 | it.range = base.transformTypeReference(relation.parameters.get(0),trace) | ||
145 | ] | ||
146 | val b = createALSVariableDeclaration => [ | ||
147 | it.name = "b" | ||
148 | it.range = base.transformTypeReference(relation.parameters.get(1),trace) | ||
149 | ] | ||
150 | it.variables += a | ||
151 | it.variables += b | ||
152 | it.type = ALSMultiplicity::ALL | ||
153 | it.expression = createALSIff => [ | ||
154 | it.leftOperand = createALSFunctionCall => [ | ||
155 | it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) | ||
156 | it.params += createALSReference => [ it.referred = a ] | ||
157 | it.params += createALSReference => [ it.referred = b ] | ||
158 | ] | ||
159 | it.rightOperand = createALSSubset => [ | ||
160 | it.leftOperand = createALSJoin => [ | ||
161 | it.leftOperand = createALSReference => [ referred = a ] | ||
162 | it.rightOperand = createALSReference => [ referred = b ] | ||
163 | ] | ||
164 | it.rightOperand = createALSJoin => [ | ||
165 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
166 | rightOperand = createALSReference => [ referred = declaration ] | ||
167 | ] | ||
168 | ] | ||
169 | ] | ||
170 | ] | ||
171 | ] | ||
172 | trace.specification.factDeclarations += fact | ||
173 | return | ||
174 | } else { | ||
175 | throw new AssertionError('''A non-binary relation "«relation.name»" is used in transitive clousure!''') | ||
176 | } | ||
177 | } | ||
178 | |||
179 | def public transformTransitiveRelationReference(Relation relation, ALSTerm source, ALSTerm target, Logic2AlloyLanguageMapperTrace trace) { | ||
180 | val alsTargetRelation = if(trace.relationInTransitiveToGlobalField.containsKey(relation)) { | ||
181 | createALSJoin => [ | ||
182 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
183 | rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] | ||
184 | ] | ||
185 | } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ | ||
186 | createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] | ||
187 | } else { | ||
188 | throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') | ||
189 | } | ||
190 | return createALSSubset => [ | ||
191 | it.leftOperand = createALSJoin => [ | ||
192 | it.leftOperand = source | ||
193 | it.rightOperand = target | ||
194 | ] | ||
195 | it.rightOperand = createAlSTransitiveClosure => [it.operand = alsTargetRelation] | ||
196 | |||
197 | ] | ||
198 | } | ||
199 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend new file mode 100644 index 00000000..0b8d2857 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend | |||
@@ -0,0 +1,207 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEquals | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSReference | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration | ||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
14 | import java.util.ArrayList | ||
15 | import java.util.HashMap | ||
16 | import java.util.List | ||
17 | import java.util.Map | ||
18 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
19 | |||
20 | class Logic2AlloyLanguageMapper_Support { | ||
21 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
22 | |||
23 | /// ID handling | ||
24 | def protected String toIDMultiple(String... ids) { | ||
25 | ids.map[it.split("\\s+").join("'")].join("'") | ||
26 | } | ||
27 | |||
28 | def protected String toID(String ids) { | ||
29 | ids.split("\\s+").join("'") | ||
30 | } | ||
31 | def protected String toID(List<String> ids) { | ||
32 | ids.map[it.split("\\s+").join("'")].join("'") | ||
33 | } | ||
34 | |||
35 | /// Support functions | ||
36 | |||
37 | def protected getBooleanType(Logic2AlloyLanguageMapperTrace trace) { | ||
38 | if(trace.boolType!=null) { | ||
39 | return trace.boolType | ||
40 | } else { | ||
41 | trace.boolType = createALSEnumDeclaration => [ | ||
42 | it.name = toID(#["util","boolean"]) | ||
43 | trace.boolTrue = createALSEnumLiteral =>[it.name=toID(#["util","boolean","true"])] | ||
44 | it.literal += trace.boolTrue | ||
45 | trace.boolFalse = createALSEnumLiteral =>[it.name=toID(#["util","boolean","false"])] | ||
46 | it.literal += trace.boolFalse | ||
47 | ] | ||
48 | trace.specification.enumDeclarations+=trace.boolType | ||
49 | return trace.boolType | ||
50 | } | ||
51 | } | ||
52 | def protected getBooleanTrue(Logic2AlloyLanguageMapperTrace trace) { | ||
53 | getBooleanType(trace) | ||
54 | return trace.boolTrue | ||
55 | } | ||
56 | def protected getBooleanFalse(Logic2AlloyLanguageMapperTrace trace) { | ||
57 | getBooleanType(trace) | ||
58 | return trace.boolFalse | ||
59 | } | ||
60 | |||
61 | def protected booleanToLogicValue(ALSTerm boolReference, Logic2AlloyLanguageMapperTrace trace) { | ||
62 | //println((boolReference as ALSReference).referred) | ||
63 | createALSEquals => [ | ||
64 | leftOperand = EcoreUtil.copy(boolReference) | ||
65 | rightOperand = createALSReference => [referred = getBooleanTrue(trace)] | ||
66 | ] | ||
67 | } | ||
68 | def protected booleanToEnumValue(ALSTerm value, Logic2AlloyLanguageMapperTrace trace) { | ||
69 | if(value instanceof ALSEquals) { | ||
70 | val rightOperand = value.rightOperand | ||
71 | if(rightOperand instanceof ALSReference) { | ||
72 | if(rightOperand.referred == getBooleanTrue(trace)) { | ||
73 | return value.leftOperand | ||
74 | } | ||
75 | } | ||
76 | } | ||
77 | return value; | ||
78 | } | ||
79 | def protected prepareParameterOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) { | ||
80 | if(type instanceof BoolTypeReference) { | ||
81 | return booleanToEnumValue(term,trace) | ||
82 | } | ||
83 | else return term | ||
84 | } | ||
85 | def protected postprocessResultOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) { | ||
86 | if(type instanceof BoolTypeReference) { | ||
87 | return booleanToLogicValue(term,trace) | ||
88 | } | ||
89 | else return term | ||
90 | } | ||
91 | |||
92 | def protected ALSTerm unfoldAnd(List<? extends ALSTerm> operands) { | ||
93 | if(operands.size == 1) { return operands.head } | ||
94 | else if(operands.size > 1) { return createALSAnd=>[ | ||
95 | leftOperand=operands.head | ||
96 | rightOperand=operands.subList(1,operands.size).unfoldAnd | ||
97 | ]} | ||
98 | else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') | ||
99 | } | ||
100 | |||
101 | def protected ALSTerm unfoldOr(List<? extends ALSTerm> operands, Logic2AlloyLanguageMapperTrace trace) { | ||
102 | if(operands.size == 0) { return unfoldTrueStatement(trace)} | ||
103 | else if(operands.size == 1) { return operands.head } | ||
104 | else if(operands.size > 1) { return createALSOr=>[ | ||
105 | leftOperand=operands.head | ||
106 | rightOperand=unfoldOr(operands.subList(1,operands.size),trace) | ||
107 | ]} | ||
108 | //else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') | ||
109 | } | ||
110 | |||
111 | protected def unfoldTrueStatement(Logic2AlloyLanguageMapperTrace trace) { | ||
112 | createALSEquals => [ | ||
113 | it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)] | ||
114 | it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)] | ||
115 | ] | ||
116 | } | ||
117 | |||
118 | protected def unfoldTFalseStatement(Logic2AlloyLanguageMapper m, Logic2AlloyLanguageMapperTrace trace) { | ||
119 | createALSEquals => [ | ||
120 | it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)] | ||
121 | it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)] | ||
122 | ] | ||
123 | } | ||
124 | |||
125 | def protected ALSTerm unfoldPlus(List<? extends ALSTerm> operands) { | ||
126 | if(operands.size == 1) { return operands.head } | ||
127 | else if(operands.size > 1) { return createALSPlus=>[ | ||
128 | leftOperand=operands.head | ||
129 | rightOperand=operands.subList(1,operands.size).unfoldPlus | ||
130 | ]} | ||
131 | else return createALSNone | ||
132 | } | ||
133 | |||
134 | def protected ALSTerm unfoldIntersection(List<? extends ALSTerm> operands) { | ||
135 | if(operands.size == 1) { return operands.head } | ||
136 | else if(operands.size > 1) { return createALSIntersection=>[ | ||
137 | leftOperand=operands.head | ||
138 | rightOperand=operands.subList(1,operands.size).unfoldIntersection | ||
139 | ]} | ||
140 | else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') | ||
141 | } | ||
142 | |||
143 | def protected ALSTerm unfoldDistinctTerms(Logic2AlloyLanguageMapper m, List<Term> operands, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
144 | if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) } | ||
145 | else if(operands.size > 1) { | ||
146 | val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2) | ||
147 | for(i:0..<operands.size) { | ||
148 | for(j: i+1..<operands.size) { | ||
149 | notEquals+=createALSNotEquals=>[ | ||
150 | leftOperand = m.transformTerm(operands.get(i),trace,variables) | ||
151 | rightOperand = m.transformTerm(operands.get(j),trace,variables) | ||
152 | ] | ||
153 | } | ||
154 | } | ||
155 | return notEquals.unfoldAnd | ||
156 | } | ||
157 | else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') | ||
158 | } | ||
159 | |||
160 | def protected ALSTerm unfoldReferenceDirectProduct(Logic2AlloyLanguageMapper m, List<TypeReference> references,Logic2AlloyLanguageMapperTrace trace) { | ||
161 | if(references.size == 1) return m.transformTypeReference(references.head,trace) | ||
162 | else if(references.size > 1) return createALSDirectProduct => [ | ||
163 | it.leftOperand = m.transformTypeReference(references.head,trace) | ||
164 | it.rightOperand = unfoldReferenceDirectProduct(m,references.subList(1,references.size),trace) | ||
165 | ] | ||
166 | else throw new UnsupportedOperationException | ||
167 | } | ||
168 | |||
169 | def protected ALSTerm unfoldDotJoin(Logic2AlloyLanguageMapper m, List<Term> elements, ALSTerm target, Logic2AlloyLanguageMapperTrace trace, | ||
170 | Map<Variable, ALSVariableDeclaration> variables) { | ||
171 | if (elements.size == 1) { | ||
172 | return createALSJoin => [ | ||
173 | it.leftOperand = m.transformTerm(elements.head,trace, variables) | ||
174 | it.rightOperand = target | ||
175 | ] | ||
176 | } else if (elements.size > 1) { | ||
177 | return createALSJoin => [ | ||
178 | it.leftOperand = m.transformTerm(elements.last,trace, variables) | ||
179 | it.rightOperand = m.unfoldDotJoin(elements.subList(0, elements.size - 1), target, trace, variables) | ||
180 | ] | ||
181 | } else | ||
182 | throw new UnsupportedOperationException | ||
183 | } | ||
184 | |||
185 | def protected ALSTerm unfoldTermDirectProduct(Logic2AlloyLanguageMapper m, List<Term> references,Logic2AlloyLanguageMapperTrace trace,Map<Variable, ALSVariableDeclaration> variables) { | ||
186 | if(references.size == 1) return m.transformTerm(references.head,trace,variables) | ||
187 | else if(references.size > 1) return createALSDirectProduct => [ | ||
188 | it.leftOperand = m.transformTerm(references.head,trace,variables) | ||
189 | it.rightOperand = unfoldTermDirectProduct(m,references.subList(1,references.size),trace, variables) | ||
190 | ] | ||
191 | else throw new UnsupportedOperationException | ||
192 | } | ||
193 | |||
194 | def protected createQuantifiedExpression(Logic2AlloyLanguageMapper m, QuantifiedExpression q, ALSMultiplicity multiplicity, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
195 | val variableMap = q.quantifiedVariables.toInvertedMap[v | createALSVariableDeclaration=> [ | ||
196 | it.name = toID(v.name) | ||
197 | it.range = m.transformTypeReference(v.range,trace) ]] | ||
198 | |||
199 | createALSQuantifiedEx=>[ | ||
200 | it.type = multiplicity | ||
201 | it.variables += variableMap.values | ||
202 | it.expression = m.transformTerm(q.expression,trace,variables.withAddition(variableMap)) | ||
203 | ] | ||
204 | } | ||
205 | |||
206 | def protected withAddition(Map<Variable, ALSVariableDeclaration> v1, Map<Variable, ALSVariableDeclaration> v2) { new HashMap(v1) => [putAll(v2)] } | ||
207 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend new file mode 100644 index 00000000..c998de1f --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend | |||
@@ -0,0 +1,18 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
7 | import java.util.Collection | ||
8 | import java.util.List | ||
9 | |||
10 | interface Logic2AlloyLanguageMapper_TypeMapper { | ||
11 | def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace); | ||
12 | def List<ALSSignatureDeclaration> transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) | ||
13 | def ALSSignatureDeclaration getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) | ||
14 | def int getUndefinedSupertypeScope(int undefinedScope,Logic2AlloyLanguageMapperTrace trace) | ||
15 | def ALSTerm transformReference(DefinedElement referred,Logic2AlloyLanguageMapperTrace trace) | ||
16 | |||
17 | def AlloyModelInterpretation_TypeInterpretation getTypeInterpreter() | ||
18 | } | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend new file mode 100644 index 00000000..17b1a87b --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend | |||
@@ -0,0 +1,15 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import java.util.HashMap | ||
7 | import java.util.Map | ||
8 | |||
9 | class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
10 | implements Logic2AlloyLanguageMapper_TypeMapperTrace | ||
11 | { | ||
12 | public var ALSSignatureDeclaration objectSupperClass; | ||
13 | public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap; | ||
14 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap | ||
15 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend new file mode 100644 index 00000000..1b04a877 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend | |||
@@ -0,0 +1,15 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import java.util.HashMap | ||
7 | import java.util.List | ||
8 | import java.util.Map | ||
9 | |||
10 | class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace { | ||
11 | public var ALSSignatureDeclaration objectSupperClass; | ||
12 | public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap; | ||
13 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap | ||
14 | public val Map<Type, List<ALSSignatureDeclaration>> typeSelection = new HashMap | ||
15 | } | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..9e548ab6 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | |||
@@ -0,0 +1,263 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
13 | import java.util.ArrayList | ||
14 | import java.util.Collection | ||
15 | import java.util.HashMap | ||
16 | import java.util.List | ||
17 | |||
18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
19 | |||
20 | /** | ||
21 | * Each object is an element of an Object set, and types are subsets of the objects. | ||
22 | */ | ||
23 | class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyLanguageMapper_TypeMapper{ | ||
24 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
25 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
26 | |||
27 | new() { | ||
28 | // Initialize package | ||
29 | LogicproblemPackage.eINSTANCE.class | ||
30 | } | ||
31 | |||
32 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
33 | val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
34 | trace.typeMapperTrace = typeTrace | ||
35 | |||
36 | // 1. A global type for Objects is created | ||
37 | val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])] | ||
38 | val objectBody = createALSSignatureBody => [ | ||
39 | it.declarations += objectSig | ||
40 | it.abstract = true | ||
41 | ] | ||
42 | typeTrace.objectSupperClass = objectSig | ||
43 | trace.specification.signatureBodies += objectBody | ||
44 | |||
45 | // 2. Each type is mapped to a unique sig | ||
46 | for(type : types) { | ||
47 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)] | ||
48 | val body = createALSSignatureBody => [it.declarations += sig] | ||
49 | trace.specification.signatureBodies += body | ||
50 | typeTrace.type2ALSType.put(type,sig) | ||
51 | } | ||
52 | |||
53 | // 3. The elements of a defined type is mapped to singleton signatures | ||
54 | // 3.1 Collect the elements | ||
55 | val elementMatcher = TypeQueries.instance.getLowestCommonSupertypeOfAllOccuranceOfElement(trace.incqueryEngine) | ||
56 | val topmostType2Elements = new HashMap<ALSSignatureDeclaration,List<DefinedElement>> | ||
57 | for(element : elements) { | ||
58 | val topmostTypes = elementMatcher.getAllValuesOftype(element) | ||
59 | var ALSSignatureDeclaration selectedTopmostType; | ||
60 | if(topmostTypes.empty) { | ||
61 | selectedTopmostType = objectSig | ||
62 | } else{ | ||
63 | selectedTopmostType = topmostTypes.head.lookup(typeTrace.type2ALSType) | ||
64 | } | ||
65 | topmostType2Elements.putOrAddToList(selectedTopmostType,element) | ||
66 | } | ||
67 | |||
68 | // 4. For each topmost types several singleton classes are generated, which represents the elements. | ||
69 | // For the sake of clarity, common bodies are used. | ||
70 | for(topmostEntry : topmostType2Elements.entrySet) { | ||
71 | |||
72 | for(element : topmostEntry.value) { | ||
73 | val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] | ||
74 | typeTrace.definedElement2Declaration.put(element,signature) | ||
75 | } | ||
76 | |||
77 | val body = createALSSignatureBody => [ | ||
78 | it.multiplicity = ALSMultiplicity.ONE | ||
79 | it.declarations += topmostEntry.value.map[it.lookup(typeTrace.definedElement2Declaration)] | ||
80 | ] | ||
81 | |||
82 | val containerLogicType = topmostEntry.key | ||
83 | body.superset += containerLogicType | ||
84 | |||
85 | trace.specification.signatureBodies+=body | ||
86 | } | ||
87 | |||
88 | // 5.1 Each Defined Type is specified as the union of its elements | ||
89 | for(definedType : types.filter(TypeDefinition)) { | ||
90 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
91 | it.name = support.toIDMultiple("typedefinition",definedType.name) | ||
92 | it.term = createALSEquals => [ | ||
93 | it.leftOperand = createALSReference => [ it.referred = definedType.lookup(typeTrace.type2ALSType) ] | ||
94 | it.rightOperand = support.unfoldPlus(definedType.elements.map[e| | ||
95 | createALSReference => [it.referred = e.lookup(typeTrace.definedElement2Declaration)]]) | ||
96 | ] | ||
97 | ] | ||
98 | } | ||
99 | // 5.2 Each Defined Element is unique | ||
100 | for(definedType : types.filter(TypeDefinition)) { | ||
101 | val allElementsIncludingSubtypes = | ||
102 | definedType.<Type>transitiveClosureStar[it.subtypes].filter(TypeDefinition) | ||
103 | .map[elements].flatten.toSet.toList | ||
104 | if(allElementsIncludingSubtypes.size>=2) { | ||
105 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
106 | it.name = support.toIDMultiple("typeElementsUnique",definedType.name) | ||
107 | it.term = unfoldDistinctElements(allElementsIncludingSubtypes,trace) | ||
108 | ] | ||
109 | } | ||
110 | } | ||
111 | |||
112 | // 6. Each inheritance is modeled by subset operator 'in' | ||
113 | for(type : types) { | ||
114 | val sigBody = type.lookup(typeTrace.type2ALSType).eContainer as ALSSignatureBody | ||
115 | if(type.supertypes.empty) { | ||
116 | sigBody.superset += typeTrace.objectSupperClass | ||
117 | } else { | ||
118 | sigBody.superset += type.supertypes.map[lookup(typeTrace.type2ALSType)] | ||
119 | } | ||
120 | } | ||
121 | |||
122 | |||
123 | // 7. Each type is in the intersection of the supertypes | ||
124 | for(type : types.filter[it.supertypes.size>=2]) { | ||
125 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
126 | it.name = support.toIDMultiple("abstract",type.name) | ||
127 | it.term = createALSEquals => [ | ||
128 | it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] | ||
129 | it.rightOperand = support.unfoldIntersection(type.supertypes.map[e| | ||
130 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
131 | ] | ||
132 | ] | ||
133 | } | ||
134 | |||
135 | // 8. Each abstract type is equal to the union of the subtypes | ||
136 | for(type : types.filter[isIsAbstract]) { | ||
137 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
138 | it.name = support.toIDMultiple("abstract",type.name) | ||
139 | it.term = createALSEquals => [ | ||
140 | it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] | ||
141 | it.rightOperand = support.unfoldPlus(type.subtypes.map[e| | ||
142 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
143 | ] | ||
144 | ] | ||
145 | } | ||
146 | // 8.1 The object type is the union of the root types. | ||
147 | val rootTypes = types.filter[it.supertypes.empty].toList | ||
148 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
149 | it.name = support.toIDMultiple(#["ObjectTypeDefinition"]) | ||
150 | it.term = createALSEquals => [ | ||
151 | it.leftOperand = createALSReference => [ it.referred = typeTrace.objectSupperClass ] | ||
152 | it.rightOperand = support.unfoldPlus(rootTypes.map[e| | ||
153 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
154 | ] | ||
155 | ] | ||
156 | |||
157 | // 9. For each type X (including Object) | ||
158 | // only the common subtypes are in the intersection | ||
159 | // of the two subtype. | ||
160 | // 9.1. for the object | ||
161 | { | ||
162 | val rootTypeList = types.filter[it.supertypes.empty].toList | ||
163 | for(type1Index: 0..<rootTypeList.size) { | ||
164 | for(type2Index: 0..<type1Index) { | ||
165 | trace.specification.factDeclarations += | ||
166 | commonSubtypeOnlyInDiamonds(rootTypeList.get(type1Index),rootTypeList.get(type2Index),trace) | ||
167 | } | ||
168 | } | ||
169 | } | ||
170 | |||
171 | //9.3 for the subtypes of each objects | ||
172 | { | ||
173 | for(inScope : types) { | ||
174 | val subtypeList = inScope.subtypes//.toList | ||
175 | if(subtypeList.size>=2) { | ||
176 | for(type1Index: 0..<subtypeList.size) { | ||
177 | for(type2Index: 0..<type1Index) { | ||
178 | trace.specification.factDeclarations += | ||
179 | commonSubtypeOnlyInDiamonds(subtypeList.get(type1Index),subtypeList.get(type2Index),trace) | ||
180 | } | ||
181 | } | ||
182 | } | ||
183 | } | ||
184 | } | ||
185 | } | ||
186 | |||
187 | private def isEnumlikeType(Type type) { | ||
188 | if(type instanceof TypeDefinition) { | ||
189 | val elements = type.elements | ||
190 | return elements.forall[it.definedInType.size === 1 && it.definedInType.head === type] | ||
191 | } | ||
192 | return false | ||
193 | } | ||
194 | |||
195 | private def isEnumlikeElement(DefinedElement d) { | ||
196 | d.definedInType.size === 1 && d.definedInType.head.isEnumlikeType | ||
197 | } | ||
198 | |||
199 | def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) { | ||
200 | val res = trace.typeMapperTrace | ||
201 | if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes) { | ||
202 | return res | ||
203 | } else { | ||
204 | throw new IllegalArgumentException(''' | ||
205 | Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name», | ||
206 | but found «res.class.name»''') | ||
207 | } | ||
208 | } | ||
209 | |||
210 | def private commonSubtypeOnlyInDiamonds(Type t1, Type t2, Logic2AlloyLanguageMapperTrace trace) { | ||
211 | val topmostCommonSubtypes = TypeQueries.instance.getTopmostCommonSubtypes(trace.incqueryEngine) | ||
212 | val allTopmostCommon = topmostCommonSubtypes.getAllValuesOfcommon(t1,t2).toList | ||
213 | return createALSFactDeclaration => [ | ||
214 | it.name = support.toIDMultiple("common","types",t1.name,t2.name) | ||
215 | it.term = createALSEquals => [ | ||
216 | it.leftOperand = createALSIntersection => [ | ||
217 | it.leftOperand = createALSReference => [it.referred = t1.lookup(trace.typeTrace.type2ALSType)] | ||
218 | it.rightOperand = createALSReference => [it.referred = t2.lookup(trace.typeTrace.type2ALSType)] | ||
219 | ] | ||
220 | it.rightOperand = support.unfoldPlus(allTopmostCommon.map[t|createALSReference => [it.referred = t.lookup(trace.typeTrace.type2ALSType)]]) | ||
221 | ] | ||
222 | ] | ||
223 | } | ||
224 | |||
225 | def private unfoldDistinctElements( | ||
226 | List<DefinedElement> operands, | ||
227 | Logic2AlloyLanguageMapperTrace trace | ||
228 | ) { | ||
229 | if(operands.size == 1 || operands.size == 0) {support.unfoldTrueStatement(trace);} | ||
230 | else { | ||
231 | val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2) | ||
232 | for(i:0..<operands.size) { | ||
233 | for(j: i+1..<operands.size) { | ||
234 | notEquals+=createALSNotEquals=>[ | ||
235 | leftOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(i)) ] | ||
236 | rightOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(j)) ] | ||
237 | ] | ||
238 | } | ||
239 | } | ||
240 | return support.unfoldAnd(notEquals) | ||
241 | } | ||
242 | } | ||
243 | |||
244 | override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
245 | return #[trace.typeTrace.type2ALSType.get(referred)] | ||
246 | } | ||
247 | |||
248 | override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { | ||
249 | trace.typeTrace.objectSupperClass | ||
250 | } | ||
251 | |||
252 | override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { | ||
253 | createALSReference => [it.referred = referred.lookup(trace.typeTrace.definedElement2Declaration)] | ||
254 | } | ||
255 | |||
256 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { | ||
257 | if(undefinedScope == Integer.MAX_VALUE) return undefinedScope else return undefinedScope + trace.typeTrace.definedElement2Declaration.size | ||
258 | } | ||
259 | |||
260 | override getTypeInterpreter() { | ||
261 | return new AlloyModelInterpretation_TypeInterpretation_FilteredTypes | ||
262 | } | ||
263 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend new file mode 100644 index 00000000..7d90b2b0 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend | |||
@@ -0,0 +1,122 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
10 | import java.util.Collection | ||
11 | import java.util.LinkedList | ||
12 | |||
13 | class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{ | ||
14 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
15 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
16 | |||
17 | new() { | ||
18 | LogicproblemPackage.eINSTANCE.class | ||
19 | } | ||
20 | |||
21 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
22 | val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal | ||
23 | trace.typeMapperTrace = typeTrace | ||
24 | |||
25 | // 1. A global type for Objects is created | ||
26 | val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])] | ||
27 | val objectBody = createALSSignatureBody => [ | ||
28 | it.declarations += objectSig | ||
29 | it.abstract = true | ||
30 | ] | ||
31 | typeTrace.objectSupperClass = objectSig | ||
32 | trace.specification.signatureBodies += objectBody | ||
33 | |||
34 | // 2. Each type is mapped to a unique sig | ||
35 | for(type : types) { | ||
36 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)] | ||
37 | val body = createALSSignatureBody => [it.declarations += sig] | ||
38 | body.abstract = type.isIsAbstract || (type instanceof TypeDefinition) | ||
39 | |||
40 | trace.specification.signatureBodies += body | ||
41 | typeTrace.type2ALSType.put(type,sig) | ||
42 | |||
43 | typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)]) | ||
44 | } | ||
45 | |||
46 | for(element : elements) { | ||
47 | val mostSpecificTypes = element.definedInType.filter[it.subtypes.empty] | ||
48 | if(mostSpecificTypes.size== 1) { | ||
49 | val mostSpecificSubtype = mostSpecificTypes.head | ||
50 | val elementContainer = createALSSignatureBody => [ | ||
51 | it.multiplicity = ALSMultiplicity::ONE | ||
52 | it.supertype =typeTrace.type2ALSType.get(mostSpecificSubtype) | ||
53 | ] | ||
54 | val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] | ||
55 | elementContainer.declarations += signature | ||
56 | typeTrace.definedElement2Declaration.put(element,signature) | ||
57 | trace.specification.signatureBodies += elementContainer | ||
58 | } else { | ||
59 | throw new UnsupportedOperationException | ||
60 | } | ||
61 | } | ||
62 | |||
63 | // 6. Each inheritance is modeled by extend keyword | ||
64 | for(type : types) { | ||
65 | if(type.supertypes.size == 0) { | ||
66 | (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = typeTrace.objectSupperClass | ||
67 | }if(type.supertypes.size == 1) { | ||
68 | val alsType = typeTrace.type2ALSType.get(type.supertypes.head) | ||
69 | (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsType | ||
70 | |||
71 | } else if(type.supertypes.size > 1){ | ||
72 | val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head) | ||
73 | (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsMainType | ||
74 | for(otherType : type.supertypes.filter[it != alsMainType]) { | ||
75 | typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(type)) | ||
76 | } | ||
77 | } | ||
78 | } | ||
79 | } | ||
80 | |||
81 | private def boolean hasDefinedSupertype(Type type) { | ||
82 | if(type instanceof TypeDefinition) { | ||
83 | return true | ||
84 | } else { | ||
85 | if(type.supertypes.empty) return false | ||
86 | else return type.supertypes.exists[it.hasDefinedSupertype] | ||
87 | } | ||
88 | } | ||
89 | |||
90 | def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) { | ||
91 | val res = trace.typeMapperTrace | ||
92 | if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal) { | ||
93 | return res | ||
94 | } else { | ||
95 | throw new IllegalArgumentException(''' | ||
96 | Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name», | ||
97 | but found «res.class.name»''') | ||
98 | } | ||
99 | } | ||
100 | |||
101 | override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
102 | trace.typeTrace.typeSelection.get(referred) | ||
103 | } | ||
104 | |||
105 | override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { | ||
106 | trace.typeTrace.objectSupperClass | ||
107 | } | ||
108 | |||
109 | override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { | ||
110 | val r = trace.typeTrace.definedElement2Declaration.get(referred) | ||
111 | return createALSReference => [it.referred =r] | ||
112 | } | ||
113 | |||
114 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { | ||
115 | return undefinedScope + trace.typeTrace.definedElement2Declaration.size | ||
116 | } | ||
117 | |||
118 | override getTypeInterpreter() { | ||
119 | return new AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal | ||
120 | } | ||
121 | |||
122 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend new file mode 100644 index 00000000..fdc35412 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend | |||
@@ -0,0 +1,105 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
10 | import java.util.LinkedList | ||
11 | import java.util.List | ||
12 | |||
13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
14 | |||
15 | class RunCommandMapper { | ||
16 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
17 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
18 | private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | ||
19 | |||
20 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | ||
21 | this.typeMapper = typeMapper | ||
22 | } | ||
23 | |||
24 | def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) | ||
25 | { | ||
26 | //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size | ||
27 | |||
28 | // add fact to ensure the existence of all literals in the scope | ||
29 | if(!config.typeScopes.knownStrings.empty) { | ||
30 | specification.factDeclarations += createALSFactDeclaration => [ | ||
31 | it.name = "EnsureAllStrings" | ||
32 | val List<? extends ALSTerm> equals = config.typeScopes.knownStrings.map[x|createALSEquals => [ | ||
33 | it.leftOperand =createALSStringLiteral => [it.value = x] | ||
34 | it.rightOperand =createALSStringLiteral => [it.value = x] | ||
35 | ]].toList | ||
36 | it.term = support.unfoldAnd(equals) | ||
37 | ] | ||
38 | } | ||
39 | val typeScopes = new LinkedList | ||
40 | for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) { | ||
41 | val key = definedScope.key | ||
42 | val amount = definedScope.value | ||
43 | val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount | ||
44 | |||
45 | val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet | ||
46 | if(amount == 0 && exactly) { | ||
47 | specification.factDeclarations += createALSFactDeclaration => [ | ||
48 | it.term = createALSEquals => [ | ||
49 | it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
50 | it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) | ||
51 | ] | ||
52 | ] | ||
53 | } | ||
54 | val int n = existing.size-amount | ||
55 | typeScopes += createALSSigScope => [ | ||
56 | it.type = typeMapper.transformTypeReference(key,mapper,trace).head | ||
57 | it.number = n | ||
58 | it.exactly =exactly | ||
59 | ] | ||
60 | } | ||
61 | |||
62 | specification.runCommand = createALSRunCommand => [ | ||
63 | it.typeScopes+= createALSSigScope => [ | ||
64 | it.type= typeMapper.getUndefinedSupertype(trace) | ||
65 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | ||
66 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | ||
67 | ] | ||
68 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | ||
69 | val integersUsed = specification.eAllContents.filter(ALSInt) | ||
70 | if(integersUsed.empty) { | ||
71 | // If no integer scope is defined, but the problem has no integers | ||
72 | // => scope can be empty | ||
73 | it.typeScopes+= createALSIntScope => [ | ||
74 | it.number = 0 | ||
75 | ] | ||
76 | } else { | ||
77 | // If no integer scope is defined, and the problem has integers | ||
78 | // => error | ||
79 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') | ||
80 | } | ||
81 | } else { | ||
82 | it.typeScopes += createALSIntScope => [ | ||
83 | if(config.typeScopes.knownIntegers.empty) { | ||
84 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | ||
85 | } else { | ||
86 | var scope = Math.max( | ||
87 | Math.abs(config.typeScopes.knownIntegers.max), | ||
88 | Math.abs(config.typeScopes.knownIntegers.min)) | ||
89 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
90 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
91 | } | ||
92 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 | ||
93 | } | ||
94 | ] | ||
95 | } | ||
96 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | ||
97 | throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') | ||
98 | } else { | ||
99 | if(config.typeScopes.maxNewStrings != 0) { | ||
100 | it.typeScopes += createALSStringScope => [it.number = 0] | ||
101 | } | ||
102 | } | ||
103 | ] | ||
104 | } | ||
105 | } \ No newline at end of file | ||