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..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 @@ -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-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/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..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 @@ -2,36 +2,41 @@ import java.io.IOException; import java.util.Set; +import java.util.concurrent.ConcurrentHashMap; import fr.lip6.move.gal.Specification; +import fr.lip6.move.gal.itscl.interpreter.IInterpreteObservable; +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; - public AbstractRunner() { - super(); - } + protected IInterpreteObservable inRunner; - @Override - public void interrupt() { - if (runnerThread != null) { - runnerThread.interrupt(); - } + public Specification getSpec() { + return spec; } - @Override - public void join() throws InterruptedException { - if (runnerThread != null) { - runnerThread.join(); - } + public void configureInterpreter(IInterpreteObservable ob) { + this.inRunner = ob; } - @Override public void configure(Specification z3Spec, Set doneProps) throws IOException { - this.spec = z3Spec ; + this.spec = z3Spec; this.doneProps = doneProps; } + public void configure(Specification spec) { + try { + configure(spec, ConcurrentHashMap.newKeySet()); + } catch (IOException e) { + e.printStackTrace(); + } + } + + public abstract void solve(); + + 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 875321898b..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 @@ -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,19 @@ 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.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; /** * 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 +45,44 @@ 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,139 @@ 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(); + InterpreteObservable inRunner = new InterpreteObservable(chRunner); + if (inRunner == null) { + System.out.println("is null"); + } 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(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(AdapterApplication.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); + itsRunner.configureInterpreter(inRunner); + } + + if (doITS) { + chRunner.attach(AdapterApplication.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); + ltsminRunner.configureInterpreter(inRunner); + chRunner.attach(AdapterApplication.add(ltsminRunner)); + } + } + FutureTask executeRunner = new FutureTask<>(chRunner); + FutureTask executeRunner2 = new FutureTask<>(inRunner); + Thread futureTh = new Thread(executeRunner); + Thread futureTh2 = new Thread(executeRunner2); + try { + futureTh.start(); + futureTh2.start(); + Boolean result = executeRunner.get(); + Boolean result2 = executeRunner2.get(); + System.out.println("Operation reussi ? " + result + "And Listener has complete correctly ? " + result2); + } 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 +255,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 +266,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 +295,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..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 @@ -6,118 +6,79 @@ 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 "); + private static Logger getLog() { + return Logger.getLogger("fr.lip6.move.gal"); - } 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(); - + } + + + public Boolean taskDone() { + for (Property prop : todoProps) { + if (!doneProps.contains(prop.getName())) { + // still some work to do + return false; } - }); - cegarRunner.start(); - return cegarRunner; + } + return true; } - private static Logger getLog() { - return Logger.getLogger("fr.lip6.move.gal"); + public void setInterpreter() { + // TODO Auto-generated method stub } - @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 void solve() { - 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"; - } + // 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); - 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."); - } - } - } - 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/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); - - -} 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..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 @@ -1,24 +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.stream.Collectors; -import org.eclipse.emf.common.util.TreeIterator; -import org.eclipse.emf.ecore.EObject; -import fr.lip6.move.gal.Constant; import fr.lip6.move.gal.Property; -import fr.lip6.move.gal.Reference; import fr.lip6.move.gal.Specification; +import fr.lip6.move.gal.interpreter.ITSInterpreter; +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; @@ -33,24 +26,20 @@ 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; + private ITSInterpreter interp; + + 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,216 +98,40 @@ 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)); + cl.setWorkingDir(new File(folder)); } } - - @Override - public void interrupt() { - super.interrupt(); - if (itsReader != null) { - itsReader.interrupt(); - } - } - - @Override - public void join() throws InterruptedException { - super.join(); - if (itsReader != null) { - itsReader.join(); - } - } - - 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(); @@ -330,8 +141,9 @@ public void run() { } } } + 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 +152,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 +166,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 +235,52 @@ public String outputGalFile() throws IOException { } return outpath; } + - @Override - public void solve(Ender ender) { - final PipedInputStream pin = new PipedInputStream(4096); - PipedOutputStream pout= null; - try { - pout = new PipedOutputStream(pin); - } catch (IOException e1) { - e1.printStackTrace(); - return; - } + + public void setDone() { + done = !done; + } + + public Boolean taskDone() { + interp.acquireResult(); + return done; + } + + /** + * Generate ITS interpreter + * + * Run both solver and interpreter and wait till termination of both threads + */ + public void solve() { + FileStreamInterprete bufferWIO = new FileStreamInterprete(); - Set todoProps = reader.getSpec().getProperties().stream().map(p -> p.getName()).collect(Collectors.toSet()); + todoProps = reader.getSpec().getProperties().stream().map(p -> p.getName()).collect(Collectors.toSet()); - runnerThread = new Thread (new ITSRealRunner(pout,cl)); + Thread runnerThread = new Thread(new ITSRealRunner(bufferWIO.getPout(), cl),"ITSRealRunner"); + interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, + this); + interp.setInput(bufferWIO); + Thread interpTh = new Thread(interp, "ITSInterpreter"); - ITSInterpreter interp = new ITSInterpreter(examination, reader.hasStructure(), reader, doneProps, todoProps, ender); - interp.setInput(pin); - itsReader = new Thread (interp); - itsReader.start(); - runnerThread.start(); + inRunner.addThInterprete(interpTh); + long time = System.currentTimeMillis(); + + try { + runnerThread.start(); + interpTh.start(); + runnerThread.join(); + interpTh.join(); + } catch (InterruptedException e) { + try { + runnerThread.interrupt(); + } catch (Exception ee) { + System.out.println("ITSRealRunner didn't interrupte"); + } + } catch (Exception e1) { + e1.printStackTrace(); + } + 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 245e1ae715..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 @@ -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; @@ -11,20 +10,19 @@ import org.eclipse.emf.ecore.EObject; 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.interpreter.LTSminInterpreter; +import fr.lip6.move.gal.itscl.interpreter.InterpreteBytArray; import fr.lip6.move.gal.itstools.CommandLine; import fr.lip6.move.gal.itstools.ProcessController.TimeOutException; import fr.lip6.move.gal.itstools.Runner; -public class LTSminRunner extends AbstractRunner implements IRunner { +public class LTSminRunner extends AbstractRunner { private String ltsminpath; private String solverPath; @@ -33,8 +31,12 @@ public class LTSminRunner extends AbstractRunner implements IRunner { private String workFolder; private Solver solver; private int timeout; + private List todo; + private boolean isdeadlock = false; + private boolean isLTL = false; - 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,176 @@ private static boolean isStutterInvariant(Property prop) { return true; } - @Override - public void solve(Ender ender) { - runnerThread = new Thread(new Runnable() { + private CommandLine linkCommandLine() { - @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); - } - } - { - // 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); - } - } - 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; - } - 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); - } - } 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 (TimeOutException to) { - System.err.println("LTSmin timed out on command " + ltsmin); - continue; - } + 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) { + + isdeadlock = false; + isLTL = false; + 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); + return (todo.isEmpty()) ? true : false; + } + + public void solve() { + + InterpreteBytArray bufferWIO = new InterpreteBytArray(); + LTSminInterpreter interp = new LTSminInterpreter(this, bufferWIO); + + long time = 0; + 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 = compilationCommandLine(); + + 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); } - todo.removeAll(doneProps); - if (todo.isEmpty()) { - ender.killAll(); + } catch (TimeOutException to) { + throw new RuntimeException("Compilation 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()); + + 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; + } + + CommandLine ltsmin = generateLTSminCommand(prop, g2p); + + try { + 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); } + } 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(); + } + interpTh.join(); + bufferWIO.getPout().close(); } - }); - runnerThread.start(); + 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); + } 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/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..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 @@ -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,59 @@ 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 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."); + 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 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."); - } - - } 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(); + // 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"); } + } \ No newline at end of file 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 new file mode 100644 index 0000000000..0da2c6cf7e --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/ITSInterpreter.java @@ -0,0 +1,187 @@ +package fr.lip6.move.gal.interpreter; + +import java.io.IOException; +import java.util.Set; + +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.ITSRunner; +import fr.lip6.move.gal.application.MccTranslator; +import fr.lip6.move.gal.itscl.interpreter.AbstractInterpreter; +import fr.lip6.move.gal.itscl.interpreter.FileStreamInterprete; + +public class ITSInterpreter extends AbstractInterpreter { + + // private Map> boundProps; + private String examination; + private boolean withStructure; + private MccTranslator reader; + private Set seen; + private Set todoProps; + private FileStreamInterprete buffWriteInOut; + private ITSRunner itsRunner; + + public ITSInterpreter(String examination, boolean withStructure, MccTranslator reader, Set doneProps, + Set todoProps, ITSRunner itsRunner) { + this.examination = examination; + this.withStructure = withStructure; + this.reader = reader; + this.seen = doneProps; + this.todoProps = todoProps; + this.itsRunner = itsRunner; + } + + public void setInput(FileStreamInterprete bufferWIO) { + this.buffWriteInOut = bufferWIO; + } + + 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")) { + 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); + } + } + } + + } + buffWriteInOut.closeIn(); + } catch (NumberFormatException e) { + e.printStackTrace(); + } catch (IOException e) { + e.printStackTrace(); + } + buffWriteInOut.closePinPout(); + + if (seen.containsAll(todoProps)) { + itsRunner.setDone(); + } + + 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 new file mode 100644 index 0000000000..23c64c023e --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/interpreter/LTSminInterpreter.java @@ -0,0 +1,139 @@ +package fr.lip6.move.gal.interpreter; + +import java.util.concurrent.Semaphore; + +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.interpreter.InterpreteBytArray; + +public class LTSminInterpreter implements Runnable { + + private IStatus status; + private boolean isLTL; + private boolean isdeadlock; + private InterpreteBytArray bufferWIO; + private Property prop; + private LTSminRunner ltsRunner; + private boolean completeProp; + + 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.nbProps = ltSminRunner.getSpec().getProperties().size(); + this.bufferWIO = bufferWIO; + } + + /** + * 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; + this.status = status; + this.prop = prop; + this.completeProp = true; + + waitRunner.release(); + } + + public void notifyInterpreter(boolean isdeadlock, boolean isLTL) { + + this.isdeadlock = isdeadlock; + this.isLTL = isLTL; + this.completeProp = false; + + waitRunner.release(); + } + + public void run() { + int i = 0; + while (i++ < nbProps) { + boolean result = false; + try { + + 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. "); + else + 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); + } + } + } + + 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(); + } + } + } + +}