From 01c3826d8d64f39b088d42b10f163ebdb2665e5d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 12 Feb 2012 00:16:03 +0000 Subject: [PATCH] Less exceptions thrown from ResultCollection error setting methods, with knock-on effect (cleaner code) in various calling sites. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4598 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismCL.java | 46 ++++++------------- prism/src/prism/ResultsCollection.java | 20 ++++---- .../networking/SimulatorNetworkHandler.java | 10 +--- .../properties/GUIExperiment.java | 28 +++-------- 4 files changed, 32 insertions(+), 72 deletions(-) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 96f8f19f..b7d05cd4 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -209,12 +209,8 @@ public class PrismCL implements PrismModelListener // in case of error, report it, store as result for any properties, and go on to the next model // (might happen for example if overflow or another numerical problem is detected at this stage) error(e.getMessage()); - try { - for (j = 0; j < numPropertiesToCheck; j++) { - results[j].setMultipleErrors(definedMFConstants, null, e); - } - } catch (PrismException e2) { - error("Problem storing results"); + for (j = 0; j < numPropertiesToCheck; j++) { + results[j].setMultipleErrors(definedMFConstants, null, e); } // iterate to next model undefinedMFConstants.iterateModel(); @@ -275,11 +271,7 @@ public class PrismCL implements PrismModelListener } catch (PrismException e) { // in case of (overall) error, report it, store as result for property, and proceed error(e.getMessage()); - try { - results[j].setMultipleErrors(definedMFConstants, null, e); - } catch (PrismException e2) { - error("Problem storing results"); - } + results[j].setMultipleErrors(definedMFConstants, null, e); continue; } catch (InterruptedException e) { // ignore - won't get interrupted @@ -313,27 +305,19 @@ public class PrismCL implements PrismModelListener // in case of build failure during model checking, store as result for any const values and continue if (modelBuildFail) { - try { - results[j].setMultipleErrors(definedMFConstants, null, modelBuildException); - } catch (PrismException e2) { - error("Problem storing results"); - } + results[j].setMultipleErrors(definedMFConstants, null, modelBuildException); continue; } // store result of model checking - try { - results[j].setResult(definedMFConstants, definedPFConstants, res.getResult()); - Object cex = res.getCounterexample(); - if (cex != null) { - mainLog.println("\nCounterexample/witness:"); - mainLog.println(cex); - if (cex instanceof cex.CexPathAsBDDs){ - ((cex.CexPathAsBDDs) cex).clear(); - } + results[j].setResult(definedMFConstants, definedPFConstants, res.getResult()); + Object cex = res.getCounterexample(); + if (cex != null) { + mainLog.println("\nCounterexample/witness:"); + mainLog.println(cex); + if (cex instanceof cex.CexPathAsBDDs) { + ((cex.CexPathAsBDDs) cex).clear(); } - } catch (PrismException e) { - error("Problem storing results"); } // if required, check result against expected value @@ -358,12 +342,8 @@ public class PrismCL implements PrismModelListener // in case of build failure during model checking, store as result for any further properties, and go on to the next model if (modelBuildFail) { - try { - for (j++; j < numPropertiesToCheck; j++) { - results[j].setMultipleErrors(definedMFConstants, null, modelBuildException); - } - } catch (PrismException e2) { - error("Problem storing results"); + for (j++; j < numPropertiesToCheck; j++) { + results[j].setMultipleErrors(definedMFConstants, null, modelBuildException); } // iterate to next model undefinedMFConstants.iterateModel(); diff --git a/prism/src/prism/ResultsCollection.java b/prism/src/prism/ResultsCollection.java index 62a762d6..7301fc35 100644 --- a/prism/src/prism/ResultsCollection.java +++ b/prism/src/prism/ResultsCollection.java @@ -104,7 +104,7 @@ public class ResultsCollection /** * Sets the result for a particular set of values. */ - public int setResult(Values values, Object result) throws PrismException + public int setResult(Values values, Object result) { // store result int ret = root.setResult(values, result); @@ -125,7 +125,7 @@ public class ResultsCollection /** * Sets the result for a particular set of values. */ - public int setResult(Values mfValues, Values pfValues, Object result) throws PrismException + public int setResult(Values mfValues, Values pfValues, Object result) { // merge mfValues and pfValues Values merged = new Values(); @@ -143,7 +143,7 @@ public class ResultsCollection * Note: individual errors can be set using setResult(). That method could easily be adapted to store * multiple values but the DisplayableData aspect isn't sorted yet. */ - public int setMultipleErrors(Values values, Exception error) throws PrismException + public int setMultipleErrors(Values values, Exception error) { // store result int ret = root.setResult(values, error); @@ -161,7 +161,7 @@ public class ResultsCollection * Note: individual errors can be set using setResult(). That method could easily be adapted to store * multiple values but the DisplayableData aspect isn't sorted yet. */ - public int setMultipleErrors(Values mfValues, Values pfValues, Exception error) throws PrismException + public int setMultipleErrors(Values mfValues, Values pfValues, Exception error) { // merge mfValues and pfValues Values merged = new Values(); @@ -360,15 +360,19 @@ public class ResultsCollection * If any constants are left undefined, the same result will be set for all values of each constant. * Returns the total number of values which were set for the the first time. */ - public int setResult(Values setThese, Object result) throws PrismException + public int setResult(Values setThese, Object result) { - Object val; + Object val = null; int valIndex, ret, i, n; // if a value has been given for this node's constant, just store the result for this value if (setThese.contains(constant.getName())) { // get value of this node's constant - val = setThese.getValueOf(constant.getName()); + try { + val = setThese.getValueOf(constant.getName()); + } catch (PrismLangException e) { + // Ignore - already checked above + } // and convert to index valIndex = constant.getValueIndex(val); // store the value @@ -586,7 +590,7 @@ public class ResultsCollection { private Object val = null; - public int setResult(Values setThese, Object result) throws PrismException + public int setResult(Values setThese, Object result) { int ret = (val == null) ? 1 : 0; val = result; diff --git a/prism/src/simulator/networking/SimulatorNetworkHandler.java b/prism/src/simulator/networking/SimulatorNetworkHandler.java index fde65aeb..4e5e88a2 100644 --- a/prism/src/simulator/networking/SimulatorNetworkHandler.java +++ b/prism/src/simulator/networking/SimulatorNetworkHandler.java @@ -480,15 +480,7 @@ public class SimulatorNetworkHandler extends Observable implements EntityResolve Values pcs = (Values)propertyConstantRanges.get(i); double res = srf.getResult(i); Object result = (res < 0.0)?null:new Double(res); - try - { - resultsCollection.setResult(modelConstants, pcs, result); - } - catch(PrismException e) - { - //do nothing - } - + resultsCollection.setResult(modelConstants, pcs, result); } } diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index 595fb28b..58159015 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/prism/src/userinterface/properties/GUIExperiment.java @@ -164,12 +164,12 @@ public class GUIExperiment table.repaint(); } - public synchronized void setResult(Values mfValues, Values pfValues, Result res) throws PrismException + public synchronized void setResult(Values mfValues, Values pfValues, Result res) { results.setResult(mfValues, pfValues, res.getResult()); } - public synchronized void setMultipleErrors(Values mfValues, Values pfValues, Exception e) throws PrismException + public synchronized void setMultipleErrors(Values mfValues, Values pfValues, Exception e) { results.setMultipleErrors(mfValues, pfValues, e); } @@ -233,11 +233,7 @@ public class GUIExperiment } catch (PrismException e) { // in case of error, report it (in log only), store as result, and go on to the next model errorLog(e.getMessage()); - try { - setMultipleErrors(definedMFConstants, null, e); - } catch (PrismException e2) { - error("Problem storing results"); - } + setMultipleErrors(definedMFConstants, null, e); undefinedConstants.iterateModel(); continue; } @@ -251,11 +247,7 @@ public class GUIExperiment } catch (PrismException e) { // in case of error, report it (in log only), store as result, and go on to the next model errorLog(e.getMessage()); - try { - setMultipleErrors(definedMFConstants, null, e); - } catch (PrismException e2) { - error("Problem storing results"); - } + setMultipleErrors(definedMFConstants, null, e); undefinedConstants.iterateModel(); continue; } @@ -302,11 +294,7 @@ public class GUIExperiment } catch (PrismException e) { // in case of error, report it (in log only), store as result, and go on to the next model errorLog(e.getMessage()); - try { - setMultipleErrors(definedMFConstants, null, e); - } catch (PrismException e2) { - error("Problem storing results"); - } + setMultipleErrors(definedMFConstants, null, e); undefinedConstants.iterateModel(); continue; } @@ -351,11 +339,7 @@ public class GUIExperiment { public void run() { - try { - GUIExperiment.this.setResult(definedMFConstants, definedPFConstants, res); - } catch (PrismException e) { - error("Problem storing results"); - } + GUIExperiment.this.setResult(definedMFConstants, definedPFConstants, res); } });