From 0ba3191214d6dc2902be8f7e507defb0792919a8 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 15 Nov 2010 15:30:09 +0000
Subject: [PATCH] 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                              |  1 +
 prism/src/parser/visitor/CheckValid.java | 14 ++++++++++++--
 prism/src/pta/DigitalClocks.java         |  8 ++------
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/prism/NOTES b/prism/NOTES
index 0cc18a9c..ed42c923 100644
--- a/prism/NOTES
+++ b/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
 
 =======================================================
 
diff --git a/prism/src/parser/visitor/CheckValid.java b/prism/src/parser/visitor/CheckValid.java
index 77ddbc7d..0f811476 100644
--- a/prism/src/parser/visitor/CheckValid.java
+++ b/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");
+		}
 	}
 }
diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java
index 09f3d0dd..e4f08152 100644
--- a/prism/src/pta/DigitalClocks.java
+++ b/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);