Fix (again) computation of number of nondet choices for symbolic models (did not work for large number of nondet DD vars).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9848 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/NondetModel.java

@@ -268,15 +268,18 @@ public class NondetModel extends ProbModel
 				transInd = JDD.Or(transInd, JDD.ThereExists(tmp, allDDColVars));
 			}
 			JDD.Deref(tmp);
-			// update mask
-			JDD.Deref(nondetMask);
+			// update transition count
+			numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans());
+			// re-build mask for nondeterminstic choices
+			// (and work out number of choices)
 			JDD.Ref(trans01);
 			JDD.Ref(reach);
-			nondetMask = JDD.And(JDD.Not(JDD.ThereExists(trans01, allDDColVars)), reach);
-			// update model stats
-			numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans());
-			double d = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars());
-			numChoices = ((Math.pow(2, getNumDDNondetVars())) * numStates) - d;
+			if (this.nondetMask != null)
+				JDD.Deref(this.nondetMask);
+			nondetMask = JDD.And(JDD.ThereExists(trans01, allDDColVars), reach);
+			numChoices = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars());
+			JDD.Ref(reach);
+			nondetMask = JDD.And(JDD.Not(nondetMask), reach);
 		}
 	}