diff options
author | 2019-10-25 04:15:39 -0400 | |
---|---|---|
committer | 2019-10-25 04:15:39 -0400 | |
commit | 25a4b1b53add70e268c3083682f8a3508c618ec2 (patch) | |
tree | 6d46e62be49cfe6c5640e2e9af80aae90da6a212 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit | |
parent | mid-measurement push (diff) | |
download | VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.gz VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.zst VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.zip |
VAMPIRE: post-submission push
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit')
8 files changed, 292 insertions, 91 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 index 2efd6b29..59ec2ae4 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | |||
@@ -9,15 +9,15 @@ class Alloy2LogicMapper { | |||
9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { | 9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { |
10 | val models = monitoredAlloySolution.aswers.map[it.key].toList | 10 | val models = monitoredAlloySolution.aswers.map[it.key].toList |
11 | 11 | ||
12 | if(!monitoredAlloySolution.finishedBeforeTimeout) { | 12 | // if(!monitoredAlloySolution.finishedBeforeTimeout) { |
13 | return createInsuficientResourcesResult => [ | 13 | // return createInsuficientResourcesResult => [ |
14 | it.problem = problem | 14 | // it.problem = problem |
15 | it.representation += models | 15 | // it.representation += models |
16 | it.trace = trace | 16 | // it.trace = trace |
17 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | 17 | // it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) |
18 | ] | 18 | // ] |
19 | } else { | 19 | // } else { |
20 | if(models.last.satisfiable || requiredNumberOfSolution == -1) { | 20 | if((!models.isEmpty && models.last.satisfiable) || requiredNumberOfSolution == -1) { |
21 | return createModelResult => [ | 21 | return createModelResult => [ |
22 | it.problem = problem | 22 | it.problem = problem |
23 | it.representation += models | 23 | it.representation += models |
@@ -32,7 +32,7 @@ class Alloy2LogicMapper { | |||
32 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | 32 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) |
33 | ] | 33 | ] |
34 | } | 34 | } |
35 | } | 35 | // } |
36 | } | 36 | } |
37 | 37 | ||
38 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { | 38 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend index ebbca624..9b4265b9 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | |||
@@ -1,7 +1,5 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | 1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder |
2 | 2 | ||
3 | import com.google.common.util.concurrent.SimpleTimeLimiter | ||
4 | import com.google.common.util.concurrent.UncheckedTimeoutException | ||
5 | import edu.mit.csail.sdg.alloy4.A4Reporter | 3 | import edu.mit.csail.sdg.alloy4.A4Reporter |
6 | import edu.mit.csail.sdg.alloy4.Err | 4 | import edu.mit.csail.sdg.alloy4.Err |
7 | import edu.mit.csail.sdg.alloy4.ErrorWarning | 5 | import edu.mit.csail.sdg.alloy4.ErrorWarning |
@@ -23,7 +21,11 @@ import java.util.LinkedList | |||
23 | import java.util.List | 21 | import java.util.List |
24 | import java.util.Map | 22 | import java.util.Map |
25 | import java.util.concurrent.Callable | 23 | import java.util.concurrent.Callable |
24 | import java.util.concurrent.ExecutionException | ||
25 | import java.util.concurrent.ExecutorService | ||
26 | import java.util.concurrent.Executors | ||
26 | import java.util.concurrent.TimeUnit | 27 | import java.util.concurrent.TimeUnit |
28 | import java.util.concurrent.TimeoutException | ||
27 | import org.eclipse.xtend.lib.annotations.Data | 29 | import org.eclipse.xtend.lib.annotations.Data |
28 | 30 | ||
29 | class AlloySolverException extends Exception{ | 31 | class AlloySolverException extends Exception{ |
@@ -46,7 +48,7 @@ class AlloyHandler { | |||
46 | 48 | ||
47 | //val fileName = "problem.als" | 49 | //val fileName = "problem.als" |
48 | 50 | ||
49 | public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { | 51 | def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { |
50 | 52 | ||
51 | //Prepare | 53 | //Prepare |
52 | val warnings = new LinkedList<String> | 54 | val warnings = new LinkedList<String> |
@@ -87,7 +89,6 @@ class AlloyHandler { | |||
87 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | 89 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart |
88 | // Finish: Alloy -> Kodkod | 90 | // Finish: Alloy -> Kodkod |
89 | 91 | ||
90 | val limiter = new SimpleTimeLimiter | ||
91 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) | 92 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) |
92 | var List<Pair<A4Solution, Long>> answers | 93 | var List<Pair<A4Solution, Long>> answers |
93 | var boolean finished | 94 | var boolean finished |
@@ -95,10 +96,20 @@ class AlloyHandler { | |||
95 | answers = callable.call | 96 | answers = callable.call |
96 | finished = true | 97 | finished = true |
97 | } else { | 98 | } else { |
99 | val ExecutorService executor = Executors.newCachedThreadPool(); | ||
100 | val future = executor.submit(callable) | ||
98 | try{ | 101 | try{ |
99 | answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) | 102 | answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS) |
100 | finished = true | 103 | finished = true |
101 | } catch (UncheckedTimeoutException e) { | 104 | } catch (TimeoutException ex) { |
105 | // handle the timeout | ||
106 | } catch (InterruptedException e) { | ||
107 | // handle the interrupts | ||
108 | } catch (ExecutionException e) { | ||
109 | // handle other exceptions | ||
110 | } finally { | ||
111 | future.cancel(true); | ||
112 | |||
102 | answers = callable.partialAnswers | 113 | answers = callable.partialAnswers |
103 | finished = false | 114 | finished = false |
104 | } | 115 | } |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend index 8019c6b5..ac75b2a1 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend | |||
@@ -1,20 +1,73 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | 1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder |
2 | 2 | ||
3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar | 3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar |
4 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
5 | import java.util.Map | ||
6 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | 4 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig |
7 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | 5 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field |
6 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
10 | import java.util.ArrayList | ||
10 | import java.util.List | 11 | import java.util.List |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | 12 | import java.util.Map |
13 | |||
14 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
12 | 15 | ||
13 | class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{ | 16 | class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{ |
14 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | 17 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE |
15 | 18 | ||
16 | override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, A4Solution solution, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String, Sig> name2AlloySig, Map<String, Field> name2AlloyField, Map<String, DefinedElement> expression2DefinedElement, Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) { | 19 | override resolveUnknownAtoms( |
17 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 20 | Iterable<ExprVar> objectAtoms, |
21 | A4Solution solution, | ||
22 | Logic2AlloyLanguageMapperTrace forwardTrace, | ||
23 | Map<String, Sig> name2AlloySig, | ||
24 | Map<String, Field> name2AlloyField, | ||
25 | Map<String,DefinedElement> expression2DefinedElement, | ||
26 | Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) | ||
27 | { | ||
28 | /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap() | ||
29 | val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/ | ||
30 | |||
31 | val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal | ||
32 | |||
33 | // 1. Evaluate the defined elements | ||
34 | for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) { | ||
35 | val name = definedElementMappingEntry.value.name | ||
36 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
37 | val elementsOfSingletonSignature = solution.eval(matchingSig) | ||
38 | if(elementsOfSingletonSignature.size != 1) { | ||
39 | throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''') | ||
40 | } else { | ||
41 | val expressionOfDefinedElement = elementsOfSingletonSignature.head.atom(0)// as ExprVar | ||
42 | expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key) | ||
43 | } | ||
44 | } | ||
45 | |||
46 | // 2. evaluate the signatures and create new elements if necessary | ||
47 | for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) { | ||
48 | val type = type2SingatureEntry.key | ||
49 | if(type instanceof TypeDeclaration) { | ||
50 | val name = type2SingatureEntry.value.name | ||
51 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
52 | val elementsOfSignature = solution.eval(matchingSig) | ||
53 | val elementList = new ArrayList(elementsOfSignature.size) | ||
54 | var newVariableIndex = 1; | ||
55 | for(elementOfSignature : elementsOfSignature) { | ||
56 | val expressionOfDefinedElement = elementOfSignature.atom(0) | ||
57 | if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) { | ||
58 | elementList += expressionOfDefinedElement.lookup(expression2DefinedElement) | ||
59 | } else { | ||
60 | val newElementName = '''newObject «newVariableIndex.toString»''' | ||
61 | val newRepresentation = createDefinedElement => [ | ||
62 | it.name = newElementName | ||
63 | ] | ||
64 | elementList += newRepresentation | ||
65 | expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation) | ||
66 | } | ||
67 | } | ||
68 | interpretationOfUndefinedType.put(type,elementList) | ||
69 | } | ||
70 | } | ||
18 | } | 71 | } |
19 | 72 | ||
20 | } \ No newline at end of file | 73 | } \ 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 index 3fc3971d..e1ffe531 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | |||
@@ -194,13 +194,12 @@ class Logic2AlloyLanguageMapper { | |||
194 | val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) | 194 | val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) |
195 | val type = relation.type | 195 | val type = relation.type |
196 | 196 | ||
197 | if(type instanceof ALSDirectProduct) { | ||
198 | type.rightMultiplicit = type.rightMultiplicit.addUpper | ||
199 | } else { | ||
200 | relation.multiplicity = relation.multiplicity.addUpper | ||
201 | } | ||
202 | |||
203 | if(assertion.upper === 1) { | 197 | if(assertion.upper === 1) { |
198 | if(type instanceof ALSDirectProduct) { | ||
199 | type.rightMultiplicit = type.rightMultiplicit.addUpper | ||
200 | } else { | ||
201 | relation.multiplicity = relation.multiplicity.addUpper | ||
202 | } | ||
204 | return true | 203 | return true |
205 | } else { | 204 | } else { |
206 | return transformAssertion(assertion.target,trace) | 205 | return transformAssertion(assertion.target,trace) |
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 index 0762efce..8de9688b 100644 --- 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 | |||
@@ -133,11 +133,11 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
133 | public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { | 133 | public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { |
134 | if(relation.parameters.size === 2) { | 134 | if(relation.parameters.size === 2) { |
135 | /** 1. Create a relation that can be used in ^relation expressions */ | 135 | /** 1. Create a relation that can be used in ^relation expressions */ |
136 | val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace) | 136 | val declaration = this.createRelationDeclaration(support.toID('''AsDeclaration «relation.name»'''),relation.parameters,trace) |
137 | trace.relationInTransitiveToHosterField.put(relation,declaration) | 137 | trace.relationInTransitiveToHosterField.put(relation,declaration) |
138 | /** 2. Add fact that the declaration corresponds to the definition */ | 138 | /** 2. Add fact that the declaration corresponds to the definition */ |
139 | val fact = createALSFactDeclaration => [ | 139 | val fact = createALSFactDeclaration => [ |
140 | it.name = '''EqualsAsDeclaration «relation.name»''' | 140 | it.name = support.toID('''EqualsAsDeclaration «relation.name»''') |
141 | it.term = createALSQuantifiedEx => [ | 141 | it.term = createALSQuantifiedEx => [ |
142 | val a = createALSVariableDeclaration => [ | 142 | val a = createALSVariableDeclaration => [ |
143 | it.name = "a" | 143 | it.name = "a" |
@@ -157,7 +157,7 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
157 | it.params += createALSReference => [ it.referred = b ] | 157 | it.params += createALSReference => [ it.referred = b ] |
158 | ] | 158 | ] |
159 | it.rightOperand = createALSSubset => [ | 159 | it.rightOperand = createALSSubset => [ |
160 | it.leftOperand = createALSJoin => [ | 160 | it.leftOperand = createALSDirectProduct => [ |
161 | it.leftOperand = createALSReference => [ referred = a ] | 161 | it.leftOperand = createALSReference => [ referred = a ] |
162 | it.rightOperand = createALSReference => [ referred = b ] | 162 | it.rightOperand = createALSReference => [ referred = b ] |
163 | ] | 163 | ] |
@@ -183,12 +183,15 @@ class Logic2AlloyLanguageMapper_RelationMapper { | |||
183 | rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] | 183 | rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] |
184 | ] | 184 | ] |
185 | } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ | 185 | } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ |
186 | createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] | 186 | createALSJoin => [ |
187 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
188 | rightOperand = createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] | ||
189 | ] | ||
187 | } else { | 190 | } else { |
188 | throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') | 191 | throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') |
189 | } | 192 | } |
190 | return createALSSubset => [ | 193 | return createALSSubset => [ |
191 | it.leftOperand = createALSJoin => [ | 194 | it.leftOperand = createALSDirectProduct => [ |
192 | it.leftOperand = source | 195 | it.leftOperand = source |
193 | it.rightOperand = target | 196 | it.rightOperand = target |
194 | ] | 197 | ] |
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 index 397fb84b..2d79e364 100644 --- 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 | |||
@@ -254,7 +254,7 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL | |||
254 | } | 254 | } |
255 | 255 | ||
256 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { | 256 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { |
257 | return undefinedScope + trace.typeTrace.definedElement2Declaration.size | 257 | if(undefinedScope == Integer.MAX_VALUE) return undefinedScope else return undefinedScope + trace.typeTrace.definedElement2Declaration.size |
258 | } | 258 | } |
259 | 259 | ||
260 | override getTypeInterpreter() { | 260 | override getTypeInterpreter() { |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend new file mode 100644 index 00000000..98d769bf --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend | |||
@@ -0,0 +1,44 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
6 | |||
7 | interface Logic2AlloyLanguageMapper_TypeScopeMapping { | ||
8 | def void addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) | ||
9 | def void addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) | ||
10 | } | ||
11 | |||
12 | class Logic2AlloyLanguageMapper_AsConstraint implements Logic2AlloyLanguageMapper_TypeScopeMapping { | ||
13 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
14 | val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
15 | val Logic2AlloyLanguageMapper_TypeMapper typeMapper | ||
16 | |||
17 | new(Logic2AlloyLanguageMapper_TypeMapper mapper) { | ||
18 | this.typeMapper = mapper | ||
19 | } | ||
20 | |||
21 | override addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
22 | document.factDeclarations += createALSFactDeclaration => [ | ||
23 | it.name = support.toID(#["LowerMultiplicity",support.toID(type.name),lowerMultiplicty.toString]) | ||
24 | it.term = createALSLeq => [ | ||
25 | it.leftOperand = createALSCardinality => [ | ||
26 | it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
27 | ] | ||
28 | it.rightOperand = createALSNumberLiteral => [it.value = lowerMultiplicty] | ||
29 | ] | ||
30 | ] | ||
31 | } | ||
32 | |||
33 | override addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
34 | document.factDeclarations += createALSFactDeclaration => [ | ||
35 | it.name = support.toID(#["UpperMultiplicity",support.toID(type.name),upperMultiplicty.toString]) | ||
36 | it.term = createALSMeq => [ | ||
37 | it.leftOperand = createALSCardinality => [ | ||
38 | it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
39 | ] | ||
40 | it.rightOperand = createALSNumberLiteral => [it.value = upperMultiplicty] | ||
41 | ] | ||
42 | ] | ||
43 | } | ||
44 | } \ 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/RunCommandMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend index 3e96f7f4..494197bc 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend | |||
@@ -3,25 +3,26 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration |
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | 4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument |
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt | 5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt |
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand | ||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | 9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm |
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | 10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
10 | import java.util.LinkedList | ||
11 | import java.util.List | 12 | import java.util.List |
12 | 13 | ||
13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
14 | |||
15 | class RunCommandMapper { | 14 | class RunCommandMapper { |
16 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 15 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
17 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | 16 | val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; |
18 | private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | 17 | val Logic2AlloyLanguageMapper_TypeMapper typeMapper; |
18 | val Logic2AlloyLanguageMapper_TypeScopeMapping typeScopeMapping; | ||
19 | 19 | ||
20 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | 20 | new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { |
21 | this.typeMapper = typeMapper | 21 | this.typeMapper = typeMapper |
22 | this.typeScopeMapping = new Logic2AlloyLanguageMapper_AsConstraint(typeMapper) | ||
22 | } | 23 | } |
23 | 24 | ||
24 | def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) | 25 | def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) |
25 | { | 26 | { |
26 | //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size | 27 | //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size |
27 | 28 | ||
@@ -36,28 +37,47 @@ class RunCommandMapper { | |||
36 | it.term = support.unfoldAnd(equals) | 37 | it.term = support.unfoldAnd(equals) |
37 | ] | 38 | ] |
38 | } | 39 | } |
39 | val typeScopes = new LinkedList | 40 | |
40 | for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) { | 41 | /* |
41 | val key = definedScope.key | 42 | val upperLimits = new LinkedList |
42 | val amount = definedScope.value | 43 | val lowerLimits = new LinkedList |
43 | val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount | 44 | |
44 | 45 | /*val typesWithScopeConstraint = config.typeScopes.maxNewElementsByType.keySet + config.typeScopes.minNewElementsByType.keySet | |
45 | val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet | 46 | for(type : typesWithScopeConstraint) { |
46 | if(amount == 0 && exactly) { | 47 | val max = if(config.typeScopes.maxNewElementsByType.containsKey(type)) { |
47 | specification.factDeclarations += createALSFactDeclaration => [ | 48 | config.typeScopes.maxNewElementsByType.get(type) |
48 | it.term = createALSEquals => [ | 49 | } else { |
49 | it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | 50 | LogicSolverConfiguration::Unlimited |
50 | it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) | 51 | } |
51 | ] | 52 | val min = if(config.typeScopes.minNewElementsByType.containsKey(type)) { |
53 | config.typeScopes.minNewElementsByType.get(type) | ||
54 | } else { | ||
55 | 0 | ||
56 | } | ||
57 | |||
58 | val exactly = min === max | ||
59 | |||
60 | if(max === 0) { | ||
61 | val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet | ||
62 | specification.factDeclarations += createALSFactDeclaration => [ | ||
63 | it.term = createALSEquals => [ | ||
64 | it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
65 | it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) | ||
52 | ] | 66 | ] |
53 | } | 67 | ] |
54 | val int n = existing.size-amount | 68 | } else if(max !== LogicSolverConfiguration::Unlimited) { |
55 | typeScopes += createALSSigScope => [ | 69 | upperLimits += createALSSigScope => [ |
56 | it.type = typeMapper.transformTypeReference(key,mapper,trace).head | 70 | it.type = typeMapper.transformTypeReference(type,mapper,trace).head |
57 | it.number = n | 71 | it.number = max |
58 | it.exactly =exactly | 72 | it.exactly =exactly |
59 | ] | 73 | ] |
74 | } else { | ||
75 | // do nothing | ||
60 | } | 76 | } |
77 | if(min != 0 && ! exactly) { | ||
78 | lowerLimits += type->min | ||
79 | } | ||
80 | }*/ | ||
61 | 81 | ||
62 | specification.runCommand = createALSRunCommand => [ | 82 | specification.runCommand = createALSRunCommand => [ |
63 | it.typeScopes+= createALSSigScope => [ | 83 | it.typeScopes+= createALSSigScope => [ |
@@ -65,41 +85,112 @@ class RunCommandMapper { | |||
65 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | 85 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) |
66 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | 86 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) |
67 | ] | 87 | ] |
68 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | 88 | |
69 | val integersUsed = specification.eAllContents.filter(ALSInt) | 89 | ] |
70 | if(integersUsed.empty) { | 90 | |
71 | // If no integer scope is defined, but the problem has no integers | 91 | for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) { |
72 | // => scope can be empty | 92 | val limit = upperLimit.value |
73 | it.typeScopes+= createALSIntScope => [ | 93 | if(limit != LogicSolverConfiguration::Unlimited) { |
74 | it.number = 0 | 94 | this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace) |
75 | ] | ||
76 | } else { | ||
77 | // If no integer scope is defined, and the problem has integers | ||
78 | // => error | ||
79 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') | ||
80 | } | ||
81 | } else { | ||
82 | it.typeScopes += createALSIntScope => [ | ||
83 | if(config.typeScopes.knownIntegers.empty) { | ||
84 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | ||
85 | } else { | ||
86 | var scope = Math.max( | ||
87 | Math.abs(config.typeScopes.knownIntegers.max), | ||
88 | Math.abs(config.typeScopes.knownIntegers.min)) | ||
89 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
90 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
91 | } | ||
92 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 | ||
93 | } | ||
94 | ] | ||
95 | } | 95 | } |
96 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | 96 | } |
97 | throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') | 97 | |
98 | for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) { | ||
99 | val limit = lowerLimit.value | ||
100 | if(limit != 0) { | ||
101 | this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace) | ||
102 | } | ||
103 | } | ||
104 | |||
105 | setIntegerScope(specification,config,specification.runCommand) | ||
106 | setStringScope(specification,config,specification.runCommand) | ||
107 | } | ||
108 | |||
109 | protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { | ||
110 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | ||
111 | throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') | ||
112 | } else { | ||
113 | if(config.typeScopes.maxNewStrings == 0) { | ||
114 | it.typeScopes += createALSStringScope => [it.number = 0] | ||
98 | } else { | 115 | } else { |
99 | if(config.typeScopes.maxNewStrings != 0) { | 116 | if(specification.eAllContents.filter(ALSString).empty) { |
100 | it.typeScopes += createALSStringScope => [it.number = 0] | 117 | it.typeScopes += createALSStringScope => [it.number = 0] |
118 | } else { | ||
119 | throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') | ||
101 | } | 120 | } |
102 | } | 121 | } |
103 | ] | 122 | } |
123 | } | ||
124 | |||
125 | protected def setIntegerScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand command) { | ||
126 | //AlloySolverConfiguration config, ALSRunCommand it | ||
127 | |||
128 | // If the scope is unlimited ... | ||
129 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | ||
130 | val integersUsed = specification.eAllContents.filter(ALSInt) | ||
131 | if(integersUsed.empty) { | ||
132 | // ... but the problem has no integers => scope can be empty | ||
133 | command.typeScopes+= createALSIntScope => [ it.number = 0 ] | ||
134 | } else { | ||
135 | // If no integer scope is defined, and the problem has integers => error | ||
136 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') | ||
137 | } | ||
138 | } else { | ||
139 | // If the scope is limited, collect the integers in the problem and the scope,... | ||
140 | //val maxIntScope = config.typeScopes.maxNewIntegers | ||
141 | //val minIntScope = config.typeScopes.minNewIntegers | ||
142 | val knownIntegers = config.typeScopes.knownIntegers | ||
143 | val minKnownInteger = if(knownIntegers.empty) { Integer.MAX_VALUE } else { knownIntegers.min } | ||
144 | val maxKnownInteger = if(knownIntegers.empty) { Integer.MIN_VALUE } else { knownIntegers.max } | ||
145 | val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value].toList | ||
146 | val minIntegerInProblem = if(integersInProblem.empty) { Integer.MAX_VALUE } else { integersInProblem.min } | ||
147 | val maxIntegerInProblem = if(integersInProblem.empty) { Integer.MIN_VALUE } else { integersInProblem.max } | ||
148 | // And select the range of integers | ||
149 | val min = #[minKnownInteger,minIntegerInProblem].min | ||
150 | val max = #[maxKnownInteger,maxIntegerInProblem].max | ||
151 | //val abs = Math.max(Math.abs(min),Math.abs(max)) | ||
152 | |||
153 | |||
154 | command.typeScopes += createALSIntScope => [ | ||
155 | it.number = toBits(min, max) | ||
156 | ] | ||
157 | } | ||
158 | |||
159 | // if(config.typeScopes.knownIntegers.empty) { | ||
160 | // return Integer.SIZE-Integer.numberOfLeadingZeros((config.typeScopes.maxNewIntegers+1)/2) | ||
161 | // } else { | ||
162 | // var scope = Math.max( | ||
163 | // Math.abs(config.typeScopes.knownIntegers.max), | ||
164 | // Math.abs(config.typeScopes.knownIntegers.min)) | ||
165 | // if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
166 | // scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
167 | // } | ||
168 | // return Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 | ||
169 | // } | ||
170 | } | ||
171 | |||
172 | private static def toBits(int min, int max) { | ||
173 | // 4 Int = {-8, ..., 7} | ||
174 | // x Int = {- (2^(x-1)) , ... , 2^(x-1)-1} | ||
175 | var int bits = 1 | ||
176 | // range = 2^(x-1) | ||
177 | var int range = 1 | ||
178 | while((!(-range <= min)) || (!(max <= range-1))) { | ||
179 | bits++ | ||
180 | range*=2 | ||
181 | } | ||
182 | return bits | ||
104 | } | 183 | } |
184 | // | ||
185 | // def static void main(String[] args) { | ||
186 | // println('''0,0->«toBits(0,0)»''') | ||
187 | // println('''1,1->«toBits(1,1)»''') | ||
188 | // println('''-1,-1->«toBits(-1,-1)»''') | ||
189 | // println('''5,6->«toBits(5,6)»''') | ||
190 | // println('''0,6->«toBits(0,6)»''') | ||
191 | // println('''-10,0->«toBits(-10,0)»''') | ||
192 | // println('''-8,7->«toBits(-8,7)»''') | ||
193 | // println('''-100,100->«toBits(-100,100)»''') | ||
194 | // println('''-300,300->«toBits(-300,300)»''') | ||
195 | // } | ||
105 | } \ No newline at end of file | 196 | } \ No newline at end of file |