From 2ab6add12f67fae51b92ddfc2194987217d2afd9 Mon Sep 17 00:00:00 2001
From: Sascha Wunderlich <sascha.wunderlich@tu-dresden.de>
Date: Fri, 12 Oct 2018 14:24:25 +0200
Subject: [PATCH] accumulation: fail on wrong engine

---
 prism/src/prism/ProbModelChecker.java | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index 37e48955..99244d38 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/prism/src/prism/ProbModelChecker.java
@@ -485,6 +485,8 @@ public class ProbModelChecker extends NonProbModelChecker
 
 		if (useSimplePathAlgo) {
 			return checkProbPathFormulaSimple(expr, qual, statesOfInterest);
+		} else if (Expression.containsAccumulationExpression(expr)) {
+			throw new PrismException("Model checking of accumulation expressions not supported for this engine!");
 		} else {
 			return checkProbPathFormulaLTL(expr, qual, statesOfInterest);
 		}