From 5666a51b0cfcb8112c6dfa2fc6f8adafd6460890 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 29 Oct 2010 12:50:34 +0000 Subject: [PATCH] Possible bug fix: Termination of simulation check in GUI not detected (thread issue?). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2199 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../computation/SimulateModelCheckThread.java | 151 +++++++++--------- 1 file changed, 74 insertions(+), 77 deletions(-) diff --git a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java index d90a3fcc..596bbcce 100644 --- a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java @@ -55,19 +55,10 @@ public class SimulateModelCheckThread extends GUIComputationThread private int noIterations; private int maxPathLength; private SimulationInformation info; - + /** Creates a new instance of SimulateModelCheckThread */ - public SimulateModelCheckThread - (GUIMultiProperties parent, - ModulesFile m, - PropertiesFile prFi, - ArrayList guiProps, - Values definedMFConstants, - Values definedPFConstants, - Values initialState, - int noIterations, - int maxPathLength, - SimulationInformation info) + public SimulateModelCheckThread(GUIMultiProperties parent, ModulesFile m, PropertiesFile prFi, ArrayList guiProps, Values definedMFConstants, + Values definedPFConstants, Values initialState, int noIterations, int maxPathLength, SimulationInformation info) { super(parent); this.parent = parent; @@ -81,13 +72,14 @@ public class SimulateModelCheckThread extends GUIComputationThread this.maxPathLength = maxPathLength; this.info = info; } - + public void run() { boolean allAtOnce = prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS); - - if(mf == null) return; - + + if (mf == null) + return; + //Notify user interface of the start of computation SwingUtilities.invokeLater(new Runnable() { @@ -98,35 +90,29 @@ public class SimulateModelCheckThread extends GUIComputationThread parent.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_START, parent)); } }); - + //Set icon for all properties to be verified to a clock - for(int i = 0; i < guiProps.size(); i++) - { + for (int i = 0; i < guiProps.size(); i++) { GUIProperty gp = guiProps.get(i); gp.setStatus(GUIProperty.STATUS_DOING); parent.repaintList(); } - - IconThread ic = new IconThread(null); - + // do all at once if requested - if(allAtOnce) - { + if (allAtOnce) { Result results[] = null; Exception resultError = null; - ArrayList properties = new ArrayList (); + ArrayList properties = new ArrayList(); ArrayList clkThreads = new ArrayList(); - for(int i = 0; i < guiProps.size(); i++) - { + for (int i = 0; i < guiProps.size(); i++) { GUIProperty gp = guiProps.get(i); properties.add(gp.getProperty()); - ic = new IconThread(gp); - ic.start(); - clkThreads.add(ic); + IconThread ict = new IconThread(gp); + ict.start(); + clkThreads.add(ict); } - - try - { + + try { // display info logln("\n-------------------------------------------"); log("\nSimulating"); @@ -138,30 +124,36 @@ public class SimulateModelCheckThread extends GUIComputationThread logln(" " + properties.get(i)); } } - if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); - if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants); - log("Simulation parameters: approx = "+info.getApprox()+", conf = "+info.getConfidence()+", num samples = "+noIterations+", max path len = "+maxPathLength+")\n"); - + if (definedMFConstants != null) + if (definedMFConstants.getNumValues() > 0) + logln("Model constants: " + definedMFConstants); + if (definedPFConstants != null) + if (definedPFConstants.getNumValues() > 0) + logln("Property constants: " + definedPFConstants); + log("Simulation parameters: approx = " + info.getApprox() + ", conf = " + info.getConfidence() + ", num samples = " + noIterations + + ", max path len = " + maxPathLength + ")\n"); + // do simulation results = prism.modelCheckSimulatorSimultaneously(mf, pf, properties, initialState, noIterations, maxPathLength); - } - catch(PrismException e) - { + } catch (PrismException e) { // in the case of an error which affects all props, store/report it resultError = e; error(e.getMessage()); } //after collecting the results stop all of the clock icons - for(int i =0; i < clkThreads.size(); i++) - { - IconThread ict = (IconThread)clkThreads.get(i); + for (int i = 0; i < clkThreads.size(); i++) { + IconThread ict = (IconThread) clkThreads.get(i); ict.interrupt(); - while(!ict.canContinue) - {} + while (!ict.canContinue) { + try { + Thread.sleep(10); + } catch (InterruptedException e) { + return; + } + } } // store results - for(int i = 0; i < guiProps.size(); i++) - { + for (int i = 0; i < guiProps.size(); i++) { GUIProperty gp = guiProps.get(i); gp.setResult((results == null) ? new Result(resultError) : results[i]); gp.setMethodString("Simulation"); @@ -169,37 +161,43 @@ public class SimulateModelCheckThread extends GUIComputationThread } } // do each property individually - else - { + else { Result result = null; - for(int i = 0; i < pf.getNumProperties(); i++) - { + for (int i = 0; i < pf.getNumProperties(); i++) { // get property GUIProperty gp = guiProps.get(i); // animate it's clock icon - ic = new IconThread(gp); - ic.start(); + IconThread ict = new IconThread(gp); + ict.start(); // do model checking - try - { + try { logln("\n-------------------------------------------"); - logln("\nSimulating"+": " + pf.getProperty(i)); - if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); - if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants); - log("Simulation parameters: approx = "+info.getApprox()+", conf = "+info.getConfidence()+", num samples = "+noIterations+", max path len = "+maxPathLength+")\n"); - result = prism.modelCheckSimulator(mf, pf, pf.getProperty(i), initialState, noIterations, maxPathLength); - } - catch(PrismException e) - { + logln("\nSimulating" + ": " + pf.getProperty(i)); + if (definedMFConstants != null) + if (definedMFConstants.getNumValues() > 0) + logln("Model constants: " + definedMFConstants); + if (definedPFConstants != null) + if (definedPFConstants.getNumValues() > 0) + logln("Property constants: " + definedPFConstants); + log("Simulation parameters: approx = " + info.getApprox() + ", conf = " + info.getConfidence() + ", num samples = " + noIterations + + ", max path len = " + maxPathLength + ")\n"); + result = prism.modelCheckSimulator(mf, pf, pf.getProperty(i), initialState, noIterations, maxPathLength); + } catch (PrismException e) { result = new Result(e); error(e.getMessage()); } - ic.interrupt(); - while(!ic.canContinue) {} + ict.interrupt(); + while (!ict.canContinue) { + try { + Thread.sleep(10); + } catch (InterruptedException e) { + return; + } + } gp.setResult(result); gp.setMethodString("Simulation"); gp.setConstants(definedMFConstants, definedPFConstants); - + parent.repaintList(); } } @@ -214,12 +212,13 @@ public class SimulateModelCheckThread extends GUIComputationThread } }); } - + class IconThread extends Thread { GUIProperty gp; ImageIcon[] images; boolean canContinue = false; + public IconThread(GUIProperty gp) { this.gp = gp; @@ -233,25 +232,23 @@ public class SimulateModelCheckThread extends GUIComputationThread images[6] = GUIPrism.getIconFromImage("smallClockAnim7.png"); images[7] = GUIPrism.getIconFromImage("smallClockAnim8.png"); } + public void run() { - try - { + try { int counter = 0; - while(!interrupted() && gp != null) - { - //System.out.println("counter = "+counter); + while (!interrupted() && gp != null) { + //System.out.println("counter = " + counter); counter++; - counter = counter%8; + counter = counter % 8; gp.setDoingImage(images[counter]); parent.repaintList(); sleep(150); } + } catch (InterruptedException e) { + } finally { + canContinue = true; } - catch(InterruptedException e) - { - } - canContinue = true; } } }