From f0f92fa2c4a6f61d5deea376f7f971e0c40238f5 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 24 Feb 2018 18:30:13 -0500 Subject: Documentation level for Alloy --- .../alloy/reasoner/builder/AlloyHandler.xtend | 29 +++++++++++++--------- 1 file changed, 17 insertions(+), 12 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend') 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 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder +import com.google.common.util.concurrent.SimpleTimeLimiter +import com.google.common.util.concurrent.UncheckedTimeoutException import edu.mit.csail.sdg.alloy4.A4Reporter import edu.mit.csail.sdg.alloy4.Err import edu.mit.csail.sdg.alloy4.ErrorWarning @@ -7,25 +9,24 @@ import edu.mit.csail.sdg.alloy4compiler.ast.Command import edu.mit.csail.sdg.alloy4compiler.parser.CompModule import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil import edu.mit.csail.sdg.alloy4compiler.translator.A4Options +import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.util.ArrayList +import java.util.HashMap import java.util.LinkedList import java.util.List -import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver -import org.eclipse.xtend.lib.annotations.Data import java.util.Map -import java.util.HashMap -import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver -import org.eclipse.emf.common.CommonPlugin -import java.util.ArrayList -import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument -import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration -import com.google.common.util.concurrent.SimpleTimeLimiter import java.util.concurrent.Callable import java.util.concurrent.TimeUnit -import com.google.common.util.concurrent.UncheckedTimeoutException -import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration +import org.eclipse.emf.common.CommonPlugin +import org.eclipse.xtend.lib.annotations.Data +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel class AlloySolverException extends Exception{ new(String s) { super(s) } @@ -48,6 +49,10 @@ class AlloyHandler { //val fileName = "problem.als" public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, String alloyCode) { + val writeToFile = ( + configuration.documentationLevel===DocumentationLevel::NORMAL || + configuration.documentationLevel===DocumentationLevel::FULL) + //Prepare val warnings = new LinkedList @@ -78,7 +83,7 @@ class AlloyHandler { // Start: Alloy -> Kodkod val kodkodTransformStart = System.currentTimeMillis(); try { - if(configuration.writeToFile) { + if(writeToFile) { compModule = CompUtil.parseEverything_fromFile(reporter,null,path) } else { compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) -- cgit v1.2.3-70-g09d2