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

@@ -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)

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); }

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;

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); }

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)

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

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()

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); }

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'