diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-06-10 19:05:05 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-06-10 19:05:05 +0200 |
commit | 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch) | |
tree | 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder | |
parent | Initial commit, migrating from SVN (diff) | |
download | VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip |
Migrating Additional projects
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder')
14 files changed, 2510 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend new file mode 100644 index 00000000..637752b0 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | |||
@@ -0,0 +1,48 @@ | |||
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, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { | ||
10 | if(solution == null) { | ||
11 | return createInsuficientResourcesResult => [ | ||
12 | it.problem = problem | ||
13 | it.statistics = transformStatistics(solution,transformationTime) | ||
14 | ] | ||
15 | } else { | ||
16 | val logicResult = solution.solution | ||
17 | if(logicResult.satisfiable) { | ||
18 | return createModelResult => [ | ||
19 | it.problem = problem | ||
20 | it.representation += solution | ||
21 | it.maxInteger = logicResult.max | ||
22 | it.minInteger = logicResult.min | ||
23 | it.trace = trace | ||
24 | it.statistics = transformStatistics(solution,transformationTime) | ||
25 | ] | ||
26 | } else { | ||
27 | return createInconsistencyResult => [ | ||
28 | it.problem = problem | ||
29 | //trace? | ||
30 | it.statistics = transformStatistics(solution,transformationTime) | ||
31 | ] | ||
32 | } | ||
33 | } | ||
34 | } | ||
35 | |||
36 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { | ||
37 | createStatistics => [ | ||
38 | it.transformationTime = transformationTime as int | ||
39 | if(solution != null) { | ||
40 | it.solverTime = solution.runtimeTime as int | ||
41 | it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [ | ||
42 | it.name = "KoodkodToCNFTransformationTime" | ||
43 | it.value = solution.getKodkodTime as int | ||
44 | ] | ||
45 | } | ||
46 | ] | ||
47 | } | ||
48 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend new file mode 100644 index 00000000..6bac4130 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | |||
@@ -0,0 +1,145 @@ | |||
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.A4Solution | ||
11 | import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod | ||
12 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
13 | import java.util.LinkedList | ||
14 | import java.util.List | ||
15 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | ||
16 | import org.eclipse.xtend.lib.annotations.Data | ||
17 | import java.util.Map | ||
18 | import java.util.HashMap | ||
19 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver | ||
20 | import org.eclipse.emf.common.CommonPlugin | ||
21 | import java.util.ArrayList | ||
22 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
23 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
24 | |||
25 | class AlloySolverException extends Exception{ | ||
26 | new(String s) { super(s) } | ||
27 | new(String s, Exception e) { super(s,e) } | ||
28 | new(String s, List<String> errors, Exception e) { | ||
29 | super(s + '\n' + errors.join('\n'), e) | ||
30 | } | ||
31 | } | ||
32 | |||
33 | @Data class MonitoredAlloySolution{ | ||
34 | List<String> warnings | ||
35 | List<String> debugs | ||
36 | long kodkodTime | ||
37 | long runtimeTime | ||
38 | |||
39 | A4Solution solution | ||
40 | } | ||
41 | |||
42 | class AlloyHandler { | ||
43 | |||
44 | //val fileName = "problem.als" | ||
45 | |||
46 | public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, String alloyCode) { | ||
47 | //Prepare | ||
48 | |||
49 | val warnings = new LinkedList<String> | ||
50 | val debugs = new LinkedList<String> | ||
51 | val runtime = new ArrayList<Long> | ||
52 | val reporter = new A4Reporter() { | ||
53 | override debug(String message) { debugs += message } | ||
54 | override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
55 | override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
56 | override warning(ErrorWarning msg) { warnings += msg.message } | ||
57 | } | ||
58 | |||
59 | val options = new A4Options() => [ | ||
60 | it.symmetry = configuration.symmetry | ||
61 | it.noOverflow = true | ||
62 | it.solver = getSolver(configuration.solver, configuration) | ||
63 | if(configuration.solver.externalSolver) { | ||
64 | it.solverDirectory = configuration.solverPath | ||
65 | } | ||
66 | it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString | ||
67 | ] | ||
68 | |||
69 | // Transform | ||
70 | var Command command = null; | ||
71 | var CompModule compModule = null | ||
72 | |||
73 | val kodkodTransformStart = System.currentTimeMillis(); | ||
74 | |||
75 | try { | ||
76 | if(configuration.writeToFile) { | ||
77 | compModule = CompUtil.parseEverything_fromFile(reporter,null,path) | ||
78 | } else { | ||
79 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) | ||
80 | } | ||
81 | if(compModule.allCommands.size != 1) | ||
82 | throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') | ||
83 | command = compModule.allCommands.head | ||
84 | } catch (Err e){ | ||
85 | throw new AlloySolverException(e.message,warnings,e) | ||
86 | } | ||
87 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | ||
88 | |||
89 | //Execute | ||
90 | var A4Solution answer = null; | ||
91 | try { | ||
92 | answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | ||
93 | }catch(Exception e) { | ||
94 | warnings +=e.message | ||
95 | } | ||
96 | |||
97 | var long runtimeFromAnswer; | ||
98 | if(runtime.empty) { | ||
99 | runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish) | ||
100 | } else { | ||
101 | runtimeFromAnswer = runtime.head | ||
102 | } | ||
103 | |||
104 | return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer) | ||
105 | } | ||
106 | |||
107 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap | ||
108 | def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { | ||
109 | val config = new SolverConfiguration(backedSolver,path,options) | ||
110 | if(previousSolverConfigurations.containsKey(config)) { | ||
111 | return previousSolverConfigurations.get(config) | ||
112 | } else { | ||
113 | val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' | ||
114 | val newSolver = A4Options.SatSolver.make(id,id,path,options) | ||
115 | previousSolverConfigurations.put(config,newSolver) | ||
116 | return newSolver | ||
117 | } | ||
118 | } | ||
119 | |||
120 | def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { | ||
121 | switch(backedSolver){ | ||
122 | case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE | ||
123 | case SpearPIPE: return A4Options.SatSolver.SpearPIPE | ||
124 | case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI | ||
125 | case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI | ||
126 | case LingelingJNI: return A4Options.SatSolver.LingelingJNI | ||
127 | case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) | ||
128 | case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI | ||
129 | case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI | ||
130 | case SAT4J: return A4Options.SatSolver.SAT4J | ||
131 | case CNF: return A4Options.SatSolver.CNF | ||
132 | case KodKod: return A4Options.SatSolver.KK | ||
133 | } | ||
134 | } | ||
135 | |||
136 | def isExternalSolver(AlloyBackendSolver backedSolver) { | ||
137 | return !(backedSolver == AlloyBackendSolver.SAT4J) | ||
138 | } | ||
139 | } | ||
140 | |||
141 | @Data class SolverConfiguration { | ||
142 | AlloyBackendSolver backedSolver | ||
143 | String path | ||
144 | String[] options | ||
145 | } | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend new file mode 100644 index 00000000..d00291e0 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend | |||
@@ -0,0 +1,331 @@ | |||
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.Field | ||
5 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
15 | import java.util.Arrays | ||
16 | import java.util.HashMap | ||
17 | import java.util.LinkedList | ||
18 | import java.util.List | ||
19 | import java.util.Map | ||
20 | import java.util.Set | ||
21 | |||
22 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
23 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | ||
24 | import java.util.ArrayList | ||
25 | |||
26 | interface AlloyModelInterpretation_TypeInterpretation { | ||
27 | def void resolveUnknownAtoms( | ||
28 | Iterable<ExprVar> objectAtoms, | ||
29 | A4Solution solution, | ||
30 | Logic2AlloyLanguageMapperTrace forwardTrace, | ||
31 | Map<String, Sig> name2AlloySig, | ||
32 | Map<String, Field> name2AlloyField, | ||
33 | Map<String,DefinedElement> expression2DefinedElement, | ||
34 | Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) | ||
35 | } | ||
36 | |||
37 | class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{ | ||
38 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
39 | |||
40 | override resolveUnknownAtoms( | ||
41 | Iterable<ExprVar> objectAtoms, | ||
42 | A4Solution solution, | ||
43 | Logic2AlloyLanguageMapperTrace forwardTrace, | ||
44 | Map<String, Sig> name2AlloySig, | ||
45 | Map<String, Field> name2AlloyField, | ||
46 | Map<String,DefinedElement> expression2DefinedElement, | ||
47 | Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) | ||
48 | { | ||
49 | /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap() | ||
50 | val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/ | ||
51 | |||
52 | val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
53 | |||
54 | // 1. Evaluate the defined elements | ||
55 | for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) { | ||
56 | val name = definedElementMappingEntry.value.name | ||
57 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
58 | val elementsOfSingletonSignature = solution.eval(matchingSig) | ||
59 | if(elementsOfSingletonSignature.size != 1) { | ||
60 | throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''') | ||
61 | } else { | ||
62 | val expressionOfDefinedElement = elementsOfSingletonSignature.head.atom(0)// as ExprVar | ||
63 | expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key) | ||
64 | } | ||
65 | } | ||
66 | |||
67 | // 2. evaluate the signatures and create new elements if necessary | ||
68 | for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) { | ||
69 | val type = type2SingatureEntry.key | ||
70 | if(type instanceof TypeDeclaration) { | ||
71 | val name = type2SingatureEntry.value.name | ||
72 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
73 | val elementsOfSignature = solution.eval(matchingSig) | ||
74 | val elementList = new ArrayList(elementsOfSignature.size) | ||
75 | var newVariableIndex = 1; | ||
76 | for(elementOfSignature : elementsOfSignature) { | ||
77 | val expressionOfDefinedElement = elementOfSignature.atom(0) | ||
78 | if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) { | ||
79 | elementList += expressionOfDefinedElement.lookup(expression2DefinedElement) | ||
80 | } else { | ||
81 | val newElementName = '''newObject «newVariableIndex.toString»''' | ||
82 | val newRepresentation = createDefinedElement => [ | ||
83 | it.name = newElementName | ||
84 | ] | ||
85 | elementList += newRepresentation | ||
86 | expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation) | ||
87 | } | ||
88 | } | ||
89 | interpretationOfUndefinedType.put(type,elementList) | ||
90 | } | ||
91 | } | ||
92 | } | ||
93 | } | ||
94 | /* | ||
95 | class AlloyModelInterpretation_TypeInterpretation_Horizontal implements AlloyModelInterpretation_TypeInterpretation{ | ||
96 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
97 | |||
98 | override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String,DefinedElement> alloyAtom2LogicElement) { | ||
99 | val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap; | ||
100 | |||
101 | //TMP sig maps to identify alloy signatures by their names | ||
102 | val Map<String,Type> sigName2LogicType = | ||
103 | forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name] | ||
104 | //val Map<String,DefinedElement> elementNameNamel2DefinedElement = | ||
105 | // forwardTrace.definedElement2Declaration.keySet.toMap[x|forwardTrace.definedElement2Declaration.get(x).name] | ||
106 | |||
107 | // Fill the interpretation map with empty lists | ||
108 | forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x|interpretationOfUndefinedType.put(x,new LinkedList)] | ||
109 | |||
110 | // exporing individuals | ||
111 | for(atom: objectAtoms) { | ||
112 | val typeName = getName(atom.type) | ||
113 | //val atomName = atom.name | ||
114 | |||
115 | if(sigName2LogicType.containsKey(typeName)) { | ||
116 | val type = sigName2LogicType.get(typeName) | ||
117 | val elementsOfType = interpretationOfUndefinedType.get(type) | ||
118 | val element = createDefinedElement => [ | ||
119 | it.name += type.name | ||
120 | it.name += (elementsOfType.size+1).toString | ||
121 | ] | ||
122 | alloyAtom2LogicElement.put(atom.label,element) | ||
123 | elementsOfType+=element | ||
124 | } | ||
125 | else throw new UnsupportedOperationException('''Unknown atom: «atom»''') | ||
126 | } | ||
127 | |||
128 | return interpretationOfUndefinedType | ||
129 | } | ||
130 | |||
131 | def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) { | ||
132 | val name = type.toString | ||
133 | if(name.startsWith("{this/") && name.endsWith("}")) { | ||
134 | return type.toString.replaceFirst("\\{this\\/","").replace("}","") | ||
135 | } | ||
136 | else throw new IllegalArgumentException('''Unknown type format: "«name»"!''') | ||
137 | } | ||
138 | //def private getName(ExprVar atom) { atom.toString.split("\\$") } | ||
139 | }*/ | ||
140 | |||
141 | class AlloyModelInterpretation implements LogicModelInterpretation{ | ||
142 | |||
143 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
144 | protected val AlloyModelInterpretation_TypeInterpretation typeInterpretator | ||
145 | |||
146 | protected val Logic2AlloyLanguageMapper forwardMapper | ||
147 | protected val Logic2AlloyLanguageMapperTrace forwardTrace; | ||
148 | |||
149 | private var ExprVar logicLanguage; | ||
150 | |||
151 | private var String logicBooleanTrue; | ||
152 | private var String logicBooleanFalse; | ||
153 | |||
154 | private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap | ||
155 | private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap | ||
156 | |||
157 | private val Map<ConstantDeclaration, Object> constant2Value | ||
158 | private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value | ||
159 | private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value | ||
160 | |||
161 | private val int minInt | ||
162 | private val int maxInt | ||
163 | |||
164 | public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { | ||
165 | this.typeInterpretator = typeInterpretator | ||
166 | this.forwardMapper = forwardMapper | ||
167 | this.forwardTrace = trace | ||
168 | |||
169 | // Maps to trace language elements to the parsed problem. | ||
170 | val Map<String, Sig> name2AlloySig = new HashMap | ||
171 | val Map<String, Field> name2AlloyField = new HashMap | ||
172 | // exploring signatures | ||
173 | for(sig:solution.allReachableSigs) { | ||
174 | name2AlloySig.put(sig.label,sig) | ||
175 | for(field : sig.fields) { | ||
176 | name2AlloyField.put(field.label,field) | ||
177 | } | ||
178 | } | ||
179 | |||
180 | val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution.allAtoms) | ||
181 | this.typeInterpretator.resolveUnknownAtoms( | ||
182 | unknownAtoms, | ||
183 | solution, | ||
184 | forwardTrace, | ||
185 | name2AlloySig, | ||
186 | name2AlloyField, | ||
187 | alloyAtom2LogicElement, | ||
188 | interpretationOfUndefinedType) | ||
189 | |||
190 | // eval consants | ||
191 | constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[ | ||
192 | solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term | ||
193 | ] | ||
194 | // eval functions | ||
195 | val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function | | ||
196 | newHashMap( | ||
197 | solution.eval(function.name.lookup(name2AlloyField)) | ||
198 | .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])] | ||
199 | |||
200 | val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function | | ||
201 | val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField) | ||
202 | val paramIndexes = 1..(function.parameters.size) | ||
203 | return newHashMap( | ||
204 | solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t | | ||
205 | new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term]) | ||
206 | -> | ||
207 | t.atom(function.parameters.size + 1).atomLabel2Term | ||
208 | ])] | ||
209 | this.function2Value = Union(hostedfunction2Value,globalfunction2Value) | ||
210 | // eval relations | ||
211 | val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation | | ||
212 | solution.eval(relation.name.lookup(name2AlloyField)).map[ t | | ||
213 | new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet] | ||
214 | val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation | | ||
215 | solution.eval(relation.name.lookup(name2AlloyField)).map[ t | | ||
216 | new ParameterSubstitution((1..<t.arity).map[int a|t.atom(a).atomLabel2Term])].toSet] | ||
217 | this.relation2Value = Union(hostedRelation2Value,globalRelation2Value) | ||
218 | |||
219 | //Int limits | ||
220 | this.minInt = solution.min | ||
221 | this.maxInt = solution.max | ||
222 | |||
223 | //print(trace) | ||
224 | } | ||
225 | |||
226 | def List<ExprVar> collectUnknownAndResolveKnownAtoms(Iterable<ExprVar> allAtoms) { | ||
227 | val List<ExprVar> unknownAtoms = new LinkedList | ||
228 | |||
229 | for(atom: allAtoms) { | ||
230 | val typeName = getName(atom.type) | ||
231 | val atomName = atom.name | ||
232 | //println(atom.toString + " < - " + typeName) | ||
233 | if(typeName == forwardTrace.logicLanguage.name) { | ||
234 | this.logicLanguage = atom | ||
235 | } else if(typeName == "Int" || typeName == "seq/Int") { | ||
236 | // do nothing, integers will be parsed from the string | ||
237 | } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { | ||
238 | if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } | ||
239 | else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} | ||
240 | else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') | ||
241 | } | ||
242 | else unknownAtoms += atom | ||
243 | } | ||
244 | |||
245 | return unknownAtoms | ||
246 | } | ||
247 | |||
248 | def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) { | ||
249 | val name = type.toString | ||
250 | if(name.startsWith("{this/") && name.endsWith("}")) { | ||
251 | return type.toString.replaceFirst("\\{this\\/","").replace("}","") | ||
252 | } | ||
253 | else throw new IllegalArgumentException('''Unknown type format: "«name»"!''') | ||
254 | } | ||
255 | def private getName(ExprVar atom) { atom.toString.split("\\$") } | ||
256 | |||
257 | def print(Logic2AlloyLanguageMapperTrace trace) { | ||
258 | println('''Undefined-----''') | ||
259 | interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v.map[name]»''')] | ||
260 | //println('''Defined-----''') | ||
261 | //trace.type2ALSType.keySet.filter(TypeDefinition).forEach[println('''«it.name» -> «it.elements.map[name.join]»''')] | ||
262 | |||
263 | println('''Constants-----''') | ||
264 | constant2Value.forEach[k, v|println('''«k.name» : «v»''')] | ||
265 | println('''Functions-----''') | ||
266 | function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]] | ||
267 | println('''Relations-----''') | ||
268 | relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]] | ||
269 | } | ||
270 | |||
271 | override getElements(Type type) { getElementsDispatch(type) } | ||
272 | def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) } | ||
273 | def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } | ||
274 | |||
275 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | ||
276 | val transformedParams = new ParameterSubstitution(parameterSubstitution) | ||
277 | return transformedParams.lookup( | ||
278 | function.lookup(this.function2Value) | ||
279 | ) | ||
280 | } | ||
281 | |||
282 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | ||
283 | relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution)) | ||
284 | } | ||
285 | |||
286 | override getInterpretation(ConstantDeclaration constant) { | ||
287 | constant.lookup(this.constant2Value) | ||
288 | } | ||
289 | |||
290 | override getMinimalInteger() { this.minInt } | ||
291 | override getMaximalInteger() { this.maxInt } | ||
292 | |||
293 | // Alloy term -> logic term | ||
294 | def private atomLabel2Term(String label) { | ||
295 | if(label.number) return Integer.parseInt(label) | ||
296 | else if(label == this.logicBooleanTrue) return true | ||
297 | else if(label == this.logicBooleanFalse) return false | ||
298 | else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement) | ||
299 | else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''') | ||
300 | } | ||
301 | def private isNumber(String s) { | ||
302 | try{ | ||
303 | Integer.parseInt(s) | ||
304 | return true | ||
305 | }catch(NumberFormatException e) { | ||
306 | return false | ||
307 | } | ||
308 | } | ||
309 | } | ||
310 | |||
311 | /** | ||
312 | * Helper class for efficiently matching parameter substitutions for functions and relations. | ||
313 | */ | ||
314 | class ParameterSubstitution{ | ||
315 | val Object[] data; | ||
316 | |||
317 | new(Object[] data) { this.data = data } | ||
318 | |||
319 | override equals(Object obj) { | ||
320 | if(obj === this) return true | ||
321 | else if(obj == null) return false | ||
322 | if(obj instanceof ParameterSubstitution) { | ||
323 | return Arrays.equals(this.data,obj.data) | ||
324 | } | ||
325 | return false | ||
326 | } | ||
327 | |||
328 | override hashCode() { | ||
329 | Arrays.hashCode(data) | ||
330 | } | ||
331 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend new file mode 100644 index 00000000..23b9027f --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | |||
@@ -0,0 +1,467 @@ | |||
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.ALSEnumLiteral | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumericOperator | ||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
51 | import java.util.Collections | ||
52 | import java.util.HashMap | ||
53 | import java.util.List | ||
54 | import java.util.Map | ||
55 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
56 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
57 | import org.eclipse.xtend.lib.annotations.Accessors | ||
58 | |||
59 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
60 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation | ||
61 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | ||
62 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation | ||
63 | import java.util.Collection | ||
64 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | ||
65 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | ||
66 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct | ||
67 | |||
68 | class Logic2AlloyLanguageMapper { | ||
69 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
70 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
71 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | ||
72 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this) | ||
73 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this) | ||
74 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_RelationMapper relationMapper = new Logic2AlloyLanguageMapper_RelationMapper(this) | ||
75 | @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_Containment containmentMapper = new Logic2AlloyLanguageMapper_Containment(this) | ||
76 | |||
77 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | ||
78 | this.typeMapper = typeMapper | ||
79 | } | ||
80 | |||
81 | public def TracedOutput<ALSDocument,Logic2AlloyLanguageMapperTrace> transformProblem(LogicProblem problem, AlloySolverConfiguration config) { | ||
82 | val logicLanguage = createALSSignatureBody => [ | ||
83 | it.multiplicity = ALSMultiplicity.ONE | ||
84 | it.declarations += | ||
85 | createALSSignatureDeclaration => [ | ||
86 | it.name = support.toID(#["util", "language"]) ] | ||
87 | ] | ||
88 | |||
89 | val specification = createALSDocument=>[ | ||
90 | it.signatureBodies+=logicLanguage | ||
91 | ] | ||
92 | val trace = new Logic2AlloyLanguageMapperTrace => [ | ||
93 | it.specification = specification | ||
94 | it.logicLanguage = logicLanguage.declarations.head | ||
95 | it.logicLanguageBody = logicLanguage | ||
96 | |||
97 | it.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem)) | ||
98 | ] | ||
99 | |||
100 | typeMapper.transformTypes(problem.types,problem.elements,this,trace) | ||
101 | |||
102 | trace.constantDefinitions = problem.collectConstantDefinitions | ||
103 | trace.functionDefinitions = problem.collectFunctionDefinitions | ||
104 | trace.relationDefinitions = problem.collectRelationDefinitions | ||
105 | |||
106 | problem.constants.forEach[this.constantMapper.transformConstant(it,trace)] | ||
107 | problem.functions.forEach[this.functionMapper.transformFunction(it, trace)] | ||
108 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] | ||
109 | |||
110 | problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstantDefinitionSpecification(it,trace)] | ||
111 | problem.functions.filter(FunctionDefinition).forEach[this.functionMapper.transformFunctionDefinitionSpecification(it,trace)] | ||
112 | problem.relations.filter(RelationDefinition).forEach[this.relationMapper.transformRelationDefinitionSpecification(it,trace)] | ||
113 | |||
114 | val containment = problem.getContainmentHierarchies.head | ||
115 | if(containment !== null) { | ||
116 | this.containmentMapper.transformContainmentHierarchy(containment,trace) | ||
117 | } | ||
118 | |||
119 | //////////////////// | ||
120 | // Collect EMF-specific assertions | ||
121 | //////////////////// | ||
122 | val assertion2InverseRelation = problem.annotations.collectAnnotations(InverseRelationAssertion) | ||
123 | val assertion2UpperMultiplicityAssertion = problem.annotations.collectAnnotations(UpperMultiplicityAssertion) | ||
124 | val assertion2LowerMultiplicityAssertion = problem.annotations.collectAnnotations(LowerMultiplicityAssertion) | ||
125 | |||
126 | //////////////////// | ||
127 | // Transform Assertions | ||
128 | //////////////////// | ||
129 | for(assertion : problem.assertions) { | ||
130 | if(assertion2InverseRelation.containsKey(assertion)) { | ||
131 | transformInverseAssertion(assertion.lookup(assertion2InverseRelation),trace) | ||
132 | } else if(assertion2UpperMultiplicityAssertion.containsKey(assertion)) { | ||
133 | transformUpperMultiplicityAssertion(assertion.lookup(assertion2UpperMultiplicityAssertion),trace) | ||
134 | } else if(assertion2LowerMultiplicityAssertion.containsKey(assertion)) { | ||
135 | transformLowerMultiplicityAssertion(assertion.lookup(assertion2LowerMultiplicityAssertion),trace) | ||
136 | } else { | ||
137 | transformAssertion(assertion,trace) | ||
138 | } | ||
139 | } | ||
140 | |||
141 | transformRunCommand(specification, trace, config) | ||
142 | |||
143 | return new TracedOutput(specification,trace) | ||
144 | } | ||
145 | |||
146 | def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
147 | val a = assertion.inverseA | ||
148 | val b = assertion.inverseB | ||
149 | if(a instanceof RelationDeclaration && b instanceof RelationDeclaration && | ||
150 | !trace.relationDefinitions.containsKey(a) && !trace.relationDefinitions.containsKey(b)) | ||
151 | { | ||
152 | val fact = createALSFactDeclaration => [ | ||
153 | it.name = support.toID(assertion.target.name) | ||
154 | it.term = createALSEquals => [ | ||
155 | it.leftOperand = relationMapper.transformRelationReference(a as RelationDeclaration, trace) | ||
156 | it.rightOperand = createALSInverseRelation => [it.operand = relationMapper.transformRelationReference(b as RelationDeclaration, trace) ] | ||
157 | ] | ||
158 | ] | ||
159 | trace.specification.factDeclarations += fact | ||
160 | } else { | ||
161 | return transformAssertion(assertion.target,trace) | ||
162 | } | ||
163 | } | ||
164 | |||
165 | def transformUpperMultiplicityAssertion(UpperMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
166 | val x = assertion.relation | ||
167 | if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) { | ||
168 | val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) | ||
169 | val type = relation.type | ||
170 | |||
171 | if(type instanceof ALSDirectProduct) { | ||
172 | type.rightMultiplicit = type.rightMultiplicit.addUpper | ||
173 | } else { | ||
174 | relation.multiplicity = relation.multiplicity.addUpper | ||
175 | } | ||
176 | |||
177 | if(assertion.upper === 1) { | ||
178 | return true | ||
179 | } else { | ||
180 | return transformAssertion(assertion.target,trace) | ||
181 | } | ||
182 | |||
183 | } else { | ||
184 | return transformAssertion(assertion.target,trace) | ||
185 | } | ||
186 | } | ||
187 | |||
188 | def transformLowerMultiplicityAssertion(LowerMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
189 | val x = assertion.relation | ||
190 | if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) { | ||
191 | val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) | ||
192 | val type = relation.type | ||
193 | |||
194 | if(type instanceof ALSDirectProduct) { | ||
195 | type.rightMultiplicit = type.rightMultiplicit.addLower | ||
196 | } else { | ||
197 | relation.multiplicity = relation.multiplicity.addLower | ||
198 | } | ||
199 | |||
200 | if(assertion.lower === 1) { | ||
201 | return true | ||
202 | } else { | ||
203 | return transformAssertion(assertion.target,trace) | ||
204 | } | ||
205 | |||
206 | } else { | ||
207 | return transformAssertion(assertion.target,trace) | ||
208 | } | ||
209 | } | ||
210 | |||
211 | private def addLower(ALSMultiplicity multiplicity) { | ||
212 | if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { | ||
213 | return ALSMultiplicity::SOME | ||
214 | } else if(multiplicity === ALSMultiplicity::LONE) { | ||
215 | return ALSMultiplicity::ONE | ||
216 | } else { | ||
217 | throw new IllegalArgumentException('''Lower multiplicity is already set!''') | ||
218 | } | ||
219 | } | ||
220 | private def addUpper(ALSMultiplicity multiplicity) { | ||
221 | if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { | ||
222 | return ALSMultiplicity::LONE | ||
223 | } else if(multiplicity === ALSMultiplicity::SOME) { | ||
224 | return ALSMultiplicity::ONE | ||
225 | } else { | ||
226 | throw new IllegalArgumentException('''Upper multiplicity is already set!''') | ||
227 | } | ||
228 | } | ||
229 | |||
230 | private def <T extends AssertionAnnotation> collectAnnotations(Collection<? extends Annotation> collection, Class<T> annotationKind) { | ||
231 | val res = new HashMap | ||
232 | collection.filter(annotationKind).forEach[res.put(it.target,it)] | ||
233 | return res | ||
234 | } | ||
235 | |||
236 | private def collectConstantDefinitions(LogicProblem problem) { | ||
237 | val res = new HashMap | ||
238 | problem.constants.filter(ConstantDefinition).filter[it.defines!==null].forEach[ | ||
239 | res.put(it.defines,it) | ||
240 | ] | ||
241 | return res | ||
242 | } | ||
243 | private def collectFunctionDefinitions(LogicProblem problem) { | ||
244 | val res = new HashMap | ||
245 | problem.functions.filter(FunctionDefinition).filter[it.defines!==null].forEach[ | ||
246 | res.put(it.defines,it) | ||
247 | ] | ||
248 | return res | ||
249 | } | ||
250 | private def collectRelationDefinitions(LogicProblem problem) { | ||
251 | val res = new HashMap | ||
252 | problem.relations.filter(RelationDefinition).filter[it.defines!==null].forEach[ | ||
253 | res.put(it.defines,it) | ||
254 | ] | ||
255 | return res | ||
256 | } | ||
257 | |||
258 | //////////////////// | ||
259 | // Type References | ||
260 | //////////////////// | ||
261 | def dispatch protected ALSTerm transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyLanguageMapperTrace trace) { | ||
262 | return createALSReference => [ it.referred = support.getBooleanType(trace) ] | ||
263 | } | ||
264 | def dispatch protected ALSTerm transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt } | ||
265 | def dispatch protected ALSTerm transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyLanguageMapperTrace trace) {throw new UnsupportedOperationException('''Real types are not supported in Alloy.''')} | ||
266 | def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { | ||
267 | val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) | ||
268 | return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) | ||
269 | } | ||
270 | |||
271 | ////////////// | ||
272 | // Scopes | ||
273 | ////////////// | ||
274 | |||
275 | def transformRunCommand(ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) { | ||
276 | specification.runCommand = createALSRunCommand => [ | ||
277 | it.typeScopes+= createALSSigScope => [ | ||
278 | it.type= typeMapper.getUndefinedSupertype(trace) | ||
279 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | ||
280 | //it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements) | ||
281 | ] | ||
282 | if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( | ||
283 | '''An integer scope have to be specified for Alloy!''') | ||
284 | it.typeScopes += createALSIntScope => [ | ||
285 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxIntScope) | ||
286 | ] | ||
287 | // for(definedScope : config.typeScopes.allDefinedScope) { | ||
288 | // it.typeScopes += createALSSigScope => [ | ||
289 | // it.type = definedScope.type.lookup(trace.type2ALSType) | ||
290 | // it.number = definedScope.upperLimit | ||
291 | // it.exactly = (definedScope.upperLimit == definedScope.lowerLimit) | ||
292 | // ] | ||
293 | // } | ||
294 | ] | ||
295 | } | ||
296 | |||
297 | |||
298 | ////////////// | ||
299 | // Assertions + Terms | ||
300 | ////////////// | ||
301 | |||
302 | def protected transformAssertion(Assertion assertion, Logic2AlloyLanguageMapperTrace trace) { | ||
303 | val res = createALSFactDeclaration => [ | ||
304 | it.name = support.toID(assertion.name) | ||
305 | it.term = assertion.value.transformTerm(trace,Collections.EMPTY_MAP) | ||
306 | ] | ||
307 | trace.specification.factDeclarations += res | ||
308 | } | ||
309 | |||
310 | def dispatch protected ALSTerm transformTerm(BoolLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
311 | var ALSEnumLiteral ref; | ||
312 | if(literal.value==true) {ref = support.getBooleanTrue(trace)} | ||
313 | else {ref = support.getBooleanFalse(trace)} | ||
314 | val refFinal = ref | ||
315 | |||
316 | return support.booleanToLogicValue((createALSReference => [referred = refFinal]),trace) | ||
317 | } | ||
318 | def dispatch protected ALSTerm transformTerm(RealLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
319 | throw new UnsupportedOperationException("RealLiteral is not supported") | ||
320 | } | ||
321 | def dispatch protected ALSTerm transformTerm(IntLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
322 | if(literal.value>=0) { createALSNumberLiteral => [value = literal.value]} | ||
323 | else {createALSUnaryMinus => [it.operand = createALSNumberLiteral => [value = literal.value] ] } | ||
324 | } | ||
325 | |||
326 | def dispatch protected ALSTerm transformTerm(Not not, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
327 | createALSNot=>[operand = not.operand.transformTerm(trace,variables)] } | ||
328 | def dispatch protected ALSTerm transformTerm(And and, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
329 | support.unfoldAnd(and.operands.map[transformTerm(trace,variables)]) } | ||
330 | def dispatch protected ALSTerm transformTerm(Or or, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
331 | support.unfoldOr(or.operands.map[transformTerm(trace,variables)],trace) } | ||
332 | def dispatch protected ALSTerm transformTerm(Impl impl, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
333 | createALSImpl => [leftOperand = impl.leftOperand.transformTerm(trace,variables) rightOperand = impl.rightOperand.transformTerm(trace,variables)] } | ||
334 | def dispatch protected ALSTerm transformTerm(Iff iff, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
335 | createALSIff => [leftOperand = iff.leftOperand.transformTerm(trace,variables) rightOperand = iff.rightOperand.transformTerm(trace,variables)] } | ||
336 | def dispatch protected ALSTerm transformTerm(MoreThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
337 | createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } | ||
338 | def dispatch protected ALSTerm transformTerm(LessThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
339 | createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } | ||
340 | def dispatch protected ALSTerm transformTerm(MoreOrEqualThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
341 | createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } | ||
342 | def dispatch protected ALSTerm transformTerm(LessOrEqualThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
343 | createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } | ||
344 | def dispatch protected ALSTerm transformTerm(Equals equals, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
345 | createALSEquals => [leftOperand = equals.leftOperand.transformTerm(trace,variables) rightOperand = equals.rightOperand.transformTerm(trace,variables)] } | ||
346 | def dispatch protected ALSTerm transformTerm(Distinct distinct, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
347 | support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } | ||
348 | |||
349 | def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
350 | createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] } | ||
351 | def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
352 | createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] } | ||
353 | def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
354 | createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] } | ||
355 | def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
356 | createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] } | ||
357 | def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
358 | createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] } | ||
359 | |||
360 | def dispatch protected ALSTerm transformTerm(Forall forall, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
361 | support.createQuantifiedExpression(this,forall,ALSMultiplicity.ALL,trace,variables) } | ||
362 | def dispatch protected ALSTerm transformTerm(Exists exists, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
363 | support.createQuantifiedExpression(this,exists,ALSMultiplicity.SOME,trace,variables) } | ||
364 | |||
365 | def dispatch protected ALSTerm transformTerm(InstanceOf instanceOf, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
366 | return createALSSubset => [ | ||
367 | it.leftOperand = instanceOf.value.transformTerm(trace,variables) | ||
368 | it.rightOperand = instanceOf.range.transformTypeReference(trace) | ||
369 | ] | ||
370 | } | ||
371 | |||
372 | def dispatch protected ALSTerm transformTerm(SymbolicValue symbolicValue, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
373 | symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } | ||
374 | |||
375 | def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
376 | typeMapper.transformReference(referred,trace)} | ||
377 | def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
378 | if(trace.constantDefinitions.containsKey(constant)) { | ||
379 | return this.transformSymbolicReference(constant.lookup(trace.constantDefinitions),parameterSubstitutions,trace,variables) | ||
380 | } else { | ||
381 | val res = createALSJoin=> [ | ||
382 | leftOperand = createALSReference => [ referred = trace.logicLanguage ] | ||
383 | rightOperand = createALSReference => [ referred = constant.lookup(trace.constantDeclaration2LanguageField) ] | ||
384 | ] | ||
385 | return support.postprocessResultOfSymbolicReference(constant.type,res,trace) | ||
386 | } | ||
387 | } | ||
388 | def dispatch protected ALSTerm transformSymbolicReference(ConstantDefinition constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
389 | val res = createALSFunctionCall => [ | ||
390 | it.referredDefinition = constant.lookup(trace.constantDefinition2Function) | ||
391 | ] | ||
392 | return support.postprocessResultOfSymbolicReference(constant.type,res,trace) | ||
393 | } | ||
394 | def dispatch protected ALSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
395 | val res = createALSReference => [referred = variable.lookup(variables)] | ||
396 | return support.postprocessResultOfSymbolicReference(variable.range,res,trace) | ||
397 | } | ||
398 | def dispatch protected ALSTerm transformSymbolicReference(FunctionDeclaration function, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
399 | if(trace.functionDefinitions.containsKey(function)) { | ||
400 | return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) | ||
401 | } else { | ||
402 | if(functionMapper.transformedToHostedField(function,trace)) { | ||
403 | val param = parameterSubstitutions.get(0).transformTerm(trace,variables) | ||
404 | val res = createALSJoin => [ | ||
405 | leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace) | ||
406 | rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)] | ||
407 | ] | ||
408 | return support.postprocessResultOfSymbolicReference(function.range,res,trace) | ||
409 | } else { | ||
410 | val functionExpression = createALSJoin=>[ | ||
411 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
412 | rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)] | ||
413 | ] | ||
414 | val res = support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables) | ||
415 | return support.postprocessResultOfSymbolicReference(function.range,res,trace) | ||
416 | } | ||
417 | } | ||
418 | } | ||
419 | def dispatch protected ALSTerm transformSymbolicReference(FunctionDefinition function, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
420 | val result = createALSFunctionCall => [ | ||
421 | it.referredDefinition = function.lookup(trace.functionDefinition2Function) | ||
422 | it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] | ||
423 | ] | ||
424 | return support.postprocessResultOfSymbolicReference(function.range,result,trace) | ||
425 | } | ||
426 | |||
427 | def dispatch protected ALSTerm transformSymbolicReference(RelationDeclaration relation, List<Term> parameterSubstitutions, | ||
428 | Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
429 | if(trace.relationDefinitions.containsKey(relation)) { | ||
430 | this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),parameterSubstitutions,trace,variables) | ||
431 | } else { | ||
432 | if(relationMapper.transformToHostedField(relation,trace)) { | ||
433 | val alsRelation = relation.lookup(trace.relationDeclaration2Field) | ||
434 | // R(a,b) => | ||
435 | // b in a.R | ||
436 | return createALSSubset => [ | ||
437 | it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace,variables) | ||
438 | it.rightOperand = createALSJoin => [ | ||
439 | it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace,variables) | ||
440 | it.rightOperand = createALSReference => [ it.referred = alsRelation ] | ||
441 | ] | ||
442 | ] | ||
443 | } else { | ||
444 | val target = createALSJoin => [ | ||
445 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
446 | rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]] | ||
447 | val source = support.unfoldTermDirectProduct(this,parameterSubstitutions,trace,variables) | ||
448 | |||
449 | return createALSSubset => [ | ||
450 | leftOperand = source | ||
451 | rightOperand = target | ||
452 | ] | ||
453 | } | ||
454 | } | ||
455 | } | ||
456 | |||
457 | |||
458 | |||
459 | def dispatch protected ALSTerm transformSymbolicReference(RelationDefinition relation, List<Term> parameterSubstitutions, | ||
460 | Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) | ||
461 | { | ||
462 | return createALSFunctionCall => [ | ||
463 | it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) | ||
464 | it.params += parameterSubstitutions.map[p | p.transformTerm(trace,variables)] | ||
465 | ] | ||
466 | } | ||
467 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend new file mode 100644 index 00000000..22f49c98 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend | |||
@@ -0,0 +1,49 @@ | |||
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 | |||
21 | interface Logic2AlloyLanguageMapper_TypeMapperTrace {} | ||
22 | |||
23 | class Logic2AlloyLanguageMapperTrace { | ||
24 | public var ViatraQueryEngine incqueryEngine; | ||
25 | |||
26 | public var ALSDocument specification; | ||
27 | public var ALSSignatureDeclaration logicLanguage; | ||
28 | public var ALSSignatureBody logicLanguageBody; | ||
29 | public var ALSEnumDeclaration boolType; | ||
30 | public var ALSEnumLiteral boolTrue; | ||
31 | public var ALSEnumLiteral boolFalse; | ||
32 | |||
33 | public var Logic2AlloyLanguageMapper_TypeMapperTrace typeMapperTrace | ||
34 | |||
35 | public val Map<ConstantDeclaration, ALSFieldDeclaration> constantDeclaration2LanguageField = new HashMap | ||
36 | public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap | ||
37 | |||
38 | public val Map<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2HostedField = new HashMap | ||
39 | public val Map<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2LanguageField = new HashMap | ||
40 | public val Map<FunctionDefinition,ALSFunctionDefinition> functionDefinition2Function = new HashMap | ||
41 | |||
42 | public val Map<RelationDeclaration,ALSFieldDeclaration> relationDeclaration2Global = new HashMap | ||
43 | public val Map<RelationDeclaration, ALSFieldDeclaration> relationDeclaration2Field = new HashMap | ||
44 | public val Map<RelationDefinition,ALSRelationDefinition> relationDefinition2Predicate = new HashMap | ||
45 | |||
46 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | ||
47 | public var Map<FunctionDeclaration, FunctionDefinition> functionDefinitions | ||
48 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | ||
49 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend b/Solvers/Alloy-Solver/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..401c2ec2 --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend b/Solvers/Alloy-Solver/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..fd519c1e --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend b/Solvers/Alloy-Solver/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..ff18ef80 --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver/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..9dd4da2f --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend | |||
@@ -0,0 +1,111 @@ | |||
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 | |||
13 | class Logic2AlloyLanguageMapper_RelationMapper { | ||
14 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
15 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
16 | val Logic2AlloyLanguageMapper base; | ||
17 | public new(Logic2AlloyLanguageMapper base) { | ||
18 | this.base = base | ||
19 | } | ||
20 | |||
21 | def dispatch protected void transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
22 | if(!trace.relationDefinitions.containsKey(r)) { | ||
23 | if(r.transformToHostedField(trace)) { | ||
24 | transformRelationDeclarationToHostedField(r,trace) | ||
25 | } else { | ||
26 | transformRelationDeclarationToGlobalField(r,trace) | ||
27 | } | ||
28 | } | ||
29 | } | ||
30 | |||
31 | def protected transformToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
32 | val first = r.parameters.get(0) | ||
33 | if(r.parameters.size == 2) { | ||
34 | if(first instanceof ComplexTypeReference) { | ||
35 | val types = base.typeMapper.transformTypeReference(first.referred,base,trace) | ||
36 | if(types.size == 1) { | ||
37 | return true | ||
38 | } | ||
39 | } | ||
40 | } | ||
41 | return false | ||
42 | } | ||
43 | |||
44 | def protected transformRelationDeclarationToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
45 | val hostType = (r.parameters.head as ComplexTypeReference).referred | ||
46 | |||
47 | val targetBody = base.typeMapper.transformTypeReference(hostType,base,trace).get(0).eContainer as ALSSignatureBody | ||
48 | val field = createALSFieldDeclaration => [ | ||
49 | it.name = support.toID(r.getName) | ||
50 | it.multiplicity = ALSMultiplicity.SET | ||
51 | it.type = base.transformTypeReference(r.parameters.get(1),trace) | ||
52 | ] | ||
53 | targetBody.fields += field | ||
54 | trace.relationDeclaration2Field.put(r,field) | ||
55 | |||
56 | } | ||
57 | |||
58 | def protected transformRelationDeclarationToGlobalField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { | ||
59 | val field = createALSFieldDeclaration => [ | ||
60 | it.name = support.toID(r.name) | ||
61 | it.type = support.unfoldReferenceDirectProduct(base,r.parameters,trace) | ||
62 | ] | ||
63 | trace.logicLanguageBody.fields += field | ||
64 | trace.relationDeclaration2Global.put(r, field) | ||
65 | } | ||
66 | |||
67 | def dispatch protected void transformRelation(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { | ||
68 | val res = createALSRelationDefinition => [ | ||
69 | name = support.toID(r.name) | ||
70 | // fill the variables later | ||
71 | // fill the expression later | ||
72 | ] | ||
73 | |||
74 | trace.relationDefinition2Predicate.put(r,res) | ||
75 | trace.specification.relationDefinitions+=res; | ||
76 | } | ||
77 | |||
78 | def protected void transformRelationDefinitionSpecification(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { | ||
79 | val predicate = r.lookup(trace.relationDefinition2Predicate) | ||
80 | if(predicate !== null) { | ||
81 | val variableMap = new HashMap | ||
82 | for(variable : r.variables) { | ||
83 | val v = createALSVariableDeclaration => [ | ||
84 | it.name = support.toID(variable.name) | ||
85 | it.range = base.transformTypeReference(variable.range,trace) | ||
86 | ] | ||
87 | predicate.variables+=v | ||
88 | variableMap.put(variable,v) | ||
89 | } | ||
90 | predicate.value = base.transformTerm(r.value,trace,variableMap) | ||
91 | } | ||
92 | } | ||
93 | |||
94 | def public transformRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { | ||
95 | if(relation.transformToHostedField(trace)) { | ||
96 | return createALSReference => [it.referred = relation.lookup(trace.relationDeclaration2Field) ] | ||
97 | } else { | ||
98 | return createALSJoin => [ | ||
99 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
100 | rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]] | ||
101 | } | ||
102 | } | ||
103 | |||
104 | def public getRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { | ||
105 | if(relation.transformToHostedField(trace)) { | ||
106 | return relation.lookup(trace.relationDeclaration2Field) | ||
107 | } else { | ||
108 | return relation.lookup(trace.relationDeclaration2Global) | ||
109 | } | ||
110 | } | ||
111 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend b/Solvers/Alloy-Solver/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..39896c27 --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend b/Solvers/Alloy-Solver/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..9927f1cc --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend | |||
@@ -0,0 +1,16 @@ | |||
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 | } | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/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..ade9860b --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | |||
@@ -0,0 +1,268 @@ | |||
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 | import java.util.Map | ||
18 | |||
19 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
20 | |||
21 | class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
22 | implements Logic2AlloyLanguageMapper_TypeMapperTrace | ||
23 | { | ||
24 | public var ALSSignatureDeclaration objectSupperClass; | ||
25 | public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap; | ||
26 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap | ||
27 | } | ||
28 | /** | ||
29 | * Each object is an element of an Object set, and types are subsets of the objects. | ||
30 | */ | ||
31 | class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyLanguageMapper_TypeMapper{ | ||
32 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
33 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
34 | |||
35 | new() { | ||
36 | // Initialize package | ||
37 | LogicproblemPackage.eINSTANCE.class | ||
38 | } | ||
39 | |||
40 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
41 | val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
42 | trace.typeMapperTrace = typeTrace | ||
43 | |||
44 | // 1. A global type for Objects is created | ||
45 | val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])] | ||
46 | val objectBody = createALSSignatureBody => [ | ||
47 | it.declarations += objectSig | ||
48 | it.abstract = true | ||
49 | ] | ||
50 | typeTrace.objectSupperClass = objectSig | ||
51 | trace.specification.signatureBodies += objectBody | ||
52 | |||
53 | // 2. Each type is mapped to a unique sig | ||
54 | for(type : types) { | ||
55 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)] | ||
56 | val body = createALSSignatureBody => [it.declarations += sig] | ||
57 | trace.specification.signatureBodies += body | ||
58 | typeTrace.type2ALSType.put(type,sig) | ||
59 | } | ||
60 | |||
61 | // 3. The elements of a defined type is mapped to singleton signatures | ||
62 | // 3.1 Collect the elements | ||
63 | val elementMatcher = TypeQueries.instance.getLowestCommonSupertypeOfAllOccuranceOfElement(trace.incqueryEngine) | ||
64 | val topmostType2Elements = new HashMap<ALSSignatureDeclaration,List<DefinedElement>> | ||
65 | for(element : elements) { | ||
66 | val topmostTypes = elementMatcher.getAllValuesOftype(element) | ||
67 | var ALSSignatureDeclaration selectedTopmostType; | ||
68 | if(topmostTypes.empty) { | ||
69 | selectedTopmostType = objectSig | ||
70 | } else{ | ||
71 | selectedTopmostType = topmostTypes.head.lookup(typeTrace.type2ALSType) | ||
72 | } | ||
73 | topmostType2Elements.putOrAddToList(selectedTopmostType,element) | ||
74 | } | ||
75 | |||
76 | // 4. For each topmost types several singleton classes are generated, which represents the elements. | ||
77 | // For the sake of clarity, common bodies are used. | ||
78 | for(topmostEntry : topmostType2Elements.entrySet) { | ||
79 | |||
80 | for(element : topmostEntry.value) { | ||
81 | val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] | ||
82 | typeTrace.definedElement2Declaration.put(element,signature) | ||
83 | } | ||
84 | |||
85 | val body = createALSSignatureBody => [ | ||
86 | it.multiplicity = ALSMultiplicity.ONE | ||
87 | it.declarations += topmostEntry.value.map[it.lookup(typeTrace.definedElement2Declaration)] | ||
88 | ] | ||
89 | |||
90 | val containerLogicType = topmostEntry.key | ||
91 | body.superset += containerLogicType | ||
92 | |||
93 | trace.specification.signatureBodies+=body | ||
94 | } | ||
95 | |||
96 | // 5.1 Each Defined Type is specified as the union of its elements | ||
97 | for(definedType : types.filter(TypeDefinition)) { | ||
98 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
99 | it.name = support.toIDMultiple("typedefinition",definedType.name) | ||
100 | it.term = createALSEquals => [ | ||
101 | it.leftOperand = createALSReference => [ it.referred = definedType.lookup(typeTrace.type2ALSType) ] | ||
102 | it.rightOperand = support.unfoldPlus(definedType.elements.map[e| | ||
103 | createALSReference => [it.referred = e.lookup(typeTrace.definedElement2Declaration)]]) | ||
104 | ] | ||
105 | ] | ||
106 | } | ||
107 | // 5.2 Each Defined Element is unique | ||
108 | for(definedType : types.filter(TypeDefinition)) { | ||
109 | val allElementsIncludingSubtypes = | ||
110 | definedType.<Type>transitiveClosureStar[it.subtypes].filter(TypeDefinition) | ||
111 | .map[elements].flatten.toSet.toList | ||
112 | if(allElementsIncludingSubtypes.size>=2) { | ||
113 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
114 | it.name = support.toIDMultiple("typeElementsUnique",definedType.name) | ||
115 | it.term = unfoldDistinctElements(allElementsIncludingSubtypes,trace) | ||
116 | ] | ||
117 | } | ||
118 | } | ||
119 | |||
120 | // 6. Each inheritance is modeled by subset operator 'in' | ||
121 | for(type : types) { | ||
122 | val sigBody = type.lookup(typeTrace.type2ALSType).eContainer as ALSSignatureBody | ||
123 | if(type.supertypes.empty) { | ||
124 | sigBody.superset += typeTrace.objectSupperClass | ||
125 | } else { | ||
126 | sigBody.superset += type.supertypes.map[lookup(typeTrace.type2ALSType)] | ||
127 | } | ||
128 | } | ||
129 | |||
130 | |||
131 | // 7. Each type is in the intersection of the supertypes | ||
132 | for(type : types.filter[it.supertypes.size>=2]) { | ||
133 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
134 | it.name = support.toIDMultiple("abstract",type.name) | ||
135 | it.term = createALSEquals => [ | ||
136 | it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] | ||
137 | it.rightOperand = support.unfoldIntersection(type.supertypes.map[e| | ||
138 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
139 | ] | ||
140 | ] | ||
141 | } | ||
142 | |||
143 | // 8. Each abstract type is equal to the union of the subtypes | ||
144 | for(type : types.filter[isIsAbstract]) { | ||
145 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
146 | it.name = support.toIDMultiple("abstract",type.name) | ||
147 | it.term = createALSEquals => [ | ||
148 | it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] | ||
149 | it.rightOperand = support.unfoldPlus(type.subtypes.map[e| | ||
150 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
151 | ] | ||
152 | ] | ||
153 | } | ||
154 | // 8.1 The object type is the union of the root types. | ||
155 | val rootTypes = types.filter[it.supertypes.empty].toList | ||
156 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
157 | it.name = support.toIDMultiple(#["ObjectTypeDefinition"]) | ||
158 | it.term = createALSEquals => [ | ||
159 | it.leftOperand = createALSReference => [ it.referred = typeTrace.objectSupperClass ] | ||
160 | it.rightOperand = support.unfoldPlus(rootTypes.map[e| | ||
161 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
162 | ] | ||
163 | ] | ||
164 | |||
165 | // 9. For each type X (including Object) | ||
166 | // only the common subtypes are in the intersection | ||
167 | // of the two subtype. | ||
168 | // 9.1. for the object | ||
169 | { | ||
170 | val rootTypeList = types.filter[it.supertypes.empty].toList | ||
171 | for(type1Index: 0..<rootTypeList.size) { | ||
172 | for(type2Index: 0..<type1Index) { | ||
173 | trace.specification.factDeclarations += | ||
174 | commonSubtypeOnlyInDiamonds(rootTypeList.get(type1Index),rootTypeList.get(type2Index),trace) | ||
175 | } | ||
176 | } | ||
177 | } | ||
178 | |||
179 | //9.3 for the subtypes of each objects | ||
180 | { | ||
181 | for(inScope : types) { | ||
182 | val subtypeList = inScope.subtypes//.toList | ||
183 | if(subtypeList.size>=2) { | ||
184 | for(type1Index: 0..<subtypeList.size) { | ||
185 | for(type2Index: 0..<type1Index) { | ||
186 | trace.specification.factDeclarations += | ||
187 | commonSubtypeOnlyInDiamonds(subtypeList.get(type1Index),subtypeList.get(type2Index),trace) | ||
188 | } | ||
189 | } | ||
190 | } | ||
191 | } | ||
192 | } | ||
193 | } | ||
194 | |||
195 | private def isEnumlikeType(Type type) { | ||
196 | if(type instanceof TypeDefinition) { | ||
197 | val elements = type.elements | ||
198 | return elements.forall[it.definedInType.size === 1 && it.definedInType.head === type] | ||
199 | } | ||
200 | return false | ||
201 | } | ||
202 | |||
203 | private def isEnumlikeElement(DefinedElement d) { | ||
204 | d.definedInType.size === 1 && d.definedInType.head.isEnumlikeType | ||
205 | } | ||
206 | |||
207 | def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) { | ||
208 | val res = trace.typeMapperTrace | ||
209 | if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes) { | ||
210 | return res | ||
211 | } else { | ||
212 | throw new IllegalArgumentException(''' | ||
213 | Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name», | ||
214 | but found «res.class.name»''') | ||
215 | } | ||
216 | } | ||
217 | |||
218 | def private commonSubtypeOnlyInDiamonds(Type t1, Type t2, Logic2AlloyLanguageMapperTrace trace) { | ||
219 | val topmostCommonSubtypes = TypeQueries.instance.getTopmostCommonSubtypes(trace.incqueryEngine) | ||
220 | val allTopmostCommon = topmostCommonSubtypes.getAllValuesOfcommon(t1,t2).toList | ||
221 | return createALSFactDeclaration => [ | ||
222 | it.name = support.toIDMultiple("common","types",t1.name,t2.name) | ||
223 | it.term = createALSEquals => [ | ||
224 | it.leftOperand = createALSIntersection => [ | ||
225 | it.leftOperand = createALSReference => [it.referred = t1.lookup(trace.typeTrace.type2ALSType)] | ||
226 | it.rightOperand = createALSReference => [it.referred = t2.lookup(trace.typeTrace.type2ALSType)] | ||
227 | ] | ||
228 | it.rightOperand = support.unfoldPlus(allTopmostCommon.map[t|createALSReference => [it.referred = t.lookup(trace.typeTrace.type2ALSType)]]) | ||
229 | ] | ||
230 | ] | ||
231 | } | ||
232 | |||
233 | def private unfoldDistinctElements( | ||
234 | List<DefinedElement> operands, | ||
235 | Logic2AlloyLanguageMapperTrace trace | ||
236 | ) { | ||
237 | if(operands.size == 1 || operands.size == 0) {support.unfoldTrueStatement(trace);} | ||
238 | else { | ||
239 | val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2) | ||
240 | for(i:0..<operands.size) { | ||
241 | for(j: i+1..<operands.size) { | ||
242 | notEquals+=createALSNotEquals=>[ | ||
243 | leftOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(i)) ] | ||
244 | rightOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(j)) ] | ||
245 | ] | ||
246 | } | ||
247 | } | ||
248 | return support.unfoldAnd(notEquals) | ||
249 | } | ||
250 | } | ||
251 | |||
252 | override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
253 | return #[trace.typeTrace.type2ALSType.get(referred)] | ||
254 | } | ||
255 | |||
256 | override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { | ||
257 | trace.typeTrace.objectSupperClass | ||
258 | } | ||
259 | |||
260 | override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { | ||
261 | createALSReference => [it.referred = referred.lookup(trace.typeTrace.definedElement2Declaration)] | ||
262 | } | ||
263 | |||
264 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { | ||
265 | return undefinedScope + trace.typeTrace.definedElement2Declaration.size | ||
266 | } | ||
267 | |||
268 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old new file mode 100644 index 00000000..7383904d --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old | |||
@@ -0,0 +1,428 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSIntersection | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
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.logiclanguage.ComplexTypeReference | ||
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.TypeDeclaration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher | ||
15 | import java.util.HashMap | ||
16 | import java.util.LinkedHashSet | ||
17 | import java.util.LinkedList | ||
18 | import java.util.List | ||
19 | import java.util.Map | ||
20 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
21 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
22 | import org.eclipse.xtend.lib.annotations.Data | ||
23 | |||
24 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
25 | |||
26 | class Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal | ||
27 | implements Logic2AlloyLanguageMapper_TypeMapperTrace { | ||
28 | public var ALSSignatureDeclaration declaredSupertype | ||
29 | public var ALSSignatureDeclaration definedSupertype | ||
30 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap | ||
31 | |||
32 | public val Map<TypeDefinition, ALSSignatureDeclaration> definition2definition = new HashMap | ||
33 | public val Map<TypeDeclaration, ALSSignatureDeclaration> declaration2definition = new HashMap | ||
34 | public val Map<TypeDeclaration, ALSSignatureDeclaration> undefined2definition = new HashMap | ||
35 | public val Map<TypeDeclaration, ALSSignatureDeclaration> new2declaration = new HashMap | ||
36 | |||
37 | def getAllDefinedTypes() { | ||
38 | return (definition2definition.values) + | ||
39 | (declaration2definition.values) + | ||
40 | (undefined2definition.values) | ||
41 | } | ||
42 | def getAllDeclaredTypes() { | ||
43 | return new2declaration.values | ||
44 | } | ||
45 | |||
46 | public val Map<Type,List<ALSSignatureDeclaration>> type2AllSignatures = new HashMap; | ||
47 | } | ||
48 | |||
49 | @Data | ||
50 | class DynamicTypeConstraints { | ||
51 | List<List<Type>> positiveCNF | ||
52 | LinkedHashSet<Type> negative | ||
53 | public new() { | ||
54 | this.positiveCNF = new LinkedList | ||
55 | this.negative = new LinkedHashSet | ||
56 | } | ||
57 | def public void addPositiveTypeOptions(List<Type> typeDisjunction) { | ||
58 | this.positiveCNF.add(typeDisjunction) | ||
59 | } | ||
60 | def public void addNegativeTypes(Iterable<Type> negativeTypes) { | ||
61 | this.negative.addAll(negativeTypes) | ||
62 | } | ||
63 | } | ||
64 | |||
65 | /** | ||
66 | * Dynamic types are represented by disjoint sets, and | ||
67 | * static types are represented by the union of the dynamic type sets. | ||
68 | * | ||
69 | * Definition Declaration | ||
70 | * | / \ | ||
71 | * | W/DefinedSuper Wo/DefinedSuper | ||
72 | * | | / \ | ||
73 | * | | undefined2declaration new2declaration | ||
74 | * definition2definition definition2declaration | ||
75 | * +----------------------------------------------------+ +-------------+ | ||
76 | * Defined Declared | ||
77 | */ | ||
78 | class Logic2AlloyLanguageMapper_TypeMapper_Horizontal implements Logic2AlloyLanguageMapper_TypeMapper{ | ||
79 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
80 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
81 | |||
82 | override transformTypes(LogicProblem problem, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
83 | // 0. Creating the traces | ||
84 | val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal | ||
85 | trace.typeMapperTrace = typeTrace | ||
86 | /** | ||
87 | * Static type -> list of possible dynamic type map | ||
88 | */ | ||
89 | val typeToConcreteSubtypes = problem.typeToConcreteSubtypes(trace) | ||
90 | |||
91 | |||
92 | |||
93 | // 1. Transforming the types | ||
94 | |||
95 | // There are two kind of types: | ||
96 | // A: one with defined supertypes (including itself), that only has defined elements | ||
97 | // Those types can have instances only from the defined elements, ie they are subset of problem.elements | ||
98 | // B: one without defined supertypes | ||
99 | // Those types can have instances from two sources | ||
100 | // B.1 from elements that dont have definitions | ||
101 | // B.2 from newly created elements | ||
102 | val allConcreteTypes = problem.types.filter[!it.isAbstract] | ||
103 | val definitions = allConcreteTypes.filter(TypeDefinition).toList | ||
104 | val declarationsWithDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[it.hasDefinedSupertype].toList | ||
105 | val declarationsWithoutDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[!it.hasDefinedSupertype].toList | ||
106 | |||
107 | // 2. If there are defined elements | ||
108 | if(trace.typeTrace.definedSupertype != null) { | ||
109 | // 3 mapping the elements | ||
110 | problem.elements.transformDefinedSupertype(trace) | ||
111 | // 4. if there are elements that are added to types, then it have to be mapped to defined parts | ||
112 | if(problem.elements.exists[!it.definedInType.empty]) { | ||
113 | definitions.forEach[it.transformDefinition2Definition(trace)] | ||
114 | declarationsWithDefinedSupertype.forEach[it.transformDeclaration2Definition(trace)] | ||
115 | } | ||
116 | // 5. if there are elements that are not added to types, then it have to be mapped to declarations without definitions | ||
117 | if(problem.elements.exists[it.definedInType.empty]) { | ||
118 | declarationsWithoutDefinedSupertype.forEach[it.transformUndefined2Definition(trace)] | ||
119 | } | ||
120 | |||
121 | definedConcreteTypesAreFull(trace) | ||
122 | definedConcreteTypesAreDisjoint(trace) | ||
123 | problem.definedConcreteTypesAreSatisfyingDefinitions(typeToConcreteSubtypes,trace) | ||
124 | } | ||
125 | |||
126 | // Transforming the declared and defined concrete types | ||
127 | problem.elements.transformDefinedSupertype(trace) | ||
128 | if(trace.typeTrace.definedSupertype != null) { | ||
129 | problem.elements.transformDefinedElements(trace) | ||
130 | declarationsWithoutDefinedSupertype.forEach[it.transformNew2Declaration(trace)] | ||
131 | } | ||
132 | |||
133 | // 2: Caching the types by filling type2AllSignatures | ||
134 | for(typeToConcreteSubtypesEntry : typeToConcreteSubtypes.entrySet) { | ||
135 | val type = typeToConcreteSubtypesEntry.key | ||
136 | val List<ALSSignatureDeclaration> signatures = new LinkedList | ||
137 | |||
138 | } | ||
139 | } | ||
140 | |||
141 | def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) { | ||
142 | val res = trace.typeMapperTrace | ||
143 | if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal) { | ||
144 | return res | ||
145 | } else { | ||
146 | throw new IllegalArgumentException(''' | ||
147 | Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal.name», | ||
148 | but found «res.class.name»''') | ||
149 | } | ||
150 | } | ||
151 | |||
152 | private def boolean hasDefinedSupertype(Type type) { | ||
153 | if(type instanceof TypeDefinition) { | ||
154 | return true | ||
155 | } else { | ||
156 | if(type.supertypes.empty) return false | ||
157 | else return type.supertypes.exists[it.hasDefinedSupertype] | ||
158 | } | ||
159 | } | ||
160 | |||
161 | private def transformDefinedSupertype(List<DefinedElement> elements, Logic2AlloyLanguageMapperTrace trace) { | ||
162 | trace.typeTrace.definedSupertype = createALSSignatureDeclaration => [ | ||
163 | it.name = support.toID(#["util","defined","Object"]) | ||
164 | ] | ||
165 | trace.specification.signatureBodies += createALSSignatureBody => [ | ||
166 | it.abstract = true | ||
167 | it.declarations += trace.typeTrace.definedSupertype | ||
168 | ] | ||
169 | } | ||
170 | |||
171 | private def transformDefinedElements(List<DefinedElement> elements, | ||
172 | Logic2AlloyLanguageMapperTrace trace){ | ||
173 | if(trace.typeTrace.definedSupertype != null) { | ||
174 | // 2. Create elements as singleton signatures subtype of definedSupertype | ||
175 | val elementBodies = createALSSignatureBody => [ | ||
176 | it.multiplicity = ALSMultiplicity::ONE | ||
177 | it.supertype = trace.typeTrace.definedSupertype | ||
178 | ] | ||
179 | trace.specification.signatureBodies += elementBodies | ||
180 | for(element : elements) { | ||
181 | val elementDeclaration = createALSSignatureDeclaration => [ | ||
182 | it.name = support.toIDMultiple(#["element"],element.name) | ||
183 | ] | ||
184 | elementBodies.declarations += elementDeclaration | ||
185 | trace.typeTrace.definedElement2Declaration.put(element,elementDeclaration) | ||
186 | } | ||
187 | // 3. Specify that definedSupertype is equal to the union of specified | ||
188 | /*trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
189 | it.name = support.toID(#["util","typehierarchy","definitionOfElements"]) | ||
190 | it.term = createALSEquals => [ | ||
191 | it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype] | ||
192 | it.rightOperand = support.unfoldPlus(elements.map[element|createALSReference=>[ | ||
193 | it.referred = element.lookup(trace.typeTrace.definedElement2Declaration) | ||
194 | ]]) | ||
195 | ] | ||
196 | ]*/ | ||
197 | } | ||
198 | } | ||
199 | |||
200 | ///// Type definitions | ||
201 | |||
202 | protected def void transformDefinition2Definition(TypeDefinition type, Logic2AlloyLanguageMapperTrace trace) { | ||
203 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["definition2definition"],type.name)] | ||
204 | val body = createALSSignatureBody => [ | ||
205 | it.declarations += sig | ||
206 | it.superset += trace.typeTrace.definedSupertype | ||
207 | ] | ||
208 | trace.specification.signatureBodies += body | ||
209 | trace.typeTrace.definition2definition.put(type,sig) | ||
210 | } | ||
211 | protected def void transformDeclaration2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) { | ||
212 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaration2definition"],type.name)] | ||
213 | val body = createALSSignatureBody => [ | ||
214 | it.declarations += sig | ||
215 | it.superset += trace.typeTrace.definedSupertype | ||
216 | ] | ||
217 | trace.specification.signatureBodies += body | ||
218 | trace.typeTrace.declaration2definition.put(type,sig) | ||
219 | } | ||
220 | protected def void transformUndefined2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) { | ||
221 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["undefined2definition"],type.name)] | ||
222 | val body = createALSSignatureBody => [ | ||
223 | it.declarations += sig | ||
224 | it.supertype = trace.typeTrace.definedSupertype | ||
225 | ] | ||
226 | trace.specification.signatureBodies += body | ||
227 | trace.typeTrace.undefined2definition.put(type,sig) | ||
228 | } | ||
229 | protected def void transformNew2Declaration(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) { | ||
230 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaredPartOfDeclaration"],type.name)] | ||
231 | val body = createALSSignatureBody => [ | ||
232 | it.declarations += sig | ||
233 | it.supertype = trace.typeTrace.declaredSupertype | ||
234 | ] | ||
235 | trace.specification.signatureBodies += body | ||
236 | trace.typeTrace.new2declaration.put(type,sig) | ||
237 | } | ||
238 | |||
239 | /** | ||
240 | * The dynamic types cover each concrete types | ||
241 | */ | ||
242 | protected def definedConcreteTypesAreFull(Logic2AlloyLanguageMapperTrace trace) { | ||
243 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
244 | it.name = support.toID(#["util","typehierarchy","elementFull"]) | ||
245 | it.term = createALSEquals => [ | ||
246 | it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype] | ||
247 | it.rightOperand = support.unfoldPlus( | ||
248 | trace.typeTrace.allDefinedTypes.map[type| | ||
249 | createALSReference=>[referred = type] | ||
250 | ].toList | ||
251 | ) | ||
252 | ] | ||
253 | ] | ||
254 | |||
255 | } | ||
256 | /** | ||
257 | * The dynamic types are disjoint | ||
258 | */ | ||
259 | protected def definedConcreteTypesAreDisjoint(Logic2AlloyLanguageMapperTrace trace) { | ||
260 | val types = trace.getTypeTrace.allDefinedTypes.toList | ||
261 | if (types.size >= 2) { | ||
262 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
263 | it.name = support.toID(#["util", "typehierarchy", "elementFull"]) | ||
264 | it.term = types.disjointSets | ||
265 | ] | ||
266 | } | ||
267 | } | ||
268 | /** | ||
269 | * The dynamic types are subtypes of the types where it is defined, but not subtypes where it is not | ||
270 | */ | ||
271 | protected def definedConcreteTypesAreSatisfyingDefinitions(LogicProblem problem, Map<Type,List<Type>> typeToConcreteSubtypes, Logic2AlloyLanguageMapperTrace trace) { | ||
272 | val constraintOnElements = problem.elements.typeConstraints(typeToConcreteSubtypes) | ||
273 | for(constraintOnElement : constraintOnElements.entrySet) { | ||
274 | val element = constraintOnElement.key | ||
275 | val elementSignature = element.lookup(trace.typeTrace.definedElement2Declaration) | ||
276 | val constraint = constraintOnElement.value | ||
277 | |||
278 | var ALSTerm negativeConstraints; | ||
279 | if(constraint.negative.isEmpty) { | ||
280 | negativeConstraints = null | ||
281 | } else { | ||
282 | negativeConstraints = support.unfoldAnd(constraint.negative.map[type| | ||
283 | createALSNot=> [ elementInDefinedType(elementSignature, type, trace) ] | ||
284 | ].toList) | ||
285 | } | ||
286 | |||
287 | var ALSTerm positiveTypeConstraints | ||
288 | if(constraint.positiveCNF.isEmpty) { | ||
289 | positiveTypeConstraints = null | ||
290 | } else { | ||
291 | positiveTypeConstraints = support.unfoldAnd(constraint.positiveCNF.map[ typeConstraintFromDefinition | | ||
292 | support.unfoldOr(typeConstraintFromDefinition.map[type | | ||
293 | elementInDefinedType(elementSignature,type,trace) | ||
294 | ].toList,trace) | ||
295 | ]) | ||
296 | } | ||
297 | |||
298 | var ALSTerm typeConstraint | ||
299 | if(negativeConstraints != null && positiveTypeConstraints == null) { | ||
300 | typeConstraint = negativeConstraints | ||
301 | } else if (negativeConstraints == null && positiveTypeConstraints != null) { | ||
302 | typeConstraint = positiveTypeConstraints | ||
303 | } else if (negativeConstraints != null && positiveTypeConstraints != null) { | ||
304 | val and = createALSAnd | ||
305 | and.leftOperand = positiveTypeConstraints | ||
306 | and.rightOperand = negativeConstraints | ||
307 | typeConstraint = and | ||
308 | } else { | ||
309 | typeConstraint = null | ||
310 | } | ||
311 | |||
312 | if(typeConstraint != null) { | ||
313 | val fact = createALSFactDeclaration => [ | ||
314 | name = support.toIDMultiple(#["util","typehierarchy","definition"],element.name) | ||
315 | ] | ||
316 | fact.term = typeConstraint | ||
317 | trace.specification.factDeclarations +=fact | ||
318 | } | ||
319 | // otherwise there is no type constraint on element | ||
320 | } | ||
321 | } | ||
322 | |||
323 | private def elementInDefinedType( | ||
324 | ALSSignatureDeclaration elementSignature, | ||
325 | Type type, | ||
326 | Logic2AlloyLanguageMapperTrace trace) | ||
327 | { | ||
328 | var ALSSignatureDeclaration signature | ||
329 | if(type instanceof TypeDeclaration) { | ||
330 | if(trace.typeTrace.declaration2definition.containsKey(type)) { | ||
331 | signature = type.lookup(trace.typeTrace.declaration2definition) | ||
332 | } else if(trace.typeTrace.undefined2definition.containsKey(type)) { | ||
333 | signature = type.lookup(trace.typeTrace.undefined2definition) | ||
334 | } else { | ||
335 | return null | ||
336 | } | ||
337 | } else if(type instanceof TypeDefinition) { | ||
338 | if(trace.typeTrace.definition2definition.containsKey(type)) { | ||
339 | signature = type.lookup(trace.typeTrace.definition2definition) | ||
340 | } else { | ||
341 | return null | ||
342 | } | ||
343 | } else throw new IllegalArgumentException('''Unknownt type «type.class.name»''') | ||
344 | |||
345 | val finalSignature = signature | ||
346 | return createALSSubset => [ | ||
347 | leftOperand = createALSReference => [ | ||
348 | referred = elementSignature | ||
349 | ] | ||
350 | rightOperand = createALSReference => [ | ||
351 | referred = finalSignature | ||
352 | ] | ||
353 | ] | ||
354 | } | ||
355 | |||
356 | def private typeToConcreteSubtypes(LogicProblem problem, Logic2AlloyLanguageMapperTrace trace) { | ||
357 | if(trace.incqueryEngine == null) { | ||
358 | trace.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem)) | ||
359 | } | ||
360 | val matcher = SupertypeStarMatcher.on(trace.incqueryEngine) | ||
361 | val Map<Type,List<Type>> typeToConcreteSubtypes = new HashMap | ||
362 | for(supertype : problem.types) { | ||
363 | typeToConcreteSubtypes.put( | ||
364 | supertype, | ||
365 | matcher.getAllValuesOfsubtype(supertype) | ||
366 | .filter[!it.isIsAbstract].toList) | ||
367 | } | ||
368 | return typeToConcreteSubtypes | ||
369 | } | ||
370 | |||
371 | /** | ||
372 | * Gives type constraints in a form of CNF | ||
373 | */ | ||
374 | def private Map<DefinedElement,DynamicTypeConstraints> typeConstraints(List<DefinedElement> elements, Map<Type,List<Type>> typeToConcreteSubtypes) { | ||
375 | val Map<DefinedElement,DynamicTypeConstraints> constraints = new HashMap | ||
376 | elements.forEach[constraints.put(it,new DynamicTypeConstraints)] | ||
377 | |||
378 | for(type : typeToConcreteSubtypes.keySet.filter(TypeDefinition)) { | ||
379 | val subtypes = type.lookup(typeToConcreteSubtypes) | ||
380 | for(elementInType:type.elements) { | ||
381 | elementInType.lookup(constraints).addPositiveTypeOptions(subtypes) | ||
382 | } | ||
383 | for(elementNotInType:elements.filter[!type.elements.contains(it)]) { | ||
384 | elementNotInType.lookup(constraints).addNegativeTypes(subtypes) | ||
385 | } | ||
386 | } | ||
387 | |||
388 | return constraints | ||
389 | } | ||
390 | |||
391 | private def ALSTerm disjointSets(List<ALSSignatureDeclaration> signatures) { | ||
392 | if(signatures.size >= 2){ | ||
393 | val top = createALSEquals => [ | ||
394 | it.leftOperand = signatures.intersectionOfTypes | ||
395 | it.rightOperand = createALSNone | ||
396 | ] | ||
397 | if(signatures.size > 2) { | ||
398 | return createALSAnd => [ | ||
399 | it.leftOperand = top | ||
400 | it.rightOperand = signatures.subList(1,signatures.size).disjointSets | ||
401 | ] | ||
402 | } else{ | ||
403 | return top | ||
404 | } | ||
405 | } else { | ||
406 | throw new UnsupportedOperationException() | ||
407 | } | ||
408 | } | ||
409 | |||
410 | private def ALSIntersection intersectionOfTypes(List<ALSSignatureDeclaration> signatures) { | ||
411 | if(signatures.size == 2) { | ||
412 | return createALSIntersection => [ | ||
413 | leftOperand = createALSReference => [it.referred = signatures.get(0)] | ||
414 | rightOperand = createALSReference => [it.referred = signatures.get(1)] | ||
415 | ] | ||
416 | } else if(signatures.size > 2) { | ||
417 | return createALSIntersection => [ | ||
418 | leftOperand = createALSReference => [it.referred = signatures.get(0)] | ||
419 | rightOperand = signatures.subList(1,signatures.size).intersectionOfTypes | ||
420 | ] | ||
421 | } else throw new UnsupportedOperationException() | ||
422 | } | ||
423 | |||
424 | |||
425 | override transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
426 | //trace.typeTrace. | ||
427 | } | ||
428 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/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..6533ad36 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend | |||
@@ -0,0 +1,50 @@ | |||
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 hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
9 | import java.util.HashMap | ||
10 | import java.util.Map | ||
11 | import java.util.Collection | ||
12 | |||
13 | class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace { | ||
14 | val Map<TypeDeclaration,ALSSignatureDeclaration> newElementTypes = new HashMap | ||
15 | val Map<Type,ALSSignatureDeclaration> definedElementTypes = new HashMap | ||
16 | var ALSSignatureDeclaration undefinedSupertype | ||
17 | var ALSSignatureDeclaration definedSupertype | ||
18 | } | ||
19 | |||
20 | class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{ | ||
21 | |||
22 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
23 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
24 | } | ||
25 | |||
26 | private def boolean hasDefinedSupertype(Type type) { | ||
27 | if(type instanceof TypeDefinition) { | ||
28 | return true | ||
29 | } else { | ||
30 | if(type.supertypes.empty) return false | ||
31 | else return type.supertypes.exists[it.hasDefinedSupertype] | ||
32 | } | ||
33 | } | ||
34 | |||
35 | override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
36 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
37 | } | ||
38 | |||
39 | override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { | ||
40 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
41 | } | ||
42 | |||
43 | override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { | ||
44 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
45 | } | ||
46 | |||
47 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { | ||
48 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
49 | } | ||
50 | } \ No newline at end of file | ||