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 --- .../META-INF/MANIFEST.MF | 4 +-- .../reasoner/AlloyAnalyzerConfiguration.xtend | 9 ++--- .../dlsreasoner/alloy/reasoner/AlloySolver.xtend | 10 ++++-- .../alloy/reasoner/builder/AlloyHandler.xtend | 29 ++++++++------- .../builder/Logic2AlloyLanguageMapper.xtend | 41 ++++++++++++++-------- 5 files changed, 55 insertions(+), 38 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner') diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF index 13ad2d10..fd78a6ae 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF @@ -18,9 +18,9 @@ Require-Bundle: com.google.guava, org.eclipse.emf.ecore;visibility:=reexport, hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport, hu.bme.mit.inf.dslreasoner.alloy.language;bundle-version="1.0.0", - org.eclipse.viatra.query.runtime;bundle-version="[1.2.0,2.0.0)", org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.3.0", - hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0" + hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", + org.eclipse.viatra.query.runtime;bundle-version="2.0.0" Bundle-RequiredExecutionEnvironment: JavaSE-1.8 Bundle-ActivationPolicy: lazy Import-Package: org.apache.log4j;version="1.2.15" 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 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration class AlloySolverConfiguration extends LogicSolverConfiguration { - /*public var boolean createCommonSupertype - public var int intScope = 1 // 5 by default - public def setIntScopeFor(int max) { - intScope = 31 - Integer.numberOfLeadingZeros(max) + 1 - }*/ public var int symmetry = 20 // by default public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J - public var boolean writeToFile = false + public var TypeMappingTechnique typeMapping = TypeMappingTechnique.InheritanceAndHorizontal public var randomise = 0 } @@ -29,5 +24,5 @@ enum AlloyBackendSolver { } enum TypeMappingTechnique { - FilteredTypes + FilteredTypes, InheritanceAndHorizontal } \ 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 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration @@ -32,6 +33,9 @@ class AlloySolver extends LogicReasoner{ override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { val alloyConfig = configuration.asConfig + val writeToFile = ( + configuration.documentationLevel===DocumentationLevel::NORMAL || + configuration.documentationLevel===DocumentationLevel::FULL) // Start: Logic -> Alloy mapping val transformationStart = System.currentTimeMillis @@ -41,7 +45,7 @@ class AlloySolver extends LogicReasoner{ var String fileURI = null; var String alloyCode = null; - if(alloyConfig.writeToFile) { + if(writeToFile) { fileURI = workspace.writeModel(alloyProblem,fileName).toFileString } else { alloyCode = workspace.writeModelToString(alloyProblem,fileName) @@ -57,7 +61,7 @@ class AlloySolver extends LogicReasoner{ val solverFinish = System.currentTimeMillis-solverStart // Finish: Solving Alloy problem - if(alloyConfig.writeToFile) workspace.deactivateModel(fileName) + if(writeToFile) workspace.deactivateModel(fileName) return logicResult } @@ -66,7 +70,7 @@ class AlloySolver extends LogicReasoner{ if(configuration instanceof AlloySolverConfiguration) { return configuration } else { - throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''') + throw new IllegalArgumentException('''The configuration has to be an «AlloySolverConfiguration.simpleName»!''') } } 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) 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 import org.eclipse.xtend.lib.annotations.Accessors import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt class Logic2AlloyLanguageMapper { private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE @@ -311,22 +312,34 @@ class Logic2AlloyLanguageMapper { it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) ] - if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( - '''An integer scope have to be specified for Alloy!''') - it.typeScopes += createALSIntScope => [ - if(config.typeScopes.knownIntegers.empty) { - number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) + if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { + val integersUsed = specification.eAllContents.filter(ALSInt) + if(integersUsed.empty) { + // If no integer scope is defined, but the problem has no integers + // => scope can be empty + it.typeScopes+= createALSIntScope => [ + it.number = 0 + ] } else { - var scope = Math.max( - Math.abs(config.typeScopes.knownIntegers.max), - Math.abs(config.typeScopes.knownIntegers.min)) - if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { - scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 - } - number = Integer.SIZE-Integer.numberOfLeadingZeros(scope) + // If no integer scope is defined, and the problem has integers + // => error + throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') } - - ] + } else { + it.typeScopes += createALSIntScope => [ + if(config.typeScopes.knownIntegers.empty) { + number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) + } else { + var scope = Math.max( + Math.abs(config.typeScopes.knownIntegers.max), + Math.abs(config.typeScopes.knownIntegers.min)) + if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { + scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 + } + number = Integer.SIZE-Integer.numberOfLeadingZeros(scope) + } + ] + } // for(definedScope : config.typeScopes.allDefinedScope) { // it.typeScopes += createALSSigScope => [ // it.type = definedScope.type.lookup(trace.type2ALSType) -- cgit v1.2.3-54-g00ecf