Merge branch 'kris'

7 files changed, 41 insertions, 50 deletions

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
index de68b5f7..25b7f16f 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
@@ -1,11 +1,15 @@
-<?xml version="1.0" encoding="UTF-8"?>

-<classpath>

-        <classpathentry kind="src" path="xtend-gen"/>

-        <classpathentry kind="src" path="queries"/>

-        <classpathentry kind="src" path="vql-gen"/>

-        <classpathentry exported="true" kind="lib" path="lib/alloy4.2_2015-02-22.jar"/>

-        <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>

-        <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>

-        <classpathentry kind="src" path="src"/>

-        <classpathentry kind="output" path="bin"/>

-</classpath>

+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+        <classpathentry kind="src" path="xtend-gen"/>
+        <classpathentry kind="src" path="queries"/>
+        <classpathentry kind="src" path="vql-gen"/>
+        <classpathentry exported="true" kind="lib" path="lib/alloy4.2_2015-02-22.jar"/>
+        <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
+        <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
+        <classpathentry kind="src" path="src">
+                <attributes>
+                        <attribute name="org.eclipse.jdt.launching.CLASSPATH_ATTR_LIBRARY_PATH_ENTRY" value="hu.bme.mit.inf.dlsreasoner.alloy.reasoner/lib"/>
+                </attributes>
+        </classpathentry>
+        <classpathentry kind="output" path="bin"/>
+</classpath>
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 b944302b..75581def 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
@@ -20,7 +20,8 @@ Require-Bundle: com.google.guava,
  org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.3.0",
  hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
  org.eclipse.viatra.query.runtime;bundle-version="2.0.0"
-Import-Package: org.apache.log4j;version="1.2.15"
-Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner
-Bundle-ActivationPolicy: lazy
 Bundle-RequiredExecutionEnvironment: JavaSE-1.8
+Bundle-ActivationPolicy: lazy
+Bundle-NativeCode: libminisat.so;osname=Linux;processor=x86_64
+Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner
+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/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
index f6b0b4a5..1eb6442b 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
@@ -62,7 +62,7 @@ class AlloySolver extends LogicReasoner{
                 val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode)

                 alloyConfig.progressMonitor.workedSearchFinished

                 

-                val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)

+                val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolutions,result2,forwardTrace,transformationTime)

                 alloyConfig.progressMonitor.workedBackwardTransformationFinished

                 //val solverFinish = System.currentTimeMillis-solverStart

                 // Finish: Solving Alloy problem

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
index 2efd6b29..328ca176 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
@@ -9,7 +9,7 @@ class Alloy2LogicMapper {
         public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {

                 val models = monitoredAlloySolution.aswers.map[it.key].toList

                 

-                if(!monitoredAlloySolution.finishedBeforeTimeout) {

+                if(models.empty || !monitoredAlloySolution.finishedBeforeTimeout) {

                         return createInsuficientResourcesResult => [

                                 it.problem = problem

                                 it.representation += models

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 9b4265b9..451aad6e 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
@@ -101,15 +101,8 @@ class AlloyHandler {
                         try{

                                 answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS)

                                 finished = true

-                        } catch (TimeoutException ex) {

-                                // handle the timeout

-                        } catch (InterruptedException e) {

-                                // handle the interrupts

-                        } catch (ExecutionException e) {

-                                // handle other exceptions

-                        } finally {

-                                future.cancel(true);

-                                

+                        } catch (TimeoutException | InterruptedException | ExecutionException e) {

+                                future.cancel(true)

                                 answers = callable.partialAnswers

                                 finished = false

                         }

@@ -195,7 +188,7 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
                                         } else {

                                                 lastAnswer = lastAnswer.next

                                         }

-                                        configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution)

+                                        configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolutions)

                                         

                                         val runtime = System.currentTimeMillis -startTime

                                         synchronized(this) {

@@ -212,8 +205,8 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
         }

         

         def hasEnoughSolution(List<?> answers) {

-                if(configuration.solutionScope.numberOfRequiredSolution < 0) return false

-                else return answers.size() == configuration.solutionScope.numberOfRequiredSolution

+                if(configuration.solutionScope.numberOfRequiredSolutions < 0) return false

+                else return answers.size() == configuration.solutionScope.numberOfRequiredSolutions

         }

         

         public def getPartialAnswers() {

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
index 494197bc..b74017d8 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
@@ -9,8 +9,12 @@ import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm

 import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition

 import java.util.List

 

+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

+

 class RunCommandMapper {

         val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE

         val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;

@@ -89,16 +93,18 @@ class RunCommandMapper {
                 ]

                 

                 for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) {

-                        val limit = upperLimit.value

+                        val type = upperLimit.key

+                        val limit = upperLimit.value + getExistingCount(type)

                         if(limit != LogicSolverConfiguration::Unlimited) {

-                                this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace)

+                                this.typeScopeMapping.addUpperMultiplicity(specification,type,limit,mapper,trace)

                         }

                 }

                 

                 for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) {

-                        val limit = lowerLimit.value

+                        val type = lowerLimit.key

+                        val limit = lowerLimit.value + getExistingCount(type)

                         if(limit != 0) {

-                                this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace)

+                                this.typeScopeMapping.addLowerMultiplicity(specification,type,limit,mapper,trace)

                         }

                 }

                 

@@ -106,6 +112,11 @@ class RunCommandMapper {
                 setStringScope(specification,config,specification.runCommand)

         }

         

+        private def getExistingCount(Type type) {

+                val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet

+                existing.size

+        }

+        

         protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) {

                 if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) {

                         throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch
deleted file mode 100644
index 77031bf1..00000000
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch
+++ /dev/null
@@ -1,18 +0,0 @@
-<?xml version="1.0" encoding="UTF-8" standalone="no"?>

-<launchConfiguration type="org.eclipse.emf.mwe2.launch.Mwe2LaunchConfigurationType">

-<stringAttribute key="org.eclipse.debug.core.ATTR_REFRESH_SCOPE" value="${working_set:&lt;?xml version=&quot;1.0&quot; encoding=&quot;UTF-8&quot;?&gt;&#10;&lt;launchConfigurationWorkingSet factoryID=&quot;org.eclipse.ui.internal.WorkingSetFactory&quot; id=&quot;1299248699643_13&quot; label=&quot;working set&quot; name=&quot;working set&quot;&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.alloy.language&quot; type=&quot;4&quot;/&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.alloy.language.generator&quot; type=&quot;4&quot;/&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.alloy.language.tests&quot; type=&quot;4&quot;/&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.alloy.language.ui&quot; type=&quot;4&quot;/&gt;&#10;&lt;/launchConfigurationWorkingSet&gt;}"/>

-<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_PATHS">

-<listEntry value="/hu.bme.mit.inf.dslreasoner.alloy.language"/>

-</listAttribute>

-<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_TYPES">

-<listEntry value="4"/>

-</listAttribute>

-<listAttribute key="org.eclipse.debug.ui.favoriteGroups">

-<listEntry value="org.eclipse.debug.ui.launchGroup.debug"/>

-<listEntry value="org.eclipse.debug.ui.launchGroup.run"/>

-</listAttribute>

-<stringAttribute key="org.eclipse.jdt.launching.MAIN_TYPE" value="org.eclipse.emf.mwe2.launch.runtime.Mwe2Launcher"/>

-<stringAttribute key="org.eclipse.jdt.launching.PROGRAM_ARGUMENTS" value="src/hu/bme/mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2"/>

-<stringAttribute key="org.eclipse.jdt.launching.PROJECT_ATTR" value="hu.bme.mit.inf.dslreasoner.alloy.language"/>

-<stringAttribute key="org.eclipse.jdt.launching.VM_ARGUMENTS" value="-Xmx512m"/>

-</launchConfiguration>