From 65882ede90b37c09d446707e95785534fabf5631 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 6 Sep 2013 18:49:40 +0000
Subject: [PATCH] Better error reporting for non-supported explicit-state CTL.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7356 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/NonProbModelChecker.java | 69 +++++++++++++++++++++
 prism/src/explicit/ProbModelChecker.java    |  2 +-
 2 files changed, 70 insertions(+), 1 deletion(-)
 create mode 100644 prism/src/explicit/NonProbModelChecker.java

diff --git a/prism/src/explicit/NonProbModelChecker.java b/prism/src/explicit/NonProbModelChecker.java
new file mode 100644
index 00000000..c8e8180b
--- /dev/null
+++ b/prism/src/explicit/NonProbModelChecker.java
@@ -0,0 +1,69 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit;
+
+import parser.ast.Expression;
+import parser.ast.ExpressionExists;
+import parser.ast.ExpressionForAll;
+import prism.PrismComponent;
+import prism.PrismException;
+
+/**
+ * Explicit-state, non-probabilistic model checker.
+ */
+public class NonProbModelChecker extends StateModelChecker
+{
+	/**
+	 * Create a new NonProbModelChecker, inherit basic state from parent (unless null).
+	 */
+	public NonProbModelChecker(PrismComponent parent) throws PrismException
+	{
+		super(parent);
+	}
+	
+	@Override
+	public StateValues checkExpression(Model model, Expression expr) throws PrismException
+	{
+		StateValues res;
+
+		// E operator
+		if (expr instanceof ExpressionExists) {
+			throw new PrismException("CTL model checking is not yet supported by the explicit engine");
+		}
+		// A operator
+		else if (expr instanceof ExpressionForAll) {
+			throw new PrismException("CTL model checking is not yet supported by the explicit engine");
+		}
+		// Otherwise, use the superclass
+		else {
+			res = super.checkExpression(model, expr);
+		}
+
+		return res;
+	}
+}
+
diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index f7ee6c4a..9ed36d99 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -44,7 +44,7 @@ import explicit.rewards.MDPRewards;
 /**
  * Super class for explicit-state probabilistic model checkers.
  */
-public class ProbModelChecker extends StateModelChecker
+public class ProbModelChecker extends NonProbModelChecker
 {
 	// Flags/settings
 	// (NB: defaults do not necessarily coincide with PRISM)