diff options
author | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-02-24 18:30:13 -0500 |
---|---|---|
committer | OszkarSemerath <oszkar.semerath@gmail.com> | 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/AlloyHandler.xtend | |
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/AlloyHandler.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | 29 |
1 files changed, 17 insertions, 12 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) |