From 2674956aeb76910420e89afa29ad2441b7b14f96 Mon Sep 17 00:00:00 2001
From: Oszkar Semerath <semerath@mit.bme.hu>
Date: Tue, 1 Oct 2019 19:09:53 +0200
Subject: handler refactor

---
 .../alloy/reasoner/builder/AlloyHandler.xtend      | 23 ++++++++++++++++------
 1 file changed, 17 insertions(+), 6 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 ebbca624..9b4265b9 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
@@ -1,7 +1,5 @@
 package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
 
-import com.google.common.util.concurrent.SimpleTimeLimiter
-import com.google.common.util.concurrent.UncheckedTimeoutException
 import edu.mit.csail.sdg.alloy4.A4Reporter
 import edu.mit.csail.sdg.alloy4.Err
 import edu.mit.csail.sdg.alloy4.ErrorWarning
@@ -23,7 +21,11 @@ import java.util.LinkedList
 import java.util.List
 import java.util.Map
 import java.util.concurrent.Callable
+import java.util.concurrent.ExecutionException
+import java.util.concurrent.ExecutorService
+import java.util.concurrent.Executors
 import java.util.concurrent.TimeUnit
+import java.util.concurrent.TimeoutException
 import org.eclipse.xtend.lib.annotations.Data
 
 class AlloySolverException extends Exception{
@@ -46,7 +48,7 @@ class AlloyHandler {
 	
 	//val fileName = "problem.als"
 	
-	public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) {
+	def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) {
 		
 		//Prepare
 		val warnings = new LinkedList<String>
@@ -87,7 +89,6 @@ class AlloyHandler {
 		val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart
 		// Finish: Alloy -> Kodkod
 		
-		val limiter = new SimpleTimeLimiter
 		val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration)
 		var List<Pair<A4Solution, Long>> answers
 		var boolean finished
@@ -95,10 +96,20 @@ class AlloyHandler {
 			answers = callable.call
 			finished = true
 		} else {
+			val ExecutorService executor = Executors.newCachedThreadPool();
+			val future = executor.submit(callable)
 			try{
-				answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true)
+				answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS)
 				finished = true
-			} catch (UncheckedTimeoutException e) {
+			} catch (TimeoutException ex) {
+   				// handle the timeout
+			} catch (InterruptedException e) {
+				// handle the interrupts
+			} catch (ExecutionException e) {
+				// handle other exceptions
+			} finally {
+				future.cancel(true);
+				
 				answers = callable.partialAnswers
 				finished = false
 			}
-- 
cgit v1.2.3-54-g00ecf


From bdae1b59c53cd1743b8b2ad2cd1d3c3a51327e8b Mon Sep 17 00:00:00 2001
From: Oszkar Semerath <semerath@mit.bme.hu>
Date: Sat, 19 Oct 2019 22:17:48 +0200
Subject: fixing index out ot bound exceptions for state coders

---
 .../statecoder/NeighbourhoodBasedStateCoderFactory.xtend                | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
index a86bcd1f..19c70574 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
@@ -133,11 +133,11 @@ class NeighbourhoodBasedPartialInterpretationStateCoder implements IStateCoder{
 	   	
         while(index < size) {
         	res.add(getCode(match.get(index)))
-        	index++
         	for(var i = 0; i<index; i++) {
         		val number = if(match.get(index) === match.get(i)){1}else{0}
         		equivalenceHash = prime * equivalenceHash + number
         	}
+        	index++
         }
         
         statecoderRuntime += (System.nanoTime - startTime)
-- 
cgit v1.2.3-54-g00ecf