diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner')
3 files changed, 57 insertions, 11 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/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 3379ba20..fb094bc5 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 index a270cb73..378c9553 100644 --- 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 | |||
@@ -1,3 +1,4 @@ | |||
1 | <<<<<<< HEAD | ||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | 2 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder |
2 | 3 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
@@ -41,4 +42,49 @@ class Logic2AlloyLanguageMapper_AsConstraint implements Logic2AlloyLanguageMappe | |||
41 | ] | 42 | ] |
42 | ] | 43 | ] |
43 | } | 44 | } |
45 | ======= | ||
46 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
47 | |||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
49 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
50 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
51 | |||
52 | interface Logic2AlloyLanguageMapper_TypeScopeMapping { | ||
53 | def void addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) | ||
54 | def void addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) | ||
55 | } | ||
56 | |||
57 | class Logic2AlloyLanguageMapper_AsConstraint implements Logic2AlloyLanguageMapper_TypeScopeMapping { | ||
58 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
59 | val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
60 | val Logic2AlloyLanguageMapper_TypeMapper typeMapper | ||
61 | |||
62 | new(Logic2AlloyLanguageMapper_TypeMapper mapper) { | ||
63 | this.typeMapper = mapper | ||
64 | } | ||
65 | |||
66 | override addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
67 | document.factDeclarations += createALSFactDeclaration => [ | ||
68 | it.name = support.toID(#["LowerMultiplicity",support.toID(type.name),lowerMultiplicty.toString]) | ||
69 | it.term = createALSLeq => [ | ||
70 | it.leftOperand = createALSCardinality => [ | ||
71 | it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
72 | ] | ||
73 | it.rightOperand = createALSNumberLiteral => [it.value = lowerMultiplicty] | ||
74 | ] | ||
75 | ] | ||
76 | } | ||
77 | |||
78 | override addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
79 | document.factDeclarations += createALSFactDeclaration => [ | ||
80 | it.name = support.toID(#["UpperMultiplicity",support.toID(type.name),upperMultiplicty.toString]) | ||
81 | it.term = createALSMeq => [ | ||
82 | it.leftOperand = createALSCardinality => [ | ||
83 | it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) | ||
84 | ] | ||
85 | it.rightOperand = createALSNumberLiteral => [it.value = upperMultiplicty] | ||
86 | ] | ||
87 | ] | ||
88 | } | ||
89 | >>>>>>> 25a4b1b5... VAMPIRE: post-submission push | ||
44 | } \ No newline at end of file | 90 | } \ No newline at end of file |