Documentation level for Alloy

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
 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<String>

@@ -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)