Additional checks on arguments for parametric model checking.

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

prism/src/prism/Prism.java

@@ -2884,9 +2884,12 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	public Result modelCheckParametric(PropertiesFile propertiesFile, Property prop, String[] paramNames, String[] paramLowerBounds, String[] paramUpperBounds)
 			throws PrismException
 	{
+		// Some checks
 		if (paramNames == null) {
 			throw new PrismException("Must specify some parameters when using " + "the parametric analysis");
 		}
+		if (!(currentModelType == ModelType.DTMC || currentModelType == ModelType.CTMC || currentModelType == ModelType.MDP))
+			throw new PrismException("Parametric model checking is only supported for DTMCs, CTMCs and MDPs");
 
 		Values definedPFConstants = propertiesFile.getConstantValues();
 		Values constlist = currentModulesFile.getConstantValues();

prism/src/prism/PrismCL.java

@@ -1860,7 +1860,7 @@ public class PrismCL implements PrismModelListener
 
 	// do some processing of the options
 
-	private void processOptions()
+	private void processOptions() throws PrismException
 	{
 		int j;
 
@@ -1920,6 +1920,8 @@ public class PrismCL implements PrismModelListener
 					paramNames[pdNr] = paramDefSplit[0];
 					paramDefSplit[1] = paramDefSplit[1].trim();
 					String[] upperLower = paramDefSplit[1].split(":");
+					if (upperLower.length != 2)
+						throw new PrismException("Invalid range \"" + paramDefSplit[1] + "\" for parameter " + paramNames[pdNr]);
 					paramLowerBounds[pdNr] = upperLower[0].trim();
 					paramUpperBounds[pdNr] = upperLower[1].trim();
 				}