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 constructProductMC(DRA dra, DTMC dtmc, Vector 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: