Fix 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@9845 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/NondetModel.java

@@ -223,16 +223,17 @@ public class NondetModel extends ProbModel
 		}
 
 		// build mask for nondeterminstic choices
+		// (and work out number of choices)
 		JDD.Ref(trans01);
 		JDD.Ref(reach);
 		if (this.nondetMask != null)
 			JDD.Deref(this.nondetMask);
 		// nb: this assumes that there are no deadlock states
-		nondetMask = JDD.And(JDD.Not(JDD.ThereExists(trans01, allDDColVars)), reach);
-
-		// work out number of choices
-		double d = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars());
-		numChoices = ((Math.pow(2, getNumDDNondetVars())) * numStates) - d;
+		nondetMask = JDD.And(JDD.ThereExists(trans01, allDDColVars), reach);
+		numChoices = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars());
+		JDD.Ref(reach);
+		nondetMask = JDD.And(JDD.Not(nondetMask), reach);
+		JDD.PrintInfo(nondetMask, getNumDDRowVars() + getNumDDNondetVars());
 	}
 
 	@Override