From 8d29d477bfa16827ab8e16cbf2ea5449198fce7c Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Mon, 19 Jun 2017 15:54:32 +0200 Subject: [PATCH 01/12] garbage --- .../fr/lip6/move/gal/application/Ender.java | 14 -------------- .../fr/lip6/move/gal/application/IRunner.java | 19 ------------------- 2 files changed, 33 deletions(-) delete mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Ender.java delete mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/IRunner.java diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Ender.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Ender.java deleted file mode 100644 index 28b32ed318..0000000000 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Ender.java +++ /dev/null @@ -1,14 +0,0 @@ -package fr.lip6.move.gal.application; - -/** - * 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/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/IRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/IRunner.java deleted file mode 100644 index 5b522edfc5..0000000000 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/IRunner.java +++ /dev/null @@ -1,19 +0,0 @@ -package fr.lip6.move.gal.application; - -import java.io.IOException; -import java.util.Set; - -import fr.lip6.move.gal.Specification; - -public interface IRunner { - - void interrupt(); - - void join() throws InterruptedException; - - void configure(Specification z3Spec, Set doneProps) throws IOException; - - void solve(Ender application); - - -} From abac8e75c7e7b1c84034224fc98f6747d28a24d0 Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Mon, 19 Jun 2017 15:54:43 +0200 Subject: [PATCH 02/12] test --- .../src/Interpreter/CegarInterpreter.java | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java new file mode 100644 index 0000000000..e3a5f5609b --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java @@ -0,0 +1,18 @@ +package Interpreter; + + +import fr.lip6.move.gal.itscl.application.IListener; +import fr.lip6.move.gal.itscl.application.Listener; + +public class CegarInterpreter extends Listener implements Runnable, IListener{ + + public CegarInterpreter(int pipeSize) { + super(pipeSize); + } + + public void run() { + + } + + +} From 4eb27e5d0c9ae352d65ad7054aa1145fd9a3b9f5 Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Tue, 20 Jun 2017 12:11:22 +0200 Subject: [PATCH 03/12] create a special class for itsinterpreter and addin listener to the app --- .../META-INF/MANIFEST.MF | 3 +- .../src/Interpreter/CegarInterpreter.java | 4 +- .../src/Interpreter/ITSInterpreter.java | 180 ++++++++ .../move/gal/application/AbstractRunner.java | 46 +- .../move/gal/application/Application.java | 345 ++++++-------- .../move/gal/application/CegarRunner.java | 139 ++---- .../lip6/move/gal/application/ITSRunner.java | 434 ++++++------------ .../move/gal/application/LTSminRunner.java | 310 ++++++------- .../move/gal/application/MccTranslator.java | 129 +++--- .../lip6/move/gal/application/SMTRunner.java | 146 ++---- 10 files changed, 800 insertions(+), 936 deletions(-) create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/META-INF/MANIFEST.MF b/pnmcc/fr.lip6.move.gal.application.pnmcc/META-INF/MANIFEST.MF index ec2e83019b..8110d4672b 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/META-INF/MANIFEST.MF +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/META-INF/MANIFEST.MF @@ -13,7 +13,8 @@ Require-Bundle: org.eclipse.core.runtime, fr.lip6.move.gal.cegar, fr.lip6.move.gal.gal2smt, fr.lip6.move.gal.gal2pins, - lip6.smtlib.SMT + lip6.smtlib.SMT, + fr.lip6.move.gal.itscl.concurrent Bundle-RequiredExecutionEnvironment: JavaSE-1.8 Bundle-ActivationPolicy: lazy Bundle-Vendor: LIP6 diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java index e3a5f5609b..09c04f6b7a 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java @@ -1,8 +1,8 @@ package Interpreter; -import fr.lip6.move.gal.itscl.application.IListener; -import fr.lip6.move.gal.itscl.application.Listener; +import fr.lip6.move.gal.itscl.modele.IListener; +import fr.lip6.move.gal.itscl.modele.Listener; public class CegarInterpreter extends Listener implements Runnable, IListener{ diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java new file mode 100644 index 0000000000..b30a3e2044 --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java @@ -0,0 +1,180 @@ +package Interpreter; + +import java.io.IOException; +import java.util.Set; +import java.util.concurrent.Callable; + +import org.eclipse.emf.common.util.TreeIterator; +import org.eclipse.emf.ecore.EObject; + +import fr.lip6.move.gal.Property; +import fr.lip6.move.gal.Reference; +import fr.lip6.move.gal.Constant; +import fr.lip6.move.gal.application.MccTranslator; +import fr.lip6.move.gal.itscl.modele.Listener; + +public class ITSInterpreter extends Listener implements Callable { + + // private Map> boundProps; + private String examination; + private boolean withStructure; + private MccTranslator reader; + private Set seen; + private Set todoProps; + + public ITSInterpreter(String examination, boolean withStructure, MccTranslator reader, Set doneProps, + Set todoProps, int pipeSize) { + super(pipeSize); + this.examination = examination; + this.withStructure = withStructure; + this.reader = reader; + this.seen = doneProps; + this.todoProps = todoProps; + } + + public Boolean call() throws Exception { + try { + for (String line = ""; line != null; line = in.readLine()) { + System.out.println(line); + // stdOutput.toString().split("\\r?\\n")) ; + if (line.matches("Max variable value.*")) { + if (examination.equals("StateSpace")) { + System.out.println("STATE_SPACE MAX_TOKEN_IN_PLACE " + line.split(":")[1] + + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure ? "USE_NUPN" : "")); + } + } + if (line.matches("Maximum sum along a path.*")) { + if (examination.equals("StateSpace")) { + int nbtok = Integer.parseInt(line.split(":")[1].replaceAll("\\s", "")); + nbtok += reader.countMissingTokens(); + System.out.println("STATE_SPACE MAX_TOKEN_PER_MARKING " + nbtok + + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure ? "USE_NUPN" : "")); + } + } + if (line.matches("Exact state count.*")) { + if (examination.equals("StateSpace")) { + System.out.println("STATE_SPACE STATES " + line.split(":")[1] + + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure ? "USE_NUPN" : "")); + } + } + if (line.matches("Total edges in reachability graph.*")) { + if (examination.equals("StateSpace")) { + System.out.println("STATE_SPACE UNIQUE_TRANSITIONS " + line.split(":")[1] + + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure ? "USE_NUPN" : "")); + } + } + if (line.matches("System contains.*deadlocks.*")) { + if (examination.equals("ReachabilityDeadlock")) { + + Property dead = reader.getSpec().getProperties().get(0); + String pname = dead.getName(); + double nbdead = Double.parseDouble(line.split("\\s+")[2]); + String res; + if (nbdead == 0) + res = "FALSE"; + else + res = "TRUE"; + System.out.println("FORMULA " + pname + " " + res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + + (withStructure ? "USE_NUPN" : "")); + seen.add(pname); + } + } + if (line.matches("Bounds property.*")) { + if (examination.contains("Bounds")) { + String[] words = line.split(" "); + String pname = words[2]; + String[] tab = line.split("<="); + + String sbound = tab[2].replaceAll("\\s", ""); + + int bound = Integer.parseInt(sbound); + Property target = null; + for (Property prop : reader.getSpec().getProperties()) { + if (prop.getName().equals(pname)) { + target = prop; + break; + } + } + int toadd = 0; + for (TreeIterator it = target.eAllContents(); it.hasNext();) { + EObject obj = it.next(); + if (obj instanceof Constant) { + Constant cte = (Constant) obj; + toadd += cte.getValue(); + } else if (obj instanceof Reference) { + it.prune(); + } + } + seen.add(pname); + System.out.println("FORMULA " + pname + " " + (bound + toadd) + + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure ? "USE_NUPN" : "")); + } + } + if (examination.startsWith("CTL")) { + if (line.matches(".*formula \\d+,\\d+,.*")) { + String[] tab = line.split(","); + int formindex = Integer.parseInt(tab[0].split(" ")[1]); + int verdict = Integer.parseInt(tab[1]); + String res; + if (verdict == 0) + res = "FALSE"; + else + res = "TRUE"; + String pname = reader.getSpec().getProperties().get(formindex).getName(); + System.out.println("FORMULA " + pname + " " + res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + + (withStructure ? "USE_NUPN" : "")); + seen.add(pname); + } + } + if (examination.startsWith("LTL")) { + if (line.matches("Formula \\d+ is .*")) { + String[] tab = line.split(" "); + int formindex = Integer.parseInt(tab[1]); + String res = tab[3]; + String pname = reader.getSpec().getProperties().get(formindex).getName(); + System.out.println("FORMULA " + pname + " " + res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + + (withStructure ? "USE_NUPN" : "")); + seen.add(pname); + } + } + + if (line.matches(".*-" + examination + "-\\d+.*")) { + // System.out.println(line); + String res; + if (line.matches(".*property.*") && !line.contains("Bounds")) { + String pname = line.split(" ")[2]; + if (line.contains("does not hold")) { + res = "FALSE"; + } else if (line.contains("No reachable states")) { + res = "FALSE"; + pname = line.split(":")[1]; + } else { + res = "TRUE"; + } + pname = pname.replaceAll("\\s", ""); + if (!seen.contains(pname)) { + System.out.println("FORMULA " + pname + " " + res + + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL COLLATERAL_PROCESSING " + + (withStructure ? "USE_NUPN" : "")); + seen.add(pname); + } + } + } + } + in.close(); + } catch (NumberFormatException e) { + e.printStackTrace(); + return false; + } catch (IOException e) { + e.printStackTrace(); + return false; + } + closePinPout(); + + if (seen.containsAll(todoProps)) { + return true; + } + return false; + } + +} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java index e0a7f483d1..a52493c6e6 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java @@ -1,37 +1,51 @@ package fr.lip6.move.gal.application; import java.io.IOException; + import java.util.Set; +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; -public abstract class AbstractRunner implements IRunner { +public abstract class AbstractRunner implements IRunner { protected Specification spec; protected Set doneProps; - protected Thread runnerThread; + protected IListener listener; + public AbstractRunner() { super(); } + + public void setListener(IListener l){ + this.listener=l; + } - @Override - public void interrupt() { - if (runnerThread != null) { - runnerThread.interrupt(); - } + public void configure(Specification z3Spec, Set doneProps) throws IOException { + this.spec = z3Spec; + this.doneProps = doneProps; } - @Override - public void join() throws InterruptedException { - if (runnerThread != null) { - runnerThread.join(); - } + public abstract void solve(); + + public Specification getSpec() { + return spec; } - @Override - public void configure(Specification z3Spec, Set doneProps) throws IOException { - this.spec = z3Spec ; - this.doneProps = doneProps; + public Set getDoneProps() { + return doneProps; + } + + public Boolean taskDone() { + for (Property prop : getSpec().getProperties()) { + if (!doneProps.contains(prop.getName())) { + // still some work to do + return false; + } + } + return true; } } \ No newline at end of file diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index 875321898b..403f537e08 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java @@ -1,11 +1,13 @@ package fr.lip6.move.gal.application; -import java.io.File; import java.io.IOException; import java.util.ArrayList; import java.util.List; import java.util.Set; import java.util.concurrent.ConcurrentHashMap; +import java.util.concurrent.ExecutionException; +import java.util.concurrent.FutureTask; + import org.eclipse.emf.ecore.util.EcoreUtil; import org.eclipse.equinox.app.IApplication; import org.eclipse.equinox.app.IApplicationContext; @@ -19,17 +21,18 @@ import fr.lip6.move.gal.Specification; import fr.lip6.move.gal.True; import fr.lip6.move.gal.gal2smt.Solver; +import fr.lip6.move.gal.itscl.adaptor.InteractApplication; +import fr.lip6.move.gal.itscl.modele.IRunner; +import fr.lip6.move.gal.itscl.modele.SolverObservable; import fr.lip6.move.serialization.SerializationUtil; /** * This class controls all aspects of the application's execution */ -public class Application implements IApplication, Ender { +public class Application implements IApplication { - - private static final String APPARGS = "application.args"; - + private static final String PNFOLDER = "-pnfolder"; private static final String EXAMINATION = "-examination"; @@ -41,57 +44,45 @@ public class Application implements IApplication, Ender { private static final String LTSMINPATH = "-ltsminpath"; private static final String ONLYGAL = "-onlyGal"; private static final String disablePOR = "-disablePOR"; - - + private IRunner cegarRunner; private IRunner z3Runner; private IRunner itsRunner; private IRunner ltsminRunner; - - - @Override - public synchronized void killAll () { - if (cegarRunner != null) - cegarRunner.interrupt(); - if (z3Runner != null) - z3Runner.interrupt(); - if (itsRunner != null) - itsRunner.interrupt(); - if (ltsminRunner != null) - ltsminRunner.interrupt(); - System.exit(0); - } - /* (non-Javadoc) - * @see org.eclipse.equinox.app.IApplication#start(org.eclipse.equinox.app.IApplicationContext) + /* + * (non-Javadoc) + * + * @see org.eclipse.equinox.app.IApplication#start(org.eclipse.equinox.app. + * IApplicationContext) */ - @Override + @SuppressWarnings("unused") public Object start(IApplicationContext context) throws Exception { - - String [] args = (String[]) context.getArguments().get(APPARGS); - + + String[] args = (String[]) context.getArguments().get(APPARGS); + String pwd = null; String examination = null; String z3path = null; String yices2path = null; String ltsminpath = null; - + boolean doITS = false; boolean doSMT = false; boolean doCegar = false; boolean onlyGal = false; boolean doLTSmin = false; boolean doPOR = true; - - for (int i=0; i < args.length ; i++) { + + for (int i = 0; i < args.length; i++) { if (PNFOLDER.equals(args[i])) { pwd = args[++i]; } else if (EXAMINATION.equals(args[i])) { - examination = args[++i]; + examination = args[++i]; } else if (Z3PATH.equals(args[i])) { - z3path = args[++i]; + z3path = args[++i]; } else if (YICES2PATH.equals(args[i])) { - yices2path = args[++i]; + yices2path = args[++i]; } else if (SMT.equals(args[i])) { doSMT = true; } else if (LTSMINPATH.equals(args[i])) { @@ -107,23 +98,12 @@ public Object start(IApplicationContext context) throws Exception { onlyGal = true; } } - - // use Z3 in preference to Yices if both are available - Solver solver = Solver.Z3; - String solverPath = z3path; - if (z3path == null && yices2path != null) { - solver = Solver.YICES2 ; - solverPath = yices2path; - } - - // EMF registration + SerializationUtil.setStandalone(true); - - // setup a "reader" that parses input property files correctly and efficiently - MccTranslator reader = new MccTranslator(pwd,examination); - - try { - // parse the model from PNML to GAL using PNMLFW for COL or fast SAX for PT models + + MccTranslator reader = new MccTranslator(pwd, examination); + + try { reader.transformPNML(); } catch (IOException e) { System.err.println("Incorrect file or folder " + pwd + "\n Error :" + e.getMessage()); @@ -135,179 +115,131 @@ public Object start(IApplicationContext context) throws Exception { return null; } - // for debug and control COL files are small, otherwise 1MB PNML limit (i.e. roughly 200kB GAL max). - if (pwd.contains("COL") || new File(pwd + "/model.pnml").length() < 1000000) { + // for debug and control + if (pwd.contains("COL")) { String outpath = pwd + "/model.pnml.img.gal"; SerializationUtil.systemToFile(reader.getSpec(), outpath); } - - // initialize a shared container to detect help detect termination in portfolio case + + boolean withStructure = reader.hasStructure(); + Set doneProps = ConcurrentHashMap.newKeySet(); - // reader now has a spec and maybe a ITS decomposition - // no properties yet. - - + reader.loadProperties(); + + SolverObservable chRunner = new SolverObservable(); + if (examination.equals("StateSpace")) { - // ITS is the only method we will run. + reader.flattenSpec(true); - if (doITS || onlyGal) { - // decompose + simplify as needed - itsRunner = new ITSRunner(examination, reader, doITS, onlyGal, reader.getFolder()); - itsRunner.configure(reader.getSpec(), doneProps); - } - - if (doITS) { - itsRunner.solve(this); - itsRunner.join(); - } - return 0; - } - // Now translate and load properties into GAL - // uses a SAX parser to load to Logic MM, then an M2M to GAL properties. - reader.loadProperties(); - - // are we going for CTL ? only ITSRunner answers this. - if (examination.startsWith("CTL") || examination.equals("UpperBounds")) { - - if (examination.startsWith("CTL")) { - // due to + being OR in the CTL syntax, we don't support this type of props - // TODO: make CTL syntax match the normal predicate syntax in ITS tools - reader.removeAdditionProperties(); - } - // we support hierarchy + } else if (examination.equals("ReachabilityDeadlock")) { reader.flattenSpec(true); - if (doITS || onlyGal) { - // decompose + simplify as needed - itsRunner = new ITSRunner(examination, reader, doITS, onlyGal, reader.getFolder()); - itsRunner.configure(reader.getSpec(), doneProps); - } - - if (doITS) { - itsRunner.solve(this); - itsRunner.join(); - } - return 0; - } - - // LTL, Deadlocks are ok for LTSmin and ITS - if (examination.startsWith("LTL") || examination.equals("ReachabilityDeadlock")) { - - boolean flattened = false; - // LTSmin prefers no hierarchy target - if (onlyGal || doLTSmin) { - reader.flattenSpec(false); - flattened = true; - // || examination.startsWith("CTL") - if (! reader.getSpec().getProperties().isEmpty()) { - System.out.println("Using solver "+solver+" to compute partial order matrices."); - ltsminRunner = new LTSminRunner(ltsminpath, solverPath, solver, doPOR, onlyGal, reader.getFolder(), 3600 / reader.getSpec().getProperties().size() ); - ltsminRunner.configure(EcoreUtil.copy(reader.getSpec()), doneProps); - ltsminRunner.solve(this); - } - } - if (doITS || onlyGal) { - // LTSmin has safely copied the spec, decompose with order if available - if (reader.hasStructure() || !flattened) { - reader.flattenSpec(true); - } - - // decompose + simplify as needed - itsRunner = new ITSRunner(examination, reader, doITS, onlyGal, reader.getFolder()); - itsRunner.configure(reader.getSpec(), doneProps); - if (doITS) { - itsRunner.solve(this); - } - } - - if (itsRunner != null) - itsRunner.join(); - if (ltsminRunner != null) - ltsminRunner.join(); - - return 0; - } - - - // ReachabilityCard and ReachFire are ok for everybody - if (examination.equals("ReachabilityFireability") || examination.equals("ReachabilityCardinality") ) { + + } else if (examination.startsWith("CTL")) { + reader.removeAdditionProperties(); + + reader.flattenSpec(true); + + } else if (examination.startsWith("LTL")) { + reader.flattenSpec(true); + + } else if (examination.startsWith("Reachability") || examination.contains("Bounds")) { reader.flattenSpec(false); - // get rid of trivial properties in spec - checkInInitial(reader.getSpec(), doneProps); - - // SMT does support hierarchy theoretically but does not like it much currently, time to start it, the spec won't get any better - if ( (z3path != null || yices2path != null) && doSMT ) { - Specification z3Spec = EcoreUtil.copy(reader.getSpec()); - // run on a fresh copy to avoid any interference with other threads. - z3Runner = new SMTRunner(pwd, solverPath, solver ); - z3Runner.configure(z3Spec, doneProps); - z3Runner.solve(this); - } - // run on a fresh copy to avoid any interference with other threads. - if (doCegar) { - cegarRunner = new CegarRunner(pwd); - cegarRunner.configure(EcoreUtil.copy(reader.getSpec()), doneProps); - cegarRunner.solve(this); - } - - // run LTS min - if (onlyGal || doLTSmin) { - if (! reader.getSpec().getProperties().isEmpty() ) { - System.out.println("Using solver "+solver+" to compute partial order matrices."); - ltsminRunner = new LTSminRunner(ltsminpath, solverPath, solver, doPOR, onlyGal, reader.getFolder(), 3600 / reader.getSpec().getProperties().size() ); - ltsminRunner.configure(EcoreUtil.copy(reader.getSpec()), doneProps); - ltsminRunner.solve(this); + if (examination.startsWith("Reachability")) { + + // get rid of trivial properties in spec + checkInInitial(reader.getSpec(), doneProps); + // cegar does not support hierarchy currently, time to start it, + // the spec won't get any better + if ((z3path != null || yices2path != null) && doSMT) { + Specification z3Spec = EcoreUtil.copy(reader.getSpec()); + Solver solver = Solver.YICES2; + String solverPath = yices2path; + if (z3path != null && yices2path == null) { + solver = Solver.Z3; + solverPath = z3path; + } + // run on a fresh copy to avoid any interference with other + // threads. + z3Runner = new SMTRunner(pwd, solverPath, solver); + z3Runner.configure(z3Spec, doneProps); + chRunner.attach(InteractApplication.add(z3Runner)); + } + + // run on a fresh copy to avoid any interference with other + // threads. + if (doCegar) { + cegarRunner = new CegarRunner(pwd); + cegarRunner.configure(EcoreUtil.copy(reader.getSpec()), doneProps); + chRunner.attach(InteractApplication.add(cegarRunner)); } } - - - if (doITS || onlyGal) { + if (doITS || onlyGal) { // decompose + simplify as needed reader.flattenSpec(true); - } - if (doITS || onlyGal) { - // decompose + simplify as needed - itsRunner = new ITSRunner(examination, reader, doITS, onlyGal, reader.getFolder()); - itsRunner.configure(reader.getSpec(), doneProps); - } - - if (doITS) { - itsRunner.solve(this); } } - - - - if (ltsminRunner != null) - ltsminRunner.join(); - if (cegarRunner != null) - cegarRunner.join(); - if (z3Runner != null) - z3Runner.join(); - if (itsRunner != null) - itsRunner.join(); - return IApplication.EXIT_OK; - } - + if (doITS || onlyGal) { + // decompose + simplify as needed + itsRunner = new ITSRunner(examination, reader, doITS, onlyGal, reader.getFolder()); + itsRunner.configure(reader.getSpec(), doneProps); + } + if (doITS) { + chRunner.attach(InteractApplication.add(itsRunner)); + } + if (onlyGal || doLTSmin) { + Solver solver = Solver.YICES2; + String solverPath = yices2path; + if (z3path != null && yices2path == null) { + // if (z3path != null) { + solver = Solver.Z3; + solverPath = z3path; + } + // || examination.startsWith("CTL") + if (!reader.getSpec().getProperties().isEmpty() + && (examination.startsWith("Reachability") || examination.startsWith("LTL"))) { + System.out.println("Using solver " + solver + " to compute partial order matrices."); + ltsminRunner = new LTSminRunner(ltsminpath, solverPath, solver, doPOR, onlyGal, reader.getFolder(), + 3600 / reader.getSpec().getProperties().size()); + ltsminRunner.configure(reader.getSpec(), doneProps); + chRunner.attach(InteractApplication.add(ltsminRunner)); + } + } + FutureTask executeRunner = new FutureTask<>(chRunner); + Thread futureTh = new Thread(executeRunner); + // exec.submit(superRunner); + try { + futureTh.start(); + Boolean result = executeRunner.get(); + System.out.println("Operation reussi ? " + result); + } catch (ExecutionException e) { + System.out.println("im here sh_________"); + e.printStackTrace(); + } + return IApplication.EXIT_OK; + } /** * Structural analysis and reduction : test in initial state. - * @param specWithProps spec which will be modified : trivial properties will be removed - * @param doneProps + * + * @param specWithProps + * spec which will be modified : trivial properties will be + * removed + * @param doneProps */ private void checkInInitial(Specification specWithProps, Set doneProps) { List props = new ArrayList(specWithProps.getProperties()); - + // iterate down so indexes are consistent - for (int i = props.size()-1; i >= 0 ; i--) { + for (int i = props.size() - 1; i >= 0; i--) { Property propp = props.get(i); if (doneProps.contains(propp.getName())) { @@ -315,7 +247,6 @@ private void checkInInitial(Specification specWithProps, Set doneProps) } if (propp.getBody() instanceof SafetyProp) { SafetyProp prop = (SafetyProp) propp.getBody(); - // discard property if (prop.getPredicate() instanceof True || prop.getPredicate() instanceof False) { @@ -327,21 +258,25 @@ private void checkInInitial(Specification specWithProps, Set doneProps) if (prop.getPredicate() instanceof True) { // positive forms : EF True , AG True <=>True - System.out.println("FORMULA "+propp.getName() + " TRUE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + System.out.println("FORMULA " + propp.getName() + " TRUE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); solved = true; } else if (prop.getPredicate() instanceof False) { // positive forms : EF False , AG False <=> False - System.out.println("FORMULA "+propp.getName() + " FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + System.out + .println("FORMULA " + propp.getName() + " FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); solved = true; } } else if (prop instanceof NeverProp) { if (prop.getPredicate() instanceof True) { - // negative form : ! EF P = AG ! P, so ! EF True <=> False - System.out.println("FORMULA "+propp.getName() + " FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + // negative form : ! EF P = AG ! P, so ! EF True <=> + // False + System.out + .println("FORMULA " + propp.getName() + " FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); solved = true; } else if (prop.getPredicate() instanceof False) { - // negative form : ! EF P = AG ! P, so ! EF False <=> True - System.out.println("FORMULA "+propp.getName() + " TRUE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + // negative form : ! EF P = AG ! P, so ! EF False <=> + // True + System.out.println("FORMULA " + propp.getName() + " TRUE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); solved = true; } } @@ -352,18 +287,10 @@ private void checkInInitial(Specification specWithProps, Set doneProps) } } - - - - /* (non-Javadoc) - * @see org.eclipse.equinox.app.IApplication#stop() - */ @Override public void stop() { - killAll(); + // TODO Auto-generated method stub + } - - - } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java index a2fc01683e..0bece6e3af 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java @@ -6,118 +6,75 @@ import java.util.logging.Logger; import fr.lip6.move.gal.Property; -import fr.lip6.move.gal.Specification; import fr.lip6.move.gal.cegar.frontend.CegarFrontEnd; import fr.lip6.move.gal.cegar.interfaces.IResult; import fr.lip6.move.gal.instantiate.CompositeBuilder; import fr.lip6.move.gal.instantiate.GALRewriter; import fr.lip6.move.gal.instantiate.Simplifier; -public class CegarRunner extends AbstractRunner implements IRunner { - +public class CegarRunner extends AbstractRunner { + private String pwd; + private List todoProps; public CegarRunner(String pwd) { this.pwd = pwd; - } - - public static Thread runCegar(final Specification spec, final String pwd, final Ender ender) { - - Thread cegarRunner = new Thread(new Runnable() { - - @Override - public void run() { - // current implem cannot deal with arrays - // degeneralize, should be ok for Petri nets at least - GALRewriter.flatten(spec, true); - CompositeBuilder cb = CompositeBuilder.getInstance(); - cb.rewriteArraysAsVariables(spec); - Simplifier.simplify(spec); - final List properties = new ArrayList(spec.getProperties()); - for (Property prop : properties) { - spec.getProperties().clear(); - spec.getProperties().add(prop); - try { - IResult res = CegarFrontEnd.processGal(spec, pwd); - String ress = "FALSE"; - if (res.isPropertyTrue()) { - ress = "TRUE"; - } - - System.out.println("FORMULA "+prop.getName()+ " "+ ress + " TECHNIQUES DECISION_DIAGRAMS COLLATERAL_PROCESSING TOPOLOGICAL CEGAR "); - - } catch (IOException e) { - e.printStackTrace(); - getLog().warning("Aborting CEGAR due to an exception"); - return; - } catch (RuntimeException re) { - re.printStackTrace(); - getLog().warning("Aborting CEGAR check of property " + prop.getName() + " due to an exception when running procedure."); - } - } - ender.killAll(); - - } - }); - cegarRunner.start(); - return cegarRunner; } - + private static Logger getLog() { return Logger.getLogger("fr.lip6.move.gal"); - - } - @Override - public void solve(Ender ender ) { - runnerThread = new Thread(new Runnable() { + } - @Override - public void run() { - // current implem cannot deal with arrays - // degeneralize, should be ok for Petri nets at least - GALRewriter.flatten(spec, true); - CompositeBuilder cb = CompositeBuilder.getInstance(); - cb.rewriteArraysAsVariables(spec); - Simplifier.simplify(spec); + public Boolean taskDone() { + for (Property prop : todoProps) { + if (!doneProps.contains(prop.getName())) { + // still some work to do + System.out.println("tasks not all resolved Cegar"); + return false; + } + } + System.out.println("tasks resolved Cegar"); + return true; + } - final List properties = new ArrayList(spec.getProperties()); - for (Property prop : properties) { - if (! doneProps.contains( prop.getName())) { - spec.getProperties().clear(); - spec.getProperties().add(prop); - try { - IResult res = CegarFrontEnd.processGal(spec, pwd); - String ress = "FALSE"; - if (res.isPropertyTrue()) { - ress = "TRUE"; - } + public void solve() { - System.out.println("FORMULA "+prop.getName()+ " "+ ress + " TECHNIQUES DECISION_DIAGRAMS COLLATERAL_PROCESSING TOPOLOGICAL CEGAR "); + // current implem cannot deal with arrays + // degeneralize, should be ok for Petri nets at least + GALRewriter.flatten(spec, true); + CompositeBuilder cb = CompositeBuilder.getInstance(); + cb.rewriteArraysAsVariables(spec); + Simplifier.simplify(spec); + todoProps = new ArrayList(spec.getProperties()); + for (Property prop : todoProps) { + if (!doneProps.contains(prop.getName())) { + spec.getProperties().clear(); + spec.getProperties().add(prop); + try { + IResult res = CegarFrontEnd.processGal(spec, pwd); - } catch (IOException e) { - e.printStackTrace(); - getLog().warning("Aborting CEGAR due to an exception"); - return; - } catch (RuntimeException re) { - re.printStackTrace(); - getLog().warning("Aborting CEGAR check of property " + prop.getName() + " due to an exception when running procedure."); - } - } - } - for (Property prop : properties) { - if (! doneProps.contains(prop.getName())) { - // still some work to do - return; + String ress = "FALSE"; + if (res.isPropertyTrue()) { + ress = "TRUE"; } + System.out.println("FORMULA " + prop.getName() + " " + ress + + " TECHNIQUES DECISION_DIAGRAMS COLLATERAL_PROCESSING TOPOLOGICAL CEGAR "); + + } catch (IOException e) { + e.printStackTrace(); + getLog().warning("Aborting CEGAR due to an exception"); + return; + } catch (RuntimeException re) { + re.printStackTrace(); + getLog().warning("Aborting CEGAR check of property " + prop.getName() + + " due to an exception when running procedure."); } - ender.killAll(); - + } - }); - runnerThread.start(); + } + System.out.println("CEGAR HAS COMPLETELY FINISHED"); + } - - } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java index 448b89e347..0ec3836cca 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java @@ -1,23 +1,17 @@ package fr.lip6.move.gal.application; -import java.io.BufferedReader; import java.io.File; import java.io.IOException; -import java.io.InputStream; -import java.io.InputStreamReader; import java.io.OutputStream; -import java.io.PipedInputStream; -import java.io.PipedOutputStream; import java.util.ArrayList; import java.util.List; import java.util.Set; +import java.util.concurrent.ExecutionException; +import java.util.concurrent.FutureTask; import java.util.stream.Collectors; -import org.eclipse.emf.common.util.TreeIterator; -import org.eclipse.emf.ecore.EObject; -import fr.lip6.move.gal.Constant; +import Interpreter.ITSInterpreter; import fr.lip6.move.gal.Property; -import fr.lip6.move.gal.Reference; import fr.lip6.move.gal.Specification; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.CommandLineBuilder; @@ -33,24 +27,19 @@ public class ITSRunner extends AbstractRunner { private CommandLine cl; private boolean doITS; private boolean onlyGal; - private String workFolder; - - private Thread itsReader; - - - - public ITSRunner(String examination, MccTranslator reader, boolean doITS, boolean onlyGal, - String workFolder) { + private String folder; + private Set todoProps; + + private boolean done = false; + + public ITSRunner(String examination, MccTranslator reader, boolean doITS, boolean onlyGal, String workFolder) { this.examination = examination; this.reader = reader; this.doITS = doITS; this.onlyGal = onlyGal; - this.workFolder = workFolder; + this.folder = workFolder; } - - - @Override public void configure(Specification spec, Set doneProps) throws IOException { super.configure(spec, doneProps); if (examination.equals("StateSpace")) { @@ -66,39 +55,37 @@ public void configure(Specification spec, Set doneProps) throws IOExcept } } else if (examination.startsWith("CTL")) { reader.removeAdditionProperties(); - - - if (doITS || onlyGal) { - String outpath = outputGalFile(); - - String ctlpath = outputPropertyFile(); - + + if (doITS || onlyGal) { + String outpath = outputGalFile(); + + String ctlpath = outputPropertyFile(); + cl = buildCommandLine(outpath, Tool.ctl); cl.addArg("-ctl"); - cl.addArg(ctlpath); - - //cl.addArg("--backward"); + cl.addArg(ctlpath); + + // cl.addArg("--backward"); } } else if (examination.startsWith("LTL")) { - + if (doITS || onlyGal) { String outpath = outputGalFile(); String ltlpath = outputPropertyFile(); - - + cl = buildCommandLine(outpath, Tool.ltl); cl.addArg("-LTL"); - cl.addArg(ltlpath); + cl.addArg(ltlpath); cl.addArg("-c"); - //cl.addArg("-SSLAP-FSA"); - + // cl.addArg("-SSLAP-FSA"); + cl.addArg("-stutter-deadlock"); } - + } else if (examination.startsWith("Reachability") || examination.contains("Bounds")) { - if (doITS || onlyGal) { + if (doITS || onlyGal) { // decompose + simplify as needed String outpath = outputGalFile(); @@ -111,227 +98,53 @@ public void configure(Specification spec, Set doneProps) throws IOExcept cl.addArg("-reachable-file"); cl.addArg(new File(propPath).getName()); - cl.addArg("--nowitness"); - } + cl.addArg("--nowitness"); + } } if (cl != null) { - cl.setWorkingDir(new File(workFolder)); - } - } - - @Override - public void interrupt() { - super.interrupt(); - if (itsReader != null) { - itsReader.interrupt(); - } - } - - @Override - public void join() throws InterruptedException { - super.join(); - if (itsReader != null) { - itsReader.join(); + cl.setWorkingDir(new File(folder)); } } - class ITSInterpreter implements Runnable { - - private BufferedReader in; - //private Map> boundProps; - private String examination; - private boolean withStructure; - private MccTranslator reader; - private Set seen; - private Set todoProps; - private Ender ender; - - - public ITSInterpreter(String examination, boolean withStructure, MccTranslator reader, Set doneProps, Set todoProps, Ender ender) { - this.examination = examination; - this.withStructure = withStructure; - this.reader = reader; - this.seen = doneProps; - this.todoProps = todoProps; - this.ender = ender; - } - - public void setInput(InputStream pin) { - this.in = new BufferedReader(new InputStreamReader(pin)); - } - - @Override - public void run() { - - - try { - for (String line = ""; line != null ; line=in.readLine() ) { - System.out.println(line); - //stdOutput.toString().split("\\r?\\n")) ; - if ( line.matches("Max variable value.*")) { - if (examination.equals("StateSpace")) { - System.out.println( "STATE_SPACE MAX_TOKEN_IN_PLACE " + line.split(":")[1] + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - } - } - if ( line.matches("Maximum sum along a path.*")) { - if (examination.equals("StateSpace")) { - int nbtok = Integer.parseInt(line.split(":")[1].replaceAll("\\s", "")); - nbtok += reader.countMissingTokens(); - System.out.println( "STATE_SPACE MAX_TOKEN_PER_MARKING " + nbtok + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - } - } - if ( line.matches("Exact state count.*")) { - if (examination.equals("StateSpace")) { - System.out.println( "STATE_SPACE STATES " + line.split(":")[1] + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - } - } - if ( line.matches("Total edges in reachability graph.*")) { - if (examination.equals("StateSpace")) { - System.out.println( "STATE_SPACE UNIQUE_TRANSITIONS " + line.split(":")[1] + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - } - } - if ( line.matches("System contains.*deadlocks.*")) { - if (examination.equals("ReachabilityDeadlock")) { - - Property dead = reader.getSpec().getProperties().get(0); - String pname = dead.getName(); - double nbdead = Double.parseDouble(line.split("\\s+")[2]); - String res ; - if (nbdead == 0) - res = "FALSE"; - else - res = "TRUE"; - System.out.println( "FORMULA " + pname + " " +res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - seen.add(pname); - } - } - if ( line.matches("Bounds property.*")) { - if (examination.contains("Bounds") ) { - String [] words = line.split(" "); - String pname = words[2]; - String [] tab = line.split("<="); - - String sbound = tab[2].replaceAll("\\s", ""); - - int bound = Integer.parseInt(sbound); - Property target = null; - for (Property prop : reader.getSpec().getProperties()) { - if (prop.getName().equals(pname) ) { - target = prop; - break; - } - } - int toadd=0; - for (TreeIterator it = target.eAllContents() ; it.hasNext() ; ) { - EObject obj = it.next(); - if (obj instanceof Constant) { - Constant cte = (Constant) obj; - toadd += cte.getValue(); - } else if (obj instanceof Reference) { - it.prune(); - } - } - seen.add(pname); - System.out.println( "FORMULA " + pname + " " + (bound+toadd) + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - } - } - if ( examination.startsWith("CTL")) { - if (line.matches(".*formula \\d+,\\d+,.*")) { - String [] tab = line.split(","); - int formindex = Integer.parseInt(tab[0].split(" ")[1]); - int verdict = Integer.parseInt(tab[1]); - String res ; - if (verdict == 0) - res = "FALSE"; - else - res = "TRUE"; - String pname = reader.getSpec().getProperties().get(formindex).getName(); - System.out.println( "FORMULA " + pname + " " +res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - seen.add(pname); - } - } - if ( examination.startsWith("LTL")) { - if (line.matches("Formula \\d+ is .*")) { - String [] tab = line.split(" "); - int formindex = Integer.parseInt(tab[1]); - String res = tab[3]; - String pname = reader.getSpec().getProperties().get(formindex).getName(); - System.out.println( "FORMULA " + pname + " " +res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - seen.add(pname); - } - } - - if ( line.matches(".*-"+examination+"-\\d+.*")) { - //System.out.println(line); - String res; - if (line.matches(".*property.*") && ! line.contains("Bounds")) { - String pname = line.split(" ")[2]; - if (line.contains("does not hold")) { - res = "FALSE"; - } else if (line.contains("No reachable states")) { - res = "FALSE"; - pname = line.split(":")[1]; - } else { - res = "TRUE"; - } - pname = pname.replaceAll("\\s", ""); - if (!seen.contains(pname)) { - System.out.println("FORMULA "+pname+ " "+ res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL COLLATERAL_PROCESSING " + (withStructure?"USE_NUPN":"")); - seen.add(pname); - } - } - } - } - in.close(); - } catch (NumberFormatException e) { - e.printStackTrace(); - } catch (IOException e) { - e.printStackTrace(); - } - if (seen.containsAll(todoProps)) { - ender.killAll(); - } - } - - } - class ITSRealRunner implements Runnable { private OutputStream pout; private CommandLine cl; - + public ITSRealRunner(OutputStream pout, CommandLine cl) { this.pout = pout; this.cl = cl; } - @Override public void run() { - try { + try { Runner.runTool(3500, cl, pout, false); + } catch (TimeOutException e) { System.out.println("Detected timeout of ITS tools."); return; - // return new Status(IStatus.ERROR, ID, - // "Check Service process did not finish in a timely way." - // + errorOutput.toString()); + // return new Status(IStatus.ERROR, ID, + // "Check Service process did not finish in a timely way." + // + errorOutput.toString()); } catch (IOException e) { System.out.println("Failure when invoking ITS tools."); return; - // return new Status(IStatus.ERROR, ID, - // "Unexpected exception executing service." - // + errorOutput.toString(), e); + // return new Status(IStatus.ERROR, ID, + // "Unexpected exception executing service." + // + errorOutput.toString(), e); } finally { try { pout.close(); + System.out.println("ITS HAS COMPLETELY FINISHED"); } catch (IOException e) { e.printStackTrace(); } } } } + private CommandLine buildCommandLine(String modelff) throws IOException { - return buildCommandLine(modelff,Tool.reach); + return buildCommandLine(modelff, Tool.reach); } private CommandLine buildCommandLine(String modelff, Tool tool) throws IOException { @@ -340,10 +153,9 @@ private CommandLine buildCommandLine(String modelff, Tool tool) throws IOExcepti cl.setModelType("CGAL"); return cl.getCommandLine(); } - - + public String outputPropertyFile() throws IOException { - String proppath = workFolder +"/" + examination ; + String proppath = folder + "/" + examination; if (examination.contains("CTL")) { proppath += ".ctl"; SerializationUtil.serializePropertiesForITSCTLTools(getOutputPath(), spec.getProperties(), proppath); @@ -355,57 +167,66 @@ public String outputPropertyFile() throws IOException { proppath += ".prop"; SerializationUtil.serializePropertiesForITSTools(getOutputPath(), spec.getProperties(), proppath); } - - + return proppath; } - -// private void buildProperty (File file) throws IOException { -// if (file.getName().endsWith(".xml") && file.getName().contains("Reachability") ) { -// -// // normal case -// { -//// Properties props = fr.lip6.move.gal.logic.util.SerializationUtil.fileToProperties(file.getLocationURI().getPath().toString()); -// // TODO : is the copy really useful ? -// Properties props = PropertyParser.fileToProperties(file.getPath().toString(), EcoreUtil.copy(spec)); -// -// Specification specWithProps = ToGalTransformer.toGal(props); -// -// if (order != null) { -// CompositeBuilder.getInstance().decomposeWithOrder((GALTypeDeclaration) specWithProps.getTypes().get(0), order.clone()); -// } -// // compute constants -// Support constants = GALRewriter.flatten(specWithProps, true); -// -// File galout = new File( file.getParent() +"/" + file.getName().replace(".xml", ".gal")); -// fr.lip6.move.serialization.SerializationUtil.systemToFile(specWithProps, galout.getAbsolutePath()); -// } -// // Abstraction case -// if (file.getParent().contains("-COL-")) { -// ToGalTransformer.setWithAbstractColors(true); -// Properties props = PropertyParser.fileToProperties(file.getPath().toString(), EcoreUtil.copy(spec)); -// -// Specification specnocol = ToGalTransformer.toGal(props); -// Instantiator.instantiateParametersWithAbstractColors(specnocol); -// GALRewriter.flatten(specnocol, true); -// -// File galout = new File( file.getParent() +"/" + file.getName().replace(".xml", ".nocol.gal")); -// fr.lip6.move.serialization.SerializationUtil.systemToFile(specnocol, galout.getAbsolutePath()); -// -// ToGalTransformer.setWithAbstractColors(false); -// } -// -// } -// } - - + + // private void buildProperty (File file) throws IOException { + // if (file.getName().endsWith(".xml") && + // file.getName().contains("Reachability") ) { + // + // // normal case + // { + //// Properties props = + // fr.lip6.move.gal.logic.util.SerializationUtil.fileToProperties(file.getLocationURI().getPath().toString()); + // // TODO : is the copy really useful ? + // Properties props = + // PropertyParser.fileToProperties(file.getPath().toString(), + // EcoreUtil.copy(spec)); + // + // Specification specWithProps = ToGalTransformer.toGal(props); + // + // if (order != null) { + // CompositeBuilder.getInstance().decomposeWithOrder((GALTypeDeclaration) + // specWithProps.getTypes().get(0), order.clone()); + // } + // // compute constants + // Support constants = GALRewriter.flatten(specWithProps, true); + // + // File galout = new File( file.getParent() +"/" + + // file.getName().replace(".xml", ".gal")); + // fr.lip6.move.serialization.SerializationUtil.systemToFile(specWithProps, + // galout.getAbsolutePath()); + // } + // // Abstraction case + // if (file.getParent().contains("-COL-")) { + // ToGalTransformer.setWithAbstractColors(true); + // Properties props = + // PropertyParser.fileToProperties(file.getPath().toString(), + // EcoreUtil.copy(spec)); + // + // Specification specnocol = ToGalTransformer.toGal(props); + // Instantiator.instantiateParametersWithAbstractColors(specnocol); + // GALRewriter.flatten(specnocol, true); + // + // File galout = new File( file.getParent() +"/" + + // file.getName().replace(".xml", ".nocol.gal")); + // fr.lip6.move.serialization.SerializationUtil.systemToFile(specnocol, + // galout.getAbsolutePath()); + // + // ToGalTransformer.setWithAbstractColors(false); + // } + // + // } + // } + private String getOutputPath() { - return workFolder + "/"+ examination +".pnml.gal"; + return folder + "/" + examination + ".pnml.gal"; } public String outputGalFile() throws IOException { - String outpath = getOutputPath(); - if (! spec.getProperties().isEmpty()) { + String outpath = getOutputPath(); + if (!spec.getProperties().isEmpty()) { List props = new ArrayList(spec.getProperties()); spec.getProperties().clear(); SerializationUtil.systemToFile(spec, outpath); @@ -415,27 +236,50 @@ public String outputGalFile() throws IOException { } return outpath; } - - @Override - public void solve(Ender ender) { - final PipedInputStream pin = new PipedInputStream(4096); - PipedOutputStream pout= null; + + 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)); + + FutureTask ft = new FutureTask<>(interp); + try { - pout = new PipedOutputStream(pin); - } catch (IOException e1) { + new Thread(ft).start(); + + runnerThread.start(); + + runnerThread.join(); + + } catch (InterruptedException e) { + try { + runnerThread.interrupt(); + } catch (Exception ee) { + System.out.println("na pas pu interrpute"); + } + } catch (Exception e1) { e1.printStackTrace(); - return; + } finally { + try { + done = ft.get(); + } catch (InterruptedException | ExecutionException e) { + e.printStackTrace(); + } + } - - Set todoProps = reader.getSpec().getProperties().stream().map(p -> p.getName()).collect(Collectors.toSet()); - - runnerThread = new Thread (new ITSRealRunner(pout,cl)); - - ITSInterpreter interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, ender); - interp.setInput(pin); - itsReader = new Thread (interp); - itsReader.start(); - runnerThread.start(); + 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; + } -} +} \ No newline at end of file diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java index 245e1ae715..d2fbeb9328 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java @@ -24,7 +24,7 @@ import fr.lip6.move.gal.itstools.ProcessController.TimeOutException; import fr.lip6.move.gal.itstools.Runner; -public class LTSminRunner extends AbstractRunner implements IRunner { +public class LTSminRunner extends AbstractRunner { private String ltsminpath; private String solverPath; @@ -33,8 +33,10 @@ public class LTSminRunner extends AbstractRunner implements IRunner { private String workFolder; private Solver solver; private int timeout; + private List todo; - public LTSminRunner(String ltsminpath, String solverPath, Solver solver, boolean doPOR, boolean onlyGal, String workFolder, int timeout) { + public LTSminRunner(String ltsminpath, String solverPath, Solver solver, boolean doPOR, boolean onlyGal, + String workFolder, int timeout) { this.ltsminpath = ltsminpath; this.solverPath = solverPath; this.solver = solver; @@ -56,170 +58,168 @@ private static boolean isStutterInvariant(Property prop) { return true; } - @Override - public void solve(Ender ender) { - runnerThread = new Thread(new Runnable() { - - @Override - public void run() { - try { - System.out.println("Built C files in : \n" + new File(workFolder + "/")); - final Gal2PinsTransformerNext g2p = new Gal2PinsTransformerNext(); - - final Gal2SMTFrontEnd gsf = new Gal2SMTFrontEnd(solverPath, solver, 300000); - g2p.setSmtConfig(gsf); - g2p.initSolver(); - g2p.transform(spec, workFolder, doPOR); - - if (ltsminpath != null) { - { - // compile - CommandLine clgcc = new CommandLine(); - clgcc.setWorkingDir(new File(workFolder)); - clgcc.addArg("gcc"); - clgcc.addArg("-c"); - clgcc.addArg("-I" + ltsminpath + "/include"); - clgcc.addArg("-I."); - clgcc.addArg("-std=c99"); - clgcc.addArg("-fPIC"); - clgcc.addArg("-O3"); - clgcc.addArg("model.c"); - try { - System.out.println("Running compilation step : " + clgcc); - IStatus status = Runner.runTool(100, clgcc); - if (!status.isOK()) { - throw new RuntimeException("Could not compile executable ." + clgcc); - } - } catch (TimeOutException to) { - throw new RuntimeException( - "Compilation of executable timed out or was killed." + clgcc); - } + public void solve() { + try { + System.out.println("Built C files in : \n" + new File(workFolder + "/")); + final Gal2PinsTransformerNext g2p = new Gal2PinsTransformerNext(); + + final Gal2SMTFrontEnd gsf = new Gal2SMTFrontEnd(solverPath, solver, 300000); + g2p.setSmtConfig(gsf); + g2p.initSolver(); + g2p.transform(spec, workFolder, doPOR); + + if (ltsminpath != null) { + { + // compile + CommandLine clgcc = new CommandLine(); + clgcc.setWorkingDir(new File(workFolder)); + clgcc.addArg("gcc"); + clgcc.addArg("-c"); + clgcc.addArg("-I" + ltsminpath + "/include"); + clgcc.addArg("-I."); + clgcc.addArg("-std=c99"); + clgcc.addArg("-fPIC"); + clgcc.addArg("-O3"); + clgcc.addArg("model.c"); + try { + System.out.println("Running compilation step : " + clgcc); + IStatus status = Runner.runTool(100, clgcc); + if (!status.isOK()) { + throw new RuntimeException("Could not compile executable ." + clgcc); } - { - // link - CommandLine clgcc = new CommandLine(); - clgcc.setWorkingDir(new File(workFolder)); - clgcc.addArg("gcc"); - clgcc.addArg("-shared"); - clgcc.addArg("-o"); - clgcc.addArg("gal.so"); - clgcc.addArg("model.o"); - try { - System.out.println("Running link step : " + clgcc); - IStatus status = Runner.runTool(100, clgcc); - if (!status.isOK()) { - throw new RuntimeException("Could not link executable ." + clgcc); - } - } catch (TimeOutException to) { - throw new RuntimeException("Link of executable timed out or was killed." + clgcc); - } + } catch (TimeOutException to) { + throw new RuntimeException("Compilation of executable timed out or was killed." + clgcc); + } + } + { + // link + CommandLine clgcc = new CommandLine(); + clgcc.setWorkingDir(new File(workFolder)); + clgcc.addArg("gcc"); + clgcc.addArg("-shared"); + clgcc.addArg("-o"); + clgcc.addArg("gal.so"); + clgcc.addArg("model.o"); + try { + System.out.println("Running link step : " + clgcc); + IStatus status = Runner.runTool(100, clgcc); + if (!status.isOK()) { + throw new RuntimeException("Could not link executable ." + clgcc); } - if (onlyGal) { - System.out.println("Successfully built gal.so in :" + workFolder); - System.out.println("It has labels for :" + (spec.getProperties().stream() - .map(p -> p.getName().replaceAll("-", "")).collect(Collectors.toList()))); - return; + } catch (TimeOutException to) { + throw new RuntimeException("Link of executable timed out or was killed." + clgcc); + } + } + if (onlyGal) { + System.out.println("Successfully built gal.so in :" + workFolder); + System.out.println("It has labels for :" + (spec.getProperties().stream() + .map(p -> p.getName().replaceAll("-", "")).collect(Collectors.toList()))); + return; + } + todo = spec.getProperties().stream().map(p -> p.getName()).collect(Collectors.toList()); + for (Property prop : spec.getProperties()) { + if (doneProps.contains(prop.getName())) { + continue; + } + CommandLine ltsmin = new CommandLine(); + ltsmin.setWorkingDir(new File(workFolder)); + ltsmin.addArg(ltsminpath + "/bin/pins2lts-mc"); + ltsmin.addArg("./gal.so"); + + ltsmin.addArg("--threads=1"); + if (doPOR && isStutterInvariant(prop)) { + ltsmin.addArg("-p"); + ltsmin.addArg("--pins-guards"); + } + ltsmin.addArg("--when"); + boolean isdeadlock = false; + boolean isLTL = false; + if (prop.getName().contains("Deadlock")) { + ltsmin.addArg("-d"); + isdeadlock = true; + } else if (prop.getBody() instanceof LTLProp) { + ltsmin.addArg("--ltl"); + ltsmin.addArg(g2p.printLTLProperty((LTLProp) prop.getBody())); + // ltsmin.addArg("--ltl-semantics"); + // ltsmin.addArg("spin"); + + isLTL = true; + } else { + ltsmin.addArg("-i"); + ltsmin.addArg(prop.getName().replaceAll("-", "") + "==true"); + } + try { + ByteArrayOutputStream baos = new ByteArrayOutputStream(); + IStatus status = Runner.runTool(timeout, ltsmin, baos, true); + if (!status.isOK() && status.getCode() != 1) { + throw new RuntimeException( + "Unexpected exception when executing ltsmin :" + ltsmin + "\n" + status); } - List todo = spec.getProperties().stream().map(p -> p.getName()) - .collect(Collectors.toList()); - for (Property prop : spec.getProperties()) { - if (doneProps.contains(prop.getName())) { - continue; - } - CommandLine ltsmin = new CommandLine(); - ltsmin.setWorkingDir(new File(workFolder)); - ltsmin.addArg(ltsminpath + "/bin/pins2lts-mc"); - ltsmin.addArg("./gal.so"); - - ltsmin.addArg("--threads=1"); - if (doPOR && isStutterInvariant(prop)) { - ltsmin.addArg("-p"); - ltsmin.addArg("--pins-guards"); - } - ltsmin.addArg("--when"); - boolean isdeadlock = false; - boolean isLTL = false; - if (prop.getName().contains("Deadlock")) { - ltsmin.addArg("-d"); - isdeadlock = true; - } else if (prop.getBody() instanceof LTLProp) { - ltsmin.addArg("--ltl"); - ltsmin.addArg(g2p.printLTLProperty((LTLProp) prop.getBody())); - // ltsmin.addArg("--ltl-semantics"); - // ltsmin.addArg("spin"); - - isLTL = true; - } else { - ltsmin.addArg("-i"); - ltsmin.addArg(prop.getName().replaceAll("-", "") + "==true"); - } - try { - ByteArrayOutputStream baos = new ByteArrayOutputStream(); - IStatus status = Runner.runTool(timeout, ltsmin, baos, true); - if (!status.isOK() && status.getCode() != 1) { - throw new RuntimeException( - "Unexpected exception when executing ltsmin :" + ltsmin + "\n" + status); + boolean result; + String output = baos.toString(); + + if (isdeadlock) { + result = output.contains("Deadlock found") || output.contains("deadlock () found"); + } else if (isLTL) { + // accepting cycle = counter example to + // formula + result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting + // cycle found") + // ; + } else { + boolean hasViol = output.contains("Invariant violation"); + + if (hasViol) { + System.out.println("Found Violation"); + if (prop.getBody() instanceof ReachableProp) { + result = true; + } else if (prop.getBody() instanceof NeverProp) { + result = false; + } else if (prop.getBody() instanceof InvariantProp) { + result = false; + } else { + throw new RuntimeException("Unexpected property type " + prop); } - boolean result; - String output = baos.toString(); - - if (isdeadlock) { - result = output.contains("Deadlock found") || output.contains("deadlock () found"); - } else if (isLTL) { - // accepting cycle = counter example to - // formula - result = ! (status.getCode() == 1) ; // output.toLowerCase().contains("accepting cycle found") ; + } else { + System.out.println("Invariant validated"); + if (prop.getBody() instanceof ReachableProp) { + result = false; + } else if (prop.getBody() instanceof NeverProp) { + result = true; + } else if (prop.getBody() instanceof InvariantProp) { + result = true; } else { - boolean hasViol = output.contains("Invariant violation"); - - if (hasViol) { - System.out.println("Found Violation"); - if (prop.getBody() instanceof ReachableProp) { - result = true; - } else if (prop.getBody() instanceof NeverProp) { - result = false; - } else if (prop.getBody() instanceof InvariantProp) { - result = false; - } else { - throw new RuntimeException("Unexpected property type " + prop); - } - } else { - System.out.println("Invariant validated"); - if (prop.getBody() instanceof ReachableProp) { - result = false; - } else if (prop.getBody() instanceof NeverProp) { - result = true; - } else if (prop.getBody() instanceof InvariantProp) { - result = true; - } else { - throw new RuntimeException("Unexpected property type " + prop); - } - } + throw new RuntimeException("Unexpected property type " + prop); } - String ress = (result + "").toUpperCase(); - System.out.println("FORMULA " + prop.getName() + " " + ress - + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); - doneProps.add(prop.getName()); - } catch (TimeOutException to) { - System.err.println("LTSmin timed out on command " + ltsmin); - continue; } } - todo.removeAll(doneProps); - if (todo.isEmpty()) { - ender.killAll(); - } - + String ress = (result + "").toUpperCase(); + System.out.println("FORMULA " + prop.getName() + " " + ress + + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); + doneProps.add(prop.getName()); + } catch (TimeOutException to) { + System.err.println("LTSmin timed out on command " + ltsmin); + continue; } - } catch (IOException e) { - e.printStackTrace(); - } catch (RuntimeException e) { - System.err.println("LTS min runner thread failed on error :" + e); - e.printStackTrace(); } } + System.out.println("LTMIN HAS FINISHED !"); + } catch (IOException e) { + e.printStackTrace(); + } catch (RuntimeException e) { + System.err.println("LTS min runner thread failed on error :" + e); + e.printStackTrace(); + } - }); - runnerThread.start(); } + + 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; + } + } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java index 46734cc7cc..8fc09a43a0 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java @@ -40,24 +40,31 @@ public class MccTranslator { private String examination; private Support simplifiedVars = new Support(); private boolean isSafeNet = false; - + public MccTranslator(String pwd, String examination) { this.folder = pwd; this.examination = examination; } - public Specification getSpec() { return spec; } + /** - * Sets the spec and order attributes, spec is set to result of PNML tranlsation and order is set to null if no nupn/computed order is available. - * @param folder input folder absolute path, containing a model.pnml file - * @param reversible set to true to add P >= 0 constraints in guards of transitions adding to P, ensuring predecessor relation is inverse to succ. - * @throws IOException if file can't be found + * Sets the spec and order attributes, spec is set to result of PNML + * tranlsation and order is set to null if no nupn/computed order is + * available. + * + * @param folder + * input folder absolute path, containing a model.pnml file + * @param reversible + * set to true to add P >= 0 constraints in guards of transitions + * adding to P, ensuring predecessor relation is inverse to succ. + * @throws IOException + * if file can't be found */ public void transformPNML() throws IOException { - File ff = new File(folder+ "/"+ "model.pnml"); + File ff = new File(folder + "/" + "model.pnml"); if (ff != null && ff.exists()) { getLog().info("Parsing pnml file : " + ff.getAbsolutePath()); @@ -67,26 +74,26 @@ public void transformPNML() throws IOException { isSafeNet = trans.foundNupn(); // SerializationUtil.systemToFile(spec, ff.getPath() + ".gal"); if (spec.getMain() == null) { - spec.setMain(spec.getTypes().get(spec.getTypes().size()-1)); + spec.setMain(spec.getTypes().get(spec.getTypes().size() - 1)); } } else { - throw new IOException("Cannot open file "+ff.getAbsolutePath()); + throw new IOException("Cannot open file " + ff.getAbsolutePath()); } } - - + public boolean applyOrder(Support supp) { if (hasStructure() && canDecompose()) { getLog().info("Applying decomposition "); getLog().fine(order.toString()); Specification saved = EcoreUtil.copy(spec); try { - supp.addAll(CompositeBuilder.getInstance().decomposeWithOrder((GALTypeDeclaration) spec.getTypes().get(0), order)); + supp.addAll(CompositeBuilder.getInstance() + .decomposeWithOrder((GALTypeDeclaration) spec.getTypes().get(0), order)); } catch (Exception e) { getLog().warning("Could not apply decomposition. Using flat GAL structure."); e.printStackTrace(); - spec = saved ; - return false ; + spec = saved; + return false; } return true; } @@ -95,15 +102,13 @@ public boolean applyOrder(Support supp) { private static Logger getLog() { return Logger.getLogger("fr.lip6.move.gal"); - - } + } public boolean hasStructure() { return order != null; } - public void flattenSpec(boolean withHierarchy) { if (withHierarchy) { if (!applyOrder(simplifiedVars)) { @@ -114,15 +119,18 @@ public void flattenSpec(boolean withHierarchy) { } } - /** Job : parse the property files into the Specification. - * The examination determines what happens in here. - * @throws IOException */ + /** + * Job : parse the property files into the Specification. The examination + * determines what happens in here. + * + * @throws IOException + */ public void loadProperties() throws IOException { if (examination.equals("StateSpace")) { - return ; + return; } else { - String propff = folder +"/" + examination + ".xml"; - Properties props = PropertyParser.fileToProperties(propff , spec); + String propff = folder + "/" + examination + ".xml"; + Properties props = PropertyParser.fileToProperties(propff, spec); spec = ToGalTransformer.toGal(props); if (isSafeNet) { rewriteVariableComparisons(spec); @@ -133,7 +141,7 @@ public void loadProperties() throws IOException { private void rewriteVariableComparisons(Specification spec) { Map todo = new HashMap(); for (Property prop : spec.getProperties()) { - for (TreeIterator it = prop.getBody().eAllContents(); it.hasNext() ;) { + for (TreeIterator it = prop.getBody().eAllContents(); it.hasNext();) { EObject obj = it.next(); if (obj instanceof IntExpression) { it.prune(); @@ -145,12 +153,12 @@ private void rewriteVariableComparisons(Specification spec) { IntExpression l = cmp.getLeft(); IntExpression r = cmp.getRight(); switch (op) { - case GE : + case GE: l = cmp.getRight(); r = cmp.getLeft(); op = ComparisonOperators.LE; break; - case GT : + case GT: l = cmp.getRight(); r = cmp.getLeft(); op = ComparisonOperators.LT; @@ -159,42 +167,41 @@ private void rewriteVariableComparisons(Specification spec) { BooleanExpression res; // break into cases switch (op) { - case EQ : + case EQ: // both 0 or both 1 res = GF2.and( GF2.createComparison(EcoreUtil.copy(l), ComparisonOperators.EQ, GF2.constant(0)), GF2.createComparison(EcoreUtil.copy(r), ComparisonOperators.EQ, GF2.constant(0))); - res = GF2.or( res , GF2.and( + res = GF2.or(res, GF2.and( GF2.createComparison(EcoreUtil.copy(l), ComparisonOperators.EQ, GF2.constant(1)), GF2.createComparison(EcoreUtil.copy(r), ComparisonOperators.EQ, GF2.constant(1)))); break; - case NE : + case NE: // 01 or 10 res = GF2.and( GF2.createComparison(EcoreUtil.copy(l), ComparisonOperators.EQ, GF2.constant(0)), GF2.createComparison(EcoreUtil.copy(r), ComparisonOperators.EQ, GF2.constant(1))); - res = GF2.or( res , GF2.and( + res = GF2.or(res, GF2.and( GF2.createComparison(EcoreUtil.copy(l), ComparisonOperators.EQ, GF2.constant(1)), GF2.createComparison(EcoreUtil.copy(r), ComparisonOperators.EQ, GF2.constant(0)))); break; - case LT : + case LT: // 01 res = GF2.and( GF2.createComparison(EcoreUtil.copy(l), ComparisonOperators.EQ, GF2.constant(0)), GF2.createComparison(EcoreUtil.copy(r), ComparisonOperators.EQ, GF2.constant(1))); break; - case LE : + case LE: // 0* or 11 => r is 1 or l is 0 => 0* or *1 - res = GF2.or( + res = GF2.or( GF2.createComparison(EcoreUtil.copy(l), ComparisonOperators.EQ, GF2.constant(0)), - GF2.createComparison(EcoreUtil.copy(r), ComparisonOperators.EQ, GF2.constant(1)) - ); - break; - default : - throw new RuntimeException("Unexpected comparison operator in conversion "+ cmp); + GF2.createComparison(EcoreUtil.copy(r), ComparisonOperators.EQ, GF2.constant(1))); + break; + default: + throw new RuntimeException("Unexpected comparison operator in conversion " + cmp); } - todo.put(cmp,res); - + todo.put(cmp, res); + } it.prune(); } @@ -205,7 +212,6 @@ private void rewriteVariableComparisons(Specification spec) { } } - private boolean canDecompose() { boolean canDecompose = true; for (Property prop : spec.getProperties()) { @@ -216,15 +222,15 @@ private boolean canDecompose() { } return canDecompose; } - + private boolean containsAdditionOrComparison(Property prop) { - for (TreeIterator it = prop.eAllContents() ; it.hasNext() ; ) { + for (TreeIterator it = prop.eAllContents(); it.hasNext();) { EObject obj = it.next(); if (obj instanceof BinaryIntExpression) { - return true; + return true; } else if (obj instanceof Comparison) { Comparison cmp = (Comparison) obj; - if (! (cmp.getLeft() instanceof Constant || cmp.getRight() instanceof Constant)) { + if (!(cmp.getLeft() instanceof Constant || cmp.getRight() instanceof Constant)) { return true; } } @@ -232,12 +238,6 @@ private boolean containsAdditionOrComparison(Property prop) { return false; } - - - - - - public int countMissingTokens() { int addedTokens = 0; if ("StateSpace".equals(examination)) { @@ -254,26 +254,23 @@ public int countMissingTokens() { return addedTokens; } - - - public String getFolder() { return folder; } - /** removes any properties with addition in them, CTL parser can't deal with them currently. */ + /** + * removes any properties with addition in them, CTL parser can't deal with + * them currently. + */ public void removeAdditionProperties() { - spec.getProperties().removeIf( - prop -> - { - for (TreeIterator it = prop.eAllContents() ; it.hasNext() ; ) { - EObject obj = it.next(); - if (obj instanceof BinaryIntExpression) { - return true; - } - } - return false; + spec.getProperties().removeIf(prop -> { + for (TreeIterator it = prop.eAllContents(); it.hasNext();) { + EObject obj = it.next(); + if (obj instanceof BinaryIntExpression) { + return true; } - ); + } + return false; + }); } } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java index d0dde78af9..87022b19dd 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java @@ -1,21 +1,21 @@ package fr.lip6.move.gal.application; import java.util.Map; -import java.util.Set; import java.util.logging.Logger; import fr.lip6.move.gal.Property; -import fr.lip6.move.gal.Specification; import fr.lip6.move.gal.gal2smt.Gal2SMTFrontEnd; import fr.lip6.move.gal.gal2smt.ISMTObserver; import fr.lip6.move.gal.gal2smt.Result; import fr.lip6.move.gal.gal2smt.Solver; -public class SMTRunner extends AbstractRunner implements IRunner { - +public class SMTRunner extends AbstractRunner { + private String pwd; private String solverPath; private Solver solver; + private int nbsolve = 0; + private Map satresult; public SMTRunner(String pwd, String solverPath, Solver solver) { this.pwd = pwd; @@ -23,113 +23,57 @@ public SMTRunner(String pwd, String solverPath, Solver solver) { this.solver = solver; } - private Logger getLog() { + public Logger getLog() { return Logger.getLogger("fr.lip6.move.gal"); } - public Thread runSMT(final String pwd, final String solverPath, final Solver solver, final Specification z3Spec, - final Ender ender, Set doneProps) { - runnerThread = new Thread(new Runnable() { - int nbsolve = 0; - - @Override - public void run() { - Gal2SMTFrontEnd gsf = new Gal2SMTFrontEnd(solverPath, solver); - - gsf.addObserver(new ISMTObserver() { - @Override - public synchronized void notifyResult(Property prop, Result res, String desc) { - if (res == Result.TRUE || res == Result.FALSE) { - System.out.println( - "FORMULA " + prop.getName() + " " + res + " " + "TECHNIQUES SAT_SMT " + desc); - nbsolve++; - } else { - // a ambiguous verdict - // System.out.println("Obtained " + prop.getName() + - // " " + res +" TECHNIQUES SAT_SMT "+desc ); - } - } - }); - try { - Map satresult = gsf.checkProperties(z3Spec, pwd, doneProps); - // test for and handle properties - if (nbsolve == satresult.size()) { - getLog().info( - "SMT solved all " + nbsolve + " properties. Interrupting other analysis methods."); - ender.killAll(); - } else { - getLog().info("SMT solved " + nbsolve + "/ " + satresult.size() - + " properties. Interrupting other analysis methods."); - } - - } catch (Exception e) { - e.printStackTrace(); + public void solve() { + Gal2SMTFrontEnd gsf = new Gal2SMTFrontEnd(solverPath, solver); + gsf.addObserver(new ISMTObserver() { + public synchronized void notifyResult(Property prop, Result res, String desc) { + if (res == Result.TRUE || res == Result.FALSE) { + System.out.println("FORMULA " + prop.getName() + " " + res + " " + "TECHNIQUES SAT_SMT " + desc); + nbsolve++; + } else { + // a ambiguous verdict + // System.out.println("Obtained " + prop.getName() + + // " " + res +" TECHNIQUES SAT_SMT "+desc ); } - // List todel = new ArrayList(); - // for (Property prop : z3Spec.getProperties()) { - // if (satresult.get(prop.getName()) == Result.SAT) { - // todel.add(prop); - // } - // } - // specWithProps.getProperties().removeAll(todel); - // } } }); - runnerThread.setContextClassLoader(Thread.currentThread().getClass().getClassLoader()); - runnerThread.start(); - return runnerThread; - } - @Override - public void solve(Ender ender) { - runnerThread = new Thread(new Runnable() { - int nbsolve = 0; + try { + satresult = gsf.checkProperties(spec, pwd, doneProps); + } catch (Exception e) { + e.printStackTrace(); - @Override - public void run() { - Gal2SMTFrontEnd gsf = new Gal2SMTFrontEnd(solverPath, solver); + } - gsf.addObserver(new ISMTObserver() { - @Override - public synchronized void notifyResult(Property prop, Result res, String desc) { - if (res == Result.TRUE || res == Result.FALSE) { - System.out.println( - "FORMULA " + prop.getName() + " " + res + " " + "TECHNIQUES SAT_SMT " + desc); - nbsolve++; - } else { - // a ambiguous verdict - // System.out.println("Obtained " + prop.getName() + - // " " + res +" TECHNIQUES SAT_SMT "+desc ); - } - } - }); - try { - Map satresult = gsf.checkProperties(spec, pwd, doneProps); - // test for and handle properties - if (nbsolve == satresult.size()) { - getLog().info( - "SMT solved all " + nbsolve + " properties. Interrupting other analysis methods."); - ender.killAll(); - } else { - getLog().info("SMT solved " + nbsolve + "/ " + satresult.size() - + " properties. Interrupting other analysis methods."); - } + // List todel = new ArrayList(); + // for (Property prop : z3Spec.getProperties()) { + // if (satresult.get(prop.getName()) == Result.SAT) { + // todel.add(prop); + // } + // } + // specWithProps.getProperties().removeAll(todel); + // } + // __________________________ + // runnerThread.setContextClassLoader(Thread.currentThread().getClass().getClassLoader()); + 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; - } catch (Exception e) { - e.printStackTrace(); - } - // List todel = new ArrayList(); - // for (Property prop : z3Spec.getProperties()) { - // if (satresult.get(prop.getName()) == Result.SAT) { - // todel.add(prop); - // } - // } - // specWithProps.getProperties().removeAll(todel); - // } - } - }); - runnerThread.setContextClassLoader(Thread.currentThread().getClass().getClassLoader()); - runnerThread.start(); } } \ No newline at end of file From 4ea03c01670107b227416106f351ab9decd8e419 Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Wed, 21 Jun 2017 10:14:16 +0200 Subject: [PATCH 04/12] fixe dependecies --- .../fr.lip6.move.gal.application.pnmcc/META-INF/MANIFEST.MF | 2 +- .../src/Interpreter/CegarInterpreter.java | 5 ++--- .../src/Interpreter/ITSInterpreter.java | 4 ++-- .../src/fr/lip6/move/gal/application/AbstractRunner.java | 3 ++- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/META-INF/MANIFEST.MF b/pnmcc/fr.lip6.move.gal.application.pnmcc/META-INF/MANIFEST.MF index 8110d4672b..9b145e695e 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/META-INF/MANIFEST.MF +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/META-INF/MANIFEST.MF @@ -14,7 +14,7 @@ Require-Bundle: org.eclipse.core.runtime, fr.lip6.move.gal.gal2smt, fr.lip6.move.gal.gal2pins, lip6.smtlib.SMT, - fr.lip6.move.gal.itscl.concurrent + fr.lip6.move.gal.itscl.concurrent;bundle-version="1.0.0" Bundle-RequiredExecutionEnvironment: JavaSE-1.8 Bundle-ActivationPolicy: lazy Bundle-Vendor: LIP6 diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java index 09c04f6b7a..6d85255391 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java @@ -1,10 +1,9 @@ package Interpreter; - import fr.lip6.move.gal.itscl.modele.IListener; -import fr.lip6.move.gal.itscl.modele.Listener; +import fr.lip6.move.gal.itscl.modele.ListenerRunner; -public class CegarInterpreter extends Listener implements Runnable, IListener{ +public class CegarInterpreter extends ListenerRunner implements Runnable, IListener{ public CegarInterpreter(int pipeSize) { super(pipeSize); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java index b30a3e2044..4dd45dcb45 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java @@ -11,9 +11,9 @@ import fr.lip6.move.gal.Reference; import fr.lip6.move.gal.Constant; import fr.lip6.move.gal.application.MccTranslator; -import fr.lip6.move.gal.itscl.modele.Listener; +import fr.lip6.move.gal.itscl.modele.ListenerRunner; -public class ITSInterpreter extends Listener implements Callable { +public class ITSInterpreter extends ListenerRunner implements Callable { // private Map> boundProps; private String examination; diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java index a52493c6e6..6dac5fba6d 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java @@ -4,9 +4,10 @@ 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; public abstract class AbstractRunner implements IRunner { From e417dc4fb0278b8dcfaa7a95078de667adb7a5be Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Fri, 23 Jun 2017 12:04:18 +0200 Subject: [PATCH 05/12] setting interpreters for each runner --- .../src/Interpreter/CegarInterpreter.java | 8 ++-- .../src/Interpreter/LTSminInterpreter.java | 16 ++++++++ .../src/Interpreter/SMTInterpreter.java | 15 ++++++++ .../move/gal/application/AbstractRunner.java | 28 +++----------- .../move/gal/application/Application.java | 4 +- .../move/gal/application/CegarRunner.java | 12 +++++- .../lip6/move/gal/application/ITSRunner.java | 37 ++++++++++--------- .../move/gal/application/LTSminRunner.java | 26 +++++++++---- .../lip6/move/gal/application/SMTRunner.java | 30 ++++++++------- 9 files changed, 106 insertions(+), 70 deletions(-) create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java index 6d85255391..041b2c2b0f 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java +++ b/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 } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java new file mode 100644 index 0000000000..29b5a1e719 --- /dev/null +++ b/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; + } + +} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java new file mode 100644 index 0000000000..592b8e700a --- /dev/null +++ b/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; + } +} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java index 6dac5fba6d..3928920608 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java +++ b/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 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 doneProps) throws IOException { - this.spec = z3Spec; - this.doneProps = doneProps; - } - + public abstract void solve(); - public Specification getSpec() { - return spec; - } - - public Set getDoneProps() { - return doneProps; - } - public Boolean taskDone() { for (Property prop : getSpec().getProperties()) { if (!doneProps.contains(prop.getName())) { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index 403f537e08..3c00efe9bc 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java +++ b/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) { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java index 0bece6e3af..fd010c53ad 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java +++ b/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"); } + + } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java index 0ec3836cca..56a80d9200 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java @@ -237,27 +237,36 @@ 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 ft = new FutureTask<>(interp); + FutureTask 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(); @@ -265,21 +274,13 @@ public void solve() { 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; - - } - } \ No newline at end of file diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java index d2fbeb9328..4098360e91 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java +++ b/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; - } } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java index 87022b19dd..22983e1441 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java +++ b/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; - - } } \ No newline at end of file From d01b5ea93b2a62767797488b2d108a23fe8e431c Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Fri, 23 Jun 2017 16:10:22 +0200 Subject: [PATCH 06/12] wrong implementation of listeners I/O --- .../src/Interpreter/CegarInterpreter.java | 4 +- .../src/Interpreter/IInterpreter.java | 6 ++ .../src/Interpreter/ITSInterpreter.java | 20 ++++--- .../src/Interpreter/LTSminInterpreter.java | 50 ++++++++++++++++- .../src/Interpreter/SMTInterpreter.java | 4 +- .../move/gal/application/AbstractRunner.java | 44 ++++++++++++--- .../move/gal/application/Application.java | 2 + .../move/gal/application/CegarRunner.java | 3 +- .../lip6/move/gal/application/ITSRunner.java | 18 +++--- .../move/gal/application/LTSminRunner.java | 55 ++----------------- 10 files changed, 121 insertions(+), 85 deletions(-) create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/IInterpreter.java diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java index 041b2c2b0f..37a425d92b 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java @@ -1,8 +1,8 @@ package Interpreter; -import fr.lip6.move.gal.itscl.modele.ListenerRunner; +import fr.lip6.move.gal.itscl.modele.ItsInterpreter; -public class CegarInterpreter extends ListenerRunner{ +public class CegarInterpreter extends ItsInterpreter{ public CegarInterpreter(int pipeSize) { super(pipeSize); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/IInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/IInterpreter.java new file mode 100644 index 0000000000..67a5826890 --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/IInterpreter.java @@ -0,0 +1,6 @@ +package Interpreter; + +public interface IInterpreter { + + +} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java index 4dd45dcb45..e912b1e77e 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java @@ -2,7 +2,6 @@ import java.io.IOException; import java.util.Set; -import java.util.concurrent.Callable; import org.eclipse.emf.common.util.TreeIterator; import org.eclipse.emf.ecore.EObject; @@ -11,9 +10,10 @@ import fr.lip6.move.gal.Reference; import fr.lip6.move.gal.Constant; import fr.lip6.move.gal.application.MccTranslator; -import fr.lip6.move.gal.itscl.modele.ListenerRunner; +import fr.lip6.move.gal.itscl.modele.IListener; +import fr.lip6.move.gal.itscl.modele.ItsInterpreter; -public class ITSInterpreter extends ListenerRunner implements Callable { +public class ITSInterpreter implements IListener { // private Map> boundProps; private String examination; @@ -21,10 +21,10 @@ public class ITSInterpreter extends ListenerRunner implements Callable private MccTranslator reader; private Set seen; private Set todoProps; + private ItsInterpreter buffWriteInOut; public ITSInterpreter(String examination, boolean withStructure, MccTranslator reader, Set doneProps, Set todoProps, int pipeSize) { - super(pipeSize); this.examination = examination; this.withStructure = withStructure; this.reader = reader; @@ -32,9 +32,13 @@ public ITSInterpreter(String examination, boolean withStructure, MccTranslator r this.todoProps = todoProps; } - public Boolean call() throws Exception { + public void setBuffWriterInOut(ItsInterpreter b) { + this.buffWriteInOut = b; + } + + public Object call() throws Exception { try { - for (String line = ""; line != null; line = in.readLine()) { + for (String line = ""; line != null; line = buffWriteInOut.readLine()) { System.out.println(line); // stdOutput.toString().split("\\r?\\n")) ; if (line.matches("Max variable value.*")) { @@ -161,7 +165,7 @@ public Boolean call() throws Exception { } } } - in.close(); + buffWriteInOut.closeIn(); } catch (NumberFormatException e) { e.printStackTrace(); return false; @@ -169,7 +173,7 @@ public Boolean call() throws Exception { e.printStackTrace(); return false; } - closePinPout(); + buffWriteInOut.closePinPout(); if (seen.containsAll(todoProps)) { return true; diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java index 29b5a1e719..efd864e8e8 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java @@ -1,15 +1,59 @@ package Interpreter; -import fr.lip6.move.gal.itscl.modele.ListenerRunner; +import fr.lip6.move.gal.InvariantProp; +import fr.lip6.move.gal.NeverProp; +import fr.lip6.move.gal.ReachableProp; +import fr.lip6.move.gal.itscl.modele.ItsInterpreter; -public class LTSminInterpreter extends ListenerRunner { +public class LTSminInterpreter extends ItsInterpreter { public LTSminInterpreter() { super(4096); } public Boolean call() throws Exception { - // TODO Auto-generated method stub + boolean result; + String output = getPout().toString(); + + if (isdeadlock) { + result = output.contains("Deadlock found") || output.contains("deadlock () found"); + } else if (isLTL) { + // accepting cycle = counter example to + // formula + result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting + // cycle found") + // ; + } else { + boolean hasViol = output.contains("Invariant violation"); + + if (hasViol) { + System.out.println("Found Violation"); + if (prop.getBody() instanceof ReachableProp) { + result = true; + } else if (prop.getBody() instanceof NeverProp) { + result = false; + } else if (prop.getBody() instanceof InvariantProp) { + result = false; + } else { + throw new RuntimeException("Unexpected property type " + prop); + } + } else { + System.out.println("Invariant validated"); + if (prop.getBody() instanceof ReachableProp) { + result = false; + } else if (prop.getBody() instanceof NeverProp) { + result = true; + } else if (prop.getBody() instanceof InvariantProp) { + result = true; + } else { + throw new RuntimeException("Unexpected property type " + prop); + } + } + } + String ress = (result + "").toUpperCase(); + System.out.println( + "FORMULA " + prop.getName() + " " + ress + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); + doneProps.add(prop.getName()); return null; } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java index 592b8e700a..76fc7795d0 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java @@ -1,8 +1,8 @@ package Interpreter; -import fr.lip6.move.gal.itscl.modele.ListenerRunner; +import fr.lip6.move.gal.itscl.modele.ItsInterpreter; -public class SMTInterpreter extends ListenerRunner { +public class SMTInterpreter extends ItsInterpreter { public SMTInterpreter() { super(4096); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java index 3928920608..417e70deba 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java @@ -1,24 +1,50 @@ package fr.lip6.move.gal.application; +import java.io.IOException; +import java.util.Set; +import java.util.concurrent.ConcurrentHashMap; 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; +import fr.lip6.move.gal.itscl.modele.ItsInterpreter; +public abstract class AbstractRunner implements IRunner { -public abstract class AbstractRunner extends Problem implements IRunner { + protected Specification spec; + protected Set doneProps; + protected IListener interp; + protected ItsInterpreter bufferWIO= new ItsInterpreter(4096); - protected IListener listener; - - public AbstractRunner() { - super(); + public Specification getSpec() { + return spec; } - - public void setListener(IListener l){ - this.listener=l; + + public Set getDoneProps() { + return doneProps; + } + public void setBuffWriterInOut(ItsInterpreter b){ + bufferWIO=b; + } + + public void configure(Specification z3Spec, Set doneProps) throws IOException { + this.spec = z3Spec; + this.doneProps = doneProps; + } + + public void configure(Specification spec) { + try { + configure(spec, ConcurrentHashMap.newKeySet()); + } catch (IOException e) { + e.printStackTrace(); + } } + public IListener getInterpreter() { + return interp; + } + public abstract void solve(); public Boolean taskDone() { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index 3c00efe9bc..80d212beb6 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java @@ -185,6 +185,8 @@ public Object start(IApplicationContext context) throws Exception { itsRunner = new ITSRunner(examination, reader, doITS, onlyGal, reader.getFolder()); itsRunner.configure(reader.getSpec(), doneProps); itsRunner.setInterpreter(); + chRunner.addInterpreter(itsRunner.getInterpreter()); + } if (doITS) { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java index fd010c53ad..298ee0da8a 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java @@ -5,7 +5,6 @@ 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; @@ -20,7 +19,6 @@ public class CegarRunner extends AbstractRunner { public CegarRunner(String pwd) { this.pwd = pwd; - setListener(new CegarInterpreter(4096)); } private static Logger getLog() { @@ -28,6 +26,7 @@ private static Logger getLog() { } + public Boolean taskDone() { for (Property prop : todoProps) { if (!doneProps.contains(prop.getName())) { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java index 56a80d9200..c78551f2ba 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java @@ -13,6 +13,7 @@ import Interpreter.ITSInterpreter; import fr.lip6.move.gal.Property; import fr.lip6.move.gal.Specification; +import fr.lip6.move.gal.itscl.modele.ItsInterpreter; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.CommandLineBuilder; import fr.lip6.move.gal.itstools.Runner; @@ -245,17 +246,14 @@ public Boolean taskDone() { 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()); - Thread runnerThread = new Thread(new ITSRealRunner(listener.getPout(), cl)); - - FutureTask ft = new FutureTask<>(listener); + Thread runnerThread = new Thread(new ITSRealRunner(bufferWIO.getPout(), cl)); + interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, 4096); + + FutureTask ft = new FutureTask<>(interp); try { new Thread(ft).start(); @@ -272,9 +270,9 @@ public void solve() { e1.printStackTrace(); } finally { try { - done = ft.get(); + done = (boolean) ft.get(); } catch (InterruptedException | ExecutionException e) { - }finally{ + } finally { if (!ft.isDone()) ft.cancel(true); } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java index 4098360e91..290404043c 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java @@ -72,16 +72,12 @@ public Boolean taskDone() { 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 + "/")); final Gal2PinsTransformerNext g2p = new Gal2PinsTransformerNext(); - final Gal2SMTFrontEnd gsf = new Gal2SMTFrontEnd(solverPath, solver, 300000); + g2p.setSmtConfig(gsf); g2p.initSolver(); g2p.transform(spec, workFolder, doPOR); @@ -135,6 +131,7 @@ public void solve() { return; } todo = spec.getProperties().stream().map(p -> p.getName()).collect(Collectors.toList()); + for (Property prop : spec.getProperties()) { if (doneProps.contains(prop.getName())) { continue; @@ -167,54 +164,14 @@ public void solve() { ltsmin.addArg(prop.getName().replaceAll("-", "") + "==true"); } try { - ByteArrayOutputStream baos = new ByteArrayOutputStream(); - IStatus status = Runner.runTool(timeout, ltsmin, baos, true); + IStatus status = Runner.runTool(timeout, ltsmin, bufferWIO.getPout(), true); if (!status.isOK() && status.getCode() != 1) { throw new RuntimeException( "Unexpected exception when executing ltsmin :" + ltsmin + "\n" + status); } - boolean result; - String output = baos.toString(); - - if (isdeadlock) { - result = output.contains("Deadlock found") || output.contains("deadlock () found"); - } else if (isLTL) { - // accepting cycle = counter example to - // formula - result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting - // cycle found") - // ; - } else { - boolean hasViol = output.contains("Invariant violation"); - - if (hasViol) { - System.out.println("Found Violation"); - if (prop.getBody() instanceof ReachableProp) { - result = true; - } else if (prop.getBody() instanceof NeverProp) { - result = false; - } else if (prop.getBody() instanceof InvariantProp) { - result = false; - } else { - throw new RuntimeException("Unexpected property type " + prop); - } - } else { - System.out.println("Invariant validated"); - if (prop.getBody() instanceof ReachableProp) { - result = false; - } else if (prop.getBody() instanceof NeverProp) { - result = true; - } else if (prop.getBody() instanceof InvariantProp) { - result = true; - } else { - throw new RuntimeException("Unexpected property type " + prop); - } - } - } - String ress = (result + "").toUpperCase(); - System.out.println("FORMULA " + prop.getName() + " " + ress - + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); - doneProps.add(prop.getName()); + + LTSminInterpreter interp= new LTSminInterpreter(isdeadlock,isLTL,status,); + } catch (TimeOutException to) { System.err.println("LTSmin timed out on command " + ltsmin); continue; From e6311ab562c8af5a69c0d895ddb76d46e99cdb6f Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Fri, 23 Jun 2017 17:49:42 +0200 Subject: [PATCH 07/12] reorder the struct of interprete observable --- .../src/Interpreter/LTSminInterpreter.java | 120 +++++++++++------- .../src/Interpreter/SMTInterpreter.java | 4 - .../move/gal/application/AbstractRunner.java | 20 +-- .../move/gal/application/Application.java | 2 - .../lip6/move/gal/application/ITSRunner.java | 24 ++-- .../move/gal/application/LTSminRunner.java | 26 ++-- 6 files changed, 111 insertions(+), 85 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java index efd864e8e8..8116793946 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java @@ -1,59 +1,93 @@ package Interpreter; +import java.util.Set; + +import org.eclipse.core.runtime.IStatus; + import fr.lip6.move.gal.InvariantProp; import fr.lip6.move.gal.NeverProp; +import fr.lip6.move.gal.Property; import fr.lip6.move.gal.ReachableProp; +import fr.lip6.move.gal.application.LTSminRunner; +import fr.lip6.move.gal.itscl.modele.IListener; import fr.lip6.move.gal.itscl.modele.ItsInterpreter; -public class LTSminInterpreter extends ItsInterpreter { +public class LTSminInterpreter implements IListener{ - public LTSminInterpreter() { - super(4096); + private IStatus status; + private boolean isLTL; + private boolean isdeadlock; + private ItsInterpreter bufferWIO; + private Property prop; + private Set doneProps; + private LTSminRunner ltsRunner; + + public LTSminInterpreter(LTSminRunner ltSminRunner) { + this.ltsRunner = ltSminRunner; + this.doneProps=ltsRunner.getDoneProps(); } - public Boolean call() throws Exception { - boolean result; - String output = getPout().toString(); - - if (isdeadlock) { - result = output.contains("Deadlock found") || output.contains("deadlock () found"); - } else if (isLTL) { - // accepting cycle = counter example to - // formula - result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting - // cycle found") - // ; - } else { - boolean hasViol = output.contains("Invariant violation"); - - if (hasViol) { - System.out.println("Found Violation"); - if (prop.getBody() instanceof ReachableProp) { - result = true; - } else if (prop.getBody() instanceof NeverProp) { - result = false; - } else if (prop.getBody() instanceof InvariantProp) { - result = false; - } else { - throw new RuntimeException("Unexpected property type " + prop); - } - } else { - System.out.println("Invariant validated"); - if (prop.getBody() instanceof ReachableProp) { - result = false; - } else if (prop.getBody() instanceof NeverProp) { - result = true; - } else if (prop.getBody() instanceof InvariantProp) { - result = true; - } else { - throw new RuntimeException("Unexpected property type " + prop); + public void configure(boolean isdeadlock, boolean isLTL, IStatus status, ItsInterpreter bufferWIO, Property prop) { + this.isdeadlock = isdeadlock; + this.isLTL = isLTL; + this.status = status; + this.bufferWIO = bufferWIO; + this.prop = prop; + } + + public Object call() { + + try { + while (true) { + boolean result; + String output = bufferWIO.getPout().toString(); + for (String line = ""; line != null; line = bufferWIO.readLine()) { + if (isdeadlock) { + result = output.contains("Deadlock found") || output.contains("deadlock () found"); + } else if (isLTL) { + // accepting cycle = counter example to + // formula + result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting + // cycle found") + // ; + } else { + boolean hasViol = output.contains("Invariant violation"); + + if (hasViol) { + System.out.println("Found Violation"); + if (prop.getBody() instanceof ReachableProp) { + result = true; + } else if (prop.getBody() instanceof NeverProp) { + result = false; + } else if (prop.getBody() instanceof InvariantProp) { + result = false; + } else { + throw new RuntimeException("Unexpected property type " + prop); + } + } else { + System.out.println("Invariant validated"); + if (prop.getBody() instanceof ReachableProp) { + result = false; + } else if (prop.getBody() instanceof NeverProp) { + result = true; + } else if (prop.getBody() instanceof InvariantProp) { + result = true; + } else { + throw new RuntimeException("Unexpected property type " + prop); + } + } + } + String ress = (result + "").toUpperCase(); + System.out.println("FORMULA " + prop.getName() + " " + ress + + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); + doneProps.add(prop.getName()); } } + } catch (Exception e) { + System.out.println("im her in catcher "); + } finally { + ltsRunner.setDoneProps(doneProps); } - String ress = (result + "").toUpperCase(); - System.out.println( - "FORMULA " + prop.getName() + " " + ress + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); - doneProps.add(prop.getName()); return null; } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java index 76fc7795d0..1ea6fb1fb3 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java @@ -4,12 +4,8 @@ public class SMTInterpreter extends ItsInterpreter { - public SMTInterpreter() { - super(4096); - } public Boolean call() throws Exception { - // TODO Auto-generated method stub return null; } } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java index 417e70deba..e755ae290a 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java @@ -6,26 +6,32 @@ 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.InterpreteObservable; import fr.lip6.move.gal.itscl.modele.ItsInterpreter; public abstract class AbstractRunner implements IRunner { protected Specification spec; protected Set doneProps; - protected IListener interp; - protected ItsInterpreter bufferWIO= new ItsInterpreter(4096); + protected InterpreteObservable obsRunner; + protected ItsInterpreter bufferWIO; public Specification getSpec() { return spec; } + public void setObservable(InterpreteObservable ob){ + this.obsRunner=ob; + } + + public Set getDoneProps() { return doneProps; } - public void setBuffWriterInOut(ItsInterpreter b){ - bufferWIO=b; + + public void setDoneProps(Set d){ + doneProps=d; } public void configure(Specification z3Spec, Set doneProps) throws IOException { @@ -41,10 +47,6 @@ public void configure(Specification spec) { } } - public IListener getInterpreter() { - return interp; - } - public abstract void solve(); public Boolean taskDone() { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index 80d212beb6..71c9f23207 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java @@ -184,8 +184,6 @@ 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(); - chRunner.addInterpreter(itsRunner.getInterpreter()); } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java index c78551f2ba..d35c4f3b55 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java @@ -13,6 +13,7 @@ import Interpreter.ITSInterpreter; import fr.lip6.move.gal.Property; import fr.lip6.move.gal.Specification; +import fr.lip6.move.gal.itscl.modele.InterpreteObservable; import fr.lip6.move.gal.itscl.modele.ItsInterpreter; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.CommandLineBuilder; @@ -239,6 +240,11 @@ public String outputGalFile() throws IOException { } public Boolean taskDone() { + try{ + while(done==2) + Thread.sleep(1000); + } + if (done) { System.out.println("tasks resolved Its"); return true; @@ -246,17 +252,16 @@ public Boolean taskDone() { System.out.println("tasks not all resolved Its"); return false; } - + public void solve() { todoProps = reader.getSpec().getProperties().stream().map(p -> p.getName()).collect(Collectors.toSet()); Thread runnerThread = new Thread(new ITSRealRunner(bufferWIO.getPout(), cl)); - interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, 4096); - - FutureTask ft = new FutureTask<>(interp); + interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, 4096, this); + + InterpreteObservable.add(interp); try { - new Thread(ft).start(); runnerThread.start(); runnerThread.join(); @@ -268,15 +273,6 @@ public void solve() { } } catch (Exception e1) { e1.printStackTrace(); - } finally { - try { - done = (boolean) ft.get(); - } catch (InterruptedException | ExecutionException e) { - } finally { - if (!ft.isDone()) - ft.cancel(true); - } - } System.out.println("ITS RUNNER FINISH !"); } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java index 290404043c..2d49b931c9 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java @@ -1,6 +1,5 @@ package fr.lip6.move.gal.application; -import java.io.ByteArrayOutputStream; import java.io.File; import java.io.IOException; import java.util.List; @@ -12,15 +11,13 @@ import Interpreter.LTSminInterpreter; import fr.lip6.move.gal.Comparison; -import fr.lip6.move.gal.InvariantProp; import fr.lip6.move.gal.LTLNext; import fr.lip6.move.gal.LTLProp; -import fr.lip6.move.gal.NeverProp; import fr.lip6.move.gal.Property; -import fr.lip6.move.gal.ReachableProp; import fr.lip6.move.gal.gal2pins.Gal2PinsTransformerNext; import fr.lip6.move.gal.gal2smt.Gal2SMTFrontEnd; import fr.lip6.move.gal.gal2smt.Solver; +import fr.lip6.move.gal.itscl.modele.ItsInterpreter; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.ProcessController.TimeOutException; import fr.lip6.move.gal.itstools.Runner; @@ -58,14 +55,14 @@ private static boolean isStutterInvariant(Property prop) { } return true; } - + public void setInterpreter() { - + } public Boolean taskDone() { todo.removeAll(doneProps); - if(todo.isEmpty()) + if (todo.isEmpty()) System.out.println("Ltsmin has all solved"); else System.out.println("Ltsmin didnt solve everything"); @@ -77,7 +74,7 @@ public void solve() { System.out.println("Built C files in : \n" + new File(workFolder + "/")); final Gal2PinsTransformerNext g2p = new Gal2PinsTransformerNext(); final Gal2SMTFrontEnd gsf = new Gal2SMTFrontEnd(solverPath, solver, 300000); - + g2p.setSmtConfig(gsf); g2p.initSolver(); g2p.transform(spec, workFolder, doPOR); @@ -131,7 +128,11 @@ public void solve() { return; } todo = spec.getProperties().stream().map(p -> p.getName()).collect(Collectors.toList()); - + + bufferWIO = new ItsInterpreter(); + LTSminInterpreter interp = new LTSminInterpreter(this); + obsRunner.attach(interp); + for (Property prop : spec.getProperties()) { if (doneProps.contains(prop.getName())) { continue; @@ -169,9 +170,9 @@ public void solve() { throw new RuntimeException( "Unexpected exception when executing ltsmin :" + ltsmin + "\n" + status); } - - LTSminInterpreter interp= new LTSminInterpreter(isdeadlock,isLTL,status,); - + + interp.configure(isdeadlock, isLTL, status, bufferWIO, prop); + } catch (TimeOutException to) { System.err.println("LTSmin timed out on command " + ltsmin); continue; @@ -188,5 +189,4 @@ public void solve() { } - } From 1478fa7824684fe74c5b28be8b715671d5917cc2 Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Mon, 26 Jun 2017 16:22:17 +0200 Subject: [PATCH 08/12] separe the running solver of output interpretation --- .../src/Interpreter/ITSInterpreter.java | 17 +-- .../src/Interpreter/LTSminInterpreter.java | 101 +++++++++--------- .../move/gal/application/AbstractRunner.java | 8 +- .../move/gal/application/Application.java | 16 ++- .../lip6/move/gal/application/ITSRunner.java | 19 ++-- .../move/gal/application/LTSminRunner.java | 21 ++-- 6 files changed, 94 insertions(+), 88 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java index e912b1e77e..bb1f5b1243 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java @@ -9,6 +9,7 @@ import fr.lip6.move.gal.Property; import fr.lip6.move.gal.Reference; import fr.lip6.move.gal.Constant; +import fr.lip6.move.gal.application.ITSRunner; import fr.lip6.move.gal.application.MccTranslator; import fr.lip6.move.gal.itscl.modele.IListener; import fr.lip6.move.gal.itscl.modele.ItsInterpreter; @@ -22,23 +23,23 @@ public class ITSInterpreter implements IListener { private Set seen; private Set todoProps; private ItsInterpreter buffWriteInOut; + private ITSRunner itsRunner; public ITSInterpreter(String examination, boolean withStructure, MccTranslator reader, Set doneProps, - Set todoProps, int pipeSize) { + Set todoProps, ITSRunner itsRunner) { this.examination = examination; this.withStructure = withStructure; this.reader = reader; this.seen = doneProps; this.todoProps = todoProps; - } - - public void setBuffWriterInOut(ItsInterpreter b) { - this.buffWriteInOut = b; + this.itsRunner=itsRunner; } public Object call() throws Exception { try { - for (String line = ""; line != null; line = buffWriteInOut.readLine()) { + + for (String line = ""; line != null; line = buffWriteInOut.getIn().readLine()) { + System.out.println(line); // stdOutput.toString().split("\\r?\\n")) ; if (line.matches("Max variable value.*")) { @@ -166,6 +167,7 @@ public Object call() throws Exception { } } buffWriteInOut.closeIn(); + } catch (NumberFormatException e) { e.printStackTrace(); return false; @@ -176,7 +178,8 @@ public Object call() throws Exception { buffWriteInOut.closePinPout(); if (seen.containsAll(todoProps)) { - return true; + System.out.println("whi here"); + itsRunner.setDone(); } return false; } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java index 8116793946..145b6f978a 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java @@ -1,5 +1,6 @@ package Interpreter; +import java.io.IOException; import java.util.Set; import org.eclipse.core.runtime.IStatus; @@ -12,7 +13,7 @@ import fr.lip6.move.gal.itscl.modele.IListener; import fr.lip6.move.gal.itscl.modele.ItsInterpreter; -public class LTSminInterpreter implements IListener{ +public class LTSminInterpreter implements IListener { private IStatus status; private boolean isLTL; @@ -22,73 +23,73 @@ public class LTSminInterpreter implements IListener{ private Set doneProps; private LTSminRunner ltsRunner; - public LTSminInterpreter(LTSminRunner ltSminRunner) { + public LTSminInterpreter(LTSminRunner ltSminRunner, ItsInterpreter bufferWIO) { this.ltsRunner = ltSminRunner; - this.doneProps=ltsRunner.getDoneProps(); + this.doneProps = ltsRunner.getDoneProps(); + this.bufferWIO = bufferWIO; } - public void configure(boolean isdeadlock, boolean isLTL, IStatus status, ItsInterpreter bufferWIO, Property prop) { + public void configure(boolean isdeadlock, boolean isLTL, IStatus status, Property prop) { this.isdeadlock = isdeadlock; this.isLTL = isLTL; this.status = status; - this.bufferWIO = bufferWIO; this.prop = prop; } - public Object call() { + public Object call() throws IOException { + + while (true) { + boolean result; + for (String line = ""; line != null; line = bufferWIO.getIn().readLine()) { + System.out.println(" buffer did read : " + line.length()); + if (isdeadlock) { + result = line.contains("Deadlock found") || line.contains("deadlock () found"); + } else if (isLTL) { + // accepting cycle = counter example to + // formula + result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting + // cycle found") + // ; + } else { + boolean hasViol = line.contains("Invariant violation"); - try { - while (true) { - boolean result; - String output = bufferWIO.getPout().toString(); - for (String line = ""; line != null; line = bufferWIO.readLine()) { - if (isdeadlock) { - result = output.contains("Deadlock found") || output.contains("deadlock () found"); - } else if (isLTL) { - // accepting cycle = counter example to - // formula - result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting - // cycle found") - // ; + if (hasViol) { + System.out.println("Found Violation"); + if (prop.getBody() instanceof ReachableProp) { + result = true; + } else if (prop.getBody() instanceof NeverProp) { + result = false; + } else if (prop.getBody() instanceof InvariantProp) { + result = false; + } else { + throw new RuntimeException("Unexpected property type " + prop); + } } else { - boolean hasViol = output.contains("Invariant violation"); + System.out.println("Invariant validated"); + + if (prop.getBody() instanceof ReachableProp) { + result = false; + + } else if (prop.getBody() instanceof NeverProp) { + result = true; + + } else if (prop.getBody() instanceof InvariantProp) { + result = true; - if (hasViol) { - System.out.println("Found Violation"); - if (prop.getBody() instanceof ReachableProp) { - result = true; - } else if (prop.getBody() instanceof NeverProp) { - result = false; - } else if (prop.getBody() instanceof InvariantProp) { - result = false; - } else { - throw new RuntimeException("Unexpected property type " + prop); - } } else { - System.out.println("Invariant validated"); - if (prop.getBody() instanceof ReachableProp) { - result = false; - } else if (prop.getBody() instanceof NeverProp) { - result = true; - } else if (prop.getBody() instanceof InvariantProp) { - result = true; - } else { - throw new RuntimeException("Unexpected property type " + prop); - } + throw new RuntimeException("Unexpected property type " + prop); } } - String ress = (result + "").toUpperCase(); - System.out.println("FORMULA " + prop.getName() + " " + ress - + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); - doneProps.add(prop.getName()); + } + String ress = (result + "").toUpperCase(); + System.out.println( + "FORMULA " + prop.getName() + " " + ress + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); + doneProps.add(prop.getName()); + synchronized (ltsRunner) { + ltsRunner.setDoneProps(doneProps); } } - } catch (Exception e) { - System.out.println("im her in catcher "); - } finally { - ltsRunner.setDoneProps(doneProps); } - return null; } } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java index e755ae290a..4efb7db5f6 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java @@ -14,15 +14,15 @@ public abstract class AbstractRunner implements IRunner { protected Specification spec; protected Set doneProps; - protected InterpreteObservable obsRunner; - protected ItsInterpreter bufferWIO; + protected InterpreteObservable inRunner; + protected ItsInterpreter bufferWIO = new ItsInterpreter(); public Specification getSpec() { return spec; } - public void setObservable(InterpreteObservable ob){ - this.obsRunner=ob; + public void setInterprete(InterpreteObservable ob){ + this.inRunner=ob; } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index 71c9f23207..468d197c11 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java @@ -23,7 +23,9 @@ import fr.lip6.move.gal.gal2smt.Solver; import fr.lip6.move.gal.itscl.adaptor.InteractApplication; import fr.lip6.move.gal.itscl.modele.IRunner; +import fr.lip6.move.gal.itscl.modele.InterpreteObservable; import fr.lip6.move.gal.itscl.modele.SolverObservable; +import fr.lip6.move.gal.itscl.modele.Synchronizer; import fr.lip6.move.serialization.SerializationUtil; /** @@ -60,7 +62,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______"); + System.out.println("im here______"); String pwd = null; String examination = null; String z3path = null; @@ -126,9 +128,12 @@ public Object start(IApplicationContext context) throws Exception { Set doneProps = ConcurrentHashMap.newKeySet(); reader.loadProperties(); - - SolverObservable chRunner = new SolverObservable(); - + Synchronizer sync = new Synchronizer(); + SolverObservable chRunner = new SolverObservable(sync); + InterpreteObservable inRunner = new InterpreteObservable(sync); + if(inRunner==null){ + System.out.println("is null"); + } if (examination.equals("StateSpace")) { reader.flattenSpec(true); @@ -184,7 +189,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.setInterprete(inRunner); } if (doITS) { @@ -206,6 +211,7 @@ public Object start(IApplicationContext context) throws Exception { ltsminRunner = new LTSminRunner(ltsminpath, solverPath, solver, doPOR, onlyGal, reader.getFolder(), 3600 / reader.getSpec().getProperties().size()); ltsminRunner.configure(reader.getSpec(), doneProps); + ltsminRunner.setInterprete(inRunner); chRunner.attach(InteractApplication.add(ltsminRunner)); } } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java index d35c4f3b55..1407564c3a 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java @@ -6,15 +6,11 @@ import java.util.ArrayList; import java.util.List; import java.util.Set; -import java.util.concurrent.ExecutionException; -import java.util.concurrent.FutureTask; import java.util.stream.Collectors; import Interpreter.ITSInterpreter; import fr.lip6.move.gal.Property; import fr.lip6.move.gal.Specification; -import fr.lip6.move.gal.itscl.modele.InterpreteObservable; -import fr.lip6.move.gal.itscl.modele.ItsInterpreter; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.CommandLineBuilder; import fr.lip6.move.gal.itstools.Runner; @@ -240,10 +236,6 @@ public String outputGalFile() throws IOException { } public Boolean taskDone() { - try{ - while(done==2) - Thread.sleep(1000); - } if (done) { System.out.println("tasks resolved Its"); @@ -253,13 +245,14 @@ public Boolean taskDone() { return false; } + public void solve() { todoProps = reader.getSpec().getProperties().stream().map(p -> p.getName()).collect(Collectors.toSet()); Thread runnerThread = new Thread(new ITSRealRunner(bufferWIO.getPout(), cl)); - interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, 4096, this); + ITSInterpreter interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps,this); - InterpreteObservable.add(interp); + inRunner.launchInterprete(interp); try { runnerThread.start(); @@ -269,7 +262,7 @@ public void solve() { try { runnerThread.interrupt(); } catch (Exception ee) { - System.out.println("na pas pu etre interrpute"); + System.out.println("ITS n'a pas pu etre interrpu"); } } catch (Exception e1) { e1.printStackTrace(); @@ -277,4 +270,8 @@ public void solve() { System.out.println("ITS RUNNER FINISH !"); } + public void setDone() { + this.done=!this.done; + } + } \ No newline at end of file diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java index 2d49b931c9..22d878821f 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java @@ -17,7 +17,6 @@ import fr.lip6.move.gal.gal2pins.Gal2PinsTransformerNext; import fr.lip6.move.gal.gal2smt.Gal2SMTFrontEnd; import fr.lip6.move.gal.gal2smt.Solver; -import fr.lip6.move.gal.itscl.modele.ItsInterpreter; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.ProcessController.TimeOutException; import fr.lip6.move.gal.itstools.Runner; @@ -56,10 +55,6 @@ private static boolean isStutterInvariant(Property prop) { return true; } - public void setInterpreter() { - - } - public Boolean taskDone() { todo.removeAll(doneProps); if (todo.isEmpty()) @@ -129,13 +124,15 @@ public void solve() { } todo = spec.getProperties().stream().map(p -> p.getName()).collect(Collectors.toList()); - bufferWIO = new ItsInterpreter(); - LTSminInterpreter interp = new LTSminInterpreter(this); - obsRunner.attach(interp); + LTSminInterpreter interp = new LTSminInterpreter(this, bufferWIO); + inRunner.launchInterprete(interp); for (Property prop : spec.getProperties()) { - if (doneProps.contains(prop.getName())) { - continue; + + synchronized (this) { + if (doneProps.contains(prop.getName())) { + continue; + } } CommandLine ltsmin = new CommandLine(); ltsmin.setWorkingDir(new File(workFolder)); @@ -164,14 +161,16 @@ public void solve() { ltsmin.addArg("-i"); ltsmin.addArg(prop.getName().replaceAll("-", "") + "==true"); } + try { + IStatus status = Runner.runTool(timeout, ltsmin, bufferWIO.getPout(), true); if (!status.isOK() && status.getCode() != 1) { throw new RuntimeException( "Unexpected exception when executing ltsmin :" + ltsmin + "\n" + status); } - interp.configure(isdeadlock, isLTL, status, bufferWIO, prop); + interp.configure(isdeadlock, isLTL, status, prop); } catch (TimeOutException to) { System.err.println("LTSmin timed out on command " + ltsmin); From 406d81134ec382aeff0b9930ebfaf76d7ee87bc4 Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Tue, 27 Jun 2017 14:05:36 +0200 Subject: [PATCH 09/12] Reorgonize, put synchro between runners and their interpreters --- .../src/Interpreter/IInterpreter.java | 6 - .../src/Interpreter/LTSminInterpreter.java | 95 ---------- .../move/gal/application/AbstractRunner.java | 36 ++-- .../move/gal/application/Application.java | 18 +- .../lip6/move/gal/application/ITSRunner.java | 28 +-- .../move/gal/application/LTSminRunner.java | 164 +++++++++++------- .../lip6/move/gal/application/SMTRunner.java | 3 - .../gal/interpreter}/CegarInterpreter.java | 7 +- .../move/gal/interpreter}/ITSInterpreter.java | 21 +-- .../gal/interpreter/LTSminInterpreter.java | 99 +++++++++++ .../move/gal/interpreter}/SMTInterpreter.java | 4 +- 11 files changed, 251 insertions(+), 230 deletions(-) delete mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/IInterpreter.java delete mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java rename pnmcc/fr.lip6.move.gal.application.pnmcc/src/{Interpreter => fr/lip6/move/gal/interpreter}/CegarInterpreter.java (53%) rename pnmcc/fr.lip6.move.gal.application.pnmcc/src/{Interpreter => fr/lip6/move/gal/interpreter}/ITSInterpreter.java (95%) create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java rename pnmcc/fr.lip6.move.gal.application.pnmcc/src/{Interpreter => fr/lip6/move/gal/interpreter}/SMTInterpreter.java (55%) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/IInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/IInterpreter.java deleted file mode 100644 index 67a5826890..0000000000 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/IInterpreter.java +++ /dev/null @@ -1,6 +0,0 @@ -package Interpreter; - -public interface IInterpreter { - - -} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java deleted file mode 100644 index 145b6f978a..0000000000 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/LTSminInterpreter.java +++ /dev/null @@ -1,95 +0,0 @@ -package Interpreter; - -import java.io.IOException; -import java.util.Set; - -import org.eclipse.core.runtime.IStatus; - -import fr.lip6.move.gal.InvariantProp; -import fr.lip6.move.gal.NeverProp; -import fr.lip6.move.gal.Property; -import fr.lip6.move.gal.ReachableProp; -import fr.lip6.move.gal.application.LTSminRunner; -import fr.lip6.move.gal.itscl.modele.IListener; -import fr.lip6.move.gal.itscl.modele.ItsInterpreter; - -public class LTSminInterpreter implements IListener { - - private IStatus status; - private boolean isLTL; - private boolean isdeadlock; - private ItsInterpreter bufferWIO; - private Property prop; - private Set doneProps; - private LTSminRunner ltsRunner; - - public LTSminInterpreter(LTSminRunner ltSminRunner, ItsInterpreter bufferWIO) { - this.ltsRunner = ltSminRunner; - this.doneProps = ltsRunner.getDoneProps(); - this.bufferWIO = bufferWIO; - } - - public void configure(boolean isdeadlock, boolean isLTL, IStatus status, Property prop) { - this.isdeadlock = isdeadlock; - this.isLTL = isLTL; - this.status = status; - this.prop = prop; - } - - public Object call() throws IOException { - - while (true) { - boolean result; - for (String line = ""; line != null; line = bufferWIO.getIn().readLine()) { - System.out.println(" buffer did read : " + line.length()); - if (isdeadlock) { - result = line.contains("Deadlock found") || line.contains("deadlock () found"); - } else if (isLTL) { - // accepting cycle = counter example to - // formula - result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting - // cycle found") - // ; - } else { - boolean hasViol = line.contains("Invariant violation"); - - if (hasViol) { - System.out.println("Found Violation"); - if (prop.getBody() instanceof ReachableProp) { - result = true; - } else if (prop.getBody() instanceof NeverProp) { - result = false; - } else if (prop.getBody() instanceof InvariantProp) { - result = false; - } else { - throw new RuntimeException("Unexpected property type " + prop); - } - } else { - System.out.println("Invariant validated"); - - if (prop.getBody() instanceof ReachableProp) { - result = false; - - } else if (prop.getBody() instanceof NeverProp) { - result = true; - - } else if (prop.getBody() instanceof InvariantProp) { - result = true; - - } else { - throw new RuntimeException("Unexpected property type " + prop); - } - } - } - String ress = (result + "").toUpperCase(); - System.out.println( - "FORMULA " + prop.getName() + " " + ress + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); - doneProps.add(prop.getName()); - synchronized (ltsRunner) { - ltsRunner.setDoneProps(doneProps); - } - } - } - } - -} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java index 4efb7db5f6..d545d242de 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java @@ -4,11 +4,10 @@ import java.util.Set; import java.util.concurrent.ConcurrentHashMap; -import fr.lip6.move.gal.Property; import fr.lip6.move.gal.Specification; +import fr.lip6.move.gal.itscl.interprete.InterpreteObservable; +import fr.lip6.move.gal.itscl.interprete.ItsInterpreter; import fr.lip6.move.gal.itscl.modele.IRunner; -import fr.lip6.move.gal.itscl.modele.InterpreteObservable; -import fr.lip6.move.gal.itscl.modele.ItsInterpreter; public abstract class AbstractRunner implements IRunner { @@ -16,22 +15,21 @@ public abstract class AbstractRunner implements IRunner { protected Set doneProps; protected InterpreteObservable inRunner; protected ItsInterpreter bufferWIO = new ItsInterpreter(); - + public Specification getSpec() { return spec; } - public void setInterprete(InterpreteObservable ob){ - this.inRunner=ob; + public void setInterprete(InterpreteObservable ob) { + this.inRunner = ob; } - - - public Set getDoneProps() { - return doneProps; + + public ItsInterpreter getItsInterpreter() { + return bufferWIO; } - - public void setDoneProps(Set d){ - doneProps=d; + + public void setDoneProps(Set d) { + doneProps = d; } public void configure(Specification z3Spec, Set doneProps) throws IOException { @@ -46,17 +44,9 @@ public void configure(Specification spec) { e.printStackTrace(); } } - + public abstract void solve(); - public Boolean taskDone() { - for (Property prop : getSpec().getProperties()) { - if (!doneProps.contains(prop.getName())) { - // still some work to do - return false; - } - } - return true; - } + public abstract Boolean taskDone(); } \ No newline at end of file diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index 468d197c11..38f01bad1e 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java @@ -22,10 +22,9 @@ import fr.lip6.move.gal.True; import fr.lip6.move.gal.gal2smt.Solver; import fr.lip6.move.gal.itscl.adaptor.InteractApplication; +import fr.lip6.move.gal.itscl.interprete.InterpreteObservable; import fr.lip6.move.gal.itscl.modele.IRunner; -import fr.lip6.move.gal.itscl.modele.InterpreteObservable; import fr.lip6.move.gal.itscl.modele.SolverObservable; -import fr.lip6.move.gal.itscl.modele.Synchronizer; import fr.lip6.move.serialization.SerializationUtil; /** @@ -128,10 +127,9 @@ public Object start(IApplicationContext context) throws Exception { Set doneProps = ConcurrentHashMap.newKeySet(); reader.loadProperties(); - Synchronizer sync = new Synchronizer(); - SolverObservable chRunner = new SolverObservable(sync); - InterpreteObservable inRunner = new InterpreteObservable(sync); - if(inRunner==null){ + SolverObservable chRunner = new SolverObservable(); + InterpreteObservable inRunner = new InterpreteObservable(chRunner); + if (inRunner == null) { System.out.println("is null"); } if (examination.equals("StateSpace")) { @@ -216,15 +214,21 @@ public Object start(IApplicationContext context) throws Exception { } } FutureTask executeRunner = new FutureTask<>(chRunner); + FutureTask executeRunner2 = new FutureTask<>(inRunner); + Thread futureTh = new Thread(executeRunner); + Thread futureTh2 = new Thread(executeRunner2); + // exec.submit(superRunner); try { futureTh.start(); + futureTh2.start(); Boolean result = executeRunner.get(); + Boolean result2 = executeRunner2.get(); - System.out.println("Operation reussi ? " + result); + System.out.println("Operation reussi ? " + result + "And Listener has complete correctly ? " + result2); } catch (ExecutionException e) { System.out.println("im here sh_________"); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java index 1407564c3a..0f0355e31d 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java @@ -8,9 +8,9 @@ import java.util.Set; import java.util.stream.Collectors; -import Interpreter.ITSInterpreter; import fr.lip6.move.gal.Property; import fr.lip6.move.gal.Specification; +import fr.lip6.move.gal.interpreter.ITSInterpreter; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.CommandLineBuilder; import fr.lip6.move.gal.itstools.Runner; @@ -133,7 +133,6 @@ public void run() { } finally { try { pout.close(); - System.out.println("ITS HAS COMPLETELY FINISHED"); } catch (IOException e) { e.printStackTrace(); } @@ -235,8 +234,12 @@ public String outputGalFile() throws IOException { return outpath; } + public void setDone() { + done = !done; + } + public Boolean taskDone() { - + if (done) { System.out.println("tasks resolved Its"); return true; @@ -245,19 +248,26 @@ public Boolean taskDone() { return false; } - + /** + * Generate ITS interpreter + * + * Run both solver and interpreter and wait till termination of both threads + */ public void solve() { todoProps = reader.getSpec().getProperties().stream().map(p -> p.getName()).collect(Collectors.toSet()); Thread runnerThread = new Thread(new ITSRealRunner(bufferWIO.getPout(), cl)); - ITSInterpreter interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps,this); + ITSInterpreter interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, + this); + Thread interpTh = new Thread(interp, "ITSInterpreter"); - inRunner.launchInterprete(interp); + inRunner.addThInterprete(interpTh); try { runnerThread.start(); + interpTh.start(); runnerThread.join(); - + interpTh.join(); } catch (InterruptedException e) { try { runnerThread.interrupt(); @@ -270,8 +280,4 @@ public void solve() { System.out.println("ITS RUNNER FINISH !"); } - public void setDone() { - this.done=!this.done; - } - } \ No newline at end of file diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java index 22d878821f..ccbde6ee18 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java @@ -9,7 +9,6 @@ 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.LTLNext; import fr.lip6.move.gal.LTLProp; @@ -17,6 +16,7 @@ import fr.lip6.move.gal.gal2pins.Gal2PinsTransformerNext; import fr.lip6.move.gal.gal2smt.Gal2SMTFrontEnd; import fr.lip6.move.gal.gal2smt.Solver; +import fr.lip6.move.gal.interpreter.LTSminInterpreter; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.ProcessController.TimeOutException; import fr.lip6.move.gal.itstools.Runner; @@ -31,6 +31,9 @@ public class LTSminRunner extends AbstractRunner { private Solver solver; private int timeout; private List todo; + private boolean first = true; + private boolean isdeadlock = false; + private boolean isLTL = false; public LTSminRunner(String ltsminpath, String solverPath, Solver solver, boolean doPOR, boolean onlyGal, String workFolder, int timeout) { @@ -55,12 +58,68 @@ private static boolean isStutterInvariant(Property prop) { return true; } + private CommandLine linkCommandLine() { + + CommandLine clgcc = new CommandLine(); + clgcc.setWorkingDir(new File(workFolder)); + clgcc.addArg("gcc"); + clgcc.addArg("-shared"); + clgcc.addArg("-o"); + clgcc.addArg("gal.so"); + clgcc.addArg("model.o"); + return clgcc; + } + + private CommandLine compilationCommandLine() { + + CommandLine clgcc = new CommandLine(); + clgcc.setWorkingDir(new File(workFolder)); + clgcc.addArg("gcc"); + clgcc.addArg("-c"); + clgcc.addArg("-I" + ltsminpath + "/include"); + clgcc.addArg("-I."); + clgcc.addArg("-std=c99"); + clgcc.addArg("-fPIC"); + clgcc.addArg("-O3"); + clgcc.addArg("model.c"); + + return clgcc; + + } + + private CommandLine generateLTSminCommand(Property prop, Gal2PinsTransformerNext g2p) { + CommandLine ltsmin = new CommandLine(); + ltsmin.setWorkingDir(new File(workFolder)); + ltsmin.addArg(ltsminpath + "/bin/pins2lts-mc"); + ltsmin.addArg("./gal.so"); + + ltsmin.addArg("--threads=1"); + if (doPOR && isStutterInvariant(prop)) { + ltsmin.addArg("-p"); + ltsmin.addArg("--pins-guards"); + } + ltsmin.addArg("--when"); + + if (prop.getName().contains("Deadlock")) { + ltsmin.addArg("-d"); + isdeadlock = true; + } else if (prop.getBody() instanceof LTLProp) { + ltsmin.addArg("--ltl"); + ltsmin.addArg(g2p.printLTLProperty((LTLProp) prop.getBody())); + // ltsmin.addArg("--ltl-semantics"); + // ltsmin.addArg("spin"); + + isLTL = true; + } else { + ltsmin.addArg("-i"); + ltsmin.addArg(prop.getName().replaceAll("-", "") + "==true"); + } + return ltsmin; + } + + 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; } @@ -77,16 +136,8 @@ public void solve() { if (ltsminpath != null) { { // compile - CommandLine clgcc = new CommandLine(); - clgcc.setWorkingDir(new File(workFolder)); - clgcc.addArg("gcc"); - clgcc.addArg("-c"); - clgcc.addArg("-I" + ltsminpath + "/include"); - clgcc.addArg("-I."); - clgcc.addArg("-std=c99"); - clgcc.addArg("-fPIC"); - clgcc.addArg("-O3"); - clgcc.addArg("model.c"); + CommandLine clgcc = compilationCommandLine(); + try { System.out.println("Running compilation step : " + clgcc); IStatus status = Runner.runTool(100, clgcc); @@ -97,70 +148,43 @@ public void solve() { throw new RuntimeException("Compilation of executable timed out or was killed." + clgcc); } } - { - // link - CommandLine clgcc = new CommandLine(); - clgcc.setWorkingDir(new File(workFolder)); - clgcc.addArg("gcc"); - clgcc.addArg("-shared"); - clgcc.addArg("-o"); - clgcc.addArg("gal.so"); - clgcc.addArg("model.o"); - try { - System.out.println("Running link step : " + clgcc); - IStatus status = Runner.runTool(100, clgcc); - if (!status.isOK()) { - throw new RuntimeException("Could not link executable ." + clgcc); - } - } catch (TimeOutException to) { - throw new RuntimeException("Link of executable timed out or was killed." + clgcc); + + // link + CommandLine clgcc = linkCommandLine(); + + try { + System.out.println("Running link step : " + clgcc); + IStatus status = Runner.runTool(100, clgcc); + if (!status.isOK()) { + throw new RuntimeException("Could not link executable ." + clgcc); } + } catch (TimeOutException to) { + throw new RuntimeException("Link of executable timed out or was killed." + clgcc); } + if (onlyGal) { System.out.println("Successfully built gal.so in :" + workFolder); System.out.println("It has labels for :" + (spec.getProperties().stream() .map(p -> p.getName().replaceAll("-", "")).collect(Collectors.toList()))); return; } + todo = spec.getProperties().stream().map(p -> p.getName()).collect(Collectors.toList()); - LTSminInterpreter interp = new LTSminInterpreter(this, bufferWIO); - inRunner.launchInterprete(interp); + LTSminInterpreter interp = new LTSminInterpreter(this, bufferWIO,doneProps); + Thread interpTh = new Thread(interp); + inRunner.addThInterprete(interpTh); for (Property prop : spec.getProperties()) { - synchronized (this) { - if (doneProps.contains(prop.getName())) { - continue; - } - } - CommandLine ltsmin = new CommandLine(); - ltsmin.setWorkingDir(new File(workFolder)); - ltsmin.addArg(ltsminpath + "/bin/pins2lts-mc"); - ltsmin.addArg("./gal.so"); - - ltsmin.addArg("--threads=1"); - if (doPOR && isStutterInvariant(prop)) { - ltsmin.addArg("-p"); - ltsmin.addArg("--pins-guards"); - } - ltsmin.addArg("--when"); - boolean isdeadlock = false; - boolean isLTL = false; - if (prop.getName().contains("Deadlock")) { - ltsmin.addArg("-d"); - isdeadlock = true; - } else if (prop.getBody() instanceof LTLProp) { - ltsmin.addArg("--ltl"); - ltsmin.addArg(g2p.printLTLProperty((LTLProp) prop.getBody())); - // ltsmin.addArg("--ltl-semantics"); - // ltsmin.addArg("spin"); - - isLTL = true; - } else { - ltsmin.addArg("-i"); - ltsmin.addArg(prop.getName().replaceAll("-", "") + "==true"); + if (doneProps.contains(prop.getName())) { + continue; } + + isdeadlock = false; + isLTL = false; + + CommandLine ltsmin = generateLTSminCommand(prop, g2p); try { @@ -171,19 +195,27 @@ public void solve() { } interp.configure(isdeadlock, isLTL, status, prop); - + if (first) { + interpTh.start(); + first = false; + } } catch (TimeOutException to) { System.err.println("LTSmin timed out on command " + ltsmin); continue; } + interpTh.join(); + } } + System.out.println("LTMIN HAS FINISHED !"); } catch (IOException e) { e.printStackTrace(); } catch (RuntimeException e) { System.err.println("LTS min runner thread failed on error :" + e); e.printStackTrace(); + } catch (InterruptedException e) { + e.printStackTrace(); } } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java index 22983e1441..c9849a6dd5 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java @@ -28,9 +28,6 @@ public Logger getLog() { } - public void setInterpreter() { - } - public Boolean taskDone() { // test for and handle properties if (nbsolve == satresult.size()) { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java similarity index 53% rename from pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java rename to pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java index 37a425d92b..3eef8929a1 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/CegarInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java @@ -1,12 +1,9 @@ -package Interpreter; +package fr.lip6.move.gal.interpreter; -import fr.lip6.move.gal.itscl.modele.ItsInterpreter; +import fr.lip6.move.gal.itscl.interprete.ItsInterpreter; public class CegarInterpreter extends ItsInterpreter{ - public CegarInterpreter(int pipeSize) { - super(pipeSize); - } public Boolean call() { return null; diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java similarity index 95% rename from pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java rename to pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java index bb1f5b1243..7a58fce282 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/ITSInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java @@ -1,4 +1,4 @@ -package Interpreter; +package fr.lip6.move.gal.interpreter; import java.io.IOException; import java.util.Set; @@ -11,10 +11,9 @@ import fr.lip6.move.gal.Constant; import fr.lip6.move.gal.application.ITSRunner; import fr.lip6.move.gal.application.MccTranslator; -import fr.lip6.move.gal.itscl.modele.IListener; -import fr.lip6.move.gal.itscl.modele.ItsInterpreter; +import fr.lip6.move.gal.itscl.interprete.ItsInterpreter; -public class ITSInterpreter implements IListener { +public class ITSInterpreter implements Runnable { // private Map> boundProps; private String examination; @@ -33,11 +32,11 @@ public ITSInterpreter(String examination, boolean withStructure, MccTranslator r this.seen = doneProps; this.todoProps = todoProps; this.itsRunner=itsRunner; + this.buffWriteInOut=itsRunner.getItsInterpreter(); } - - public Object call() throws Exception { + + public void run() { try { - for (String line = ""; line != null; line = buffWriteInOut.getIn().readLine()) { System.out.println(line); @@ -167,21 +166,19 @@ public Object call() throws Exception { } } buffWriteInOut.closeIn(); - } catch (NumberFormatException e) { e.printStackTrace(); - return false; } catch (IOException e) { e.printStackTrace(); - return false; } buffWriteInOut.closePinPout(); if (seen.containsAll(todoProps)) { - System.out.println("whi here"); + System.out.println("YES i did solved everythin"); itsRunner.setDone(); } - return false; + System.out.println("I DID IT ITS"); + } } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java new file mode 100644 index 0000000000..6c54a8d350 --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java @@ -0,0 +1,99 @@ +package fr.lip6.move.gal.interpreter; + +import java.io.IOException; +import java.util.Set; + +import org.eclipse.core.runtime.IStatus; + +import fr.lip6.move.gal.InvariantProp; +import fr.lip6.move.gal.NeverProp; +import fr.lip6.move.gal.Property; +import fr.lip6.move.gal.ReachableProp; +import fr.lip6.move.gal.application.LTSminRunner; +import fr.lip6.move.gal.itscl.interprete.ItsInterpreter; + +public class LTSminInterpreter implements Runnable { + + private IStatus status; + private boolean isLTL; + private boolean isdeadlock; + private ItsInterpreter bufferWIO; + private Property prop; + private Set doneProps; + private LTSminRunner ltsRunner; + + public LTSminInterpreter(LTSminRunner ltSminRunner, ItsInterpreter bufferWIO, Set doneProps) { + this.ltsRunner = ltSminRunner; + this.doneProps = doneProps; + this.bufferWIO = bufferWIO; + } + + public void configure(boolean isdeadlock, boolean isLTL, IStatus status, Property prop) { + this.isdeadlock = isdeadlock; + this.isLTL = isLTL; + this.status = status; + this.prop = prop; + } + + public void run() { + + while (true) { + boolean result = false; + try { + System.out.println("im i interpreter k ? "); + for (String line = ""; line != null; line = bufferWIO.getIn().readLine()) { + + if (line.length() != 0) { + System.out.println(" buffer did read : " + line); + if (isdeadlock) { + result = line.contains("Deadlock found") || line.contains("deadlock () found"); + } else if (isLTL) { + // accepting cycle = counter example to + // formula + result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting + // cycle found") + // ; + } else { + boolean hasViol = line.contains("Invariant violation"); + + if (hasViol) { + System.out.println("Found Violation"); + if (prop.getBody() instanceof ReachableProp) { + result = true; + } else if (prop.getBody() instanceof NeverProp) { + result = false; + } else if (prop.getBody() instanceof InvariantProp) { + result = false; + } else { + throw new RuntimeException("Unexpected property type " + prop); + } + } else { + System.out.println("Invariant validated"); + if (prop.getBody() instanceof ReachableProp) { + result = false; + + } else if (prop.getBody() instanceof NeverProp) { + result = true; + + } else if (prop.getBody() instanceof InvariantProp) { + result = true; + + } else { + throw new RuntimeException("Unexpected property type " + prop); + } + } + } + String ress = (result + "").toUpperCase(); + System.out.println("FORMULA " + prop.getName() + " " + ress + + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); + doneProps.add(prop.getName()); + ltsRunner.setDoneProps(doneProps); + } + } + } catch (IOException e) { + e.printStackTrace(); + } + } + } + +} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java similarity index 55% rename from pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java rename to pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java index 1ea6fb1fb3..ac22950da0 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/Interpreter/SMTInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java @@ -1,6 +1,6 @@ -package Interpreter; +package fr.lip6.move.gal.interpreter; -import fr.lip6.move.gal.itscl.modele.ItsInterpreter; +import fr.lip6.move.gal.itscl.interprete.ItsInterpreter; public class SMTInterpreter extends ItsInterpreter { From ef17ae98f9c1fc203ad96e8f6dd8098023bc44c9 Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Thu, 29 Jun 2017 18:13:13 +0200 Subject: [PATCH 10/12] concurrence done but busy waiting method --- .../move/gal/application/AbstractRunner.java | 10 -- .../move/gal/application/Application.java | 2 - .../move/gal/application/CegarRunner.java | 2 - .../lip6/move/gal/application/ITSRunner.java | 23 +-- .../move/gal/application/LTSminRunner.java | 45 ++++-- .../gal/interpreter/CegarInterpreter.java | 4 +- .../move/gal/interpreter/ITSInterpreter.java | 31 ++-- .../gal/interpreter/LTSminInterpreter.java | 143 +++++++++++------- .../move/gal/interpreter/SMTInterpreter.java | 4 +- 9 files changed, 153 insertions(+), 111 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java index d545d242de..2828e0c12c 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java @@ -6,7 +6,6 @@ import fr.lip6.move.gal.Specification; import fr.lip6.move.gal.itscl.interprete.InterpreteObservable; -import fr.lip6.move.gal.itscl.interprete.ItsInterpreter; import fr.lip6.move.gal.itscl.modele.IRunner; public abstract class AbstractRunner implements IRunner { @@ -14,7 +13,6 @@ public abstract class AbstractRunner implements IRunner { protected Specification spec; protected Set doneProps; protected InterpreteObservable inRunner; - protected ItsInterpreter bufferWIO = new ItsInterpreter(); public Specification getSpec() { return spec; @@ -24,14 +22,6 @@ public void setInterprete(InterpreteObservable ob) { this.inRunner = ob; } - public ItsInterpreter getItsInterpreter() { - return bufferWIO; - } - - public void setDoneProps(Set d) { - doneProps = d; - } - public void configure(Specification z3Spec, Set doneProps) throws IOException { this.spec = z3Spec; this.doneProps = doneProps; diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index 38f01bad1e..69ad81943c 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java @@ -61,7 +61,6 @@ 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; @@ -220,7 +219,6 @@ public Object start(IApplicationContext context) throws Exception { Thread futureTh2 = new Thread(executeRunner2); - // exec.submit(superRunner); try { futureTh.start(); futureTh2.start(); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java index 298ee0da8a..0db13e30fe 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java @@ -31,11 +31,9 @@ public Boolean taskDone() { for (Property prop : todoProps) { if (!doneProps.contains(prop.getName())) { // still some work to do - System.out.println("tasks not all resolved Cegar"); return false; } } - System.out.println("tasks resolved Cegar"); return true; } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java index 0f0355e31d..cb6fd762a9 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java @@ -11,6 +11,7 @@ import fr.lip6.move.gal.Property; import fr.lip6.move.gal.Specification; import fr.lip6.move.gal.interpreter.ITSInterpreter; +import fr.lip6.move.gal.itscl.interprete.FileStreamInterprete; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.CommandLineBuilder; import fr.lip6.move.gal.itstools.Runner; @@ -29,6 +30,7 @@ public class ITSRunner extends AbstractRunner { private Set todoProps; private boolean done = false; + private ITSInterpreter interp; public ITSRunner(String examination, MccTranslator reader, boolean doITS, boolean onlyGal, String workFolder) { this.examination = examination; @@ -239,13 +241,8 @@ public void setDone() { } public Boolean taskDone() { - - if (done) { - System.out.println("tasks resolved Its"); - return true; - } - System.out.println("tasks not all resolved Its"); - return false; + interp.acquireResult(); + return done; } /** @@ -254,14 +251,18 @@ public Boolean taskDone() { * Run both solver and interpreter and wait till termination of both threads */ public void solve() { - + FileStreamInterprete bufferWIO = new FileStreamInterprete(); + todoProps = reader.getSpec().getProperties().stream().map(p -> p.getName()).collect(Collectors.toSet()); + Thread runnerThread = new Thread(new ITSRealRunner(bufferWIO.getPout(), cl)); - ITSInterpreter interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, + interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, this); + interp.setInput(bufferWIO); Thread interpTh = new Thread(interp, "ITSInterpreter"); inRunner.addThInterprete(interpTh); + long time = System.currentTimeMillis(); try { runnerThread.start(); @@ -272,12 +273,12 @@ public void solve() { try { runnerThread.interrupt(); } catch (Exception ee) { - System.out.println("ITS n'a pas pu etre interrpu"); + System.out.println("ITSRealRunner didn't interrupte"); } } catch (Exception e1) { e1.printStackTrace(); } - System.out.println("ITS RUNNER FINISH !"); + System.out.println("I do finish yes ITS. Time : " + (System.currentTimeMillis() - time)); } } \ No newline at end of file diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java index ccbde6ee18..a1d1b50389 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java @@ -17,6 +17,7 @@ import fr.lip6.move.gal.gal2smt.Gal2SMTFrontEnd; import fr.lip6.move.gal.gal2smt.Solver; import fr.lip6.move.gal.interpreter.LTSminInterpreter; +import fr.lip6.move.gal.itscl.interprete.InterpreteBytArray; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.ProcessController.TimeOutException; import fr.lip6.move.gal.itstools.Runner; @@ -31,7 +32,6 @@ public class LTSminRunner extends AbstractRunner { private Solver solver; private int timeout; private List todo; - private boolean first = true; private boolean isdeadlock = false; private boolean isLTL = false; @@ -86,8 +86,11 @@ private CommandLine compilationCommandLine() { return clgcc; } - + private CommandLine generateLTSminCommand(Property prop, Gal2PinsTransformerNext g2p) { + + isdeadlock = false; + isLTL = false; CommandLine ltsmin = new CommandLine(); ltsmin.setWorkingDir(new File(workFolder)); ltsmin.addArg(ltsminpath + "/bin/pins2lts-mc"); @@ -117,13 +120,18 @@ private CommandLine generateLTSminCommand(Property prop, Gal2PinsTransformerNext return ltsmin; } - public Boolean taskDone() { + inRunner.acquireFinalResult(); todo.removeAll(doneProps); return (todo.isEmpty()) ? true : false; } public void solve() { + + InterpreteBytArray bufferWIO = new InterpreteBytArray(); + LTSminInterpreter interp = new LTSminInterpreter(this, bufferWIO); + long time = 0; + System.out.println("lts do comm"); try { System.out.println("Built C files in : \n" + new File(workFolder + "/")); final Gal2PinsTransformerNext g2p = new Gal2PinsTransformerNext(); @@ -171,53 +179,58 @@ public void solve() { todo = spec.getProperties().stream().map(p -> p.getName()).collect(Collectors.toList()); - LTSminInterpreter interp = new LTSminInterpreter(this, bufferWIO,doneProps); - Thread interpTh = new Thread(interp); + Thread interpTh = new Thread(interp, "LTSminInterpreter"); inRunner.addThInterprete(interpTh); + interpTh.start(); + + time = System.currentTimeMillis(); for (Property prop : spec.getProperties()) { + interp.waitInterpreter(); + if (doneProps.contains(prop.getName())) { continue; } - - isdeadlock = false; - isLTL = false; CommandLine ltsmin = generateLTSminCommand(prop, g2p); try { - + // dont know why it blocks at the 4th prop IStatus status = Runner.runTool(timeout, ltsmin, bufferWIO.getPout(), true); + + interp.notifyInterpreter(isdeadlock, isLTL, status, prop); + if (!status.isOK() && status.getCode() != 1) { throw new RuntimeException( "Unexpected exception when executing ltsmin :" + ltsmin + "\n" + status); } - interp.configure(isdeadlock, isLTL, status, prop); - if (first) { - interpTh.start(); - first = false; - } } catch (TimeOutException to) { System.err.println("LTSmin timed out on command " + ltsmin); continue; } - interpTh.join(); } + interpTh.join(); + bufferWIO.getPout().close(); } - System.out.println("LTMIN HAS FINISHED !"); + System.out.println("LTMIN HAS FINISHED !. Time :" + (System.currentTimeMillis() - time)); } catch (IOException e) { e.printStackTrace(); } catch (RuntimeException e) { System.err.println("LTS min runner thread failed on error :" + e); e.printStackTrace(); } catch (InterruptedException e) { + interp.notifyInterpreter(isdeadlock, isLTL); e.printStackTrace(); } } + public void addToDoneProps(String prop) { + doneProps.add(prop); + } + } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java index 3eef8929a1..d96d4c90b1 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java @@ -1,8 +1,8 @@ package fr.lip6.move.gal.interpreter; -import fr.lip6.move.gal.itscl.interprete.ItsInterpreter; +import fr.lip6.move.gal.itscl.interprete.FileStreamInterprete; -public class CegarInterpreter extends ItsInterpreter{ +public class CegarInterpreter extends FileStreamInterprete{ public Boolean call() { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java index 7a58fce282..0b98c3aacc 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java @@ -2,6 +2,7 @@ import java.io.IOException; import java.util.Set; +import java.util.concurrent.Semaphore; import org.eclipse.emf.common.util.TreeIterator; import org.eclipse.emf.ecore.EObject; @@ -11,7 +12,7 @@ import fr.lip6.move.gal.Constant; import fr.lip6.move.gal.application.ITSRunner; import fr.lip6.move.gal.application.MccTranslator; -import fr.lip6.move.gal.itscl.interprete.ItsInterpreter; +import fr.lip6.move.gal.itscl.interprete.FileStreamInterprete; public class ITSInterpreter implements Runnable { @@ -21,9 +22,11 @@ public class ITSInterpreter implements Runnable { private MccTranslator reader; private Set seen; private Set todoProps; - private ItsInterpreter buffWriteInOut; + private FileStreamInterprete buffWriteInOut; private ITSRunner itsRunner; + private Semaphore hasComplete = new Semaphore(0); + public ITSInterpreter(String examination, boolean withStructure, MccTranslator reader, Set doneProps, Set todoProps, ITSRunner itsRunner) { this.examination = examination; @@ -31,15 +34,25 @@ public ITSInterpreter(String examination, boolean withStructure, MccTranslator r this.reader = reader; this.seen = doneProps; this.todoProps = todoProps; - this.itsRunner=itsRunner; - this.buffWriteInOut=itsRunner.getItsInterpreter(); + this.itsRunner = itsRunner; } - public void run() { + + public void setInput(FileStreamInterprete bufferWIO) { + this.buffWriteInOut=bufferWIO; + } + + public void acquireResult() { try { - for (String line = ""; line != null; line = buffWriteInOut.getIn().readLine()) { + hasComplete.acquire(); + } catch (InterruptedException e) { + e.printStackTrace(); + } + } - System.out.println(line); + public void run() { + try { + for (String line = ""; line != null; line = buffWriteInOut.getWrittenData()) { // stdOutput.toString().split("\\r?\\n")) ; if (line.matches("Max variable value.*")) { if (examination.equals("StateSpace")) { @@ -164,6 +177,7 @@ public void run() { } } } + } buffWriteInOut.closeIn(); } catch (NumberFormatException e) { @@ -174,10 +188,9 @@ public void run() { buffWriteInOut.closePinPout(); if (seen.containsAll(todoProps)) { - System.out.println("YES i did solved everythin"); itsRunner.setDone(); } - System.out.println("I DID IT ITS"); + hasComplete.release(); } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java index 6c54a8d350..402c7f4991 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java @@ -1,7 +1,6 @@ package fr.lip6.move.gal.interpreter; -import java.io.IOException; -import java.util.Set; +import java.util.concurrent.Semaphore; import org.eclipse.core.runtime.IStatus; @@ -10,87 +9,117 @@ import fr.lip6.move.gal.Property; import fr.lip6.move.gal.ReachableProp; import fr.lip6.move.gal.application.LTSminRunner; -import fr.lip6.move.gal.itscl.interprete.ItsInterpreter; +import fr.lip6.move.gal.itscl.interprete.InterpreteBytArray; public class LTSminInterpreter implements Runnable { private IStatus status; private boolean isLTL; private boolean isdeadlock; - private ItsInterpreter bufferWIO; + private InterpreteBytArray bufferWIO; private Property prop; - private Set doneProps; private LTSminRunner ltsRunner; + private boolean completeProp; - public LTSminInterpreter(LTSminRunner ltSminRunner, ItsInterpreter bufferWIO, Set doneProps) { + private int nbProps = 0; + private final Semaphore waitRunner = new Semaphore(0); + private final Semaphore waitInterpreter = new Semaphore(1); + + public LTSminInterpreter(LTSminRunner ltSminRunner, InterpreteBytArray bufferWIO) { this.ltsRunner = ltSminRunner; - this.doneProps = doneProps; + this.nbProps = ltSminRunner.getSpec().getProperties().size(); this.bufferWIO = bufferWIO; } - public void configure(boolean isdeadlock, boolean isLTL, IStatus status, Property prop) { + private void waitRunner() throws InterruptedException { + waitRunner.acquire(); + } + + public void waitInterpreter() throws InterruptedException { + waitInterpreter.acquire(); + } + + private void notifyRunner() { + waitInterpreter.release(); + } + + public void notifyInterpreter(boolean isdeadlock, boolean isLTL, IStatus status, Property prop) { this.isdeadlock = isdeadlock; this.isLTL = isLTL; this.status = status; this.prop = prop; + this.completeProp = true; + + waitRunner.release(); } - public void run() { + public void notifyInterpreter(boolean isdeadlock, boolean isLTL) { + + this.isdeadlock = isdeadlock; + this.isLTL = isLTL; + this.completeProp = false; - while (true) { + waitRunner.release(); + } + + public void run() { + int i = 0; + while (i++ < nbProps) { boolean result = false; try { - System.out.println("im i interpreter k ? "); - for (String line = ""; line != null; line = bufferWIO.getIn().readLine()) { - - if (line.length() != 0) { - System.out.println(" buffer did read : " + line); - if (isdeadlock) { - result = line.contains("Deadlock found") || line.contains("deadlock () found"); - } else if (isLTL) { - // accepting cycle = counter example to - // formula - result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting - // cycle found") - // ; + + waitRunner(); + + String output = bufferWIO.getWrittenData(); + + if (isdeadlock) { + result = output.contains("Deadlock found") || output.contains("deadlock () found"); + } else if (isLTL) { + // accepting cycle = counter example to + // formula + if (!completeProp) + System.out.println("Runner was interrupted before completing the treatment. "); + result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting + // cycle found") + // ; + } else { + boolean hasViol = output.contains("Invariant violation"); + + if (hasViol) { + System.out.println("Found Violation"); + if (prop.getBody() instanceof ReachableProp) { + result = true; + } else if (prop.getBody() instanceof NeverProp) { + result = false; + } else if (prop.getBody() instanceof InvariantProp) { + result = false; } else { - boolean hasViol = line.contains("Invariant violation"); - - if (hasViol) { - System.out.println("Found Violation"); - if (prop.getBody() instanceof ReachableProp) { - result = true; - } else if (prop.getBody() instanceof NeverProp) { - result = false; - } else if (prop.getBody() instanceof InvariantProp) { - result = false; - } else { - throw new RuntimeException("Unexpected property type " + prop); - } - } else { - System.out.println("Invariant validated"); - if (prop.getBody() instanceof ReachableProp) { - result = false; - - } else if (prop.getBody() instanceof NeverProp) { - result = true; - - } else if (prop.getBody() instanceof InvariantProp) { - result = true; - - } else { - throw new RuntimeException("Unexpected property type " + prop); - } - } + throw new RuntimeException("Unexpected property type " + prop); + } + } else { + System.out.println("Invariant validated"); + if (prop.getBody() instanceof ReachableProp) { + result = false; + + } else if (prop.getBody() instanceof NeverProp) { + result = true; + + } else if (prop.getBody() instanceof InvariantProp) { + result = true; + + } else { + throw new RuntimeException("Unexpected property type " + prop); } - String ress = (result + "").toUpperCase(); - System.out.println("FORMULA " + prop.getName() + " " + ress - + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); - doneProps.add(prop.getName()); - ltsRunner.setDoneProps(doneProps); } } - } catch (IOException e) { + ltsRunner.addToDoneProps(prop.getName()); + notifyRunner(); + String ress = (result + "").toUpperCase(); + System.out.println( + "FORMULA " + prop.getName() + " " + ress + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); + + + } catch (InterruptedException e) { e.printStackTrace(); } } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java index ac22950da0..8f49b873a4 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java @@ -1,8 +1,8 @@ package fr.lip6.move.gal.interpreter; -import fr.lip6.move.gal.itscl.interprete.ItsInterpreter; +import fr.lip6.move.gal.itscl.interprete.FileStreamInterprete; -public class SMTInterpreter extends ItsInterpreter { +public class SMTInterpreter extends FileStreamInterprete { public Boolean call() throws Exception { From c1afd4886f09c456d1bbd707255229be75c7a99c Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Fri, 30 Jun 2017 15:54:49 +0200 Subject: [PATCH 11/12] final maj runner and their interpreters --- .../move/gal/application/CegarRunner.java | 2 +- .../lip6/move/gal/application/ITSRunner.java | 4 ++-- .../move/gal/application/LTSminRunner.java | 13 ++++++------ .../lip6/move/gal/application/SMTRunner.java | 1 + .../gal/interpreter/AbstractInterpreter.java | 20 +++++++++++++++++++ .../move/gal/interpreter/IInterpreter.java | 5 +++++ .../move/gal/interpreter/ITSInterpreter.java | 16 ++++----------- .../gal/interpreter/LTSminInterpreter.java | 1 + 8 files changed, 41 insertions(+), 21 deletions(-) create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/AbstractInterpreter.java create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/IInterpreter.java diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java index 0db13e30fe..3602613a38 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java @@ -11,6 +11,7 @@ import fr.lip6.move.gal.instantiate.CompositeBuilder; import fr.lip6.move.gal.instantiate.GALRewriter; import fr.lip6.move.gal.instantiate.Simplifier; +import fr.lip6.move.gal.itscl.interprete.InterpreteObservable; public class CegarRunner extends AbstractRunner { @@ -78,7 +79,6 @@ public void solve() { } } System.out.println("CEGAR HAS COMPLETELY FINISHED"); - } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java index cb6fd762a9..65f38508fb 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java @@ -255,7 +255,7 @@ public void solve() { todoProps = reader.getSpec().getProperties().stream().map(p -> p.getName()).collect(Collectors.toSet()); - Thread runnerThread = new Thread(new ITSRealRunner(bufferWIO.getPout(), cl)); + Thread runnerThread = new Thread(new ITSRealRunner(bufferWIO.getPout(), cl),"ITSRealRunner"); interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, this); interp.setInput(bufferWIO); @@ -278,7 +278,7 @@ public void solve() { } catch (Exception e1) { e1.printStackTrace(); } - System.out.println("I do finish yes ITS. Time : " + (System.currentTimeMillis() - time)); + System.out.println("ITS complete. Time : " + (System.currentTimeMillis() - time)); } } \ No newline at end of file diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java index a1d1b50389..7ff2fa94de 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java @@ -121,17 +121,18 @@ private CommandLine generateLTSminCommand(Property prop, Gal2PinsTransformerNext } public Boolean taskDone() { - inRunner.acquireFinalResult(); +// inRunner.acquireFinalResult(); todo.removeAll(doneProps); return (todo.isEmpty()) ? true : false; } public void solve() { + InterpreteBytArray bufferWIO = new InterpreteBytArray(); - LTSminInterpreter interp = new LTSminInterpreter(this, bufferWIO); + LTSminInterpreter interp = new LTSminInterpreter(this, bufferWIO); + long time = 0; - System.out.println("lts do comm"); try { System.out.println("Built C files in : \n" + new File(workFolder + "/")); final Gal2PinsTransformerNext g2p = new Gal2PinsTransformerNext(); @@ -139,8 +140,8 @@ public void solve() { g2p.setSmtConfig(gsf); g2p.initSolver(); - g2p.transform(spec, workFolder, doPOR); + g2p.transform(spec, workFolder, doPOR); if (ltsminpath != null) { { // compile @@ -182,7 +183,8 @@ public void solve() { Thread interpTh = new Thread(interp, "LTSminInterpreter"); inRunner.addThInterprete(interpTh); interpTh.start(); - + System.out.println("I created it ! LTSmin"); + time = System.currentTimeMillis(); for (Property prop : spec.getProperties()) { @@ -221,7 +223,6 @@ public void solve() { e.printStackTrace(); } catch (RuntimeException e) { System.err.println("LTS min runner thread failed on error :" + e); - e.printStackTrace(); } catch (InterruptedException e) { interp.notifyInterpreter(isdeadlock, isLTL); e.printStackTrace(); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java index c9849a6dd5..49b0355244 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java @@ -29,6 +29,7 @@ public Logger getLog() { } public Boolean taskDone() { + System.out.println("SMT HAS FINISH SO TREAT RESULT"); // test for and handle properties if (nbsolve == satresult.size()) { getLog().info("SMT solved all " + nbsolve + " properties. Interrupting other analysis methods."); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/AbstractInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/AbstractInterpreter.java new file mode 100644 index 0000000000..271708d557 --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/AbstractInterpreter.java @@ -0,0 +1,20 @@ +package fr.lip6.move.gal.interpreter; + +import java.util.concurrent.Semaphore; + +public abstract class AbstractInterpreter implements IInterpreter { + private Semaphore hasComplete = new Semaphore(0); + + public void acquireResult() { + try { + hasComplete.acquire(); + } catch (InterruptedException e) { + e.printStackTrace(); + } + } + + public void releaseResult(){ + hasComplete.release(); + } + +} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/IInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/IInterpreter.java new file mode 100644 index 0000000000..dc2fed0ad0 --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/IInterpreter.java @@ -0,0 +1,5 @@ +package fr.lip6.move.gal.interpreter; + +public interface IInterpreter extends Runnable{ + +} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java index 0b98c3aacc..1305e1ea6f 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java @@ -2,7 +2,6 @@ import java.io.IOException; import java.util.Set; -import java.util.concurrent.Semaphore; import org.eclipse.emf.common.util.TreeIterator; import org.eclipse.emf.ecore.EObject; @@ -14,7 +13,7 @@ import fr.lip6.move.gal.application.MccTranslator; import fr.lip6.move.gal.itscl.interprete.FileStreamInterprete; -public class ITSInterpreter implements Runnable { +public class ITSInterpreter extends AbstractInterpreter { // private Map> boundProps; private String examination; @@ -24,8 +23,7 @@ public class ITSInterpreter implements Runnable { private Set todoProps; private FileStreamInterprete buffWriteInOut; private ITSRunner itsRunner; - - private Semaphore hasComplete = new Semaphore(0); + public ITSInterpreter(String examination, boolean withStructure, MccTranslator reader, Set doneProps, Set todoProps, ITSRunner itsRunner) { @@ -42,13 +40,6 @@ public void setInput(FileStreamInterprete bufferWIO) { this.buffWriteInOut=bufferWIO; } - public void acquireResult() { - try { - hasComplete.acquire(); - } catch (InterruptedException e) { - e.printStackTrace(); - } - } public void run() { try { @@ -190,7 +181,8 @@ public void run() { if (seen.containsAll(todoProps)) { itsRunner.setDone(); } - hasComplete.release(); + + releaseResult(); } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java index 402c7f4991..0b6b559571 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java @@ -31,6 +31,7 @@ public LTSminInterpreter(LTSminRunner ltSminRunner, InterpreteBytArray bufferWIO this.bufferWIO = bufferWIO; } + private void waitRunner() throws InterruptedException { waitRunner.acquire(); } From 5f2fa87c6367bdefac3a02671c12c2e60a3bc362 Mon Sep 17 00:00:00 2001 From: Anissa Kheireddine Date: Mon, 3 Jul 2017 13:06:10 +0200 Subject: [PATCH 12/12] comments --- .../move/gal/application/AbstractRunner.java | 6 ++-- .../move/gal/application/Application.java | 16 +++++----- .../move/gal/application/CegarRunner.java | 1 - .../lip6/move/gal/application/ITSRunner.java | 4 ++- .../move/gal/application/LTSminRunner.java | 10 ++----- .../gal/interpreter/AbstractInterpreter.java | 20 ------------- .../gal/interpreter/CegarInterpreter.java | 14 --------- .../move/gal/interpreter/IInterpreter.java | 5 ---- .../move/gal/interpreter/ITSInterpreter.java | 8 ++--- .../gal/interpreter/LTSminInterpreter.java | 30 ++++++++++++------- .../move/gal/interpreter/SMTInterpreter.java | 11 ------- 11 files changed, 40 insertions(+), 85 deletions(-) delete mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/AbstractInterpreter.java delete mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java delete mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/IInterpreter.java delete mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java index 2828e0c12c..0331a64a57 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java @@ -5,20 +5,20 @@ import java.util.concurrent.ConcurrentHashMap; import fr.lip6.move.gal.Specification; -import fr.lip6.move.gal.itscl.interprete.InterpreteObservable; +import fr.lip6.move.gal.itscl.interpreter.IInterpreteObservable; import fr.lip6.move.gal.itscl.modele.IRunner; public abstract class AbstractRunner implements IRunner { protected Specification spec; protected Set doneProps; - protected InterpreteObservable inRunner; + protected IInterpreteObservable inRunner; public Specification getSpec() { return spec; } - public void setInterprete(InterpreteObservable ob) { + public void configureInterpreter(IInterpreteObservable ob) { this.inRunner = ob; } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index 69ad81943c..a567f13373 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java @@ -21,8 +21,8 @@ import fr.lip6.move.gal.Specification; import fr.lip6.move.gal.True; import fr.lip6.move.gal.gal2smt.Solver; -import fr.lip6.move.gal.itscl.adaptor.InteractApplication; -import fr.lip6.move.gal.itscl.interprete.InterpreteObservable; +import fr.lip6.move.gal.itscl.adaptor.AdapterApplication; +import fr.lip6.move.gal.itscl.interpreter.InterpreteObservable; import fr.lip6.move.gal.itscl.modele.IRunner; import fr.lip6.move.gal.itscl.modele.SolverObservable; import fr.lip6.move.serialization.SerializationUtil; @@ -167,14 +167,14 @@ public Object start(IApplicationContext context) throws Exception { // threads. z3Runner = new SMTRunner(pwd, solverPath, solver); z3Runner.configure(z3Spec, doneProps); - chRunner.attach(InteractApplication.add(z3Runner)); + chRunner.attach(AdapterApplication.add(z3Runner)); } // run on a fresh copy to avoid any interference with other // threads. if (doCegar) { cegarRunner = new CegarRunner(pwd); cegarRunner.configure(EcoreUtil.copy(reader.getSpec()), doneProps); - chRunner.attach(InteractApplication.add(cegarRunner)); + chRunner.attach(AdapterApplication.add(cegarRunner)); } } if (doITS || onlyGal) { @@ -186,11 +186,11 @@ 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.setInterprete(inRunner); + itsRunner.configureInterpreter(inRunner); } if (doITS) { - chRunner.attach(InteractApplication.add(itsRunner)); + chRunner.attach(AdapterApplication.add(itsRunner)); } if (onlyGal || doLTSmin) { @@ -208,8 +208,8 @@ public Object start(IApplicationContext context) throws Exception { ltsminRunner = new LTSminRunner(ltsminpath, solverPath, solver, doPOR, onlyGal, reader.getFolder(), 3600 / reader.getSpec().getProperties().size()); ltsminRunner.configure(reader.getSpec(), doneProps); - ltsminRunner.setInterprete(inRunner); - chRunner.attach(InteractApplication.add(ltsminRunner)); + ltsminRunner.configureInterpreter(inRunner); + chRunner.attach(AdapterApplication.add(ltsminRunner)); } } FutureTask executeRunner = new FutureTask<>(chRunner); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java index 3602613a38..6984d1e3af 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/CegarRunner.java @@ -11,7 +11,6 @@ import fr.lip6.move.gal.instantiate.CompositeBuilder; import fr.lip6.move.gal.instantiate.GALRewriter; import fr.lip6.move.gal.instantiate.Simplifier; -import fr.lip6.move.gal.itscl.interprete.InterpreteObservable; public class CegarRunner extends AbstractRunner { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java index 65f38508fb..169e7a384c 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java @@ -11,7 +11,7 @@ import fr.lip6.move.gal.Property; import fr.lip6.move.gal.Specification; import fr.lip6.move.gal.interpreter.ITSInterpreter; -import fr.lip6.move.gal.itscl.interprete.FileStreamInterprete; +import fr.lip6.move.gal.itscl.interpreter.FileStreamInterprete; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.CommandLineBuilder; import fr.lip6.move.gal.itstools.Runner; @@ -236,6 +236,8 @@ public String outputGalFile() throws IOException { return outpath; } + + public void setDone() { done = !done; } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java index 7ff2fa94de..3e5fbd0103 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java @@ -17,7 +17,7 @@ import fr.lip6.move.gal.gal2smt.Gal2SMTFrontEnd; import fr.lip6.move.gal.gal2smt.Solver; import fr.lip6.move.gal.interpreter.LTSminInterpreter; -import fr.lip6.move.gal.itscl.interprete.InterpreteBytArray; +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; @@ -121,17 +121,15 @@ private CommandLine generateLTSminCommand(Property prop, Gal2PinsTransformerNext } public Boolean taskDone() { -// inRunner.acquireFinalResult(); todo.removeAll(doneProps); return (todo.isEmpty()) ? true : false; } public void solve() { - InterpreteBytArray bufferWIO = new InterpreteBytArray(); - LTSminInterpreter interp = new LTSminInterpreter(this, bufferWIO); - + LTSminInterpreter interp = new LTSminInterpreter(this, bufferWIO); + long time = 0; try { System.out.println("Built C files in : \n" + new File(workFolder + "/")); @@ -183,7 +181,6 @@ public void solve() { Thread interpTh = new Thread(interp, "LTSminInterpreter"); inRunner.addThInterprete(interpTh); interpTh.start(); - System.out.println("I created it ! LTSmin"); time = System.currentTimeMillis(); @@ -198,7 +195,6 @@ public void solve() { CommandLine ltsmin = generateLTSminCommand(prop, g2p); try { - // dont know why it blocks at the 4th prop IStatus status = Runner.runTool(timeout, ltsmin, bufferWIO.getPout(), true); interp.notifyInterpreter(isdeadlock, isLTL, status, prop); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/AbstractInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/AbstractInterpreter.java deleted file mode 100644 index 271708d557..0000000000 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/AbstractInterpreter.java +++ /dev/null @@ -1,20 +0,0 @@ -package fr.lip6.move.gal.interpreter; - -import java.util.concurrent.Semaphore; - -public abstract class AbstractInterpreter implements IInterpreter { - private Semaphore hasComplete = new Semaphore(0); - - public void acquireResult() { - try { - hasComplete.acquire(); - } catch (InterruptedException e) { - e.printStackTrace(); - } - } - - public void releaseResult(){ - hasComplete.release(); - } - -} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java deleted file mode 100644 index d96d4c90b1..0000000000 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/CegarInterpreter.java +++ /dev/null @@ -1,14 +0,0 @@ -package fr.lip6.move.gal.interpreter; - -import fr.lip6.move.gal.itscl.interprete.FileStreamInterprete; - -public class CegarInterpreter extends FileStreamInterprete{ - - - public Boolean call() { - return null; - //interpretation of wat do we recieve in OutPut - } - - -} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/IInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/IInterpreter.java deleted file mode 100644 index dc2fed0ad0..0000000000 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/IInterpreter.java +++ /dev/null @@ -1,5 +0,0 @@ -package fr.lip6.move.gal.interpreter; - -public interface IInterpreter extends Runnable{ - -} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java index 1305e1ea6f..0da2c6cf7e 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java @@ -11,7 +11,8 @@ import fr.lip6.move.gal.Constant; import fr.lip6.move.gal.application.ITSRunner; import fr.lip6.move.gal.application.MccTranslator; -import fr.lip6.move.gal.itscl.interprete.FileStreamInterprete; +import fr.lip6.move.gal.itscl.interpreter.AbstractInterpreter; +import fr.lip6.move.gal.itscl.interpreter.FileStreamInterprete; public class ITSInterpreter extends AbstractInterpreter { @@ -23,7 +24,6 @@ public class ITSInterpreter extends AbstractInterpreter { private Set todoProps; private FileStreamInterprete buffWriteInOut; private ITSRunner itsRunner; - public ITSInterpreter(String examination, boolean withStructure, MccTranslator reader, Set doneProps, Set todoProps, ITSRunner itsRunner) { @@ -34,13 +34,11 @@ public ITSInterpreter(String examination, boolean withStructure, MccTranslator r this.todoProps = todoProps; this.itsRunner = itsRunner; } - public void setInput(FileStreamInterprete bufferWIO) { - this.buffWriteInOut=bufferWIO; + this.buffWriteInOut = bufferWIO; } - public void run() { try { for (String line = ""; line != null; line = buffWriteInOut.getWrittenData()) { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java index 0b6b559571..23c64c023e 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java @@ -9,7 +9,7 @@ import fr.lip6.move.gal.Property; import fr.lip6.move.gal.ReachableProp; import fr.lip6.move.gal.application.LTSminRunner; -import fr.lip6.move.gal.itscl.interprete.InterpreteBytArray; +import fr.lip6.move.gal.itscl.interpreter.InterpreteBytArray; public class LTSminInterpreter implements Runnable { @@ -31,19 +31,28 @@ public LTSminInterpreter(LTSminRunner ltSminRunner, InterpreteBytArray bufferWIO this.bufferWIO = bufferWIO; } - - private void waitRunner() throws InterruptedException { - waitRunner.acquire(); - } - + /** + * block {@link LTSminRunner} till it completes interpretation of the last + * result + */ public void waitInterpreter() throws InterruptedException { waitInterpreter.acquire(); } + /** + * wake {@link LTSminRunner} to continue the treatment of props + */ private void notifyRunner() { waitInterpreter.release(); } + /** + * sync between interpreter and runner + */ + private void waitRunner() throws InterruptedException { + waitRunner.acquire(); + } + public void notifyInterpreter(boolean isdeadlock, boolean isLTL, IStatus status, Property prop) { this.isdeadlock = isdeadlock; this.isLTL = isLTL; @@ -80,9 +89,10 @@ public void run() { // formula if (!completeProp) System.out.println("Runner was interrupted before completing the treatment. "); - result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting - // cycle found") - // ; + else + result = !(status.getCode() == 1); // output.toLowerCase().contains("accepting + // cycle found") + // ; } else { boolean hasViol = output.contains("Invariant violation"); @@ -113,13 +123,13 @@ public void run() { } } } + ltsRunner.addToDoneProps(prop.getName()); notifyRunner(); String ress = (result + "").toUpperCase(); System.out.println( "FORMULA " + prop.getName() + " " + ress + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); - } catch (InterruptedException e) { e.printStackTrace(); } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java deleted file mode 100644 index 8f49b873a4..0000000000 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/SMTInterpreter.java +++ /dev/null @@ -1,11 +0,0 @@ -package fr.lip6.move.gal.interpreter; - -import fr.lip6.move.gal.itscl.interprete.FileStreamInterprete; - -public class SMTInterpreter extends FileStreamInterprete { - - - public Boolean call() throws Exception { - return null; - } -}