aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-25 04:15:39 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-25 04:15:39 -0400
commit25a4b1b53add70e268c3083682f8a3508c618ec2 (patch)
tree6d46e62be49cfe6c5640e2e9af80aae90da6a212 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder
parentmid-measurement push (diff)
downloadVIATRA-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/inf/dlsreasoner/alloy/reasoner/builder')
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend20
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend23
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend63
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend11
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend13
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend2
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend44
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend207
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 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder 1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2 2
3import com.google.common.util.concurrent.SimpleTimeLimiter
4import com.google.common.util.concurrent.UncheckedTimeoutException
5import edu.mit.csail.sdg.alloy4.A4Reporter 3import edu.mit.csail.sdg.alloy4.A4Reporter
6import edu.mit.csail.sdg.alloy4.Err 4import edu.mit.csail.sdg.alloy4.Err
7import edu.mit.csail.sdg.alloy4.ErrorWarning 5import edu.mit.csail.sdg.alloy4.ErrorWarning
@@ -23,7 +21,11 @@ import java.util.LinkedList
23import java.util.List 21import java.util.List
24import java.util.Map 22import java.util.Map
25import java.util.concurrent.Callable 23import java.util.concurrent.Callable
24import java.util.concurrent.ExecutionException
25import java.util.concurrent.ExecutorService
26import java.util.concurrent.Executors
26import java.util.concurrent.TimeUnit 27import java.util.concurrent.TimeUnit
28import java.util.concurrent.TimeoutException
27import org.eclipse.xtend.lib.annotations.Data 29import org.eclipse.xtend.lib.annotations.Data
28 30
29class AlloySolverException extends Exception{ 31class 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 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder 1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2 2
3import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar 3import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
4import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
5import java.util.Map
6import edu.mit.csail.sdg.alloy4compiler.ast.Sig 4import edu.mit.csail.sdg.alloy4compiler.ast.Sig
7import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field 5import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
6import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration 9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
10import java.util.ArrayList
10import java.util.List 11import java.util.List
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory 12import java.util.Map
13
14import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
12 15
13class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{ 16class 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 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
5import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
6
7interface 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
12class 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
3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration 3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument 4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
5import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt 5import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt
6import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral
7import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand
8import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString
6import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm 9import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
7import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory 10import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
8import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration 11import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
10import java.util.LinkedList
11import java.util.List 12import java.util.List
12 13
13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
14
15class RunCommandMapper { 14class 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
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-08-17 22:18:57 +0000