diff options
author | 2018-02-24 18:30:13 -0500 | |
---|---|---|
committer | 2018-02-24 18:30:13 -0500 | |
commit | f0f92fa2c4a6f61d5deea376f7f971e0c40238f5 (patch) | |
tree | fdb366741dd69fd9ad5325476682b6db905ef0df /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf | |
parent | Working injector for linking viatra and emf execution time. (diff) | |
download | VIATRA-Generator-f0f92fa2c4a6f61d5deea376f7f971e0c40238f5.tar.gz VIATRA-Generator-f0f92fa2c4a6f61d5deea376f7f971e0c40238f5.tar.zst VIATRA-Generator-f0f92fa2c4a6f61d5deea376f7f971e0c40238f5.zip |
Documentation level for Alloy
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf')
4 files changed, 53 insertions, 36 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend index 992479da..89328610 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend | |||
@@ -3,14 +3,9 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
4 | 4 | ||
5 | class AlloySolverConfiguration extends LogicSolverConfiguration { | 5 | class AlloySolverConfiguration extends LogicSolverConfiguration { |
6 | /*public var boolean createCommonSupertype | ||
7 | public var int intScope = 1 // 5 by default | ||
8 | public def setIntScopeFor(int max) { | ||
9 | intScope = 31 - Integer.numberOfLeadingZeros(max) + 1 | ||
10 | }*/ | ||
11 | public var int symmetry = 20 // by default | 6 | public var int symmetry = 20 // by default |
12 | public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J | 7 | public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J |
13 | public var boolean writeToFile = false | 8 | public var TypeMappingTechnique typeMapping = TypeMappingTechnique.InheritanceAndHorizontal |
14 | public var randomise = 0 | 9 | public var randomise = 0 |
15 | } | 10 | } |
16 | 11 | ||
@@ -29,5 +24,5 @@ enum AlloyBackendSolver { | |||
29 | } | 24 | } |
30 | 25 | ||
31 | enum TypeMappingTechnique { | 26 | enum TypeMappingTechnique { |
32 | FilteredTypes | 27 | FilteredTypes, InheritanceAndHorizontal |
33 | } \ No newline at end of file | 28 | } \ 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/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend index a29af455..9c2d7bf1 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | |||
@@ -9,6 +9,7 @@ import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapp | |||
9 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes | 9 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes |
10 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated | 10 | import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated |
11 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage | 11 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
@@ -32,6 +33,9 @@ class AlloySolver extends LogicReasoner{ | |||
32 | 33 | ||
33 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | 34 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { |
34 | val alloyConfig = configuration.asConfig | 35 | val alloyConfig = configuration.asConfig |
36 | val writeToFile = ( | ||
37 | configuration.documentationLevel===DocumentationLevel::NORMAL || | ||
38 | configuration.documentationLevel===DocumentationLevel::FULL) | ||
35 | 39 | ||
36 | // Start: Logic -> Alloy mapping | 40 | // Start: Logic -> Alloy mapping |
37 | val transformationStart = System.currentTimeMillis | 41 | val transformationStart = System.currentTimeMillis |
@@ -41,7 +45,7 @@ class AlloySolver extends LogicReasoner{ | |||
41 | 45 | ||
42 | var String fileURI = null; | 46 | var String fileURI = null; |
43 | var String alloyCode = null; | 47 | var String alloyCode = null; |
44 | if(alloyConfig.writeToFile) { | 48 | if(writeToFile) { |
45 | fileURI = workspace.writeModel(alloyProblem,fileName).toFileString | 49 | fileURI = workspace.writeModel(alloyProblem,fileName).toFileString |
46 | } else { | 50 | } else { |
47 | alloyCode = workspace.writeModelToString(alloyProblem,fileName) | 51 | alloyCode = workspace.writeModelToString(alloyProblem,fileName) |
@@ -57,7 +61,7 @@ class AlloySolver extends LogicReasoner{ | |||
57 | val solverFinish = System.currentTimeMillis-solverStart | 61 | val solverFinish = System.currentTimeMillis-solverStart |
58 | // Finish: Solving Alloy problem | 62 | // Finish: Solving Alloy problem |
59 | 63 | ||
60 | if(alloyConfig.writeToFile) workspace.deactivateModel(fileName) | 64 | if(writeToFile) workspace.deactivateModel(fileName) |
61 | 65 | ||
62 | return logicResult | 66 | return logicResult |
63 | } | 67 | } |
@@ -66,7 +70,7 @@ class AlloySolver extends LogicReasoner{ | |||
66 | if(configuration instanceof AlloySolverConfiguration) { | 70 | if(configuration instanceof AlloySolverConfiguration) { |
67 | return configuration | 71 | return configuration |
68 | } else { | 72 | } else { |
69 | throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''') | 73 | throw new IllegalArgumentException('''The configuration has to be an «AlloySolverConfiguration.simpleName»!''') |
70 | } | 74 | } |
71 | } | 75 | } |
72 | 76 | ||
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 c1f2ec4c..b78165dc 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,5 +1,7 @@ | |||
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 | ||
3 | import edu.mit.csail.sdg.alloy4.A4Reporter | 5 | import edu.mit.csail.sdg.alloy4.A4Reporter |
4 | import edu.mit.csail.sdg.alloy4.Err | 6 | import edu.mit.csail.sdg.alloy4.Err |
5 | import edu.mit.csail.sdg.alloy4.ErrorWarning | 7 | import edu.mit.csail.sdg.alloy4.ErrorWarning |
@@ -7,25 +9,24 @@ import edu.mit.csail.sdg.alloy4compiler.ast.Command | |||
7 | import edu.mit.csail.sdg.alloy4compiler.parser.CompModule | 9 | import edu.mit.csail.sdg.alloy4compiler.parser.CompModule |
8 | import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil | 10 | import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil |
9 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Options | 11 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Options |
12 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver | ||
10 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | 13 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution |
11 | import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod | 14 | import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod |
15 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | ||
16 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
17 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
12 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 19 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
20 | import java.util.ArrayList | ||
21 | import java.util.HashMap | ||
13 | import java.util.LinkedList | 22 | import java.util.LinkedList |
14 | import java.util.List | 23 | 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 | 24 | 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 | import com.google.common.util.concurrent.SimpleTimeLimiter | ||
25 | import java.util.concurrent.Callable | 25 | import java.util.concurrent.Callable |
26 | import java.util.concurrent.TimeUnit | 26 | import java.util.concurrent.TimeUnit |
27 | import com.google.common.util.concurrent.UncheckedTimeoutException | 27 | import org.eclipse.emf.common.CommonPlugin |
28 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 28 | import org.eclipse.xtend.lib.annotations.Data |
29 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
29 | 30 | ||
30 | class AlloySolverException extends Exception{ | 31 | class AlloySolverException extends Exception{ |
31 | new(String s) { super(s) } | 32 | new(String s) { super(s) } |
@@ -48,6 +49,10 @@ class AlloyHandler { | |||
48 | //val fileName = "problem.als" | 49 | //val fileName = "problem.als" |
49 | 50 | ||
50 | public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, String alloyCode) { | 51 | public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, String alloyCode) { |
52 | val writeToFile = ( | ||
53 | configuration.documentationLevel===DocumentationLevel::NORMAL || | ||
54 | configuration.documentationLevel===DocumentationLevel::FULL) | ||
55 | |||
51 | //Prepare | 56 | //Prepare |
52 | 57 | ||
53 | val warnings = new LinkedList<String> | 58 | val warnings = new LinkedList<String> |
@@ -78,7 +83,7 @@ class AlloyHandler { | |||
78 | // Start: Alloy -> Kodkod | 83 | // Start: Alloy -> Kodkod |
79 | val kodkodTransformStart = System.currentTimeMillis(); | 84 | val kodkodTransformStart = System.currentTimeMillis(); |
80 | try { | 85 | try { |
81 | if(configuration.writeToFile) { | 86 | if(writeToFile) { |
82 | compModule = CompUtil.parseEverything_fromFile(reporter,null,path) | 87 | compModule = CompUtil.parseEverything_fromFile(reporter,null,path) |
83 | } else { | 88 | } else { |
84 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) | 89 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) |
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 5c16f406..4ecebb62 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 | |||
@@ -65,6 +65,7 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope | |||
65 | import org.eclipse.xtend.lib.annotations.Accessors | 65 | import org.eclipse.xtend.lib.annotations.Accessors |
66 | 66 | ||
67 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 67 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
68 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt | ||
68 | 69 | ||
69 | class Logic2AlloyLanguageMapper { | 70 | class Logic2AlloyLanguageMapper { |
70 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 71 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
@@ -311,22 +312,34 @@ class Logic2AlloyLanguageMapper { | |||
311 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | 312 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) |
312 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | 313 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) |
313 | ] | 314 | ] |
314 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( | 315 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { |
315 | '''An integer scope have to be specified for Alloy!''') | 316 | val integersUsed = specification.eAllContents.filter(ALSInt) |
316 | it.typeScopes += createALSIntScope => [ | 317 | if(integersUsed.empty) { |
317 | if(config.typeScopes.knownIntegers.empty) { | 318 | // If no integer scope is defined, but the problem has no integers |
318 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | 319 | // => scope can be empty |
320 | it.typeScopes+= createALSIntScope => [ | ||
321 | it.number = 0 | ||
322 | ] | ||
319 | } else { | 323 | } else { |
320 | var scope = Math.max( | 324 | // If no integer scope is defined, and the problem has integers |
321 | Math.abs(config.typeScopes.knownIntegers.max), | 325 | // => error |
322 | Math.abs(config.typeScopes.knownIntegers.min)) | 326 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') |
323 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
324 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
325 | } | ||
326 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope) | ||
327 | } | 327 | } |
328 | 328 | } else { | |
329 | ] | 329 | it.typeScopes += createALSIntScope => [ |
330 | if(config.typeScopes.knownIntegers.empty) { | ||
331 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | ||
332 | } else { | ||
333 | var scope = Math.max( | ||
334 | Math.abs(config.typeScopes.knownIntegers.max), | ||
335 | Math.abs(config.typeScopes.knownIntegers.min)) | ||
336 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
337 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
338 | } | ||
339 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope) | ||
340 | } | ||
341 | ] | ||
342 | } | ||
330 | // for(definedScope : config.typeScopes.allDefinedScope) { | 343 | // for(definedScope : config.typeScopes.allDefinedScope) { |
331 | // it.typeScopes += createALSSigScope => [ | 344 | // it.typeScopes += createALSSigScope => [ |
332 | // it.type = definedScope.type.lookup(trace.type2ALSType) | 345 | // it.type = definedScope.type.lookup(trace.type2ALSType) |