Add restrictions on which reward properties supported by digital clocks, and remove complaint about existence of both state/transition rewards.

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

prism/NOTES

@@ -14,6 +14,7 @@ DOC!
 
 timelock reported as deadlock for digital
 verbose has new behaviour now?! (wrt filters)
+pta rewards with digital clocks
 
 =======================================================
 

prism/src/parser/visitor/CheckValid.java

@@ -46,11 +46,17 @@ public class CheckValid extends ASTTraverse
 
 	public void visitPost(ExpressionTemporal e) throws PrismLangException
 	{
-		if (e.getOperator() == ExpressionTemporal.R_S) {
-			if (modelType == ModelType.MDP) {
+		// R operator types restricted for some models
+		if (modelType == ModelType.MDP) {
+			if (e.getOperator() == ExpressionTemporal.R_S) {
 				throw new PrismLangException("Steady-state reward properties cannot be used for MDPs");
 			}
 		}
+		else if (modelType == ModelType.PTA) {
+			if (e.getOperator() == ExpressionTemporal.R_C || e.getOperator() == ExpressionTemporal.R_I || e.getOperator() == ExpressionTemporal.R_S) {
+				throw new PrismLangException("Only reachability (F) reward properties can be used for PTAs");
+			}
+		}
 		// Apart from CTMCs, we only support upper time bounds
 		if (e.getLowerBound() != null) {
 			if (modelType == ModelType.DTMC) {
@@ -85,8 +91,12 @@ public class CheckValid extends ASTTraverse
 
 	public void visitPost(ExpressionSS e) throws PrismLangException
 	{
+		// S operator only works for some models
 		if (modelType == ModelType.MDP) {
 			throw new PrismLangException("The S operator cannot be used for MDPs");
 		}
+		if (modelType == ModelType.PTA) {
+			throw new PrismLangException("The S operator cannot be used for PTAs");
+		}
 	}
 }

prism/src/pta/DigitalClocks.java

@@ -258,13 +258,9 @@ public class DigitalClocks
 			pf = (PropertiesFile) pf.accept(asttm);
 
 		// Change state rewards in reward structures to use time action
-		// TODO: need to check properties file and see if used in non-cumulative way
+		// (no need to change transition rewards)
+		// Note: only cumulative (F) properties supported currently.
 		for (RewardStruct rs : mf.getRewardStructs()) {
-			if (rs.getNumStateItems() == 0)
-				continue;
-			// TODO: handle this case
-			if (rs.getNumTransItems() > 0)
-				throw new PrismLangException("Translation of reward structures with both state/transition items is not yet supported");
 			n = rs.getNumItems();
 			for (i = 0; i < n; i++) {
 				RewardStructItem rsi = rs.getRewardStructItem(i);