setting interpreters for each runner

pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java

@@ -1,16 +1,16 @@
 package Interpreter;
 
-import fr.lip6.move.gal.itscl.modele.IListener;
 import fr.lip6.move.gal.itscl.modele.ListenerRunner;
 
-public class CegarInterpreter extends ListenerRunner implements Runnable, IListener{
+public class CegarInterpreter extends ListenerRunner{
 
 	public CegarInterpreter(int pipeSize) {
 		super(pipeSize);
 	}
 
-	public void run() {
-
+	public Boolean call() {
+		return null;
+		//interpretation of wat do we recieve in OutPut 
 	}
 
 

pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java

@@ -0,0 +1,16 @@
+package Interpreter;
+
+import fr.lip6.move.gal.itscl.modele.ListenerRunner;
+
+public class LTSminInterpreter extends ListenerRunner {
+
+	public LTSminInterpreter() {
+		super(4096);
+	}
+
+	public Boolean call() throws Exception {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+}

pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java

@@ -0,0 +1,15 @@
+package Interpreter;
+
+import fr.lip6.move.gal.itscl.modele.ListenerRunner;
+
+public class SMTInterpreter extends ListenerRunner {
+
+	public SMTInterpreter() {
+		super(4096);
+	}
+
+	public Boolean call() throws Exception {
+		// TODO Auto-generated method stub
+		return null;
+	}
+}

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java

@@ -1,19 +1,14 @@
 package fr.lip6.move.gal.application;
 
-import java.io.IOException;
-
-import java.util.Set;
-
-import org.smtlib.Log.IListener;
 
 import fr.lip6.move.gal.Property;
-import fr.lip6.move.gal.Specification;
+import fr.lip6.move.gal.itscl.modele.IListener;
 import fr.lip6.move.gal.itscl.modele.IRunner;
+import fr.lip6.move.gal.itscl.modele.Problem;
 
-public abstract class AbstractRunner implements IRunner {
 
-	protected Specification spec;
-	protected Set<String> doneProps;
+public abstract class AbstractRunner extends Problem implements IRunner {
+
 	protected IListener listener;
 
 	public AbstractRunner() {
@@ -23,22 +18,9 @@ public AbstractRunner() {
 	public void setListener(IListener l){
 		this.listener=l;
 	}
-
-	public void configure(Specification z3Spec, Set<String> doneProps) throws IOException {
-		this.spec = z3Spec;
-		this.doneProps = doneProps;
-	}
-
+
 	public abstract void solve();
 
-	public Specification getSpec() {
-		return spec;
-	}
-
-	public Set<String> getDoneProps() {
-		return doneProps;
-	}
-
 	public Boolean taskDone() {
 		for (Property prop : getSpec().getProperties()) {
 			if (!doneProps.contains(prop.getName())) {

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java

@@ -60,7 +60,7 @@ public class Application implements IApplication {
 	public Object start(IApplicationContext context) throws Exception {
 
 		String[] args = (String[]) context.getArguments().get(APPARGS);
-
+System.out.println("im here______");
 		String pwd = null;
 		String examination = null;
 		String z3path = null;
@@ -167,7 +167,6 @@ public Object start(IApplicationContext context) throws Exception {
 					z3Runner.configure(z3Spec, doneProps);
 					chRunner.attach(InteractApplication.add(z3Runner));
 				}
-
 				// run on a fresh copy to avoid any interference with other
 				// threads.
 				if (doCegar) {
@@ -185,6 +184,7 @@ public Object start(IApplicationContext context) throws Exception {
 			// decompose + simplify as needed
 			itsRunner = new ITSRunner(examination, reader, doITS, onlyGal, reader.getFolder());
 			itsRunner.configure(reader.getSpec(), doneProps);
+			itsRunner.setInterpreter();
 		}
 
 		if (doITS) {

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java

@@ -5,6 +5,7 @@
 import java.util.List;
 import java.util.logging.Logger;
 
+import Interpreter.CegarInterpreter;
 import fr.lip6.move.gal.Property;
 import fr.lip6.move.gal.cegar.frontend.CegarFrontEnd;
 import fr.lip6.move.gal.cegar.interfaces.IResult;
@@ -19,14 +20,14 @@ public class CegarRunner extends AbstractRunner {
 
 	public CegarRunner(String pwd) {
 		this.pwd = pwd;
-
+		setListener(new CegarInterpreter(4096));
 	}
 
 	private static Logger getLog() {
 		return Logger.getLogger("fr.lip6.move.gal");
 
 	}
-
+	
 	public Boolean taskDone() {
 		for (Property prop : todoProps) {
 			if (!doneProps.contains(prop.getName())) {
@@ -38,6 +39,11 @@ public Boolean taskDone() {
 		System.out.println("tasks resolved Cegar");
 		return true;
 	}
+
+	public void setInterpreter() {
+		// TODO Auto-generated method stub
+
+	}
 
 	public void solve() {
 
@@ -77,4 +83,6 @@ public void solve() {
 		System.out.println("CEGAR HAS COMPLETELY FINISHED");
 
 	}
+
+
 }

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java

@@ -237,49 +237,50 @@ public String outputGalFile() throws IOException {
 		return outpath;
 	}
 
+	public Boolean taskDone() {
+		if (done) {
+			System.out.println("tasks resolved Its");
+			return true;
+		}
+		System.out.println("tasks not all resolved Its");
+		return false;
+	}
+
+	public void setInterpreter() {
+		setListener(new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, 4096));
+	}
+
 	public void solve() {
 
 		todoProps = reader.getSpec().getProperties().stream().map(p -> p.getName()).collect(Collectors.toSet());
-		ITSInterpreter interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps,
-				4096);
-		Thread runnerThread = new Thread(new ITSRealRunner(interp.getPout(), cl));
+		Thread runnerThread = new Thread(new ITSRealRunner(listener.getPout(), cl));
 
-		FutureTask<Boolean> ft = new FutureTask<>(interp);
+		FutureTask<Boolean> ft = new FutureTask<>(listener);
 
 		try {
 			new Thread(ft).start();
-
 			runnerThread.start();
-
 			runnerThread.join();
 
 		} catch (InterruptedException e) {
 			try {
 				runnerThread.interrupt();
 			} catch (Exception ee) {
-				System.out.println("na pas pu interrpute");
+				System.out.println("na pas pu etre interrpute");
 			}
 		} catch (Exception e1) {
 			e1.printStackTrace();
 		} finally {
 			try {
 				done = ft.get();
 			} catch (InterruptedException | ExecutionException e) {
-				e.printStackTrace();
+			}finally{
+				if (!ft.isDone())
+					ft.cancel(true);
 			}
 
 		}
 		System.out.println("ITS RUNNER FINISH !");
 	}
 
-	public Boolean taskDone() {
-		if (done) {
-			System.out.println("tasks resolved Its");
-			return true;
-		}
-		System.out.println("tasks not all resolved Its");
-		return false;
-
-	}
-
 }

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java

@@ -10,6 +10,7 @@
 import org.eclipse.emf.common.util.TreeIterator;
 import org.eclipse.emf.ecore.EObject;
 
+import Interpreter.LTSminInterpreter;
 import fr.lip6.move.gal.Comparison;
 import fr.lip6.move.gal.InvariantProp;
 import fr.lip6.move.gal.LTLNext;
@@ -57,7 +58,24 @@ private static boolean isStutterInvariant(Property prop) {
 		}
 		return true;
 	}
+
+	public void setInterpreter() {
+
+	}
+
+	public Boolean taskDone() {
+		todo.removeAll(doneProps);
+		if(todo.isEmpty())
+			System.out.println("Ltsmin has all solved");
+		else
+			System.out.println("Ltsmin didnt solve everything");
+		return (todo.isEmpty()) ? true : false;
+	}
 
+	public void generateListener() {
+		setListener(new LTSminInterpreter());
+	}	
+
 	public void solve() {
 		try {
 			System.out.println("Built C files in : \n" + new File(workFolder + "/"));
@@ -213,13 +231,5 @@ public void solve() {
 
 	}
 
-	public Boolean taskDone() {
-		todo.removeAll(doneProps);
-		if(todo.isEmpty())
-			System.out.println("Ltsmin has all solved");
-		else
-			System.out.println("Ltsmin didnt solve everything");
-		return (todo.isEmpty()) ? true : false;
-	}
 
 }

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java

@@ -27,7 +27,24 @@ public Logger getLog() {
 		return Logger.getLogger("fr.lip6.move.gal");
 
 	}
+
+	public void setInterpreter() {
+	}
+
+	public Boolean taskDone() {
+		// test for and handle properties
+		if (nbsolve == satresult.size()) {
+			getLog().info("SMT solved all " + nbsolve + " properties. Interrupting other analysis methods.");
+			System.out.println("tasks resolved Smt");
+			return true;
+		} else {
+			getLog().info("SMT solved " + nbsolve + "/ " + satresult.size() + " properties.");
+		}
+		System.out.println("tasks not all resolved Smt");
+		return false;
 
+	}
+
 	public void solve() {
 		Gal2SMTFrontEnd gsf = new Gal2SMTFrontEnd(solverPath, solver);
 		gsf.addObserver(new ISMTObserver() {
@@ -63,17 +80,4 @@ public synchronized void notifyResult(Property prop, Result res, String desc) {
 		System.out.println("SMT HAS COMPLETELY FINISHED");
 	}
 
-	public Boolean taskDone() {
-		// test for and handle properties
-		if (nbsolve == satresult.size()) {
-			getLog().info("SMT solved all " + nbsolve + " properties. Interrupting other analysis methods.");
-			System.out.println("tasks resolved Smt");
-			return true;
-		} else {
-			getLog().info("SMT solved " + nbsolve + "/ " + satresult.size() + " properties.");
-		}
-		System.out.println("tasks not all resolved Smt");
-		return false;
-
-	}
 }