From 2b6a966076342ae1d9d632e17651dadf033357e9 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 19 Jul 2013 21:14:29 +0000
Subject: [PATCH] DRA-DTMC product code works for any type of DTMC, not just
 DTMCSimple.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7099 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/LTLModelChecker.java | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java
index 2dae0715..3a646711 100644
--- a/prism/src/explicit/LTLModelChecker.java
+++ b/prism/src/explicit/LTLModelChecker.java
@@ -127,16 +127,11 @@ public class LTLModelChecker
 	 */
 	public Pair<Model, int[]> constructProductMC(DRA<BitSet> dra, DTMC dtmc, Vector<BitSet> labelBS) throws PrismException
 	{
-		if (!(dtmc instanceof DTMCSimple)) {
-			throw new PrismException("Expecting a DTMC here");
-		}
-
-		DTMCSimple modelDTMC = (DTMCSimple) dtmc;
 		DTMCSimple prodModel = new DTMCSimple();
 
 		int draSize = dra.size();
 		int numAPs = dra.getAPList().size();
-		int modelNumStates = modelDTMC.getNumStates();
+		int modelNumStates = dtmc.getNumStates();
 		int prodNumStates = modelNumStates * draSize;
 
 		// Encoding: