diff --git a/.travis.yml b/.travis.yml index 2dfdc09..be55fdf 100644 --- a/.travis.yml +++ b/.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 - + diff --git a/fr.lip6.move.gal.itscl.application/.classpath b/fr.lip6.move.gal.itscl.application/.classpath index cf36b56..6133948 100644 --- a/fr.lip6.move.gal.itscl.application/.classpath +++ b/fr.lip6.move.gal.itscl.application/.classpath @@ -2,6 +2,7 @@ - + + diff --git a/fr.lip6.move.gal.itscl.application/META-INF/MANIFEST.MF b/fr.lip6.move.gal.itscl.application/META-INF/MANIFEST.MF index 6c4ce7e..47c1689 100644 --- a/fr.lip6.move.gal.itscl.application/META-INF/MANIFEST.MF +++ b/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 diff --git a/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/Application.java b/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/Application.java index 8638e43..213ffb4 100644 --- a/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/Application.java +++ b/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 executeRunner = new FutureTask<>(superRunner); + Thread futureTh = new Thread(executeRunner); + FutureTask 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 props = new ArrayList(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"); } + } diff --git a/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/InterpreterApp.java b/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/InterpreterApp.java new file mode 100644 index 0000000..8c49d0f --- /dev/null +++ b/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(); + } + +} diff --git a/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/ItsSolver.java b/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/ItsSolver.java new file mode 100644 index 0000000..e07a0c3 --- /dev/null +++ b/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; + } + +} diff --git a/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/ProblemSS.java b/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/ProblemSS.java new file mode 100644 index 0000000..b6d62a0 --- /dev/null +++ b/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/ProblemSS.java @@ -0,0 +1,38 @@ +package fr.lip6.move.gal.itscl.application; + +import fr.lip6.move.gal.Specification; +import fr.lip6.move.gal.itstools.BinaryToolsPlugin.Tool; + +public class ProblemSS{ + + private Tool tool; + private String folder; + private int timeout; + @SuppressWarnings("unused") + private Specification spec; + + public ProblemSS(Tool tool, String folder) { + this.tool = tool; + this.folder = folder; + } + + public void configure(Specification spec, int timeout) { + this.spec = spec; + this.timeout = timeout; + } + + public Tool getTool() { + return tool; + } + + public String getFolder() { + return folder; + } + + public int getTimeout() { + return timeout; + } + + + +} \ No newline at end of file diff --git a/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/SolverSeq.java b/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/SolverSeq.java new file mode 100644 index 0000000..5d2b9b4 --- /dev/null +++ b/fr.lip6.move.gal.itscl.application/src/fr/lip6/move/gal/itscl/application/SolverSeq.java @@ -0,0 +1,55 @@ +package fr.lip6.move.gal.itscl.application; + +import java.io.IOException; + +import org.eclipse.core.runtime.IStatus; + +import fr.lip6.move.gal.itscl.interpreter.InterpreteBytArray; +import fr.lip6.move.gal.itstools.CommandLine; +import fr.lip6.move.gal.itstools.ProcessController.TimeOutException; +import fr.lip6.move.gal.itstools.Runner; + +public class SolverSeq extends ItsSolver { + + private InterpreteBytArray bufferWIO = new InterpreteBytArray(); + private Boolean complete = true; + private InterpreterApp interp; + + public SolverSeq(ProblemSS p, CommandLine cl) { + super(p, cl); + } + + public void setResult() { + this.complete =false; + } + + public int hasComplete() { + interp.acquireResult(); + return complete?0:1; + } + + public Integer call() { + + try { + IStatus status; + interp = new InterpreterApp(bufferWIO,this); + Thread interpTh = new Thread(interp, "InterpreterApp"); + inRunner.addThInterprete(interpTh); + interpTh.start(); + status = Runner.runTool(p.getTimeout(), getCmd(), bufferWIO.getPout(), true); + + + if (!status.isOK() && status.getCode() != 1) { + throw new RuntimeException( + "Unexpected exception when executing commandline :" + getCmd() + "\n" + status); + } + return hasComplete(); + + } catch (IOException | TimeOutException e) { + e.printStackTrace(); + return -1; + } + + } + +} diff --git a/fr.lip6.move.gal.itscl.application/test/.gitignore b/fr.lip6.move.gal.itscl.application/test/.gitignore new file mode 100644 index 0000000..76b5fe4 --- /dev/null +++ b/fr.lip6.move.gal.itscl.application/test/.gitignore @@ -0,0 +1 @@ +/work/ diff --git a/fr.lip6.move.gal.itscl.application/test/model.gal b/fr.lip6.move.gal.itscl.application/test/model.gal new file mode 100644 index 0000000..f80f851 --- /dev/null +++ b/fr.lip6.move.gal.itscl.application/test/model.gal @@ -0,0 +1,100 @@ + +gal bridge($fastest=5, $fast=10, $slow=20, $slowest=25){ + typedef Torchid_t= 0..0 ; + typedef Soldierid_t= 0..3 ; + int glob_range_L = 0; + int glob_clock_time = 0; + /**Torch states [ 0=one, 1=S0, 2=free, 3=tw] */ + array [1]Torch_state = (2 ); + /**Soldier states [ 0=S0, 1=safe, 2=S1, 3=unsaf] */ + array [4]Soldier_state = (3, 3, 3, 3 ); + array [4]Soldier_delay = ($fastest, $fast, $slow, $slowest ); + array [4]Soldier_clock_y = (0, 0, 0, 0 ); + /** To represent channel take */ + transition chantake [ true ] { + self."Sendtake"; + self."Recvtake"; + } + /** To represent channel release */ + transition chanrelease [ true ] { + self."Sendrelease"; + self."Recvrelease"; + } + transition elapse [ true ] { + for ($Torchid : Torchid_t) { + self."passUrgentTorch"( $Torchid ); + } + for ($Soldierid : Soldierid_t) { + self."updateClockSoldiery"( $Soldierid ); + } + } + /** State one is not urgent. */ + transition passUrgentTorch_one(Torchid_t $Torchid) [ Torch_state[ $Torchid ] == 0 ] label "passUrgentTorch" ($Torchid){ + } + /** State free is not urgent. */ + transition passUrgentTorch_free(Torchid_t $Torchid) [ Torch_state[ $Torchid ] == 2 ] label "passUrgentTorch" ($Torchid){ + } + /** State two is not urgent. */ + transition passUrgentTorch_two(Torchid_t $Torchid) [ Torch_state[ $Torchid ] == 3 ] label "passUrgentTorch" ($Torchid){ + } + transition t1Torchfree_S0(Torchid_t $Torchid) [ Torch_state[ $Torchid ] == 2 ] label "Recvtake" { + Torch_state[ $Torchid ] = 1 ; + } + transition t2TorchS0_one(Torchid_t $Torchid) [ Torch_state[ $Torchid ] == 1 ] { + Torch_state[ $Torchid ] = 0 ; + } + transition t3TorchS0_two(Torchid_t $Torchid) [ Torch_state[ $Torchid ] == 1 ] label "Recvtake" { + Torch_state[ $Torchid ] = 3 ; + } + transition t4Torchone_free(Torchid_t $Torchid) [ Torch_state[ $Torchid ] == 0 ] label "Recvrelease" { + Torch_state[ $Torchid ] = 2 ; + glob_range_L = ( 1 - glob_range_L ) ; + } + transition t5Torchtwo_one(Torchid_t $Torchid) [ Torch_state[ $Torchid ] == 3 ] label "Recvrelease" { + Torch_state[ $Torchid ] = 0 ; + } + /** State S0 has a max tracking value. */ + transition updateClockSoldiery_S0(Soldierid_t $Soldierid) [ Soldier_state[ $Soldierid ] == 0 ] label "updateClockSoldiery" ($Soldierid){ + if (!Soldier_clock_y[ $Soldierid ] >= Soldier_delay[ $Soldierid ]) { + Soldier_clock_y[ $Soldierid ] += 1 ; + } + } + /** State Soldier safe is inactive. */ + transition updateClockSoldiery_safe(Soldierid_t $Soldierid) [ Soldier_state[ $Soldierid ] == 1 ] label "updateClockSoldiery" ($Soldierid){ + } + /** State S1 has a max tracking value. */ + transition updateClockSoldiery_S1(Soldierid_t $Soldierid) [ Soldier_state[ $Soldierid ] == 2 ] label "updateClockSoldiery" ($Soldierid){ + if (!Soldier_clock_y[ $Soldierid ] >= Soldier_delay[ $Soldierid ]) { + Soldier_clock_y[ $Soldierid ] += 1 ; + } + } + /** State Soldier unsafe is inactive. */ + transition updateClockSoldiery_unsafe(Soldierid_t $Soldierid) [ Soldier_state[ $Soldierid ] == 3 ] label "updateClockSoldiery" ($Soldierid){ + } + transition t1SoldierS0_safe(Soldierid_t $Soldierid) [ Soldier_state[ $Soldierid ] == 0 && Soldier_clock_y[ $Soldierid ] >= Soldier_delay[ $Soldierid ] ] label "Sendrelease" { + Soldier_state[ $Soldierid ] = 1 ; + Soldier_clock_y[ $Soldierid ] = 0 ; + } + transition t2Soldiersafe_S1(Soldierid_t $Soldierid) [ Soldier_state[ $Soldierid ] == 1 && glob_range_L == 1 ] label "Sendtake" { + Soldier_state[ $Soldierid ] = 2 ; + Soldier_clock_y[ $Soldierid ] = 0 ; + } + transition t3SoldierS1_unsafe(Soldierid_t $Soldierid) [ Soldier_state[ $Soldierid ] == 2 && Soldier_clock_y[ $Soldierid ] >= Soldier_delay[ $Soldierid ] ] label "Sendrelease" { + Soldier_state[ $Soldierid ] = 3 ; + Soldier_clock_y[ $Soldierid ] = 0 ; + } + transition t4Soldierunsafe_S0(Soldierid_t $Soldierid) [ Soldier_state[ $Soldierid ] == 3 && glob_range_L == 0 ] label "Sendtake" { + Soldier_state[ $Soldierid ] = 0 ; + Soldier_clock_y[ $Soldierid ] = 0 ; + } +} + + +property safe [reachable] : +<<<<<<< HEAD + Soldier_state[0]==1 && Soldier_state[1]==1 && Soldier_state[2]==1 && Soldier_state[3]==1; +======= + Soldier_state[0]==1 && Soldier_state[1]==1 && Soldier_state[2]==1 && Soldier_state[3]==1 +; +>>>>>>> refs/heads/test + diff --git a/fr.lip6.move.gal.itscl.concurrent/.classpath b/fr.lip6.move.gal.itscl.concurrent/.classpath new file mode 100644 index 0000000..eca7bdb --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/.classpath @@ -0,0 +1,7 @@ + + + + + + + diff --git a/fr.lip6.move.gal.itscl.concurrent/.gitignore b/fr.lip6.move.gal.itscl.concurrent/.gitignore new file mode 100644 index 0000000..b83d222 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/.gitignore @@ -0,0 +1 @@ +/target/ diff --git a/fr.lip6.move.gal.itscl.concurrent/.project b/fr.lip6.move.gal.itscl.concurrent/.project new file mode 100644 index 0000000..e7f36dc --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/.project @@ -0,0 +1,28 @@ + + + fr.lip6.move.gal.itscl.concurrent + + + + + + org.eclipse.jdt.core.javabuilder + + + + + org.eclipse.pde.ManifestBuilder + + + + + org.eclipse.pde.SchemaBuilder + + + + + + org.eclipse.pde.PluginNature + org.eclipse.jdt.core.javanature + + diff --git a/fr.lip6.move.gal.itscl.concurrent/.settings/org.eclipse.jdt.core.prefs b/fr.lip6.move.gal.itscl.concurrent/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 0000000..0c68a61 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,7 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.source=1.8 diff --git a/fr.lip6.move.gal.itscl.concurrent/META-INF/MANIFEST.MF b/fr.lip6.move.gal.itscl.concurrent/META-INF/MANIFEST.MF new file mode 100644 index 0000000..0ae9df8 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/META-INF/MANIFEST.MF @@ -0,0 +1,11 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: Concurrent Support for Portfolio +Bundle-SymbolicName: fr.lip6.move.gal.itscl.concurrent +Bundle-RequiredExecutionEnvironment: JavaSE-1.8 +Bundle-Vendor: LIP6 +Export-Package: fr.lip6.move.gal.itscl.adaptor, + fr.lip6.move.gal.itscl.interpreter, + fr.lip6.move.gal.itscl.modele +Bundle-Version: 1.0.0.qualifier +Require-Bundle: fr.lip6.move.gal;bundle-version="1.0.0" diff --git a/fr.lip6.move.gal.itscl.concurrent/bin/.gitignore b/fr.lip6.move.gal.itscl.concurrent/bin/.gitignore new file mode 100644 index 0000000..44fde90 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/bin/.gitignore @@ -0,0 +1 @@ +/fr/ diff --git a/fr.lip6.move.gal.itscl.concurrent/build.properties b/fr.lip6.move.gal.itscl.concurrent/build.properties new file mode 100644 index 0000000..5b359b5 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/build.properties @@ -0,0 +1,4 @@ +source.. = src/ +output.. = bin/ +bin.includes = META-INF/,\ + . \ No newline at end of file diff --git a/fr.lip6.move.gal.itscl.concurrent/pom.xml b/fr.lip6.move.gal.itscl.concurrent/pom.xml new file mode 100644 index 0000000..3dfa55b --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/pom.xml @@ -0,0 +1,16 @@ + + 4.0.0 + + + fr.lip6.move.gal + fr.lip6.move.gal.parent + 1.0.0-SNAPSHOT + ../fr.lip6.move.gal.parent/pom.xml + + + fr.lip6.move.gal.itscl.concurrent + eclipse-plugin + Extensions :: Concurent Features for Portfolio + Portfolio support classes and interfaces. + + \ No newline at end of file diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/Adapter.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/Adapter.java new file mode 100644 index 0000000..1d8f0f6 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/Adapter.java @@ -0,0 +1,24 @@ +package fr.lip6.move.gal.itscl.adaptor; + +import fr.lip6.move.gal.itscl.modele.IRunner; +import fr.lip6.move.gal.itscl.modele.ISolverSeq; + +public class Adapter implements ISolverSeq { + + protected IRunner runner; + + public Adapter(IRunner r) { + this.runner = r; + } + + public int hasComplete() { + return runner.taskDone() ? 0 : 1; + } + + public Integer call() throws Exception { + runner.solve(); + return hasComplete(); + + } + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterApplication.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterApplication.java new file mode 100644 index 0000000..8c6e602 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterApplication.java @@ -0,0 +1,12 @@ +package fr.lip6.move.gal.itscl.adaptor; + +import fr.lip6.move.gal.itscl.modele.IRunner; +import fr.lip6.move.gal.itscl.modele.ISolverSeq; + +public class AdapterApplication { + + public static ISolverSeq add(IRunner r) { + return new Adapter(r); + } + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterCegar.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterCegar.java new file mode 100644 index 0000000..81d5594 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterCegar.java @@ -0,0 +1,10 @@ +package fr.lip6.move.gal.itscl.adaptor; + +import fr.lip6.move.gal.itscl.modele.IRunner; + +public class AdapterCegar extends Adapter { + + public AdapterCegar(IRunner ceg) { + super(ceg); + } +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterITS.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterITS.java new file mode 100644 index 0000000..b6a095c --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterITS.java @@ -0,0 +1,11 @@ +package fr.lip6.move.gal.itscl.adaptor; + +import fr.lip6.move.gal.itscl.modele.IRunner; + +public class AdapterITS extends Adapter { + + public AdapterITS(IRunner its) { + super(its); + } + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterLTSmin.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterLTSmin.java new file mode 100644 index 0000000..2e3491d --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterLTSmin.java @@ -0,0 +1,12 @@ +package fr.lip6.move.gal.itscl.adaptor; + +import fr.lip6.move.gal.itscl.modele.IRunner; + +public class AdapterLTSmin extends Adapter { + + public AdapterLTSmin(IRunner lts) { + + super(lts); + } + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterSMTR.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterSMTR.java new file mode 100644 index 0000000..ea3f094 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/adaptor/AdapterSMTR.java @@ -0,0 +1,11 @@ +package fr.lip6.move.gal.itscl.adaptor; + +import fr.lip6.move.gal.itscl.modele.IRunner; + +public class AdapterSMTR extends Adapter { + + public AdapterSMTR(IRunner smt) { + super(smt); + } + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/AbstractInterpreter.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/AbstractInterpreter.java new file mode 100644 index 0000000..f9c557e --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/AbstractInterpreter.java @@ -0,0 +1,27 @@ +package fr.lip6.move.gal.itscl.interpreter; + +import java.util.concurrent.Semaphore; + +public abstract class AbstractInterpreter implements Runnable { + + private Semaphore hasComplete = new Semaphore(0); + + /** + * Block until interpreter of the specific runner complete + */ + public void acquireResult() { + try { + hasComplete.acquire(); + } catch (InterruptedException e) { + e.printStackTrace(); + } + } + + /** + * notify its runner that I finish the last interpretation + */ + public void releaseResult() { + hasComplete.release(); + } + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/FileStreamInterprete.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/FileStreamInterprete.java new file mode 100644 index 0000000..66c26cb --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/FileStreamInterprete.java @@ -0,0 +1,64 @@ +package fr.lip6.move.gal.itscl.interpreter; + +import java.io.BufferedReader; +import java.io.IOException; +import java.io.InputStreamReader; +import java.io.PipedInputStream; +import java.io.PipedOutputStream; + +/** + * Interpreters that uses File I/O stream + */ +public class FileStreamInterprete { + + private final PipedInputStream pin; + + private PipedOutputStream pout = null; + private BufferedReader in; + + public FileStreamInterprete() { + + this.pin = new PipedInputStream(4096); + + try { + this.pout = new PipedOutputStream(pin); + } catch (IOException e1) { + e1.printStackTrace(); + System.out.println("error pipou"); + } + this.in = new BufferedReader(new InputStreamReader(pin)); + + } + + public PipedOutputStream getPout() { + return pout; + } + + public PipedInputStream getPin() { + return pin; + } + + public void closePinPout() { + try { + pin.close(); + pout.close(); + } catch (IOException e) { + System.out.println("Problemo uno fermento dilistener"); + e.printStackTrace(); + } + } + + public String getWrittenData() { + try { + return in.readLine(); + } catch (IOException e) { + e.printStackTrace(); + } + return null; + } + + public void closeIn() throws IOException { + in.close(); + } + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/IInterpreteObservable.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/IInterpreteObservable.java new file mode 100644 index 0000000..c73107d --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/IInterpreteObservable.java @@ -0,0 +1,9 @@ +package fr.lip6.move.gal.itscl.interpreter; + +import java.util.concurrent.Callable; + + +public interface IInterpreteObservable extends Callable { + public void addThInterprete(Thread o); + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/InterpreteBytArray.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/InterpreteBytArray.java new file mode 100644 index 0000000..0ddbf82 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/InterpreteBytArray.java @@ -0,0 +1,25 @@ +package fr.lip6.move.gal.itscl.interpreter; + +import java.io.ByteArrayOutputStream; + + +/** + * Interpreters that use ByteArray I/O stream + */ +public class InterpreteBytArray { + + ByteArrayOutputStream pout; + + public InterpreteBytArray() { + pout = new ByteArrayOutputStream(); + } + + public String getWrittenData() { + return pout.toString(); + } + + public ByteArrayOutputStream getPout() { + return pout; + } + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/InterpreteObservable.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/InterpreteObservable.java new file mode 100644 index 0000000..82e6cfc --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/interpreter/InterpreteObservable.java @@ -0,0 +1,48 @@ +package fr.lip6.move.gal.itscl.interpreter; + +import java.util.ArrayList; + +import fr.lip6.move.gal.itscl.modele.ISolverObservable; + +public class InterpreteObservable implements IInterpreteObservable { + + private ArrayList interpTh = new ArrayList(); + private ISolverObservable so; + + public InterpreteObservable(ISolverObservable so) { + this.so = so; + } + + public void addThInterprete(Thread interpTh) { + this.interpTh.add(interpTh); + } + + /** + * Join all interpreters in the list to ensure they complete well. + */ + public Boolean call() { + try { + // waits SolverObservable to acquire a result from a solver OR no + // one did + so.waitSolver(); + + for (int i = 0; i < interpTh.size(); i++) { + Thread th = interpTh.get(i); + if (!th.isInterrupted()) { + th.join(); + System.out.println("Name threads : " + th.getName()); + + } + } + } catch (InterruptedException e) { + e.printStackTrace(); + return false; + } + + // wake SolverObservable + so.notifySolver(); + + return true; + } + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/Ender.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/Ender.java new file mode 100644 index 0000000..50be400 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/Ender.java @@ -0,0 +1,14 @@ +package fr.lip6.move.gal.itscl.modele; + +/** + * Something you tell when it's time to end it. + * + */ +public interface Ender { + /** + * It's over, kill them all. + * Called by a solver that has solved all problem instances. + */ + void killAll(); + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/IRunner.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/IRunner.java new file mode 100644 index 0000000..8d3cc4f --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/IRunner.java @@ -0,0 +1,38 @@ +package fr.lip6.move.gal.itscl.modele; + +import java.io.IOException; +import java.util.Set; + +import fr.lip6.move.gal.Specification; +import fr.lip6.move.gal.itscl.interpreter.IInterpreteObservable; + + +/** + * Adapter to the current Runners (Solvers) + */ + +public interface IRunner { + + /** + * configure specification and initialize doneProps attribute to an empty keySet + */ + public void configure(Specification spec); + + public void configure(Specification z3Spec, Set doneProps) throws IOException; + + /** + * run the solver ! + */ + public void solve(); + + /** + * initialize the manager of interpreters threads + */ + public void configureInterpreter(IInterpreteObservable ob); + + /** +  * Returns if solver did or not well its job + */ + public Boolean taskDone(); + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/ISolverObservable.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/ISolverObservable.java new file mode 100644 index 0000000..4d0dce5 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/ISolverObservable.java @@ -0,0 +1,45 @@ +package fr.lip6.move.gal.itscl.modele; + +import java.util.concurrent.Callable; + +import fr.lip6.move.gal.itscl.interpreter.IInterpreteObservable; + +/** + * It extends : + * + * Callable : run solvers + * + * Ender : manages the completion of solvers + * + * It also manages the synchronization with solvers and their interpreters + */ +public interface ISolverObservable extends Callable, Ender { + + public void attach(ISolverSeq obs); + + public void detach(ISolverSeq obs); + + + /** + * wait till all interpreters end correctly + */ + public void interpreterDone(); + + /** + * Notify SolverObservable that interpreters have complete + */ + public void notifySolver(); + + + /** + * {@link IInterpreteObservable} blocks for future creation of interpreter + */ + public void waitSolver() throws InterruptedException; + + /** + * notify {@link IInterpreteObservable} to start joining interpreters + * threads, when a solver has done the task or none. + */ + public void notifyInterpreter(); + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/ISolverSeq.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/ISolverSeq.java new file mode 100644 index 0000000..faa9f11 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/ISolverSeq.java @@ -0,0 +1,15 @@ +package fr.lip6.move.gal.itscl.modele; + +import java.util.concurrent.Callable; + +/** + * Main runner + */ +public interface ISolverSeq extends Callable { + + /** + * @return 0 : if solve all the props. 1 : didn't achieve them all + */ + public int hasComplete(); + +} diff --git a/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/SolverObservable.java b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/SolverObservable.java new file mode 100644 index 0000000..30a3fc8 --- /dev/null +++ b/fr.lip6.move.gal.itscl.concurrent/src/fr/lip6/move/gal/itscl/modele/SolverObservable.java @@ -0,0 +1,109 @@ +package fr.lip6.move.gal.itscl.modele; + +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import java.util.concurrent.CompletionService; +import java.util.concurrent.ExecutionException; +import java.util.concurrent.ExecutorCompletionService; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.Future; +import java.util.concurrent.Semaphore; + +public class SolverObservable implements ISolverObservable { + + private Set obs = new HashSet<>(); + private List> fsolvers = new ArrayList>(); + private ExecutorService executor = Executors.newCachedThreadPool(); + private Semaphore interpreteComplete = new Semaphore(0); + private Semaphore stopInterpretation = new Semaphore(0); + + public void attach(ISolverSeq o) { + obs.add(o); + } + + public void detach(ISolverSeq o) { + obs.remove(o); + } + + public void interpreterDone() { + + try { + interpreteComplete.acquire(); + } catch (InterruptedException e) { + e.printStackTrace(); + } + } + + public void notifySolver() { + interpreteComplete.release(); + } + + /** + * Try to shutdown immediately all ISolverSeq thread that still running. It + * assure that they really been canceled. + */ + public void killAll() { + + List notFinished = executor.shutdownNow(); // savoir qui a + if (notFinished == null) { + System.out.println("they all complete");// fini + } + for (Future o : fsolvers) { + if (!o.isDone()) { + o.cancel(true); + } + } + // Wait interpreters to finish interpret the last results + interpreterDone(); + } + + public void waitSolver() throws InterruptedException { + stopInterpretation.acquire(); + } + + public void notifyInterpreter() { + stopInterpretation.release(); + } + + /** + * Run all recorded solvers. Wait for a result, if solver did complete well: + * kill 'em all (solvers), if not : repeat wait for the next result + */ + public Boolean call() { + + CompletionService runSolvers = new ExecutorCompletionService(executor); + + for (ISolverSeq o : obs) { + fsolvers.add(runSolvers.submit(o)); + } + + int i = 0; + do { + + try { + // waiting for the first solver to complete + Future solverDone = runSolvers.take(); + + // Test if it did complete well + if (solverDone.get() == 0) { + break; + } + } catch (InterruptedException | ExecutionException e) { + e.printStackTrace(); + return false; + } + } while (i++ < obs.size()); + + // Wake interpreterObservable, it joins all interpreters in order to + // ensure they have completed well + notifyInterpreter(); + + killAll(); + + return (i == obs.size()) ? false : true; + } + +} diff --git a/fr.lip6.move.gal.itscl.parent/.project b/fr.lip6.move.gal.itscl.parent/.project new file mode 100644 index 0000000..6154c28 --- /dev/null +++ b/fr.lip6.move.gal.itscl.parent/.project @@ -0,0 +1,11 @@ + + + fr.lip6.move.gal.itscl.parent + + + + + + + + diff --git a/fr.lip6.move.gal.itscl.parent/pom.xml b/fr.lip6.move.gal.itscl.parent/pom.xml index a553392..2b09d13 100644 --- a/fr.lip6.move.gal.itscl.parent/pom.xml +++ b/fr.lip6.move.gal.itscl.parent/pom.xml @@ -18,6 +18,11 @@ Command-line interaction with code built for Eclipse + + ../fr.lip6.move.gal.itscl.concurrent + ../fr.lip6.move.gal.itscl.adaptors + ../fr.lip6.move.gal.itscl.pnmcc.adaptors + ../fr.lip6.move.gal.itscl.application @@ -124,7 +129,7 @@ org.eclipse.jdt.core - + eclipse-plugin diff --git a/install_eclipse.sh b/install_eclipse.sh deleted file mode 100755 index 9ee9ca0..0000000 --- a/install_eclipse.sh +++ /dev/null @@ -1,37 +0,0 @@ -#! /bin/bash - -set -x - -if [ ! -f eclipse/eclipse ] ; then - if [ ! -f eclipse-platform-4.6.3-linux-gtk-x86_64.tar.gz ] ; then - wget --progress=dot:mega http://mirror.ibcp.fr/pub/eclipse//eclipse/downloads/drops4/R-4.6.3-201703010400/eclipse-platform-4.6.3-linux-gtk-x86_64.tar.gz -# wget http://mirror.ibcp.fr/pub/eclipse//eclipse/downloads/drops4/R-4.6.2-201611241400/eclipse-platform-4.6.2-linux-gtk-x86_64.tar.gz -# wget http://mirror.ibcp.fr/pub/eclipse//eclipse/downloads/drops4/R-4.5.2-201602121500/eclipse-platform-4.5.2-linux-gtk-x86_64.tar.gz -# wget http://mirror.ibcp.fr/pub/eclipse//eclipse/downloads/drops4/R-4.5.1-201509040015/eclipse-platform-4.5.1-linux-gtk-x86_64.tar.gz -# wget http://mirror.ibcp.fr/pub/eclipse//eclipse/downloads/drops4/R-4.4.2-201502041700/eclipse-platform-4.4.2-linux-gtk-x86_64.tar.gz - fi - - tar xzf eclipse-platform-*-linux-gtk-x86_64.tar.gz - rm eclipse-platform-*-linux-gtk-x86_64.tar.gz -fi - -cd eclipse - -# cleanup install -./eclipse \ --clean -purgeHistory \ --application org.eclipse.equinox.p2.director \ --noSplash \ --uninstallIUs fr.lip6.move.gal.feature.pnmcc.feature.group - - -# install -./eclipse \ --clean -purgeHistory \ --application org.eclipse.equinox.p2.director \ --noSplash \ --repository http://yanntm.github.io/Xtext-Light/,https://lip6.github.io/ITSTools \ --installIUs fr.lip6.move.gal.feature.pnmcc.feature.group - -#-repository http://download.eclipse.org/releases/neon,https://lip6.github.io/ITSTools \ - diff --git a/runeclipse.sh b/runeclipse.sh old mode 100755 new mode 100644 index a41c32e..7403668 --- a/runeclipse.sh +++ b/runeclipse.sh @@ -5,11 +5,11 @@ set -x ulimit -s 65536 -java -Dosgi.requiredJavaVersion=1.6 -Xss8m -Xms40m -Xmx8192m -Declipse.pde.launch=true -Dfile.encoding=UTF-8 -classpath $BINDIR/eclipse/plugins/org.eclipse.equinox.launcher_1.3.201.v20161025-1711.jar org.eclipse.equinox.launcher.Main -application fr.lip6.move.gal.application.pnmcc -data $BINDIR/workspace -os linux -ws gtk -arch x86_64 -nl en_US -consoleLog -pnfolder $1 -examination $2 -yices2path $BINDIR/yices/bin/yices ${@:3} +java -Dosgi.requiredJavaVersion=1.6 -Xss8m -Xms40m -Xmx8192m -Declipse.pde.launch=true -Dfile.encoding=UTF-8 -classpath $BINDIR/eclipse/plugins/org.eclipse.equinox.launcher_1.3.201.v20161025-1711.jar org.eclipse.equinox.launcher.Main -application fr.lip6.move.gal.application.pnmcc -data $BINDIR/workspace -os linux -ws gtk -arch x86_64 -nl en_US -consoleLog -pnfolder $1 -examination $2 -z3path $BINDIR/z3/bin/z3 -yices2path $BINDIR/yices/bin/yices ${@:3} # -XX:MaxPermSize=512m # -z3path $BINDIR/z3/bin/z3 # -its #-configuration file:/home/mcc/workspace/.metadata/.plugins/org.eclipse.pde.core/fr.lip6.move.gal.application/ #-dev file:/data/ythierry/workspaces/luna2/.metadata/.plugins/org.eclipse.pde.core/fr.lip6.move.gal.application/dev.properties # luna : org.eclipse.equinox.launcher_1.3.0.v20140415-2008.jar -# mars : org.eclipse.equinox.launcher_1.3.100.v20150511-1540.jar +# mars : org.eclipse.equinox.launcher_1.3.100.v20150511-1540.jar \ No newline at end of file