Adding multiple model generation support for the alloy solver.

3 files changed, 11 insertions, 10 deletions

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 d0c7d320..65539155 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
@@ -16,6 +16,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult

 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace

+import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution

+import java.util.List

 

 class AlloySolver extends LogicReasoner{

         

@@ -72,16 +74,16 @@ class AlloySolver extends LogicReasoner{
         }

         

         override getInterpretations(ModelResult modelResult) {

-                val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]

-                val res = answers.map [

+                //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]

+                val sols = modelResult.representation// as List<A4Solution>

+                //val res = answers.map 

+                sols.map[

                         new AlloyModelInterpretation(

                                 new AlloyModelInterpretation_TypeInterpretation_FilteredTypes,

-                                it,

+                                it as A4Solution,

                                 forwardMapper,

                                 modelResult.trace as Logic2AlloyLanguageMapperTrace

                         )

                 ]

-                        

-                return res

         }       

 }
\ 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/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 7db9e0ea..2efd6b29 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(!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 17220776..c1f2ec4c 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
@@ -191,10 +191,9 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
                                 

                                 val runtime = System.currentTimeMillis -startTime

                                 synchronized(this) {

-                                        answers += lastAnswer->runtime

+                                        answers += (lastAnswer->runtime)

                                 }

-                                println( answers.size )

-                        } while(lastAnswer.satisfiable != false && hasEnoughSolution(answers))

+                        } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers))

                         

                 }catch(Exception e) {

                         warnings +=e.message

@@ -205,7 +204,7 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
         

         def hasEnoughSolution(List<?> answers) {

                 if(numberOfRequiredSolution < 0) return false

-                else return answers.size < numberOfRequiredSolution

+                else return answers.size() == numberOfRequiredSolution

         }

         

         public def getPartialAnswers() {