From 724ac6983edec49f5a847b6afeacde4709df17ca Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 13 Nov 2013 10:06:27 +0000 Subject: [PATCH] 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 | 3 +++ prism/src/prism/PrismCL.java | 4 +++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index a565f61f..4be68c59 100644 --- a/prism/src/prism/Prism.java +++ b/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(); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 63a2a737..bc11cae5 100644 --- a/prism/src/prism/PrismCL.java +++ b/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(); }