From a325400ba27ae344cf016cc7d68b3edfeec4f520 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 30 Jun 2016 14:57:27 +0000
Subject: [PATCH] Sampler.createSampler: For reward properties, catch the new
 case of a co-safety path formula properly

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11446 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/simulator/sampler/Sampler.java | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/prism/src/simulator/sampler/Sampler.java b/prism/src/simulator/sampler/Sampler.java
index 469ad151..eca8f947 100644
--- a/prism/src/simulator/sampler/Sampler.java
+++ b/prism/src/simulator/sampler/Sampler.java
@@ -235,6 +235,11 @@ public abstract class Sampler
 			throw new PrismException("Invalid reward structure index \"" + rs + "\"");
 
 		// Construct sampler based on type
+		if (!(expr.getExpression() instanceof ExpressionTemporal) ||
+		    !(expr.isSimplePathFormula())) {
+			// catch co-safety reward specifications
+			throw new PrismException("Can't create sampler for property \"" + expr + "\"");
+		}
 		ExpressionTemporal exprTemp = (ExpressionTemporal) expr.getExpression();
 		switch (exprTemp.getOperator()) {
 		case ExpressionTemporal.R_C: