From 7460297a7ae2a769f4097abeeb9056c4e041b776 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 9 Nov 2006 09:38:13 +0000 Subject: [PATCH] Fixed various possible sources of round-off error when converting doubles to ints/longs (see previous revision). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@133 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ExpressionConstant.java | 2 +- prism/src/prism/NondetModel.java | 8 ++++---- prism/src/prism/PrismUtils.java | 2 +- prism/src/prism/ProbModel.java | 6 +++--- prism/src/prism/SCCComputer.java | 2 +- prism/src/prism/StateListMTBDD.java | 4 ++-- prism/src/prism/StateProbsMTBDD.java | 2 +- prism/src/prism/StochModel.java | 6 +++--- prism/src/prism/StochModelChecker.java | 2 +- 9 files changed, 17 insertions(+), 17 deletions(-) diff --git a/prism/src/parser/ExpressionConstant.java b/prism/src/parser/ExpressionConstant.java index 0d8575e1..d5264731 100644 --- a/prism/src/parser/ExpressionConstant.java +++ b/prism/src/parser/ExpressionConstant.java @@ -214,7 +214,7 @@ public class ExpressionConstant extends Expression if(o instanceof Double) { dval = ((Double)o).doubleValue(); - ival = (int)dval; + ival = (int)Math.round(dval); bval = (ival==0) ? false : true; } else if(o instanceof Integer) diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index 6ec7abe2..5b2037b5 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -113,10 +113,10 @@ public class NondetModel implements Model // rewards public int getNumRewardStructs() { return numRewardStructs; } // stats - public long getNumStates() { return (numStates>Long.MAX_VALUE) ? -1 : (long)numStates; } - public long getNumTransitions() { return (numTransitions>Long.MAX_VALUE) ? -1 : (long)numTransitions; } - public long getNumChoices() { return (numChoices>Long.MAX_VALUE) ? -1 : (long)numChoices; } - public long getNumStartStates() { return (numStartStates>Long.MAX_VALUE) ? -1 : (long)numStartStates; } + public long getNumStates() { return (numStates>Long.MAX_VALUE) ? -1 : Math.round(numStates); } + public long getNumTransitions() { return (numTransitions>Long.MAX_VALUE) ? -1 : Math.round(numTransitions); } + public long getNumChoices() { return (numChoices>Long.MAX_VALUE) ? -1 : Math.round(numChoices); } + public long getNumStartStates() { return (numStartStates>Long.MAX_VALUE) ? -1 : Math.round(numStartStates); } // additional methods to get stats as strings public String getNumStatesString() { return PrismUtils.bigIntToString(numStates); } public String getNumTransitionsString() { return PrismUtils.bigIntToString(numTransitions); } diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java index 8c5a103b..f1739433 100644 --- a/prism/src/prism/PrismUtils.java +++ b/prism/src/prism/PrismUtils.java @@ -60,7 +60,7 @@ public class PrismUtils public static String bigIntToString(double d) { if (d <= Long.MAX_VALUE) { - return "" + (long)d; + return "" + Math.round(d); } else { return "" + d; diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index 4deec460..7e4c8a40 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -108,9 +108,9 @@ public class ProbModel implements Model // rewards public int getNumRewardStructs() { return numRewardStructs; } // stats - public long getNumStates() { return (numStates>Long.MAX_VALUE) ? -1 : (long)numStates; } - public long getNumTransitions() { return (numTransitions>Long.MAX_VALUE) ? -1 : (long)numTransitions; } - public long getNumStartStates() { return (numStartStates>Long.MAX_VALUE) ? -1 : (long)numStartStates; } + public long getNumStates() { return (numStates>Long.MAX_VALUE) ? -1 : Math.round(numStates); } + public long getNumTransitions() { return (numTransitions>Long.MAX_VALUE) ? -1 : Math.round(numTransitions); } + public long getNumStartStates() { return (numStartStates>Long.MAX_VALUE) ? -1 : Math.round(numStartStates); } // additional methods to get stats as strings public String getNumStatesString() { return PrismUtils.bigIntToString(numStates); } public String getNumTransitionsString() { return PrismUtils.bigIntToString(numTransitions); } diff --git a/prism/src/prism/SCCComputer.java b/prism/src/prism/SCCComputer.java index b7dbbb40..49ee83cb 100644 --- a/prism/src/prism/SCCComputer.java +++ b/prism/src/prism/SCCComputer.java @@ -139,7 +139,7 @@ public class SCCComputer // } // mainLog.print("States not in BSCCs:\nx: "); // JDD.PrintVector(notInBSCCs, allDDRowVars); - mainLog.println(" Transient states: " + (int)JDD.GetNumMinterms(notInBSCCs, allDDRowVars.n())); + mainLog.println(" Transient states: " + JDD.GetNumMintermsString(notInBSCCs, allDDRowVars.n())); } // pick a random (actually the first) state from set (set not empty) diff --git a/prism/src/prism/StateListMTBDD.java b/prism/src/prism/StateListMTBDD.java index d602c855..7a542019 100644 --- a/prism/src/prism/StateListMTBDD.java +++ b/prism/src/prism/StateListMTBDD.java @@ -89,12 +89,12 @@ public class StateListMTBDD implements StateList public int size() { - return (size > Integer.MAX_VALUE) ? -1 : (int)size; + return (size > Integer.MAX_VALUE) ? -1 : (int)Math.round(size); } public String sizeString() { - return (size > Long.MAX_VALUE) ? "" + size : "" + (long)size; + return (size > Long.MAX_VALUE) ? "" + size : "" + Math.round(size); } // print whole list diff --git a/prism/src/prism/StateProbsMTBDD.java b/prism/src/prism/StateProbsMTBDD.java index 9793f11d..ac74e5ff 100644 --- a/prism/src/prism/StateProbsMTBDD.java +++ b/prism/src/prism/StateProbsMTBDD.java @@ -138,7 +138,7 @@ public class StateProbsMTBDD implements StateProbs public int getNNZ() { double nnz = JDD.GetNumMinterms(probs, numDDRowVars); - return (nnz > Integer.MAX_VALUE) ? -1 : (int)nnz; + return (nnz > Integer.MAX_VALUE) ? -1 : (int)Math.round(nnz); } public String getNNZString() diff --git a/prism/src/prism/StochModel.java b/prism/src/prism/StochModel.java index 56b0ef81..1571c09c 100644 --- a/prism/src/prism/StochModel.java +++ b/prism/src/prism/StochModel.java @@ -108,9 +108,9 @@ public class StochModel implements Model // rewards public int getNumRewardStructs() { return numRewardStructs; } // stats - public long getNumStates() { return (numStates>Long.MAX_VALUE) ? -1 : (long)numStates; } - public long getNumTransitions() { return (numTransitions>Long.MAX_VALUE) ? -1 : (long)numTransitions; } - public long getNumStartStates() { return (numStartStates>Long.MAX_VALUE) ? -1 : (long)numStartStates; } + public long getNumStates() { return (numStates>Long.MAX_VALUE) ? -1 : Math.round(numStates); } + public long getNumTransitions() { return (numTransitions>Long.MAX_VALUE) ? -1 : Math.round(numTransitions); } + public long getNumStartStates() { return (numStartStates>Long.MAX_VALUE) ? -1 : Math.round(numStartStates); } // additional methods to get stats as strings public String getNumStatesString() { return PrismUtils.bigIntToString(numStates); } public String getNumTransitionsString() { return PrismUtils.bigIntToString(numTransitions); } diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index cf136da1..1d1c40ad 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/prism/src/prism/StochModelChecker.java @@ -2436,7 +2436,7 @@ public class StochModelChecker implements ModelChecker // avoid a call to GetNumMinterms in this simple (and common) case n = numStates; } else { - n = (long)JDD.GetNumMinterms(subset, allDDRowVars.n()); + n = Math.round(JDD.GetNumMinterms(subset, allDDRowVars.n())); } // special case - there is only one state in 'subset'