portfolio concurrent

.travis.yml

@@ -18,12 +18,6 @@ script :
  - zip -d fr.lip6.move.gal.itscl.product-macosx.cocoa.x86_64.zip '*its-*-win64' '*its-*-linux32' '*its-*-linux64'
  - zip -d fr.lip6.move.gal.itscl.product-win32.win32.x86_64.zip '*its-*-linux64' '*its-*-linux32' '*its-*-Darwin'
  - cd ..
- - ./install_eclipse.sh 
- - cd eclipse/plugins/fr.lip6.move.gal.itstools.binaries_1.0.0.*/bin/
- - \rm *Darwin* *linux32* *win64*
- - cd -
- - tar czf itscl_linux.tgz eclipse/ runeclipse.sh
- - mv itscl_linux.tgz website/
  - ls -lah website/
 
 deploy:
@@ -34,6 +28,4 @@ deploy:
   on:
     branch: master
 
-after_deploy:
-  - curl -s -X POST -H "Content-Type:application/json" -H "Accept:application/json"   -H "Travis-API-Version:3" -H "Authorization:token $APITOKEN" -d '{"request":{"message":"Triggered by ITS Tools build.","branch":"master"}}' https://api.travis-ci.org/repo/yanntm%2FITS-Tools-pnmcc/requests
-
+

fr.lip6.move.gal.itscl.application/.classpath

@@ -2,6 +2,7 @@
 <classpath>
 	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
 	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
-	<classpathentry kind="src" path="src/"/>
+	<classpathentry kind="src" path="src"/>
+	<classpathentry kind="lib" path="/local/akheireddine/eclipses/eclipse/plugins/ch.qos.logback.classic_1.0.7.v20121108-1250.jar"/>
 	<classpathentry kind="output" path="target/classes"/>
 </classpath>

fr.lip6.move.gal.itscl.application/META-INF/MANIFEST.MF

@@ -7,6 +7,6 @@ Require-Bundle: org.eclipse.core.runtime,
  fr.lip6.move.gal,
  fr.lip6.move.gal.itstools.binaries,
  org.antlr.runtime;bundle-version="[3.2.0,3.3.0]",
- fr.lip6.move.gal.application.pnmcc;bundle-version="1.0.0"
+ fr.lip6.move.gal.itscl.concurrent;bundle-version="1.0.0"
 Bundle-RequiredExecutionEnvironment: JavaSE-1.8
 Bundle-Vendor: UPMC/CNRS, LIP6

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

@@ -1,10 +1,13 @@
 package fr.lip6.move.gal.itscl.application;
 
+
 import java.io.File;
 import java.io.IOException;
 import java.util.ArrayList;
-import java.util.Arrays;
 import java.util.List;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
+import java.util.concurrent.FutureTask;
 
 import org.eclipse.equinox.app.IApplication;
 import org.eclipse.equinox.app.IApplicationContext;
@@ -15,9 +18,10 @@
 import fr.lip6.move.gal.SafetyProp;
 import fr.lip6.move.gal.Specification;
 import fr.lip6.move.gal.instantiate.GALRewriter;
+import fr.lip6.move.gal.itscl.interpreter.InterpreteObservable;
+import fr.lip6.move.gal.itscl.modele.SolverObservable;
 import fr.lip6.move.gal.itstools.CommandLine;
 import fr.lip6.move.gal.itstools.CommandLineBuilder;
-import fr.lip6.move.gal.itstools.Runner;
 import fr.lip6.move.gal.itstools.BinaryToolsPlugin.Tool;
 import fr.lip6.move.serialization.SerializationUtil;
 
@@ -28,28 +32,32 @@ public class Application implements IApplication {
 	private static final String REACH_EXAM = "-reach";
 	private static final String CTL_EXAM = "-ctl";
 	private static final String LTL_EXAM = "-ltl";
-
-	/* (non-Javadoc)
-	 * @see org.eclipse.equinox.app.IApplication#start(org.eclipse.equinox.app.IApplicationContext)
+
+	private ExecutorService exec;
+
+	/*
+	 * (non-Javadoc)
+	 * 
+	 * @see org.eclipse.equinox.app.IApplication#start(org.eclipse.equinox.app.
+	 * IApplicationContext)
 	 */
+	@Override
 	public Object start(IApplicationContext context) throws Exception {
-
-		String [] args = (String[]) context.getArguments().get(APPARGS);
-
-		if (Arrays.asList(args).contains("-pnfolder")) {
-			return new fr.lip6.move.gal.application.Application().start(context);
-		}
+
+		String[] args = (String[]) context.getArguments().get(APPARGS);
+
 		String inputff = null;
+		@SuppressWarnings("unused")
 		String inputType = null;
-		
+
 		Tool tool = Tool.reach;
 		boolean doIts = false;
-		
-		for (int i=0; i < args.length ; i++) {
+
+		for (int i = 0; i < args.length; i++) {
 			if (INPUT_FILE.equals(args[i])) {
 				inputff = args[++i];
 			} else if (INPUT_TYPE.equals(args[i])) {
-				inputType = args[++i]; 
+				inputType = args[++i];
 			} else if (REACH_EXAM.equals(args[i])) {
 				tool = Tool.reach;
 				doIts = true;
@@ -59,88 +67,141 @@ public Object start(IApplicationContext context) throws Exception {
 			} else if (LTL_EXAM.equals(args[i])) {
 				tool = Tool.ltl;
 				doIts = true;
-//			} else if (LTSMINPATH.equals(args[i])) {
-//				ltsminpath = args[++i];
-//				doLTSmin = true;
-//			} else if (ITS.equals(args[i])) {
-//				doITS = true;
-//			} else if (disablePOR.equals(args[i])) {
-//				doPOR = false;
-//			} else if (ONLYGAL.equals(args[i])) {
-//				onlyGal = true;
+				// } else if (LTSMINPATH.equals(args[i])) {
+				// ltsminpath = args[++i];
+				// doLTSmin = true;
+				// } else if (ITS.equals(args[i])) {
+				// doITS = true;
+				// } else if (disablePOR.equals(args[i])) {
+				// doPOR = false;
+				// } else if (ONLYGAL.equals(args[i])) {
+				// onlyGal = true;
 			}
 		}
-		
+
 		if (inputff == null) {
 			System.err.println("Please provide input file with -i option");
 			return null;
 		}
-
+
+		if (!doIts) {
+			System.err.println("Please provide tool (ex: reach, ctl, ltl...)");
+		}
+
 		File ff = new File(inputff);
-		if (! ff.exists()) {
-			System.err.println("Input file "+inputff +" does not exist");
+		if (!ff.exists()) {
+			System.err.println("Input file " + inputff + " does not exist");
 			return null;
 		}
+
 		String pwd = ff.getParent();
 		String modelName = ff.getName().replace(".gal", "");
 		SerializationUtil.setStandalone(true);
-
+
+		// parse l'entrée
 		long time = System.currentTimeMillis();
-		Specification spec = SerializationUtil.fileToGalSystem(inputff);		
-		System.out.println("Successfully read input file : " + inputff +" in " + (time - System.currentTimeMillis()) + " ms.");
+		Specification spec = SerializationUtil.fileToGalSystem(inputff);
+		System.out.println(
+				"Successfully read input file : " + inputff + " in " + (time - System.currentTimeMillis()) + " ms.");
+
+		time = System.currentTimeMillis();
+		ProblemSS p = loadModel(pwd, spec, tool);
+		System.out.println("Simplifications done in " + (time - System.currentTimeMillis()) + " ms.");
+
+		time = System.currentTimeMillis();
+		CommandLine cl = getCmdLine(spec, p.getFolder(), modelName, tool);
+		System.out.println("Built GAL and property files in " + (time - System.currentTimeMillis()) + " ms.");
+		SolverObservable superRunner = new SolverObservable();
+		exec = Executors.newSingleThreadExecutor();
+		InterpreteObservable interpRunner = new InterpreteObservable(superRunner);
+		SolverSeq s = new SolverSeq(p, cl);
+
+		superRunner.attach(s);
+		// run les solvers
+		FutureTask<Boolean> executeRunner = new FutureTask<>(superRunner);
+		Thread futureTh = new Thread(executeRunner);
+		FutureTask<Boolean> executeInterp = new FutureTask<>(interpRunner);
+		Thread futureTh2 = new Thread(executeInterp);
 
+		futureTh.start();
+		futureTh2.start();
+
+		Boolean result = executeRunner.get();
+		Boolean result2 = executeInterp.get();
+
+		if (futureTh != null)
+			futureTh.join();
+		if (futureTh2 != null)
+			futureTh2.join();
+		System.out.println("Operation reussi ? " + result + ". And Interpreter ? "+result2);
+		return IApplication.EXIT_OK;
+	}
+
+	// Traitement du problème : transformations + simplifications
+	public ProblemSS loadModel(String pwd, Specification spec, Tool tool) throws IOException {
+
 		String cwd = pwd + "/work";
 		File fcwd = new File(cwd);
-		if (! fcwd.exists()) {
-			if (! fcwd.mkdir()) {
-				System.err.println("Could not set up work folder in "+cwd);
+		if (!fcwd.exists()) {
+			if (!fcwd.mkdir()) {
+				System.err.println("Could not set up work folder in " + cwd);
 			}
-		}				
-
-		time = System.currentTimeMillis();
+		}
 		GALRewriter.flatten(spec, true);
-		System.out.println("Simplifications done in " + (time - System.currentTimeMillis()) + " ms.");
-
-		time = System.currentTimeMillis();
-		String outpath = cwd+"/"+ modelName + ".gal";
+		ProblemSS p = new ProblemSS(tool, cwd);
+		p.configure(spec, 35000);
+
+		return p;
+	}
+
+	/**
+	 * // On produit un fichier de modèle pour l'outil ligne de commande
+	 * @param spec
+	 * @param cwd
+	 * @param modelName
+	 * @param tool
+	 * @return
+	 * @throws IOException
+	 */
+	public CommandLine getCmdLine(Specification spec, String cwd, String modelName, Tool tool) throws IOException {
+
+		String outpath = cwd + "/" + modelName + ".gal";
 		outputGalFile(spec, outpath);
-		
+
 		CommandLine cl = buildCommandLine(outpath, tool);
-		
+
 		if (tool == Tool.reach) {
-			spec.getProperties().removeIf( (p) -> ! (p.getBody() instanceof SafetyProp) );
-			String proppath = cwd + "/" +modelName  +".prop";
+			spec.getProperties().removeIf((p) -> !(p.getBody() instanceof SafetyProp));
+			String proppath = cwd + "/" + modelName + ".prop";
 			SerializationUtil.serializePropertiesForITSTools(outpath, spec.getProperties(), proppath);
 			cl.addArg("-reachable-file");
 			cl.addArg(proppath);
 			// cl.addArg("--stats");
 		} else if (tool == Tool.ctl) {
-			spec.getProperties().removeIf( (p) -> ! (p.getBody() instanceof CTLProp) );
-			String proppath = cwd + "/" +modelName  +".ctl";
+			spec.getProperties().removeIf((p) -> !(p.getBody() instanceof CTLProp));
+			String proppath = cwd + "/" + modelName + ".ctl";
 			SerializationUtil.serializePropertiesForITSCTLTools(outpath, spec.getProperties(), proppath);
 			cl.addArg("-ctl");
 			cl.addArg(proppath);
 		} else if (tool == Tool.ltl) {
-			spec.getProperties().removeIf( (p) -> ! (p.getBody() instanceof LTLProp) );
-			String proppath = cwd + "/" +modelName  +".ltl";
+			spec.getProperties().removeIf((p) -> !(p.getBody() instanceof LTLProp));
+			String proppath = cwd + "/" + modelName + ".ltl";
 			SerializationUtil.serializePropertiesForITSLTLTools(outpath, spec.getProperties(), proppath);
 			cl.addArg("-LTL");
-			cl.addArg(proppath);	
+			cl.addArg(proppath);
 			cl.addArg("-c");
 			cl.addArg("-stutter-deadlock");
 		}
 		if (cl != null) {
 			cl.setWorkingDir(new File(cwd));
 		}
-		System.out.println("Built GAL and proeprty files in "+ (time - System.currentTimeMillis()) + " ms.");
-
-		Runner.runTool(3500, cl, System.out, true);
-
-		return IApplication.EXIT_OK;
+
+		return cl;
+
 	}
-	
+
 	public void outputGalFile(Specification spec, String outpath) throws IOException {
-		if (! spec.getProperties().isEmpty()) {
+		if (!spec.getProperties().isEmpty()) {
 			List<Property> props = new ArrayList<Property>(spec.getProperties());
 			spec.getProperties().clear();
 			SerializationUtil.systemToFile(spec, outpath);
@@ -149,17 +210,18 @@ public void outputGalFile(Specification spec, String outpath) throws IOException
 			SerializationUtil.systemToFile(spec, outpath);
 		}
 	}
-	
+
 	private CommandLine buildCommandLine(String modelff, Tool tool) throws IOException {
 		CommandLineBuilder cl = new CommandLineBuilder(tool);
 		cl.setModelFile(modelff);
 		cl.setModelType("CGAL");
 		return cl.getCommandLine();
 	}
-
-	/* (non-Javadoc)
-	 * @see org.eclipse.equinox.app.IApplication#stop()
-	 */
+
 	public void stop() {
+		exec.shutdown();
+		if (!exec.isShutdown())
+			System.out.println("Problem to shutdown executor of runners");
 	}
+
 }

fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/InterpreterApp.java

@@ -0,0 +1,28 @@
+package fr.lip6.move.gal.itscl.application;
+
+
+import fr.lip6.move.gal.itscl.interpreter.AbstractInterpreter;
+import fr.lip6.move.gal.itscl.interpreter.InterpreteBytArray;
+
+public class InterpreterApp extends AbstractInterpreter {
+
+	private InterpreteBytArray bufferWIO;
+	private SolverSeq sq;
+
+	public InterpreterApp(InterpreteBytArray buff, SolverSeq sq) {
+		this.bufferWIO = buff;
+		this.sq = sq;
+	}
+
+	public void run() {
+		String output = bufferWIO.getPout().toString();
+
+		if (output.contains("Error"))
+			sq.setResult();
+		else
+			System.out.println("  "+output);
+
+		releaseResult();
+	}
+
+}

fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/ItsSolver.java

@@ -0,0 +1,30 @@
+package fr.lip6.move.gal.itscl.application;
+
+import fr.lip6.move.gal.itscl.interpreter.IInterpreteObservable;
+import fr.lip6.move.gal.itscl.modele.ISolverSeq;
+import fr.lip6.move.gal.itstools.CommandLine;
+
+public abstract class ItsSolver implements ISolverSeq {
+
+	private final CommandLine cl;
+	protected final ProblemSS p;
+	protected IInterpreteObservable inRunner;
+
+	public ItsSolver(ProblemSS p, CommandLine cl) {
+		this.cl = cl;
+		this.p = p;
+	}
+
+	public CommandLine getCmd() {
+		return cl;
+	}
+
+	public ProblemSS getProblem() {
+		return p;
+	}
+
+	public void configureInterpreter(IInterpreteObservable interp){
+		this.inRunner=interp;
+	}
+
+}