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/dlsreasoner/alloy/reasoner/builder | |
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/dlsreasoner/alloy/reasoner/builder')
2 files changed, 44 insertions, 26 deletions
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) |