From ea14a0a7b6c2c2d2a4af30695d4e750d2ba02cce Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 5 Jul 2011 08:05:26 +0000
Subject: [PATCH] Explicit engine: better error reporting of some unsupported
 properties.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3207 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/ProbModelChecker.java | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index 5ad92517..f27d9556 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -154,7 +154,9 @@ public class ProbModelChecker extends StateModelChecker
 		}
 
 		// Check for unhandled cases
-		// TODO
+		if (expr.getReward() != null)
+			throw new PrismException("Explicit engine does not yet handle bounded R operators");
+		// More? TODO
 
 		// For nondeterministic models, determine whether min or max rewards needed
 		if (modelType.nondeterministic()) {