1 files changed, 50 insertions, 35 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 7dfc3161..d0c7d320 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
@@ -3,8 +3,10 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner
 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation

+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace

+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution

 import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated

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

@@ -14,9 +16,6 @@ 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 hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes

-import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes

-import org.eclipse.emf.common.util.URI

 

 class AlloySolver extends LogicReasoner{

         

@@ -33,40 +32,56 @@ class AlloySolver extends LogicReasoner{
         val fileName = "problem.als"

         

         override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {

+                val alloyConfig = configuration.asConfig

+                

+                // Start: Logic -> Alloy mapping

+                val transformationStart = System.currentTimeMillis

+                val result = forwardMapper.transformProblem(problem,alloyConfig)

+                val alloyProblem = result.output

+                val forwardTrace = result.trace

+                

+                var String fileURI = null;

+                var String alloyCode = null;

+                if(alloyConfig.writeToFile) {

+                        fileURI = workspace.writeModel(alloyProblem,fileName).toFileString

+                } else {

+                        alloyCode = workspace.writeModelToString(alloyProblem,fileName)

+                } 

+                val transformationTime = System.currentTimeMillis - transformationStart

+                // Finish: Logic -> Alloy mapping

+                

+                

+                // Start: Solving Alloy problem

+                val solverStart = System.currentTimeMillis

+                val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode)

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

+                val solverFinish = System.currentTimeMillis-solverStart

+                // Finish: Solving Alloy problem

+                

+                if(alloyConfig.writeToFile) workspace.deactivateModel(fileName)

+                

+                return logicResult

+        }

+        

+        def asConfig(LogicSolverConfiguration configuration) {

                 if(configuration instanceof AlloySolverConfiguration) {

-                        val transformationStart = System.currentTimeMillis

-                        val result = forwardMapper.transformProblem(problem,configuration)

-                        val alloyProblem = result.output

-                        

-                        /*val x = alloyProblem.eAllContents.filter(ALSFunctionCall).filter[it.referredDefinition == null].toList

-                        println(x)*/

-                        val forwardTrace = result.trace

-                        

-                        var String fileURI = null;

-                        var String alloyCode = null;

-                        if(configuration.writeToFile) {

-                                fileURI = workspace.writeModel(alloyProblem,fileName).toFileString

-                        } else {

-                                alloyCode = workspace.writeModelToString(alloyProblem,fileName)

-                        }

-                        

-                        //val alloyCode = workspace.readText(fileName)

-                        //val FunctionWithTimeout<MonitoredAlloySolution> call = new FunctionWithTimeout[] 

-                        

-                        val transformationTime = System.currentTimeMillis - transformationStart

-                        val result2 = handler.callSolver(alloyProblem,workspace,configuration,fileURI,alloyCode)

-                        workspace.deactivateModel(fileName)

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

-                        return logicResult

-                } else throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''')

+                        return configuration

+                } else {

+                        throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''')      

+                }

         }

         

-        override getInterpretation(ModelResult modelResult) {

-                return new AlloyModelInterpretation(

-                        new AlloyModelInterpretation_TypeInterpretation_FilteredTypes,

-                        (modelResult.representation as MonitoredAlloySolution).solution,

-                        forwardMapper,

-                        modelResult.trace as Logic2AlloyLanguageMapperTrace

-                );

+        override getInterpretations(ModelResult modelResult) {

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

+                val res = answers.map [

+                        new AlloyModelInterpretation(

+                                new AlloyModelInterpretation_TypeInterpretation_FilteredTypes,

+                                it,

+                                forwardMapper,

+                                modelResult.trace as Logic2AlloyLanguageMapperTrace

+                        )

+                ]

+                        

+                return res

         }       

 }
\ No newline at end of file