Alloy implementation of multiple model generation

author: OszkarSemerath <oszka@152.66.252.189> 2017-07-02 23:34:27 +0200
committer: OszkarSemerath <oszka@152.66.252.189> 2017-07-02 23:34:27 +0200
commit: f00ce77fdc3a1417ddfd833f122b64ecef80d7d6 (patch)
tree: 2a26b61a43576f58ed4c35680bd47fa3c15df3d8 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit
parent: Multiple model with interpretations (diff)
download: VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.tar.gz
VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.tar.zst
VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.zip
4 files changed, 178 insertions, 70 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
+                        return configuration
-                        val result = forwardMapper.transformProblem(problem,configuration)
+                } else {
-                        val alloyProblem = result.output
+                        throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''')      
-                        
+                }
-                        /*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»!''')
        }
        
-        override getInterpretation(ModelResult modelResult) {
+        override getInterpretations(ModelResult modelResult) {
-                return new AlloyModelInterpretation(
+                val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
-                        new AlloyModelInterpretation_TypeInterpretation_FilteredTypes,
+                val res = answers.map [
-                        (modelResult.representation as MonitoredAlloySolution).solution,
+                        new AlloyModelInterpretation(
-                        forwardMapper,
+                                new AlloyModelInterpretation_TypeInterpretation_FilteredTypes,
-                        modelResult.trace as Logic2AlloyLanguageMapperTrace
+                                it,
-                );
+                                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 637752b0..7db9e0ea 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
@@ -6,28 +6,30 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
 class Alloy2LogicMapper {
        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
        
-        public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
+        public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
-                if(solution == null) {
+                val models = monitoredAlloySolution.aswers.map[it.key].toList
+                
+                if(monitoredAlloySolution.finishedBeforeTimeout) {
                        return createInsuficientResourcesResult => [
                                it.problem = problem
-                                it.statistics = transformStatistics(solution,transformationTime)
+                                it.representation += models
+                                it.trace = trace
+                                it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
                        ]
                } else {
-                        val logicResult = solution.solution
+                        if(models.last.satisfiable || requiredNumberOfSolution == -1) {
-                        if(logicResult.satisfiable) {
                                return createModelResult => [
                                        it.problem = problem
-                                        it.representation += solution
+                                        it.representation += models
-                                        it.maxInteger = logicResult.max
-                                        it.minInteger = logicResult.min
                                        it.trace = trace
-                                        it.statistics = transformStatistics(solution,transformationTime)
+                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
                                ]
                        } else {
                                return createInconsistencyResult => [
                                        it.problem = problem
-                                        //trace?
+                                        it.representation += models
-                                        it.statistics = transformStatistics(solution,transformationTime)
+                                        it.trace = trace
+                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
                                ]
                        }
                }
@@ -36,13 +38,29 @@ class Alloy2LogicMapper {
        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
                createStatistics => [
                        it.transformationTime = transformationTime as int
-                        if(solution != null) {
+                        for(solutionIndex : 0..<solution.aswers.size) {
-                                it.solverTime = solution.runtimeTime as int
+                                val solutionTime = solution.aswers.get(solutionIndex).value
-                                it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [
+                                 it.entries+= createIntStatisticEntry => [
-                                        it.name = "KoodkodToCNFTransformationTime"
+                                        it.name = '''Answer«solutionIndex»Time'''
-                                        it.value = solution.getKodkodTime as int
+                                        it.value = solutionTime.intValue
                                ]
                        }
+                        it.entries+= createIntStatisticEntry => [
+                                it.name = "Alloy2KodKodTransformationTime"
+                                it.value = solution.kodkodTime as int
+                        ]
+                        it.entries+= createIntStatisticEntry => [
+                                it.name = "Alloy2KodKodTransformationTime"
+                                it.value = solution.kodkodTime as int
+                        ]
+                        it.entries+= createStringStatisticEntry => [
+                                it.name = "warnings"
+                                it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
+                        ]
                ]
        }
+        
+        def sum(Iterable<Long> ints) {
+                ints.reduce[p1, p2|p1+p2]
+        }
 }
 \ 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/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 6bac4130..17220776 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
@@ -21,6 +21,11 @@ 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
 class AlloySolverException extends Exception{
        new(String s) { super(s) }
@@ -34,9 +39,8 @@ class AlloySolverException extends Exception{
        List<String> warnings
        List<String> debugs
        long kodkodTime
-        long runtimeTime
+        val List<Pair<A4Solution, Long>> aswers
-        
+        val boolean finishedBeforeTimeout
-        A4Solution solution
 }
 class AlloyHandler {
@@ -63,6 +67,7 @@ class AlloyHandler {
                        if(configuration.solver.externalSolver) {
                                it.solverDirectory = configuration.solverPath
                        }
+                        //it.inferPartialInstance
                        it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString
                ]
                
@@ -70,8 +75,8 @@ class AlloyHandler {
                var Command command = null;
                var CompModule compModule = null
                
+                // Start: Alloy -> Kodkod
                val kodkodTransformStart = System.currentTimeMillis();
-                
                try {
                        if(configuration.writeToFile) {
                                compModule = CompUtil.parseEverything_fromFile(reporter,null,path)
@@ -85,23 +90,26 @@ class AlloyHandler {
                        throw new AlloySolverException(e.message,warnings,e)
                }
                val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart
+                // Finish: Alloy -> Kodkod
                
-                //Execute
+                val limiter = new SimpleTimeLimiter
-                var A4Solution answer = null;
+                val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration.solutionScope.numberOfRequiredSolution)
-                try {
+                var List<Pair<A4Solution, Long>> answers
-                        answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
+                var boolean finished
-                }catch(Exception e) {
+                if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) {
-                        warnings +=e.message
+                        answers = callable.call
-                }
+                        finished = true
-                
-                var long runtimeFromAnswer;
-                if(runtime.empty) {
-                        runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish)
                } else {
-                        runtimeFromAnswer = runtime.head
+                        try{
+                                answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true)
+                                finished = true
+                        } catch (UncheckedTimeoutException e) {
+                                answers = callable.partialAnswers
+                                finished = false
+                        }
                }
-                
-                return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer)
+                new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished)
        }
        
        val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap
@@ -138,6 +146,73 @@ class AlloyHandler {
        }
 }
+class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
+        
+        val List<String> warnings
+        val List<String> debugs
+        val A4Reporter reporter
+        val A4Options options
+        
+        val Command command
+        val CompModule compModule
+        val int numberOfRequiredSolution
+        
+        val List<Pair<A4Solution,Long>> answers = new LinkedList()
+        
+        new(List<String> warnings,
+                List<String> debugs,
+                A4Reporter reporter,
+                A4Options options,
+                Command command,
+                CompModule compModule,
+                int numberOfRequiredSolution)
+        {
+                this.warnings = warnings
+                this.debugs = debugs
+                this.reporter = reporter
+                this.options = options
+                this.command = command
+                this.compModule = compModule
+                this.numberOfRequiredSolution = numberOfRequiredSolution
+        }
+        
+        override call() throws Exception {
+                val startTime = System.currentTimeMillis
+                
+                // Start: Execute
+                var A4Solution lastAnswer = null
+                try {
+                        do{
+                                if(lastAnswer == null) {
+                                        lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
+                                } else {
+                                        lastAnswer = lastAnswer.next
+                                }
+                                
+                                val runtime = System.currentTimeMillis -startTime
+                                synchronized(this) {
+                                        answers += lastAnswer->runtime
+                                }
+                                println( answers.size )
+                        } while(lastAnswer.satisfiable != false && hasEnoughSolution(answers))
+                        
+                }catch(Exception e) {
+                        warnings +=e.message
+                }
+                // Finish: execute
+                return answers
+        }
+        
+        def hasEnoughSolution(List<?> answers) {
+                if(numberOfRequiredSolution < 0) return false
+                else return answers.size < numberOfRequiredSolution
+        }
+        
+        public def getPartialAnswers() {
+                return answers
+        }
+}
 @Data class SolverConfiguration {
        AlloyBackendSolver backedSolver
        String path
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 23b9027f..65fdcfdf 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
@@ -277,7 +277,7 @@ class Logic2AlloyLanguageMapper {
                        it.typeScopes+= createALSSigScope => [
                                it.type= typeMapper.getUndefinedSupertype(trace)
                                it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) 
-                                //it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements)
+                                it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
                        ]
                        if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException(
                                '''An integer scope have to be specified for Alloy!''')
author	OszkarSemerath <oszka@152.66.252.189>	2017-07-02 23:34:27 +0200
committer	OszkarSemerath <oszka@152.66.252.189>	2017-07-02 23:34:27 +0200
commit	f00ce77fdc3a1417ddfd833f122b64ecef80d7d6 (patch)
tree	2a26b61a43576f58ed4c35680bd47fa3c15df3d8 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit
parent	Multiple model with interpretations (diff)
download	VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.tar.gz VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.tar.zst VIATRA-Generator-f00ce77fdc3a1417ddfd833f122b64ecef80d7d6.zip

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
3	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper	3	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper
4	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler	4	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler
5	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation	5	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation
		6	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes
6	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper	7	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper
7	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace	8	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace
		9	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes
8	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution	10	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution
9	import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated	11	import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated
10	import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage	12	import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage
@@ -14,9 +16,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
14	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem	16	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
15	import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult	17	import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
16	import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace	18	import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
17	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes
18	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes
19	import org.eclipse.emf.common.util.URI
20		19
21	class AlloySolver extends LogicReasoner{	20	class AlloySolver extends LogicReasoner{
22		21
@@ -33,40 +32,56 @@ class AlloySolver extends LogicReasoner{
33	val fileName = "problem.als"	32	val fileName = "problem.als"
34		33
35	override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {	34	override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
		35	val alloyConfig = configuration.asConfig
		36
		37	// Start: Logic -> Alloy mapping
		38	val transformationStart = System.currentTimeMillis
		39	val result = forwardMapper.transformProblem(problem,alloyConfig)
		40	val alloyProblem = result.output
		41	val forwardTrace = result.trace
		42
		43	var String fileURI = null;
		44	var String alloyCode = null;
		45	if(alloyConfig.writeToFile) {
		46	fileURI = workspace.writeModel(alloyProblem,fileName).toFileString
		47	} else {
		48	alloyCode = workspace.writeModelToString(alloyProblem,fileName)
		49	}
		50	val transformationTime = System.currentTimeMillis - transformationStart
		51	// Finish: Logic -> Alloy mapping
		52
		53
		54	// Start: Solving Alloy problem
		55	val solverStart = System.currentTimeMillis
		56	val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode)
		57	val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
		58	val solverFinish = System.currentTimeMillis-solverStart
		59	// Finish: Solving Alloy problem
		60
		61	if(alloyConfig.writeToFile) workspace.deactivateModel(fileName)
		62
		63	return logicResult
		64	}
		65
		66	def asConfig(LogicSolverConfiguration configuration) {
36	if(configuration instanceof AlloySolverConfiguration) {	67	if(configuration instanceof AlloySolverConfiguration) {
37	val transformationStart = System.currentTimeMillis	68	return configuration
38	val result = forwardMapper.transformProblem(problem,configuration)	69	} else {
39	val alloyProblem = result.output	70	throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''')
40		71	}
41	/*val x = alloyProblem.eAllContents.filter(ALSFunctionCall).filter[it.referredDefinition == null].toList
42	println(x)*/
43	val forwardTrace = result.trace
44
45	var String fileURI = null;
46	var String alloyCode = null;
47	if(configuration.writeToFile) {
48	fileURI = workspace.writeModel(alloyProblem,fileName).toFileString
49	} else {
50	alloyCode = workspace.writeModelToString(alloyProblem,fileName)
51	}
52
53	//val alloyCode = workspace.readText(fileName)
54	//val FunctionWithTimeout<MonitoredAlloySolution> call = new FunctionWithTimeout[]
55
56	val transformationTime = System.currentTimeMillis - transformationStart
57	val result2 = handler.callSolver(alloyProblem,workspace,configuration,fileURI,alloyCode)
58	workspace.deactivateModel(fileName)
59	val logicResult = backwardMapper.transformOutput(problem,result2,forwardTrace,transformationTime)
60	return logicResult
61	} else throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''')
62	}	72	}
63		73
64	override getInterpretation(ModelResult modelResult) {	74	override getInterpretations(ModelResult modelResult) {
65	return new AlloyModelInterpretation(	75	val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
66	new AlloyModelInterpretation_TypeInterpretation_FilteredTypes,	76	val res = answers.map [
67	(modelResult.representation as MonitoredAlloySolution).solution,	77	new AlloyModelInterpretation(
68	forwardMapper,	78	new AlloyModelInterpretation_TypeInterpretation_FilteredTypes,
69	modelResult.trace as Logic2AlloyLanguageMapperTrace	79	it,
70	);	80	forwardMapper,
		81	modelResult.trace as Logic2AlloyLanguageMapperTrace
		82	)
		83	]
		84
		85	return res
71	}	86	}
72	} \ No newline at end of file	87	} \ 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 637752b0..7db9e0ea 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
@@ -6,28 +6,30 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
6	class Alloy2LogicMapper {	6	class Alloy2LogicMapper {
7	val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE	7	val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
8		8
9	public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {	9	public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
10	if(solution == null) {	10	val models = monitoredAlloySolution.aswers.map[it.key].toList
		11
		12	if(monitoredAlloySolution.finishedBeforeTimeout) {
11	return createInsuficientResourcesResult => [	13	return createInsuficientResourcesResult => [
12	it.problem = problem	14	it.problem = problem
13	it.statistics = transformStatistics(solution,transformationTime)	15	it.representation += models
		16	it.trace = trace
		17	it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
14	]	18	]
15	} else {	19	} else {
16	val logicResult = solution.solution	20	if(models.last.satisfiable \|\| requiredNumberOfSolution == -1) {
17	if(logicResult.satisfiable) {
18	return createModelResult => [	21	return createModelResult => [
19	it.problem = problem	22	it.problem = problem
20	it.representation += solution	23	it.representation += models
21	it.maxInteger = logicResult.max
22	it.minInteger = logicResult.min
23	it.trace = trace	24	it.trace = trace
24	it.statistics = transformStatistics(solution,transformationTime)	25	it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
25	]	26	]
26	} else {	27	} else {
27	return createInconsistencyResult => [	28	return createInconsistencyResult => [
28	it.problem = problem	29	it.problem = problem
29	//trace?	30	it.representation += models
30	it.statistics = transformStatistics(solution,transformationTime)	31	it.trace = trace
		32	it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
31	]	33	]
32	}	34	}
33	}	35	}
@@ -36,13 +38,29 @@ class Alloy2LogicMapper {
36	def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {	38	def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
37	createStatistics => [	39	createStatistics => [
38	it.transformationTime = transformationTime as int	40	it.transformationTime = transformationTime as int
39	if(solution != null) {	41	for(solutionIndex : 0..<solution.aswers.size) {
40	it.solverTime = solution.runtimeTime as int	42	val solutionTime = solution.aswers.get(solutionIndex).value
41	it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [	43	it.entries+= createIntStatisticEntry => [
42	it.name = "KoodkodToCNFTransformationTime"	44	it.name = '''Answer«solutionIndex»Time'''
43	it.value = solution.getKodkodTime as int	45	it.value = solutionTime.intValue
44	]	46	]
45	}	47	}
		48	it.entries+= createIntStatisticEntry => [
		49	it.name = "Alloy2KodKodTransformationTime"
		50	it.value = solution.kodkodTime as int
		51	]
		52	it.entries+= createIntStatisticEntry => [
		53	it.name = "Alloy2KodKodTransformationTime"
		54	it.value = solution.kodkodTime as int
		55	]
		56	it.entries+= createStringStatisticEntry => [
		57	it.name = "warnings"
		58	it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
		59	]
46	]	60	]
47	}	61	}
		62
		63	def sum(Iterable<Long> ints) {
		64	ints.reduce[p1, p2\|p1+p2]
		65	}
48	} \ No newline at end of file	66	} \ 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/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 6bac4130..17220776 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
@@ -21,6 +21,11 @@ import org.eclipse.emf.common.CommonPlugin
21	import java.util.ArrayList	21	import java.util.ArrayList
22	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument	22	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
23	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration	23	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
		24	import com.google.common.util.concurrent.SimpleTimeLimiter
		25	import java.util.concurrent.Callable
		26	import java.util.concurrent.TimeUnit
		27	import com.google.common.util.concurrent.UncheckedTimeoutException
		28	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
24		29
25	class AlloySolverException extends Exception{	30	class AlloySolverException extends Exception{
26	new(String s) { super(s) }	31	new(String s) { super(s) }
@@ -34,9 +39,8 @@ class AlloySolverException extends Exception{
34	List<String> warnings	39	List<String> warnings
35	List<String> debugs	40	List<String> debugs
36	long kodkodTime	41	long kodkodTime
37	long runtimeTime	42	val List<Pair<A4Solution, Long>> aswers
38		43	val boolean finishedBeforeTimeout
39	A4Solution solution
40	}	44	}
41		45
42	class AlloyHandler {	46	class AlloyHandler {
@@ -63,6 +67,7 @@ class AlloyHandler {
63	if(configuration.solver.externalSolver) {	67	if(configuration.solver.externalSolver) {
64	it.solverDirectory = configuration.solverPath	68	it.solverDirectory = configuration.solverPath
65	}	69	}
		70	//it.inferPartialInstance
66	it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString	71	it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString
67	]	72	]
68		73
@@ -70,8 +75,8 @@ class AlloyHandler {
70	var Command command = null;	75	var Command command = null;
71	var CompModule compModule = null	76	var CompModule compModule = null
72		77
		78	// Start: Alloy -> Kodkod
73	val kodkodTransformStart = System.currentTimeMillis();	79	val kodkodTransformStart = System.currentTimeMillis();
74
75	try {	80	try {
76	if(configuration.writeToFile) {	81	if(configuration.writeToFile) {
77	compModule = CompUtil.parseEverything_fromFile(reporter,null,path)	82	compModule = CompUtil.parseEverything_fromFile(reporter,null,path)
@@ -85,23 +90,26 @@ class AlloyHandler {
85	throw new AlloySolverException(e.message,warnings,e)	90	throw new AlloySolverException(e.message,warnings,e)
86	}	91	}
87	val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart	92	val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart
		93	// Finish: Alloy -> Kodkod
88		94
89	//Execute	95	val limiter = new SimpleTimeLimiter
90	var A4Solution answer = null;	96	val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration.solutionScope.numberOfRequiredSolution)
91	try {	97	var List<Pair<A4Solution, Long>> answers
92	answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)	98	var boolean finished
93	}catch(Exception e) {	99	if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) {
94	warnings +=e.message	100	answers = callable.call
95	}	101	finished = true
96
97	var long runtimeFromAnswer;
98	if(runtime.empty) {
99	runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish)
100	} else {	102	} else {
101	runtimeFromAnswer = runtime.head	103	try{
		104	answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true)
		105	finished = true
		106	} catch (UncheckedTimeoutException e) {
		107	answers = callable.partialAnswers
		108	finished = false
		109	}
102	}	110	}
103		111
104	return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer)	112	new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished)
105	}	113	}
106		114
107	val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap	115	val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap
@@ -138,6 +146,73 @@ class AlloyHandler {
138	}	146	}
139	}	147	}
140		148
		149	class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
		150
		151	val List<String> warnings
		152	val List<String> debugs
		153	val A4Reporter reporter
		154	val A4Options options
		155
		156	val Command command
		157	val CompModule compModule
		158	val int numberOfRequiredSolution
		159
		160	val List<Pair<A4Solution,Long>> answers = new LinkedList()
		161
		162	new(List<String> warnings,
		163	List<String> debugs,
		164	A4Reporter reporter,
		165	A4Options options,
		166	Command command,
		167	CompModule compModule,
		168	int numberOfRequiredSolution)
		169	{
		170	this.warnings = warnings
		171	this.debugs = debugs
		172	this.reporter = reporter
		173	this.options = options
		174	this.command = command
		175	this.compModule = compModule
		176	this.numberOfRequiredSolution = numberOfRequiredSolution
		177	}
		178
		179	override call() throws Exception {
		180	val startTime = System.currentTimeMillis
		181
		182	// Start: Execute
		183	var A4Solution lastAnswer = null
		184	try {
		185	do{
		186	if(lastAnswer == null) {
		187	lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
		188	} else {
		189	lastAnswer = lastAnswer.next
		190	}
		191
		192	val runtime = System.currentTimeMillis -startTime
		193	synchronized(this) {
		194	answers += lastAnswer->runtime
		195	}
		196	println( answers.size )
		197	} while(lastAnswer.satisfiable != false && hasEnoughSolution(answers))
		198
		199	}catch(Exception e) {
		200	warnings +=e.message
		201	}
		202	// Finish: execute
		203	return answers
		204	}
		205
		206	def hasEnoughSolution(List<?> answers) {
		207	if(numberOfRequiredSolution < 0) return false
		208	else return answers.size < numberOfRequiredSolution
		209	}
		210
		211	public def getPartialAnswers() {
		212	return answers
		213	}
		214	}
		215
141	@Data class SolverConfiguration {	216	@Data class SolverConfiguration {
142	AlloyBackendSolver backedSolver	217	AlloyBackendSolver backedSolver
143	String path	218	String path


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 23b9027f..65fdcfdf 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
@@ -277,7 +277,7 @@ class Logic2AlloyLanguageMapper {
277	it.typeScopes+= createALSSigScope => [	277	it.typeScopes+= createALSSigScope => [
278	it.type= typeMapper.getUndefinedSupertype(trace)	278	it.type= typeMapper.getUndefinedSupertype(trace)
279	it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace)	279	it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace)
280	//it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements)	280	it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
281	]	281	]
282	if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException(	282	if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException(
283	'''An integer scope have to be specified for Alloy!''')	283	'''An integer scope have to be specified for Alloy!''')