From c997b76f2a7354065fff026565aaf044a808eeea Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Mon, 28 Aug 2017 12:45:48 +0200
Subject: [PATCH] parametric / exact ValueComputer: treat MDP with maximum of 1
 choice per state as a DTMC, skip policy iteration

---
 prism/src/param/ValueComputer.java | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/prism/src/param/ValueComputer.java b/prism/src/param/ValueComputer.java
index a23370d1..2afd8fd4 100644
--- a/prism/src/param/ValueComputer.java
+++ b/prism/src/param/ValueComputer.java
@@ -285,6 +285,9 @@ final class ValueComputer extends PrismComponent
 		case DTMC:
 			return computeUnboundedMC(region, b1, b2, rew);
 		case MDP:
+			if (model.getMaxNumChoices() == 1) {
+				return computeUnboundedMC(region, b1, b2, rew);
+			}
 			return computeUnboundedMDP(region, b1, b2, min, rew);
 		default:
 			throw new PrismNotSupportedException("Parametric unbounded reachability computation not supported for " + model.getModelType());