ParamModelChecker: more helpful error messages for unsupported reward computations (co-safe LTL, ...)

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

prism/src/param/ParamModelChecker.java

@@ -83,6 +83,8 @@ import parser.ast.RewardStruct;
 import parser.type.TypeBool;
 import parser.type.TypeDouble;
 import parser.type.TypeInt;
+import parser.type.TypePathBool;
+import parser.type.TypePathDouble;
 import prism.ModelType;
 import prism.PrismComponent;
 import prism.PrismException;
@@ -1002,21 +1004,20 @@ final public class ParamModelChecker extends PrismComponent
 	private RegionValues checkRewardFormula(ParamModel model,
 			ParamRewardStruct rew, Expression expr, boolean min, BitSet needStates) throws PrismException {
 		RegionValues rewards = null;
-		
-		if (expr instanceof ExpressionTemporal) {
+
+		if (expr.getType() instanceof TypePathDouble) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			switch (exprTemp.getOperator()) {
-			case ExpressionTemporal.P_F:
-				rewards = checkRewardReach(model, rew, exprTemp, min, needStates);
-				break;
 			case ExpressionTemporal.R_S:
 				rewards = checkRewardSteady(model, rew, exprTemp, min, needStates);				
 				break;
 			default:
 				throw new PrismNotSupportedException("Parametric engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator");
 			}
+		} else if (expr.getType() instanceof TypePathBool || expr.getType() instanceof TypeBool) {
+			rewards = checkRewardPathFormula(model, rew, expr, min, needStates);
 		}
-		
+
 		if (rewards == null) {
 			throw new PrismException("Unrecognised operator in R operator");
 		}
@@ -1024,6 +1025,20 @@ final public class ParamModelChecker extends PrismComponent
 		return rewards;
 	}
 
+	/**
+	 * Compute rewards for a path formula in a reward operator.
+	 */
+	private RegionValues checkRewardPathFormula(ParamModel model, ParamRewardStruct rew, Expression expr, boolean min, BitSet needStates) throws PrismException
+	{
+		if (Expression.isReach(expr)) {
+			return checkRewardReach(model, rew, (ExpressionTemporal) expr, min, needStates);
+		} else if (Expression.isCoSafeLTLSyntactic(expr, true)) {
+			throw new PrismNotSupportedException("Parametric engine does not yet support co-safe reward computation");
+		} else {
+			throw new PrismException("R operator contains a path formula that is not syntactically co-safe: " + expr);
+		}
+	}
+
 	private RegionValues checkRewardReach(ParamModel model,
 			ParamRewardStruct rew, ExpressionTemporal expr, boolean min, BitSet needStates) throws PrismException {
 		RegionValues allTrue = regionFactory.completeCover(true);