1 files changed, 93 insertions, 18 deletions
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/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